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