Document Open Access Logo

Polynomial Calculus for MaxSAT

Authors Ilario Bonacina , Maria Luisa Bonet , Jordi Levy

PDF
Thumbnail PDF

File

LIPIcs.SAT.2023.5.pdf
  • Filesize: 0.83 MB
  • 17 pages

Document Identifiers

Author Details

Ilario Bonacina
  • Polytechnic University of Catalonia, Barcelona, Spain
Maria Luisa Bonet
  • Polytechnic University of Catalonia, Barcelona, Spain
Jordi Levy
  • Artificial Intelligence Research Institute, Spanish Research Council (IIIA-CSIC), Barcelona, Spain

Funding

This work was supported by the Spanish Agencia Estatal de Investigación with the grant PID2019-109137GB-C21/AEI/10.13039/501100011033 and the grant PID2019-109137GB-C22/AEI/10.13039/501100011033.
  • Bonacina, Ilario: Partially supported by the grant IJC2018-035334-I/AEI/10.13039/501100011033.
  • Bonet, Maria Luisa: Partially supported by Simons Institute.
  • Levy, Jordi: Partially supported by Simons Institute.

Cite AsGet BibTex

Ilario Bonacina, Maria Luisa Bonet, and Jordi Levy. Polynomial Calculus for MaxSAT. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 5:1-5:17, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.SAT.2023.5

Abstract

MaxSAT is the problem of finding an assignment satisfying the maximum number of clauses in a CNF formula. We consider a natural generalization of this problem to generic sets of polynomials and propose a weighted version of Polynomial Calculus to address this problem. Weighted Polynomial Calculus is a natural generalization of MaxSAT-Resolution and weighted Resolution that manipulates polynomials with coefficients in a finite field and either weights in ℕ or ℤ. We show the soundness and completeness of these systems via an algorithmic procedure. Weighted Polynomial Calculus, with weights in ℕ and coefficients in 𝔽₂, is able to prove efficiently that Tseitin formulas on a connected graph are minimally unsatisfiable. Using weights in ℤ, it also proves efficiently that the Pigeonhole Principle is minimally unsatisfiable.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
  • Theory of computation → Automated reasoning
Keywords
  • Polynomial Calculus
  • MaxSAT
  • Proof systems
  • Algebraic reasoning

Metrics

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

