2026-08-06T04:24:49Z https://drops.dagstuhl.de/oai
oai:drops-oai.dagstuhl.de:18467 2024-03-06T11:01:58Z ddc:004 open_access
Polynomial Calculus for MaxSAT Bonacina, Ilario Bonet, Maria Luisa Levy, Jordi Polynomial Calculus MaxSAT Proof systems Algebraic reasoning 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. Schloss Dagstuhl – Leibniz-Zentrum fΓΌr Informatik Ilario Bonacina and Maria Luisa Bonet and Jordi Levy 2023 Is Part Of LIPIcs, Volume 271, 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.SAT.2023.5 urn:nbn:de:0030-drops-184670 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.5 eng https://creativecommons.org/licenses/by/4.0/legalcode