An Efficient Core-Guided Solver for Weighted Partial MaxSAT

1 Introduction

The maximum satisfiability problem (MaxSAT) is a generalization of the well-known and NP-complete Boolean satisfiability problem (SAT) [Cook, 1971]. While both SAT and MaxSAT are fundamentally similar, the optimization aspect of MaxSAT makes it significantly more challenging to solve in practice. Unlike SAT, where the goal is to determine if there exists a satisfied assignment, MaxSAT requires finding an assignment that satisfies the maximum number of clauses, with some clauses necessarily falsified. Many real-world problems can be naturally encoded as MaxSAT problems, such as hardware verification [Biere et al., 2009], model-based diagnosis [Marques-Silva et al., 2015], planning [Kautz et al., 1992], and data analysis [Berg et al., 2019].

∗ corresponding author

Research on MaxSAT algorithms can be categorized into two primary groups: exact algorithms, which guarantee optimal solutions, and heuristic algorithms, which provide solutions of good quality within a reasonable amount of time, though without guarantees of optimality. This paper focuses on exact algorithms for weighted partial MaxSAT, which seek to maximizes the total weight of satisfied clauses.

Recently, exact MaxSAT solvers can be broadly classified into two categories: solvers based on SAT solvers and solvers that employ branch-and-bound strategies. Early branch-andbound MaxSAT solvers, such as MaxSatz [Li et al., 2007], MiniMaxSat [Heras et al., 2008], Ahmaxsat [Abram´e and Habet, 2014], and Akmaxsat [K¨ugel, 2010], achieved significant improvements by effectively leveraging MaxSAT resolution rules for local propagation [Li et al., 2007; Heras and Larrosa, 2006; Li et al., 2009] and incorporating lowerbound estimation techniques. Specifically, these solvers utilized unit-clause propagation to identify disjoint inconsistent subsets, which were then used for lower-bound estimation [Li et al., 2005; Li et al., 2006]. However, following Fu and Malik's groundbreaking introduction of SAT-based MaxSAT solvers in 2006 [Fu and Malik, 2006], the performance of branch-and-bound solvers on real-world instances has gradually been surpassed by SAT-based methods. In recent years, a promising direction has emerged with the development of MaxCDCL [Li et al., 2021b; Li et al., 2021a], a branch-andbound MaxSAT solver that integrates conflict-driven clause learning (CDCL). Subsequently, Li et al. [2025] further enhanced this framework by introducing an unlocking mechanism that reuses relaxation variables to extract more disjoint cores, thereby strengthening the lower bound. MaxCDCL has demonstrated outstanding performance, particularly on unweighted MaxSAT problems. Its weighted version has also shown competitive results compared to SAT-based MaxSAT solvers, marking a significant advancement in the field of branch-and-bound MaxSAT solvers.

The first SAT-based MaxSAT solver was introduced by Fu et al. [2006]. Later, Ans´otegui et al. [2009; 2010; 2017] improved the SAT-based solvers for weighted partial MaxSAT. MaxSAT solvers based on SAT solvers can generally be divided into three categories: model-guided, core-guided, and minimum hitting set (MHS)-guided solvers. Model-guided solvers set a cost value k and transform the MaxSAT problem into a SAT problem by checking whether a solution with a cost less than or equal to k exists. The value of k is then gradually reduced until the transformed SAT instance becomes unsatisfiable. Representative solvers of this approach include SAT4J-MaxSAT [Le Berre and Parrain, 2010], QMaxSat [Koshimura et al., 2012], Open-WBO [Martins et al., 2014], and Pacose [Paxian and Becker, 2024]. In contrast, core-guided and MHS-guided solvers treat the MaxSAT problem as the SAT instance and use a CDCL SAT solver to identify unsatisfiable cores. Core-guided solvers, after identifying an unsatisfiable core, learn new clauses from the core and add them to the original instance, thereby increasing the lower bound. SAT solving is then applied to the updated instance, and this process is repeated until a satisfiable solution is found. Representative core-guided solvers include UWrMaxSAT [Piotr´ow, 2020], CGSS2 [Ihalainen et al., 2024], and EvalMaxSAT [Berg et al., 2024]. For MHSguided solvers, each time an unsatisfiable core is identified, the set of clauses to be passed to the SAT solver in the next round is updated. The goal of this update is to minimize the number of clauses not passed to the SAT solver by computing the MHS of all known unsatisfiable cores. This process is repeated iteratively until a satisfiable solution is found. Typically, mixed integer programming (MIP) solvers are used to solve the MHS. Notable MHS-guided solvers include LMHS [Saikko et al., 2016] and MaxHS [Bacchus, 2022].

