Complexity Analysis of Propositional Resolution with Autarky Pruning

An algorithm called Modoc", which has been introduced elsewhere, enhances propositional model elimination with autarky pruning, and other features. The model elimination method is based on linear resolution, and is designed to produce refutations of formulas in conjunctive normal form CNF. Informally, an autarky is a self-su cient" model for some clauses, but which does not a ect the remaining clauses of the formula. Modoc nds a model if it fails to nd a refutation, essentially by combining autarkies. Although the original motivation for autarky pruning was to extract a model when the refutation attempt failed, practical experience has shown that it also greatly increases the performance, by reducing the amount of search redundancy. This paper presents a worst-case analysis of Modoc as a function of the number of propositional variables in the formula. The analysis sheds light on why autarky pruning improves the performance, compared to standard" model elimination. A wo...

• Type: Journal
• Year: 1999
• Where: DAM
• Authors: Allen Van Gelder
• Keywords: DAM 1999, Model Elimination, Refutation, Upper Bound