3
$\begingroup$

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:

enter image description 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.

enter image description here enter image description here

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.

$\endgroup$
  • 1
    $\begingroup$ This is helpful, the idea of an implication graph. That was left out in most of the papers and resources on DPLL I have seen. Starting to get closer to an actual working implementation level of detail. Then there is the idea of "decision level is incremented by one". More on implementation detail which I'm looking for. $\endgroup$ – Lance Pollard Jul 22 '18 at 0:04
4
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ The problem I've had with this approach is I don't know how choose-literal, if Φ is a consistent set of literals, if Φ contains an empty clause, for every unit clause {l} in Φ, unit-propagate(l, Φ);, for every literal l that occurs pure in Φ, and pure-literal-assign(l, Φ); are implemented. Basically, the entire method's implementation details are left out. This makes this version super hard to understand as a newcomer. This answer gives no additional information than the Wikipedia algorithm provides, which is pretty much empty of implementation detail :/ $\endgroup$ – Lance Pollard Jul 24 '18 at 22:46
  • $\begingroup$ @LancePollard Implementation details would be language-specific and we try to avoid that here. Generally you'd expect literals to be popped off a priority queue and pushed onto a stack of assignments, the queue being ordered by some feature of the formula such as the number of times a variable appears. When all the variables have been assigned without a conflict, "Φ is a consistent set of literals" and you have a valid assignment. Unit propagation is usualy implemented atop a scheme called "two watched literals" which performs much better than naive clause satisfaction tracking schemes. $\endgroup$ – Kyle Jones Jul 25 '18 at 2:33
  • $\begingroup$ @LancePollard Beyond that you'll have to look at an implementation, e.g. Minisat, to glean more details. There are several SAT solvers with source code available. See http://www.satcompetition.org/ for lots of code, papers and more. $\endgroup$ – Kyle Jones Jul 25 '18 at 2:42

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.