An Exact MaxSAT Algorithm: Further Observations and Further Improvements

An Exact MaxSAT Algorithm: Further Observations and Further Improvements

Mingyu Xiao

Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence
Main Track. Pages 1887-1893. https://doi.org/10.24963/ijcai.2022/262

In the maximum satisfiability problem (MaxSAT), given a CNF formula with m clauses and n variables, we are asked to find an assignment of the variables to satisfy the maximum number of clauses. Chen and Kanj showed that this problem can be solved in O*(1.3248^m) time (DAM 2004) and the running time bound was improved to O*(1.2989^m) by Xu et al. (IJCAI 2019). In this paper, we further improve the result to O*(1.2886^m). By using some new reduction and branching techniques we can avoid several bottlenecks in previous algorithms and get the improvement on this important problem.
Keywords:
Constraint Satisfaction and Optimization: Satisfiabilty