Narrow proofs may be spacious: Separating space and width in resolution
Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
Standard
Narrow proofs may be spacious : Separating space and width in resolution. / Nordström, Jakob.
STOC'06: Proceedings of the 38th Annual ACM Symposium on Theory of Computing. 2006. p. 507-516 (Proceedings of the Annual ACM Symposium on Theory of Computing, Vol. 2006).Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
Harvard
APA
Vancouver
Author
Bibtex
}
RIS
TY - GEN
T1 - Narrow proofs may be spacious
T2 - 38th Annual ACM Symposium on Theory of Computing, STOC'06
AU - Nordström, Jakob
PY - 2006
Y1 - 2006
N2 - 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 clauses kept in memory simultaneously if the proof is only allowed to infer new clauses from clauses currently in memory. Both of these measures have previously been studied and related to the resolution refutation size of unsatisfiable CNF formulas. Also, the refutation space of a formula has been proven to be at least as large as the refutation width, but it has been open 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 a problem mentioned in several previous papers.
AB - 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 clauses kept in memory simultaneously if the proof is only allowed to infer new clauses from clauses currently in memory. Both of these measures have previously been studied and related to the resolution refutation size of unsatisfiable CNF formulas. Also, the refutation space of a formula has been proven to be at least as large as the refutation width, but it has been open 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 a problem mentioned in several previous papers.
KW - Lower bound
KW - Pebble game
KW - Pebbling contradiction
KW - Proof complexity
KW - Resolution
KW - Separation
KW - Space
KW - Width
UR - http://www.scopus.com/inward/record.url?scp=33748114893&partnerID=8YFLogxK
M3 - Article in proceedings
AN - SCOPUS:33748114893
SN - 1595931341
SN - 9781595931344
T3 - Proceedings of the Annual ACM Symposium on Theory of Computing
SP - 507
EP - 516
BT - STOC'06
Y2 - 21 May 2006 through 23 May 2006
ER -
ID: 251871221