Solving weighted Maximum Satisfiability with Branch and Bound and clause learning

Abstract

MaxSAT is a widely studied NP-hard optimization problem due to its broad applicability in modeling and solving diverse real-world optimization problems. Branch-and-Bound (BnB) MaxSAT solvers have proven efficient for solving random and crafted instances but have traditionally struggled to compete with SAT-based MaxSAT solvers on industrial instances. However, this changed with the introduction of the MaxCDCL algorithm, which successfully integrates clause learning into BnB to solve unweighted MaxSAT. Despite this progress, solving Weighted MaxSAT instances remained an open challenge. In this paper, we present WMaxCDCL, the first branch-and-bound (BnB) Weighted Partial MaxSAT solver with clause learning. We describe its algorithm and implementation in detail, experimentally evaluating key aspects that are critical to achieving strong performance. Our results demonstrate that WMaxCDCL can compete with the best state-of-the-art MaxSAT solvers and, more importantly, that this new solving approach complements the existing SAT-based MaxSAT methods, which have dominated the field until now. Notably, the combination of WMaxCDCL with other techniques won the weighted track of the 2023 MaxSAT Evaluation, which is the leading annual competition for MaxSAT solvers, affiliated with the International Conference on Theory and Applications of Satisfiability Testing

This work has been supported by grants PID2022-139835NB-C21 and PID2021-122274OB-I00 funded by MCIN/AEI/10.13039/501100011033 and by ERDF, EU, and by grant ANR-19-CHIA-0013-01 co-funded by the French Agence Nationale de la Recherche and the French electricity distribution network manager Enedis. F. Manyà was supported by mobility grant PRX23/00344 of the Ministerio de Ciencia, Innovación y Universidades, Spain. Open Access funding provided thanks to the CRUE-CSIC agreement with Elsevier