DPLL algorithm

The DPLL algorithm is a SAT solving algorithm for propositional formulas in conjunctive normal form. It is guided by the structure of the given formula.

The algorithm was devised in 1962, by Martin Davis, George Logemann und Donald W. Loveland. It is based on an algorithm devised by Martin Davis and Hilary Putnam in 1960.

Fundamental observations

The basic idea of the DPLL algorithm is that it determines a 1-assignment for a given formula in CNF in clausal notation in a backtracking fashion step by step, setting one variable after the other, using the self reducibility lemma.

Recall that the self reducibility lemma says that when one wants to find a satisfying assignment for a propositional formula one can simply set one of the variables to true and false and then work recursively on the two resulting simpler formulas. Here, "setting to true and false" means substituting $\top$ and $\bot$, respectively, for the variable.

In clausal notation, substitutions are especially easy to carry out!

Example Let $\varphi = (X_0 \vee X_1) \wedge (\neg X_0 \vee X_2) \wedge (X_1 \vee X_2)$. Then $\varphi\{X_0 \mapsto \bot\} \SemEquiv X_1 \wedge (X_1 \vee X_2)$. In clausal notation, $\varphi$ can be written as $\bigwedge \bigvee \{\{X_0, X_1\}, \{\neg X_0, X_2\}, \{X_1, X_2\}\}$ and $\varphi\{X_0 \mapsto \bot\}$ as $\bigwedge \bigvee \{\{X_1\}, \{X_1, X_2\}\}$. So setting $X_0$ to $\bot$ means to remove all clauses with $\neg X_0$ in them and to remove $X_0$ from the remaining ones.

This example can be generalized.

Lemma Let $M$ be a clause set and $X_i \in \text{vars}(M)$. Then \begin{align} \bigwedge\bigvee M \{X_i \mapsto \bot\} & \SemEquiv \bigwedge \bigvee \{K \setminus \{X_i\} \colon K \in M \text{ and } \neg X_i \notin K\}\\ \bigwedge\bigvee M \{X_i \mapsto \top\} & \SemEquiv \bigwedge \bigvee \{K \setminus \{\neg X_i\} \colon K \in M \text{ and } X_i \notin K\} \enspace. \end{align}

This motivates new notation: \begin{align} M \vert_{\neg X_i} & = \{K \setminus \{X_i\} \colon K \in M \text{ and } \neg X_i \notin K\}\\ M \vert_{X_i} & = \{K \setminus \{\neg X_i\} \colon K \in M \text{ and } X_i \notin K\} \enspace. \end{align}

With these definitions, the self reducibility lemma reads as follows.

Self reducibility for formulas in CNF in clausal notation Let $M$ be a clause set, $V = \text{vars}(M)$, $X_i \in \text{vars}(M)$, $W = V \setminus \{X_i\}$, and \begin{align} M_0 & = \bigwedge\bigvee M \vert_{\neg X_i}\\ M_1 & = \bigwedge\bigvee M \vert_{X_i} \enspace. \end{align} Then:

1. The formula $\bigwedge\bigvee M$ is satisfiable if, and only if, $\bigwedge\bigvee M_0$ or $\bigwedge\bigvee M_1$ is satisfiable.
2. Let $\beta \colon V \to \{0,1\}$ be a 1-assignment for $\bigwedge\bigvee M$. Then $\beta \vert_W$ is a 1-assignment for $\bigwedge\bigvee M_{\beta(X_i)}$.
3. Let $\beta_b \colon W \to \{0,1\}$ be a 1-assignment for $\bigwedge\bigvee M_b$ for some $b \in \{0,1\}$. Then $\beta \cup \{X_i \mapsto b\}$ is a 1-assignment for $\bigwedge\bigvee M$.

This lemma is the basis for the DPLL algorithm, but there are four more observations that are crucial ingredients.

Lemma Let $M$ be a clause set.

