Towards an optimal separation of space and length in resolution
(2008) 40th Annual ACM Symposium on Theory of Computing, STOC 2008 In Proceedings of the Annual ACM Symposium on Theory of Computing p.701-710- Abstract
Most state-of-the-art satisfiability algorithms today are variants of the DPLL procedure augmented with clause learning. The main bottleneck for such algorithms, other than the obvious one of time, is the amount of memory used, fn the field of proof complexity, the resources of time and memory correspond to the length and space of resolution proofs. There has been a long line of research trying to understand these proof complexity measures, as well as relating them to the width of proofs, i.e., the size of the largest clause in the proof, which has been shown to be intimately connected with both length and space. While strong results have been proven for length and width, our understanding of space is still quite poor. For instance, it... (More)
Most state-of-the-art satisfiability algorithms today are variants of the DPLL procedure augmented with clause learning. The main bottleneck for such algorithms, other than the obvious one of time, is the amount of memory used, fn the field of proof complexity, the resources of time and memory correspond to the length and space of resolution proofs. There has been a long line of research trying to understand these proof complexity measures, as well as relating them to the width of proofs, i.e., the size of the largest clause in the proof, which has been shown to be intimately connected with both length and space. While strong results have been proven for length and width, our understanding of space is still quite poor. For instance, it has remained open whether the fact that a formula is provable in short length implies that it is also provable in small space (which is the case for length versus width), or whether on the contrary these measures are completely unrelated in the sense that short proofs can be arbitrarily complex with respect to space. In this paper, we present some evidence that the true answer should be that the latter case holds and provide a possible roadmap for how such an optimal separation result could be obtained. We do this by proving a tight bound of Θ(√n) on the space needed for so-called pebbling contradictions over pyramid graphs of size n. Also, continuing the line of research initiated by (Ben-Sasson 2002) into trade-offs between different proof complexity measures, we present a simplified proof of the recent length-space trade-off result in (Hertel and Pitassi 2007), and show how our ideas can be used to prove a couple of other exponential trade-offs in resolution.
(Less)
- author
- Nordström, Jakob LU and Håstad, Johan
- publishing date
- 2008
- type
- Chapter in Book/Report/Conference proceeding
- publication status
- published
- subject
- keywords
- Length, Lower bound, Pebbling, Proof complexity, Resolution, Separation, Space
- host publication
- STOC'08 : Proceedings of the 2008 ACM Symposium on Theory of Computing - Proceedings of the 2008 ACM Symposium on Theory of Computing
- series title
- Proceedings of the Annual ACM Symposium on Theory of Computing
- pages
- 10 pages
- publisher
- Association for Computing Machinery (ACM)
- conference name
- 40th Annual ACM Symposium on Theory of Computing, STOC 2008
- conference location
- Victoria, BC, Canada
- conference dates
- 2008-05-17 - 2008-05-20
- external identifiers
-
- scopus:57049099276
- ISSN
- 0737-8017
- ISBN
- 9781605580470
- DOI
- 10.1145/1374376.1374478
- language
- English
- LU publication?
- no
- id
- d87bb537-615d-488c-89b2-5a2a6f0c2d1d
- date added to LUP
- 2020-12-18 22:29:41
- date last changed
- 2025-04-04 14:50:54
@inproceedings{d87bb537-615d-488c-89b2-5a2a6f0c2d1d,
abstract = {{<p>Most state-of-the-art satisfiability algorithms today are variants of the DPLL procedure augmented with clause learning. The main bottleneck for such algorithms, other than the obvious one of time, is the amount of memory used, fn the field of proof complexity, the resources of time and memory correspond to the length and space of resolution proofs. There has been a long line of research trying to understand these proof complexity measures, as well as relating them to the width of proofs, i.e., the size of the largest clause in the proof, which has been shown to be intimately connected with both length and space. While strong results have been proven for length and width, our understanding of space is still quite poor. For instance, it has remained open whether the fact that a formula is provable in short length implies that it is also provable in small space (which is the case for length versus width), or whether on the contrary these measures are completely unrelated in the sense that short proofs can be arbitrarily complex with respect to space. In this paper, we present some evidence that the true answer should be that the latter case holds and provide a possible roadmap for how such an optimal separation result could be obtained. We do this by proving a tight bound of Θ(√n) on the space needed for so-called pebbling contradictions over pyramid graphs of size n. Also, continuing the line of research initiated by (Ben-Sasson 2002) into trade-offs between different proof complexity measures, we present a simplified proof of the recent length-space trade-off result in (Hertel and Pitassi 2007), and show how our ideas can be used to prove a couple of other exponential trade-offs in resolution.</p>}},
author = {{Nordström, Jakob and Håstad, Johan}},
booktitle = {{STOC'08 : Proceedings of the 2008 ACM Symposium on Theory of Computing}},
isbn = {{9781605580470}},
issn = {{0737-8017}},
keywords = {{Length; Lower bound; Pebbling; Proof complexity; Resolution; Separation; Space}},
language = {{eng}},
pages = {{701--710}},
publisher = {{Association for Computing Machinery (ACM)}},
series = {{Proceedings of the Annual ACM Symposium on Theory of Computing}},
title = {{Towards an optimal separation of space and length in resolution}},
url = {{http://dx.doi.org/10.1145/1374376.1374478}},
doi = {{10.1145/1374376.1374478}},
year = {{2008}},
}