Understanding DPLL algorithm

I'm trying to understand DPLL algorithm for solving SAT problem. And here it is:

Algorithm DPLL
  Input: A set of clauses Φ.
  Output: A Truth Value.
function DPLL(Φ)
   if Φ is a consistent set of literals
       then return true;
   if Φ contains an empty clause
       then return false;
   for every unit clause l in Φ
      Φ ← unit-propagate(l, Φ);
   for every literal l that occurs pure in Φ
      Φ ← pure-literal-assign(l, Φ);
   l ← choose-literal(Φ);
   return DPLL(Φ ∧ l) or DPLL(Φ ∧ not(l));

At first, I don't clearly understand how unit-propagate(l, Φ), pure-literal-assign(l, Φ) and choose-literal(Φ) work. I'll try to guess on particular examples. Correct me please if I do something wrong.

-
For the first one

unit-propagate(a, (0 v -a) ∧ (a v b) ∧ (b v d) ∧ (f v g) v ...)

we will have

((0 v -0) ∧ (0 or 1) ∧ (1 v d) ∧ (f v g) ∧ ... = (f v g) v ...,

having a = 0, b = 1.

-
For second procedure

pure-literal-assign(a, (a v b v c) ∧ (d v -b v a) ∧ (-d v b))

result is

(b v c) ∧ (d v -b) ∧ (-d v b),

assigning a = 1.

-
And finally choose-literal(Φ) just returns some random (in common case) unassigned literal for further computations.

Now, I don't understand why algorithm has such strange conditions for finishing? Why does it work?

Thanks!

I think your problem is not the algorithm itself but a few surrounding notions.

• A literal is a variable or its negation: $a$ or $\neg a$ for example.

• A clause is a disjunction of literals: $a \lor b$

• A unit clause contains only one literal: $\neg a$ is an example

• The empty clause contains no literals and is written $\{\}$ or $()$ or $\Box$. The empty clause is not satisfiable and you can think of it as equivalent to $False$.

• A conjunctive normal form (CNF) formula is a conjunction of clauses: $(a \lor b)\land(\neg a)$

• The empty formula contains no clauses and is written $\emptyset$. The empty formula is satisfied by every assignment and you can think of it as $True$.

Please notice the difference between an empty clause and an empty formula. These are the basic objects that the algorithms manipulates. Now we come to the operations.

• The unit rule says that if we have a unit clause $\neg a$ and a clause $a \lor \theta$, then to satisfy the formula, we must satisfy the clause $\theta$. This is because to satisfy the unit clause $\neg a$, the variable $a$ must be set to $False$ meaning, we cannot satisfy $a$, so we must satisfy $\theta$. Unit propagation repeatedly applies the unit rule.

• Observe that in implementing the unit rule as above, we are deleting unsatisfiable literals from a clause and leaving only literals that may help satisfy the clause. If we delete all literals, we have the empty clause, which means that no constraint of that clause is satisfiable, in turn meaning that the entire formula is not satisfiable.

• The pure literal rule is based on the observation that if a variable occurs only with one polarity in the entire formula, meaning we either only have $a$ or only have $\neg a$ in the formula, then there is never going to be a constraint of the form $a \land (\neg a \lor b)$ in the formula. So we can make that literal true. This will satisfy every clause in which that literal occurs, so we can delete those entire clauses.

There is a difference between unit propagation and the pure literal rule. Unit propagation deletes literals from inside a clause and brings us closer to discovering if there is an empty clause, in which case the formula is not satisfiable. The pure literal rule deletes entire clauses and brings us closer to the empty formula, in which case the formula is trivially satisfiable.

If you consider the two cases above, you see that it does not cover all possible behaviour. Specifically there may not be any unit clauses and there may not be any pure literals. In this case, to make progress, we pick a literal that does not occur in a unit clause and assign it a value. The choose-literal step can be viewed as adding a unit clause to the formula, which has the effect of triggering more unit propagations.

StackExchange Computer Science Q#10932, answer score: 6