The DPLL backtracking search procedure

The acronym DPLL stands for “Davis–Putnam–Logemann–Loveland” by the names of the inventors of the method [DavisPutnam1960] [DavisEtAl1962]. It can be considered as the basic backtracking search approach for solving propositional satisfiability.

The backtracking DPLL search algorithm simply starts from an empty partial truth assignment, and then, recursively, tries both the false and true branches for an unassigned variable until either

a truth assignment satisfying all the clauses is found, in which case the search terminates, or
a conflict (a falsified clause) is found, in which case the search backtracks to the previous search node.

In pseudocode, one can express the algorithm as follows:

def \(\PseudoDPLL(\phi)\):     // \(\phi\) is a CNF formula
   return \(\PseudoDPLL(\phi,\emptyset)\)

def \(\PseudoDPLL(\phi,\TA)\): // \(\TA\) is the current partial truth assignment
   // A dead-end node?
   if \(\phi\) contains a clause falsified by \(\TA\): return \(\PseudoUnsat\)
   // Found a satisfying truth assignment?
   if \(\TA(x)\) is defined for all \(x \in \VarsOf{\phi}\): return \((\PseudoSat,\TA)\)
   // No, choose a branching literal and recurse for both values
   choose a literal \(l\) such that \(\TA(l)\) is undefined
   if \(\PseudoDPLL(\phi,\TA \cup \Set{l}) = (\PseudoSat,\TA')\): return \((\PseudoSat,\TA')\)
   if \(\PseudoDPLL(\phi,\TA \cup \Set{\neg{l}}) = (\PseudoSat,\TA')\): return \((\PseudoSat,\TA')\)
   // There is no extension of \(\TA\) satisfying \(\phi\)
   return \(\PseudoUnsat\)

Example

Consider the unsatisfiable CNF formula

\[(a \lor \neg b) \land (\neg a \lor c \lor \neg d) \land (a \lor c \lor \neg d) \land (\neg c \lor \neg e) \land (\neg c \lor e) \land (c \lor d)\]

One search tree for the formula is shown below. The nodes denote calls to \(\PseudoDPLL\), the labels next to them describe their partial truth assignments, and edge labels denote the branching literal. To save space in figures, we use \(\bar x\) to denote \(\neg x\).

All the search paths end in nodes where at least one clause is falsified, marked with a cross, and the algorithm returns \(\PseudoUnsat\).

For instance, in the node with the assignment \(\Set{a,\Neg c,\Neg d}\), the clause \((c \lor d)\) is falsified.

Example

Consider the satisfiable CNF formula

\[(a \lor \neg b) \land (a \lor c \lor \neg d) \land (\neg c \lor \neg e) \land (\neg c \lor e) \land (c \lor d)\]

One search tree for the formula is shown below:

The search is terminated after the node with the satisfying truth assignment \(\Set{a,b,\Neg c,d,e}\) is reached.

Incorporating unit clause propagation

In practise, one always uses Unit clause propagation to prune the DPLL search space. One way to incorporate unit propagation in the algorithm is given below as pseudocode.

def \(\PseudoDPLL(\phi)\):
   return \(\PseudoDPLL(\phi,\emptyset)\)

def \(\PseudoDPLL(\phi,\TA)\):
   if \(\phi\) contains a clause falsified by \(\TA\): return \(\PseudoUnsat\)
   // Added: perform unit clause propagation
   while \(\phi\) contains a unit clause \(C\) in \(\TA\):
     \(\TA \PseudoAsgn \TA \cup \Set{l}\), where \(l\) is the literal implied by \(C\)
     if \(\phi\) contains a clause falsified by \(\TA\): return \(\PseudoUnsat\)
   // No conflict found, continue as earlier
   if \(\TA(x)\) is defined for all \(x \in \VarsOf{\phi}\): return \((\PseudoSat,\TA)\)
   choose a literal \(l\) such that \(\TA(l)\) is undefined
   if \(\PseudoDPLL(\phi,\TA \cup \Set{l}) = (\PseudoSat,\TA')\): return \((\PseudoSat,\TA')\)
   if \(\PseudoDPLL(\phi,\TA \cup \Set{\neg l}) = (\PseudoSat,\TA')\): return \((\PseudoSat,\TA')\)
   return \(\PseudoUnsat\)

Example

Consider again unsatisfiable CNF formula

\[(a \lor \neg b) \land (\neg a \lor c \lor \neg d) \land (a \lor c \lor \neg d) \land (\neg c \lor \neg e) \land (\neg c \lor e) \land (c \lor d)\]

If we illustrate the unit clause propagation as out-degree 1 nodes, then one possible search tree is illustrated below.

After branching on \(\Neg a\), unit propagation of the clause \((a \lor \neg b)\) implies \(\Neg b\). In the resulting node with the truth assignment \(\Set{\Neg a, \Neg b}\), no further unit clause propagation is possible.

From the node with the truth assignment \(\Set{\Neg a, \Neg b, \Neg c}\) we obtain \(\Neg d\) by unit clause propagation on the clause \((a \lor c \lor \Neg d)\). In the resulting node the clause \((c \lor d)\) is falsified and the search backtracks.

Unit clause propagation can be “simulated” in the basic version that does not have it: the unassigned literal from a unit clause is chosen as the branching literal whenever possible, and thus

the next branch on which the literal is false, will terminate immediately, and
the other next branch will have have the literal set to the correct value.

This simulation will be used in the Section The resolution proof system because we can rather directly derive a proof of unsatisfiability from the basic DPLL search tree.

Example

Consider again unsatisfiable CNF formula

\[(a \lor \neg b) \land (\neg a \lor c \lor \neg d) \land (a \lor c \lor \neg d) \land (\neg c \lor \neg e) \land (\neg c \lor e) \land (c \lor d)\]

The tree below shows the search of the basic version when unit propagation described in the previous example is simulated with immediately terminating branches.

After branching on \(\Neg a\), unit propagation of the clause \((a \lor \neg b)\) is shown as the next branch on \(b\) terminating immediately, effectively forcing \(\Neg b\) to hold.