Abstract
We exhibit families of -CNF formulas over variables that have sums-of-squares (SOS) proofs of unsatisfiability of degree (a.k.a. rank) but require SOS proofs of size for values of from constant all the way up to for some universal constant. This shows that the running time obtained by using the Lasserre semidefinite programming relaxations to find degree- SOS proofs is optimal up to constant factors in the exponent. We establish this result by combining -reductions expressible as low-degree SOS derivations with the idea of relativizing CNF formulas in [Krajíček '04] and [Dantchev and Riis'03], and then applying a restriction argument as in [Atserias, Müller, and Oliva '13] and [Atserias, Lauria, and Nordström '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.
Connections
Explore this paper’s authors, topics and related work.
Building this map preview
BZPEER is loading the nearby papers, people, topics and institutions for this page.
Reviews 0
Write a review
No reviews yet.
Discussion 0
Add a comment
No comments yet.