If satisfiable is returned by the algorithm,
then you can see that all involved unit clauses yield a satisfying assignment.
So then we have proved that a formula is satisfiable.
In the remaining case,
we can consider the algorithm as finding
a big case analysis and if never satisfiable is returned,
then it's a big case analysis ending at
every case in the empty clause being a contradiction.
So we can say, we have split up the whole formula in several cases.
Every case yields a contradiction and that has
approved that our formula is unsatisfiable.
So, DPLL is a complete method to establish satisfiability.
Let's consider an example.
Here we have a CNF consisting of
nine clauses and we want to establish whether this formula is satisfiable or not.
We see that no unit resolution is possible
since none of the nine clauses is a unit clause.
So we have to choose a variable and do a case analysis on this variable.
Let's choose variable p. That means first we add p,
but if we add p as an extra clause,
we can do unit resolution.
The two red clauses contain "Not p",
so there we can do unit resolution and we may remove "Not
p" from these two clauses yielding to new unit clauses,
"Not s" and "Not r".
But now, we may do a unit resolution on these new clauses,
"Not s" and "Not r".
If we do so, we can apply then on the two red clauses if we see
the clause q or s unit resolution with "Not s" yields the new unit clause, q.
If we consider the clause r or t,
unit resolution with "Not r" yields the new unit clause,
t and we can continue.
Now we have q and t. If we look at the red clause "Not q" or "Not t",
and we have our clause q,
we can derive the new clause "Not t".
But now we see we have t and "Not t" which yields a contradiction.
It can be seen as a unit resolution step,
but in any case, we derived the empty clause.
So, this ends this first case in which we added p. In the remaining case,
we have to add "Not p".
Well, if we add "Not p",
we can do unit resolution on the two red clauses p
or r and p or s yielding two new unit clauses,
r and s. Again,
using r and using s,
we can derive two new unit clauses q and t. Using q and to the clause,
"Not q or "Not t",
we can derive a new unit clause, "Not t".
Now we have both the unit clause t and "Not t" yielding the empty clause.
So also, in the second case,
we have bottom, we have derived a contradiction.
So in both cases,
we a found contradiction showing that this formula is unsatisfiable.
In this simple example,
we only have two cases typically in more complicated examples.
This goes on recursively several times and we can have thousands of cases to consider.
Let's consider a next example consisting of only eight clauses.
In fact, it's the same example as before,
only the last clause has been removed.
Again we see that in the starting CNF,
there is no unit clause so we should start by case analysis and again,
let's choose p as the variable on which we do case analysis.
Well, the case for p,
adding p is exactly the same,
yields a contradiction s in the example which you saw.
But in the next case,
we have "Not p".
We add "Not p" to this formula and then we can do unit resolution
yielding r and s as two new unit clauses based on the two red clauses,
p or r and p or s. If we continue,
we have the clause s and we have the clause "Not s" or t,
unit resolution yields t. Once we have t,
we have the clause "Not q" or "Not t",
we can derive the clause "Not q".
How to continue?
We see we have added "Not p",
we have derived r, we have derived s,
we have derived t,
and we have derived "Not q".
So, for every letter,
we have either the variable itself or its
negation in the list and if we do the unit resolution,
where we remove everything as indicated, nothing remains.
So here we are in the situation where nothing remains.
Now we can see that indeed,
"Not p", "Not q",
r, s, and, t yields a satisfying assignment which is easily checked.
But, it's also easily checked that in a general setting,
this holds as soon as we find
satisfiable then the corresponding values yield a satisfying assignment.
Concluding, we can state that this algorithm
DPLL is a complete method for satisfiability,
based on unit resolution and case analysis.
The efficiency of this algorithm strongly depends on the choice of the variable.
If no unit resolution is possible anymore,
we have to choose a variable and typically if we apply this on the big formula,
there is a lot of choice and
some choice will lead to much more efficient computation than others.
In fact, current SAT solvers follow this scheme combined
with good heuristics for variable choice and several optimizations. Thank you.
