From small space to small width in resolution
(2015) In ACM Transactions on Computational Logic 16(4).- Abstract
In 2003, Atserias and Dalmau resolved a major open question about the resolution proof system by establishing that the space complexity of a Conjunctive Normal Form (CNF) formula is always an upper bound on the width needed to refute the formula. Their proof is beautiful but uses a nonconstructive argument based on Ehrenfeucht-Fraïssé games. We give an alternative, more explicit, 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" complexitymeasure that works against any resolution refutation-previous techniques have been inherently adaptive. We conclude by showing that the related question for polynomial calculus... (More)
In 2003, Atserias and Dalmau resolved a major open question about the resolution proof system by establishing that the space complexity of a Conjunctive Normal Form (CNF) formula is always an upper bound on the width needed to refute the formula. Their proof is beautiful but uses a nonconstructive argument based on Ehrenfeucht-Fraïssé games. We give an alternative, more explicit, 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" complexitymeasure 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 similarmethods.
(Less)
- author
- Filmus, Yuval ; Lauria, Massimo ; Mikša, Mladen ; Nordström, Jakob LU and Vinyals, Marc
- publishing date
- 2015-08-01
- type
- Contribution to journal
- publication status
- published
- subject
- keywords
- degree, PCR, Polynomial calculus, Polynomial calculus resolution, Proof complexity, Resolution, Space, Width
- in
- ACM Transactions on Computational Logic
- volume
- 16
- issue
- 4
- article number
- 28
- publisher
- Association for Computing Machinery (ACM)
- external identifiers
-
- scopus:84941557324
- ISSN
- 1529-3785
- DOI
- 10.1145/2746339
- language
- English
- LU publication?
- no
- id
- 624417e8-2740-4903-9bb4-a5f7f678633d
- date added to LUP
- 2020-12-18 22:23:39
- date last changed
- 2022-02-01 18:41:08
@article{624417e8-2740-4903-9bb4-a5f7f678633d,
abstract = {{<p>In 2003, Atserias and Dalmau resolved a major open question about the resolution proof system by establishing that the space complexity of a Conjunctive Normal Form (CNF) formula is always an upper bound on the width needed to refute the formula. Their proof is beautiful but uses a nonconstructive argument based on Ehrenfeucht-Fraïssé games. We give an alternative, more explicit, 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" complexitymeasure 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 similarmethods.</p>}},
author = {{Filmus, Yuval and Lauria, Massimo and Mikša, Mladen and Nordström, Jakob and Vinyals, Marc}},
issn = {{1529-3785}},
keywords = {{degree; PCR; Polynomial calculus; Polynomial calculus resolution; Proof complexity; Resolution; Space; Width}},
language = {{eng}},
month = {{08}},
number = {{4}},
publisher = {{Association for Computing Machinery (ACM)}},
series = {{ACM Transactions on Computational Logic}},
title = {{From small space to small width in resolution}},
url = {{http://dx.doi.org/10.1145/2746339}},
doi = {{10.1145/2746339}},
volume = {{16}},
year = {{2015}},
}