Skip to main content

Lund University Publications

LUND UNIVERSITY LIBRARIES

Tight Size-Degree Bounds for Sums-of-Squares Proofs

Lauria, Massimo and Nordström, Jakob LU (2017) In Computational Complexity 26(4). p.911-948
Abstract

We exhibit families of 4-CNF formulas over n variables that have sums-of-squares (SOS) proofs of unsatisfiability of degree (a.k.a. rank) d but require SOS proofs of size nΩ ( d ) for values of d = d(n) from constant all the way up to nδ for some universal constant δ. This shows that the nO ( d ) running time obtained by using the Lasserre semidefinite programming relaxations to find degree-d SOS proofs is optimal up to constant factors in the exponent. We establish this result by combining NP-reductions expressible as low-degree SOS derivations with the idea of relativizing CNF formulas in... (More)

We exhibit families of 4-CNF formulas over n variables that have sums-of-squares (SOS) proofs of unsatisfiability of degree (a.k.a. rank) d but require SOS proofs of size nΩ ( d ) for values of d = d(n) from constant all the way up to nδ for some universal constant δ. This shows that the nO ( d ) running time obtained by using the Lasserre semidefinite programming relaxations to find degree-d SOS proofs is optimal up to constant factors in the exponent. We establish this result by combining NP-reductions expressible as low-degree SOS derivations with the idea of relativizing CNF formulas in Krajíček (Arch Math Log 43(4):427–441, 2004) and Dantchev & Riis (Proceedings of the 17th international workshop on computer science logic (CSL ’03), 2003) and then applying a restriction argument as in Atserias et al. (J Symb Log 80(2):450–476, 2015; ACM Trans Comput Log 17:19:1–19:30, 2016). This yields a generic method of amplifying SOS degree lower bounds to size lower bounds and also generalizes the approach used in Atserias et al. (2016) to obtain size lower bounds for the proof systems resolution, polynomial calculus, and Sherali–Adams from lower bounds on width, degree, and rank, respectively.

(Less)
Please use this url to cite or link to this publication:
author
and
publishing date
type
Contribution to journal
publication status
published
subject
keywords
clique, degree, Lasserre, lower bound, Positivstellensatz, Proof complexity, rank, resolution, semidefinite programming, size, SOS, sums-of-squares
in
Computational Complexity
volume
26
issue
4
pages
38 pages
publisher
Birkhäuser Verlag
external identifiers
  • scopus:85018513275
ISSN
1016-3328
DOI
10.1007/s00037-017-0152-4
language
English
LU publication?
no
id
ee60c4be-4cd0-45db-99ca-474b92f28010
date added to LUP
2020-12-18 22:20:44
date last changed
2022-03-03 20:26:41
@article{ee60c4be-4cd0-45db-99ca-474b92f28010,
  abstract     = {{<p>We exhibit families of 4-CNF formulas over n variables that have sums-of-squares (SOS) proofs of unsatisfiability of degree (a.k.a. rank) d but require SOS proofs of size n<sup>Ω</sup>         <sup>(</sup>         <sup>d</sup>         <sup>)</sup> for values of d = d(n) from constant all the way up to n<sup>δ</sup> for some universal constant δ. This shows that the n<sup>O</sup>         <sup>(</sup>         <sup>d</sup>         <sup>)</sup> running time obtained by using the Lasserre semidefinite programming relaxations to find degree-d SOS proofs is optimal up to constant factors in the exponent. We establish this result by combining NP-reductions expressible as low-degree SOS derivations with the idea of relativizing CNF formulas in Krajíček (Arch Math Log 43(4):427–441, 2004) and Dantchev &amp; Riis (Proceedings of the 17th international workshop on computer science logic (CSL ’03), 2003) and then applying a restriction argument as in Atserias et al. (J Symb Log 80(2):450–476, 2015; ACM Trans Comput Log 17:19:1–19:30, 2016). This yields a generic method of amplifying SOS degree lower bounds to size lower bounds and also generalizes the approach used in Atserias et al. (2016) to obtain size lower bounds for the proof systems resolution, polynomial calculus, and Sherali–Adams from lower bounds on width, degree, and rank, respectively.</p>}},
  author       = {{Lauria, Massimo and Nordström, Jakob}},
  issn         = {{1016-3328}},
  keywords     = {{clique; degree; Lasserre; lower bound; Positivstellensatz; Proof complexity; rank; resolution; semidefinite programming; size; SOS; sums-of-squares}},
  language     = {{eng}},
  month        = {{12}},
  number       = {{4}},
  pages        = {{911--948}},
  publisher    = {{Birkhäuser Verlag}},
  series       = {{Computational Complexity}},
  title        = {{Tight Size-Degree Bounds for Sums-of-Squares Proofs}},
  url          = {{http://dx.doi.org/10.1007/s00037-017-0152-4}},
  doi          = {{10.1007/s00037-017-0152-4}},
  volume       = {{26}},
  year         = {{2017}},
}