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)
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 ("not 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 ("not A" in C and V[A]=TRUE) then delete "not 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 "not A") then V[A] := FALSE;
}