A Tableau Calculus for Non-clausal Maximum Satisfiability

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.