A Clause Tableau Calculus for MaxSAT

Chu-Min Li (1) , Felip Manya (1) , J.R. Soler

1 MIS - Modélisation, Information et Systèmes - UR UPJV 4290

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 that can be falsified in and an optimal assignment. We also describe how the algorithm can be extended to solve weighted MaxSAT and weighted partial MaxSAT.

Domaines: Intelligence artificielle [cs.AI]

Chu-Min Li, Felip Manya, J.R. Soler. A Clause Tableau Calculus for MaxSAT. IJCAI International Joint Conference on Artificial Intelligence, Jul 2016, New-York, United States. pp.766--772. ⟨hal-03702170⟩