Solving weighted Maximum Satisfiability with Branch and Bound and clause learning
提出了首个集成子句学习的分支定界加权部分MaxSAT求解器WMaxCDCL，实验表明它能与顶尖求解器竞争，并补充了现有SAT方法，在2023年MaxSAT评估中赢得加权赛道。
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.