Talk:DPLL algorithm

From Wikipedia, the free encyclopedia

You have new messages (last change).

[edit] Subsumption

I've checked the original CACM-1962 paper, and it does not mention subsumption in the DPLL algorithm at all. The three rules are I) the one literal clause rule, now known as "unit propagation", II) affirmative-negative rule, now "pure literal elemination", and III*) Splitting Rule, still known under that name. The authors do mention "systematic elemination of redundancy", but only with respect to the original Davis-Putnam algorithm, not with respect to DPLL. I'll revert todays change (with some extra clarification). If anyone has more information, I'm interested in hearing it. --Stephan Schulz 17:40, 24 October 2005 (UTC)

Ok. I had based my description on not-so-recent papers. In particular, I think that one by Crawford and Auton mentioned the clause subsumption rule (and said it was not useful); the fact that the pure literal rule was decided not useful seems to be a very recent finding--I didn't know it. User:Tizio 18:23, 24 October 2005 (UTC)
The "two watch literal" technique pioneered in Chaff has made unit propagation very cheap. In particular, it makes the speed of unit propagation nearly independent of the number of clauses. Thus the gain of a smaller (by number of clauses) formula is nearly nil, while a comparable breakthrough in searching for pure literals has not yet been found. --Stephan Schulz 18:53, 24 October 2005 (UTC)

Good to know! Thanks for the clarification. User:Tizio 21:39, 24 October 2005 (UTC)

In the DPLL pseudocode, why is the second argument provided, given that it is neither used nor returned? Wouldn't the pseudocode be clearer and shorter without this second argument? If the second argument were to be retained, shouldn't the text describe how the algorithm can be modified to return a satisfying truth assignment if there is one? 58.162.12.107 04:10, 29 October 2006 (UTC)

But it is used, in the recursive calls to the sub-provers. It's not returned, though. I've added a note to this effect.--Stephan Schulz 22:54, 29 October 2006 (UTC)
Retrieved from "http://en.wikipedia.org../../../d/p/l/Talk%7EDPLL_algorithm_6255.html"