Resolution and Domination: An Improved Exact MaxSAT Algorithm
Abstract
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.
Cite
Text
Xu et al. "Resolution and Domination: An Improved Exact MaxSAT Algorithm." International Joint Conference on Artificial Intelligence, 2019. doi:10.24963/IJCAI.2019/166Markdown
[Xu et al. "Resolution and Domination: An Improved Exact MaxSAT Algorithm." International Joint Conference on Artificial Intelligence, 2019.](https://mlanthology.org/ijcai/2019/xu2019ijcai-resolution/) doi:10.24963/IJCAI.2019/166BibTeX
@inproceedings{xu2019ijcai-resolution,
title = {{Resolution and Domination: An Improved Exact MaxSAT Algorithm}},
author = {Xu, Chao and Li, Wenjun and Yang, Yongjie and Chen, Jianer and Wang, Jianxin},
booktitle = {International Joint Conference on Artificial Intelligence},
year = {2019},
pages = {1191-1197},
doi = {10.24963/IJCAI.2019/166},
url = {https://mlanthology.org/ijcai/2019/xu2019ijcai-resolution/}
}