A Tableau Calculus for Non-clausal Maximum Satisfiability

Chu Min Li (1) , Felip Manya (2) , Joan Ramon Soler

1 MIS - Modélisation, Information et Systèmes - UR UPJV 4290
2 IIIA / CSIC - Artificial Intelligence Research Institute / Spanish Scientific Research Council

We define a non-clausal MaxSAT tableau calculus. Given a multiset of propositional formulas phi, we prove that the calculus is sound in the sense that if the minimum number of contradictions derived among the branches of a completed tableau for phi is m, then the minimum number of unsatisfied formulas in phi is m. We also prove that it is complete in the sense that if the minimum number of unsatisfied formulas in phi is m, then the minimum number of contradictions among the branches of any completed tableau for phi is m. Moreover, we describe how to extend the proposed calculus to deal with hard and weighted soft formulas.

Domaines: Informatique [cs]

Chu Min Li, Felip Manya, Joan Ramon Soler. A Tableau Calculus for Non-clausal Maximum Satisfiability. AUTOMATED REASONING WITH ANALYTIC TABLEAUX AND RELATED METHODS, TABLEAUX 2019, Sep 2019, London, United Kingdom. pp.58-73, ⟨10.1007/978-3-030-29026-9\_4⟩. ⟨hal-03636422⟩