Abstract
A Clause Tableau Calculus for MaxSAT / 766
Chu-Min Li, Felip Manyà, Joan Ramon Soler
We define a clause tableau calculus for MaxSAT, prove its soundness and completeness, and describe a tableau-based algorithm for MaxSAT. Given a multiset of clauses C, the algorithm computes both the minimum number of clauses that can be falsified in C, and an optimal assignment. We also describe how the algorithm can be extended to solve weighted MaxSAT and weighted partial MaxSAT.