Weizmann Logo
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



TR04-112 | 26th November 2004 00:00

Resolution and pebbling games


Authors: Neil Thapen, Nicola Galesi
Publication: 1st December 2004 22:31
Downloads: 3163


We define a collection of Prover-Delayer games that characterize certain subsystems of resolution. This allows us to give some natural criteria which guarantee lower bounds on the resolution width of a formula, and to extend these results to formulas of unbounded initial width.

We also use games to give upper bounds on proof size, and in particular describe a good strategy for the Prover in a certain game which yields a short refutation of the Linear Ordering principle.

Using previous ideas we devise a new algorithm to automatically generate resolution refutations. On bounded width formulas, our algorithm is as least as good as the width based algorithm of [Ben-Sasson Wigderson]. Moreover, it finds short proofs of the Linear Ordering principle when the variables respect a given order.

Finally we approach the question of proving that a formula F is hard to refute if and only if is "almost" satisfiable. We prove both directions when "almost satisfiable" means that it is hard to distuinguish F from a satisfiable formula using limited pebbling games.

ISSN 1433-8092 | Imprint