In this paper, we propose a core-guided MaxSAT solver, built upon the UWrMaxSAT solver [Piotr´ow, 2024], with two key improvements. The first and most important improvement is a novel extended stratified strategy that guides the algorithm to focus primarily on solving high-weight soft clauses. This strategy is applied adaptively, based on the specific characteristics of the instance, thereby improving overall efficiency. The second improvement is a stratified-based method for extracting multiple disjoint unsatisfiable cores in each iteration, which helps accelerate the solving process.

By incorporating these two ideas, we developed an enhanced MaxSAT solver, CASHWMaxSAT, which was submitted to the MaxSAT Evaluation 2024 1 . Extensive experiments are conducted to evaluate CASHWMaxSAT on the complete weighted benchmarks of the MaxSAT Evaluations from 2022 to 2024. The experimental results demonstrate that CASHWMaxSAT outperforms eight state-of-theart MaxSAT exact solvers across all benchmarks. Furthermore, our analysis reveals that the proposed strategies significantly contribute to the outstanding performance of CASHWMaxSAT.

This paper is organized as follows: Section 2 provides the preliminaries. Sections 3 and 4 describe the two proposed strategies. Section 5 reviews the framework of our proposed MaxSAT solver. Section 6 presents an empirical evaluation and analysis of our solver. Section 7 concludes the paper.

2 Preliminaries

Let V = {x1, x2, . . . , xn} be a set of propositional variables. A literal is either a variable x or its negation ¬x. A clause is a disjunction of k literals, i.e., cj = lj1 ∨ lj2 ∨ · · · ∨ ljk, where lji represents the literal in the clause and |cj| = k denotes the length of the clause. A clause is called a unit clause if it contains exactly one literal. A propositional formula in conjunctive normal form (CNF) is a conjunction of m clauses, i.e., F = c1 ∧ c2 ∧ · · · ∧ cm, where |F | = m represents the number of clauses in the formula. A truth assignment ρ assigns each variable in V a truth value from {0, 1}, where 0 represents false and 1 represents true. A literal x is satisfied by a truth assignment ρ if x = 1, and a literal ¬x is satisfied if x = 0. A clause is satisfied if at least one of its literals is satisfied, and a CNF formula is satisfied if all its clauses are satisfied.

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

The Boolean satisfiability (SAT) problem is to determine whether there exists a truth assignment that satisfies a given CNF formula F. A SAT formula is considered satisfiable if there exists a truth assignment that satisfies all its clauses; otherwise, it is deemed unsatisfiable. For an unsatisfiable SAT formula F , an unsatisfiable core (core) is a subset of the clauses in F that is itself unsatisfiable. A minimal unsatisfiable core is an unsatisfiable core with the additional property that removing any clause from it results in a satisfiable set of clauses. An optimized version of SAT, known as MaxSAT, seeks to determine whether there exists a truth assignment that satisfies the maximum number of clauses in F . In partial MaxSAT, the clauses are divided into hard clauses Fhard and soft clauses Fsoft, and the goal is to find a truth assignment that satisfies all hard clauses and maximizes the number of satisfied soft clauses. In weighted partial MaxSAT (WPMS), each soft clause c ∈ Fsoft is assigned a weight w(c) to reflect its importance, and the objective is to find a truth assignment that satisfies all the hard clauses while maximizing the total weight of the satisfied soft clauses. Given a soft clause set F ′ , we use maxw(F ′ ), minw(F ′ ), and avgw(F ′ ) to represent the maximum, minimum, and average weight values of all soft clauses in F ′ , respectively.

In the process of solving MaxSAT, the input MaxSAT instance is first normalized. Given a CNF formula F = Fhard∪Fsoft, for each non-unit soft clause c = l1∨l2∨· · ·∨ll (i.e., |c| > 1), we introduce a relaxation variable ri to transform the clause into a unit soft clause. Specifically, we add a literal ¬ri to the clause c, resulting in a new clause cnew = l1 ∨ l2 ∨ · · · ∨ ll ∨ ¬ri. This new clause is treated as a hard clause and added to Fhard. The original clause c is then removed from Fsoft, and a unit clause ri, whose weight equals w(c), is added to Fsoft. If the relaxation variable ri is assigned true, it indicates that the original clause c is satisfied; otherwise, c is not satisfied. During the search process, we will maintain a lower bound (LB) and upper bound (UB) of the total weight of unsatisfied soft clauses, and the assumption set (assump) is defined as the set of unit soft clauses that must be satisfied under the current assignment during a SAT solver call.

