Search: onr:"swepub:oai:DiVA.org:kth-168868" >
Narrow proofs may b...
Narrow proofs may be maximally long
-
Atserias, A. (author)
-
- Lauria, Massimo (author)
- KTH,Teoretisk datalogi, TCS
-
- Nordström, Jakob (author)
- KTH,Teoretisk datalogi, TCS
-
(creator_code:org_t)
- 2014
- 2014
- English.
-
In: Proceedings of the Annual IEEE Conference on Computational Complexity. - 9781479936267 ; , s. 286-297
- Related links:
-
https://urn.kb.se/re...
-
show more...
-
https://doi.org/10.1...
-
show less...
Abstract
Subject headings
Close
- 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.
Subject headings
- NATURVETENSKAP -- Data- och informationsvetenskap (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences (hsv//eng)
Keyword
- degree
- Lasserre
- length
- PCR
- polynomial calculus
- proof complexity
- rank
- resolution
- Sherali-Adams
- size
- width
- Calculations
- Computational complexity
- Optical resolving power
- Polynomials
Publication and Content Type
- ref (subject category)
- kon (subject category)
Find in a library
To the university's database