Content deleted Content added
fixed category |
m link equisatisfiability |
||
Line 7:
*** 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
The step done for each variable preserve satisfiability, while not preserving the models; in other words, the generated formula is [[equisatisfiable]] but not [[equivalent]] with the original one.
The name ''Davis–Putnam algorithm'' or ''DP algorithm'' is sometimes incorrectly used to refer to the related but distinct [[DPLL algorithm]].
| |||