DPLL

The DPLL Procedure

The Davis-Putnam-Logemann-Loveland procedure is a decision procedure for CNF formulae in propositional logic. 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) { 
           return("unsatisfiable");
       } else {
           S = Simplify(S,p);
       }
    }
    if (S is empty) {
        return("satisfiable");
    }

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

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)
There is a unit clause t, S1 = Simplify(S1,t) 
S1 = { ~n,
       m | q | n,
       l | ~m,
       l | ~q,
       ~l | ~p,
       r | p | n,
       ~r | ~l }
There is a unit clause ~n, S1 = Simplify(S1,~n) 
S1 = { m | q,
       l | ~m,
       l | ~q,
       ~l | ~p,
       r | p,
       ~r | ~l }
Pick m, Simplify(S1,m) 
     { l,
       l | ~q,
       ~l | ~p,
       r | p,
       ~r | ~l }
DPLL(Simplify(S1,m))
There is a unit clause l, S2 = Simplify(S2,l) 
S2 = { ~p,
       r | p,
       ~r }
There is a unit clause ~p, S2 = Simplify(S1,~p) 
S2 = { r,
       ~r }
r and ~r are both in S1, return("unsatisfiable")
DPLL(Simplify(S1,m)) != "satisfiable", Simplify(S1,~m) 
     { q,
       l | ~q,
       ~l | ~p,
       r | p,
       ~r | ~l }
DPLL(Simplify(S1,~m))
There is a unit clause q, S2 = Simplify(S2,q) 
S2 = { l,
       ~l | ~p,
       r | p,
       ~r | ~l }
There is a unit clause l, S2 = Simplify(S2,l) 
S2 = { ~p,
       r | p,
       ~r }
There is a unit clause ~p, S2 = Simplify(S1,~p) 
S2 = { r,
       ~r }
r and ~r are both in S1, 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) 
     { p | r,
       p | ~r,
       ~p | r,
       ~p | ~r }
DPLL(Simplify(S1,~q))
Pick p, Simplify(S2,p) 
     { r,
       ~r }
DPLL(Simplify(S2,p))
r and ~r are both in S1, return("unsatisfiable")
DPLL(Simplify(S1,p)) != "satisfiable", Simplify(S2,~p) 
     { r,
       ~r
       }
DPLL(Simplify(S2,~p))
r and ~r are both in S1, return("unsatisfiable")
return("unsatisfiable")
DPLL(Simplify(S1,~q)) != "satisfiable", Simplify(S1,q) 
     { p | r,
       p | ~r,
       ~p | r }
DPLL(Simplify(S1,q))
Pick p, Simplify(S2,p) 
     { r }
DPLL(Simplify(S2,p))
There is a pure literal r, S3 = Simplify(S3,r) 
S3 = { }
S3 is empty, return("satisfiable")
DPLL(Simplify(S2,p)) == "satisfiable", return("satisfiable")
return("satisfiable")