Core-guided MaxSAT solver typically starts by adding all unit soft clauses in Fsoft to the assumption set assump. The solver then iteratively calls a SAT solver on the working formula Fhard ∪ assump. The SAT solver will say whether the formula is satisfiable or not, and in case the formula is unsatisfiable, it will give an unsatisfiable core core. At this point the algorithm will produce new relax variables, one for each clause in core. The working formula will consist in adding the new variables to the formulas of the core, adding a cardinality constraint saying that exactly one of the new variables should be true, and increasing LB by 1. This procedure is applied until the SAT solver returns satisfiable.

3 Extended Stratified Strategy forWPMS

Many previous MaxSAT solvers, such as MaxHS [Bacchus, 2022], start with the initial assumption that all soft clauses must be satisfied and pass this assumption directly to the SAT solver for processing. However, this approach has a significant drawback: the SAT solver must handle all soft clauses from the beginning, regardless of their varying weights. As a result, the solver may spend substantial time on low-weight soft clauses, diverting focus from high-weight clauses that are more critical.

To tackle this issue, Ans´otegui et al. [2012] proposed the stratified strategy. The key idea behind this strategy is to limit the clauses passed to the SAT solver, prioritizing high-weight soft clauses first.

3.1 Traditional Stratified Strategies

The stratified strategy proposed by [Ans´otegui et al., 2012] optimizes the solving process by dividing the soft clauses into multiple layers based on their weights and solving them layer by layer. The minimum weight value for the current layer (denoted as assump weight in our work) is set to be the maximum weight among all unprocessed soft clauses. These unprocessed soft clauses include the remaining original soft clauses (denoted as F ′s ) and the soft clauses whose weights have been decreased to below assump weight during the handling of unsatisfiable cores (denoted as delay). In detail, when processing a current layer, all soft clauses with weight values greater than or equal to assump weight should be removed from both F ′s and delay, and added to the assumption set assump for further processing. In addition, if any clause c ∈ assump is later found to have w(c) < assump weight, it should be removed from assump and added to delay for deferred handling.

The UWrMaxSAT algorithm improves upon the stratified strategy by introducing two key enhancements [Piotr´ow, 2020]. First, the algorithm separately evaluates F ′s and delay and selects the candidate set with the larger maximum weight (maxw) between the two. If both sets have the same maxw, delay is prioritized as the candidate set. Second, the algorithm refines the determination of assump weight based on the selected candidate set. When the candidate set is F ′s , assump weight is set to the second-highest weight if the difference between the highest and second-highest weights is only 1; otherwise, it is set to the highest weight. When the candidate set is delay, assump weight is always set to the highest weight.

3.2 Details of Extended Stratified Strategy

In this subsection, we first analyze the drawbacks of traditional stratified strategies and then introduce our extended stratified strategy.

The traditional stratified strategies described above adopt a fine-grained approach to stratification, where the assump weight value for each layer is set close to the maximum weight value among all unprocessed soft clauses. However, if the assumption sets for several successive layers (i.e., different unprocessed soft clauses) are set to true individually, and the SAT solver repeatedly returns true without generating any unsatisfiable core-particularly in cases where satisfying the hard clauses is inherently challenging-this finegrained approach can significantly slow down the solving process. A potential improvement is to merge multiple successive layers into a single layer, allowing the SAT solver to handle them collectively in one step. On the other hand, if the assump weight value of the current layer is set significantly lower than the maximum weight among all unprocessed soft clauses, the approach becomes coarse-grained. This results in excessive processing within a single layer, thereby reducing the algorithm's ability to prioritize high-weight soft clauses effectively.

To strike a balance between fine-grained and coarsegrained approaches, our method sets assump weight to ⌊maxw(F ′s )/2⌋ + 1 when handling F ′s . The rationale for this value is explained below, followed by an example to provide a more concrete illustration. With our method, each soft clause is processed at most once in the current layer. Specifically, once a soft clause appears in an unsatisfiable core and is processed, it is removed from the current layer and added to delay for subsequent handling. Additionally, to prevent the top layer from becoming overloaded with too many soft clauses, we compare ⌊maxw(F ′s )/2⌋ + 1 with avgw(F ′s ). The larger of these two values is selected as the assump weight for the top layer.

Furthermore, we analyze the triggering condition for adopting our proposed extended stratified strategy. Preliminary experiments revealed that for certain instances, the algorithm performs better without using the stratified strategy. Upon analyzing the structural features of these instances, we observed that they often exhibit similar weight distributions, characterized by a ratio of the standard deviation to the average weight (denoted as coeff) smaller than 1. We hypothesize that when the weight distribution of a problem is highly dispersed, it is more effective to process the problem layer by layer. Based on this observation, our algorithm applies the stratified strategy only if coeff ≥ 1; otherwise, the stratified strategy is bypassed.

