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 L, or some pure literal L) {
       if (L and ~L are both in S) {      //----The "model" isn't
           return("unsatisfiable");
       } else {
           S = Simplify(S,L);                 //----Assign L TRUE in model
       }
    }
    if (S is empty) {
        return("satisfiable");
    }

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

function Simplify(S,L) {

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

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

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

Example 
S = { p | q | r,
      p | q | ~r,
      p | ~q | r,
      p | ~q | ~r,
      ~p | q | r,
      ~p | q | ~r,
      ~p | ~q | r }

DPLL(S)
Pick ~q, Simplify(S,~q)
Model=[~q] 
S = { p | r,
      p | ~r,
      ~p | r,
      ~p | ~r }
DPLL(S) Pick p, Simplify(S,p)
Model=[~q, p] 
S = { r,
      ~r }
DPLL(S) r and ~r are both in S, partial "model" isn't
return("unsatisfiable")
DPLL(Simplify(S,p)) != "satisfiable", Simplify(S,~p)
Model=[~q, ~p] 
S = { r,
      ~r }
DPLL(S) r and ~r are both in S, partial "model" isn't return("unsatisfiable")
return("unsatisfiable")
DPLL(Simplify(S,~q)) != "satisfiable", Simplify(S,q)
Model=[q] 
S = { p | r,
      p | ~r,
      ~p | r }
DPLL(S) Pick p, Simplify(S,p)
Model=[q, p] 
S = { r }
DPLL(S) There is a pure literal r, S = Simplify(S,r)
Model=[q, p, r] 
S = { }
S is empty, return("satisfiable")
DPLL(Simplify(S,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 L, or some pure literal L) {
       if (L and ~L are both in S) {      //----The "model" isn't
           if (there have been some picks) {
               new_clause = disjunction of negations of picks
               return(Backjump@PlaceOfEarliestPick(new_clause));
           } else {
               return("unsatisfiable");
           }
       } else {
           S = Simplify(S,L);                 //----Assign p TRUE in model
       }
    }
    if (S is empty) {
        return("satisfiable");
    }

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

function Simplify(S,L) {

    delete every clause in S containing L;
    delete every occurrence in S of ~L;
    return(S);
}
Example 
S = { p | q | r,
      p | q | ~r,
      p | ~q | r,
      p | ~q | ~r,
      ~p | q | r,
      ~p | q | ~r,
      ~p | ~q | r }

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