How the Abstract DPLL Algorithm Works in SAT Solving

Question

I have come across many definitions of the DPLL algorithm but haven't been able to follow them. The ones that are closest to making sense to me are the ones based on state-transition systems with transition rules such as defined here:

$F$ is a CNF formula, $C$ is a clause, and $M$ is a model. A description of it is as follows:

Here, a DPLL procedure will be modeled by a transition system: a set of states together with a relation, called the transition relation, over these states. States will be denoted by (possibly subscripted) $S$.... A state is either fail or a pair $M \parallel F$, where $F$ is a finite set of clauses and $M$ is a sequence of annotated literals.... We will not go into a complete formalization of annotated literals; it suffices to know that some literals $l$ will be annotated as being decision literals; this fact will be denoted here by writing $l^d$ (roughly, decision literals are the ones that have been added to $M$ by the Decide rule given below). Most of the time the sequence $M$ will be simply seen as a set of literals, denoting an assignment, i.e., ignoring both the annotations and the fact that $M$ is a sequence and not a set.

I understand that a literal is an atom or its negation, but I don't understand what an annotated literal is, which is a core part of understanding what a model $M$ is in $M \parallel F$. I also don't understand what the decision literals are.

Two examples are as follows.

This is as much as I can gather. This:

$$\emptyset \parallel 1 \lor \bar{3}, \bar{1} \lor \bar{4} \lor 5 \lor 2, \bar{1} \lor \bar{2}$$

Is essentially an implementation of this:

$$M \parallel F$$

Also, the commas are really $\land$, as in:

$$\emptyset \parallel (1 \lor \bar{3}) \land (\bar{1} \lor \bar{4} \lor 5 \lor 2) \land (\bar{1} \lor \bar{2})$$

So each of the blocks between the commas or $\land$ are clauses. On the left is a growing list of literals (atoms or their negation). On the right are the rules being applied (like Decide). But I don't understand (a) how the rules are being applied / why they are chosen at the time they are chosen, (b) how it results in an annotated literal for $M$ on the left, and (c) why some of them are marked in bold as the "decision" literals.

The final result, from my understanding, is the model $M$ (on the left) that satisfies the formula $F$ on the right. Essentially, it's a valuation.

Wondering if one could clarify how the first example works, how the annotated literals get added to the model $M$ on the left.

Answer 1

Describing DPLL as a series of state-transition rules is the worst way I've ever seen to aid understanding the algorithm. The pseudocode provided in the WIkipedia article on DPLL is much easier to understand if you're approaching the algorithm for the first time.

;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)});

Decision literals are the literals returned by the choose-literal function called above. Annotated literals are just literals that are members of M that are marked in some way so the DPLL implementation can distinguish decision literals from literals added to M by unit propagation. This marking is for the sake of the backjumping code which must unroll assignments until the one responsible for the current conflict is found and then replace it.

Note that the original DPLL algorithm did not have backjumping in it. It simply backtracked, either reversing the current assignment or returning false if the algorithm had run out of assignments to try. Backjumping was a later innovation.

Note also that pure literal assignment isn't usually done in modern SAT solvers that implement some form of DPLL. It is a fairly expensive check to do in an algorithm expected to recurse and backtrack an exponential number of times and the benefits of doing the check don't outweigh the costs.