Example 1. Consider an example where maxw(F ′s ) is 9, and let c be a unit soft clause with the maximum weight value in F ′s . According to our approach, we set assump weight = ⌊maxw(F ′s )/2⌋ + 1 = 5. If c appears in an unsatisfiable core, then after processing the core, w(c) becomes at most 4. Because w(c) is now smaller than assump weight, the clause c is removed from the current layer.

Based on the above considerations, we propose an extended stratification strategy, outlined in Algorithm 1. First, the algorithm determines whether the stratified strategy should be applied. If the stratified strategy is not used, all soft clauses are returned directly (Line 1). Otherwise, the algorithm calculates the assump weight value for the top layer based on the larger of avgw(F ′s ) and (⌊maxw(F ′s )/2⌋ + 1), moves all satisfied soft clauses from F ′s to assump, and then

Algorithm 1: Stratification

Input: the remaining soft clauses F ′s Output: the modified assumption set assump 1 if coeff < 1 then mark := -1 and return F ′s ; 2 if mark = 0 then 3 if avgw(F ′s) > ⌊maxw(F ′s)/2⌋ + 1 then assump weight := ⌊avgw(F ′s)⌋ ; 4 else assump weight := ⌊maxw(F ′s)/2⌋ +1 ; 5 mark := 1; 6 for each ci ∈ F ′s do 7 if w(ci) ≥ assump weight then F ′s := F ′s \ {ci}, assump := assump ∪ {ci} ; 8 return assump; 9 if state = SAT then 10 if delay ̸= ∅ and maxw(F ′s) ≤ maxw(delay) then 11 assump weight :=maxw(delay); 12 for each ci ∈ delay do 13 if w(ci) ≥ assump weight then 14 delay := delay \ {ci}; 15 assump := assump ∪ {ci}; 16 else 17 assump weight := ⌊maxw(F ′s)/2⌋ + 1; 18 for each ci ∈ F ′s do 19 if w(ci) ≥ assump weight then 20 F ′s := F ′s \ {ci}; 21 assump = assump ∪ {ci}; 22 else if state = UNSAT then 23 for each ci ∈ assump do 24 if w(ci) < assump weight then 25 assump := assump \ {ci}; 26 delay := delay ∪ {ci}; 27 else if state = UNKNOWN then 28 for each ci ∈ assump do 29 if w(ci) = assump weight then 30 assump := assump \ {ci}; 31 delay := delay ∪ {ci}; 32 assump weight :=minw(assump); 33 return assump;

returns the updated assump (Lines 2-8). During the subsequent stratified process, if the SAT solver returns SAT, the algorithm selects a candidate set (either delay or F ′s ) for further processing (Lines 9-10). If delay is selected, assump weight is set to maxw(delay) (Line 11); otherwise, it is set to ⌊maxw(F ′s )/2⌋ + 1 (Line 17). The corresponding sets are then updated accordingly (Lines 12-15 and Lines 18-21). If the SAT solver returns UNSAT, all soft clauses in assump with weights less than assump weight are removed and added to delay (Lines 22-26). If the SAT solver returns UNKNOWN, the algorithm removes the soft clauses in assump with the smallest weight, adds them to delay, and updates assump weight to minw(assump) (Lines 27-32). Finally, assump is returned (Line 33).

Algorithm 2: MUS

Input: CNF formula Fhard, an unsatisfiable core core Output: the minimal unsatisfiable core core 1 foreach ci ∈ core do 2 core := core \ {ci}; 3 state := SATSolver(Fhard ∪ core); 4 if state ̸= UNSAT then core := core ∪ {ci} ; 5 return core;

4 Stratified-BasedMulti-Unsatisfiable Cores Extraction Method for WPMS

Several existing works focus on extracting multiple unsatisfiable cores to improve MaxSAT solving efficiency. For instance, in the first stage of the MaxHS algorithm [Davies and Bacchus, 2011], identifying as many disjoint unsatisfiable cores as possible significantly enhances the algorithm's performance. Furthermore, Saikko [2015] demonstrates that extracting multiple disjoint unsatisfiable cores in each iteration can improve the efficiency of MHS-guided MaxSAT solvers. Building on this idea, Berg et al. [2017] introduces a weightaware core extraction technique for the WPMS, which leverages disjoint unsatisfiable cores. The authors [2017] propose that, instead of requiring all unsatisfiable cores within the same disjoint phase to be strictly disjoint, soft clauses with higher weight values may be shared among multiple cores. This approach aims to increase the number of unsatisfiable cores extracted during the same disjoint phase.

