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.
Fiorino, G. (2025). New tableau characterizations for non-clausal regular MinSAT and MaxSAT problems. LOGIC JOURNAL OF THE IGPL, 33(6) [10.1093/jigpal/jzaf058].
New tableau characterizations for non-clausal regular MinSAT and MaxSAT problems
Fiorino G.
Primo
2025
Abstract
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.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
