eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2015-06-06
448
466
10.4230/LIPIcs.CCC.2015.448
article
Tight Size-Degree Bounds for Sums-of-Squares Proofs
Lauria, Massimo
Nordström, Jakob
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^Omega(d) for values of d = d(n) from constant all the way up to n^delta for some universal constant delta. This shows that the n^O(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 [Krajicek '04] and [Dantchev and Riis '03], and then applying a restriction argument as in [Atserias, Müller, and Oliva '13] and [Atserias, Lauria, and Nordstrom '14]. This yields a generic method of amplifying SOS degree lower bounds to size lower bounds, and also generalizes the approach in [ALN14] to obtain size lower bounds for the proof systems resolution, polynomial calculus, and Sherali-Adams from lower bounds on width, degree, and rank, respectively.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol033-ccc2015/LIPIcs.CCC.2015.448/LIPIcs.CCC.2015.448.pdf
Proof complexity
resolution
Lasserre
Positivstellensatz
sums-of-squares
SOS
semidefinite programming
size
degree
rank
clique
lower bound