[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ skip to main content
10.1145/3531130.3533344acmconferencesArticle/Chapter ViewAbstractPublication PageslicsConference Proceedingsconference-collections
research-article

On the strength of Sherali-Adams and Nullstellensatz as propositional proof systems

Published: 04 August 2022 Publication History

Abstract

We characterize the strength of the algebraic proof systems Sherali-Adams () and Nullstellensatz () in terms of Frege-style proof systems. Unlike bounded-depth Frege, has polynomial-size proofs of the pigeonhole principle (). A natural question is whether adding to bounded-depth Frege is enough to simulate .
We show that, with unary integer coefficients, lies strictly between tree-like and tree-like Resolution. We introduce a weighted version of () and we show that with integer coefficients lies strictly between tree-like and Resolution.
Analogous results are shown for using the bijective (i.e. onto and functional) pigeonhole principle and a weighted version of it.

References

[1]
M. Ajtai. 1990. Parity and the Pigeonhole Principle. Birkhäuser Boston, Boston, MA, 1–24.
[2]
Albert Atserias and Massimo Lauria. 2019. Circular (Yet Sound) Proofs. In Theory and Applications of Satisfiability Testing - SAT 2019 - 22nd International Conference, SAT 2019, Lisbon, Portugal, July 9-12, 2019, Proceedings(Lecture Notes in Computer Science, Vol. 11628), Mikolás Janota and Inês Lynce (Eds.). Springer, 1–18.
[3]
Albert Atserias and Joanna Ochremiak. 2018. Proof Complexity Meets Algebra. ACM Trans. Comput. Logic 20, 1 (Dec. 2018), 1–46.
[4]
Paul Beame, Stephen Cook, Jeff Edmonds, Russell Impagliazzo, and Toniann Pitassi. 1998. The Relative Complexity of NP Search Problems. J. Comput. System Sci. 57, 1 (1998), 3 – 19.
[5]
P. Beame, R. Impagliazzo, J. Krajicek, T. Pitassi, and P. Pudlak. 1994. Lower bounds on Hilbert’s Nullstellensatz and propositional proofs. In Proceedings 35th Annual Symposium on Foundations of Computer Science. 794–806.
[6]
Paul Beame and Toniann Pitassi. 1996. An Exponential Separation between the Parity Principle and the Pigeonhole Principle. Ann. Pure Appl. Log. 80 (10 1996), 195–228.
[7]
Arnold Beckmann and Sam Buss. 2019. On transformations of constant depth propositional proofs. Ann. Pure Appl. Log. 170, 10 (2019), 1176–1187.
[8]
Maria Luisa Bonet, Sam Buss, Alexey Ignatiev, João Marques-Silva, and António Morgado. 2018. MaxSAT Resolution With the Dual Rail Encoding. In AAAI. 6565–6572.
[9]
Maria Luisa Bonet, Sam Buss, Alexey Ignatiev, Antonio Morgado, and Joao Marques-Silva. 2021. Propositional proof systems based on maximum satisfiability. Artificial Intelligence 300 (2021), 103552.
[10]
Maria Luisa Bonet and Jordi Levy. 2020. Equivalence Between Systems Stronger Than Resolution. In Theory and Applications of Satisfiability Testing – SAT 2020. Springer International Publishing, Cham, 166–181.
[11]
Samuel R. Buss. 1998. Lower bounds on Nullstellensatz proofs via designs. In Proof complexity and feasible arithmetics (Rutgers, NJ, 1996). DIMACS Ser. Discrete Math. Theoret. Comput. Sci., Vol. 39. Amer. Math. Soc., Providence, RI, 59–71.
[12]
Stephen A. Cook and Robert A. Reckhow. 1979. The Relative Efficiency of Propositional Proof Systems. The Journal of Symbolic Logic 44, 1 (1979), 36–50.
[13]
Stefan S. Dantchev, Abdul Ghani, and Barnaby Martin. 2020. Sherali-Adams and the Binary Encoding of Combinatorial Principles. In LATIN 2020: Theoretical Informatics - 14th Latin American Symposium, São Paulo, Brazil, January 5-8, 2021, Proceedings(Lecture Notes in Computer Science, Vol. 12118), Yoshiharu Kohayakawa and Flávio Keidi Miyazawa (Eds.). Springer, 336–347.
[14]
Susanna F. de Rezende, Massimo Lauria, Jakob Nordström, and Dmitry Sokolov. 2021. The Power of Negative Reasoning. In 36th Computational Complexity Conference (CCC 2021)(Leibniz International Proceedings in Informatics (LIPIcs), Vol. 200), Valentine Kabanets (Ed.). Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 40:1–40:24.
[15]
Noah Fleming, Stephan Grosser, Mika Göös, and Robert Robere. 2022. On Semi-Algebraic Proofs and Algorithms. Electron. Colloquium Comput. Complex.(2022), TR22–003.
[16]
Noah Fleming, Pravesh Kothari, and Toniann Pitassi. 2019. Semialgebraic Proofs and Efficient Algorithm Design. Foundations and Trends® in Theoretical Computer Science 14, 1-2(2019), 1–221.
[17]
Mika Göös, Alexandros Hollender, Siddhartha Jain, Gilbert Maystre, William Pires, Robert Robere, and Ran Tao. 2022. Separations in Proof Complexity and TFNP. CoRR abs/2205.02168(2022). https://doi.org/10.48550/arXiv.2205.02168 arXiv:2205.02168
[18]
Tuomas Hakoniemi. 2021. Monomial size vs. Bit-complexity in Sums-of-Squares and Polynomial Calculus. In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021. IEEE, 1–7.
[19]
Russell Impagliazzo and Nathan Segerlind. 2006. Constant-Depth Frege Systems with Counting Axioms Polynomially Simulate Nullstellensatz Refutations. ACM Trans. Comput. Logic 7, 2 (April 2006), 199–218.
[20]
Jan Krajíček. 2019. Proof Complexity. Cambridge University Press.
[21]
Jan Krajíček, Pavel Pudlák, and Alan Woods. 1995. An exponential lower bound to the size of bounded depth frege proofs of the pigeonhole principle. Random Structures and Algorithms 7, 1 (Aug. 1995), 15–39.
[22]
Jan Krajiček. 1994. Lower Bounds to the Size of Constant-Depth Propositional Proofs. The Journal of Symbolic Logic 59, 1 (1994), 73–86.
[23]
Javier Larrosa and Emma Rollon. 2020. Augmenting the Power of (Partial) MaxSat Resolution with Extension. Proceedings of the AAAI Conference on Artificial Intelligence 34, 02 (Apr. 2020), 1561–1568.
[24]
Javier Larrosa and Emma Rollon. 2020. Towards a Better Understanding of (Partial Weighted) MaxSAT Proof Systems. In Theory and Applications of Satisfiability Testing – SAT 2020, Luca Pulina and Martina Seidl (Eds.). Springer International Publishing, Cham, 218–232.
[25]
Toniann Pitassi, Paul Beame, and Russell Impagliazzo. 1993. Exponential lower bounds for the pigeonhole principle. Computational Complexity 3, 2 (Jun 1993), 97–140.
[26]
Toniann Pitassi and Robert Robere. 2017. Strongly Exponential Lower Bounds for Monotone Computation. In Proceedings of the 49th Annual ACM SIGACT Symposium on Theory of Computing(STOC 2017). Association for Computing Machinery, New York, NY, USA, 1246–1255.
[27]
Toniann Pitassi and Robert Robere. 2018. Lifting Nullstellensatz to Monotone Span Programs over Any Field. In Proceedings of the 50th Annual ACM SIGACT Symposium on Theory of Computing(STOC 2018). Association for Computing Machinery, New York, NY, USA, 1207–1219.
[28]
Robert Robere, Toniann Pitassi, Benjamin Rossman, and Stephen A. Cook. 2016. Exponential Lower Bounds for Monotone Span Programs. In 2016 IEEE 57th Annual Symposium on Foundations of Computer Science (FOCS). 406–415.
[29]
Hanif D. Sherali and Warren P. Adams. 1990. A Hierarchy of Relaxations between the Continuous and Convex Hull Representations for Zero-One Programming Problems. SIAM Journal on Discrete Mathematics 3, 3 (1990), 411–430.
[30]
Alasdair Urquhart and Xudong Fu. 1996. Simplified Lower Bounds for Propositional Proofs. Notre Dame Journal of Formal Logic 37, 4 (1996), 523–544.

Cited By

View all
  • (2024)Separations in Proof Complexity and TFNPJournal of the ACM10.1145/366375871:4(1-45)Online publication date: 9-May-2024
  • (2024)Strength and limitations of Sherali-Adams and Nullstellensatz proof systemsAnnals of Pure and Applied Logic10.1016/j.apal.2024.103538(103538)Online publication date: Nov-2024

Recommendations

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences
LICS '22: Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science
August 2022
817 pages
ISBN:9781450393515
DOI:10.1145/3531130
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 04 August 2022

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. Nullstellensatz
  2. Pigeonhole Principle
  3. Sherali-Adams
  4. bounded-depth Frege

Qualifiers

  • Research-article
  • Research
  • Refereed limited

Funding Sources

  • MICIN

Conference

LICS '22
Sponsor:

Acceptance Rates

Overall Acceptance Rate 215 of 622 submissions, 35%

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)32
  • Downloads (Last 6 weeks)19
Reflects downloads up to 12 Dec 2024

Other Metrics

Citations

Cited By

View all
  • (2024)Separations in Proof Complexity and TFNPJournal of the ACM10.1145/366375871:4(1-45)Online publication date: 9-May-2024
  • (2024)Strength and limitations of Sherali-Adams and Nullstellensatz proof systemsAnnals of Pure and Applied Logic10.1016/j.apal.2024.103538(103538)Online publication date: Nov-2024

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

HTML Format

View this article in HTML Format.

HTML Format

Media

Figures

Other

Tables

Share

Share

Share this Publication link

Share on social media