10/01/1995 09:00 AM
Computer Science
Methodology is developed to attempt to construct simultaneously either a refutation or a model for a propositional formula in conjunctive normal form. The method exploits the concept of \"autarky\", which was introduced by Monien and Speckenmeyer. Informally, an autarky is a \"self-sufficient\" model for some clauses, but which does not affect the remaining clauses of the formula. Whereas their work was oriented toward finding a model, our method has as its primary goal to find a refutation in the style of model elimination. It also finds a model if it fails to find a refutation, essentially by combining autarkies. However, the autarky-related processing is integrated with the refutation search, and can greatly improve the efficiency of that search even when a refutation does exist. Unlike the pruning strategies of most refinements of resolution, autarky-related pruning does not prune any successful refutation; it only prunes attempts that ultimately will be unsuccessful; consequently, it will not force the underlying search to find an unnecessarily long refutation. A game characterization of refutation search is introduced, which demonstrates some symmetries in the search for a refutation and the search for a model. Limited experience with a prototype implementation is reported, and indicates the possibility of developing high-performance refutation methods that are competitive with recently reported model- searching methods. Considerations for first-order refutation methods are discussed briefly.
