Title
Clause tableaux for maximum and minimum satisfiability
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...
Year
DOI
Venue
2021
10.1093/jigpal/jzz025
Logic Journal of the IGPL
Keywords
DocType
Volume
Boolean optimization,MaxSAT,MinSAT,tableaux,calculus,completeness
Journal
29
Issue
ISSN
Citations 
1
1367-0751
0
PageRank 
References 
Authors
0.34
0
4
Name
Order
Citations
PageRank
Josep Argelich119018.95
Chu Min Li2119485.65
Felip Manyà300.68
Joan Ramon Soler412.06