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?



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.

  • $\begingroup$ Were my examples correct? And what does empty clause mean? Does it mean that all variables were assigned or what? Well, just in this case if all variables were assigned it means that we were succeeded and we should return true, but algorithm says that we should return false in this case. So I'm a little bit confused. $\endgroup$
    – DaZzz
    Mar 31 '13 at 14:19
  • $\begingroup$ The empty clause corresponds to a conjunction over the empty set, which is considered to be vacuously false. The empty clause can be made by the unit propagation function. This function finds some unit clause $\cdots \land (l) \land \cdots$, sets all occurrences of $l$ to true and removes every occurrence of $\neg l$. Hence, if there also is a $(\neg l)$, this will be replaced by $()$ and after recursing, this will return false. $\endgroup$
    – Pål GD
    Mar 31 '13 at 15:06
  • $\begingroup$ I meant a disjunction over the empty set, sorry about that. And that is usually considered to be vacuously false. A conjunction over the empty set is usually considered vacuously true. Just think of a disjunction as "there exists bla bla true" and a conjunction as "for all bla bla true". Then you see how that works when you do disjunctions/conjunctions over sets. $\endgroup$
    – Pål GD
    Mar 31 '13 at 18:05

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

  1. A literal is a variable or its negation: $a$ or $\neg a$ for example.
  2. A clause is a disjunction of literals: $a \lor b$
  3. A unit clause contains only one literal: $\neg a$ is an example
  4. 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$.
  5. A conjunctive normal form (CNF) formula is a conjunction of clauses: $(a \lor b)\land(\neg a)$
  6. 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.

  1. 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.
  2. 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.
  3. 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.

  • $\begingroup$ By the way - do you know that you can vote for the answers if you like them? Not accept, just vote, which you don't seem to have done. Especially if you found the answers helpful. $\endgroup$
    – Vijay D
    Apr 1 '13 at 16:38
  • $\begingroup$ Yes, I do. I'd like to vote but I still don't have enough reputation for voting (15 points). I'll fix this in nearest feature but now just thank you very much. :) $\endgroup$
    – DaZzz
    Apr 1 '13 at 17:53
  • $\begingroup$ I didn't realise that. Sorry! $\endgroup$
    – Vijay D
    Apr 1 '13 at 18:17
  • $\begingroup$ Hello, I couldn't understand the sentence in the DPLL algorithm "if Φ is a consistent set of literals then return true;" can you explain it for me? $\endgroup$
    – Hari
    Nov 5 '13 at 4:13
  • 2
    $\begingroup$ If $\Phi$ is a set of literals, then every clause is a unit clause. As long as there is no contradictory pair, the conjunction will be consistent and the formula is satisfiable. $\endgroup$
    – Vijay D
    Nov 5 '13 at 5:49

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.