Document Open Access Logo

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

Authors Massimo Lauria, Jakob Nordström

PDF

File

Thumbnail PDF
PDF
LIPIcs.CCC.2015.448.pdf
  • Filesize: 481 kB
  • 19 pages

Document Identifiers

Subject Classification

Keywords
  • Proof complexity
  • resolution
  • Lasserre
  • Positivstellensatz
  • sums-of-squares
  • SOS
  • semidefinite programming
  • size
  • degree
  • rank
  • clique
  • lower bound

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

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

Cite As Get BibTex

Massimo Lauria and Jakob Nordström. Tight Size-Degree Bounds for Sums-of-Squares Proofs. In 30th Conference on Computational Complexity (CCC 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 33, pp. 448-466, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.CCC.2015.448

Author Details

Massimo Lauria
Jakob Nordström

References

  1. 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. Google Scholar
  2. 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. Google Scholar
  3. 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. Google Scholar
  4. 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. Google Scholar
  5. 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. Google Scholar
  6. 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. Google Scholar
  7. 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. Google Scholar
  8. 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. Google Scholar
  9. 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. Google Scholar
  10. Stefan Dantchev and Barnaby Martin. Relativization makes contradictions harder for resolution. Annals of Pure and Applied Logic, 165(3):837-857, March 2014. Google Scholar
  11. 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. Google Scholar
  12. Dima Grigoriev. Complexity of Positivstellensatz proofs for the knapsack. Computational Complexity, 10(2):139-154, December 2001. Google Scholar
  13. Dima Grigoriev. Linear lower bound on degrees of Positivstellensatz calculus proofs for the parity. Theoretical Computer Science, 259(1-2):613-622, May 2001. Google Scholar
  14. 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. Google Scholar
  15. Dima Grigoriev and Nicolai Vorobjov. Complexity of Null- and Positivstellensatz proofs. Annals of Pure and Applied Logic, 113(1-3):153-160, December 2001. Google Scholar
  16. 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. Google Scholar
  17. 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. Google Scholar
  18. 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. Google Scholar
  19. Jan Krajíček. Combinatorics of first order structures and propositional proof systems. Archive for Mathematical Logic, 43(4):427-441, May 2004. Google Scholar
  20. Jean-Louis Krivine. Anneaux préordonnés. Journal d’Analyse Mathématique, 12(1):307-326, 1964. Google Scholar
  21. 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. Google Scholar
  22. 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. Google Scholar
  23. 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. Google Scholar
  24. 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. Google Scholar
  25. 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. Google Scholar
  26. 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. Google Scholar
  27. 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.
  28. 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. Google Scholar
  29. 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. Google Scholar
  30. 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. Google Scholar
  31. Gilbert Stengle. A Nullstellensatz and a Positivstellensatz in semialgebraic geometry. Mathematische Annalen, 207(2):87-97, 1973. Google Scholar
  32. 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. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact