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

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