Short proofs may be spacious : An optimal separation of space and length in resolution
(2008) 49th Annual IEEE Symposium on Foundations of Computer Science, FOCS 2008 In Proceedings - Annual IEEE Symposium on Foundations of Computer Science, FOCS p.709-718- Abstract
A number of works have looked at the relationship between length and space of resolution proofs. A notorious question has been whether the existence of a short proof implies the existence of a proof that can be verified using limited space. In this paper we resolve the question by answering it negatively in the strongest possible way. We show that there are families of 6-CNF formulas of size n, for arbitrarily large n, that have resolution proofs of length O(n) but for which any proof requires space Ω(n/log n). This is the strongest asymptotic separation possible since any proof of length O(n) can always be transformed into a proof in space O(n/log n). Our result follows by reducing the space complexity of so called pebbling formulas... (More)
A number of works have looked at the relationship between length and space of resolution proofs. A notorious question has been whether the existence of a short proof implies the existence of a proof that can be verified using limited space. In this paper we resolve the question by answering it negatively in the strongest possible way. We show that there are families of 6-CNF formulas of size n, for arbitrarily large n, that have resolution proofs of length O(n) but for which any proof requires space Ω(n/log n). This is the strongest asymptotic separation possible since any proof of length O(n) can always be transformed into a proof in space O(n/log n). Our result follows by reducing the space complexity of so called pebbling formulas over a directed acyclic graph to the black-white pebbling price of the graph. The proof is somewhat simpler than previous results (in particular, those reported in [Nordström 2006, Nordström and Håstad 2008]) as it uses a slightly different flavor of pebbling formulas which allows for a rather straightforward reduction of proof space to standard black-white pebbling price.
(Less)
- author
- Ben-Sasson, Eli and Nordström, Jakob LU
- publishing date
- 2008
- type
- Chapter in Book/Report/Conference proceeding
- publication status
- published
- subject
- host publication
- Proceedings of the 49th Annual IEEE Symposium on Foundations of Computer Science, FOCS 2008
- series title
- Proceedings - Annual IEEE Symposium on Foundations of Computer Science, FOCS
- article number
- 4691003
- pages
- 10 pages
- publisher
- IEEE - Institute of Electrical and Electronics Engineers Inc.
- conference name
- 49th Annual IEEE Symposium on Foundations of Computer Science, FOCS 2008
- conference location
- Philadelphia, PA, United States
- conference dates
- 2008-10-25 - 2008-10-28
- external identifiers
-
- scopus:57949109817
- ISSN
- 0272-5428
- ISBN
- 9780769534367
- DOI
- 10.1109/FOCS.2008.42
- language
- English
- LU publication?
- no
- id
- b9f6c820-6f6f-4bb4-bdb4-e99495954c98
- date added to LUP
- 2020-12-18 22:29:19
- date last changed
- 2022-02-01 18:41:10
@inproceedings{b9f6c820-6f6f-4bb4-bdb4-e99495954c98,
abstract = {{<p>A number of works have looked at the relationship between length and space of resolution proofs. A notorious question has been whether the existence of a short proof implies the existence of a proof that can be verified using limited space. In this paper we resolve the question by answering it negatively in the strongest possible way. We show that there are families of 6-CNF formulas of size n, for arbitrarily large n, that have resolution proofs of length O(n) but for which any proof requires space Ω(n/log n). This is the strongest asymptotic separation possible since any proof of length O(n) can always be transformed into a proof in space O(n/log n). Our result follows by reducing the space complexity of so called pebbling formulas over a directed acyclic graph to the black-white pebbling price of the graph. The proof is somewhat simpler than previous results (in particular, those reported in [Nordström 2006, Nordström and Håstad 2008]) as it uses a slightly different flavor of pebbling formulas which allows for a rather straightforward reduction of proof space to standard black-white pebbling price.</p>}},
author = {{Ben-Sasson, Eli and Nordström, Jakob}},
booktitle = {{Proceedings of the 49th Annual IEEE Symposium on Foundations of Computer Science, FOCS 2008}},
isbn = {{9780769534367}},
issn = {{0272-5428}},
language = {{eng}},
pages = {{709--718}},
publisher = {{IEEE - Institute of Electrical and Electronics Engineers Inc.}},
series = {{Proceedings - Annual IEEE Symposium on Foundations of Computer Science, FOCS}},
title = {{Short proofs may be spacious : An optimal separation of space and length in resolution}},
url = {{http://dx.doi.org/10.1109/FOCS.2008.42}},
doi = {{10.1109/FOCS.2008.42}},
year = {{2008}},
}