Jump to content

Talk:DPLL algorithm

Page contents not supported in other languages.
From Wikipedia, the free encyclopedia
This is an old revision of this page, as edited by Stephan Schulz (talk | contribs) at 17:40, 24 October 2005 (Subsumption). The present address (URL) is a permanent link to this revision, which may differ significantly from the current revision.
(diff) ← Previous revision | Latest revision (diff) | Newer revision → (diff)

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)[reply]

Retrieved from "https://en.wikipedia.org/w/index.php?title=Talk:DPLL_algorithm&oldid=26367576"