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

Research output: Contribution to journal › Journal article › Research › peer-review

Standard

Tight Size-Degree Bounds for Sums-of-Squares Proofs. / Lauria, Massimo; Nordström, Jakob.

In: Computational Complexity, Vol. 26, No. 4, 01.12.2017, p. 911-948.

Research output: Contribution to journal › Journal article › Research › peer-review

Harvard

Lauria, M & Nordström, J 2017, 'Tight Size-Degree Bounds for Sums-of-Squares Proofs', Computational Complexity, vol. 26, no. 4, pp. 911-948. https://doi.org/10.1007/s00037-017-0152-4

APA

Lauria, M., & Nordström, J. (2017). Tight Size-Degree Bounds for Sums-of-Squares Proofs. Computational Complexity, 26(4), 911-948. https://doi.org/10.1007/s00037-017-0152-4

Vancouver

Lauria M, Nordström J. Tight Size-Degree Bounds for Sums-of-Squares Proofs. Computational Complexity. 2017 Dec 1;26(4):911-948. https://doi.org/10.1007/s00037-017-0152-4

Author

Lauria, Massimo ; Nordström, Jakob. / Tight Size-Degree Bounds for Sums-of-Squares Proofs. In: Computational Complexity. 2017 ; Vol. 26, No. 4. pp. 911-948.

Bibtex

@article{879c6689dab641308e32a8154acb3b70,
title = "Tight Size-Degree Bounds for Sums-of-Squares Proofs",
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 Kraj{\'i}{\v c}ek (Arch Math Log 43(4):427–441, 2004) and Dantchev & Riis (Proceedings of the 17th international workshop on computer science logic (CSL {\textquoteright}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.",
keywords = "clique, degree, Lasserre, lower bound, Positivstellensatz, Proof complexity, rank, resolution, semidefinite programming, size, SOS, sums-of-squares",
author = "Massimo Lauria and Jakob Nordstr{\"o}m",
year = "2017",
month = dec,
day = "1",
doi = "10.1007/s00037-017-0152-4",
language = "English",
volume = "26",
pages = "911--948",
journal = "Computational Complexity",
issn = "1016-3328",
publisher = "Birkhauser Verlag Basel",
number = "4",

}

RIS

TY - JOUR

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

AU - Lauria, Massimo

AU - Nordström, Jakob

PY - 2017/12/1

Y1 - 2017/12/1

N2 - 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.

AB - 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.

KW - clique

KW - degree

KW - Lasserre

KW - lower bound

KW - Positivstellensatz

KW - Proof complexity

KW - rank

KW - resolution

KW - semidefinite programming

KW - size

KW - SOS

KW - sums-of-squares

UR - http://www.scopus.com/inward/record.url?scp=85018513275&partnerID=8YFLogxK

U2 - 10.1007/s00037-017-0152-4

DO - 10.1007/s00037-017-0152-4

M3 - Journal article

AN - SCOPUS:85018513275

VL - 26

SP - 911

EP - 948

JO - Computational Complexity

JF - Computational Complexity

SN - 1016-3328

IS - 4

ER -

ID: 251868223