Document Open Access Logo

An Algebraic Approach to MaxCSP

Authors Ilario Bonacina , Jordi Levy

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.SAT.2025.6.pdf
  • Filesize: 0.83 MB
  • 17 pages
HTML5 Logo HTML (experimental)
LIPIcs.SAT.2025.6.html

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
  • Computing methodologies → Algebraic algorithms
  • Mathematics of computing → Solvers
Keywords
  • MaxCSP
  • Polynomial Calculus
  • MaxSAT

Metrics

Abstract

Recently, there have been some attempts to base SAT and MaxSAT solvers on calculi beyond Resolution, even trying to solve SAT using MaxSAT proof systems. One of these directions was to perform MaxSAT sound inferences using polynomials over finite fields, extending the proof system Polynomial Calculus, which is known to be more powerful than Resolution. 
In this work, we extend the use of the Polynomial Calculus for optimization, showing its completeness over many-valued variables. This allows using a more direct and efficient encoding of CSP problems (e.g., k-Coloring) and solving the maximization version of the problem on such encoding (e.g., Max-k-Coloring).

Cite As Get BibTex

Ilario Bonacina and Jordi Levy. An Algebraic Approach to MaxCSP. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 6:1-6:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.SAT.2025.6

Author Details

Ilario Bonacina
  • UPC Universitat Politècnica de Catalunya, Barcelona, Spain
Jordi Levy
  • IIIA, CSIC, Bellatera, Spain

Funding

This work was supported by the grant numbers PID2022-138506NB-C21, and PID2022-138506NB-C22 funded by AEI.

References

  1. Albert Atserias, Johannes Klaus Fichte, and Marc Thurley. Clause-learning algorithms with many restarts and bounded-width resolution. Journal of Artificial Intelligence Research, 40:353-373, 2011. URL: https://doi.org/10.1613/JAIR.3152.
  2. Ilario Bonacina, Maria Luisa Bonet, and Jordi Levy. Polynomial calculus for MaxSAT. In Proceedings of the 26th International Conference on Theory and Applications of Satisfiability Testing (SAT), 2023. URL: https://doi.org/10.4230/LIPIcs.SAT.2023.5.
  3. Ilario Bonacina, Maria Luisa Bonet, and Jordi Levy. Polynomial calculus for optimization. Artificial Intelligence, 337:104208, 2024. A preliminary version of this work appeared as [Ilario Bonacina et al., 2023]. URL: https://doi.org/10.1016/j.artint.2024.104208.
  4. Maria Luisa Bonet, Jordi Levy, and Felip Manyà. A complete calculus for Max-SAT. In Proceedings of the 9th International Conference on Theory and Applications of Satisfiability Testing, (SAT), volume 4121 of LNCS, pages 240-251. Springer, 2006. URL: https://doi.org/10.1007/11814948_24.
  5. Maria Luisa Bonet, Jordi Levy, and Felip Manyà. Resolution for Max-SAT. Artificial Intelligence, 171(8-9):606-618, 2007. URL: https://doi.org/10.1016/j.artint.2007.03.001.
  6. 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.
  7. B. Buchberger. A theoretical basis for the reduction of polynomials to canonical forms. ACM SIGSAM Bulletin, 10(3):19-29, August 1976. URL: https://doi.org/10.1145/1088216.1088219.
  8. 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. URL: https://doi.org/10.1006/JCSS.2000.1726.
  9. Matthew Clegg, Jeff Edmonds, and Russell Impagliazzo. Using the Groebner basis algorithm to find proofs of unsatisfiability. In Proceedings of the 28th Annual ACM Symposium on the Theory of Computing (STOC), pages 174-183, 1996. URL: https://doi.org/10.1145/237814.237860.
  10. 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. URL: https://doi.org/10.1016/J.JSC.2011.08.007.
  11. 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 (ISSAC), pages 133-140, 2015. URL: https://doi.org/10.1145/2755996.2756639.
  12. 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), pages 75-83, 2002. URL: https://doi.org/10.1145/780506.780516.
  13. 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), pages 1431-1436, 2022. URL: https://doi.org/10.23919/DATE54114.2022.9774587.
  14. Daniela Kaufmann and Armin Biere. Nullstellensatz-proofs for multiplier verification. In Proceedings of the 22nd International Workshop on Computer Algebra in Scientific Computing (CASC), pages 368-389, 2020. URL: https://doi.org/10.1007/978-3-030-60026-6_21.
  15. Daniela Kaufmann, Armin Biere, and Manuel Kauers. Verifying large multipliers by combining SAT and computer algebra. In Proceedings of the 19th Conference on Formal Methods in Computer Aided Design (FMCAD), pages 28-36, 2019. URL: https://doi.org/10.23919/FMCAD.2019.8894250.
  16. Daniela Kaufmann, Armin Biere, and Manuel Kauers. From DRUP to PAC and back. In Proceedigns of the 2020 Design, Automation & Test in Europe Conference & Exhibition (DATE), pages 654-657, 2020. URL: https://doi.org/10.23919/DATE48585.2020.9116276.
  17. Javier Larrosa and Federico Heras. Resolution in Max-SAT and its relation to local consistency in weighted CSPs. In Proceedings of the 19th International Joint Conference on Artificial Intelligence (IJCAI), pages 193-198, 2005. URL: http://ijcai.org/Proceedings/05/Papers/0360.pdf.
  18. Jesús A. De Loera, Jon Lee, Susan Margulies, and Shmuel Onn. Expressing combinatorial problems by systems of polynomial equations and Hilbert’s Nullstellensatz. Combinatorics, Probability and Computing, 18(4):551-582, 2009. URL: https://doi.org/10.1017/S0963548309009894.
  19. Sasank Mouli. Polynomial calculus sizes over the Boolean and Fourier bases are incomparable. In Proceedings of the 65th IEEE Annual Symposium on Foundations of Computer Science (FOCS), pages 790-796, 2024. URL: https://doi.org/10.1109/FOCS61266.2024.00055.
  20. Knot Pipatsrisawat and Adnan Darwiche. On the power of clause-learning SAT solvers as resolution engines. Artificial Intelligence, 175(2):512-525, 2011. URL: https://doi.org/10.1016/j.artint.2010.10.002.
  21. Toby Walsh. SAT v CSP. In Proceedings of the 6th International Conference on Principles and Practice of Constraint Programming (CP), volume 1894, pages 441-456, 2000. URL: https://doi.org/10.1007/3-540-45349-0_32.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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