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 Argelich | 1 | 190 | 18.95 |
Chu Min Li | 2 | 1194 | 85.65 |
Felip Manyà | 3 | 0 | 0.68 |
Joan Ramon Soler | 4 | 1 | 2.06 |