Given these advancements, a natural question arises: can our proposed extended stratified strategy be combined with the multi-unsatisfiable cores extraction method? To explore this, we adapt the existing unsatisfiable core extraction techniques to align with our extended stratified strategy, resulting in a novel stratified-based multi-unsatisfiable cores extraction (MUCE) method.

4.1 Extraction of Minimal Unsatisfiability Core

To extract multiple unsatisfiable cores, the first step is to obtain a single unsatisfiable core. In the context of MaxSAT, an unsatisfiable core is a set of clauses from soft clauses that cannot be satisfied simultaneously, regardless of the truth assignments to the involved soft clauses. This subset inherently contains a conflict that prevents any possible satisfying assignment. Our proposed MaxSAT solver relies on a SAT solver to extract unsatisfiable cores. When an unsatisfiable core is obtained, at least one clause within the core is guaranteed to be unsatisfiable, enabling the derivation of a cardinality constraint. To generate these constraints, we adopt the OLL procedure [Andres et al., 2012; Morgado et al., 2014; Ignatiev et al., 2019] and convert the resulting cardinality constraints into clauses using the encoding approach outlined in UWrMaxSAT [Piotr´ow, 2020].

However, the unsatisfiable core extracted by the SAT solver is typically not minimal, meaning it may include redundant clauses that are not necessary for its unsatisfiability. As highlighted by EvalMaxSAT [Avellaneda, 2020], smaller unsatisfiable cores lead to better performance in the OLL procedure. To address this, we apply a core minimization technique pro-

Algorithm 3: MUCE

Input: CNF formula Fhard ∪ assump, lower bound LB, an unsatisfiable core core, minimum weight value assump weight for the current layer Output: lower bound LB, hard clauses Fhard, the assumption set assump 1 assumpt := assump; 2 wt(c) := w(c), for each c ∈ assumpt ; 3 cores := corem := ∅; 4 while assumpt ̸= ∅ do 5 corem := MUS(Fhard, core); 6 LB := LB +minw(corem); 7 cores := cores ∪ {corem}; 8 foreach ci ∈ assumpt do 9 if ci ∈ corem then 10 wt(ci) := wt(ci) -minw(corem); 11 if wt(ci) < assump weight then 12 assumpt := assumpt \ {ci}; 13 (state, ρ, core) := SATSolver(Fhard ∪ assumpt); 14 if state ̸= UNSAT then break; 15 for corem ∈ cores do 16 (Fhard, assump) := OLL(corem, Fhard, assump); 17 return (LB, Fhard, assump)

posed by Marques-Silva et al. [2010] after extracting the unsatisfiable core. This step removes redundant clauses, resulting in a minimal unsatisfiable core (MUS).

Algorithm 2 illustrates the process of minimizing the unsatisfiable core. The algorithm iterates through all the unit soft clause ci in the core and removes each soft clause from the core (Line 2). Then, we call the SAT solver to check the satisfiability of the remaining core, which also includes the hard clauses (Line 3). If the solver returns UNSAT, this means ci is a redundant soft clause in the core and should be deleted. Otherwise, ci is an essential part of the unsatisfiable core, and the algorithm adds it back to the core (Line 4). Finally, the obtained minimal unsatisfiable core is returned (Line 5).

4.2 Details of the MUCEMethod

The MUCE method, presented in Algorithm 3, begins by initializing a temporary set, assumpt, to store the assumption set assump (Line 1), and an array, wt, to store the weight values of each unit soft clause c in assumpt (Line 2). Two core sets, cores and corem, are also initialized as empty sets (Line 3). The algorithm proceeds to enumerate the minimal unsatisfiable cores until assumpt becomes empty (Line 4). After minimizing the current unsatisfiable core (Line 5), the algorithm updates the lower bound by the minimum weight value of the current minimal unsatisfiable core, minw(corem) (Line 6), and adds the minimal core corem to cores (Line 7). For each unit soft clause in assumpt, if it exists in the current minimal unsatisfiable core, the algorithm reduces its weight by minw(corem) (Line 10). Because the MaxSAT algorithm uses the proposed extended stratified strategy, the weight value of every unit soft clause in assump is always greater than or equal to the minimum weight of the current layer, assump weight. As a result, the algorithm removes those unsatisfied unit soft clauses from assumpt (Lines 11-12), which is mainly different from previous extraction methods. Next, the algorithm calls the SAT solver to solve the formula Fhard ∪ assumpt. If the result is UNSAT, this indicates that additional unsatisfiable cores exist in the formula; otherwise, the enumeration process terminates (Lines 13-14). Finally, for all minimal unsatisfiable cores, the algorithm converts them into corresponding clauses using the OLL procedure and adds them to Fhard and assump (Lines 15-16). The algorithm then returns the lower bound, LB, along with the updated Fhard and assump (Line 17).

