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
APA
Vancouver
Author
Bibtex
}
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