Implementing the Davis–Putnam Method

摘要: The method proposed by Davis, Putnam, Logemann, and Loveland for propositional reasoning, often referred to as the Davis–Putnam method, is one of major practical methods satisfiability (SAT) problem logic. We show how implement efficiently using trie data structure clauses. A new technique indexing only first last literals clauses yields a unit propagation procedure whose complexity sublinear number occurrences variable in input. also that can work better when subsumption not used. illustrate performance our programs on some quasigroup problems. efficiency has enabled us solve open