DPLL and CDCL

The DPLL Algorithm

The Davis-Putnam-Logemann-Loveland algorithm is a decision procedure for CNF formulae in propositional logic. It tries to construct a model for the clauses, and if it fails there is no model. To prove logical consequence take the axioms and negated conjecture in CNF, and check for unsatisfiability.

function DPLL(S) {

    if (S is empty) {
        return("satisfiable");
    }
    while (there is some unit clause {p}, or some pure literal p) {
       if ({p} and {~p} are both in S) {      //----The "model" isn't
           return("unsatisfiable");
       } else {
           S = Simplify(S,p);                 //----Assign p TRUE in model
       }
    }
    if (S is empty) {
        return("satisfiable");
    }

    pick some literal p from a shortest clause in S;
    if (DPLL(Simplify(S,p)) == "satisfiable") { //----Assign p TRUE in model
       return("satisfiable");
    } else {
       return(DPLL(Simplify(S,~p));           //----Assign p FALSE in model
    }
}

function Simplify(S,p) {

    delete every clause in S containing p;
    delete every occurrence in S of ~p;
    return(S);
}

Example

S1 = { ~n | ~t, m | q | n, l | ~m, l | ~q, ~l | ~p, r | p | n, ~r | ~l, t }

DPLL(S1)
Unit clause t, S1 = Simplify(S1,t)
Model=[t]
S1 = { ~n, m | q | n, l | ~m, l | ~q, ~l | ~p, r | p | n, ~r | ~l }

Unit clause ~n, S1 = Simplify(S1,~n)
Model=[t, ~n]
S1 = { m | q, l | ~m, l | ~q, ~l | ~p, r | p, ~r | ~l }

Pick m, Simplify(S1,m) Model=[t, ~n, m] S2 = { l, l | ~q, ~l | ~p, r | p, ~r | ~l }
DPLL(S2)
Unit clause l, S2 = Simplify(S2,l)
Model=[t, ~n, m, l]
S2 = { ~p, r | p, ~r }

Unit clause ~p, S2 = Simplify(S2,~p)
Model=[t, ~n, m, l, ~p]
S2 = { r, ~r }

r and ~r are both in S2, partial "model" isn't
return("unsatisfiable")
DPLL(Simplify(S1,m)) != "satisfiable"
Simplify(S1,~m)
Model=[t, ~n, ~m]
S2 = { q, l | ~q, ~l | ~p, r | p, ~r | ~l }

DPLL(S2))

Unit clause q, S2 = Simplify(S2,q)
Model=[t, ~n, ~m, q]
S2 = { l, ~l | ~p, r | p, ~r | ~l }

Unit clause l, S2 = Simplify(S2,l)
Model=[t, ~n, ~m, q, l]
S2 = { ~p, r | p, ~r }

Unit clause ~p, S2 = Simplify(S2,~p)
Model=[t, ~n, ~m, q, l, ~p]
S2 = { r, ~r }

r and ~r are both in S2, partial "model" isn't
return("unsatisfiable")

return("unsatisfiable")

Example

S1 = { p | q | r, p | q | ~r, p | ~q | r, p | ~q | ~r, ~p | q | r, ~p | q | ~r, ~p | ~q | r }

DPLL(S1)
Pick ~q, Simplify(S1,~q)
Model=[~q]
S2 = { p | r, p | ~r, ~p | r, ~p | ~r }

DPLL(S2)
Pick p, Simplify(S2,p) Model=[~q, p] S3 = { r, ~r }
DPLL(S3)
r and ~r are both in S3, partial "model" isn't
return("unsatisfiable")
DPLL(Simplify(S1,p)) != "satisfiable", Simplify(S2,~p)
Model=[~q, ~p]
S3 = { r, ~r }

DPLL(S3)
r and ~r are both in S3, partial "model" isn't return("unsatisfiable")
return("unsatisfiable")

DPLL(Simplify(S1,~q)) != "satisfiable", Simplify(S1,q)
Model=[q]
S2 = { p | r, p | ~r, ~p | r }

DPLL(S2)
Pick p, Simplify(S2,p) Model=[q, p] S3 = { r }
DPLL(S3)
There is a pure literal r, S3 = Simplify(S3,r)
Model=[q, p, r]
S3 = { }

S3 is empty, return("satisfiable")

DPLL(Simplify(S2,p)) == "satisfiable", return("satisfiable")
return("satisfiable")
Model=[q, p, r]

The CDCL Algorithm

The Conflict-Driven-Clause-Learning algorithm extends DPLL with a mechanism for learning clauses to prevent repeating decisions that cannot lead to a model.

function CDCL(S) {

    if (S is empty) {
        return("satisfiable");
    }
    while (there is some unit clause {p}, or some pure literal p) {
       if ({p} and {~p} are both in S) {      //----The "model" isn't
           if (there have been some picks) {
               new_clause = LearnClause();
               backjump("unsatisfiable",new_clause,PlaceOfEarliestPick(new_clause));
           } else {
               return("unsatisfiable");
           }
       } else {
           S = Simplify(S,p);                 //----Assign p TRUE in model
       }
    }
    if (S is empty) {
        return("satisfiable");
    }

    pick some literal p from a shortest clause in S;
    if (CDCL(Simplify(S,p)) == "satisfiable") { //----Assign p TRUE in model
       return("satisfiable");
    } else {
       if (backjumped to here) {
           Add new_clause to S (as it was before the Simplify)
           return(CDCL(S));
       } else {
           return(CDCL(Simplify(S,~p));        //----Assign p FALSE in model
       }
    }
}

function Simplify(S,p) {

    delete every clause in S containing p;
    delete every occurrence in S of ~p;
    return(S);
}

function LearnClause() {

    return(DisjunctionOf(NegatedPx()));
}

Example

S1 = { p | q | r,
       p | q | ~r,
       p | ~q | r,
       p | ~q | ~r,
       ~p | q | r,
       ~p | q | ~r,
       ~p | ~q | r }

CDCL(S1), Model=[], Px={}
Pick ~q, Model=[~q], Px={~q}
Simplify(S1,~q)
S2 = { p | r, p | ~r, ~p | r, ~p | ~r }

CDCL(S2), Model=[~q], Px={~q}
Pick p, Model=[~q,p], Px={~q,p} Simplify(S2,p) S3 = { r, ~r }
CDCL(S3), Model=[~q,p], Px={~q,p}
r and ~r are both in S3
Px={~q,p}, learn q | ~p
Backjump to level that picked ~q
Add q | ~p
S2 = { p | q | r, p | q | ~r, p | ~q | r, p | ~q | ~r, ~p | q | r, ~p | q | ~r, ~p | ~q | r, q | ~p }

CDCL(S2), Model=[], Px={}
Pick q, Model=[q], Px={q}
Simplify(S2,q)
S3 = { p | r, p | ~r, ~p | r }

CDCL(S3), Model=[q], Px={q}
Pick p, Model=[q,p], Px={q,p}
Simplify(S3,p)
S4 = { r }

CDCL(S4), Model=[q,p], Px={q,p}
Unit clause r, Model=[q,p,r]
Simplify(S4,r)
S4 = { }

S4 is empty, return "satisfiable"
Return "satisfiable"
Return "satisfiable"
Return "satisfiable"