Davis-Putnam
The best complete algorithm for SAT is Davis-Putnam
- first work by Davis-Putnam 1961
- current version by Davis-Logemann-Loveland 1962
- variously called DP/DLL/DPLL or just Davis-Putnam
- I will present a slight variant omitting “Pure literal” rule
Two stopping cases
- an empty set of clauses is trivially satisfiable
- an empty clause is trivially unsatisfiable
- there is no way to satisfy the clause