Skip to main content

Lund University Publications

LUND UNIVERSITY LIBRARIES

Narrow proofs may be maximally long

Atserias, Albert ; Lauria, Massimo and Nordström, Jakob LU (2016) In ACM Transactions on Computational Logic 17(3).
Abstract

We prove that there are 3-conjunctive normal form 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(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 not extend all the way to Lasserre, however, since we show that there the formulas we study have proofs of constant rank and size polynomial in both n and w.

Please use this url to cite or link to this publication:
author
; and
publishing date
type
Contribution to journal
publication status
published
subject
keywords
Degree, PCR, Polynomial calculus, Polynomial calculus resolution, Proof complexity, Resolution, SAR, Sherali-Adams, Width
in
ACM Transactions on Computational Logic
volume
17
issue
3
article number
19
publisher
Association for Computing Machinery (ACM)
external identifiers
  • scopus:84973879640
ISSN
1529-3785
DOI
10.1145/2898435
language
English
LU publication?
no
id
0a98501a-f642-480e-a037-8bbb572faff0
date added to LUP
2020-12-18 22:22:20
date last changed
2022-04-11 06:37:03
@article{0a98501a-f642-480e-a037-8bbb572faff0,
  abstract     = {{<p>We prove that there are 3-conjunctive normal form formulas over n variables that can be refuted in resolution in width w but require resolution proofs of size n<sup>Ω(w)</sup>. This shows that the simple counting argument that any formula refutable in width w must have a proof in size n<sup>O(w)</sup> 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 not extend all the way to Lasserre, however, since we show that there the formulas we study have proofs of constant rank and size polynomial in both n and w.</p>}},
  author       = {{Atserias, Albert and Lauria, Massimo and Nordström, Jakob}},
  issn         = {{1529-3785}},
  keywords     = {{Degree; PCR; Polynomial calculus; Polynomial calculus resolution; Proof complexity; Resolution; SAR; Sherali-Adams; Width}},
  language     = {{eng}},
  number       = {{3}},
  publisher    = {{Association for Computing Machinery (ACM)}},
  series       = {{ACM Transactions on Computational Logic}},
  title        = {{Narrow proofs may be maximally long}},
  url          = {{http://dx.doi.org/10.1145/2898435}},
  doi          = {{10.1145/2898435}},
  volume       = {{17}},
  year         = {{2016}},
}