Content deleted Content added
→Overview: The stopping conditions should be moved right before the DP procedure to ensure that there IS a non-pure literal |
→Overview: "For every" is not appropriate, as pure literal elimination may create new pure literals. |
||
Line 32:
Φ ← ''remove-from-formula''(''c'', Φ);
// ''pure literal elimination:''
'''
'''for every''' clause ''c'' in Φ that contains ''l'' '''do'''
Φ ← ''remove-from-formula''(''c'', Φ);
| |||