Tableau characterizations improve Maximum Satisfiability problem solutions in non-clausal formulas, suggesting efficiency gains.
In this paper we provide a new tableau characterization for the Weighted Partial Regular MinSat and Weighted Partial Regular MaxSat problems, which are, respectively, variants of the Minimum and Maximum Satisfiability problems. Our characterization has the advantage of constructing tableaux with fewer nodes compared to those built with known characterizations. We address the problems for the case of formulas in non-clausal form. We also discuss how our results can be adapted to the other versions of these problems.
No takes yet. Share an insight, caveat, or question.
Guido Fiorino (2025) studied this question.
Synapse has enriched 5 closely related papers on similar clinical questions. Consider them for comparative context: