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

1 Introduction

Maximum Satisfiability (MaxSAT) is an optimization extension of the Satisfiability problem (SAT) [Bacchus et al., 2021], alongside other variants such as Minimum Satisfiability (MinSAT) [Li et al., 2010]. Generally, MaxSAT encompasses three main variants: Partial MaxSAT (PMS), which partitions clauses into hard and soft ones; Weighted MaxSAT, where each clause has a positive integer weight representing the cost for its violation; and Weighted Partial MaxSAT (WPMS), which combines hard clauses with weighted soft clauses. Thanks to the continuous efforts of the research community, MaxSAT has been successfully applied to solve a wide range of practical combinatorial optimization problems, such as scheduling [Demirovi´c et al., 2019; Cherif et al., 2024], maximum clique [Li and Quan, 2010], FPGA routing [Fu and Malik, 2006], and protein design [Allouche et al., 2014].

∗Corresponding authors.

Algorithms for the MaxSAT problem are generally categorized into exact (complete) and heuristic (incomplete) algorithms. Exact algorithms guarantee optimal solutions and certify optimality. Conversely, heuristic algorithms, while often competitive in finding high-quality solutions, do not provide optimality guarantees. This paper focuses on exact algorithms for WPMS, which are primarily categorized into SATbased and Branch-and-Bound (BnB) algorithms, although it can also be exactly solved using a tableau calculus [Li et al., 2016].

SAT-based algorithms reduce the MaxSAT problem to a sequence of SAT decision problems and solve them with a SAT oracle. The representative solvers include SAT4JMaxsat [Berre and Parrain, 2010], QMaxSAT [Koshimura et al., 2012], Open-WBO [Martins et al., 2014], Pacose [Paxian and Becker, 2024], MaxHS [Bacchus, 2022], RC2 [Ignatiev et al., 2019], EvalMaxSAT [Avellaneda, 2024], CGSS [Berg et al., 2023] and UwrMaxsat [Piotr´ow, 2020]. SATbased solvers demonstrate superior performance on industrial WPMS benchmarks, driven by the core-guided algorithm [Fu and Malik, 2006] and its subsequent refinements such as the stratification strategy [Ans´otegui et al., 2009; Ans´otegui et al., 2010]. More recently, [Pan et al., 2025] proposed an extended stratified strategy implemented in the CASHWMaxSAT solver, enabling it to win the first place in the weighted track of the MaxSAT Evaluation (MSE) 2024.

BnB algorithms maintain a global upper bound (UB), representing the cost of the best complete assignment found so far, and a lower bound (LB) of the cost for the current partial assignment. The search space is pruned whenever LB ≥ UB. Early BnB solvers, such as MaxSatz [Li et al., 2007], MiniMaxSat [Heras et al., 2008], Akmaxsat [Kuegel, 2010], and Ahmaxsat [Abram´e and Habet, 2014; Cherif et al., 2020], demonstrated strong performance on random benchmarks but struggled with industrial instances. To address this, the MaxCDCL algorithm [Li et al., 2021; Li et al., 2022] leverages conflict-driven clause learning (CDCL) to effectively capture the structure of industrial problems. Furthermore, its unlocking mechanism enhances the accuracy of LB estimation [Li et al., 2025]. Yet, despite these advancements, its weighted variant, WMaxCDCL [Coll et al., 2025], remains less competitive than state-of-the-art SAT-based solvers when solving WPMS instances.

While leading heuristic solvers and SAT-based solvers effectively leverage weight information (e.g., NuWLS [Chu et al., 2023] by considering soft clause weights in the variable scoring schema, and CASHWMaxSAT by stratification), modern BnB solvers have not yet fully exploited this potential. In this paper, we enhance the state-of-the-art BnB solver WMaxCDCL by integrating two novel weight-aware strategies. The first strategy employs a stratification strategy in the preprocessing phase, which significantly simplifies WPMS instances exhibiting hierarchical weight structures. The second strategy optimizes the lookahead framework of WMaxCDCL, resulting in a substantially better lower-bound estimation for dispersed WPMS instances. Experimental evaluations demonstrate that these strategies significantly improve the performance of WMaxCDCL, establishing a new stateof-the-art in exact WPMS solving.

The rest of the paper is organized as follows. Section 2 presents preliminary background. Section 3 details our proposed weight-aware strategies for MaxSAT BnB. Experimental results are presented in Section 4. Finally, we conclude and discuss future work in Section 5.

2 Preliminaries

2.1 Maximum Satisfiability