1. If $\{X_i, \neg X_i\} \in K$ for some $i \in \mathbf N$ and $K \in M$, then $\bigwedge \bigvee M \SemEquiv \bigwedge\bigvee (M \setminus K)$.
2. If $\emptyset \in M$, then $\bigwedge\bigvee M$ is unsatisfiable.
3. If $M = \emptyset$, then $\bigwedge\bigvee M$ is a tautology.
4. If $\{L\} \in M$ for some Literal $L$, then $\bigwedge \bigvee M \vert_{\overline{L} }$ is unsatisfiable.
5. If $L \in \bigcup M$ and $\bar L \notin \bigcup M$ for some literal $L$, then $\bigwedge \bigvee M \vert_{\bar L} \models \bigwedge \bigvee M \vert_L$.

This lemma motivates the following definitions.

A clause $K$ with $\{X_i, \neg X_i\} \in K$ for some $i \in \mathbf N$ is said to be tautological.

A clause $\{L\}$ is said to be a unit clause.

When $M$ is a clause set and $L$ a literal such that $L \in \bigcup M$ and $\bar L \notin \bigcup M$, then $L$ is said to be a pure literal for $M$.

The Algorithm

The last two lemmas motivate the following approach for finding 1-assignments for a formula $\bigwedge\bigvee M$ where $M$ is a clause set.

In a first, preprocessing step eliminate all tautological clauses. (Note that the following steps never generate tautological clauses.)

Then proceed recursively as follows.

1. If $\emptyset \in M$, then $\bigwedge \bigvee M$ is unsatisfiable; return this fact.
2. If $M = \emptyset$, then $\bigwedge\bigvee M$ is satisfiable and the empty assignment is a 1-assignment; return the empty assignment.
3. If there is a unit clause $\{L\}$, then determine a 1-assignment for $\bigwedge\bigvee M \vert_L$ and extend it to a 1-assignment for $\bigwedge \bigvee M$; return this assignment. If no such assignment exists, then $\bigwedge\bigvee M$ is unsatisfiable; return this fact.
4. If there is a pure literal $L$, then determine a 1-assignment for $\bigwedge\bigvee M \vert_L$ and extend it to a 1-assignment for $\bigwedge \bigvee M$; return this assignment. If no such assignment exists, then $\bigwedge\bigvee M$ is unsatisfiable; return this fact.
5. In any other case, let $X_i \in \text{vars}(M)$. Determine 1-assignments for $\bigwedge \bigvee M \vert_{X_i}$ and $\bigwedge\bigvee M \vert_{\neg X_i}$ and extend one of them to a 1-assignment for $\bigwedge\bigvee M$ and return it. If no such assignment exists, then $\bigwedge\bigvee M$ is unsatisfiable; return this fact.

Pseudocode for the recursive procedure looks as follows.

  DPLL($M$)
  Precondition: $M$ is a clause set without tautological clauses
  if $\emptyset \in M$ then return $\bot$ -- unsatisfiable
  if $M = \emptyset$ then return $\emptyset$ -- tautology
  // unit clause
  if $\{L\} \in M$ for some literal $L$
    r = DPLL($M \vert_L$) 
    if $r \neq \bot$ then return $\{L \mapsto 1\} \cup r$ else return $\bot$
  // pure literal
  if $L \in \bigcup M$ and $\bar L \notin \bigcup M$ for some literal $L$
    r = DPLL($M \vert_L$) 
    if $r \neq \bot$ then return $\{L \mapsto 1\} \cup r$ else return $\bot$
  // branching
  let $X_i$ $\in$ vars($M$)
  r = DPLL($M \vert_{X_i}$)  
  if $r \neq \bot$
    return $\{X_i \mapsto 1\} \cup r$
  else
    r = DPLL($M \vert_{\neg X_i}$) 
    if $r \neq \bot$
      return $\{X_i \mapsto 0\} \cup r$
    else
      return $\bot$

In the above, $L \mapsto 1$ means that $X_i$ is mapped to 1 if $L = X_i$ and $X_i$ is mapped to 0 if $L = \neg X_i$.

Example Let $M = \{\{X_0, X_1\}, \{\neg X_0, \neg X_1\}, \{X_1, X_2\}, \{\neg X_1, \neg X_2\}, \{X_2, X_0\}\}$. The computation of the algorithm can be illustrated by visualizing the tree of recursive calls.

The 1-assignment the algorithm returns is $\{X_0 \mapsto 0, X_1 \mapsto 1, X_2 \mapsto 0\}$.

Although there are three variables, for only one of these three variables the two choices need to be checked. For the two other variables, there are no choices because of unit clauses.