Document Open Access Logo

The Power of Negative Reasoning

Authors Susanna F. de Rezende, Massimo Lauria, Jakob Nordström, Dmitry Sokolov

PDF
Thumbnail PDF

File

LIPIcs.CCC.2021.40.pdf
  • Filesize: 0.74 MB
  • 24 pages

Document Identifiers

Author Details

Susanna F. de Rezende
  • Institute of Mathematics of the Czech Academy of Sciences, Prague, Czech Republic
Massimo Lauria
  • Sapienza Università di Roma, Italy
Jakob Nordström
  • University of Copenhagen, Denmark
  • Lund University, Sweden
Dmitry Sokolov
  • St. Petersburg State University, Russia
  • PDMI RAS, St. Petersburg, Russia

Funding

Susanna F. de Rezende was supported by Knut and Alice Wallenberg grant KAW 2018.0371. Jakob Nordström received funding from the Swedish Research Council grant 2016-00782 and the Independent Research Fund Denmark grant 9040-00389B. Part of this work was carried out while visiting the Simons Institute for the Theory of Computing.

Acknowledgements

We thank Or Meir for fruitful discussions and the anonymous reviewers for comments on the presentation.

Cite As Get BibTex

Susanna F. de Rezende, Massimo Lauria, Jakob Nordström, and Dmitry Sokolov. The Power of Negative Reasoning. In 36th Computational Complexity Conference (CCC 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 200, pp. 40:1-40:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.CCC.2021.40

Abstract

Semialgebraic proof systems have been studied extensively in proof complexity since the late 1990s to understand the power of Gröbner basis computations, linear and semidefinite programming hierarchies, and other methods. Such proof systems are defined alternately with only the original variables of the problem and with special formal variables for positive and negative literals, but there seems to have been no study how these different definitions affect the power of the proof systems. We show for Nullstellensatz, polynomial calculus, Sherali-Adams, and sums-of-squares that adding formal variables for negative literals makes the proof systems exponentially stronger, with respect to the number of terms in the proofs. These separations are witnessed by CNF formulas that are easy for resolution, which establishes that polynomial calculus, Sherali-Adams, and sums-of-squares cannot efficiently simulate resolution without having access to variables for negative literals.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
  • Computing methodologies → Representation of polynomials
Keywords
  • Proof complexity
  • Polynomial calculus
  • Nullstellensatz
  • Sums-of-squares
  • Sherali-Adams

Metrics

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

References

  1. Michael Alekhnovich, Eli Ben-Sasson, Alexander A. Razborov, and Avi Wigderson. Space complexity in propositional calculus. SIAM Journal on Computing, 31(4):1184-1211, 2002. Preliminary version in STOC '00. Google Scholar
  2. Michael Alekhnovich and Alexander A. Razborov. Lower bounds for polynomial calculus: Non-binomial case. Proceedings of the Steklov Institute of Mathematics, 242:18-35, 2003. Preliminary version in FOCS '01. Google Scholar
  3. Joël Alwen, Susanna F. de Rezende, Jakob Nordström, and Marc Vinyals. Cumulative space in black-white pebbling and resolution. In Proceedings of the 8th Innovations in Theoretical Computer Science Conference (ITCS '17), volume 67 of Leibniz International Proceedings in Informatics (LIPIcs), pages 38:1-38:21, 2017. Google Scholar
  4. Albert Atserias and Tuomas Hakoniemi. Size-degree trade-offs for Sums-of-Squares and Positivstellensatz proofs. In Proceedings of the 34th Annual Computational Complexity Conference (CCC '19), volume 137 of Leibniz International Proceedings in Informatics (LIPIcs), pages 24:1-24:20, July 2019. Google Scholar
  5. Albert Atserias, Massimo Lauria, and Jakob Nordström. Narrow proofs may be maximally long. ACM Transactions on Computational Logic, 17(3):19:1-19:30, May 2016. Preliminary version in CCC '14. Google Scholar
  6. Albert Atserias and Moritz Müller. Automating resolution is NP-hard. In Proceedings of the 60th Annual IEEE Symposium on Foundations of Computer Science (FOCS '19), pages 498-509, November 2019. Google Scholar
  7. 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, 1994. Google Scholar
  8. Chris Beck, Jakob Nordström, and Bangsheng Tang. Some trade-off results for polynomial calculus. In Proceedings of the 45th Annual ACM Symposium on Theory of Computing (STOC '13), pages 813-822, May 2013. Google Scholar
  9. Eli Ben-Sasson and Avi Wigderson. Short proofs are narrow - resolution made simple. Journal of the ACM, 48(2):149-169, March 2001. Preliminary version in STOC '99. Google Scholar
  10. Charles H. Bennett. Time/space trade-offs for reversible computation. SIAM Journal on Computing, 18(4):766-776, August 1989. Google Scholar
  11. Christoph Berkholz. The relation between polynomial calculus, Sherali-Adams, and sum-of-squares proofs. In Proceedings of the 35th Symposium on Theoretical Aspects of Computer Science (STACS '18), volume 96 of Leibniz International Proceedings in Informatics (LIPIcs), pages 11:1-11:14, 2018. Google Scholar
  12. Joshua Buresh-Oppenheim, Matthew Clegg, Russell Impagliazzo, and Toniann Pitassi. Homogenization and the polynomial calculus. Computational Complexity, 11(3-4):91-108, 2002. Preliminary version in ICALP '00. Google Scholar
  13. Samuel R. Buss and Jakob Nordström. Proof complexity and SAT solving. In Armin Biere, Marijn J. H. Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability, volume 336 of Frontiers in Artificial Intelligence and Applications, chapter 7, pages 233-350. IOS Press, 2nd edition, February 2021. Google Scholar
  14. Matthew Clegg, Jeffery Edmonds, and Russell Impagliazzo. Using the Groebner basis algorithm to find proofs of unsatisfiability. In Proceedings of the 28th Annual ACM Symposium on Theory of Computing (STOC '96), pages 174-183, 1996. Google Scholar
  15. Stephen A. Cook and Robert A. Reckhow. The relative efficiency of propositional proof systems. Journal of Symbolic Logic, 44(1):36-50, 1979. Preliminary version in STOC '74. Google Scholar
  16. Stefan S. Dantchev, Barnaby Martin, and Martin Rhodes. Tight rank lower bounds for the Sherali-Adams proof system. Theoretical Computer Science, 410(21-23):2054-2063, May 2009. Google Scholar
  17. 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 Proceedings of the 53rd Annual ACM Symposium on Theory of Computing (STOC '21), June 2021. To appear. Google Scholar
  18. 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 Proceedings of the 61st Annual IEEE Symposium on Foundations of Computer Science (FOCS '20), pages 24-30, November 2020. Google Scholar
  19. Susanna F. de Rezende, Jakob Nordström, Or Meir, and Robert Robere. Nullstellensatz size-degree trade-offs from reversible pebbling. In Proceedings of the 34th Annual Computational Complexity Conference (CCC '19), volume 137 of Leibniz International Proceedings in Informatics (LIPIcs), pages 18:1-18:16, 2019. Google Scholar
  20. Yuval Filmus, Massimo Lauria, Jakob Nordström, Noga Ron-Zewi, and Neil Thapen. Space complexity in polynomial calculus. SIAM Journal on Computing, 44(4):1119-1153, August 2015. Preliminary version in CCC '12. Google Scholar
  21. Noah Fleming, Pravesh Kothari, and Toniann Pitassi. Semialgebraic proofs and efficient algorithm design. Foundations and Trends in Theoretical Computer Science, 14(1-2):1-221, December 2019. Google Scholar
  22. Nicola Galesi, Leszek Kołodziejczyk, and Neil Thapen. Polynomial calculus space and resolution width. In Proceedings of the 60th Annual IEEE Symposium on Foundations of Computer Science (FOCS '19), pages 1325-1337, November 2019. Google Scholar
  23. Nicola Galesi and Massimo Lauria. Optimality of size-degree trade-offs for polynomial calculus. ACM Transactions on Computational Logic, 12(1):4:1-4:22, November 2010. Google Scholar
  24. John R. Gilbert and Robert Endre Tarjan. Variations of a pebble game on graphs. Technical Report STAN-CS-78-661, Stanford University, 1978. Available at URL: http://infolab.stanford.edu/TR/CS-TR-78-661.html.
  25. Dima Grigoriev and Nicolai Vorobjov. Complexity of Null- and Positivstellensatz proofs. Annals of Pure and Applied Logic, 113(1-3):153-160, 2001. Google Scholar
  26. Russell Impagliazzo, Pavel Pudlák, and Jiří Sgall. Lower bounds for the polynomial calculus and the Gröbner basis algorithm. Computational Complexity, 8(2):127-144, 1999. Google Scholar
  27. Daniela Kaufmann, Armin Biere, and Manuel Kauers. From DRUP to PAC and back. In Proceedings of the Design, Automation & Test in Europe Conference & Exhibition (DATE '20), pages 654-657, March 2020. Google Scholar
  28. Jan Krajíček. Proof Complexity, volume 170 of Encyclopedia of Mathematics and Its Applications. Cambridge University Press, March 2019. Google Scholar
  29. Balakrishnan Krishnamurthy. Short proofs for tricky formulas. Acta Informatica, 22(3):253-275, 1985. Google Scholar
  30. 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, 2001. Google Scholar
  31. Massimo Lauria and Jakob Nordström. Tight size-degree bounds for sums-of-squares proofs. Computational Complexity, 26(3):911-948, December 2017. Preliminary version in CCC '15. Google Scholar
  32. Robert Y. Levin and Alan T. Sherman. A note on Bennett’s time-space tradeoff for reversible computation. SIAM Journal on Computing, 19(4):673-677, August 1990. URL: https://doi.org/10.1137/0219046.
  33. Mladen Mikša and Jakob Nordström. A generalized method for proving polynomial calculus degree lower bounds. In Proceedings of the 30th Annual Computational Complexity Conference (CCC '15), volume 33 of Leibniz International Proceedings in Informatics (LIPIcs), pages 467-487, June 2015. Google Scholar
  34. Wolfgang J. Paul, Robert Endre Tarjan, and James R. Celoni. Space bounds for a game on graphs. Mathematical Systems Theory, 10:239-251, 1977. Google Scholar
  35. Aaron Potechin. Sum of squares bounds for the ordering principle. In Shubhangi Saraf, editor, 35th Computational Complexity Conference, CCC 2020, July 28-31, 2020, Saarbrücken, Germany (Virtual Conference), volume 169 of LIPIcs, pages 38:1-38:37. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.CCC.2020.38.
  36. Amr Sayed-Ahmed, Daniel Große, Mathias Soeken, and Rolf Drechsler. Equivalence checking using Gröbner bases. In Proceedings of the 16th Conference on Formal Methods in Computer-Aided Design (FMCAD '16), pages 169-176, 2016. Google Scholar
  37. Nathan Segerlind, Samuel R. Buss, and Russell Impagliazzo. A switching lemma for small restrictions and lower bounds for k-DNF resolution. SIAM Journal on Computing, 33(5):1171-1200, 2004. Preliminary version in FOCS '02. Google Scholar
  38. Hanif D. Sherali and Warren P. Adams. A hierarchy of relaxations between the continuous and convex hull representations for zero-one programming problems. SIAM Journal on Discrete Mathematics, 3:411-430, 1990. Google Scholar
  39. Gunnar Stålmarck. Short resolution proofs for a sequence of tricky formulas. Acta Informatica, 33(3):277-280, May 1996. 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-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact