Revision #2 Authors: Oliver Kullmann

Accepted on: 16th February 2000 00:00

Downloads: 28245

Keywords:

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.

Revision #1 Authors: Oliver Kullmann

Accepted on: 27th October 1999 00:00

Downloads: 996

Keywords:

automatization,
generalized Horn formulas,
generalized input resolution,
linear autarkies,
pebble games,
pebbling formulas,
pigeonhole formulas,
polynomial time,
relativized resolution,
SAT decision,
upper and lower bounds for size and space complexity of (tree-like) resolution,
width restricted resolution

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.