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.
@InProceedings{bonacina_et_al:LIPIcs.SAT.2023.5, author = {Bonacina, Ilario and Bonet, Maria Luisa and Levy, Jordi}, title = {{Polynomial Calculus for MaxSAT}}, booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)}, pages = {5:1--5:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-286-0}, ISSN = {1868-8969}, year = {2023}, volume = {271}, editor = {Mahajan, Meena and Slivovsky, Friedrich}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.5}, URN = {urn:nbn:de:0030-drops-184670}, doi = {10.4230/LIPIcs.SAT.2023.5}, annote = {Keywords: Polynomial Calculus, MaxSAT, Proof systems, Algebraic reasoning} }
Feedback for Dagstuhl Publishing