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.
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.
