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 }
|
Example | ||||||||||||||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
S = { p | q | r, p | q | ~r, p | ~q | r, p | ~q | ~r, ~p | q | r, ~p | q | ~r, ~p | ~q | r }
|
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 }
|