Lauria, Massimo ;
Nordström, Jakob
Tight SizeDegree Bounds for SumsofSquares Proofs
Abstract
We exhibit families of 4CNF formulas over n variables that have sumsofsquares (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 degreed SOS proofs is optimal up to constant factors in the exponent. We establish this result by combining NPreductions expressible as lowdegree 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 SheraliAdams from lower bounds on width, degree, and rank, respectively.
BibTeX  Entry
@InProceedings{lauria_et_al:LIPIcs:2015:5073,
author = {Massimo Lauria and Jakob Nordstr{\"o}m},
title = {{Tight SizeDegree Bounds for SumsofSquares Proofs}},
booktitle = {30th Conference on Computational Complexity (CCC 2015)},
pages = {448466},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783939897811},
ISSN = {18688969},
year = {2015},
volume = {33},
editor = {David Zuckerman},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2015/5073},
URN = {urn:nbn:de:0030drops50736},
doi = {10.4230/LIPIcs.CCC.2015.448},
annote = {Keywords: Proof complexity, resolution, Lasserre, Positivstellensatz, sumsofsquares, SOS, semidefinite programming, size, degree, rank, clique, lower bound}
}
2015
Keywords: 

Proof complexity, resolution, Lasserre, Positivstellensatz, sumsofsquares, SOS, semidefinite programming, size, degree, rank, clique, lower bound 
Seminar: 

30th Conference on Computational Complexity (CCC 2015)

Issue date: 

2015 
Date of publication: 

2015 