Davis-Putnam procedure Martin Davis and Hillary Putnam, 1961 dp(in ATOMS : set of propositional atoms; F : Propositional formula in CNF) return either a valuation on ATOMS satisfying F or NIL if none exists. var V : boolean array[ATOMS]; { for (A in ATOMS) do V[A] := UNBOUND; return dp1(ATOMS,F,V) } end dp. dp1(ATOMS,F,V) /* call F,V by value */ if F is empty then return V else if F contains an empty clause then return NIL else { if F contains a singleton clause C then if the single literal in C is A then V[A] := TRUE else if the single literal in C is "not A" then V[A] := FALSE; F := propagate(A,ATOMS,F,V) return dp1(ATOMS,F,V) } else { pick A in ATOMS; V[A] := TRUE; F1 := propagate(A,ATOMS,F,V) VNEW := dp1(ATOMS,F1,V); if VNEW != NIL then return VNEW; V[A] := FALSE; F := propagate(A,ATOMS,F,V) return dp1(ATOMS,F,V) } end dp1 propagate(A,ATOMS,F,V) { for each clause C in F do if ((A in C and V[A]=TRUE) or ("not A" in C and V[A]=FALSE)) then delete C from F else if (A in C and V[A]=FALSE) then delete A from C else if ("not A" in C and V[A]=TRUE) then delete "not A" from C; return F; } end propagate.