5 The Framework for CASHWMaxSAT

Algorithm 4 presents the framework of our proposed CASHWMaxSAT. We first introduce the key variables and functions used in our proposed algorithm.

The remaining set of soft clauses is expressed as F ′s . To facilitate our stratification method, we use assump weight to record the minimum weight value in the current layer under the proposed stratified strategy, i.e., all soft clauses whose weight is not smaller than assump weight in F ′s being added into the assumption set assump as the current layer. The tag variable mark can take three possible values: -1 indicates that the algorithm does not use the proposed stratified strategy; 0 indicates that the algorithm is using the proposed stratified strategy for the first time; and 1 indicates that the proposed stratified strategy has already been applied more than once.

The current assignment is denoted as ρ, while the best assignment found so far is represented as ρ∗ . The function cost(F, ρ) computes the total weight of unsatisfied soft clauses under the assignment ρ. Each SAT solver call returns a triple (state, ρ, core), where state represents the solver's status: satisfiable (SAT), unsatisfiable (UNSAT), or unknown (UNKNOWN). If the solver returns SAT, ρ is the current assignment that satisfies Fhard ∪ assump. If the solver returns UNSAT, it indicates no assignments can satisfy all assumptions, and core contains a subset of soft clauses from Fhard ∪assump that form an unsatisfiable core. If the solver returns UNKNOWN, it means the solver fails to resolve the current formula. In our work, the termination condition of the SAT solver is that when the number of conflicts generated during the search reaches a certain threshold, the solver returns UNKNOWN.

The input CNF formula F is normalized, meaning that each soft clause is a unit soft clause. The algorithm begins by initializing necessary variables (Lines 1-2). It then applies an extended stratification strategy to organize the soft clauses based on their weights and returns the minimum weight of the top layer as assump weight (Line 3).

The main iterations of the algorithm are carried out in Lines 4-13. If UB equals LB, it indicates that the optimal solution has been found, and the loop terminates (Lines 9 and 12). In each iteration, the SAT solver is invoked on the current formula, which consists of all hard clauses and the assumption set assump. This process essentially sets all unit soft clauses (treated as literals) in assump to true. The SAT solver then returns its result, which is stored in the variable

Algorithm 4: CASHWMaxSAT

Input: CNF formula F = Fhard ∪ Fsoft Output: upper bound UB, truth assignment ρ∗ 1 assump := delay := ρ∗ := ρ := ∅; 2 UB := ∑c∈Fsoft w(c), mark := LB := 0, F ′s := Fsoft; /* Extended Stratified Strategy */ 3 assump := Stratification(F ′s); 4 while true do 5 (state, ρ, core) := SATSolver(Fhard ∪ assump); 6 if state = SAT then 7 if UB > cost(F, ρ) then 8 UB := cost(F, ρ), ρ∗ := ρ; 9 if UB = LB then return (UB, ρ∗ ); 10 else if state = UNSAT then /* Cores Extraction Method */ 11 (LB, Fhard, assump) := MUCE(Fhard ∪ assump, LB, core, minw(assump)); 12 if UB = LB then return (UB, ρ∗ ); /* Extended Stratified Strategy */ 13 if mark ̸= -1 then assump := Stratification(F ′s) ;

state (Line 5).

If the SAT solver returns SAT, the algorithm retrieves a truth assignment from the solver (Line 6). If UB is improved, the algorithm updates UB and ρ∗ accordingly (Lines 7-8). If the SAT solver returns UNSAT, indicating a conflict within assump, the proposed MUCE method is employed to enumerate disjoint unsatisfiable cores (Lines 1112). This method incorporates unsatisfiable core minimization techniques to generate a high-quality set of disjoint unsatisfiable cores. The MUCE method returns updated values for LB, Fhard, and assump. At the end of each iteration, the algorithm calls the proposed stratified strategy to update assump accordingly (Line 13).

In our proposed algorithm, we also use some additional existing techniques to further improve the performance of our algorithm, including the harden strategy [Ans´otegui et al., 2013] to transform soft clauses with relatively large weights into hard unit clauses based on the current values of lower and upper bounds whenever the value of lower or upper bound is changed, the mixed strategy [Piotr´ow, 2020] to switch from core-guided linear search to binary search if the predefined time limit is exceeded, the preprocessing strategy [Ignatiev et al., 2019] to preprocess the literals of assump to detect unit cores and at-most-one cores after using the stratified strategy, and a general Boolean multi-level optimization technique [Paxian et al., 2021] to detect weighted instances that encode multi-objective problems with a lexicographic optimality criterion, optimizing the search procedure accordingly.

