Narrow proofs may be maximally long
Document typeConference report
PublisherInstitute of Electrical and Electronics Engineers (IEEE)
Rights accessOpen Access
European Commission's projectUTHOTP - Understanding the Hardness of Theorem Proving (EC-FP7-279611)
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.
CitationAtserias, A.; Lauria, M.; Nordström, J. Narrow proofs may be maximally long. A: IEEE Conference on Computational Complexity. "IEEE 29th Conference on Computational Complexity: 11-13 June 2014, Vancouver, British Columbia, Canada: proceedings". Vancouver: Institute of Electrical and Electronics Engineers (IEEE), 2014, p. 286-297.