Revision as of 19:45, 21 May 2015 edit Jochen Burghardt (talk \| contribs) Extended confirmed users 24,306 edits Undid own revision 663446391: DPLL was already mentioned in article ← Previous edit		Revision as of 19:48, 21 May 2015 edit undo Jochen Burghardt (talk \| contribs) Extended confirmed users 24,306 edits →top: devote an own paragraph to DPLL, as it is the best algorithm as of today Next edit →
Line 17: ** remove all original clauses containing the variable or its negation At each step, the intermediate formula generated is [[equisatisfiable]] to the original formula, but it does not retain [[Logical equivalence\|equivalence]]. The resolution step leads to a worst-case exponential blow-up in the size of the formula. The [[~~DPLL~~Davis–Putnam–Logemann–Loveland algorithm]] is a 1962 refinement of the propositional satisfiability step of the Davis–Putnam procedure, ~~that~~which requires only a linear amount of memory in the worst case. It still forms the basis for today's (as of 2015) most efficient complete [[SAT solver]]s. ==See also==

Davis–Putnam algorithm: Difference between revisions