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

Nordström, J 2006, Narrow proofs may be spacious: Separating space and width in resolution. in STOC'06: Proceedings of the 38th Annual ACM Symposium on Theory of Computing. Proceedings of the Annual ACM Symposium on Theory of Computing, vol. 2006, pp. 507-516, 38th Annual ACM Symposium on Theory of Computing, STOC'06, Seattle, WA, United States, 21/05/2006.

APA

Nordström, J. (2006). Narrow proofs may be spacious: Separating space and width in resolution. In STOC'06: Proceedings of the 38th Annual ACM Symposium on Theory of Computing (pp. 507-516). Proceedings of the Annual ACM Symposium on Theory of Computing Vol. 2006

Vancouver

Nordström J. Narrow proofs may be spacious: Separating space and width in resolution. In 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).

Author

Nordström, Jakob. / Narrow proofs may be spacious : Separating space and width in resolution. STOC'06: Proceedings of the 38th Annual ACM Symposium on Theory of Computing. 2006. pp. 507-516 (Proceedings of the Annual ACM Symposium on Theory of Computing, Vol. 2006).

Bibtex

@inproceedings{32766fa4309e4b3483ca639a92f8a521,
title = "Narrow proofs may be spacious: Separating space and width in resolution",
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 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.",
keywords = "Lower bound, Pebble game, Pebbling contradiction, Proof complexity, Resolution, Separation, Space, Width",
author = "Jakob Nordstr{\"o}m",
year = "2006",
language = "English",
isbn = "1595931341",
series = "Proceedings of the Annual ACM Symposium on Theory of Computing",
publisher = "Association for Computing Machinery (ACM)",
pages = "507--516",
booktitle = "STOC'06",
note = "38th Annual ACM Symposium on Theory of Computing, STOC'06 ; Conference date: 21-05-2006 Through 23-05-2006",

}

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