Abstract:
Two side remarks are made in the previous version: -- on page 16 that a directed graph G' is embedabble into another directed graph G iff G' is a minor of G; -- on page 41 that the notion of "width" (defined on page 40) gives the pebbling complexity for arbitrary directed acyclic graphs G. Both assertions are used only for binary trees, where they hold true, but they are (quite obviously) false in the generality stated above. So this has been corrected. Additionally a few typos have been removed.

Abstract:
A relativized hierarchy of conjunctive normal forms is introduced, recognizable and SAT decidable in polynomial time. The corresponding hardness parameter h, the first level of inclusion in the hierarchy, is studied in detail and various natural characterizations are obtained, e.g., in the case of unsatisfiability, by means of pebble games, the space complexity of (relativized) tree-like resolution, or the necessary level of "nested input resolution." Furthermore h yields a "quasi-precise" general lower bound for (relativized) tree-like resolution, and hence searching through the hierarchy from below quasi-automatizes (relativized) tree-like resolution. Several examples are considered, like k-CNF, the Pigeonhole and the Pebbling formulas, and Krishnamurthy's graph formulas. For an improved handling of satisfiable formulas a new (and natural) application of Linear Programming is shown. Also a new form of width bounded (relativized) resolution is introduced, simulating nested input resolution and releasing the general lower bound on resolution of [Ben-Sasson, Wigderson 99] (TR99-022) from its dependence on the maximal input clause length.

Abstract:
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, and also yielding the best general lower bound for (relativized) tree-like resolution. Several examples are considered, for example k-CNF, the Pigeonhole and the Pebbling formulas, and Krishnamurthy's graph formulas. Also a new form of width bounded (relativized) resolution is introduced, simulating nested input resolution and releasing the general lower bound from [Ben-Sasson, Wigderson 99] from its dependence on the maximal input clause length.