A Complete Tableau Calculus for the Regular MaxSAT Problem
Jordi Coll, Chu-Min Li, Felip Manyà, Elifnaz Yangin · Frontiers in artificial intelligence and applications · 2023
We define a tableau calculus for solving the Maximum Satisfiability problem of regular propositional logic (Regular MaxSAT). Given a multiset of regular clauses Φ, 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 Φ is m, then the minimum number of unsatisfied clauses in Φ is m. We also prove that it is complete in the sense that if the minimum number of unsatisfied clauses in Φ is m, then the minimum number of contradictions among the branches of any completed tableau for Φ is m. Furthermore, we describe how to extend the proposed calculus to solve Regular MaxSAT in the case where we consider weighted formulas.