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

TL;DR

This paper demonstrates that for certain 4-CNF formulas, the size of sums-of-squares proofs grows exponentially with the degree, establishing the optimality of current SDP-based proof search methods.

Contribution

It introduces a method to convert SOS degree lower bounds into size lower bounds, extending previous techniques to various proof systems.

Findings

SOS proofs of degree d can require size n^{Ω(d)}

The Lasserre SDP relaxation time is optimal up to constants

Provides a generic method to amplify SOS degree lower bounds to size lower bounds

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^{\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 $\mathsf{NP}$-reductions expressible as low-degree SOS derivations with the idea of relativizing CNF formulas in [Kraj\'i\v{c}ek '04] and [Dantchev and Riis'03], and then applying a restriction argument as in [Atserias, M\"uller, and Oliva '13] and [Atserias, Lauria, and Nordstr\"om '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.