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^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.
Proof complexity
resolution
Lasserre
Positivstellensatz
sums-of-squares
SOS
semidefinite programming
size
degree
rank
clique
lower bound
448-466
Regular Paper
Massimo
Lauria
Massimo Lauria
Jakob
Nordström
Jakob Nordström
10.4230/LIPIcs.CCC.2015.448
Albert Atserias, Massimo Lauria, and Jakob Nordström. Narrow proofs may be maximally long. Technical Report TR14-118, Electronic Colloquium on Computational Complexity (ECCC), September 2014. Preliminary version appeared in CCC'14.
Albert Atserias, Moritz Müller, and Sergi Oliva. Lower bounds for DNF-refutations of a relativized weak pigeonhole principle. In Proceedings of the 28th Annual IEEE Conference on Computational Complexity (CCC'13), pages 109-120, June 2013.
Boaz Barak, Fernando G. S. L. Brandão, Aram Wettroth Harrow, Jonathan A. Kelner, David Steurer, and Yuan Zhou. Hypercontractivity, sum-of-squares proofs, and their applications. In Proceedings of the 44th Annual ACM Symposium on Theory of Computing (STOC'12), pages 307-326, May 2012.
Boaz Barak and David Steurer. Sum-of-squares proofs and the quest toward optimal algorithms. Technical Report TR14-059, Electronic Colloquium on Computational Complexity (ECCC), April 2014.
Paul Beame, Russell Impagliazzo, Jan Krajíček, Toniann Pitassi, and Pavel Pudlák. Lower bounds on Hilbert’s Nullstellensatz and propositional proofs. In Proceedings of the 35th Annual IEEE Symposium on Foundations of Computer Science (FOCS'94), pages 794-806, November 1994.
Paul Beame, Toniann Pitassi, and Nathan Segerlind. Lower bounds for Lovász-Schrijver systems and beyond follow from multiparty communication complexity. SIAM Journal on Computing, 37(3):845-869, 2007. Preliminary version appeared in ICALP'05.
Olaf Beyersdorff, Nicola Galesi, and Massimo Lauria. Parameterized complexity of DPLL search procedures. ACM Transactions on Computational Logic, 14(3):20:1-20:21, August 2013. Preliminary version appeared in SAT'11.
Olaf Beyersdorff, Nicola Galesi, Massimo Lauria, and Alexander A. Razborov. Parameterized bounded-depth Frege is not optimal. ACM Transactions on Computation Theory, 4:7:1-7:16, September 2012. Preliminary version appeared in ICALP'11.
Stefan Dantchev. Relativisation provides natural separations for resolution-based proof systems. In Proceedings of the 1st International Computer Science Symposium in Russia (CSR'06), volume 3967 of Lecture Notes in Computer Science, pages 147-158. Springer, June 2006.
Stefan Dantchev and Barnaby Martin. Relativization makes contradictions harder for resolution. Annals of Pure and Applied Logic, 165(3):837-857, March 2014.
Stefan Dantchev and Søren Riis. On relativisation and complexity gap for resolution-based proof systems. In Proceedings of the 17th International Workshop on Computer Science Logic (CSL'03), volume 2803 of Lecture Notes in Computer Science, pages 142-154. Springer, August 2003.
Dima Grigoriev. Complexity of Positivstellensatz proofs for the knapsack. Computational Complexity, 10(2):139-154, December 2001.
Dima Grigoriev. Linear lower bound on degrees of Positivstellensatz calculus proofs for the parity. Theoretical Computer Science, 259(1-2):613-622, May 2001.
Dima Grigoriev, Edward A. Hirsch, and Dmitrii V. Pasechnik. Exponential lower bound for static semi-algebraic proofs. In Proceedings of the 29th International Colloquium on Automata, Languages and Programming (ICALP'02), volume 2380 of Lecture Notes in Computer Science, pages 257-268. Springer, July 2002.
Dima Grigoriev and Nicolai Vorobjov. Complexity of Null- and Positivstellensatz proofs. Annals of Pure and Applied Logic, 113(1-3):153-160, December 2001.
Mika Göös and Toniann Pitassi. Communication lower bounds via critical block sensitivity. In Proceedings of the 46th Annual ACM Symposium on Theory of Computing (STOC'14), pages 847-856, May 2014.
Subhash Khot. On the power of unique 2-prover 1-round games. In Proceedings of the 34th Annual ACM Symposium on Theory of Computing (STOC'02), pages 767-775, May 2002.
Arist Kojevnikov and Dmitry Itsykson. Lower bounds of static Lovász-Schrijver calculus proofs for Tseitin tautologies. In Proceedings of the 33rd International Colloquium on Automata, Languages and Programming (ICALP'06), volume 4051 of Lecture Notes in Computer Science, pages 323-334. Springer, July 2006.
Jan Krajíček. Combinatorics of first order structures and propositional proof systems. Archive for Mathematical Logic, 43(4):427-441, May 2004.
Jean-Louis Krivine. Anneaux préordonnés. Journal d’Analyse Mathématique, 12(1):307-326, 1964.
Jean B. Lasserre. An explicit exact SDP relaxation for nonlinear 0-1 programs. In Proceedings of the 8th International Conference on Integer Programming and Combinatorial Optimization (IPCO'01), volume 2081 of Lecture Notes in Computer Science, pages 293-303. Springer, June 2001.
Massimo Lauria and Jakob Nordström. Tight size-degree bounds for sums-of-squares proofs. Technical Report TR15-053, Electronic Colloquium on Computational Complexity (ECCC), April 2015.
Massimo Lauria, Pavel Pudlák, Vojtěch Rödl, and Neil Thapen. The complexity of proving that a graph is Ramsey. In Proceedings of the 40th International Colloquium on Automata, Languages and Programming (ICALP'13), volume 7965 of Lecture Notes in Computer Science, pages 684-695. Springer, July 2013.
James R. Lee, Prasad Raghavendra, David Steurer, and Ning Tan. On the power of symmetric LP and SDP relaxations. In Proceedings of the 29th Annual IEEE Conference on Computational Complexity (CCC'14), pages 13-21, June 2014.
Yurii Nesterov. Squared functional systems and optimization problems. In H. Frenk, K. Roos, T. Terlaky, and S. Zhang, editors, High Performance Optimization, pages 405-440. Kluwer Academic Publisher, 2000.
Ryan O'Donnell and Yuan Zhou. Approximability and proof complexity. In Proceedings of the 24th Annual ACM-SIAM Symposium on Discrete Algorithms (SODA'13), pages 1537-1556, January 2013.
Pablo A. Parrilo. Structured Semidefinite Programs and Semialgebraic Geometry Methods in Robustness and Optimization. PhD thesis, California Institute of Technology, May 2000. Available at URL: http://resolver.caltech.edu/CaltechETD:etd-05062004-055516.
http://resolver.caltech.edu/CaltechETD:etd-05062004-055516
Toniann Pitassi and Nathan Segerlind. Exponential lower bounds and integrality gaps for tree-like Lovász-Schrijver procedures. SIAM Journal on Computing, 41(1):128-159, 2012. Preliminary version appeared in SODA'09.
Grant Schoenebeck. Linear level Lasserre lower bounds for certain k-CSPs. In Proceedings of the 49th Annual IEEE Symposium on Foundations of Computer Science (FOCS'08), pages 593-602, October 2008.
N. Z. Shor. An approach to obtaining global extremums in polynomial mathematical programming problems. Cybernetics, 23(5):695-700, 1987. Translated from Kibernetika, No. 5, pages 102-–106, 1987.
Gilbert Stengle. A Nullstellensatz and a Positivstellensatz in semialgebraic geometry. Mathematische Annalen, 207(2):87-97, 1973.
Madhur Tulsiani. CSP gaps and reductions in the Lasserre hierarchy. In Proceedings of the 41st Annual ACM Symposium on Theory of Computing (STOC'09), pages 303-312, June 2009.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode