Davis-Putnam (DPLL) procedure
Martin Davis, Hillary Putnam, George Logemann, and Donald Loveland (1962)
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.
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 = obviousAssign(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 = obviousAssign(L,V)
S = propagate(atom(L), S, V);
}
else exitloop; % No easy cases found
} % end loop
% HARD CASE: PICK SOME ATOM AND TRY EACH ASSIGNMENT IN TURN
pick atom A such that V[A] == UNBOUND; % Try one assignment
V[A] = TRUE;
S1 = copy(S);
S1 = propagate(A, S1, V);
VNEW = dp1(ATOMS,S1,V);
if (VNEW != NIL) then return(VNEW); % Found a satisfying valuation
% If V[A] = TRUE didn't work, try V[A] = FALSE;
V[A] = FALSE;
S1 = propagate(A, S, V);
return(dp1(ATOMS,S1,V)); % Either found a satisfying valuation or backtrack
} end dp1
% Propagate the effect of assigning atom A to be value V.
% Delete every clause where A appears with sign V
% Delete every literal where A appears with sign not V.
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.
% Given a literal L with atom A, make V[A] the sign indicated by L.
obviousAssign(L,V) {
if (L is an atom A) then V[A] = TRUE;
else if (L has the form ~A) then V[A] = FALSE;
}