Narrow proofs may be maximally long

Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › fagfællebedømt

Standard

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

Proceedings - IEEE 29th Conference on Computational Complexity, CCC 2014. IEEE Computer Society Press, 2014. s. 286-297 6875497 (Proceedings of the Annual IEEE Conference on Computational Complexity).

Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › fagfællebedømt

Harvard

Atserias, A, Lauria, M & Nordström, J 2014, Narrow proofs may be maximally long. i Proceedings - IEEE 29th Conference on Computational Complexity, CCC 2014., 6875497, IEEE Computer Society Press, Proceedings of the Annual IEEE Conference on Computational Complexity, s. 286-297, 29th Annual IEEE Conference on Computational Complexity, CCC 2014, Vancouver, BC, Canada, 11/06/2014. https://doi.org/10.1109/CCC.2014.36

APA

Atserias, A., Lauria, M., & Nordström, J. (2014). Narrow proofs may be maximally long. I Proceedings - IEEE 29th Conference on Computational Complexity, CCC 2014 (s. 286-297). [6875497] IEEE Computer Society Press. Proceedings of the Annual IEEE Conference on Computational Complexity https://doi.org/10.1109/CCC.2014.36

Vancouver

Atserias A, Lauria M, Nordström J. Narrow proofs may be maximally long. I Proceedings - IEEE 29th Conference on Computational Complexity, CCC 2014. IEEE Computer Society Press. 2014. s. 286-297. 6875497. (Proceedings of the Annual IEEE Conference on Computational Complexity). https://doi.org/10.1109/CCC.2014.36

Author

Atserias, Albert ; Lauria, Massimo ; Nordström, Jakob. / Narrow proofs may be maximally long. Proceedings - IEEE 29th Conference on Computational Complexity, CCC 2014. IEEE Computer Society Press, 2014. s. 286-297 (Proceedings of the Annual IEEE Conference on Computational Complexity).

Bibtex

@inproceedings{f9a0b535d0d243d8b2716c6dca2cca09,
title = "Narrow proofs may be maximally long",
abstract = "We prove that there are 3-CNF 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(ω) is essentially tight. Moreover, our lower bounds can be generalized to polynomial calculus resolution (PCR) and Sherali-Adams, implying that the corresponding size upper bounds in terms of degree and rank are tight as well. Our results do not extend all the way to Lasserre, however-the formulas we study have Lasserre proofs of constant rank and size polynomial in both n and w.",
keywords = "degree, Lasserre, length, PCR, polynomial calculus, proof complexity, rank, resolution, Sherali-Adams, size, width",
author = "Albert Atserias and Massimo Lauria and Jakob Nordstr{\"o}m",
year = "2014",
doi = "10.1109/CCC.2014.36",
language = "English",
isbn = "9781479936267",
series = "Proceedings of the Annual IEEE Conference on Computational Complexity",
publisher = "IEEE Computer Society Press",
pages = "286--297",
booktitle = "Proceedings - IEEE 29th Conference on Computational Complexity, CCC 2014",
address = "United States",
note = "29th Annual IEEE Conference on Computational Complexity, CCC 2014 ; Conference date: 11-06-2014 Through 13-06-2014",

}

RIS

TY - GEN

T1 - Narrow proofs may be maximally long

AU - Atserias, Albert

AU - Lauria, Massimo

AU - Nordström, Jakob

PY - 2014

Y1 - 2014

N2 - We prove that there are 3-CNF 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(ω) is essentially tight. Moreover, our lower bounds can be generalized to polynomial calculus resolution (PCR) and Sherali-Adams, implying that the corresponding size upper bounds in terms of degree and rank are tight as well. Our results do not extend all the way to Lasserre, however-the formulas we study have Lasserre proofs of constant rank and size polynomial in both n and w.

AB - We prove that there are 3-CNF 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(ω) is essentially tight. Moreover, our lower bounds can be generalized to polynomial calculus resolution (PCR) and Sherali-Adams, implying that the corresponding size upper bounds in terms of degree and rank are tight as well. Our results do not extend all the way to Lasserre, however-the formulas we study have Lasserre proofs of constant rank and size polynomial in both n and w.

KW - degree

KW - Lasserre

KW - length

KW - PCR

KW - polynomial calculus

KW - proof complexity

KW - rank

KW - resolution

KW - Sherali-Adams

KW - size

KW - width

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

U2 - 10.1109/CCC.2014.36

DO - 10.1109/CCC.2014.36

M3 - Article in proceedings

AN - SCOPUS:84906667234

SN - 9781479936267

T3 - Proceedings of the Annual IEEE Conference on Computational Complexity

SP - 286

EP - 297

BT - Proceedings - IEEE 29th Conference on Computational Complexity, CCC 2014

PB - IEEE Computer Society Press

T2 - 29th Annual IEEE Conference on Computational Complexity, CCC 2014

Y2 - 11 June 2014 through 13 June 2014

ER -

ID: 251870042