Revision as of 17:04, 26 June 2006 edit Jpbowen (talk \| contribs) Extended confirmed users, Pending changes reviewers 83,164 edits m Added category, links, tidying ← Previous edit		Revision as of 13:42, 6 September 2006 edit undo Jon Awbrey (talk \| contribs) 13,224 edits m ndash for polynominals Next edit →
Line 1: The '''~~Davis-Putnam~~Davis–Putnam algorithm''' is an algorithm developed by [[Martin Davis]] and [[Hilary Putnam]] for checking the [[Boolean satisfiability problem\|satisfiability]] of [[propositional logic]] formulae in [[conjunctive normal form]], ''i.e.'', sets of [[Clause (logic)\|clauses]]. It is a form of [[resolution (logic)\|resolution]] in which variables are iteratively chosen and removed by resolving every clause in which the variable is contained positively with any clause in which the variable is negated. The algorithm works as follows:

Davis–Putnam algorithm: Difference between revisions