Weight-Aware Branch-and-Bound for Weighted Maximum Satisfiability
Weight-Aware Branch-and-Bound for Weighted Maximum Satisfiability
Jialu Zhang, Chu-Min Li, Sami Cherif, Shuolin Li
Proceedings of the Thirty-Fifth International Joint Conference on Artificial Intelligence
Main Track. Pages 2427-2436.
https://doi.org/10.24963/ijcai.2026/270
The Weighted Partial MaxSAT (WPMS) problem requires finding an assignment that satisfies all hard clauses while maximizing the total weight of satisfied soft clauses. From a computational perspective, WPMS is not merely an extension of the uniform-weight Partial MaxSAT (PMS); rather, it requires search strategies that actively exploit weight information to navigate the solution space. While state-of-the-art heuristic and SAT-based solvers have successfully integrated weight-aware mechanisms, Branch-and-Bound (BnB) solvers, notably WMaxCDCL, largely treat weight information passively during search and pruning. In this paper, we bridge this gap by introducing two novel weight-aware strategies into the BnB framework. Our methods integrate weight information directly into the preprocessing and lower-bound estimation. Experimental results demonstrate that these strategies significantly enhance the performance of WMaxCDCL, establishing a new state-of-the-art for exact WPMS solving.
Keywords:
Constraint Satisfaction and Optimization: Constraint optimization problems
Constraint Satisfaction and Optimization: Satisfiabilty
Constraint Satisfaction and Optimization: Solvers and tools
Search: Combinatorial search and optimisation
