Carregant...
Carregant...

Vés al contingut (premeu Retorn)

Narrow proofs may be maximally long

Autor
Atserias, A.; Lauria, M.; Nordström, J.
Tipus d'activitat
Article en revista
Revista
ACM transactions on computational logic
Data de publicació
2016-07-03
Volum
17
Número
3
Pàgina inicial
19:1
Pàgina final
19:30
DOI
https://doi.org/10.1145/2898435 Obrir en finestra nova
Projecte finançador
Teoría y aplicaciones en satisfactibilidad y optimización de restricciones
Repositori
http://hdl.handle.net/2117/99737 Obrir en finestra nova
URL
http://dl.acm.org/citation.cfm?doid=2894199.2898435 Obrir en finestra nova
Resum
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(Omega(w)). This shows that the simple counting argument that any formula refutable in width w must have a proof in size n(O(w)) is essentially tight. Moreover, our lower bound generalizes to polynomial calculus resolution and Sherali-Adams, implying that the corresponding size upper bounds in terms of degree and rank are tight as well. The lower bound does ...
Citació
Atserias, A., Lauria, M., Nordström, J. Narrow proofs may be maximally long. "ACM transactions on computational logic", 3 Juliol 2016, vol. 17, núm. 3, p. 19:1-19:30.
Paraules clau
Proof Complexity, Resolution, Width, Polynomial Calculus, Polynomial Calculus Resolution, Pcr, Sherali-adams, Sar, Degree
Grup de recerca
ALBCOM - Algorismia, Bioinformàtica, Complexitat i Mètodes Formals

Participants

Arxius