6 Computational Experiments

We conducted an experimental investigation to evaluate the performance of the proposed CASHWMaxSAT solver. Developed based on the COMiniSatPS SAT solver [Oh, 2016], the CASHWMaxSAT was implemented in C++11 with -O3 optimization to ensure high performance. All experiments were conducted on a system running Ubuntu 22.04.5 LTS, equipped with an Intel(R) Xeon(R) Platinum 8260 CPU @ 2.40GHz and 512GB of memory.

We selected all test instances from the complete weighted track of the MaxSAT Evaluation (MSE) 2022, 2023, and 2024 2 , resulting in a total of 1,736 instances. These instances span a wide range of domains, including combinatorial optimization, artificial intelligence, circuit design, software engineering, and bioinformatics, ensuring both diversity and representativeness for a comprehensive evaluation of algorithm performance. For each test instance and algorithm, the runtime was set to 3,600 seconds, aligning with the competition's time limit.

To ensure a fair comparison, we excluded all hybrid solvers that rely on other independent solvers and focused solely on the latest versions of independent MaxSAT exact solvers that participated in the complete weighted track of the MSEs from MSE2022 to MSE2024, excluding our algorithm. This resulted in the selection of seven solvers: Exact [Devriendt, 2024], Open-WBO [Martins et al., 2023], Pacose [Paxian and Becker, 2024], CGSS2 [Ihalainen et al., 2024], WMaxCDCL [Li et al., 2024], UwrMaxSAT [Piotr´ow, 2024], and EvalMaxSAT [Berg et al., 2024]. Additionally, we included SCIP (version 8.1.0) [Bestuzheva et al., 2021], a constraint integer programming solver often used in combination with other MaxSAT solvers as an independent solver in recent MSEs, as a competitor. In total, we compared our method against eight state-of-the-art MaxSAT solvers.

Furthermore, many algorithms in recent MSEs have adopted hybrid approaches by combining multiple solvers to improve performance. In this context, we also compare the hybrid version of our algorithm with five state-ofthe-art hybrid MaxSAT solvers from the complete weighted track of the MSEs: WMaxCDCL+Open-WBO [Li et al., 2024], MaxHS [Bacchus, 2022], UwrMaxSAT+SCIP [Piotr´ow, 2024], WMaxCDCL+SCIP+MaxHS [Coll et al., 2023], and EvalMaxSAT+SCIP [Berg et al., 2024]. It is important to note that MaxHS, in addition to being a MaxSAT solver based on a SAT solver, also utilizes the commercial linear programming solver CPLEX 3 for solving the hitting set problem, which classifies MaxHS as a hybrid algorithm. In the WMaxCDCL+SCIP+MaxHS configuration, the SCIP is called by using the competition version of UwrMaxSAT+SCIP, but this version does not execute SCIP for certain large instances and instead runs UwrMaxSAT. As a result, this hybrid algorithm essentially combines four distinct solvers. Among these solvers, some provide multiple parameter configurations in recent MSEs, and for consistency, we selected the best-performing configuration for each algorithm (including our own competition version) for comparison.

6.1 Overall Results

Independent Algorithm Comparison. Table 1 presents a comparison of all algorithms across three sets of instances. #solve represents the number of instances solved, while avg denotes the average time in seconds required to solve these instances. PAR2 refers to the penalized average runtime [Hutter et al., 2009], with a penalization constant of 2, which is used for the first time in the MSE2024. The results indicate that our solver not only achieves the highest number of optimal solutions across all benchmark tests but also outperforms the second-best solver by more than 10 instances solved to optimality per benchmark set, while maintaining significantly lower average solving times. Furthermore, in terms of the PAR2 score, our algorithm clearly demonstrates an advantage, with at least 100 fewer penalized average runtime compared to the other algorithms, underscoring its superior performance in both solution quality and solving speed. Additionally, Figure 1 illustrates the increase in the number of solutions processed by all algorithms over time, with our algorithm consistently outperforming the others at every time interval, further emphasizing its efficiency.

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

3 https://www.ibm.com/products/ilog-cplex-optimization-studio

