Logic seminar

Polynomial Calculus for MaxSAT

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 N or Z. We show the soundness and completeness of these systems 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.