A resolution calculus for MinSAT. (23rd October 2019)

• Record Type: Journal Article
• Authors: Li, Chu-Min; Xiao, Fan; Manyà, Felip
• Is Part Of: Logic journal of the IGPL. Volume 29:Number 1(2021)
• Page Start: 28
• Page End: 44
• Publication Date: 2019-10-23
• Subjects: Boolean optimization -- MinSAT -- signed MinSAT -- resolution -- calculus -- completeness; Logic, Symbolic and mathematical -- Periodicals; 511.3
• DOI: 10.1093/jigpal/jzz028
• Languages: English
• ISSNs: 1367-0751

Abstract

Abstract: The logical calculus for SAT are not valid for MaxSAT and MinSAT because they preserve satisfiability but not the number of unsatisfied clauses. To overcome this drawback, a MaxSAT resolution rule preserving the number of unsatisfied clauses was defined in the literature. This rule is complete for MaxSAT when it is applied following a certain strategy. In this paper we first prove that the MaxSAT resolution rule also provides a complete calculus for MinSAT if it is applied following the strategy proposed here. We then describe an exact variable elimination algorithm for MinSAT based on that rule. Finally, we show how the results for Boolean MinSAT can be extended to solve the MinSAT problem of the multiple-valued clausal forms known as signed conjunctive normal form formulas.