ECCC-Report TR04-112https://eccc.weizmann.ac.il/report/2004/112Comments and Revisions published for TR04-112en-usWed, 01 Dec 2004 22:31:31 +0200
Paper TR04-112
| Resolution and pebbling games |
Neil Thapen,
Nicola Galesi
https://eccc.weizmann.ac.il/report/2004/112We 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.
Wed, 01 Dec 2004 22:31:31 +0200https://eccc.weizmann.ac.il/report/2004/112