ECCC
Electronic Colloquium on Computational Complexity
Login | Register | Classic Style



REPORTS > DETAIL:

Revision(s):

Revision #2 to TR05-066 | 11th November 2005 00:00

Narrow Proofs May Be Spacious: Separating Space and Width in Resolution

RSS-Feed




Revision #2
Authors: Jakob Nordström
Accepted on: 11th November 2005 00:00
Downloads: 590
Keywords: 


Abstract:

The width of a resolution proof is the maximal number of literals
in any clause of the proof. The space of a proof is the maximal
number of memory cells used if the proof is only allowed to
resolve on clauses kept in memory. Both of these measures have
previously been studied and related to the refutation size of
unsatisfiable CNF formulas. Also, the resolution refutation space
of a formula has been proven to be at least as large as the
refutation width, but it has remained unknown whether space can
be separated from width or the two measures coincide
asymptotically. We prove that there is a family of k-CNF formulas
for which the refutation width in resolution is constant but the
refutation space is non-constant, thus solving an open problem
mentioned in several previous papers.

In this revision of our article, we improve our previous result
to an asymptotically tight bound on the refutation space of
pebbling contradictions over binary trees. This is done by
proving some technical results on the structure of unsatisfiable
CNF formulas that might be of independent interest.


Revision #1 to TR05-066 | 23rd August 2005 00:00

Narrow Proofs May Be Spacious: Separating Space and Width in Resolution





Revision #1
Authors: Jakob Nordström
Accepted on: 23rd August 2005 00:00
Downloads: 577
Keywords: 


Abstract:

The width of a resolution proof is the maximal number of literals in any clause of the proof. The space of a proof is the maximal number of memory cells used if the proof is only allowed to resolve on clauses kept in memory. Both of these measures have previously been studied and related to the refutation size of unsatisfiable CNF formulas. Also, the resolution refutation space of a formula has been proven to be at least as large as the refutation width, but it has remained unknown whether space can be separated from width or the two measures coincide asymptotically. We prove that there is a family of k-CNF formulas for which the refutation width in resolution is constant but the refutation space is non-constant, thus solving an open problem mentioned in several previous papers.


Paper:

TR05-066 | 4th June 2005 00:00

Narrow Proofs May Be Spacious: Separating Space and Width in Resolution





TR05-066
Authors: Jakob Nordström
Publication: 30th June 2005 16:21
Downloads: 565
Keywords: 


Abstract:

The width of a resolution proof is the maximal number of literals in any clause of the proof. The space of a proof is the maximal number of memory cells used if the proof is only allowed to resolve on clauses kept in memory. Both of these measures have previously been studied and related to the refutation size of unsatisfiable CNF formulas. Also, the resolution refutation space of a formula has been proven to be at least as large as the refutation width, but it has remained unknown whether space can be separated from width or the two measures coincide asymptotically. We prove that there is a family of k-CNF formulas for which the refutation width in resolution is constant but the refutation space is non-constant, thus solving an open problem mentioned in several previous papers.


Comment(s):

Comment #1 to TR05-066 | 14th September 2005 17:33

A Tight Bound on the Refutation Clause Space of Pebbling Contradictions over Binary Trees Comment on: TR05-066





Comment #1
Authors: Jakob Nordström
Accepted on: 14th September 2005 17:33
Downloads: 583
Keywords: 


Abstract:

In ECCC Technical Report TR05-066, we proved that space
can be separated from width, answering an open question in several
previous papers. In these notes we sharpen this result to a tight
bound on the refutation space of pebbling contradictions over binary
trees. The new result, which also allows a considerable
simplification of the analysis of the pebbling game induced by
resolution derivations, will be incorporated in a later version of
the technical report.




ISSN 1433-8092 | Imprint