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

DOI10.1016/J.IPL.2021.106167MaRDI QIDQ2234795zbMATH OpenOpenAlexWikidataFDO

Authors Guido Fiorino

Publication date 19 October 2021

Published in Information Processing Letters (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.ipl.2021.106167

zbMATH Keywords

automatic theorem provingclassical propositional logicminimum satisfiability problemtableaux

Mathematics Subject Classification ID

Classical propositional logic (03B05) Mechanization of proofs and logical operations (03B35) Computational aspects of satisfiability (68R07) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Review text

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.

Recommendations

• A tableau calculus for non-clausal maximum satisfiability
• New tableau characterizations for non-clausal \textsc{MaxSAT} problem
• A Complete Calculus for Max-SAT
• A tableau calculus for minimal model reasoning
• Resolution for Max-SAT

Cites work

• A resolution calculus for MinSAT
• A tableau calculus for non-clausal maximum satisfiability
• Clause tableaux for maximum and minimum satisfiability
• fCube: an efficient prover for intuitionistic propositional logic
• scientific article; zbMATH DE number 1189106 (Why is no real title available?)
• scientific article; zbMATH DE number 3274715 (Why is no real title available?)
• scientific article; zbMATH DE number 3300581 (Why is no real title available?)
• On approximation algorithms for the minimum satisfiability problem
• On reducing maximum independent set to minimum satisfiability
• Optimizing with minimum satisfiability
• SAT and SMT technology for many-valued logics
• Simplification Rules for Intuitionistic Propositional Tableaux
• The Minimum Satisfiability Problem

Cited in

(5)

• The possibilistic Horn non-clausal knowledge bases
• A tableau calculus for non-clausal maximum satisfiability
• Clause tableaux for maximum and minimum satisfiability
• A resolution calculus for MinSAT
• New tableau characterizations for non-clausal \textsc{MaxSAT} problem

Describes a project that uses

Uses Software

• fCube

This page was built for publication: A non-clausal tableau calculus for \textsc{MinSat}

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2234795)