Revision #2 Authors: Jakob Nordström

Accepted on: 11th November 2005 00:00

Downloads: 3034

Keywords:

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.

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.

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 #1 Authors: Jakob Nordström

Accepted on: 14th September 2005 17:33

Downloads: 3287

Keywords:

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.