From small space to small width in resolution

Publikation: Bidrag til tidsskrift › Tidsskriftartikel › Forskning › fagfællebedømt

Standard

From small space to small width in resolution. / Filmus, Yuval; Lauria, Massimo; Mikša, Mladen; Nordström, Jakob; Vinyals, Marc.

I: ACM Transactions on Computational Logic, Bind 16, Nr. 4, 28, 01.08.2015.

Publikation: Bidrag til tidsskrift › Tidsskriftartikel › Forskning › fagfællebedømt

Harvard

Filmus, Y, Lauria, M, Mikša, M, Nordström, J & Vinyals, M 2015, 'From small space to small width in resolution', ACM Transactions on Computational Logic, bind 16, nr. 4, 28. https://doi.org/10.1145/2746339

APA

Filmus, Y., Lauria, M., Mikša, M., Nordström, J., & Vinyals, M. (2015). From small space to small width in resolution. ACM Transactions on Computational Logic, 16(4), [28]. https://doi.org/10.1145/2746339

Vancouver

Filmus Y, Lauria M, Mikša M, Nordström J, Vinyals M. From small space to small width in resolution. ACM Transactions on Computational Logic. 2015 aug. 1;16(4). 28. https://doi.org/10.1145/2746339

Author

Filmus, Yuval ; Lauria, Massimo ; Mikša, Mladen ; Nordström, Jakob ; Vinyals, Marc. / From small space to small width in resolution. I: ACM Transactions on Computational Logic. 2015 ; Bind 16, Nr. 4.

Bibtex

@article{cf3a6f5118a64fa48ab2f3e086deb03e,
title = "From small space to small width in resolution",
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{\"i}ss{\'e} 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.",
keywords = "degree, PCR, Polynomial calculus, Polynomial calculus resolution, Proof complexity, Resolution, Space, Width",
author = "Yuval Filmus and Massimo Lauria and Mladen Mik{\v s}a and Jakob Nordstr{\"o}m and Marc Vinyals",
year = "2015",
month = aug,
day = "1",
doi = "10.1145/2746339",
language = "English",
volume = "16",
journal = "ACM Transactions on Computational Logic",
issn = "1529-3785",
publisher = "Association for Computing Machinery, Inc.",
number = "4",

}

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