Abstract:
We show that the Player-Adversary game from a paper by Pudlak and Impagliazzo played over CNF propositional formulas gives an exact characterization of the space needed in treelike resolution refutations. This characterization is purely combinatorial and independent of the notion of resolution. We use this characterization to give for the first time a separation between the space needed in tree-like and general resolution.