This post is primarily directed at students in the AI class at University Erlangen to explain the Davis-Putnam (Logemann-Loveland) Algorithm for SAT solving and implication graphs for clause learning.

The goal in a SAT problem is to find an assignment that satisfies a set of propositional formulae \Delta, or a proof that none exist, i.e. that the set is unsatisfiable. DPLL is closely related to the resolution calculus, and as with resolution we first transform \Delta to a set of clauses \Delta=\{L_1, \ldots, L_n\}, where each clause L_i is a set of literals L_i=\{ \ell_{i1}, \ldots, \ell_{in_i}\}, where a literal \ell is either a propositional variable or the negation of a propositional variable. We write \ell=A^T if \ell is the propositional variable A and \ell=A^F if it is the negation of A. Then \Delta corresponds to the formula

\displaystyle\bigwedge_{L\in\Delta}\bigvee_{\ell\in L}\ell=\bigwedge_{i=1}^n\bigvee_{j=1}^{n_i}\ell_{ij}

in conjunctive normal form (CNF).

The basic algorithm \textsf{DPLL} takes a clause set \Delta and a partial assignment I: V\to\{0,1\} (where V is the set of propositional variables) as arguments (starting with the empty assignment) and returns either a partial assignment that satisfies \Delta or \textsf{unsatisfiable} if none exist. It proceeds as follows:

  1. Unit Propagation: If \Delta contains a unit, that is a clause L=\{ \ell \} with just one literal, then we extend our current assignment by that literal; meaning if L=\{ A^T \}, then we let I(A)=1 and if L=\{ A^F \} we let I(A)=0. Then we simplify (more on that later) \Delta with our new assignment and repeat.
  2. When \Delta contains no units anymore, we check whether \Delta is now empty; if so, we are done and we return our current assignment I. If not, we check whether \Delta now contains an empty clause; if so, we return \textsf{unsatisfiable}.
  3. Splitting: So \Delta now is not empty, contains no empty clauses and contains no units. We’re left with guessing an assignment, so we pick one propositional variable A on which our assignment I is currently undefined, let I(A)=1, simplify \Delta with our new assignment and recurse. If \textsf{DPLL}(\Delta,I) returns an assignment, that means we guessed currently and we return that. If it returns \textsf{unsatisfiable}, we guessed wrong and instead let I(A)=0, simplify and recurse with that.
  • By simplify I mean: If in our current assignment we have I(A)=1 (or I(A)=0 respectively), then we delete from \Delta all clauses that contain the literal A^T (respectively A^F). In the remaining clauses, we eliminate the literal A^F (respectively A^T).

Now why does this work? Let’s start with unit propagation: If \Delta contains a unit literal \{ A^T \}, then the formula corresponding to our clause set looks like this: \displaystyle L_1\wedge\ldots\wedge L_n\wedge A and obviously, for this formula to be satisfied, we need to set I(A)=1. Conversely, if we have the unit literal \{ A^F \}, then the formula looks like this: \displaystyle L_1\wedge\ldots\wedge L_n\wedge \neg A and we obviously need to set I(A)=0 to satisfy \Delta. Now for simplification: If we assign I(A)=1, then any clause that contains the literal A^T will be satisfied by I, since clauses are interpreted as the disjunction of its literals. Consequently, we can ignore these clauses from now on. The remaining clauses however will still need to be satisfied, and if we have I(A)=1, then we know that the literal A^F will be false anyway, which means we can ignore it in any disjunction (i.e. clause) containing it.


Example: Let \Delta = \{ \{P^F, Q^F, R^T\}, \{P^F,Q^F,R^F\}, \{ P^F, Q^T, R^T\}, \{P^F, Q^T, R^F\} \}. Then \textsf{DPLL}(\Delta,\{\}) proceeds like this:

  • We have no unit clauses, our assignment is empty, no clause is empty and \Delta isn’t empty, so we can only split. We pick the variable P:
    1. We let I(P)=1 and simplify, yielding \Delta_1 = \{ \{Q^F, R^T\}, \{Q^F, R^F\}, \{Q^T, R^T\}, \{Q^T, R^F\} \}. We have no unit clauses, no clause is empty and \Delta_1 isn’t empty, so we can only split. We pick the variable Q:
      1. We let I(Q)=1 and simplify, yielding \Delta_2 = \{ \{R^T\}, \{R^F\} \}. We have a unit clause, so we do unit propagation by letting I(R)=1 and simplifying. Unfortunately, that yields \Delta_3=\{ \{\} \} containing the empty clause, so we return \textsf{unsatisfiable}.
      2. Since the former branch failed, we let I(Q)=0 and simplify, yielding \Delta_2 = \{ \{R^T\}, \{R^F\} \}. We have a unit clause, so we do unit propagation by letting I(R)=1 and simplifying. Again, that yields \Delta_3=\{ \{\} \} containing the empty clause, so we return \textsf{unsatisfiable}
    2. The former branch failed, so we let I(P)=0 and simplify, yielding \Delta_1 = \{\}. \Delta_1 is empty, so we return the current assignment I=\{P\to0\}.

Apart from unit propagation and simplification, all that \textsf{DPLL} does is guessing assignments and backtracking if it fails. As such, it can very easily happen that the algorithm tries the same failing partial assignment again and again; e.g. because somewhere along the way it splits on a propositional variable that has nothing to do with why it failed before. A nice example of how this can happen is, if we have basically independent clauses that don’t share any propositional variables in the first place:

Example: We take the clause set from before and pointlessly extend it by the independent clauses \{ X_1^T, \ldots, X_{100}^T \} and \{ X_1^F, \ldots, X_{100}^F \}. Obviously, these are basically two independent SAT problems that don’t share any propositional variables. But as we’ve seen before, if we start with I(P)=1 our original clause set will necessarily fail, but the algorithm will only notice once Q (and R) have been assigned as well. If our \textsf{DPLL} run will start with P=1, but (in the worst case) then continue with X_1,\ldots X_{100} first, it will try the same assignments for Q and R again and again:

(Image taken from Michael’s lecture notes)


This is where clause learning comes into play: If we fail, we want to figure out why we failed and make sure we don’t make the same mistake all over again. One way to do this is with implication graphs, that systematically capture which chosen assignments lead to a contradiction (or imply which other assignments via unit propagation). An implication graph is a directed graph whose nodes are literals and the symbols \Box_L (representing the clause L becoming empty, i.e. a failed attempt). We construct such a graph during runtime of \textsf{DPLL}:

  • If at any point a clause L=\{\ell_1,\ldots,\ell_n, u\} becomes the unit clause \{ u \}, then for each literal \ell\in L with \ell\neq u we add an edge from \overline{\ell} to u (where \overline \ell is the negation of the literal \ell).
    The intuition behind this being, that when we do unit propagation, we’re using the fact the formula \ell_1 \vee \ldots \vee \ell_n \vee u is logically equivalent to (\overline{\ell_1} \wedge \ldots \wedge \overline{\ell_n}) \to u. The new edge is (sort-of) supposed to capture this implication.
  • If at any point a clause L=\{\ell_1,\ldots,\ell_n\} becomes empty, then for each literal \ell\in L we add an edge from \overline{\ell} to \Box_L.
    Here we are using the fact, that the formula \ell_1 \vee \ldots \vee \ell_n is logically equivalent to (\overline{\ell_1} \wedge \ldots \wedge \overline{\ell_n}) \to \bot.

Before we answer the question why we’re doing this, let’s go back to our previous example and construct the implication graph to the first contradiction. To keep track of which clause a literal is coming from, let’s name them:

Example: Let again \Delta = \{ L_1, L_2, L_3, L_4 \} where L_1=\{P^F, Q^F, R^T\}, L_2=\{P^F,Q^F,R^F\}, L_3=\{ P^F, Q^T, R^T\} and L_4=\{P^F, Q^T, R^F\} \}. Then \textsf{DPLL}(\Delta,\{\}) proceeds like this:

  • We start by splitting at the variable P:
    1. We let I(P)=1 and simplify, yielding \Delta_1 = \{ L_1=\{Q^F, R^T\}, L_2=\{Q^F, R^F\}, L_3=\{Q^T, R^T\}, L_4=\{Q^T, R^F\} \}. Then we split at the variable Q:
      1. We let I(Q)=1 and simplify, yielding \Delta_2 = \{ L_1=\{R^T\}, L_2=\{R^F\} \}. L_1 is now a unit clause. Apart from R^T, the original L_1 also contained the literals P^F and Q^F, so we add to our graph two new edges to R^T, one from P^T and one from Q^T (remember: from the negations of the original literals!).Now we do unit propagation , resulting in L_2 becoming the empty clause. The original L_2 contained the literals P^FQ^F and R^F, so we add edges from P^TQ^T and R^T to \Box_{L_2} and return \textsf{unsatisfiable}.

The resulting graph looks like this:

So, how does that help? Well, the graph tells us pretty straight, which decisions lead to the contradiction, namely P^TQ^T and R^T. But more than that, it tells us that R^T wasn’t actually a decision; it was implied by the other two choices. So in our next attempt, we need to make sure we don’t set P and Q to 1. The easiest way to do that is to add a new clause for \neg (P \wedge Q), which is Ln_1=\{ P^F, Q^F \}. Hooray, we learned a new clause! Before we examine how exactly we construct clauses out of graphs, let’s continue our example with this newly added clause:

Example continued:

      1. Since the former branch failed, we add our new clause and simplify, yielding \Delta_1 = \{ L_1=\{Q^F, R^T\}, L_2=\{Q^F, R^F\}, L_3=\{Q^T, R^T\}, L_4=\{Q^T, R^F\}, Ln_1=\{Q^F\} \}. Now Ln_1 became a unit clause, so we add an edge from P^T to Q^F, do unit propagation by letting I(Q)=0 and simplify, yielding \Delta_2 = \{ L_3=\{R^T\}, L_4=\{R^F\} \}.
        Now L_3 became a unit, so we need to add edges from P^T and Q^F to R^T.We do unit propagation again and L_4 becomes the empty clause, adding the edges from P^T, Q^F and R^T to \Box_{L_4}.  Finally, we return \textsf{unsatisfiable}.

The resulting graph:

This time, we can immediately see that the bad choice was P^T. We can learn from this, by adding the new clause Ln_2=\{ P^F \}, which of course is a unit and thus immediately becomes part of our assignment.

So, how exactly do we get from implication graphs to clauses? That’s simple: starting from the contradiction we arrived at, we take every ancestor of the \Box-node with no incoming edges – i.e. the roots. Those are the literals that were chosen during a split-step in the algorithm, and the other ancestors are all implied (via unit propagation) necessarily by those choices. These choices (i.e. their conjunction) lead to the problem, so we take their negation and add them as a new clause: In the first example graph, the roots were the node P^T and Q^T, so we added the new clause \{ P^F, Q^F \}. In the second graph, the only root was P^T, so we added the clause \{ P^F \}.


Admittedly, in this example adding the learned clauses didn’t actually help much – but imagine bringing the variables X_1,\ldots,X_{100} back into the mix. Where we had hundreds of almost identical branches before, with clause learning the search tree of the algorithm will look more like this:

(Image taken from Michael’s lecture notes)

Two failures are now enough to conclude, that setting I(P)=1 was already a mistake and we can immediately backtrack to the beginning.