A non-clausal tableau calculus for \textsc{MinSat} (Q2234795)

The non-clausal MinSAT problem is to find an assignment which minimizes the number of satisfied formulas in a given multiset of propositional formulas. Basing on earlier work for non-clausal MaxSAT [\textit{C. M. Li} et al., Lect. Notes Comput. Sci. 11714, 58--73 (2019; Zbl 1435.68372)], the author introduces a tableau calculus for the non-clausal MinSAT problem. The calculus is proven sound and complete in the sense that the minimal number of occurrences of \(\top\) in the leaves of a completed tableau for a multiset \(\Gamma\) coincides with the minimum number of formulas satisfied in \(\Gamma\). The author also provides extensions of the tableau calculus to other variants of the MinSAT problem: partial MinSAT, weighted MinSAT and partial weighted MinSAT.