Show simple item record

dc.contributor.authorAtserias, Albert
dc.contributor.authorLauria, Massimo
dc.contributor.authorNordström, Jakob
dc.contributor.otherUniversitat Politècnica de Catalunya. Departament de Ciències de la Computació
dc.date.accessioned2014-10-17T11:02:37Z
dc.date.available2014-10-17T11:02:37Z
dc.date.created2014
dc.date.issued2014
dc.identifier.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.
dc.identifier.isbn978-1-4799-3626-7
dc.identifier.urihttp://hdl.handle.net/2117/24406
dc.description.abstractWe 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.
dc.format.extent12 p.
dc.language.isoeng
dc.publisherInstitute of Electrical and Electronics Engineers (IEEE)
dc.subjectÀrees temàtiques de la UPC::Informàtica::Informàtica teòrica
dc.subject.lcshComputational complexity
dc.subject.otherDegree
dc.subject.otherLasserre
dc.subject.otherLength
dc.subject.otherPCR
dc.subject.otherPolynomial calculus
dc.subject.otherProof complexity
dc.subject.otherRank
dc.subject.otherResolution
dc.subject.otherSherali-Adams
dc.subject.otherSize
dc.subject.otherWidth
dc.titleNarrow proofs may be maximally long
dc.typeConference report
dc.subject.lemacComplexitat computacional
dc.contributor.groupUniversitat Politècnica de Catalunya. ALBCOM - Algorismia, Bioinformàtica, Complexitat i Mètodes Formals
dc.identifier.doi10.1109/CCC.2014.36
dc.relation.publisherversionhttp://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=6875497
dc.rights.accessOpen Access
drac.iddocument15250698
dc.description.versionPostprint (author’s final draft)
dc.relation.projectidinfo:eu-repo/grantAgreement/EC/FP7/279611/EU/Understanding the Hardness of Theorem Proving/UTHOTP
upcommons.citation.authorAtserias, A.; Lauria, M.; Nordström, J.
upcommons.citation.contributorIEEE Conference on Computational Complexity
upcommons.citation.pubplaceVancouver
upcommons.citation.publishedtrue
upcommons.citation.publicationNameIEEE 29th Conference on Computational Complexity: 11-13 June 2014, Vancouver, British Columbia, Canada: proceedings
upcommons.citation.startingPage286
upcommons.citation.endingPage297


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record

All rights reserved. This work is protected by the corresponding intellectual and industrial property rights. Without prejudice to any existing legal exemptions, reproduction, distribution, public communication or transformation of this work are prohibited without permission of the copyright holder