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.

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.

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.