Hybrid Algorithm Comparison. Table 2 presents a comparison of all hybrid algorithms, showing that our algorithm performs slightly worse than WMaxCDCL+SCIP+MaxHS on the MSE22 benchmark, where it achieved two additional optimal solutions. However, on the other two benchmarks, our algorithm outperforms all the others, clearly demonstrating its superior performance. As shown in Tables 1 and 2, our solver with SCIP solves 44 more instances than the version without SCIP. In comparison, EvalMaxSAT and UWrMaxSAT with SCIP solve 60 and 53 more instances, respectively, than their versions without SCIP. These results suggest that while incorporating SCIP into our method does lead to improvements, the gain is less significant compared to its contribution in other solvers. Additionally, our proposed CASHWMaxSAT utilizes the best-performing configuration of WMaxCDCL+SCIP+MaxHS, resulting in a new solver, CASHWMaxSAT+SCIP+MaxHS. The results show that our new algorithm achieves 449 optimal solutions, which represents the best performance on the MSE 22 instances. Due to the lower server configuration used in our experiments compared to those in MSE 23, our results are slightly less favorable than those reported in MSE 23. To address this, we extended the time limit for the top three performing solvers to 7200 seconds and re-ran these algorithms on all the instances from MSE 23. The results show that CASHWMaxSAT+SCIP, WMaxCDCL+SCIP+MaxHS, EvalMaxSAT+SCIP, and UwrMaxSAT+SCIP achieved 451, 446, 442, and 439 optimal solutions, respectively.

6.2 Evaluating Two Strategies

We conducted an effectiveness analysis on two strategies of our algorithm: the extended stratified strategy and the MUCE method. Table 3 compares CASHWMaxSAT with the following variants: 1) CASHWMaxSAT\STRA. CASHWMaxSAT ignores the proposed stratified strategy; 2) CASHWMaxSAT+TSTR. CASHWMaxSAT uses a traditional stratified strategy, as implemented in UWrMaxSAT [Piotr´ow, 2020], instead of the proposed stratified strategy; 3) CASHWMaxSAT\MUCE. CASHWMaxSAT ignores the MUCE; 4) CASHWMaxSAT\MUST. CASHWMaxSAT ignores the MUCE and the proposed stratified strategy.

These results highlight the impact of stratified strategy and MUCE on the algorithm's performance under various conditions. From the comparison with CASHWMaxSAT\MUST, our algorithm achieves 17.3 more instances solved to optimality per benchmark set compared to this, it is evident that the strategies we designed are highly effective in improving the solving performance. Moreover, the effectiveness of the additional techniques, including the hardening strategy, preprocessing strategy, BMO technique, mixed strategy, and others, can be assessed through the results of CASHWMaxSAT\MUST presented in Table 3.

CASHWMaxSAT\MUST performs worse than both EvalMaxSAT and UwrMaxSAT, suggesting that the application of additional techniques alone is insufficient. A significant performance gain can only be achieved when these techniques are combined with the two main extensions.

The number of optimal solutions found by CASHWMaxSAT+TSTR is, on average, 7.3 fewer per benchmark compared to CASHWMaxSAT\STRA, indicating that the previous stratified strategy did not integrate well with our designed MUCE strategy. On the other hand, CASHWMaxSAT+TSTR has, on average, 16.3 fewer instances solved to optimality per benchmark set than our algorithm, further highlighting that the new stratified strategy we designed integrates exceptionally well with the MUCE strategy, leading to a significant improvement in performance. The number of optimal solutions obtained by CASHWMaxSAT\MUCE and CASHWMaxSAT\STRA both show a noticeable gap compared to our algorithm, especially in the MSE23 benchmark, where the difference is most apparent. This clearly demonstrates that both strategies are indispensable. In contrast, our algorithm outperforms both, demonstrating that our designed stratified strategy integrates more effectively with the MUCE strategy, leading to a significant improvement in the solving performance. Additionally, Figure 2 illustrates the number of optimal solutions obtained by each algorithm over time, offering a more intuitive comparison of the effectiveness of our algorithm.

7 Conclusions and FutureWork

In this paper, we present CASHWMaxSAT, an efficient unsatisfiable core-guided MaxSAT solver that leverages an extended stratified strategy and a stratified-based multiunsatisfiable core extraction method. Our experiments demonstrate the excellent performance of our solver.

As future work, while the MaxSAT community has traditionally focused on maximizing the number of optimal solutions, the introduction of the PAR2 scoring evaluation in MSE 24 has highlighted the importance of minimizing runtime. In addition, when combined with SCIP, the solving time tends to be longer. This suggests that future work should involve adjusting the model inputs to SCIP in order to improve performance.

Figure 2: The cumulative distribution functions of CASHWMaxSAT and its five modified versions for all the benchmarks.

Acknowledgements

We would like to thank the anonymous referees for their helpful comments. This work is supported by National Cryptologic Science Fund of China 2025NCSF02046, NSFC under Grant No. 61806050, Jilin Science and Technology Department YDZJ202201ZYTS412.