Clause tableaux for maximum and minimum satisfiability. (27th August 2019)

• Record Type: Journal Article
• Authors: Argelich, Josep; Li, Chu Min; Manyà, Felip; Soler, Joan Ramon
• Is Part Of: Logic journal of the IGPL. Volume 29:Number 1(2021)
• Page Start: 7
• Page End: 27
• Publication Date: 2019-08-27
• Subjects: Boolean optimization -- MaxSAT -- MinSAT -- tableaux -- calculus -- completeness; Logic, Symbolic and mathematical -- Periodicals; 511.3
• DOI: 10.1093/jigpal/jzz025
• Languages: English
• ISSNs: 1367-0751

Abstract

Abstract: The inference systems proposed for solving SAT are unsound for solving MaxSAT and MinSAT, because they preserve satisfiability but not the minimum and maximum number of clauses that can be falsified, respectively. To address this problem, we first define a clause tableau calculus for MaxSAT and prove its soundness and completeness. We then define a clause tableau calculus for MinSAT and also prove its soundness and completeness. Finally, we define a complete clause tableau calculus for solving both MaxSAT and MinSAT, in that the minimum number of generated empty clauses provides an optimal MaxSAT solution and the maximum number provides an optimal MinSAT solution.