A relativized hierarchy of conjunctive normal forms is introduced, recognizable and SAT decidable in polynomial time. The corresponding hardness parameter, the first level of inclusion in the hierarchy, is studied in detail, admitting several characterizations, e.g., using pebble games, the space complexity of (relativized) tree-like resolution or nested input resolution, ... more >>>

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 ... more >>>