A Tableau Calculus for Non-Clausal Regular MaxSAT
Jordi Coll, Chu Min Li, Felip Manyà, Elifnaz Yangin · 2024
We define a tableau calculus for solving the Maximum Satisfiability problem of regular propositional logic (Regular MaxSAT), and prove that the proposed calculus is sound and complete. Additionally, we describe how the calculus can be extended to handle hard and weighted soft formulas.