New article in Artificial Intelligence

The article Polynomial Calculus for Optimization just appeared in the journal Artificial Intelligence!

This is joint work with Maria Luisa Bonet (UPC) and Jordi Levy (IIIA-CSIC).

read the article

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 \(\mathbb N\) or \(\mathbb Z\). We show the soundness and completeness of these systems via an algorithmic procedure. Weighted Polynomial Calculus, with weights in \(\mathbb N\) and coefficients in \(\mathbb F_2\), is able to prove efficiently that Tseitin formulas on a connected graph are minimally unsatisfiable. Using weights in \(\mathbb Z\), it also proves efficiently that the Pigeonhole Principle is minimally unsatisfiable.

BibTeX

@article{BBL24-JAIR,
  author       = {Ilario Bonacina and
                  Maria Luisa Bonet and
                  Jordi Levy},
  title        = {Weighted, Circular and Semi-Algebraic Proofs},
  journal      = {J. Artif. Intell. Res.},
  volume       = {79},
  pages        = {447--482},
  year         = {2024},
  doi          = {10.1613/JAIR.1.15075}
}