From small space to small width in resolution
Research output: Contribution to journal › Journal article › Research › peer-review
Standard
From small space to small width in resolution. / Filmus, Yuval; Lauria, Massimo; Mikša, Mladen; Nordström, Jakob; Vinyals, Marc.
In: ACM Transactions on Computational Logic, Vol. 16, No. 4, 28, 01.08.2015.Research output: Contribution to journal › Journal article › Research › peer-review
Harvard
APA
Vancouver
Author
Bibtex
}
RIS
TY - JOUR
T1 - From small space to small width in resolution
AU - Filmus, Yuval
AU - Lauria, Massimo
AU - Mikša, Mladen
AU - Nordström, Jakob
AU - Vinyals, Marc
PY - 2015/8/1
Y1 - 2015/8/1
N2 - 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.
AB - 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.
KW - degree
KW - PCR
KW - Polynomial calculus
KW - Polynomial calculus resolution
KW - Proof complexity
KW - Resolution
KW - Space
KW - Width
UR - http://www.scopus.com/inward/record.url?scp=84941557324&partnerID=8YFLogxK
U2 - 10.1145/2746339
DO - 10.1145/2746339
M3 - Journal article
AN - SCOPUS:84941557324
VL - 16
JO - ACM Transactions on Computational Logic
JF - ACM Transactions on Computational Logic
SN - 1529-3785
IS - 4
M1 - 28
ER -
ID: 251869364