Sciweavers

DAM
1999

Complexity Analysis of Propositional Resolution with Autarky Pruning

13 years 3 months ago
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...
Allen Van Gelder
Added 22 Dec 2010
Updated 22 Dec 2010
Type Journal
Year 1999
Where DAM
Authors Allen Van Gelder
Comments (0)