Weight-Aware Branch-and-Bound for Weighted Maximum Satisfiability

Abstract

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.