Polynomial calculus for optimization

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 the systems MaxSAT-Resolution and weighted Resolution. Unlike such systems, weighted Polynomial Calculus manipulates polynomials with coefficients in a finite field and either weights in N or Z. We show the soundness and completeness of weighted Polynomial Calculus via an algorithmic procedure. Weighted Polynomial Calculus, with weights in N and coefficients in F 2, is able to prove efficiently that Tseitin formulas on a connected graph are minimally unsatisfiable. Using weights in Z, it also proves efficiently that the Pigeonhole Principle is minimally unsatisfiable.

Authors

• Ilario Bonacina a:1:{s:5:"en_US";s:18:"UPC Barcelona Tech";}
• Maria Luisa Bonet
• Jordi Levy IIIA - CSIC

Keywords

• MaxSAT
• SAT
• Proof systems
• Polynomial calculus
• Algebraic reasoning
• Proof complexity