A non-clausal tableau calculus for \textsc{MinSat} (Q2234795)
From MaRDI portal
 | This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use this page instead for the normal view: A non-clausal tableau calculus for \textsc{MinSat} |
scientific article
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | A non-clausal tableau calculus for \textsc{MinSat} |
scientific article |
Statements
A non-clausal tableau calculus for \textsc{MinSat} (English)
0 references
19 October 2021
0 references
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.
0 references
minimum satisfiability problem
0 references
tableaux
0 references
classical propositional logic
0 references
automatic theorem proving
0 references
