Davis–Putnam algorithm: Difference between revisions

Content deleted Content added
Overview: Resolution is not a function of c and n only, it also depends on the choice of l. Better to spell this out. Unit propagation is also easy to spell out to reduce dependence on unexplained functions.
Overview: Unit propagation etc. is supposed to be done before EACH elimination of a literal l by the DP procedure, thus the loop should be moved outwards. In fact, there is no need to make this formally a recursive algorithm.
Line 21:
 
'''function''' DP-SAT(Φ)
'''repeat'''
'''if''' Φ is empty '''then'''
'''return''' true;
'''if''' Φ contains an empty clause '''then'''
'''return''' false;
// ''unit propagation:''
'''while''' Φ contains a unit clause {''l''} '''do'''
Φ ← ''remove-from-formula''({''l''}, Φ);
'''for every''' clause ''c'' in Φ that contains ¬''l'' '''do'''
Φ ← ''remove-from-formula''(''c'', Φ);
Φ ← ''add-to-formula''(''c'' \ {¬''l''}, Φ);
'''for every''' clause ''c'' in Φ containingthat ''l''contains andboth everya clauseliteral ''nl'' in Φ containingand its negation ¬''l'' '''do'''
Φ ← ''remove-from-formula''(''c'', Φ);
// ''pure literal elimination:''
Φ ← ''add-to-formula''(''c'' \ {¬''l''}, Φ);
'''for every''' clauseliteral ''cl'' in Φ that containsoccurs bothpure ain literal ''l'' and its negation ¬''l''Φ '''do'''
Φ ''remove-from-formula'for every'('' clause ''c'', in Φ); that contains ''l'' '''do'''
Φ ← ''remove-from-formula''(''c'', Φ);
// ''pure literal elimination:''
// ''Davis-Putnam procedure:''
'''for every''' literal ''l'' that occurs pure in Φ '''do'''
pick '''for every'''a clauseliteral ''cl'' inthat Φoccurs thatwith containsboth ''l''polarities '''do'''in Φ
'''for every''' clause ''c'' in Φ containing ''l'' and every clause ''n'' in Φ containing its negation ¬''l'' '''do'''
Φ ← ''remove-from-formula''(''c'', Φ);
// ''Davis-Putnam procedure:''
'''for every''' literal ''l'' that occurs with both polarities in Φ '''do'''
'''for every''' clause ''c'' in Φ containing ''l'' and every clause ''n'' in Φ containing its negation ¬''l'' '''do'''
// ''resolve c with n:''
''r'' ← (''c'' \ {''l''}) ∪ (''n'' \ {¬''l''});
Φ ← ''add-to-formula''(''r'', Φ);
'''for every''' clause ''c'' that contains ''l'' or ¬''l'' '''do'''
Φ ← ''remove-from-formula''(''c'', Φ);
'''return''' ''DP-SAT''(Φ);
{{Algorithm-end}}