References

  1. Carlos Ansótegui, Maria Luisa Bonet, Jordi Levy, and Felip Manyà. The logic behind weighted CSP. In Manuela M. Veloso, editor, IJCAI 2007, Proceedings of the 20th International Joint Conference on Artificial Intelligence, Hyderabad, India, January 6-12, 2007, pages 32-37, 2007. URL: http://ijcai.org/Proceedings/07/Papers/003.pdf.
  2. Carlos Ansótegui and Jordi Levy. Reducing SAT to Max2SAT. In Proc. of the 30th International Joint Conference on Artificial Intelligence (IJCAI'21), pages 1367-1373, 2021. Google Scholar
  3. Albert Atserias, Johannes Klaus Fichte, and Marc Thurley. Clause-learning algorithms with many restarts and bounded-width resolution. In Lecture Notes in Computer Science, pages 114-127. Springer Berlin Heidelberg, 2009. Google Scholar
  4. Albert Atserias and Massimo Lauria. Circular (yet sound) proofs. In Mikolás Janota and Inês Lynce, editors, Theory and Applications of Satisfiability Testing - SAT 2019 - 22nd International Conference, SAT 2019, Lisbon, Portugal, July 9-12, 2019, Proceedings, volume 11628 of Lecture Notes in Computer Science, pages 1-18. Springer, 2019. Google Scholar
  5. Maria Luisa Bonet, Sam Buss, Alexey Ignatiev, Antonio Morgado, and Joao Marques-Silva. Propositional proof systems based on maximum satisfiability. Artificial Intelligence, 300:103552, 2021. Google Scholar
  6. Maria Luisa Bonet and Jordi Levy. Equivalence between systems stronger than resolution. In Luca Pulina and Martina Seidl, editors, Theory and Applications of Satisfiability Testing - SAT 2020, pages 166-181, Cham, 2020. Springer International Publishing. Google Scholar
  7. Maria Luisa Bonet, Jordi Levy, and Felip Manyà. A complete calculus for Max-SAT. In Proc. of the 9th Int. Conf. on Theory and Applications of Satisfiability Testing (SAT'06), pages 240-251, 2006. Google Scholar
  8. Maria Luisa Bonet, Jordi Levy, and Felip Manyà. Resolution for max-SAT. Artif. Intell., 171(8-9):606-618, 2007. Google Scholar
  9. Michael Brickenstein and Alexander Dreyer. Polybori: A framework for groebner-basis computations with boolean polynomials. Journal of Symbolic Computation, 44(9):1326-1345, 2009. Effective Methods in Algebraic Geometry. URL: https://doi.org/10.1016/j.jsc.2008.02.017.
  10. B. Buchberger. A theoretical basis for the reduction of polynomials to canonical forms. SIGSAM Bull., 10(3):19-29, August 1976. URL: https://doi.org/10.1145/1088216.1088219.
  11. Sam Buss, Dima Grigoriev, Russell Impagliazzo, and Toniann Pitassi. Linear gaps between degrees for the polynomial calculus modulo distinct primes. Journal of Computer and System Sciences, 62(2):267-289, 2001. Google Scholar
  12. Matthew Clegg, Jeff Edmonds, and Russell Impagliazzo. Using the Groebner basis algorithm to find proofs of unsatisfiability. In Gary L. Miller, editor, Proceedings of the Twenty-Eighth Annual ACM Symposium on the Theory of Computing, Philadelphia, Pennsylvania, USA, May 22-24, 1996, pages 174-183. ACM, 1996. Google Scholar
  13. Stephen A. Cook and Robert A. Reckhow. The relative efficiency of propositional proof systems. The Journal of Symbolic Logic, 44(1):36-50, 1979. Google Scholar
  14. Jesús A De Loera, J. Lee, S. Margulies, and S. Onn. Expressing combinatorial problems by systems of polynomial equations and Hilbert’s Nullstellensatz. Comb. Probab. Comput., 18(4):551-582, July 2009. URL: https://doi.org/10.1017/S0963548309009894.
  15. Jesús A De Loera, Jon Lee, Peter N Malkin, and Susan Margulies. Computing infeasibility certificates for combinatorial problems through Hilbert’s Nullstellensatz. Journal of Symbolic Computation, 46(11):1260-1283, 2011. Google Scholar
  16. Jesús A De Loera, Susan Margulies, Michael Pernpeintner, Eric Riedl, David Rolnick, Gwen Spencer, Despina Stasi, and Jon Swenson. Graph-coloring ideals: Nullstellensatz certificates, Gröbner bases for chordal graphs, and hardness of Gröbner bases. In Proceedings of the 2015 ACM on International Symposium on Symbolic and Algebraic Computation, pages 133-140. ACM, 2015. Google Scholar
  17. Susanna F. de Rezende, Massimo Lauria, Jakob Nordström, and Dmitry Sokolov. The Power of Negative Reasoning. In Valentine Kabanets, editor, 36th Computational Complexity Conference (CCC 2021), volume 200 of Leibniz International Proceedings in Informatics (LIPIcs), pages 40:1-40:24, Dagstuhl, Germany, 2021. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. Google Scholar
  18. Jean Charles Faugère. A new efficient algorithm for computing gröbner bases without reduction to zero (f5). In Proceedings of the 2002 International Symposium on Symbolic and Algebraic Computation, ISSAC '02, pages 75-83, New York, NY, USA, 2002. Association for Computing Machinery. URL: https://doi.org/10.1145/780506.780516.
  19. Yuval Filmus, Edward A. Hirsch, Artur Riazanov, Alexander Smal, and Marc Vinyals. Proving unsatisfiability with hitting formulas. Electron. Colloquium Comput. Complex., TR23-016, 2023. URL: https://arxiv.org/abs/TR23-016.
  20. 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
  21. Alexey Ignatiev, António Morgado, and João Marques-Silva. On tackling the limits of resolution in SAT solving. In Proc. of the 20th Int. Conf. on Theory and Applications of Satisfiability Testing (SAT'17), pages 164-183, 2017. Google Scholar
  22. Daniela Kaufmann, Paul Beame, Armin Biere, and Jakob Nordström. Adding dual variables to algebraic reasoning for gate-level multiplier verification. In Proceedings of the 25th Design, Automation and Test in Europe Conference (DATE'22), 2022. Google Scholar
  23. Daniela Kaufmann and Armin Biere. Nullstellensatz-proofs for multiplier verification. In Computer Algebra in Scientific Computing - 22nd International Workshop, CASC 2020, Linz, Austria, September 14-18, 2020, Proceedings, pages 368-389, 2020. URL: https://doi.org/10.1007/978-3-030-60026-6_21.
  24. Daniela Kaufmann, Armin Biere, and Manuel Kauers. Verifying large multipliers by combining SAT and computer algebra. In 2019 Formal Methods in Computer Aided Design, FMCAD 2019, San Jose, CA, USA, October 22-25, 2019, pages 28-36, 2019. URL: https://doi.org/10.23919/FMCAD.2019.8894250.
  25. Daniela Kaufmann, Armin Biere, and Manuel Kauers. From DRUP to PAC and back. In 2020 Design, Automation & Test in Europe Conference & Exhibition, DATE 2020, Grenoble, France, March 9-13, 2020, pages 654-657, 2020. URL: https://doi.org/10.23919/DATE48585.2020.9116276.
  26. Javier Larrosa and Emma Rollon. Towards a better understanding of (partial weighted) maxsat proof systems. In Proc. of the 23nd Int. Conf. on Theory and Applications of Satisfiability Testing (SAT'20), pages 218-232, 2020. Google Scholar
  27. Javier Larrosa and Emma Rollón. Augmenting the power of (partial) MaxSAT resolution with extension. In Proc. of the 34th Nat. Conf. on Artificial Intelligence (AAAI'20), 2020. Google Scholar
  28. Knot Pipatsrisawat and Adnan Darwiche. On the power of clause-learning SAT solvers as resolution engines. Artif. Intell., 175(2):512-525, 2011. Google Scholar
  29. A.A. Razborov. Lower bounds for the polynomial calculus. Computational Complexity, 7(4):291-324, December 1998. Google Scholar
  30. Emma Rollon and Javier Larrosa. Proof complexity for the maximum satisfiability problem and its use in SAT refutations. J. Log. Comput., 32(7):1401-1435, 2022. Google Scholar
  31. Dmitry Sokolov. (Semi)Algebraic proofs over ± 1 variables. In Proceedings of the 52nd Annual ACM SIGACT Symposium on Theory of Computing. ACM, June 2020. Google Scholar
  32. Alasdair Urquhart. Hard examples for resolution. J. ACM, 34(1):209-219, January 1987. 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 Schloss Dagstuhl - LZI GmbH Imprint Privacy Contact