Davis-Putnam (DPLL) procedure Martin Davis and Hillary Putnam, 1961 dp(in ATOMS : set of propositional atoms; S : Set of propositional formulas in CNF) return either a valuation on ATOMS satisfying S or NIL if none exists. var V : array[ATOMS]; { for (A in ATOMS) do V[A] := UNBOUND; return dp1(ATOMS,S,V) } end dp. dp1(ATOMS,S,V) /* call S,V by value */ { loop { /* Loop as long as there are easy cases to cherry pick */ /* BASE OF THE RECURSION: SUCCESS OR FAILURE */ if (S is empty) /* Success: All clauses are satisfied */ { for (A in ATOMS) if V[A] == UNBOUND then assign V[A] either TRUE or FALSE; return(V); } else if (some clause in S is empty) /* Failure: Some clause */ then return(NIL); /* is unsatisfiable under V */; /* EASY CASES: PURE LITERAL ELIMINATION AND FORCED ASSIGNMENT */ else if (there exists a literal L in S /* Pure literal elimination */ such that the negation of L does not appear in S) then { V := obvious_assign(L,V); delete every clause containing L from S; } else if (there exists a clause C in S /* Forced assignment */ containing a single literal L) then { V := obvious_assign(L,V) S := propagate(atom(L), S, V); } else exitloop; /* No easy cases found */ } /* endloop */ /* PICK SOME ATOM AND TRY EACH ASSIGNMENT IN TURN */ pick atom A such that V[A] == UNBOUND; /* Try one assignment */ V[A] := TRUE; S1 := propagate(A, S, V); VNEW := dp1(ATOMS,S1,V); if (VNEW != NIL) then return(VNEW); /* IF V[A] := TRUE didn't work, try V[A} := FALSE; V[A] := FALSE; S1 := propagate(A, S, V); return(dp1(ATOMS,S1,V)); } end dp1 propagate(A,S,V) { for each clause C in S do if ((A in C and V[A]=TRUE) or (~A in C and V[A]==FALSE)) then delete C from S else if (A in C and V[A]==FALSE) then delete A from C else if (~A in C and V[A]==TRUE) then delete ~A from C; return S; } end propagate. obvious_assign(L,V) { if (L is an atom A) then V[A] := TRUE; else if (L has the form ~A) then V[A] := FALSE; }