The Davis-Putnam algorithm (Martin Davis, Hilary Putnam) Input: A propositional formula in CNF (clausal form). Output: Either a truth-valuation that satisfies the formula, or "FAIL" if no such valuation exists. function davis-putnam(in FORMULA : a list of clauses) reduce(FORMULA, VREDUCE) if FORMULA is empty then return VREDUCE; else if FORMULA contains an empty clause (clause with no literals) then return "FAIL" else begin pick a variable V in FORMULA; VALUATION := davis-putnam(substitute(TRUE, V, FORMULA)) if VALUATION != FAIL then return append(V->TRUE, VREDUCE, VALUATION); VALUATION := davis-putnam(substitute(FALSE, V, FORMULA)) if VALUATION != FAIL then return append(V->FALSE, VREDUCE, VALUATION); return FAIL end endif end davis-putnam Or, more elegantly as a non-deterministic algorithm. function davis-putnam(FORMULA: a list of clauses) FORMULA := reduce(FORMULA,VREDUCE); if FORMULA is empty then return VREDUCE else if FORMULA contains an empty clause then *fail* else begin pick a variable V in FORMULA; *choose* a truth value TF; return(append(V->TF, VREDUCE, davis-putnam(substitute(V,TF,FORMULA))) end endif end davis-putnam /* substitute(TF, V, FORMULA) returns the formula obtained by substituting truth-vakye TF for variable V in FORMULA */ function substitute(TF, V, FORMULA) for each clause C in FORMULA do if [C contains V and TF = TRUE] or [C contains not V and TF = FALSE] then delete C from FORMULA else if [C contains V and TF = FALSE] or [C contains not V and TF = TRUE] then delete V from C endif endfor return FORMULA end substitute /* reduce(FORMULA,VREDUCE) does simple reduction on a formula without lookahead. If there is a clause with only one literal, then that variable must have the indicated value, and this value can be substituted. This can be iterated until all clauses have at least two literals. VREDUCE holds the values computed. procedure reduce(in out FORMULA, VREDUCE) VREDUCE := the empty valuation; while there exists a clause C in FORMULA with only one literal L if L is a positive variable V then FORMULA := substitute(TRUE, V, FORMULA) VREDUCE := cons(V-> TRUE, VREDUCE); else if L is the negation of variable V then FORMULA := substitute(FALSE,V,FORMULA) VREDUCE := cons(V-> FALSE, VREDUCE); endif endwhile return(FORMULA) end reduce Example: Let F1 be the following set of clauses { 1. not p or q or r or not z. 2. not p or not q or not z 3. not p or not r. 4. not p or q or z. 5. p or not q or r. 6. z } dp(F1) reduce(F1) substitutes z->TRUE, giving the new formula F2 { 1. not p or q or r 2. not p or not q 3. not p or not r. 5. p or not q or r.} and the valuation { z-> TRUE } try p -> TRUE substitute(TRUE,p,F2) gives the new formula F3 { 1. q or r 2. not q 3. not r } dp(F3) reduce F3 gives the empty clause in 1; fail;' try p -> FALSE substitute(FALSE,p,F2) gives the new formula F4 { 5. not q or r } dp(F4) reduce(F4) has no effect; try q -> TRUE; substitute(TRUE,q,F4) gives the new formula F5: { r } reduce(F5) returns the empty formula and the valuation {r -> TRUE} return q -> TRUE, r -> TRUE; return p -> FALSE, z -> TRUE, q -> TRUE, r -> TRUE.