Sökning: onr:"swepub:oai:DiVA.org:kth-168868" >
Narrow proofs may b...
Narrow proofs may be maximally long
-
Atserias, A. (författare)
-
- Lauria, Massimo (författare)
- KTH,Teoretisk datalogi, TCS
-
- Nordström, Jakob (författare)
- KTH,Teoretisk datalogi, TCS
-
(creator_code:org_t)
- 2014
- 2014
- Engelska.
-
Ingår i: Proceedings of the Annual IEEE Conference on Computational Complexity. - 9781479936267 ; , s. 286-297
- Relaterad länk:
-
https://urn.kb.se/re...
-
visa fler...
-
https://doi.org/10.1...
-
visa färre...
Abstract
Ämnesord
Stäng
- 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.
Ämnesord
- NATURVETENSKAP -- Data- och informationsvetenskap (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences (hsv//eng)
Nyckelord
- degree
- Lasserre
- length
- PCR
- polynomial calculus
- proof complexity
- rank
- resolution
- Sherali-Adams
- size
- width
- Calculations
- Computational complexity
- Optical resolving power
- Polynomials
Publikations- och innehållstyp
- ref (ämneskategori)
- kon (ämneskategori)
Hitta via bibliotek
Till lärosätets databas