Davis–Putnam algorithm: Difference between revisions

Revision as of 12:14, 25 October 2008

Revision as of 04:27, 13 November 2008

Line 14:

* for every variable in the formula

** for every clause <math>c</math> containing the variable and every clause <math>n</math> containing the negation of the variable

*** [[Resolution (logic)|resolve]] <math>''c</math>'' and <math>''n</math>'' and add the resolvent to the formula

** remove all original clauses containing the variable or its negation