Combining Clause Learning and Branch and Bound for MaxSAT (Extended Abstract)

Chu-Min Li (1, 2, 3) , Zhenxing Xu (2) , Jordi Coll (4) , Felip Manyà (5) , Djamal Habet (4) , Kun He (2)

1 LIS - Laboratoire d'Informatique et des Systèmes (LIS) (Marseille, Toulon)
2 HUST - Huazhong University of Science and Technology [Wuhan]
3 MIS - Modélisation, Information et Systèmes - UR UPJV 4290
4 COALA - COntraintes, ALgorithmes et Applications
5 IIIA / CSIC - Artificial Intelligence Research Institute / Spanish Scientific Research Council

Branch and Bound (BnB) has been successfully used to solve many combinatorial optimization problems. However, BnB MaxSAT solvers perform poorly when solving real-world and academic optimization problems. They are only competitive for random and some crafted instances. Thus, it is a prevailing opinion in the community that BnB is not really useful for practical MaxSAT solving. We refute this opinion by presenting a new BnB MaxSAT solver, called MaxCDCL, which combines clause learning and an efficient bounding procedure. MaxCDCL is among the top 5 out of a total of 15 exact solvers that participated in the 2020 MaxSAT Evaluation, solving several instances that other solvers cannot solve. Furthermore, MaxCDCL solves the highest number of instances from different MaxSAT Evaluations when combined with the best existing solvers.

Domaines: Logique en informatique [cs.LO]

Chu-Min Li, Zhenxing Xu, Jordi Coll, Felip Manyà, Djamal Habet, et al.. Combining Clause Learning and Branch and Bound for MaxSAT (Extended Abstract). 31ST INTERNATIONAL JOINT CONFERENCE ON ARTIFICIAL INTELLIGENCE (IJCAI 2022), Jul 2022, Vienne, Austria. ⟨hal-03775319⟩