Content deleted Content added
→Overview: Wth? Φ is never a set of literals, but a set of clauses. What is meant here is that Φ consists of a single nonempty clause; this is not enough, as it does not catch the case when Φ is empty, and on the other hand, the single clause would be immediately eliminated by pure literal elimination anyway. Thus, it's easiest to just check for Φ being empty. |
→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. |
||
Line 25:
'''if''' Φ contains an empty clause '''then'''
'''return''' false;
'''for every''' unit clause {''l''}
Φ ← ''unit-propagate''(''l'', Φ);
'''for every'''
Φ ← ''remove-from-formula''(''c'', Φ);
'''for every''' literal ''l'' that occurs pure in Φ '''do'''
Φ ← ''pure-literal-assign''(''l'', Φ);
// ''Davis-Putnam procedure:''
'''for every''' literal ''l'' that occurs in both polarities
'''for every''' clause ''c'' containing ''l'' and every clause ''n'' containing the negation of ''l''
''r'' ← ''resolve''(''c'', ''n'');
Φ ← ''add-to-formula''(''r'', Φ);
'''for every''' clause ''c'' that contains ''l'' or its negation '''do'''
Φ ← ''remove-from-formula''(''c'', Φ);
'''return''' ''DP-SAT''(Φ);
{{Algorithm-end}}
| |||