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

PDF BibTeX Video

Abstract

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
Welcome Future Conferences AI Journal Division IJCAI Proceedings Travel Grant Program IJCAI Awards