A Clause Tableau Calculus for MinSAT

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 clause tableau calculus for MinSAT, and prove its soundness and completeness. The calculus allows one to compute the maximum number of clauses that can be falsified in a multiset of clauses by applying, finitely many times, tableaux-like inference rules. We also describe how the calculus can be extended to solve weighted MinSAT and weighted partial MinSAT.

Domaines: Informatique [cs]

Chu Min Li, Felip Manya, Joan Ramon Soler. A Clause Tableau Calculus for MinSAT. ARTIFICIAL INTELLIGENCE RESEARCH AND DEVELOPMENT, Oct 2016, Barcelona, Spain. pp.88-97, ⟨10.3233/978-1-61499-696-5-88⟩. ⟨hal-03636431⟩