Resolution and Pebbling Games

We define a collection of Prover-Delayer games to charac- terise some subsystems of propositional resolution. We give some natural criteria for the games which guarantee lower bounds on the resolution width. By an adaptation of the size-width tradeoff for resolution of [10] this result also gives lower bounds on proof size. We also use games to give upper bounds on proof size, and in par- ticular 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 gen- erate resolution refutations. On bounded width formulas, our algorithm is as least as good as the width based algorithm of [10]. 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 results in both directions when “almost satisfiable” means that it is hard to distuinguish F from a satisfiable formula using limited pebbling games.