07/01/1996 09:00 AM
Resolution has not been an effective tool for deciding satisfiability of propositional CNF formulas, due to explosion of the search space, particularly when the formula is satisfiable. A new pruning method is described, which is designed to eliminate certain refutation attempts that cannot succeed. The method exploits the concept of ``autarky\'\', which was introduced by Monien and Speckenmeyer. New forms of lemma creation are also introduced, which eliminate the need to carry out refutation attempts that must succeed. The resulting algorithm, called ``Modoc\'\', is a modification of propositional model elimination. Informally, an autarky is a ``self- sufficient\'\' model for some clauses, but which does not affect the remaining clauses of the formula. Whereas Monien and Speckenmeyer\'s work was oriented toward finding a model, our method has as its primary goal to find a refutation in the style of model elimination. However, Modoc finds a model if it fails to find a refutation, essentially by combining autarkies. Unlike the pruning strategies of most refinements of resolution, autarky-related pruning only prunes refutation attempts that ultimately will be unsuccessful; consequently, it will not force the underlying search to find an unnecessarily long refutation. The other major innovation is Modoc\'s lemma management. Building upon the C-literal strategy proposed by Shostak and studied further by Letz, Mayr and Goller, methods for ``eager\'\' lemmas, ``quasi-persistent\'\' lemmas, and two forms of controlled cut are described. Experimental data based on an implementation in C is reported. On random formulas, Modoc is not as effective as recently reported model-searching methods. On more structured formulas, such as circuit-fault detection, it is superior.