Narrow proofs may be spacious : Separating space and width in resolution
(2006) 38th Annual ACM Symposium on Theory of Computing, STOC'06 In Proceedings of the Annual ACM Symposium on Theory of Computing 2006. p.507-516- 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... (More)
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.
(Less)
- author
- Nordström, Jakob LU
- publishing date
- 2006
- type
- Chapter in Book/Report/Conference proceeding
- publication status
- published
- subject
- keywords
- Lower bound, Pebble game, Pebbling contradiction, Proof complexity, Resolution, Separation, Space, Width
- host publication
- STOC'06 : Proceedings of the 38th Annual ACM Symposium on Theory of Computing - Proceedings of the 38th Annual ACM Symposium on Theory of Computing
- series title
- Proceedings of the Annual ACM Symposium on Theory of Computing
- volume
- 2006
- pages
- 10 pages
- publisher
- Association for Computing Machinery (ACM)
- conference name
- 38th Annual ACM Symposium on Theory of Computing, STOC'06
- conference location
- Seattle, WA, United States
- conference dates
- 2006-05-21 - 2006-05-23
- external identifiers
-
- scopus:33748114893
- ISSN
- 0737-8017
- ISBN
- 1595931341
- 9781595931344
- DOI
- 10.1145/1132516.1132590
- language
- English
- LU publication?
- no
- id
- 8daf018d-0f74-4303-9161-dc3f137ea9b6
- date added to LUP
- 2020-12-18 22:29:58
- date last changed
- 2022-02-01 18:41:10
@inproceedings{8daf018d-0f74-4303-9161-dc3f137ea9b6,
abstract = {{<p>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.</p>}},
author = {{Nordström, Jakob}},
booktitle = {{STOC'06 : Proceedings of the 38th Annual ACM Symposium on Theory of Computing}},
isbn = {{1595931341}},
issn = {{0737-8017}},
keywords = {{Lower bound; Pebble game; Pebbling contradiction; Proof complexity; Resolution; Separation; Space; Width}},
language = {{eng}},
pages = {{507--516}},
publisher = {{Association for Computing Machinery (ACM)}},
series = {{Proceedings of the Annual ACM Symposium on Theory of Computing}},
title = {{Narrow proofs may be spacious : Separating space and width in resolution}},
url = {{http://dx.doi.org/10.1145/1132516.1132590}},
doi = {{10.1145/1132516.1132590}},
volume = {{2006}},
year = {{2006}},
}