Understanding DPLL algorithm

Problem Detail: 

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!

Asked By : DaZzz

Answered By : Pål GD

It works because the three cases you mention will remove every non-pure variable after some number of steps, but it is crucial that you also consider the recursive step, namely $\mbox{dpll}(\phi \land l) \lor \mbox{dpll}(\phi \land \neg l)$.

After a recursive step, you are guaranteed to have at least one unit clause, so the unit clause will be set to its value and hence all the variable will in the end be assigned a value.

I think your misunderstanding must arise from the recursive calls. Observe that if you have any formula $\phi = ((a \lor b \lor c) \land \cdots)$, then $\mbox{choose-literal}(\phi)$ will return some unassigned variable, say $a$. The recursive call will then be with $\phi \land a$ which will be $(a \lor b \lor c) \land \cdots) \land (a)$. And then $\mbox{unit-literal}(\phi)$ will return $a$ and set it to true. The other recursive call is equivalent, but with $\phi \land (\neg a)$ so $\mbox{unit-literal}(\phi)$ will still return $a$ and set $a$ to false.

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/10932