Let X be a set of Boolean variables. A literal l is either a variable x ∈ X or its negation ¬x. A clause c is a disjunction of literals, represented as a set of literals. A formula F in Conjunctive Normal Form (CNF) is a conjunction of clauses, also represented as a set of clauses. An assignment α maps variables to values in {1, 0}. It is complete if every variable is assigned a value. Otherwise, it is partial. A literal x (resp. ¬x) is satisfied if variable x is assigned 1 (resp. 0). It is falsified if x is assigned 0 (resp. 1). It is unassigned if x is unassigned. We represent α as the set of satisfied literals.

A clause c is satisfied if at least one of its literals is satisfied. An empty clause does not contain any literals and cannot be satisfied. A unit clause contains only one literal. Any clause can become unit by falsifying all its literals but one. Unit propagation (UP) is a procedure that iteratively propagates the only unassigned literal l of a unit clause by satisfying l and all clauses containing l, and removing ¬l from all other clauses, until all clauses are satisfied or an empty clause is produced, which is falsified. A formula F is satisfied if all its clauses are satisfied. The SAT problem thus consists in finding an assignment that satisfies a given CNF formula F .

As an optimization extension of SAT, Maximum Satisfiability (MaxSAT) aims to find a solution that satisfies the maximum number of clauses, making it significantly more challenging than standard SAT [Li and Many`a, 2021]. For the Weighted Partial MaxSAT (WPMS) problem, there are two sets of clauses: H, the set of hard clauses; and S, the set of soft clauses. Each soft clause c is associated with a positive integer w(c), called the weight of c, representing the cost of falsifying c. The cost of a complete assignment satisfying all hard clauses is the sum of the costs of the falsified soft clauses. The goal of WPMS is to find an assignment that satisfies all hard clauses while minimizing the total weight (or cost) of falsified soft clauses (or maximizing the weight of satisfied ones). When all soft clauses are assigned a uniform weight, WPMS reduces to Partial MaxSAT (PMS).

2.2 BooleanMultilevel Optimization

WPMS instances can be divided into three categories: crafted, random, and industrial. Crafted and random instances are primarily synthetic, typically exhibiting uniform or normal weight distributions. In contrast, industrial instances encode real-world problems and follow a characteristic power-law distribution [Ans´otegui et al., 2012], where a small number of soft clauses have extremely high weights. Furthermore, some industrial instances may display clear stratification, formalized as Boolean Multilevel Optimization (BMO) in [Marques-Silva et al., 2011]. Equation (1) defines a BMO instance, where m denotes the number of distinct weights in the instance, wj represents the j th weight in the decreasing weight sequence, and |Ci| means the number of clauses with weight wi. This definition guarantees that wj exceeds the sum of weights of all clauses with a lower weight, forcing higher-weight clauses to be satisfied first.

2.3 Lookahead Framework inWMaxCDCL

WMaxCDCL removes each soft clause c, after introducing a fresh soft literal l with weight w(l) = w(c), and forcing the equivalence l ↔ c by inserting a set of hard clauses into H. The computation of a lower bound is based on detecting disjoint local cores, where a local core is a subset of soft literals that cannot all be satisfied without falsifying a hard clause under the current partial assignment α. Each soft literal l in a core κ has a weight locked in the core, denoted as wlock(l, κ). By definition, wlock(l, κ) = 0 if l /∈ κ. Each core κ is associated with a weight w(κ), such that ∑¬l∈ext(α) wlock(l, κ) ≥ w(κ) for any complete extension ext(α) of α. Let K be the set of all cores. The lower bound LB under α is equal to ∑κ∈K w(κ), subject to the condition ∑κ∈K wlock(l, κ) ≤ w(l) for any l. We use rw(l) = w(l) - ∑κ∈K wlock(l, κ) to denote the remaining weight of l not locked in any core. Note that the condition ∑κ∈K wlock(l, κ) ≤ w(l) is required to ensure the soundness of LB.

If LB ≥ UB, where UB is the cost of the best solution found so far, the current branch can safely be pruned. In earlier versions of WMaxCDCL, only soft literals l such that rw(l) > 0 can be used to detect a new core. When a core κ = {l1, . . . , lk} is detected, w(κ) = minl∈κrw(l), wlock(li, κ) = w(κ) and rw(li) is updated to rw(li) - w(κ) for 1 ≤ i ≤ k. In this way, the condition ∑κ∈K wlock(l, κ) ≤ w(l) is naturally ensured [Coll et al., 2025]. However, in this case, we necessarily have w(κ) = wlock(l, κ) for any core κ and any l ∈ κ, limiting the capacity of WMaxCDCL to compute a tight lower bound.

In the last version of WMaxCDCL [Li et al., 2025], an unlocking mechanism is introduced, allowing the reuse of the weight of literals locked in previous cores to detect a new core under some conditions. Consequently, a core κ with w(κ) > wlock(l, κ) for some l ∈ κ can be detected. Example 1 shows

Algorithm 1: Lookahead in WMaxCDCL

Input: H: hard clauses, S: soft literals, α: partial assignment, UB: upper bound. Output: LB: estimated lower bound, K: local cores. 1 LB← cost(α); 2 α′ ←α; A← {}; 3 S′ ← {l | l ∈ S, l /∈ α, ¬l /∈ α}; 4 while LB < UB and S′ ̸= ∅ do 5 l ← PickSoftLiteral(S′ ) ; 6 S′ ←S′ \ {l}; 7 A←A∪ {l}; 8 α′ ←α∪ {l} ; 9 (fc, fs, α′ ) ← UPforLA(H, K, α′ , l) ; 10 if fc ̸= ⊥ or fs ̸= ⊥ then 11 κ ← AnalyzeImplicationGraph(f c, f s); 12 K ← K ∪ {κ} ; 13 LB←LB+w(κ) ; 14 foreach l ∈ κ do 15 rw(l) ← rw(l) - wlock(l, κ) ; 16 S′ ←S′ ∪A \ {l | l ∈ κ, rw(l) = 0} ; 17 A ← {}; α′ ← α ; 18 return (LB,K);

such a core taken from [Li et al., 2025]. With the unlocking mechanism and the reuse of the weight locked in previous cores, a tighter lower bound can be computed for WPMS.

Example 1. A core κ={l1(3), l2(3), l3(3), l4(1), l5(1)} is given in [Li et al., 2025], where each integer between brackets denotes the weight of the preceding literal locked in the core, and w(κ) = 4.

A local core under α is usually detected by propagating a sequence of soft literals until a soft literal becomes falsified or a hard clause is falsified. Algorithm 1 outlines the current lookahead framework procedure employed in WMaxCDCL, omitting details not relevant to this study.

Based on the partial assignment α and the set of unassigned soft literals S′ , the algorithm actively propagates unassigned soft literals from S′ one by one as assumptions (Lines 59). Upon the falsification of a hard clause fc or a soft literal fs (Line 10), conflict analysis identifies the set δ of actively propagated soft literals contributing to the falsification and returns a local core κ, defined as δ in the former case and δ ∪ {fs} in the latter (Line 11). Then, the lower bound LB is increased by w(κ) (Line 13). Accordingly, the remaining weight of each soft literal l ∈ κ is decreased by wlock(l, κ) (Line 15). To prepare for the next local core detection, the set of picked soft literals (recorded in A) is restored to the candidate set S′ , whereas those with zero remaining weight are removed (Line 16). Finally, the algorithm restores α (Line 17).

3 Weight-Aware BnB forWPMS

Existing Branch and Bound (BnB) solvers for MaxSAT often fail to actively exploit the weight information carried by soft clauses, limiting their effectiveness on weighted instances. To address this limitation, we introduce two weight-aware mechanisms in MaxSAT BnB, namely a stratified hardening preprocessing strategy and an in-processing weight-aware lookahead framework to estimate the cost LB of the current partial assignment in state-of-the-art BnB.

3.1 Motivation

We characterize the weight structure of WPMS benchmarks from the MaxSAT Evaluations 1 (MSEs) 2022 to 2024 and find that a significant number of instances exhibit a clear hierarchical structure, as illustrated in Figure 1 in both concentrated high-weight and heavy-tailed distributions. BnB solvers such as WMaxCDCL do not exploit this hierarchical structure, which is the first motivation of our study.

Furthermore, we measure the weight distributions of the instances from MSEs 2022 to 2024, using the number of distinct weights and the Coefficient of Variation (CV ) computed as stdDeviation/meanWeight. A low CV suggests a concentrated distribution, while a high CV signifies substantial diversity; notably, a distribution with CV > 1.0 is typically regarded as highly dispersed. As illustrated in Figure 2, over 30% of the WPMS instances display a highly dispersed weight distribution, a trend particularly evident in MSE23, where nearly 40% of the instances showed this feature. Specifically, across the entire MSE 2022-2024 benchmark set, 301 instances (17%) satisfy the BMO condition (Equation 1), comprising 80 instances (13%) in MSE22, 118 (21%) in MSE23, and 103 (18%) in MSE24.

Then, we stress out the inefficiency of the existing lookahead framework in dealing with instances exhibiting such highly dispersed weights. Specifically, classical lookahead

1 https://maxsat-evaluations.github.io

Input: H: hard clauses; S: soft clauses. 1 if not IsBMOInst(S) then 2 return MaxSATSolver(H, S); 3 wmax ←∞; state ←SAT; 4 while S ̸= ∅ and state = SAT do 5 wmax ←max{w(c) | c ⊆ S,w(c) < wmax} ; 6 hardens ← {c | c ⊆ S,w(c) = wmax}; 7 H ←H ∪ hardens; 8 state ←SATsolver(H) ; 9 if state = SAT then 10 S ← S \ hardens ; 11 else 12 H ← H \ hardens ; 13 returnMaxSATsolver(H, S) ;

does not prioritize soft literals based on their weights, potentially mixing literals of significantly disparate magnitudes into a local core. Since the weight of a local core is constrained by the minimum weight of the soft literals within it, this leads to the generation of low-weight local cores, diminishing the efficiency of the lookahead framework.

This limitation is concretely illustrated in Example 2, where the lookahead procedure needs to detect two local cores to meet the pruning condition. This is because the first detected local core κ1 contains the soft literal l3 with weight w(l3) = 1, which makes κ1 low-weight and reduces the lookahead efficiency.

Example 2. Consider soft literals S = {l1, l2, l3} with weights w(l1) = w(l2) = 10, w(l3) = 1, UB = 10, and H = (x1 ∨ ¬l1 ∨ ¬l3) ∧ (¬l1 ∨ ¬l2 ∨ l3). The remaining weight rw(l) of each literal l is initialized to its weight w(l). Given the partial assignment α = {¬x1}, we illustrate a typical case of the lookahead procedure:

1. Propagating l1 implies ¬l3, yielding a local core κ1 = {l1, l3} with weight w(κ1) = min(rw(l1), rw(l3)) = 1. The remaining weights are updated to rw(l1) ← 9, rw(l3) ← 0 and LB = 1.
2. Propagating l1 makes l3 falsified and the second hard clause unit, making l2 = 0. This identifies a local core κ2 = {l1, l2} with weight w(κ2) = min(rw(l1), rw(l2)) = 9. Subsequently, the remaining weights are updated to rw(l1) ← 0 and rw(l2) ← 1, and LB = 10. Finally, the lookahead terminates since LB ≥ UB.

3.2 Stratified Hardening Strategy

In this subsection, we propose a preprocessing strategy for BnB solvers to exploit the hierarchical structure in WPMS instances, whenever it exists, inspired by stratification techniques in core-guided algorithms. The strategy consists of hardening high-weight soft clauses to simplify BMO instances. It is implemented in Algorithm 2.

The algorithm first checks whether the weight distribution satisfies the BMO condition, as defined in Equation (1), via

Algorithm 3: UPforLA (Weight-Aware Version)

Input: H: hard clauses, K: local cores, α: partial assignment, l: a soft literal to propagate. Output: fc: a falsified clause or ⊥, fs: a falsified soft literal or ⊥, α: extended partial assignment. 1 Q← {l}; Γ← ∅; Φ← ∅; 2 while Q ̸= ∅ do 3 p ← Pop(Q); 4 for each clause c ∈ H containing ¬p do 5 if c is falsified under α then 6 return (c, ⊥, α) ; 7 else if c is unit under α then 8 Let l be the sole unassigned literal in c; 9 α ← α ∪ {l} ; 10 if ¬l is a soft literal then 11 if rw(¬l) > 0 then 12 Γ ← Γ ∪ {¬l} ; 13 else 14 Φ←Φ∪ {κ | κ ∈ K, κ is unlocked} ; 15 Push(Q, l);

16 fs ←WA-Select(Γ,Φ) ; 17 return (⊥, fs, α);

the IsBMOInst procedure (Line 1). For confirmed BMO instances, it iteratively hardens soft clauses in descending order of weights and invokes a SAT oracle to check the satisfiability of the extended hard clause set H (Lines 5-8). If H remains satisfiable, the hardened clauses are removed from the soft clause set S (Line 10). Conversely, if H becomes unsatisfiable, the algorithm restores consistency by discarding the clauses hardened in the current iteration and terminates the hardening phase (Line 12). Finally, the simplified formula (H, S) is passed to the MaxSAT solver (Line 13).

The main difference between our algorithm and the stratified approach in core-guided MaxSAT solvers is that the latter is applied throughout the iterative solving process, whereas our approach is restricted to the preprocessing phase. Although the preprocessing procedure halts when unsatisfiability arises, which may restrict the extent of reduction, experimental results indicate that it is particularly effective for WMaxCDCL, notably boosting its performance.

3.3 Weight-Aware Lookahead

In this subsection, we address the limitations of existing lookahead procedures in BnB for WPMS, which often fail to identify high-quality cores, because they do not actively exploit weight information during lower bound computation. Specifically, note that most cores κ = {l1, . . . , lk} are obtained by actively propagating l1, . . . , lk-1 as assumptions, falsifying lk. However, as indicated in Example 2, the weight of a core κ = {l1, . . . , lk} depends on the remaining weight of each soft literal in κ. The existing lookahead procedures do not actively search for high remaining weights. In this subsection, we introduce a weight-aware approach to address the actively propagated soft literals and the falsified literals separately. The purpose is to overcome the limitations of the existing lookahead framework by detecting high-weight cores to increase LB quickly.

To address the actively propagated soft literals, we introduce a new soft literal selection heuristic in module PickSoftLiteral called in Line 5 of Algorithm 1. In the baseline approach, the selection of the soft literals to propagate relies primarily on their recent activity in conflicts, neglecting the significance of their associated weights. In contrast, our heuristic gives precedence to soft literals with higher remaining weights, employing activity scores only to distinguish between candidates of equal weight.

To address the falsified soft literals, we modify the unit propagation process in module UPforLA (Algorithm 3) called in Line 9 of Algorithm 1. In the baseline version of UPforLA, unit propagation aborts as soon as a soft literal is falsified (fs) (Line 10). In contrast, our proposed approach continues propagation until a hard clause is falsified (Line 6) or there are no more unit clauses to propagate (i.e., propagation queue Q becomes empty), so that several soft literals can be falsified.

Example 3. Considering the same input as in Example 2, we illustrate the execution trace of the modified lookahead:

Propagating l1 implies ¬l3. In Example 2, the propagation stopped and a core κ1={l1, l3} with w(κ1)=1 is identified. However, in our new strategy, we do not stop unit propagation, but continue falsifying l2. Then, we have two falsified soft literals {l2, l3}. Since rw(l2)>rw(l3), we choose l2 to identify the local core κ2={l1, l2} with a weight of w(κ2)=10, increasing the lower bound to LB=10 by itself. So, only one local core is sufficient to prune the current branch, because we already have LB≥UB.

Example 3 illustrates a simple situation in which all falsified literals have positive remaining weights, and we just need to choose the one with the highest remaining weight to form a high-weight core. However, in the latest version of WMaxCDCL (version of MSE 2024), a sophisticated unlocking mechanism is implemented to reuse the soft literals already locked in cores. By the unlocking mechanism, a core κ is unlocked if the total locked weights of the falsified literals in κ is equal to or greater than w(κ) during unit propagation, namely, ∑¬l∈α wlock(l, κ) ≥ w(κ), where α is the current partial assignment. It is shown in [Li et al., 2025] that all unassigned literals in an unlocked core, together with their weights locked in this core, can be used to detect a new core. Indeed, the contribution of a core κ to LB is w(κ). The falsification of an unassigned literal when or after κ is unlocked can produce an additional contribution to LB w.r.t. w(κ). We need to choose a literal falsified when or after κ is unlocked for detecting a high-weight core.

Example 4. Let κ1={l1(4), l2(4), l3(6), l4(3), l5(3)} with w(κ1)=7, and each integer between brackets denoting the weight of the preceding literal locked in κ1 (e.g., wlock(l3, κ1)=6), the remaining weight rw(l)=0 for each l ∈ κ1, and UB=10. Since LB=w(κ1)=7. We need to detect new cores to prune the current branch. Let l6 be a soft literal with rw(l6)=3. Propagating l6 falsifies successively l1, l2 and l3.

The two combinations (l1=0, l2=0) and (l1=0, l3=0) both unlock κ1. The current version of WMaxCDCL will use (l1=0, l2=0) to derive a new core, because l2 is the first soft literal unlocking κ1, and the new core is κ2={l1(4), l2(4), l3(6), l4(3), l5(3), l6(1)} with w(κ2)=8, including κ1. To see this, we distinguish two branches: l6=0 and l6=1. For any complete extension of α including l6=0, the total minimum falsified weight is w(κ1) + rw(l6)=10. If l6=1, the total minimum falsified weight using l1 = 0 and l2 = 0 is wlock(l1, κ1) + wlock(l2, κ1) = 8. Since w(κ2) is the minimum among the two branches, w(κ2) = min(10, 8) = 8. So, LB=w(κ2)=8 < UB, which is not enough to prune the current branch.

Note that if rw(l6) were 1, the total minimum falsified weight for branch l6=1 would be reduced to w(κ1) + rw(l6)=8, but w(κ2) would always be 8. So, we only need to lock weight 1 of l6 in κ2.

However, we can also choose (l1=0, l3=0) and derive a new core κ3={l1(4), l2(4), l3(6), l4(3), l5(3), l6(3)} with w(κ3)=10, increasing LB to 10 and allowing us to prune the current branch. In fact, in branch l6=0, the total minimum falsified weight is always w(κ1) + rw(l6)=10, while in branch l6=1, the total minimum falsified weight using l1=0 and l3=0 is wlock(l1, κ1)+w(l3, κ1)=4+6=10. Since w(κ3) is the minimum among the two branches, we have w(κ3)=min(10, 10)=10.

Note that if rw(l6) were smaller than 3, the total minimum falsified weight would be smaller than 10 for branch l6 = 0. So, we need to lock weight 3 of l6 in κ3 to make w(κ3)=10.

Note that we can use the combination (l1=0, l2=0, l3=0) and obtain a new core κ4 with w(κ4) = 10. The drawback is that, in a more realistic situation, the reasons falsifying l2 and the reasons falsifying l3 can be different. If we take both l2 and l3, we need to take all these reasons into account to form the new core, which generally results in a larger new core and reduces the efficiency in detecting the next new cores.

Also note that if l4 is falsified after l1, we cannot take the combination (l1, l4), although it unlocks κ1, because this combination does not give any additional falsified weight w.r.t. w(κ1). In fact, wlock(l1, κ1)+wlock(l4, κ1)-w(κ1)=0.

In the general case, we define the notion of additional falsified weight, aw for short, w.r.t. existing cores, during unit propagation for detecting a new core. If the falsified literal l has a positive remaining weight rw(l), then aw(l) = rw(l). Otherwise, l has weight locked in existing cores. The additional falsified weight of l depends on its falsification time and the unlocking time of the cores it belongs to.

The falsification time of l during a core detection is defined to be the smallest cardinality of α after α receives ¬l (See Line 9 in Algorithm 3), denoted as falsifyTime(l), or falsifyT(l) for short. The unlocking time of an existing core κ is defined to be the first falsifyTime(l) making ∑¬l∈α wlock(l, κ) ≥ w(κ), denoted as unlockTime(κ), or unlockT(κ) for short. By definition, unlockTime(κ) = ∞ if κ is not unlocked.

The computation of additional falsified weight of l w.r.t. κ,

Algorithm 4: WA-Select

Input: Γ: falsified soft literals, Φ: unlocked cores. Output: fs: a falsified soft literal or ⊥. 1 fs ←⊥; wmax ← 0; 2 for each l ∈ Γ do 3 if rw(l) > wmax then 4 fs ← l; wmax ← rw(l); 5 for each κ ∈ Φ do 6 for each l ∈ κ s.t. falsifyT(l) > unlockT (Case (1)) or falsifyT(l) ≥ unlockT (Case (2)) do 7 Compute aw(l, κ) according to Case (1) or Case (2) 8 if aw(l, κ) > wmax then 9 fs ← l; 10 wmax ← aw(l, κ); 11 return fs;

denoted as aw(l, κ), depends on two cases:

In Case (1), aw(l, κ) = wlock(l, κ) for each l falsified af-

ter κ is unlocked (i.e., such that falsifyT(l) > unlockT(κ)).

In Case (2), we define

for base unlocking weight of κ. Then, the additional falsified weight of each soft literal l falsified in κ such that falsifyT(l) ≥ unlockT(κ) is computed using the base unlocking weight as follows:

Example 5. Consider the same core κ1 = {l1(4), l2(4), l3(6), l4(3), l5(3)} in Example 4, with w(κ1) = 7, the remaining weight rw(l) = 0 for each l ∈ κ1, and α = ∅. Propagating a literal l6 falsifies successively l1, l2 and l3, updating α to {l6, ¬l1, ¬l2, ¬l3}.

We have falsifyT(l1)=2, falsifyT(l2)=3, falsifyT(l3)=4, unlockT(κ1) = falsifyT(l2) = 3. We are in Case (2), because w(κ1) < wlock(l1, κ1) + wlock(l2, κ1). Then, buw(κ1) = wlock(l1, κ1) = 4, aw(l2, κ1) = wlock(l2, κ1) + buw(κ1) - w(κ1) = 1, aw(l3, κ1) = wlock(l3, κ1) + buw(κ1) - w(κ1) = 3.

Since aw(l3, κ1) > aw(l2, κ1), we should choose the combination (l1 = 0, l3 = 0) to form the new core.

We now present Algorithm 3 and Algorithm 4, whose purpose is to select the greatest additional falsified weight to form a high-weight core. In Algorithm 3, if a hard clause is falsified, it is simply returned, because the additional falsified weight is considered to be ∞ in this case. Otherwise, every falsified soft literal with positive remaining weight is collected into Γ (Line 12), and every unlocked core is collected into Φ (Line 14). Then, Algorithm 4 is called to select the falsified literal with the greatest additional falsified weight, done via lines 2-4 which select the falsified soft literal with the greatest remaining weight from Γ, and lines 5-10 which select the falsified soft literal with the greatest additional falsified weight w.r.t. an unlocked core from Φ. The algorithm returns the falsified soft literal with the global maximum additional falsified weight.

4 Experimental Results

In this section, we evaluate the proposed approach against state-of-the-art MaxSAT solvers, and the different strategies in the approach. We implemented our methods on top of the MaxSAT Evaluation 2024 version of WMaxCDCL [Li et al., 2024], which integrates the unlocking mechanism in [Li et al., 2025]. The code was compiled using GCC 12.2.0 with -O3 optimization and static linking.

Proposed variants. To assess our contributions, we evaluated the following variants of WMaxCDCL (WM), with source code available in the supplementary material 2 :

• WM-S: Incorporates the stratified hardening strategy described in Section 3.2.
• WM-WA: Implements the weight-aware lookahead framework detailed in Section 3.3.
• WM-WA-: An ablation version of WM-WA that modifies Algorithm 4, by selecting all falsified literals in a core κ ∈ Φ and uses aw = ∑l∈κ∧¬l∈α wlock(l, κ) - w(κ), e.g., it uses the combination {l1 = 0, l2 = 0, l3 = 0} in Example 4, instead of {l1 = 0, l2 = 0} or {l1 = 0, l3 = 0}.

2 https://github.com/zjl9959/IJCAI26.git

• WM-SWA: Combines both the stratified hardening strategy and the weight-aware lookahead framework.

Compared solvers. We downloaded state-of-the-art solvers participating in the three most recent MaxSAT Evaluations (MSE 2022-2024). To ensure a fair comparison, we excluded portfolio-based approaches and focused on six independent solvers: Open-WBO [Martins et al., 2023], Pacose [Paxian and Becker, 2024], CGSS2 [Ihalainen et al., 2024], UwrMaxSAT [Piotr´ow, 2024], EvalMaxSAT [Avellaneda, 2024], and CASHWMaxSAT [Pan et al., 2024]. Notably, CASHWMaxSAT, UwrMaxSAT, and EvalMaxSAT ranked as the top three solvers in the weighted track of MSE 2024. Each solver was configured using the settings that yielded the best performance in its most recent competition participation.

Benchmarks. For the empirical evaluation, we first conduct an in-depth analysis of the WPMS instances fromMSE 2022, 2023, and 2024, followed by a comprehensive robustness check across the extended MSE 2019-2024 benchmarks. The dataset spans diverse domains (e.g., combinatorial optimization, AI, and bioinformatics) to ensure a representative and robust evaluation.

Experimental environment. The experiments were conducted on the MatriCS platform 3 , equipped with AMD EPYC 7502 processors (2.5 GHz) running Linux. Each instance was restricted to a single CPU core and 31 GB of RAM, with a timeout of 5000 seconds. The 5000s limit was chosen to calibrate our evaluation to the MSE24 performance benchmarks, as our hardware is slower than the official MSE infrastructure.

4.1 Overall Evaluation

Table 1 presents the results of the proposed variants and stateof-the-art solvers on the MSE 2022-2024 WPMS benchmarks. The evaluation metrics include the number of solved instances (#sol) and the Penalized Average Runtime with a factor of 2 (PAR2) [Hutter et al., 2009], which was first used in MSE 2024. The data indicate that while the baseline WMaxCDCL remains competitive on MSE22, it lags behind other state-of-the-art solvers on MSE23 and MSE24. By leveraging weight distribution information, our proposed variant, WM-SWA, effectively addresses this shortcoming. Across the combined MSE22-24 benchmarks, WM-SWA solves a total of 1291 instances-an improvement of 73 instances over the baseline-matching the performance of the current leading solver, CASHWMaxSAT. Notably, WMSWA solves the most instances (439) in MSE24, surpassing all other competitors.

3 https://www.matrics.u-picardie.fr/

Figure 3 presents the number of solved instances over time, demonstrating that WM-SWA performs on par with CASHWMaxSAT while outperforming all other solvers. Notably, the solver rankings remain stable within the [1000, 5000] seconds interval; the only exception is EvalMaxSAT, which stabilizes after 3933 seconds without changing the ranking of WM-SWA. Ultimately, these results demonstrate that our proposed weight-aware strategies enable the BnB solver to achieve state-of-the-art performance on WPMS solving.

4.2 Evaluation of Strategies

We analyzed the performance of the proposed variants compared to WMaxCDCL. As summarized in Table 2, all proposed variants enhance the overall performance of WMaxCDCL. Specifically, WM-S solves an additional 23 and 24 instances in MSE23 and MSE24, respectively. Meanwhile, WM-WA yields improvements across all years, solving 2, 15, and 9 more instances in MSE22, MSE23, and MSE24. Furthermore, the performance gain of WM-SWA reflects the cumulative benefits of WM-S and WM-WA, indicating that these two strategies are synergistic and complementary.

It is important to note that the improvement on MSE22 is relatively limited compared to the substantial gains on MSE23 and MSE24, which is mainly attributed to two factors: (1) Increased Complexity: MSE22 instances are harder (69.5% solved by the best solver) compared to MSE23/24 (≈ 77%) (Table 1); (2) Structural Mismatch: MSE22 contains significantly fewer BMO instances (Section 3.1), which limits the utility of the stratified hardening strategy. Consequently, as shown in Table 2, weight-aware lookahead emerges as the primary performance driver on MSE22. This enables WMWA to outperform other solvers, confirming that lookahead mechanisms are more critical than stratified hardening for harder, less-structured instances.

As illustrated in Figure 4, WM-SWA effectively reduces solving times across the majority of instances when compared to WMaxCDCL. Notably, this reduction in CPU time is particularly pronounced for instances featuring the BMO structure (Equation 1). To investigate this further, we revisit the three representative weight distribution patterns presented in Figure 1. We observe that WM-S excels on instances with concentrated high-weight and heavy-tailed distributionsmany of which satisfy the BMO condition. For instance, the frb (CV < 0.3) and drmx-cryptogen (0.3 < CV < 0.6) families clearly exemplify this behavior. Meanwhile, WM-WA demonstrates superior efficiency on instances exhibiting more random weight patterns, such as the judgement-aggregation family (0.4 < CV < 1.3). Ultimately, these findings suggest that the performance of the proposed strategies is governed by the interaction between the BMO property and weight diversity, rather than dispersion alone.

Additionally, the ablated variant WM-WA- solves 3 fewer instances than WM-WA in both MSE22 and MSE23. This demonstrates that the literal selection strategy proposed in Algorithm 4 outperforms the naive strategy of selecting all falsified soft literals within the core. As discussed in Example 4, although the naive strategy can select a core with a larger additional falsified weight, it also uses more literals to form the new core.

Finally, Table 3 offers insights into the performance of WM-WA compared to WMaxCDCL. The data indicates that for each benchmark, WM-WA detects cores with higher weights and smaller sizes, and requires fewer cores per lookahead to prune the search. Aggregated across the complete benchmark set of MSE 2022-2024, the changes are also substantial: core weight (+22.04%), core size (-1.15%), and cores per lookahead (-8.46%). This confirms that our strategy successfully guides the lookahead search to identify highweight cores, thereby improving pruning efficiency.

4.3 Extended Evaluation

To validate robustness across a broader scope, we extend our evaluation to a six-year dataset (MSE 2019-2024). To avoid duplication, we excluded instances from the evaluation of year 2000 + k (25 > k > 19) if they appeared in years 2019, . . ., 2000+k-1. The extended dataset comprises 2223 weighted partial MaxSAT instances.

We compare WM-SWA against leading MaxSAT solvers recognized in recent MaxSAT Evaluations (Table 1). Specifically, across the comprehensive MSE 2019-2024 benchmarks, WM-SWA solves 1661 instances, successfully outperforming CASHWMaxSAT (1655), EvalMaxSAT (1631), CGSS2 (1626), UwrMaxSAT (1611), and WMaxCDCL (1590). As shown in Figure 5, WM-SWA demonstrates superior performance compared to other leading MaxSAT solvers across this six-year dataset. These results confirm that our refinements on WMaxCDCL effectively bridge the performance gap for weighted instances, establishing a consistent and significant improvement over existing independent SATbased WPMS solvers.

5 Conclusion

In this paper, we introduced two weight-aware strategies designed to enhance Branch-and-Bound (BnB) MaxSAT solvers for WPMS. The first approach implements a hardening mechanism for high-weight soft clauses within a BMO structure. The second approach addresses fundamental limitations in current lookahead frameworks by introducing the concept of additional falsified weight. This metric, calculated based on literal falsification and core unlock times, enables the solver to prioritize soft literals that lead to the detection of high-weight, small-size local cores.

We integrated these approaches into WMaxCDCL, a stateof-the-art BnB solver. Our experimental evaluation on datasets from MSE 2022-2024 demonstrates that while each approach independently improves performance, their combination is particularly synergistic, allowing WMaxCDCL to solve 73 additional instances. These results effectively bridge the performance gap between BnB and SAT-based solvers for WPMS.

For future work, we intend to develop an efficient weightaware further-lookahead mechanism, aiming to break selected low-weight or large-size cores when the standard lookahead fails to increase the lower bound (LB<UB), thereby facilitating the discovery of higher-quality cores and further accelerating the search process.

Acknowledgements

This work is partially supported by the French National Research Agency (ANR) under the Chair MASSAL'IA (ANR19-CHIA-0013-01), co-funded by the French electricity distribution network operator Enedis, as well as under the project ANR-24-CE23-6126 (BforSAT). It was granted access to HPC resources of "Plateforme MatriCS" within University of Picardie Jules Verne, co-funded by the European Union with the European Regional Development Fund (FEDER) and the Hauts-De-France Regional Council.