Revision as of 17:07, 5 February 2009 edit SmackBot (talk \| contribs) 3,734,324 edits m Date maintenance tags and general fixes ← Previous edit		Revision as of 19:06, 8 April 2009 edit undo CRGreathouse (talk \| contribs) Autopatrolled, Administrators 13,002 edits See also links per WP:ALSO; disambig link Next edit →
Line 17: ** remove all original clauses containing the variable or its negation The step done for each variable preserve satisfiability, while not preserving the models; in other words, the generated formula is [[equisatisfiable]] but not [[Logical equivalence\|equivalent]] with the original one. The [[DPLL algorithm]] is a refinement of the Davis–Putnam procedure that stemmed from its first implementation. ==See also== [[DPLL algorithm]] [[Herbrandization]] Line 30 ⟶ 28: \|last=Davis \|first=Martin \| coauthors= ~~[[Hillary Putnam\|~~Putnam, Hillary]]▼ ~~\| authorlink= Martin Davis~~ ▲\| coauthors= [[Hillary Putnam\|Putnam, Hillary]] \| title=A Computing Procedure for Quantification Theory \| journal =[[Journal of the ACM]]

Davis–Putnam algorithm: Difference between revisions