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 give the first extension of the result due to Paul, Pippenger, Szemeredi and Trotter that deterministic linear time is distinct from nondeterministic linear time. We show that DTIME(n \sqrt(log^{*}(n))) \neq NTIME(n \sqrt(log^{*}(n))). We show that atleast one of the following statements holds: (1) P \neq L (2) For all ... more >>>

We provide a characterization of the resolution width introduced in the context of Propositional Proof Complexity in terms of the existential pebble game introduced in the context of Finite Model Theory. The characterization is tight and purely combinatorial. Our first application of this result is a surprising proof that the ... more >>>

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