An Exact MaxSAT Algorithm: Further Observations and Further Improvements

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.