Weizmann Logo
ECCC
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



REPORTS > DETAIL:

Revision(s):

Revision #2 to TR99-041 | 16th February 2000 00:00

Investigating a general hierarchy of polynomially decidable classes of CNF's based on short tree-like resolution proofs

RSS-Feed




Revision #2
Authors: Oliver Kullmann
Accepted on: 16th February 2000 00:00
Downloads: 28139
Keywords: 


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.


Revision #1 to TR99-041 | 27th October 1999 00:00

Investigating a general hierarchy of polynomially decidable classes of CNF's based on short tree-like resolution proofs Revision of: TR99-041


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.


Paper:

TR99-041 | 22nd August 1999 00:00

Investigating a general hierarchy of polynomially decidable classes of CNF's based on short tree-like resolution proofs


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.



ISSN 1433-8092 | Imprint