Narrow proofs may be maximally long

Research output: Contribution to journal › Journal article › Research › peer-review

Standard

Narrow proofs may be maximally long. / Atserias, Albert; Lauria, Massimo; Nordström, Jakob.

In: ACM Transactions on Computational Logic, Vol. 17, No. 3, 19, 02.2016.

Research output: Contribution to journal › Journal article › Research › peer-review

Harvard

Atserias, A, Lauria, M & Nordström, J 2016, 'Narrow proofs may be maximally long', ACM Transactions on Computational Logic, vol. 17, no. 3, 19. https://doi.org/10.1145/2898435

APA

Atserias, A., Lauria, M., & Nordström, J. (2016). Narrow proofs may be maximally long. ACM Transactions on Computational Logic, 17(3), [19]. https://doi.org/10.1145/2898435

Vancouver

Atserias A, Lauria M, Nordström J. Narrow proofs may be maximally long. ACM Transactions on Computational Logic. 2016 Feb;17(3). 19. https://doi.org/10.1145/2898435

Author

Atserias, Albert ; Lauria, Massimo ; Nordström, Jakob. / Narrow proofs may be maximally long. In: ACM Transactions on Computational Logic. 2016 ; Vol. 17, No. 3.

Bibtex

@article{5bfe05c828e84d34a4ca8d1db7af2f03,
title = "Narrow proofs may be maximally long",
abstract = "We prove that there are 3-conjunctive normal form formulas over n variables that can be refuted in resolution in width w but require resolution proofs of size nΩ(w). This shows that the simple counting argument that any formula refutable in width w must have a proof in size nO(w) is essentially tight. Moreover, our lower bound generalizes to polynomial calculus resolution and Sherali-Adams, implying that the corresponding size upper bounds in terms of degree and rank are tight as well. The lower bound does not extend all the way to Lasserre, however, since we show that there the formulas we study have proofs of constant rank and size polynomial in both n and w.",
keywords = "Degree, PCR, Polynomial calculus, Polynomial calculus resolution, Proof complexity, Resolution, SAR, Sherali-Adams, Width",
author = "Albert Atserias and Massimo Lauria and Jakob Nordstr{\"o}m",
year = "2016",
month = feb,
doi = "10.1145/2898435",
language = "English",
volume = "17",
journal = "ACM Transactions on Computational Logic",
issn = "1529-3785",
publisher = "Association for Computing Machinery, Inc.",
number = "3",

}

RIS

TY - JOUR

T1 - Narrow proofs may be maximally long

AU - Atserias, Albert

AU - Lauria, Massimo

AU - Nordström, Jakob

PY - 2016/2

Y1 - 2016/2

N2 - We prove that there are 3-conjunctive normal form formulas over n variables that can be refuted in resolution in width w but require resolution proofs of size nΩ(w). This shows that the simple counting argument that any formula refutable in width w must have a proof in size nO(w) is essentially tight. Moreover, our lower bound generalizes to polynomial calculus resolution and Sherali-Adams, implying that the corresponding size upper bounds in terms of degree and rank are tight as well. The lower bound does not extend all the way to Lasserre, however, since we show that there the formulas we study have proofs of constant rank and size polynomial in both n and w.

AB - We prove that there are 3-conjunctive normal form formulas over n variables that can be refuted in resolution in width w but require resolution proofs of size nΩ(w). This shows that the simple counting argument that any formula refutable in width w must have a proof in size nO(w) is essentially tight. Moreover, our lower bound generalizes to polynomial calculus resolution and Sherali-Adams, implying that the corresponding size upper bounds in terms of degree and rank are tight as well. The lower bound does not extend all the way to Lasserre, however, since we show that there the formulas we study have proofs of constant rank and size polynomial in both n and w.

KW - Degree

KW - PCR

KW - Polynomial calculus

KW - Polynomial calculus resolution

KW - Proof complexity

KW - Resolution

KW - SAR

KW - Sherali-Adams

KW - Width

UR - http://www.scopus.com/inward/record.url?scp=84973879640&partnerID=8YFLogxK

U2 - 10.1145/2898435

DO - 10.1145/2898435

M3 - Journal article

AN - SCOPUS:84973879640

VL - 17

JO - ACM Transactions on Computational Logic

JF - ACM Transactions on Computational Logic

SN - 1529-3785

IS - 3

M1 - 19

ER -

ID: 251868677