zbMATH — the first resource for mathematics

Satisfiability testing with more reasoning and less guessing. (English) Zbl 0868.03007
Johnson, David S. (ed.) et al., Cliques, coloring, and satisfiability. Second DIMACS implementation challenge. Proceedings of a workshop held at DIMACS, October 11–13, 1993. Providence, RI: American Mathematical Society. DIMACS, Ser. Discrete Math. Theor. Comput. Sci. 26, 559-586 (1996).
This paper presents a new algorithm for propositional satisfiability. The algorithm is a development of the classical Davis-Putnam algorithm. The Davis-Putnam algorithm (as modified by Davis-Logemann-Loveland) interleaves phases of “reasoning” (i.e., the unit-clause rule and the pure-literal rule) and phases of “guessing” (i.e., the splitting rule). The thrust of the new algorithm is to increase the amount of reasoning and decrease the amount of guessing. The proposed reasoning component is \(k\)-limited resolution (with \(k=2,3\)), that is, resolution where parents and resolvents may have at most \(k\) literals. The advantage with respect to unlimited resolution is that \(k\)-limited resolution takes polynomial time \(O(n^k)\), where \(n\) is the number of propositional variables. Other inference rules are equivalent literals recognition, subsumption and clausal simplification by unit or binary clauses, and the pure-literal rule. For the “guessing” part, the paper proposes a new criterion to select the propositional variable for the next step of splitting. This criterion aims at maximizing the reduction of the size of the set of clauses.
The second part of the paper is a statistical analysis of the performances of an implementation of the algorithm on various sets of clauses, including both randomly generated sets, and sets from circuit-fault analysis.The discussion includes important remarks on the proper application of statistics to computer experiments. A related paper is H. Zhang, M. P. Bonacina and J. Hsiang, “PSATO: a distributed propositional prover and its application to quasigroup problems” [J. Symb. Comput. 21, No. 4-6, 543-560 (1996; Zbl 0863.68013)], which presents a parallelization of the Davis-Putnam algorithm, and its application to satisfiability problems from quasigroup theory.
For the entire collection see [Zbl 0851.00080].

03B35 Mechanization of proofs and logical operations
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03B05 Classical propositional logic
PDF BibTeX Cite