Tableaux for Maximum Satisfiability in Łukasiewicz Logic
Chu Min Li, Felip Manyà, Amanda Vidal · 2020
We define a tableau calculus for solving the MaxSAT problem of 3-valued Łukasiewicz logic, and prove its soundness and completeness. The calculus can be naturally extended to other finitely-valued logics. Our contributions establish the foundations of a generic problem solving paradigm for combinatorial optimization based on Łukasiewicz logic.