2026-07-20T05:27:54Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:23740 2025-11-12T12:59:58Z ddc:004 open_access

An Algebraic Approach to MaxCSP Bonacina, Ilario Levy, Jordi MaxCSP Polynomial Calculus MaxSAT 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). Schloss Dagstuhl – Leibniz-Zentrum für Informatik Ilario Bonacina and Jordi Levy 2025 Is Part Of LIPIcs, Volume 341, 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.SAT.2025.6 urn:nbn:de:0030-drops-237407 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.6 eng https://creativecommons.org/licenses/by/4.0/legalcode