Document Open Access Logo

On Semi-Algebraic Proofs and Algorithms

Authors Noah Fleming, Mika Göös, Stefan Grosser, Robert Robere

PDF
Thumbnail PDF

File

LIPIcs.ITCS.2022.69.pdf
  • Filesize: 0.86 MB
  • 25 pages

Document Identifiers

Author Details

Noah Fleming
  • University of California, San Diego, CA, USA
  • Memorial University, St. John’s, Canada
Mika Göös
  • EPFL, Lausanne, Switzerland
Stefan Grosser
  • McGill University, Montreal, Canada
Robert Robere
  • McGill University, Montreal, Canada

Funding

  • Fleming, Noah: Research supported by NSERC.
  • Robere, Robert: Research supported by NSERC.

Cite AsGet BibTex

Noah Fleming, Mika Göös, Stefan Grosser, and Robert Robere. On Semi-Algebraic Proofs and Algorithms. In 13th Innovations in Theoretical Computer Science Conference (ITCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 215, pp. 69:1-69:25, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.ITCS.2022.69

Abstract

We give a new characterization of the Sherali-Adams proof system, showing that there is a degree-d Sherali-Adams refutation of an unsatisfiable CNF formula C if and only if there is an ε > 0 and a degree-d conical junta J such that viol_C(x) - ε = J, where viol_C(x) counts the number of falsified clauses of C on an input x. Using this result we show that the linear separation complexity, a complexity measure recently studied by Hrubeš (and independently by de Oliveira Oliveira and Pudlák under the name of weak monotone linear programming gates), monotone feasibly interpolates Sherali-Adams proofs. We then investigate separation results for viol_C(x) - ε. In particular, we give a family of unsatisfiable CNF formulas C which have polynomial-size and small-width resolution proofs, but for which any representation of viol_C(x) - 1 by a conical junta requires degree Ω(n); this resolves an open question of Filmus, Mahajan, Sood, and Vinyals. Since Sherali-Adams can simulate resolution, this separates the non-negative degree of viol_C(x) - 1 and viol_C(x) - ε for arbitrarily small ε > 0. Finally, by applying lifting theorems, we translate this lower bound into new separation results between extension complexity and monotone circuit complexity.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
Keywords
  • Proof Complexity
  • Extended Formulations
  • Circuit Complexity
  • Sherali-Adams

Metrics

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

References

  1. Sanjeev Arora, Béla Bollobás, László Lovász, and Iannis Tourlakis. Proving integrality gaps without knowing the linear program. Theory Comput., 2(2):19-51, 2006. URL: https://doi.org/10.4086/toc.2006.v002a002.
  2. Albert Atserias and Elitza N. Maneva. Sherali-adams relaxations and indistinguishability in counting logics. In Shafi Goldwasser, editor, Innovations in Theoretical Computer Science 2012, Cambridge, MA, USA, January 8-10, 2012, pages 367-379. ACM, 2012. URL: https://doi.org/10.1145/2090236.2090265.
  3. Albert Atserias and Joanna Ochremiak. Proof complexity meets algebra. ACM Trans. Comput. Log., 20(1):1:1-1:46, 2019. URL: https://doi.org/10.1145/3265985.
  4. Paul Beame, Stephen A. Cook, Jeff Edmonds, Russell Impagliazzo, and Toniann Pitassi. The relative complexity of NP search problems. In Frank Thomson Leighton and Allan Borodin, editors, Proceedings of the Twenty-Seventh Annual ACM Symposium on Theory of Computing, 29 May-1 June 1995, Las Vegas, Nevada, USA, pages 303-314. ACM, 1995. URL: https://doi.org/10.1145/225058.225147.
  5. Paul Beame, Toniann Pitassi, and Nathan Segerlind. Lower bounds for lov[a-acute]sz-schrijver systems and beyond follow from multiparty communication complexity. SIAM J. Comput., 37(3):845-869, 2007. URL: https://doi.org/10.1137/060654645.
  6. Siavosh Benabbas, Konstantinos Georgiou, Avner Magen, and Madhur Tulsiani. SDP gaps from pairwise independence. Theory Comput., 8(1):269-289, 2012. URL: https://doi.org/10.4086/toc.2012.v008a012.
  7. Christoph Berkholz. The relation between polynomial calculus, sherali-adams, and sum-of-squares proofs. In Rolf Niedermeier and Brigitte Vallée, editors, 35th Symposium on Theoretical Aspects of Computer Science, STACS 2018, February 28 to March 3, 2018, Caen, France, volume 96 of LIPIcs, pages 11:1-11:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.STACS.2018.11.
  8. Maria Luisa Bonet, Toniann Pitassi, and Ran Raz. Lower bounds for cutting planes proofs with small coefficients. J. Symb. Log., 62(3):708-728, 1997. URL: https://doi.org/10.2307/2275569.
  9. Gábor Braun, Samuel Fiorini, Sebastian Pokutta, and David Steurer. Approximation limits of linear programs (beyond hierarchies). Math. Oper. Res., 40(3):756-772, 2015. URL: https://doi.org/10.1287/moor.2014.0694.
  10. Gábor Braun and Sebastian Pokutta. Common information and unique disjointness. Algorithmica, 76(3):597-629, 2016. URL: https://doi.org/10.1007/s00453-016-0132-0.
  11. Mark Braverman and Ankur Moitra. An information complexity approach to extended formulations. In Dan Boneh, Tim Roughgarden, and Joan Feigenbaum, editors, Symposium on Theory of Computing Conference, STOC'13, Palo Alto, CA, USA, June 1-4, 2013, pages 161-170. ACM, 2013. URL: https://doi.org/10.1145/2488608.2488629.
  12. Samuel R. Buss. Lower bounds on nullstellensatz proofs via designs. In Paul Beam and Samuel R. Buss, editors, Proof Complexity and Feasible Arithmetics, Proceedings of a DIMACS Workshop, New Brunswick, New Jersey, USA, April 21-24, 1996, volume 39 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science, pages 59-71. DIMACS/AMS, 1996. URL: https://doi.org/10.1090/dimacs/039/04.
  13. Siu Man Chan and Aaron Potechin. Tight bounds for monotone switching networks via fourier analysis. Theory Comput., 10:389-419, 2014. URL: https://doi.org/10.4086/toc.2014.v010a015.
  14. Siu On Chan, James R. Lee, Prasad Raghavendra, and David Steurer. Approximate constraint satisfaction requires large LP relaxations. J. ACM, 63(4):34:1-34:22, 2016. URL: https://doi.org/10.1145/2811255.
  15. Moses Charikar, Konstantin Makarychev, and Yury Makarychev. Local global tradeoffs in metric embeddings. SIAM J. Comput., 39(6):2487-2512, 2010. URL: https://doi.org/10.1137/070712080.
  16. Arkadev Chattopadhyay, Yuval Filmus, Sajin Koroth, Or Meir, and Toniann Pitassi. Query-to-communication lifting using low-discrepancy gadgets. SIAM J. Comput., 50(1):171-210, 2021. URL: https://doi.org/10.1137/19M1310153.
  17. Arkadev Chattopadhyay, Michal Koucký, Bruno Loff, and Sagnik Mukhopadhyay. Simulation theorems via pseudorandom properties. CoRR, abs/1704.06807, 2017. URL: http://arxiv.org/abs/1704.06807.
  18. Stefan S. Dantchev, Barnaby Martin, and Mark Nicholas Charles Rhodes. Tight rank lower bounds for the sherali-adams proof system. Theor. Comput. Sci., 410(21-23):2054-2063, 2009. URL: https://doi.org/10.1016/j.tcs.2009.01.002.
  19. Wenceslas Fernandez de la Vega and Claire Kenyon-Mathieu. Linear programming relaxations of maxcut. In Nikhil Bansal, Kirk Pruhs, and Clifford Stein, editors, Proceedings of the Eighteenth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2007, New Orleans, Louisiana, USA, January 7-9, 2007, pages 53-61. SIAM, 2007. URL: http://dl.acm.org/citation.cfm?id=1283383.1283390.
  20. Mateus de Oliveira Oliveira and Pavel Pudlák. Representations of monotone boolean functions by linear programs. ACM Trans. Comput. Theory, 11(4):22:1-22:31, 2019. URL: https://doi.org/10.1145/3337787.
  21. Susanna F. de Rezende, Mika Göös, Jakob Nordström, Toniann Pitassi, Robert Robere, and Dmitry Sokolov. Automating algebraic proof systems is np-hard. In Samir Khuller and Virginia Vassilevska Williams, editors, STOC '21: 53rd Annual ACM SIGACT Symposium on Theory of Computing, Virtual Event, Italy, June 21-25, 2021, pages 209-222. ACM, 2021. URL: https://doi.org/10.1145/3406325.3451080.
  22. Susanna F. de Rezende, Or Meir, Jakob Nordström, Toniann Pitassi, Robert Robere, and Marc Vinyals. Lifting with simple gadgets and applications to circuit and proof complexity. In 61st IEEE Annual Symposium on Foundations of Computer Science, FOCS 2020, Durham, NC, USA, November 16-19, 2020, pages 24-30. IEEE, 2020. URL: https://doi.org/10.1109/FOCS46700.2020.00011.
  23. Susanna F. de Rezende, Jakob Nordström, and Marc Vinyals. How limited interaction hinders real communication (and what it means for proof and circuit complexity). In Irit Dinur, editor, IEEE 57th Annual Symposium on Foundations of Computer Science, FOCS 2016, 9-11 October 2016, Hyatt Regency, New Brunswick, New Jersey, USA, pages 295-304. IEEE Computer Society, 2016. URL: https://doi.org/10.1109/FOCS.2016.40.
  24. Yuval Filmus, Meena Mahajan, Gaurav Sood, and Marc Vinyals. Maxsat resolution and subcube sums. In Luca Pulina and Martina Seidl, editors, Theory and Applications of Satisfiability Testing - SAT 2020 - 23rd International Conference, Alghero, Italy, July 3-10, 2020, Proceedings, volume 12178 of Lecture Notes in Computer Science, pages 295-311. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-51825-7_21.
  25. Samuel Fiorini, Serge Massar, Sebastian Pokutta, Hans Raj Tiwary, and Ronald de Wolf. Exponential lower bounds for polytopes in combinatorial optimization. J. ACM, 62(2):17:1-17:23, 2015. URL: https://doi.org/10.1145/2716307.
  26. Noah Fleming, Mika Göös, Russell Impagliazzo, Toniann Pitassi, Robert Robere, Li-Yang Tan, and Avi Wigderson. On the power and limitations of branch and cut. In Valentine Kabanets, editor, 36th Computational Complexity Conference, CCC 2021, volume 200 of LIPIcs, pages 6:1-6:30. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.CCC.2021.6.
  27. Noah Fleming, Pravesh Kothari, and Toniann Pitassi. Semialgebraic proofs and efficient algorithm design. Electron. Colloquium Comput. Complex., 26:106, 2019. URL: https://eccc.weizmann.ac.il/report/2019/106.
  28. Noah Fleming, Denis Pankratov, Toniann Pitassi, and Robert Robere. Random Θ(log n)-CNFs are hard for cutting planes. In 58th IEEE Annual Symposium on Foundations of Computer Science, FOCS 2017, Berkeley, CA, USA, October 15-17, 2017, pages 109-120, 2017. URL: https://doi.org/10.1109/FOCS.2017.19.
  29. Ankit Garg, Mika Göös, Pritish Kamath, and Dmitry Sokolov. Monotone circuit lower bounds from resolution. In Ilias Diakonikolas, David Kempe, and Monika Henzinger, editors, Proceedings of the 50th Annual ACM SIGACT Symposium on Theory of Computing, STOC 2018, Los Angeles, CA, USA, June 25-29, 2018, pages 902-911. ACM, 2018. URL: https://doi.org/10.1145/3188745.3188838.
  30. Mika Goos. Communication Lower Bounds via Query Complexity. PhD thesis, University of Toronto (Canada), 2016. Google Scholar
  31. Mika Göös, Rahul Jain, and Thomas Watson. Extension complexity of independent set polytopes. SIAM J. Comput., 47(1):241-269, 2018. URL: https://doi.org/10.1137/16M109884X.
  32. Mika Göös, Sajin Koroth, Ian Mertz, and Toniann Pitassi. Automating cutting planes is np-hard. In Konstantin Makarychev, Yury Makarychev, Madhur Tulsiani, Gautam Kamath, and Julia Chuzhoy, editors, Proccedings of the 52nd Annual ACM SIGACT Symposium on Theory of Computing, STOC 2020, Chicago, IL, USA, June 22-26, 2020, pages 68-77. ACM, 2020. URL: https://doi.org/10.1145/3357713.3384248.
  33. Mika Göös, Shachar Lovett, Raghu Meka, Thomas Watson, and David Zuckerman. Rectangles are nonnegative juntas. SIAM J. Comput., 45(5):1835-1869, 2016. URL: https://doi.org/10.1137/15M103145X.
  34. Mika Göös and Toniann Pitassi. Communication lower bounds via critical block sensitivity. SIAM J. Comput., 47(5):1778-1806, 2018. URL: https://doi.org/10.1137/16M1082007.
  35. Mika Göös, Toniann Pitassi, and Thomas Watson. Query-to-communication lifting for BPP. SIAM J. Comput., 49(4), 2020. URL: https://doi.org/10.1137/17M115339X.
  36. Dima Grigoriev. Linear lower bound on degrees of positivstellensatz calculus proofs for the parity. Theor. Comput. Sci., 259(1-2):613-622, 2001. URL: https://doi.org/10.1016/S0304-3975(00)00157-2.
  37. Tuomas Hakoniemi. Feasible interpolation for polynomial calculus and sums-of-squares. In Artur Czumaj, Anuj Dawar, and Emanuela Merelli, editors, 47th International Colloquium on Automata, Languages, and Programming, ICALP 2020, July 8-11, 2020, Saarbrücken, Germany (Virtual Conference), volume 168 of LIPIcs, pages 63:1-63:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.ICALP.2020.63.
  38. Samuel B. Hopkins, Tselil Schramm, and Luca Trevisan. Subexponential lps approximate max-cut. In 61st IEEE Annual Symposium on Foundations of Computer Science, FOCS 2020, Durham, NC, USA, November 16-19, 2020, pages 943-953. IEEE, 2020. URL: https://doi.org/10.1109/FOCS46700.2020.00092.
  39. Pavel Hrubes. On the nonnegative rank of distance matrices. Inf. Process. Lett., 112(11):457-461, 2012. URL: https://doi.org/10.1016/j.ipl.2012.02.009.
  40. Pavel Hrubes. On ε-sensitive monotone computations. Comput. Complex., 29(2):6, 2020. URL: https://doi.org/10.1007/s00037-020-00196-6.
  41. Pavel Hrubes and Pavel Pudlák. Random formulas, monotone circuits, and interpolation. In Chris Umans, editor, 58th IEEE Annual Symposium on Foundations of Computer Science, FOCS 2017, Berkeley, CA, USA, October 15-17, 2017, pages 121-131. IEEE Computer Society, 2017. URL: https://doi.org/10.1109/FOCS.2017.20.
  42. Pravesh Kothari, Raghu Meka, and Prasad Raghavendra. Approximating rectangles by juntas and weakly-exponential lower bounds for LP relaxations of csps. CoRR, abs/1610.02704, 2016. URL: http://arxiv.org/abs/1610.02704.
  43. Pravesh K. Kothari, Ryuhei Mori, Ryan O'Donnell, and David Witmer. Sum of squares lower bounds for refuting any CSP. In Hamed Hatami, Pierre McKenzie, and Valerie King, editors, Proceedings of the 49th Annual ACM SIGACT Symposium on Theory of Computing, STOC 2017, Montreal, QC, Canada, June 19-23, 2017, pages 132-145. ACM, 2017. URL: https://doi.org/10.1145/3055399.3055485.
  44. Jan Krajícek. Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic. J. Symb. Log., 62(2):457-486, 1997. URL: https://doi.org/10.2307/2275541.
  45. Claire Mathieu and Alistair Sinclair. Sherali-adams relaxations of the matching polytope. In Michael Mitzenmacher, editor, Proceedings of the 41st Annual ACM Symposium on Theory of Computing, STOC 2009, Bethesda, MD, USA, May 31 - June 2, 2009, pages 293-302. ACM, 2009. URL: https://doi.org/10.1145/1536414.1536456.
  46. Ryan O'Donnell and Tselil Schramm. Sherali - adams strikes back. In Amir Shpilka, editor, 34th Computational Complexity Conference, CCC 2019, July 18-20, 2019, New Brunswick, NJ, USA, volume 137 of LIPIcs, pages 8:1-8:30. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.CCC.2019.8.
  47. Pavel Pudlák. Lower bounds for resolution and cutting plane proofs and monotone computations. J. Symb. Log., 62(3):981-998, 1997. URL: https://doi.org/10.2307/2275583.
  48. Pavel Pudlák and Jirí Sgall. Algebraic models of computation and interpolation for algebraic proof systems. In Paul Beam and Samuel R. Buss, editors, Proof Complexity and Feasible Arithmetics, Proceedings of a DIMACS Workshop, New Brunswick, New Jersey, USA, April 21-24, 1996, volume 39 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science, pages 279-295. DIMACS/AMS, 1996. URL: https://doi.org/10.1090/dimacs/039/15.
  49. Prasad Raghavendra and David Steurer. Integrality gaps for strong SDP relaxations of UNIQUE GAMES. In 50th Annual IEEE Symposium on Foundations of Computer Science, FOCS 2009, October 25-27, 2009, Atlanta, Georgia, USA, pages 575-585. IEEE Computer Society, 2009. URL: https://doi.org/10.1109/FOCS.2009.73.
  50. Ran Raz and Pierre McKenzie. Separation of the monotone NC hierarchy. Comb., 19(3):403-435, 1999. URL: https://doi.org/10.1007/s004930050062.
  51. Alexander A Razborov. Unprovability of lower bounds on circuit size in certain fragments of bounded arithmetic. Izvestiya: mathematics, 59(1):205, 1995. Google Scholar
  52. Robert Robere. Unified lower bounds for monotone computation. PhD thesis, University of Toronto (Canada), 2018. Google Scholar
  53. Robert Robere, Toniann Pitassi, Benjamin Rossman, and Stephen A. Cook. Exponential lower bounds for monotone span programs. In Irit Dinur, editor, IEEE 57th Annual Symposium on Foundations of Computer Science, FOCS 2016, pages 406-415. IEEE Computer Society, 2016. URL: https://doi.org/10.1109/FOCS.2016.51.
  54. Thomas Rothvoß. Some 0/1 polytopes need exponential size extended formulations. Math. Program., 142(1-2):255-268, 2013. URL: https://doi.org/10.1007/s10107-012-0574-3.
  55. Thomas Rothvoss. The matching polytope has exponential extension complexity. J. ACM, 64(6):41:1-41:19, 2017. URL: https://doi.org/10.1145/3127497.
  56. Grant Schoenebeck. Linear level lasserre lower bounds for certain k-csps. In 49th Annual IEEE Symposium on Foundations of Computer Science, FOCS 2008, October 25-28, 2008, Philadelphia, PA, USA, pages 593-602. IEEE Computer Society, 2008. URL: https://doi.org/10.1109/FOCS.2008.74.
  57. Xiaodi Wu, Penghui Yao, and Henry S. Yuen. Raz-mckenzie simulation with the inner product gadget. Electron. Colloquium Comput. Complex., page 10, 2017. URL: https://eccc.weizmann.ac.il/report/2017/010.
  58. Mihalis Yannakakis. Expressing combinatorial optimization problems by linear programs. J. Comput. Syst. Sci., 43(3):441-466, 1991. URL: https://doi.org/10.1016/0022-0000(91)90024-Y.
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 Schloss Dagstuhl - LZI GmbH Imprint Privacy Contact