From small space to small width in resolution
(2014) 31st International Symposium on Theoretical Aspects of Computer Science, STACS 2014 In Leibniz International Proceedings in Informatics, LIPIcs 25. p.300-311- Abstract
In 2003, Atserias and Dalmau resolved a major open question about the resolution proof system by establishing that the space complexity of formulas is always an upper bound on the width needed to refute them. Their proof is beautiful but somewhat mysterious in that it relies heavily on tools from finite model theory. We give an alternative, completely elementary, proof that works by simple syntactic manipulations of resolution refutations. As a by-product, we develop a "black-box" technique for proving space lower bounds via a "static" complexity measure that works against any resolution refutation-previous techniques have been inherently adaptive. We conclude by showing that the related question for polynomial calculus (i.e., whether... (More)
In 2003, Atserias and Dalmau resolved a major open question about the resolution proof system by establishing that the space complexity of formulas is always an upper bound on the width needed to refute them. Their proof is beautiful but somewhat mysterious in that it relies heavily on tools from finite model theory. We give an alternative, completely elementary, proof that works by simple syntactic manipulations of resolution refutations. As a by-product, we develop a "black-box" technique for proving space lower bounds via a "static" complexity measure that works against any resolution refutation-previous techniques have been inherently adaptive. We conclude by showing that the related question for polynomial calculus (i.e., whether space is an upper bound on degree) seems unlikely to be resolvable by similar methods.
(Less)
- author
- Filmus, Yuval ; Lauria, Massimo ; Mikša, Mladen ; Nordström, Jakob LU and Vinyals, Marc
- publishing date
- 2014-03-01
- type
- Chapter in Book/Report/Conference proceeding
- publication status
- published
- subject
- keywords
- PCR, Polynomial calculus, Proof complexity, Resolution, Space, Width
- host publication
- 31st International Symposium on Theoretical Aspects of Computer Science, STACS 2014
- series title
- Leibniz International Proceedings in Informatics, LIPIcs
- editor
- Portier, Natacha and Mayr, Ernst W.
- volume
- 25
- pages
- 12 pages
- publisher
- Schloss Dagstuhl - Leibniz-Zentrum für Informatik
- conference name
- 31st International Symposium on Theoretical Aspects of Computer Science, STACS 2014
- conference location
- Lyon, France
- conference dates
- 2014-03-05 - 2014-03-08
- external identifiers
-
- scopus:84907818998
- ISSN
- 1868-8969
- ISBN
- 9783939897651
- DOI
- 10.4230/LIPIcs.STACS.2014.300
- language
- English
- LU publication?
- no
- id
- 03ffae44-7f85-4cee-9e57-e8d3400140cc
- date added to LUP
- 2020-12-18 22:24:57
- date last changed
- 2025-04-04 13:56:30
@inproceedings{03ffae44-7f85-4cee-9e57-e8d3400140cc,
abstract = {{<p>In 2003, Atserias and Dalmau resolved a major open question about the resolution proof system by establishing that the space complexity of formulas is always an upper bound on the width needed to refute them. Their proof is beautiful but somewhat mysterious in that it relies heavily on tools from finite model theory. We give an alternative, completely elementary, proof that works by simple syntactic manipulations of resolution refutations. As a by-product, we develop a "black-box" technique for proving space lower bounds via a "static" complexity measure that works against any resolution refutation-previous techniques have been inherently adaptive. We conclude by showing that the related question for polynomial calculus (i.e., whether space is an upper bound on degree) seems unlikely to be resolvable by similar methods.</p>}},
author = {{Filmus, Yuval and Lauria, Massimo and Mikša, Mladen and Nordström, Jakob and Vinyals, Marc}},
booktitle = {{31st International Symposium on Theoretical Aspects of Computer Science, STACS 2014}},
editor = {{Portier, Natacha and Mayr, Ernst W.}},
isbn = {{9783939897651}},
issn = {{1868-8969}},
keywords = {{PCR; Polynomial calculus; Proof complexity; Resolution; Space; Width}},
language = {{eng}},
month = {{03}},
pages = {{300--311}},
publisher = {{Schloss Dagstuhl - Leibniz-Zentrum für Informatik}},
series = {{Leibniz International Proceedings in Informatics, LIPIcs}},
title = {{From small space to small width in resolution}},
url = {{http://dx.doi.org/10.4230/LIPIcs.STACS.2014.300}},
doi = {{10.4230/LIPIcs.STACS.2014.300}},
volume = {{25}},
year = {{2014}},
}