Resolution and Domination: An Improved Exact MaxSAT Algorithm

Resolution and Domination: An Improved Exact MaxSAT Algorithm

Chao Xu, Wenjun Li, Yongjie Yang, Jianer Chen, Jianxin Wang

Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence
Main track. Pages 1191-1197. https://doi.org/10.24963/ijcai.2019/166

We study the Maximum Satisfiability problem (MaxSAT). Particularly, we derive a branching algorithm of running time O*(1.2989^m) for the MaxSAT problem, where m denotes the number of clauses in the given CNF formula. Our algorithm considerably improves the previous best result O*(1.3248^m) by Chen and Kanj [2004] published 15 years ago. For our purpose, we derive improved branching strategies for variables of degrees 3, 4, and 5. The worst case of our branching algorithm is at variables of degree 4 which occur twice both positively and negatively in the given CNF formula. To serve the branching rules and shrink the size of the CNF formula, we also propose a variety of reduction rules which can be exhaustively applied in polynomial time and, moreover, some of them solve a bottleneck of the previous best algorithm.
Keywords:
Constraints and SAT: MaxSAT, MinSAT
Agent-based and Multi-agent Systems: Algorithmic Game Theory
Constraints and SAT: SAT: Evaluation and Analysis