Content deleted Content added
→Overview: Even if not present in the original formula, the resolution step may generate clauses that contain a variable with both polarities. These better be be eliminated. |
→Overview: This is a confusing name, as the procedure as given does not construct a satisfying assignment, it only checks satisfiability. In fact, it's easiest to just spell it out. |
||
Line 29:
'''for every''' clause ''c'' in Φ that contains both a literal ''l'' and its negation '''do'''
Φ ← ''remove-from-formula''(''c'', Φ);
// ''pure literal elimination:''
'''for every''' literal ''l'' that occurs pure in Φ '''do'''
Φ ← ''remove-from-formula''(''c'', Φ);
// ''Davis-Putnam procedure:''
'''for every''' literal ''l'' that occurs in both polarities in Φ '''do'''
| |||