ECCC-Report TR05-066https://eccc.weizmann.ac.il/report/2005/066Comments and Revisions published for TR05-066en-usFri, 11 Nov 2005 00:00:00 +0200
Revision 2
| Narrow Proofs May Be Spacious: Separating Space and Width in Resolution |
Jakob Nordström
https://eccc.weizmann.ac.il/report/2005/066#revision2The 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.
Fri, 11 Nov 2005 00:00:00 +0200https://eccc.weizmann.ac.il/report/2005/066#revision2
Comment 1
| A Tight Bound on the Refutation Clause Space of Pebbling Contradictions over Binary Trees Comment on: TR05-066 |
Jakob Nordström
https://eccc.weizmann.ac.il/report/2005/066#comment1 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.
Wed, 14 Sep 2005 17:33:52 +0300https://eccc.weizmann.ac.il/report/2005/066#comment1
Revision 1
| Narrow Proofs May Be Spacious: Separating Space and Width in Resolution |
Jakob Nordström
https://eccc.weizmann.ac.il/report/2005/066#revision1The 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.
Tue, 23 Aug 2005 00:00:00 +0300https://eccc.weizmann.ac.il/report/2005/066#revision1
Paper TR05-066
| Narrow Proofs May Be Spacious: Separating Space and Width in Resolution |
Jakob Nordström
https://eccc.weizmann.ac.il/report/2005/066The 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.
Thu, 30 Jun 2005 16:21:20 +0300https://eccc.weizmann.ac.il/report/2005/066