<figure><img src="image_1.png" /></figure>

HAL
open science

# Solving weighted Maximum Satisfiability with Branch and Bound and clause learning

Jordi Coll, Chu-Min Li, Shuolin Li, Djamal Habet, Felip Manyà

► To cite this version:

Jordi Coll, Chu-Min Li, Shuolin Li, Djamal Habet, Felip Manyà. Solving weighted Maximum Satisfiability with Branch and Bound and clause learning. Computers and Operations Research, 2025, 183, pp.107195. 10.1016/j.cor.2025.107195. hal-05352912

HAL Id: hal-05352912

https://hal.science/hal-05352912v1

Submitted on 7 Nov 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_2.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
<figure><img src="image_3.png" /></figure>

# Solving weighted Maximum Satisfiability with Branch and Bound and clause learning

Jordi Coll<sup>a, b, c</sup>, Chu-Min Li<sup>c, d, e</sup>, Shuolin Li<sup>c, d</sup>, Djamal Habet<sup>c, d</sup>, Felip Manyà<sup>b, d</sup>

<figure><img src="image_4.png" /></figure>

## ARTICLE INFO

Dataset link: Source code and input parameters
(Original data)

**Keywords:**

Combinatorial optimization

Weighted partial MaxSAT

Branch-and-Bound algorithm

Clause learning

## ABSTRACT

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.

## 1. Introduction

The Maximum Satisfiability (MaxSAT) Problem is an optimization extension of the NP-complete Propositional Satisfiability (SAT) Problem (Cook, 1971) (another optimization extension of SAT is MinSAT Li et al. (2010)). Given a multiset of soft clauses, MaxSAT aims to maximize the number of satisfied soft clauses in it. There are several variants of MaxSAT: Partial MaxSAT (PMS) introduces hard clauses, which must be satisfied in any solution. Weighted Partial MaxSAT (WPMS) assigns a weight to each soft clause, and the goal is to satisfy all hard clauses while maximizing the total weights of satisfied soft clauses. All these variants are NP-hard (Papadimitriou, 1994).

Algorithms for MaxSAT can be categorized into two types: heuristic algorithms, which quickly find good solutions without guaranteeing optimality, and exact algorithms, which return proven optimal solutions but require more computational time. In this paper, we focus on exact MaxSAT solving, which has been an active research area for the past two decades (Bacchus et al., 2021; Li and Manyà, 2021),

despite its NP-hardness. Thanks to the concerted efforts of the scientific community, MaxSAT has become an effective technology for modeling, optimally solving, and certifying the optimality of solutions for a wide range of practical problems. Exact MaxSAT solvers have been successfully applied in diverse fields such as bioinformatics (Marques-Silva et al., 2011), combinatorial testing (Ansótegui et al., 2022), planning (Zhang and Bacchus, 2012), scheduling (Bofill et al., 2022a) and team formation (Manyà et al., 2020), among others.

Broadly, we categorize exact MaxSAT solvers into two principal groups: SAT-based solvers (Bacchus et al., 2021), which reduce a MaxSAT problem into a series of SAT problems and leverage SAT solvers to find solutions, and Branch-and-Bound (BnB) solvers (Li and Manyà, 2021), which explore the solution space by constructing a binary assignment tree. The results of the annual MaxSAT Evaluation (MSE) (MSE, 2024) consistently highlight that, even though BnB solvers outperform their SAT-based counterparts on random and some crafted instances, SAT-based solvers excel in tackling large industrial

<footnote><sup>a</sup> Universitat de Girona, Girona, Spain</footnote>

<footnote><sup>b</sup> Artificial Intelligence Research Institute, CSIC, Bellaterra, Spain</footnote>

<footnote><sup>c</sup> Aix Marseille Univ, Université de Toulon, CNRS, LIS, Marseille, France</footnote>

<footnote><sup>d</sup> Université de Picardie Jules Verne, Amiens, France</footnote>

<footnote>* Corresponding author.</footnote>

<footnote>E-mail addresses: jordicoll@udg.edu (J. Coll), chu-min.li@u-picardie.fr (C.-M. Li), shuolin.li@etu.univ-amu.fr (S. Li), Djamal.Habet@univ-amu.fr (D. Habet), felip@iiaa.csic.es (F. Manyà).</footnote>
instances and have maintained their dominance in such category until very recently. This performance gap can be attributed to the inherent design of SAT-based solvers, which fully exploit advanced SAT-solving techniques such as unit propagation and clause learning, features that previous BnB solvers have utilized to a lesser extent.

The BnB solver MaxCDCL, which is the first BnB solver designed for unweighted PMS that successfully integrates clause learning into BnB, was introduced in Li et al. (2022, 2021). The results in these works demonstrated that MaxCDCL ranks among the top-5 solvers when evaluated against the instances and solvers of the 2020 edition of MSE (MSE20). MaxCDCL not only efficiently solved industrial instances that other BnB solvers failed to solve, but also solved classes of instances that remained unsolved by other SAT-based solvers. These findings highlight the potential of integrating clause learning into BnB to advance MaxSAT solving. However, whether BnB with clause learning could efficiently handle weighted MaxSAT variants remained unanswered until the 2022 and 2023 editions of MSE (MSE22 and MSE23), where our solver WMaxCDCL participated and was classified in top positions. In particular, one of the versions of WMaxCDCL achieved the first position in MSE23.<fnref n="1" />

In this paper, we present for the first time the high-level WMaxCDCL algorithm, which combines BnB and clause learning for solving WPMS. We also describe the different techniques and implementation details that make it effective. At its core, the algorithm adapts the well-known CDCL framework from SAT (Marques-Silva et al., 2021) to WPMS, enriched with novel optimization techniques. Moreover, WMaxCDCL is designed to solve MaxSAT and all its variants, including WPMS. The existence of soft clauses with different weights presents several challenges that we will analyze in the subsequent sections. In addition, we experimentally demonstrate that BnB is indeed competitive for WPMS and provide results showing the high complementarity of WMaxCDCL with the other state-of-the-art techniques. Moreover, our experimental evaluation identifies and evaluates the key techniques for the good performance of WMaxCDCL.

The paper is organized as follows. Section 2 introduces the notation and preliminaries on SAT-based problem solving. Section 3 contains the related work. Section 4 describes the high-level WMaxCDCL algorithm. Section 5 explains the lower bound computation technique and its integration with clause learning. Section 6 presents the hardening method in WMaxCDCL and how it is combined with unit propagation. Section 7 describes other relevant techniques and implementation details of our solver WMaxCDCL. Section 8 discusses similarities and differences of the presented techniques with other approaches. Section 9 presents the experimental results. Finally, Section 10 gives the conclusions.

## 2. Preliminaries

A Boolean propositional variable $x$ can be assigned false or true, respectively represented as 0 and 1. Every variable $x$ corresponds to two literals: the positive literal $x$ and the negative literal $\neg x$. A clause is a disjunction of literals, i.e. it is of the form $l_1 \lor \dots \lor l_k$, where $l_i$ ($1 \le i \le k$) is a literal. A propositional formula in Conjunctive Normal Form (CNF) is a conjunction of clauses, usually represented as a set of clauses. An assignment $v$ assigns 0 or 1 to one or several variables. Given a variable $x$, an assignment such that $v(x) = 1$ satisfies the positive literal $x$ and falsifies the negative literal $\neg x$, whereas $v(x) = 0$ falsifies $x$ and satisfies $\neg x$. We will represent an assignment using the set of satisfied literals, e.g. $v = \{x_1, \neg x_2, x_3\}$ meaning $v(x_1) = 1$, $v(x_2) = 0$, $v(x_3) = 1$. An assignment is complete w.r.t. a formula if every variable in the formula is assigned a value, otherwise it is partial. When a variable is assigned, its two literals are also said assigned. The variables as well as their literals not assigned in a partial assignment are said free. A clause is satisfied if at least one of its literals is satisfied, and is falsified if all

<figure><img src="image_5.png" /><figcaption>**Algorithm 1:** CDCL($\phi$) algorithm for solving SAT.</figcaption></figure>

its literals are falsified. We also refer to falsified clauses as conflicting or empty clauses. A formula in CNF is satisfied if all its clauses are satisfied, and is falsified if at least one clause is falsified. Note that given a partial assignment the satisfaction of a clause or CNF can be undecided. A clause is unit if one of its literals is free and its other literals are falsified.

Given a CNF formula, the Boolean satisfiability (SAT) problem consists in determining the existence of an assignment that satisfies this CNF formula. MaxSAT generalizes SAT by finding an assignment that maximizes the number of satisfied clauses. Usually MaxSAT admits a multiset of clauses in which some clauses are repeated, in order to give more relevance to the satisfaction of these clauses. There are several variants of MaxSAT including Partial MaxSAT (PMS), Weighted Partial MaxSAT (WPMS) and Weighted MaxSAT. In Partial MaxSAT (PMS), each clause can be either hard or soft, and the goal is to maximize the number of satisfied soft clauses while satisfying all hard clauses. In Weighted Partial MaxSAT (WPMS), each soft clause $c$ has a cost to pay $\omega(c)$ (referred to as its weight) if it is falsified. The goal of WPMS is to maximize the sum of weights of satisfied soft clauses while satisfying all hard clauses. PMS is a particular case of WPMS when $\omega(c) = 1$ for each soft clause $c$. Weighted MaxSAT is WPMS with an empty set of hard clauses. The different MaxSAT variants are usually stated equivalently as a minimization problem w.r.t. falsified soft clauses, e.g. WPMS consists in minimizing the sum of the weights of falsified soft clauses. If no hard clause is falsified under the current assignment, the assignment is said feasible. A feasible complete assignment is also called a solution. An optimal solution is a solution that satisfies all hard clauses and minimizes the sum of the costs of falsified soft clauses in the formula.

The basis of modern SAT solvers is the Conflict-Driven Clause Learning (CDCL) algorithm, displayed in Algorithm 1. The algorithm starts with an empty partial assignment $v$. First, at line 6, Unit Propagation (UP) is used to extend $v$ while trying to satisfy the input formula $\phi$. UP is the repetitive application of the unit clause rule which states that, if there is a unit clause, its only free literal must be assigned true to

<footnote n="1">¹ https://maxsat-evaluations.github.io/2023/rankings.html</footnote>
<figure><img src="image_6.png" /><figcaption>Fig. 1. Illustration of an implication graph, where decision nodes are in grey and the last decision is dashed.</figcaption></figure>

satisfy $\phi$. UP continues until a clause becomes falsified (we have found a conflict), or until no unit clause remains in $\phi$.

Let us first consider the case where UP finishes without finding any conflict (line 15). If all the variables are assigned in $v$, we conclude that $\phi$ is satisfiable (line 17). Otherwise, a free literal is heuristically chosen and satisfied by assigning a value to its variable (we make a *decision*, line 20). Every assigned literal is associated with a decision level equal to the number of decisions before it is assigned.

Let us now consider the case where UP finds a falsified clause (line 7). If the conflict is found at decision level 0, we conclude that $\phi$ is unsatisfiable (line 9). Otherwise, we inspect the *implication graph* to derive a new clause logically implied by $\phi$ that explains the conflict (line 11). This process is called *conflict analysis*. This clause is added to $\phi$ (is learnt), we backtrack to the decision level marked by the learnt clause as explained below (line 14), and the search continues

We illustrate an example of an implication graph in Fig. 1. It is a directed acyclic graph representing the clauses involved in the UPs of the current assignment. A node $l@dl$ represents that literal $l$ has been satisfied at decision level $dl$. Nodes without incoming edges correspond to decisions, while the other nodes correspond to UPs. The clause that originated UP of a node $l@ld$ is represented in the graph by the propagated node and the negations of the literals of incoming edges. For instance, clause $\neg x_7 \lor x_8 \lor x_{13}$ propagated $x_{13}@5$ because $x_7$ and $\neg x_8$ were satisfied. The conflicting clause is represented by the incoming edges to $\square$; in this example, clause $\neg x_3 \lor x_{16}$. A Unique Implication Point (UIP) is a node that is traversed in any path from the last decision to $\square$. There are three UIPs in Fig. 1: $x_{13}$, $x_8$, and the last decision $\neg x_9$.

The most used learning scheme consists in finding the *first UIP* (1UIP), which is the closest UIP to the conflict, in this case $x_{13}$. Starting from the conflicting clause, this process derives a new clause to be learnt, consisting of literals of levels smaller than the conflicting level (level 5 in Fig. 1) that directly imply one or more literals in the conflicting level, together with the negation of 1UIP in the conflicting level ($x_{13}$ in Fig. 1). Considering the literals of clause under construction in reverse order of assignment, every step in the process replaces one literal by the falsified literals that implied it, i.e. by the negations of the predecessors in the graph. The process finishes when the 1UIP is the only remaining literal of the conflicting level, giving a learnt clause. In Fig. 1 the learnt clause would be $x_1 \lor \neg x_5 \lor \neg x_6 \lor \neg x_{13}$, derived by the following sequence of steps: from the conflicting clause $\neg x_3 \lor x_{16}$, (i) we resolve $x_3$ (i.e., resolve $\neg x_3 \lor x_{16}$ and $x_3 \lor x_1 \lor x_{18}$, the clause implying $x_3$) and get $x_1 \lor x_{16} \lor x_{18}$, (ii) we resolve $x_{16}$ and get $x_1 \lor x_{10} \lor x_{18}$, (iii) we resolve $x_{10}$ and get $x_1 \lor \neg x_6 \lor \neg x_{13} \lor x_{18}$, and (iv) we resolve $x_{18}$ and get $x_1 \lor \neg x_5 \lor \neg x_6 \lor \neg x_{13}$.

The learnt clause explains the conflict in the sense that falsifying all its literals would reproduce the implication graph and derive the same conflict. Hence, adding the learnt clause prevents the same conflict in the future search. The learnt clause also dictates the backtracking point, which is the second highest decision level among its literals (level 3 in the running example), where all literals of the clause but the 1UIP will be falsified, and hence the 1UIP will be propagated in a new UP.

All modern solvers complement the CDCL algorithm with a number of well-established techniques such as restarts and periodic deletion of learnt clauses. WMaxCDCL also includes these techniques which we do not describe since, although they have a critical impact on performance, they are conceptually orthogonal to the current work. We refer the reader to Marques-Silva et al. (2021) for a detailed description of the CDCL algorithm.

### 3. Related work

The exact MaxSAT solvers can be roughly divided into two categories: BnB solvers (Li and Manyà, 2021) and SAT-based solvers (Bacchus et al., 2021). BnB solvers search for an optimal assignment by constructing a binary search tree in which each node corresponds to a partial assignment. Let $ub$ be the cost of the best solution found so far (which is initialized to $\infty$). At every node of the search tree, BnB solvers compute a lower bound $lb$ of the total cost of falsified soft clauses. If $lb \ge ub$, the current branch cannot yield a better solution, leading the solvers to prune and backtrack; otherwise, the search continues. Ahmaxsat Abramé and Habet (2014), Cherif et al. (2020), Akmaxsat Kuegel (2010), MaxSatz (Li et al., 2007) and MiniMaxSat Heras et al. (2008) are the most representative BnB solvers.

Given a multiset of clauses $\phi$, SAT-based MaxSAT solvers solve $\phi$ by solving a sequence of SAT problems (Bacchus et al., 2021). We can further classify these solvers as model-guided, core-guided and Implicit Hitting Set (IHS)-guided. Model-guided solvers encode the problem of finding a feasible assignment falsifying at most $ub$ soft clauses in $\phi$ into SAT, and solve the obtained SAT instance using a SAT solver, by iteratively reducing $ub$ from $\infty$ until the SAT instance becomes unsatisfiable. Some representative model-based solvers are SAT4J-Maxsat Le Berre and Parrain (2011), QMaxSat Koshimura et al. (2012), Zha (2020), Open-WBO (Martins et al., 2014) or Pacose (Paxian and Becker, 2020). Core-guided and IHS-guided approaches have in common that they iteratively call a SAT solver to extract a subset of soft clauses (called a *core*) that cannot be satisfied at the same time without falsifying a hard clause. Their differences are as follows. Core-guided solvers iteratively relax the obtained cores until the instance become satisfiable, at which point the obtained assignment is optimal. IHS solvers maintain a set of the found cores and solve a minimum hitting set problem to compute a minimum-cost subset of soft clauses that covers all the cores. The hitting set problem is typically solved with Integer Programming. Among core-guided solvers we can find msu1.2 (Marques-Silva and Manquinho, 2008), WBO (Manquinho et al., 2009), Open-WBO (Martins et al., 2014), WPM1 (Ansótegui et al., 2009), PM2 (Ansótegui et al., 2013), WPM2 (Ansótegui et al., 2010), WPM3 (Ansótegui and Gabàs, 2017), Eva (Narodytska and Bacchus, 2014), RC2 (Ignatiev et al., 2019), EvalMaxSAT (Avellaneda, 2023), CashWMaxSAT (Lei et al., 2021b) and among MHS-guided solvers there are MHS (Saikko et al., 2016) and MaxHS (Bacchus, 2020; Bacchus et al., 2017; Davies and Bacchus, 2011, 2013).

The previous BnB or SAT-based MaxSAT solvers usually have the corresponding WPMS version or directly handle WPMS instances. The most important techniques to deal with different weights of soft clauses include clause splitting and weight stratification. *Clause splitting* consists in replacing a weighted soft clause $(C, m+n)$, where $C$ is a clause and $m+n$ is an integer weight written as a sum, with clauses $(C, m)$ and $(C, n)$. This is typically used when clauses $(C_1, m_1),..., (C_k, m_k)$ are involved in a rule application requiring equal weights of the clauses. In this case, the rule is applied to clauses $(C_1, m),..., (C_k, m)$, where $m = \min(m_1, ..., m_k)$, and the residual clauses $(C_1, m_1 - m),..., (C_k, m_k - m)$ can be used in the further rule applications, as in Ansótegui et al. (2009), Li et al. (2007), Manquinho et al. (2009). Clause splitting is also implicitly used in WMaxCDCL, as we describe later.

Weight stratification is mainly used in SAT-based MaxSAT solvers (Ansótegui et al., 2012). It partitions the soft clauses into $k$ sets so that
the clauses in set $i$ ($1 < i \le k$) have a higher weight than the clauses in set $i-1$. The solver first solves the instance only considering the clauses in set $k$. Then, it adds the set $k-1$ and solves the resulting instance. This process continues until the problem has been solved considering all the soft clauses. This technique moves the cost towards the optimum more rapidly and greatly reduces the number of calls to the SAT solver.

SAT-based MaxSAT solvers clearly surpass BnB solvers without clause learning on industrial and large crafted instances, because they benefit from the clause learning capabilities by the CDCL SAT solver that they use to solve the sub-problems. MaxCDCL was the first BnB solver directly exploiting clause learning, becoming competitive on unweighted industrial and large crafted instances (Li et al., 2021).

# 4. General structure of a weighted MaxCDCL solver for WPMS

This section describes the main structure of the WMaxCDCL algorithm.

## 4.1. Input formula normalization

WMaxCDCL is designed to work with formulas that have been normalized. An input WPMS instance $\phi$, which in the general case consists of a set of hard clauses and a multiset of weighted soft clauses, must be transformed into a new instance $\phi'$ formed by a set of hard clauses ($H$) and a set of weighted soft literals ($S$). A soft literal receives this name because it represents a soft clause. The weight of soft literal $y$ is denoted as $\omega(y)$.

We compute $H$ and $S$, and define $\omega(y)$ for each soft literal $y \in S$ as follows: Let $\alpha$ be an integer variable representing a constant cost and initialized to 0. Initially, $H$ contains the original hard clauses. For each original non-unit soft clause $sc$, we insert a fresh soft literal $y$ into $S$ with weight $\omega(y) = \omega(sc)$ and force $y$ to be true if and only if $sc$ is satisfied, by adding hard clauses representing $y \leftrightarrow sc$ into $H$. All unit soft clauses with the same literal $l$ are first merged into a single unit soft clause with weight $\omega(l) = \sum_{sc \in S_l} \omega(sc)$, where $S_l$ is the set of original unit soft clauses containing literal $l$. After merging these duplicates, for any two complementary soft unit clauses $l$ and $\neg l$ such that $\omega(l) \ge \omega(\neg l)$, we remove soft clause $\neg l$, increase $\alpha$ by $\omega(\neg l)$, and update $\omega(l)$ to $\omega(l) - \omega(\neg l)$. If after this update $\omega(l) > 0$, soft literal $l$ is inserted into $S$.

**Example 1.** Let $\phi$ be a WPMS instance composed of the hard clauses $x_1 \lor x_2, \neg x_1 \lor x_2, \neg x_1 \lor \neg x_2, \neg x_2 \lor x_3, x_2 \lor \neg x_3$ and the weighted soft clauses $(x_1 \lor \neg x_2, 3), (x_3, 5), (\neg x_3, 3)$. The new instance $\phi'$ is composed of the set of hard clauses $H = \{x_1 \lor x_2, \neg x_1 \lor x_2, \neg x_1 \lor \neg x_2, \neg x_2 \lor x_3, x_2 \lor \neg x_3, y_1 \leftrightarrow (x_1 \lor \neg x_2)\}$ and the set of weighted soft literals $S = \{(y_1, 3), (x_3, 2)\}$, and $\alpha = 3$.

After this preprocess, $\alpha$ is set aside as a constant cost to be added to any solution of the resulting WPMS instance, and the definition of the WPMS problem is equivalently stated as follows.

**Definition 1.** An instance of the WPMS problem is a formula $\phi = (H, S)$, where $H$ is a set of hard clauses, and $S$ is a set of weighted soft literals. WPMS is the problem of finding a complete assignment that satisfies all clauses in $H$, and that minimizes the objective function $f(\phi)$ defined below:

$$f(\phi) = \sum_{y \in S} \omega(y) \cdot (1 - y) \qquad (1)$$

We will denote the cost of a (complete or partial) assignment $v$ by $cost(v)$, which is defined as the sum of weights of soft literals falsified by $v$:

$$cost(v) = \sum_{y \in S, \neg y \in v} \omega(y) \qquad (2)$$

<figure><img src="image_7.png" /><figcaption>**Algorithm 2:** WMaxCDCL(H, S, ub), a generic CDCL procedure with lookahead for WPMS</figcaption></figure>

## 4.2. WMaxCDCL algorithm

The main WMaxCDCL algorithm is a generalization for WPMS of the CDCL algorithm for SAT. It is described in Algorithm 2, where we underline the differences w.r.t. Algorithm 1, which are mainly two. Firstly, the goal of CDCL is to find an assignment $v$ that satisfies all hard clauses, while WMaxCDCL also requires that $cost(v) < ub$. Notice hence that Algorithm 2 is a decision algorithm. The minimization of $cost(v)$ will be achieved by successive calls of this algorithm, asking for cost-improving solutions every time a solution is found, until no solution improving the lowest cost found so far can be found. Secondly, we distinguish two kinds of conflicts: a **hard conflict** occurs when $v$ falsifies a hard clause (like in CDCL), and a **soft conflict** occurs when the solver detects that the current assignment $v$ cannot be extended to a solution of cost less than $ub$. In either case, the conflict is represented by a falsified clause $cl$, and is dealt with standard conflict analysis techniques. Therefore, WMaxCDCL can be implemented by extending any state-of-the-art CDCL SAT solver.

The particular features of the WMaxCDCL algorithm are encapsulated in the call to the function UPLA in line 6. This function is the responsible of extending the current partial assignment before and after a decision is made, as well as detecting both hard and soft conflicts. This is described in Algorithm 3. First, at line 5, two different techniques are applied in function UP-harden to extend the partial assignment with newly propagated literals: unit propagation and hardening. Hardening is described in detail in Section 6; intuitively, it consists in assigning 1 to a soft literal if its falsification would imply that $lb = cost(v) \ge ub$.

When UP-harden is finished, if a hard conflict is detected, the conflicting clause is returned. Otherwise, we may detect a soft conflict when $lb = cost(v) \ge ub$. In this case, a falsified clause representing the soft conflict will be generated by function softConflictClause. If neither a hard nor a soft conflict has been detected, WMaxCDCL may return the extended assignment or, if a custom-defined condition is met, run
<caption>**Algorithm 3:** UPLA(H, S, v, ub)</caption>

Input: $H$: set of hard clauses, $S$: set of soft literals, $v$: partial assignment, $ub$: upper bound.
Output: $(cl, v):$ $cl$ is a clause falsified by a hard or soft conflict, or _ if none is found; $v$ is the possibly extended assignment.
1 begin
2 & $lb \leftarrow cost(v);$ 
3 & $C \leftarrow \{\{y\} | y \in S, v(y) = 0\};$ /* Set storing all detected cores */ 
4 & $R \leftarrow \{\neg y | y \in S, v(y) = 0\};$ /* Set of literals storing the union of all reasons of $C$ */ 
5 & $(cl, v, lb, C, R) \leftarrow \text{UP-harden}(H, S, v, ub, lb, C, R);$ 
6 & **if** $cl$ is a conflicting clause then
7 & & **return** $(cl, v);$ 
8 & **else if** $lb \ge ub$ then
9 & & $cl \leftarrow \text{softConflictClause}(ub, lb, C, R);$ 
10 & & **return** $(cl, v);$ 
11 & **if** lookahead condition satisfied then
12 & & $(lb, C, R) \leftarrow \text{lookahead}(H, S, v, ub);$ 
13 & & **if** $lb \ge ub$ then
14 & & & $cl \leftarrow \text{softConflictClause}(ub, lb, C, R);$ 
15 & & & restoreWeights$(S);$ 
16 & & & **return** $(cl, v);$ 
17 & & $(cl, v, lb, C, R) \leftarrow \text{UP-harden}(H, S, v, ub, lb, C, R);$ 
18 & & **if** $cl$ is a conflicting clause then
19 & & & restoreWeights$(S);$ 
20 & & & **return** $(cl, v);$ 
21 & & **else if** $lb \ge ub$ then
22 & & & $cl \leftarrow \text{softConflictClause}(ub, lb, C, R);$ 
23 & & & restoreWeights$(S);$ 
24 & & & **return** $(cl, v);$ 
25 & **return** $(\neg, v)$
end

function lookahead (line 12) to compute a larger $lb$. This increased $lb$ must be an underestimation of the cost that will have any extension of the current partial assignment $v$ that satisfies $H$. The increased $lb$ may allow to find a soft conflict (line 14), or to propagate more literals with UP-harden (line 17), which in turn can also trigger a hard or a soft conflict (lines 18–22).

Three key components in Algorithm 3 remain to be explained, which we do in the following sections. Firstly, we show in Section 5 how to underestimate a $lb$ with lookahead and combine soft conflicts with clause learning. Then, in Section 6, we present the propagation and hardening procedure executed in UP-harden. Finally, Section 7 explains, among other implementation details, what condition we establish to run lookahead (line 11).

## 5. Lower bound computation

Similarly to other BnB MaxSAT solvers, given a partial assignment $v$, WMaxCDCL underestimates a lower bound $lb \ge cost(v)$ of the minimum cost that will have any extension of $v$ satisfying the hard clauses $H$. More formally, it detects that given $H \cup v$, we have that $f(\phi) \ge lb \ge cost(v)$.

### 5.1. Lower bounding principle

The method that WMaxCDCL uses to underestimate a $lb$ is based on the computation of unsatisfiability cores.

**Definition 2.** An unsatisfiability core, or in brief a core, is a non-empty set of soft literals $C = \{y_1, \dots, y_{|C|}\}$ such that $y_1 \wedge \dots \wedge y_{|C|}$ cannot be satisfied without falsifying a hard clause. That is, given a set of hard clauses $H$, it holds $H \to (\neg y_1 \vee \dots \vee \neg y_{|C|})$, also denoted $H \to \neg C$.

A core can be implied by a subset $R = \{l_1, l_2, \dots, l_{|R|}\}$ of a partial assignment $v$. In this case, it is called a local core, we have that $H \cup R \to \neg C$, and we say that the set $R$ are the reasons of core $C$. In the rest of the paper, we will omit $H$ for simplicity, and just denote the relation between a core and its reasons as $R \to \neg C$. When the set of reasons is empty, we refer to $C$ as a global core. By definition, at least one soft literal of a local core must be false if the reasons are satisfied. Therefore, given a core $R \to \neg C$, we can compute a minimum cost $cost(C)$ that must be paid in order to satisfy the hard clauses:

$$cost(C) = \min_{y \in C} \omega(y) \qquad (3)$$

**Example 2.** Let $S = \{y_1, y_2, y_3, y_4\}$ with weights $\{2, 3, 4, 5\}$ respectively, and let $H$ be formed by: $\neg x_1 \vee \neg y_1 \vee x_3$, $x_2 \vee \neg y_2 \vee \neg x_4$, $\neg x_5 \vee \neg y_3 \vee x_3$, $x_2 \vee \neg y_4 \vee \neg x_4$, $\neg x_3 \vee x_4$. If no variable is assigned, we can satisfy all soft literals $y_1, \dots, y_4$ and the formula will be still satisfiable. Therefore, no global core exists. Assume now that we have the partial assignment $v = \{x_1, \neg x_2, x_5\}$. If we set $y_1, y_2$ to 1, the formula becomes unsatisfiable. Therefore, the following is a local core:

$$\{x_1, \neg x_2, x_5\} \to (\neg y_1 \vee \neg y_2)$$

From this core, we can deduce that given assignment $v$, $lb = cost(\{y_1, y_2\}) = 2$, which is the weight of $y_1$.

**Proposition 1** provides the foundation of the general method. Intuitively, if we find a set of local cores $\{R_1 \to \neg C_1, R_2 \to \neg C_2, \dots, R_n \to \neg C_n\}$ that together induce a cost $\ge ub$, we can conclude that some of the reasons in $R_1, \dots, R_n$ must be false.

**Proposition 1.** Let $H$ be a set of hard clauses and let $S$ be a set of soft literals. Let $\{R_1 \to \neg C_1, R_2 \to \neg C_2, \dots, R_n \to \neg C_n\}$ be a set of local cores, where $C_i \subseteq S$ for all $1 \le i \le n$, and such that:

$$\sum_{1 \le i \le n, y \in C_i} cost(C_i) \le \omega(y) \quad \forall y \in S \qquad (4)$$

$$\sum_{1 \le i \le n} cost(C_i) \ge ub \qquad (5)$$

Constraint (4) means that the total contribution of a soft literal over the cost of the different local cores must not exceed its weight. Constraint (5) means that the sum of the weights of all cores is greater than or equal to a given upper bound $ub$. Then, we have that:

$$H \wedge f(\phi) < ub \to \bigvee_{1 \le i \le n} \neg R_i \qquad (6)$$

In other words, the clause $\vee_{1 \le i \le n} \neg R_i$ is a logic consequence of the hard clauses and the upper bound on the total cost.

Given a partial assignment $v$, the lookahead procedure tries to find a set of local cores with the properties of Proposition 1 such that $R_i \in v$ for all $1 \le i \le n$. Hence, $v$ falsifies the implicit clause $\vee_{1 \le i \le n} \neg R_i$. The falsification of this clause is what we refer to as a soft conflict. Note that $v$ can contain some falsified soft literals, which also contribute to the lower bound. Each already falsified soft literal $y$ can be seen as a local core $\{\neg y\} \to \neg y$, which can also be used as specified by Proposition 1 to obtain a soft conflict clause.

The first key point in the method is to ensure that the considered local cores satisfy Constraint (4) to guarantee the soundness of the method, because a soft literal can belong to several cores. This can be achieved by updating $\omega(y) = \omega(y) - cost(C_i)$ every time $y$ is added to a new local core $C_i$ as the local cores are sequentially derived. Once the soft conflict derivation process is finished, the original weight of $y$ is restored. Similar management has been used in Weight-aware Core
Extraction (Berg and Järvisalo, 2017; Ihalainen et al., 2021). Note that Constraint (4), in the case of PMS, is much simpler to state and to check, since all soft literals have weight 1 and all cores have cost 1. Hence, in PMS, the constraint simply requires that every soft literal belongs to at most one core.

The second key point in the method is Constraint (6) allowing to combine core detection with clause learning. Note that this is not the case in Berg and Järvisalo (2017), Ihalainen et al. (2021) because their cores are global.

Example 3 shows the full derivation of a soft conflict.

**Example 3.** Let $S = \{y_1, y_2, y_3, y_4, y_5, y_6\}$ with weights $\{7, 2, 5, 12, 5, 3\}$ respectively, let the current partial assignment be $v = \{x_1, \neg x_2, x_3, \neg x_4, x_5, \neg y_6\}$, and let $ub = 13$. The given assignment already contains a core:

$$ \{\neg y_6\} \rightarrow \neg y_6, \quad \text{with } cost(\{y_6\}) = 3 $$

Therefore, we decrease $\omega(y_6)$ by 3, obtaining the weights $\{7, 2, 5, 12, 5, 0\}$. After this, we sequentially find the cores:

$$ \{x_1, \neg x_4\} \rightarrow \neg y_1 \lor \neg y_2, \quad cost(\{y_1, y_2\}) = 2, \quad \text{weights} \leftarrow \{5, 0, 5, 12, 5, 0\} $$

$$ \{\neg x_2, x_5\} \rightarrow \neg y_3 \lor \neg y_4, \quad cost(\{y_3, y_4\}) = 5, \quad \text{weights} \leftarrow \{5, 0, 0, 7, 5, 0\} $$

$$ \{x_1, \neg x_2\} \rightarrow \neg y_1 \lor \neg y_4, \quad cost(\{y_1, y_4\}) = 5, \quad \text{weights} \leftarrow \{0, 0, 0, 2, 5, 0\} $$

Hence, we detect $lb = 3+2+5+5 = 15$. Since $lb \ge ub$, we have reached a soft conflict. The clause explaining this soft conflict is $y_6 \lor \neg x_1 \lor x_2 \lor x_4 \lor \neg x_5$, which is falsified by $v$.

## 5.2. Local core detection and minimization

The full lookahead process to obtain weighted local cores can be found in Algorithm 4. It uses a set of soft literals $S'$ that maintains all unassigned soft literals $y$ with $\omega(y) > 0$. Starting with a partial assignment $v' = v$, literals from $S'$ are added to $v'$ as assumptions at decision level decisionLevel($v$) + 1 and, after every assumption, unit propagation is applied (line 12). Function UPforLA extends $v'$ with UP until no UP can be done, or a local core is detected. There are two cases where a local core $\{y_1, ..., y_m\}$ is detected: (i) a hard clause $cl$ is falsified after assuming $\{y_1, ..., y_m\}$; (ii) a soft literal $sl = y_m$ is propagated to false after assuming $\{y_1, ..., y_{m-1}\}$. After this, in lines 19–24, $lb$ is incremented, the weights of the soft literals in $C_i$ are updated, the assumed literals are reinserted into $S'$ excluding those with weight 0, and $v'$ is reset to the current assignment $v$. This iterative process concludes either when a soft conflict is detected ($lb \ge ub$) or no more local cores can be detected, in which case $S'$ becomes empty.

Detecting a soft conflict can require the derivation of numerous local cores. Additionally, the lookahead method to find a $lb$ is executed numerous times during the solving process. Therefore, it is of the utmost importance to use fast techniques such as UP to detect local cores. Furthermore, the size of the detected local cores and their reasons are equally critical. Detecting smaller local cores allows to have more free soft literals to be used to detect further cores, hence obtaining a better $lb$. Regarding the reasons, a smaller number of them leads to the generation of smaller soft conflicting clauses and, consequently, results in higher-quality clauses for the solver. For this reason, after detecting a local core, the generated implication graph is analyzed (line 16) to obtain a minimized local core and its reasons. Namely:

* The minimized core contains the assumed soft literals that have a path to $cl$ or $sl$, and also contains $sl$ in case (ii).

* The reasons are the set of literals that are assigned at a decision level smaller than decisionLevel($v$) + 1, have a path to $cl$ or $sl$, and have an outgoing edge pointing to some literal of level decisionLevel($v$) + 1.

**Example 4.** Let $y_1, ..., y_6$ be soft literals, and let $H$ be formed by:

<caption>**Algorithm 4: lookahead(H, S, v, ub)**, Lookahead method to detect local cores</caption>

**Input:** $H$: a set of hard clauses, $S$: a set of soft literals, $v$: a partial assignment, $ub$: an upper bound.
**Output:** $C = \{C_1, ..., C_n\}$: a set of cores; $R$: union of reasons of $C$; $lb$: a computed lower bound of the cost

1. **begin**
2. &nbsp;&nbsp;&nbsp;&nbsp;$C \leftarrow \{\{y\} | y \in S, v(y) = 0\}$; /* Set storing all detected cores */
3. &nbsp;&nbsp;&nbsp;&nbsp;$R \leftarrow \{\neg y | y \in S, v(y) = 0\}$; /* Set of literals storing the union of all reasons of $C$ */
4. &nbsp;&nbsp;&nbsp;&nbsp;$lb = cost(v)$;
5. &nbsp;&nbsp;&nbsp;&nbsp;$v' \leftarrow v$; $dl \leftarrow$ decisionLevel($v$) + 1;
6. &nbsp;&nbsp;&nbsp;&nbsp;$S' \leftarrow \{y | y \in S, y \notin v, \neg y \notin v\}$;
7. &nbsp;&nbsp;&nbsp;&nbsp;$A \leftarrow \{\}$; /* Set of assumed literals in a round of core detection */ while $lb < ub$ and $S' \ne \emptyset$ do
8. &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;$y \leftarrow$ pickSoftLiteral($S'$);
9. &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;$S' \leftarrow S' \setminus \{y\}$;
10. &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;$A \leftarrow A \cup \{y\}$;
11. &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;$v' \leftarrow v' \cup \{y\}$; /* Assume $y$ at decision level $dl$ */
12. &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;($cl, sl, v'$) $\leftarrow$ UPforLA(H, S, $v'$);
13. &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;/* Check if a hard clause $cl$ is falsified or a soft literal $sl$ with $\omega(sl) > 0$ is falsified */
14. &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;if $cl \ne$ or $sl \ne$ then
15. &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;/* Obtain the local core: $R_i \rightarrow \neg C_i$ */
16. &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;($C_i, R_i$) $\leftarrow$ analyzeImplicationGraph($cl, sl, dl$);
17. &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;$C \leftarrow C \cup \{C_i\}$;
18. &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;$R \leftarrow R \cup R_i$;
19. &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;$lb \leftarrow lb + cost(C_i)$;
20. &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**foreach** $y \in C_i$ **do**
21. &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;$$ \omega(y) \leftarrow \omega(y) - cost(C_i) $$
22. &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;$S' \leftarrow S' \cup A \setminus \{y | y \in C_i, \omega(y) = 0\}$;
23. &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;$A \leftarrow \{\}$;
24. &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;$v' \leftarrow v$; /*Cancel assignments done to find $C_i$ */
25. &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**return** ($lb, C, R$);

<table><tr><td>¬y<sub>1</sub> ∨ ¬y<sub>3</sub> ∨ x<sub>3</sub></td><td>x<sub>2</sub> ∨ ¬y<sub>4</sub> ∨ ¬x<sub>6</sub></td><td>¬x<sub>3</sub> ∨ ¬x<sub>5</sub> ∨ y<sub>4</sub></td></tr><tr><td>¬x<sub>1</sub> ∨ ¬x<sub>2</sub></td><td>¬y<sub>2</sub> ∨ ¬x<sub>4</sub></td><td>x<sub>6</sub> ∨ ¬y<sub>4</sub></td></tr></table>

Let $v = \{x_1, \neg x_2, x_5\}$, where $\neg x_2$ is propagated due to clause $\neg x_1 \lor \neg x_2$, and the other literals have been decided. Therefore, the current decision level is 2. We will assume soft literals at level 3. We pick them in lexicographical order. After assuming $y_1$, no unit propagation is done. After assuming $y_2$, we unit-propagate $\neg x_4$. Finally, after assuming $y_3$, we unit-propagate $x_3, y_4, \neg x_6$ and a conflicting clause $cl = x_6 \lor \neg y_4$ is detected. This process generates the implication graph in Fig. 2, and we obtain the minimized core and reasons $\{\neg x_2, x_5\} \rightarrow \neg y_1 \lor \neg y_3$. Notice that, without looking at the implication graph, a conservative representation of the core detected at line 14 of Algorithm 4 would be $\{x_1, \neg x_2, x_5\} \rightarrow \neg y_1 \lor \neg y_2 \lor \neg y_3$.

### 5.2.1. Free soft literal picking strategy

As we will see in the experimental evaluation, the strategy used to pick free soft literals to be assumed, at line 8 of Algorithm 4, has a substantial impact on the solver's performance. The strategy employed within WMaxCDCL draws inspiration from the insight that soft literals recently involved in local cores are likely candidates to be part of new local cores. Indeed, in cases where no backtracking has occurred since the previous lookahead call, it is possible to detect subsets of the previous cores, as the reasons of those cores remain assigned. Upon the conclusion of a lookahead process, we record the list of cores that have been found. Then, on the next run of lookahead, we pick free soft literals in the following order: firstly, we pick the literals from the
<figure><img src="image_8.png" /><figcaption>Fig. 2. Illustration of the implication graph involved in Example 4, where grey nodes are decisions or assumptions, and dashed nodes are assignments made during lookahead.</figcaption></figure>

last core detected in the current lookahead execution if some core has already been detected. Secondly, we pick all literals from a local core of the previous run, if some exists, and forget that core. Finally, the remaining free literals are picked.

### 5.2.2. Simplification of soft conflict clause

In unweighted MaxSAT, all soft literals have weight 1, hence local cores have also cost 1, and a soft conflict is found as soon as $lb = ub$ (more specific case than the general case $lb \ge ub$). Therefore, when generating the clause explaining a soft conflict for an unweighted instance in function softConflictClause (see Algorithm 3), all the detected cores and their reasons are needed to define a conflicting clause. However, in the general case of weighted soft literals, some of the detected cores can become unnecessary due to the detection of a new core with greater weight.

**Example 5.** Consider Example 3, where we have found the sequence of cores:

$$ 
\begin{array}{l@{\quad}l}
\{\neg y_6\} \rightarrow \neg y_6, & cost(\{y_6\}) = 3 \\
\{x_1, \neg x_4\} \rightarrow \neg y_1 \vee \neg y_2, & cost(\{y_1, y_2\}) = 2 \\
\{\neg x_2, x_5\} \rightarrow \neg y_3 \vee \neg y_4, & cost(\{y_3, y_4\}) = 5 \\
\{x_1, \neg x_2\} \rightarrow \neg y_1 \vee \neg y_4, & cost(\{y_1, y_4\}) = 5
\end{array}
$$

Again, $lb = 15$ and $ub = 13$. Note that we can remove the second core of the list, hence having $lb = 13 \ge ub$, still producing a soft conflict. This reduces the total number of reasons since $\neg x_4$ is not involved anymore in any remaining core. In consequence, the conflicting clause will be shorter, i.e. $y_6 \vee \neg x_1 \vee x_2 \vee \neg x_5$ instead of $y_6 \vee \neg x_1 \vee x_2 \vee x_4 \vee \neg x_5$.

We have experimentally observed that this situation occurs frequently when solving the WPMS instances of the MaxSAT Evaluations. Consequently, upon identifying a soft conflict, we run a simplification process to remove local cores until we obtain a subset of the detected local cores, named $C'$, where all its cores are needed. That is, we compute a subset $C' \subseteq C$ such that $\sum_{C_j \in C'} cost(C_j) \ge ub$ and $\sum_{C_j \in C' \setminus \{C_j\}} cost(C_j) < ub$ for all $C_j \in C'$.

Our method is designed to reduce the Literal Block Distance (LBD) (Audemard and Simon, 2009) of the generated clauses. For each core, we compute a value, denoted as $lbdInc(C_i)$, which corresponds to the number of distinct decision levels that are exclusively in the reasons of $C_i$. We prioritize the removal of cores with the highest values of $lbdInc(C_i)$. In the event of a tie, we keep the cores with reasons that have decision levels closest to the current decision level. The time complexity of this process is in $O(\max(|R| \cdot |C|, |C| \cdot \log(|C|)))$. First, all reasons of all cores are visited to compute $lbdInc(C_i)$. Then, we sort the cores by $lbdInc(C_i)$ and visit all cores once.

Note that the simplification of soft conflict clause is more important for WPMS than for PMS, because there are usually more cores in a soft conflict in WPMS so that the soft conflict clause is longer.

## 6. Integration of hardening and unit propagation

Hardening is a technique aimed at ensuring consistency and is typically integrated into BnB MaxSAT solvers. Given a partial assignment, if $lb < ub$ but $lb+\omega(y) \ge ub$ for some unassigned soft literal $y$ not belonging to the cores used for the computation of $lb$, then $y$ can be safely set to true. In unweighted MaxSAT, this situation only arises when $lb = ub - 1$. In this case, all free literals not involved in the computation of $lb$ are propagated. However, the situation differs in the case of

WPMS because soft literals can have different weights. Consequently, there might be only a subset of free soft literals $y$ not involved in the computation of $lb$ that satisfy $lb + \omega(y) \ge ub$. Furthermore, as $lb$ increases, other free soft literals $z$ can also start satisfying $lb + \omega(z) \ge ub$. Therefore, WMaxCDCL actively seeks to harden soft literals every time $lb$ is increased. Our experiments demonstrate that this hardening process significantly enhances the performance of WMaxCDCL.

Note that hardening extends the partial assignment $v$ with new literals, potentially enabling further unit propagations. This, in turn, can lead to propagate certain soft literals to false, increasing both $cost(v)$ and $lb$, which can allow further hardening. Therefore, during the propagation phase, WMaxCDCL alternates between UP and the hardening procedure until either a soft or hard conflict is encountered or no further increase in $lb$ occurs. This propagation loop corresponds to UP-harden, used in Algorithm 3 and described in Algorithm 5.

Another distinguishing feature of WMaxCDCL in comparison to other BnB MaxSAT solvers is that the hardened literals are propagated due to a unit clause. Therefore, similar to CDCL SAT solvers, each assigned literal in WMaxCDCL has been either decided (see Algorithm 2, line 20,) or unit-propagated by a unit clause. The rationale behind finding a unit clause for hardening based on the $lb$ is the same to the detection of a falsified clause in a soft conflict (see Proposition 1).

**Proposition 2.** Let $H$ be a set of hard clauses, let $S$ be a set of soft literals, and let $y \in S$. Let $\{R_1 \rightarrow \neg C_1, R_2 \rightarrow \neg C_2, \dots, R_n \rightarrow \neg C_n\}$ be a set of local cores, where $C_i \subseteq S$ and $y \notin C_i$ for all $1 \le i \le n$, and such that:

$$ \sum_{1 \le i \le n, y' \in C_i} cost(C_i) \le \omega(y') \quad \forall y' \in S \quad (7) $$

$$ \sum_{1 \le i \le n} cost(C_i) + \omega(y) \ge ub \quad (8) $$

Then, we have that:

$$ H \wedge f(\phi) < ub \rightarrow y \vee \bigvee_{1 \le i \le n} \neg R_i \quad (9) $$

In other words, the clause $y \vee \bigvee_{1 \le i \le n} \neg R_i$ is a logic consequence of the hard clauses and the upper bound on the total cost.

At the moment of hardening literal $y$, given an assignment $v$, we have that $R_i \in v$ for all $1 \le i \le n$, and $y \notin v$ and $\neg y \notin v$. Hence, the implicit clause $y \vee \bigvee_{1 \le i \le n} \neg R_i$ is unit under assignment $v$, and this clause will unit-propagate $y$.

**Example 6.** Let $S = \{y_1, y_2, y_3, y_4, y_5, y_6\}$ with weights $\{5, 3, 4, 8, 5, 2\}$ respectively, let the current partial assignment be $v = \{x_1, \neg x_2, x_3, x_4, \neg y_6\}$, and let $ub = 16$. We have that $cost(v) = 2$ due to core:

$$ \{\neg y_6\} \rightarrow \neg y_6, \text{ with } cost(\{y_6\}) = 2. $$

After a run of lookahead, we have detected the following additional cores:

$$ \{x_1, \neg x_2\} \rightarrow \neg y_1 \vee \neg y_2, \text{ with } cost(\{y_1, y_2\}) = 3. $$

$$ \{\neg x_2, x_4\} \rightarrow \neg y_3 \vee \neg y_4, \text{ with } cost(\{y_3, y_4\}) = 4. $$

$$ \{x_1, \neg x_2\} \rightarrow \neg y_1 \vee \neg y_4, \text{ with } cost(\{y_1, y_4\}) = 2. $$

Hence, we detect $lb = 11$. Since $lb + \omega(y_5) = 11+5 \ge ub$, we can harden $y_5$ with clause $y_5 \vee y_6 \vee \neg x_1 \vee x_2 \vee \neg x_4$.
**Algorithm 5:** UP-harden(H, S, v, ub, lb, C, R)

<figure><img src="image_9.png" /></figure>

# 7. Implementation and other techniques in WMaxCDCL

The WMaxCDCL solver is implemented on top of the MaxCDCL solver version introduced in Li et al. (2022). MaxCDCL is, in turn, an extension of the CDCL SAT solver Maple_CM (Luo et al., 2017; Li et al., 2020). In this section we explain the different implementation details and additional techniques included in WMaxCDCL. These techniques have proven effective in solving a greater number of problem instances, as substantiated by the results from our experimental evaluation.

## 7.1. Detection of an initial upper bound

WMaxCDCL finds and certifies the optimal solution of a WPMS formula by running Algorithm 2 with decreasing values of ub, where the cost of the last solution found is the value of ub for the subsequent iteration. This process could start at a trivial ub defined as trivialub = 1 + $\sum_{y \in S} \omega(y)$. However, we observed that, in many instances, a considerable amount of time is spent searching for suboptimal solutions that yield only marginal cost improvements. As a consequence, reaching the optimal solution within the specified time cutoff becomes unfeasible. To address this issue, WMaxCDCL incorporates a mechanism for detecting an initial feasible upper bound initub that is smaller than trivialub.

Let lsub be a feasible upper bound found with a local search WPMS solver. Starting with ub = 1, WMaxCDCL iteratively runs Algorithm 2 with increasing values of ub, updating ub = 3ub/2. If a solution is found before ub ≥ lsub, the cost of this solution is adopted as the value of initub. Otherwise, initub = lsub.

## 7.2. Probing strategy to run lookahead

As contemplated in Algorithm 3 (line 11), we do not execute lookahead at every node of the search tree. Instead, we selectively execute it based on certain conditions. This strategy aims at reducing the number of unsuccessful lookahead runs; i.e., we consider a run to be successful if an only if lb > ub and hence a soft conflict has been found. To be more precise, we apply the following rules:

* If the previous run has been successful, we run lookahead.

* Otherwise, with probability 1%, we run lookahead as a sampling run. We compute the average avg and standard deviation stdev of the value lb-cost(v) found in the subset of successful runs among sampling runs.

* Out of this 1% probability, we only run lookahead if ub-cost(v) < avg+coef·stdev, where coef is a coefficient dynamically adjusted to try to maintain the success ratio between 60% and 75%, as done in (Li et al., 2021).

## 7.3. Addition of encodings of implied PB constraints

Under some conditions, we add to WMaxCDCL a SAT encoding of the pseudo-Boolean (PB) constraint representing the current upper bound as an implied constraint; i.e., the constraint $\sum_{y \in S} (1 - y) \cdot \omega(y) < ub$. These constraints are added to small-sized formulas, more precisely those where $|S| < 500$, or $|S| < 5000 \land |S| \times ub \le 100000$. We use the MDD-based encoding of Bofill et al. (2020) if $ub < 50$, and otherwise we utilize the GGPW encoding of Bofill et al. (2022b). These values have been experimentally adjusted, and the selection between the two encodings is ruled by a trade-off between the propagation power (only MDD encoding maintains Generalized Arc Consistency by UP), and the size of the resulting formulas (GGPW is significantly smaller when ub is large) (Bofill et al., 2022b).

## 7.4. Preprocessing and inprocessing steps

Besides the WMaxCDCL algorithm itself and the other features explained before, WMaxCDCL solver includes several preprocessing and inprocessing techniques from the literature that we list now for completeness. Preprocessing steps are performed after parsing the instance and before starting the full search, and inprocessing steps are done at some selected points during the search, always after a restart or after a new solution for the current upper bound has been found.

WMaxCDCL inherits the implementation of the Bounded Variable Elimination preprocess from Maple_CM, which has been adapted to WPMS by restricting it to variables not corresponding to soft literals. Other inferences and reformulations done as inprocessing steps are failed literal detection, equivalent literal detection, and clause simplification.

Before starting the search we use UP to find sets of soft clauses, of which at most one of them can be satisfied according to hard clauses. Let {$cl_1, ..., cl_n$} be such a set of soft clauses. By using weight splitting we consider that every clause in the set has the same weight w. Then, {$cl_1, ..., cl_n$} is replaced by a new unit soft clause d with weight w, defined by hard clauses encoding d $\leftrightarrow$ cl_1 $\lor$ ... $\lor$ cl_n. Then the cost of any solution of the new instance will be increased by w · (n − 1) to obtained the cost for the original instance. An equivalent preprocessing step was proposed before in the context of independent set partitions in Maximum Clique problems (Fang et al., 2016; Li et al., 2018). It has also been used in other MaxSAT solvers such as MaxCDCL, RC2, MaxHS or CGSS, sometimes also referred to as intrinsic atMost1 constraints (Ignatiev et al., 2019).

When a new sub-optimal solution for the current upper bound is found, we try to improve it using a custom implementation of the local search method described in Zheng et al. (2022).

# 8. Relation to other solving techniques

In this section we discuss the main similarities and differences between WMaxCDCL and core-based WMPS solvers and native PB solvers.

## 8.1. Relation to core-based WMPS solvers

WMaxCDCL has in common with core-based WMPS solvers the detection of cores. However, it strongly differs from core-based WPMS solvers in three main aspects: the type of cores it detects, the method of detection, and their usage. On the first aspect, WMaxCDCL identifies local cores, i.e. cores that depend on a partial assignment, whereas core-based solvers only find global cores. Regarding the detection method,
core-based solvers perform a full CDCL-based search over a set of assumptions to detect the cores, whereas WMaxCDCL is only based on UP, which is crucial to achieving a fast computation of the cores, since we can potentially execute lookahead at any inner node of the search tree. Finally, WMaxCDCL combines a set of local cores to deduce a lower bound, examine the reasons that lead to the soft conflict, and naturally integrate this process with clause learning and backtracking, which is fundamentally different from the core relaxations and reformulations used to drive the optimization in core-based solvers.

## 8.2. Relation to PB solvers

Generally, a (linear) PB constraint is of the form $\sum_{i=1}^{n} q_i l_i \# K$, where $l_1, \dots, l_n$ are literals, $q_1, \dots, q_n$, $K$ are integers, and # is some comparator in $\{<, \le, \ge, >\}$. Clearly, a PB constraint generalizes a clause, which can be stated as $\sum_{i=1}^{n} l_i \ge 1$. Similarly, a set of PB constraints generalizes a propositional formula in CNF. Hence, Algorithm 2, that solves the problem of finding an assignment that satisfies a set of hard clauses and that has a cost smaller than the input *ub*, can be seen essentially as finding an assignment that satisfies a particular kind of PB constraints. Recall from Section 7.3 that the requirement of obtaining a solution that improves the current *ub* can be stated as a single PB constraint over the soft literals.

Pseudo-Boolean Optimization, i.e., the problem of solving a set of PB constraints possibly with a PB objective function, is in fact a formalism to model and solve problems that is growing interest, especially because they use refutations based on cutting planes, that are exponentially stronger than resolution-based algorithms such as CDCL for some kinds of instances. Native PB solvers exploiting this theoretical advantage, such as Galena (Chai and Kuehlmann, 2003), SAT4J (Le Berre and Par rain, 2011) and RoundingSAT (Elffers and Nordström, 2018; Devriendt et al., 2021), are a research focus.

There exist differences and similarities between the techniques used by native PB solvers and those of WMaxCDCL, especially related to constraint propagation, that we now discuss. First, it must be noted that the notion of unit propagation is generalized from clauses to PB constraints in PB solvers. Given a partial assignment $v$, the *slack* of a PB constraint of the form $\sum_{i=1}^{n} q_i l_i \ge K$ is $\sum_{i=1, \dots, l_i \notin t} q_i - K$. UP will satisfy any $l_i \notin v$ such that $q_i > \text{slack}$. Intuitively, UP will satisfy any unassigned literal that must be necessarily satisfied to reach the value $K$. The falsification of the PB constraint can be detected when *slack* < 0.

In absence of local cores (i.e. when the lower bound corresponds to the cost of the current assignment), there is a conceptual connection between WMaxCDCL and PB constraint propagation:

* A soft conflict in WMaxCDCL corresponds to falsifying a PB constraint (in particular, the *ub* improvement constraint).

* Hardening corresponds to applying unit propagation on the *ub* improvement PB constraint.

Notice however that reasoning on the partial assignment to detect local cores and improve the lower bound, and integrating this process with conflict detection, hardening and clause learning, is the main and distinguishing feature of WMaxCDCL. To the best of our knowledge, this has not been investigated in native PB to anticipate PB constraint falsification or to improve unit propagation. Similarly, constraint detection techniques used in PB solvers such as strengthening (Dixon and Ginsberg, 2002) do not apply reasoning over a partial assignment in inner nodes of the search tree. Instead, they reason over the whole formula as a preprocess step for reformulation purposes. In particular, strengthening is used to detect cardinality constraints, of the form $\sum_{i=1}^{n} l_i \ge K$.

Another important difference is that PB solvers manage an arbitrary (usually large) number of PB constraints, whereas the *ub* improvement constraint is the only (non-clausal) PB constraint present in WMax-CDCL. This has a direct impact on implementation and efficiency: hard

clauses are efficiently handled in WMaxCDCL with 2-watched literals, and hardening only deals with one PB constraint with a priority queue. On the contrary, achieving an efficient implementation of UP for a set of PB constraints is a challenging task under research (Devriendt, 2020; Nieuwenhuis et al., 2024), especially because a same constraint can propagate different literals at different depths of the same branch of the search tree.

# 9. Experimental evaluation

All the experiments of this section were run with an AMD EPYC 7502 32-core Processor @ 2.50 GHz under Linux with 32 GB of memory. To evaluate the solvers, we used the set of 558 instances from the exact weighted track of MaxSAT Evaluation 2023 (MSE23). Unless otherwise stated, we followed the same experimental setup as in the exact tracks of MSE23: there is a time limit of one hour to solve an instance; an instance is counted as solved if the solver finds an optimal solution and claims it by printing its OPTIMUM FOUND before the time limit expires, otherwise it is counted as unsolved; and the average solving times only considers solved instances. In this section, we empirically demonstrate the performance of WMaxCDCL. First, in Section 9.1, we provide experimental insights into the impact of various WMaxCDCL components on its overall performance. Next, in Section 9.2, we replicate the results from the exact weighted track of MSE23 on our machine to ensure a unified experimental setup, and run additional experiments to illustrate how different state-of-the-art approaches complement each other.

WMaxCDCL is available for download on the MSE23 webpage (Järvisalo et al., 2023). For this paper, we used a slightly modified version of the solver, which is accessible via a public repository.<fnref n="2" /> These modifications do not alter the behaviour of WMaxCDCL w.r.t. MSE23, but include some extra code and various compiler macros to enable or disable the features experimentally evaluated in Section 9.1. On the other hand, as explained in Section 7.1, unless otherwise stated, WMaxCDCL starts its execution by finding a first feasible upper bound *lsub* using a local search solver. In this work, we ran SatLike-ck (Lei et al., 2021a) for 60 s. For the sake of a fair comparison and to avoid obtaining different values of *lsub* across different runs, SatLike-ck was executed externally only once, and the obtained *lsub* for a particular instance was passed as a parameter to the different variants of WMaxCDCL. The values of *lsub* are also available in the public repository.

## 9.1. Evaluation of WMaxCDCL components

The first experiment evaluates the impact of the different components of WMaxCDCL (*wmccl* in short). We compare different versions of WMaxCDCL, each with certain components either removed or modified. The results are shown in Table 1. Column #sol contains the number of solved instances and column avg contains the average run time in seconds. The baseline solver, containing all features explained in this work, is *wmccl*. We consider the following modifications, which we describe in increasing order w.r.t. the number of solved instances, i.e. the first modification is the one that decreases the most the number of solved instances wr.t. the baseline.

*wmccl\LA.* Lookahead is never run, and hence soft conflicts are only detected when cost($v$)≥ub. Consequently, hardening will also be delayed to deeper nodes of the search tree. This is achieved by always falsifying the condition of line 11 in Algorithm 3. The results indicate that the absence of lookahead significantly harms WMaxCDCL, emphasizing its role as a key feature.

<footnote n="2">² https://github.com/jordicollcaballero/WMaxCDCL_Paper</footnote>
### wmcdcl\harden.
In this experiment we never use hardening in Algorithm 5, by making it return after UP has been done at line 3. The results demonstrate that hardening is a crucial feature of WMaxCDCL.

### wmcdcl\LS.
We do not run a local search solver as a preprocessing step. Hence, the procedure to find a first feasible upper bound initub proceeds as explained in Section 7.1, but without stopping at a given value lsub. In this case, we observe a noticeable decrease in performance, which is mostly due to the fact that, having a narrow ub when reading the instance allows for an initial trivial hardening at parse time for any clause cl with weight w(cl) ≥ ub. This initial hardening enables us to significantly simplify certain instances using the preprocessing techniques described in Section 7.4. This improvement is particularly noticeable in instances from the drmx-cryptogen family.

### wmcdcl\initub.
Search starts top-down from lsub, instead of finding an initial upper bound initub as explained in Section 7.1. The performance is decreased because, in some cases, even the upper bound provided by the local search phase is too large to start the complete search. Finding a first feasible upper bound down-top gives a tighter value that speeds up the search.

### wmcdcl+alwaysPB.
Always add PB constraints (Section 7.3) without a size limit. The results show that a remarkable number of instances have a large ub or a high number of variables that produce SAT encodings of PB constraints of prohibitive size. This negatively impacts the number of instances that can be solved. We avoid this issue in the baseline solver by adding the size limit constraints established in Section 7.3.

### wmcdcl+loLA.
When picking literals to be assumed during the search of a local core, at line 8 of Algorithm 4, the soft literals are picked in lexicographic order instead of using the strategy in Section 5.2.1. We observe that trying to reuse the last found local cores is highly beneficial.

### wmcdcl\PB.
Never add the SAT encoding of the cost improvement PB constraint (Section 7.3). We observe that seven instances benefit from this set of clauses. Previous works on IHS MaxSAT solving have shown that, in some instances like the drmx-atmostk family, adding encodings of cardinality (in this case, PB) constraints prevents dealing with exponentially many combinations of cores that can reach the upper bound (Berg et al., 2020). Although MSE23 did not include instances from the drmx-atmostk family, we have observed in benchmarks from earlier editions of the competition that WMaxCDCL also suffers from this problem. These instances remain unsolved unless SAT encodings of PB constraints are added.

### wmcdcl+alwaysLA.
Lookahead is always executed by forcing the satisfaction of the condition of line 11 in Algorithm 3. The results reveal that, while running lookahead is crucial, always running it can waste computation time by attempting to identify soft conflicts without success. Therefore, the strategy presented in Section 7.2 can help solve a few additional instances.

### wmcdcl\simp.
Do not use the simplification of Section 5.2.2. This feature has a moderate but still positive impact on the number of solved instances.

## 9.2. Analysis of results in MSE23

In this section, we reproduce and further investigate the results of WMaxCDCL in the Exact Weighted Track of MSE23, where a solver that combines WMaxCDCL with other techniques achieved the first position. We submitted three solvers based on WMaxCDCL<fnref n="3" />: WMaxCDCL, WMaxCDCL1800-S600-HS1200 and WMaxCDCL1800-S900-HS900.

<caption>**Table 1**</caption>

Number of optimally solved instances and average time in seconds for different WMaxCDCL variants on instances from Exact Weighted Track of MSE23.

<table><caption>**Table 2**</caption><thead><tr><th>Solver</th><th>#sol</th><th>avg</th></tr></thead><tbody><tr><td>wmcdcl\LA</td><td>351</td><td>93 s</td></tr><tr><td>wmcdcl\harden</td><td>379</td><td>154 s</td></tr><tr><td>wmcdcl\LS</td><td>383</td><td>135 s</td></tr><tr><td>wmcdcl\initub</td><td>386</td><td>104 s</td></tr><tr><td>wmcdcl+alwaysPB</td><td>392</td><td>186 s</td></tr><tr><td>wmcdcl+loLA</td><td>396</td><td>180 s</td></tr><tr><td>wmcdcl\PB</td><td>401</td><td>141 s</td></tr><tr><td>wmcdcl+alwaysLA</td><td>405</td><td>177 s</td></tr><tr><td>wmcdcl\simp</td><td>406</td><td>120 s</td></tr><tr><td>wmcdcl</td><td>408</td><td>196 s</td></tr></tbody></table>

Number of optimally solved instances and average time in seconds for different solvers on instances from the Exact Weighted Track of MSE23.

<table><thead><tr><th rowspan="2">Solver</th><th colspan="2">AMD EPYC</th><th colspan="2">MSE23</th></tr><tr><th>#sol</th><th>avg</th><th>#sol</th><th>avg</th></tr></thead><tbody><tr><td>WMaxCDCL1800-S600-HS1200</td><td>439</td><td>283 s</td><td>446</td><td>277 s</td></tr><tr><td>WMaxCDCL1800-S900-HS900</td><td>439</td><td>355 s</td><td>446</td><td>343 s</td></tr><tr><td>EvalMaxSAT-SCIP</td><td>433</td><td>454 s</td><td>442</td><td>405 s</td></tr><tr><td>CASHWMAXSAT-CorePlus</td><td>423</td><td>356 s</td><td>432</td><td>128 s</td></tr><tr><td>CASHWMAXSAT-CorePlus-m</td><td>427</td><td>427 s</td><td>431</td><td>402 s</td></tr><tr><td>EvalMaxSAT</td><td>418</td><td>433 s</td><td>429</td><td>330 s</td></tr><tr><td>CGSS2-SCIP</td><td>417</td><td>260 s</td><td>420</td><td>204 s</td></tr><tr><td>CGSS2</td><td>414</td><td>139 s</td><td>419</td><td>98 s</td></tr><tr><td>WMaxCDCL (wmcdcl\LS)</td><td>383</td><td>135 s</td><td>389</td><td>121 s</td></tr><tr><td>Pacose</td><td>365</td><td>265 s</td><td>372</td><td>256 s</td></tr><tr><td>Pacose-MaxPre2</td><td>348</td><td>201 s</td><td>350</td><td>186 s</td></tr><tr><td>wmcdcl</td><td>408</td><td>196 s</td><td>-</td><td>-</td></tr><tr><td>WMaxCDCL1800</td><td>379</td><td>96 s</td><td>-</td><td>-</td></tr><tr><td>S600</td><td>318</td><td>50 s</td><td>-</td><td>-</td></tr><tr><td>S3600</td><td>350</td><td>182 s</td><td>-</td><td>-</td></tr><tr><td>HS1200</td><td>408</td><td>92 s</td><td>-</td><td>-</td></tr><tr><td>WMaxCDCL1800-S600</td><td>413</td><td>223 s</td><td>-</td><td>-</td></tr><tr><td>WMaxCDCL-HS1200</td><td>433</td><td>197 s</td><td>-</td><td>-</td></tr><tr><td>S600-HS1200</td><td>426</td><td>226 s</td><td>-</td><td>-</td></tr></tbody></table>

WMaxCDCL is a version of WMaxCDCL that excludes the local search preprocessing, allowing us to evaluate a pure implementation of WMaxCDCL without any additional WMPS solver. Thus, the WMaxCDCL solver corresponds to wmcdcl\LS from Section 9.1. The other two solvers initiate the execution of WMaxCDCL by first solving an Integer Linear Programming formulation of the WPMS instance using SCIP (Gamrath et al., 2020). Following this, they run the hitting set-based solver MaxHS (a version obtained from MSE22 (Bacchus, 2022)). For the SCIP phase, we reuse the implementation of the UWrMaxSAT-SCIP solver from MSE22 (Piotrów, 2022). Therefore, the WMaxCDCL1800-S600-HS1200 solver first runs SCIP for 600 s. If the instance is not solved, it then executes MaxHS for 1200 s. If the instance is still unresolved, it subsequently runs WMaxCDCL for 1800 s. The WMaxCDCL1800-S900-HS900 solver operates similarly, with 900 s allocated to both SCIP and MaxHS. In both cases, WMaxCDCL corresponds to wmcdcl\LS, but in this case, the best solution obtained by MaxHS is provided to WMaxCDCL as lsub.

### 9.2.1. MSE23 participants

The top section of Table 2 contains the results of MSE23, considering all the solvers that participated in the evaluation. The number of solved instances (#sol) and average solving time (avg) are reported twice for every solver. In column AMD EPYC, we reproduced the experiments with our machine in order to obtain values comparable to the ones in Section 9.1. Column MSE23 contains the results exactly as reported in MSE23 (Järvisalo et al., 2023). Fig. 3 contains a cactus plot with the results of MSE23 obtained with our machine. With some minor variations, the overall picture remains consistent, though performances

<footnote n="3">³ The solvers WMaxCDCL1800-S600-HS1200 and WMaxCDCL1800-S900-HS900 were named WMaxCDCL-S6-HS12 and WMaxCDCL-S9-HS9, respectively, in MSE23. We have renamed them here to make more explicit their configurations.</footnote>
<figure><img src="image_10.png" /><figcaption>Fig. 3. Cactus plot of the results of MSE23 reproduced with our machine. The solver names appear in the legend of the map sorted decreasingly by number of solved instances within 3600, which corresponds to the maximum x-axis value for each curve.</figcaption></figure>

are slower on our machine. The competition is largely dominated by solvers that combine various complete WPMS solvers. In particular, all solvers, except for EvalMaxSAT, CGSS, WMaxCDCL, Pacose and Pacose-MaxPre2, at least run an Integer Programming solver as a preprocessing step. This approach became widely adopted after MSE21, where the CASHWMaxSAT solver demonstrated that this technique could significantly increase the number of solved instances.

### 9.2.2. Non-combined solvers

When considering only the five pure (non-combined) solvers that participated to MSE23 (i.e.; EvalMaxSAT, CGSS2, WMaxCDCL, Pacose, and Pacose-MaxPre2) we observe that WMaxCDCL(wmcdcl\LS) ranked third, solving 383 (389) instances. This remains true even when the local search preprocessing step is enabled to compute an upper bound (corresponding to the wmcdcl solver in the center section of Table 2, with 408 solved instances). However, in this case, the gap in the number of solved instances compared to EvalMaxSAT and CGSS2 narrows to just 10 and 6 instances, respectively, demonstrating that the WMaxCDCL algorithm is competitive with state-of-the-art SAT-based WPMS solvers.

### 9.2.3. Hybridization of WMaxCDCL

The two solvers that combine SCIP and MaxHS in the first half of the execution time and WMaxCDCL in the second half achieved the first position with 439 (446) solved instances. The complementarity of the different components in these solvers is analyzed at the bottom section of Table 2, where we evaluate all possible combinations of sub-parts of the winner solver, WMaxCDCL1800-S600-HS1200. The name of each solver represents its configuration. For instance, WMaxCDCL1800 is a solver that only runs WMaxCDCL for 1800 s, S600 only runs SCIP for 600 s, and S600-HS1200 first runs SCIP for 600 s, followed by MaxHS for 1200 s if the instance remains unsolved. We also include the standalone performance of SCIP with 3600 s to evaluate the impact of SCIP over solvers using it in MSE23. Our analysis shows that all components are essential for achieving the best-performing configuration. SCIP and MaxHS both use integer linear programming techniques such as dual bounds and cutting planes which WMaxCDCL does not use. Hence, the hybridization of WMaxCDCL with SCIP and MaxHS allows us to take advantage of these ILP techniques which turn out to be effective in solving some kinds of instances. We have identified that indeed there are some families of instances that are more suitable for ILP-based techniques than WMaxCDCL, since WMaxCDCL fails to solve a significant number of instances that can be solved by SCIP or MaxHS. These are correlation clustering (Berg and Järvisalo, 2013), judgment aggregation (Conati et al., 2023), relational inference (Mangal et al., 2016), setcover rail (Lei and Cai, 2020), shift design (Abseher et al., 2015; Martin, 2017) and warehouses (De Givry et al., 2005).

## 10. Conclusions

We have presented, for the first time, a detailed description of the WMaxCDCL algorithm for solving WPMS, as well as particular implementation details in the solver by the same name. The most noticeable difference of WMaxCDCL compared to SAT-based WPMS solvers is the use of fast lower bounding techniques to anticipate soft conflicts at earlier decision levels. This early pruning of the search tree is always explained by means of a conflicting clause, thus obtaining a generalization of the CDCL SAT algorithm capable of solving any MaxSAT variant. In this regard, another contribution of this work is providing a simple yet precise explanation of the main design changes required to transform any state-of-the-art CDCL-based SAT into a WMaxCDCL-based WMPS solver.

WMaxCDCL generalizes the MaxCDCL algorithm from unweighted (Partial) MaxSAT (Li et al., 2021) to WPMS. Note however that WMaxCDCL is not a simple generalization of MaxCDCL. Procedures like lower bound computation, falsified clause generation, and hardening become more complex in WMaxCDCL, as they must handle soft clauses with varying weights, while MaxCDCL only treats soft clauses having a uniform weight of 1. A key point is that, in MaxCDCL, a soft clause can belong to only one core while, in WMPS, a soft clause can belong to several different cores, which imposes several challenges to guarantee the soundness of a lower bound in the lookahead procedure and to keep the pruning power of soft conflict clause. Furthermore, there are numerous design choices that can profoundly impact the performance of WMaxCDCL. Our results demonstrate that these design decisions are critical to the algorithm's efficiency, opening up promising avenues for future research. For example, the strategy to decide when to run lookahead might be improved if we seek not only a high detection of soft conflicts but also intensive and early hardening of soft literals. Also, the potentially large differences between the weights of the clauses can be studied to obtain better soft literal selection strategies in lookahead, using techniques such as stratification, or to design better mechanisms for simplifying soft conflict clauses.

Although WMaxCDCL is a novel approach, our experiments demonstrate that it is competitive with state-of-the-art SAT-based WPMS solvers, which are the result of many years of research. One key factor in this success is the inclusion of clause learning, which makes WMaxCDCL competitive for industrial instances that could not be solved with previously existing WPMS BnB solvers, which have been absent from the MaxSAT Evaluation since 2017. Moreover, we can conclude from our results on combining solving techniques that WMaxCDCL complements the state of the art in WPMS solving. These results suggest that the pursuit of algorithms effectively combining SAT-based techniques
and WMaxCDCL within a single solver is a promising research direction. For instance, a reasonable approach would be to use a WMaxCDCL solver in place of a SAT solver as the oracle in a core-based WPMS solver. This would allow the solver to distinguish between soft clauses to be relaxed in the main core-based algorithm, and soft clauses to be used in a BnB process to find global cores.

WMaxCDCL is an exact solver, and as such it claims that the reported solutions are optimal. However, there is no formal support for this claim in the form of an optimality certificate, hence design or implementation errors might lead to incorrect results. Proof logging has emerged as an effective way of certifying the correctness of results. Most modern SAT solvers are capable of reporting proof logs, since this is currently mandatory for participating in the SAT competition. However, this is still not mandatory in MaxSAT Evaluation, and just very recently some MaxSAT solvers have started including proof logging. At the moment of publishing this work, the implementation of proof logging to WMaxCDCL using cutting planes derivations with the VERIPB proof system (Bogaerts et al., 2023) is work in progress. The theoretical basis has already been presented (Vandesande et al., 2024).

Last but not least, we highlight that the proposed conflict-based clause learning technique holds the potential to be adapted to BnB solvers for other combinatorial optimization problems besides WMPS, such as graph coloring, maximum clique or PB optimization. Consequently, these contributions represent a notable advancement in optimization strategies, with implications for both industrial applications and broader theoretical studies.

## CRediT authorship contribution statement

**Jordi Coll:** Methodology, Conceptualization, Writing – original draft, Resources, Data curation, Software, Formal analysis, Writing – review & editing, Investigation.
**Chu-Min Li:** Software, Investigation, Data curation, Project administration, Writing – original draft, Funding acquisition, Conceptualization, Writing – review & editing, Methodology, Formal analysis.
**Shuolin Li:** Writing – original draft, Investigation, Formal analysis, Conceptualization, Writing – review & editing, Data curation, Software.
**Djamal Habet:** Writing – original draft, Formal analysis, Writing – review & editing, Project administration, Funding acquisition, Investigation, Conceptualization.
**Felip Manyà:** Writing – original draft, Investigation, Methodology, Conceptualization, Writing – review & editing, Funding acquisition.

## Acknowledgments

This work has been supported by grants PID2022-139835NB-C21 and PID2021-122274OB-I00 funded by MCIN/AEI/10.13039/5011000-11033 and by ERDF, EU, and by grant ANR-19-CHIA-0013-01 co-funded by the French Agence Nationale de la Recherche and the French electricity distribution network manager Enedis. F. Manyà was supported by mobility grant PRX23/00344 of the Ministerio de Ciencia, Innovación y Universidades, Spain. We thank the Université de Picardie Jules Verne for providing the Matrics Platform.

## Data availability

The provided link contains the software involved in this paper, including the software and the instructions and necessary data to reproduce the experiments.

Source code and input parameters (Original data) (GitHub)

## References

Abramé, A., Habet, D., 2014. Ahmaxsat: Description and evaluation of a branch and bound Max-SAT solver. J. Satisf. Boolean Model. Comput. 9, 89–128.

Abseher, M., Gebser, M., Musliu, N., Schaub, T., Woltran, S., 2015. Shift design with answer set programming. LPNMR 2015, In: Logic Programming and Nonmonotonic Reasoning - 13th International Conference, vol. 9345, pp. 32–39.

Ánsótegui, C., Bonet, M.L., Gabàs, J., Levy, J., 2012. Improving SAT-based weighted MaxSAT solvers. In: 18th International Conference on Principles and Practice of Constraint Programming. CP 2012, pp. 86–101.

Ánsótegui, C., Bonet, M.L., Levy, J., 2009. Solving (weighted) partial MaxSAT through satisfiability testing. In: Theory and Applications of Satisfiability Testing. SAT 2009, Springer LNCS 5584, pp. 427–440.

Ánsótegui, C., Bonet, M.L., Levy, J., 2010. A new algorithm for weighted partial MaxSAT. Proceedings of the AAAI Conference on Artificial Intelligence 24 (1), 3–8.

Ánsótegui, C., Bonet, M.L., Levy, J., 2013. SAT-based MaxSAT algorithms. Artificial Intelligence 196, 77–105.

Ánsótegui, C., Gabàs, J., 2017. WPM3: An (in)complete algorithm for weighted partial MaxSAT. Artificial Intelligence 250, 37–57.

Ánsótegui, C., Manyà, F., Ojeda, J., Salvia, J.M., Torres, E., 2022. Incomplete MaxSAT approaches for combinatorial testing. J. Heuristics 28 (4), 377–431.

Audemard, G., Simon, L., 2009. Predicting learnt clauses quality in modern SAT solvers. In: Twenty-First International Joint Conference on Artificial Intelligence. IJCAI 2009, pp. 399–404.

Avellaneda, F., 2023. EvalMaxSAT 2023. In: MaxSAT Evaluation 2023. p. 12.

Bacchus, F., 2020. MaxHS in the 2020 MaxSAT Evaluation. In: MaxSAT Evaluation 2020: Solver and Benchmark Descriptions. pp. 19–20.

Bacchus, F., 2022. MaxHS in the 2022 MaxSAT evaluation. In: MaxSAT Evaluation 2022. p. 17.

Bacchus, F., Hyttinen, A., Järvisalo, M., Saikko, P., 2017. Reduced cost fixing in MaxSAT. In: Principles and Practice of Constraint Programming. CP 2017. In: Springer LNCS, pp. 641–651.

Bacchus, F., Järvisalo, M., Ruben, M., 2021. Maximum satisfiability. In: Handbook of Satisfiability, second ed. IOS Press, pp. 929–991.

Berg, J., Bacchus, F., Poole, A., 2020. Abstract cores in implicit hitting set MaxSat solving. In: Pulina, L., Seidl, M. (Eds.), Theory and Applications of Satisfiability Testing. SAT 2020, In: Lecture Notes in Computer Science, vol. 12178, Springer, pp. 277–294.

Berg, J., Järvisalo, M., 2013. Optimal correlation clustering via MaxSAT. In: 2013 IEEE 13th International Conference on Data Mining Workshops. IEEE, pp. 750–757.

Berg, J., Järvisalo, M., 2017. Weight-aware core extraction in SAT-based MaxSAT solving. In: Twenty-third International Conference on Principles and Practice of Constraint Programming. CP 2017, Springer, pp. 652–670.

Bofill, M., Coll, J., Garcia, M., Giráldez-Cru, J., Pesant, G., Suy, J., Villaret, M., 2022a. Constraint solving approaches to the business-to-business meeting scheduling problem. J. Artificial Intelligence Res. 74, 263–301.

Bofill, M., Coll, J., Nightingale, P., Suy, J., Ulrich-Oltean, F., Villaret, M., 2022b. SAT encodings for pseudo-boolean constraints together with at-most-one constraints. Artificial Intelligence 302, 103604.

Bofill, M., Coll, J., Suy, J., Villaret, M., 2020. An MDD-based SAT encoding for pseudo-boolean constraints with at-most-one relations. Artif. Intell. Rev. 53 (7), 5157–5188.

Bogaerts, B., Gocht, S., McCreesh, C., Nordström, J., 2023. Certified dominance and symmetry breaking for combinatorial optimisation. J. Artificial Intelligence Res. 77, 1539–1589, Preliminary version in AAAI '22.

Chai, D., Kuehlmann, A., 2003. A fast pseudo-boolean constraint solver. In: Proceedings of the 40th Annual Design Automation Conference. pp. 830–835.

Cherif, M.S., Habet, D., Abramé, A., 2020. Understanding the power of Max-SAT resolution through UP-resilience. Artificial Intelligence 289, 103397.

Conati, A.F., Niskanen, A., Järvisalo, M., 2023. Sat-based judgment aggregation. In: International Conference on Autonomous Agents and Multiagent Systems. ACM, pp. 1412–1420.

Cook, S.A., 1971. The complexity of theorem-proving procedures. In: Proceedings of the 3rd Annual ACM Symposium on Theory of Computing. ACM, pp. 151–158.

Davies, J., Bacchus, F., 2011. Solving MAXSAT by solving a sequence of simpler SAT instances. In: Seventeenth International Conference on Principles and Practice of Constraint Programming. CP 2011. Springer, pp. 225–239.

Davies, J., Bacchus, F., 2013. Exploiting the power of MIP solvers in MAXSAT. In: Theory and Applications of Satisfiability Testing. SAT 2013, Springer, pp. 166–181.

De Givry, S., Heras, F., Zytnicki, M., Larrosa, J., 2005. Existential arc consistency: Getting closer to full arc consistency in weighted CSPs. In: Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence, IJCAI 2005, pp. 84–89.

Devriendt, J., 2020. Watched propagation of integer linear constraints. In: Twenty-Sixth International Conference on Principles and Practice of Constraint Programming. CP 2020. Springer, pp. 160–176.

Devriendt, J., Gocht, S., Demirović, E., Nordström, J., Stuckey, P.J., 2021. Cutting to the core of pseudo-boolean optimization: Combining core-guided search with cutting planes reasoning. In: Proceedings of the AAAI Conference on Artificial Intelligence, vol. 35, pp. 3750–3758.
Dixon, H.E., Ginsberg, M.L., 2002. Inference methods for a pseudo-boolean satisfiability solver. In: Proceedings of the AAAI Conference on Artificial Intelligence. 18, pp. 635-640.

Elffers, J., Nordström, J., 2018. Divide and conquer: Towards faster pseudo-boolean solving. In: Proceedings of the Twenty-seventh International Joint Conference on Artificial Intelligence. pp. 1291-1299.

Fang, Z., Li, C., Xu, K., 2016. An exact algorithm based on maxsat reasoning for the maximum weight Anderson problem. J. Artificial Intelligence Res. 55, 799-833.

Gamrath, G., Anderson, D., Bestuzheva, K., Chen, W.K., Eifler, L., Gasse, M., Gemander, P., Gleixner, A., Gottwald, L., Halbig, K., Hendel, G., Hojny, C., Koch, T., Le Bodic, P., Maher, S.J., Matter, F., Miltenberger, M., Mühmer, E., Müller, B., Pfetsch, M.E., Schlösser, F., Serrano, F., Shinano, Y., Tawfik, C., Vigerske, S., Wegscheider, F., Weninger, D., Witzig, J., 2020. The SCIP Optimization Suite 7.0. ZIB-Report 20-10, Zuse Institute Berlin, URL http://nbn-resolving.de/urn:nbn:de:0297-zib-78023.

Heras, F., Larrosa, J., Oliveras, A., 2008. MiniMaxSAT: An efficient weighted Max-SAT solver. J. Artificial Intelligence Res. 31, 1-32.

Ignatiev, A., Morgado, A., Marques-Silva, J., 2019. RC2: an efficient MaxSAT solver. J. Satisf. Boolean Model. Comput. 11 (1), 53-64.

Ihalainen, H., Berg, J., Järvisalo, M., 2021. Refined core relaxation for core-guided MaxSAT solving. In: 27th International Conference on Principles and Practice of Constraint Programming. CP 2021, pp. 28:1-18.

Järvisalo, M., Berg, J., Martins, R., Niskanen, A., 2023. MaxSAT evaluation 2023 website. https://maxsat-evaluations.github.io/2023/descriptions.html. (Accessed October 2024).

Koshimura, M., Zhang, T., Fujita, H., Hasegawa, R., 2012. QMaxSAT: A partial Max-SAT solver. J. Satisf. Boolean Model. Comput. 8 (1/2), 95-100.

Kuegel, A., 2010. Improved exact solver for the Weighted MAX-SAT problem. In: Proceedings of Workshop Pragmatics of SAT. POS-10, pp. 15-27.

Le Berre, D., Parrain, A., 2011. The sat4j library, release 2.2: System description. J. Satisf. Boolean Model. Comput. 7 (2-3), 59-64.

Lei, Z., Cai, S., 2020. Solving set cover and dominating set via maximum satisfiability. In: Proceedings of the AAAI Conference on Artificial Intelligence, vol. 34, pp. 1569-1576.

Lei, Z., Cai, S., Geng, F., Wang, D., Peng, Y., Wan, D., Deng, Y., Lu, P., 2021a. SATLike-c: Solver description. In: MaxSAT Evaluation 2021. p. 19.

Lei, Z., Cai, S., Wang, D., Peng, Y., Geng, F., Wan, D., Deng, Y., Lu, P., 2021b. CASHWMaxSAT: Solver description. In: MaxSAT Evaluation 2021. pp. 8-9.

Li, C.M., Fang, Z., Jiang, H., Xu, K., 2018. Incremental upper bound for the maximum clique problem. INFORMS Journal on Computing 30 (1), 137-153.

Li, C.M., Manyà, F., 2021. MaxSAT, hard and soft constraints. In: Handbook of Satisfiability, second ed. IOS Press, pp. 903-927.

Li, C.M., Manyà, F., Planes, J., 2007. New inference rules for Max-SAT. J. Artificial Intelligence Res. 30, 321-359.

Li, C.M., Manya, F., Quan, Z., Zhu, Z., 2010. Exact minsat solving. In: International Conference on Theory and Applications of Satisfiability Testing (SAT-2010). pp. 363-368.

Li, C.-M., Xiao, F., Luo, M., Manyà, F., Lü, Z., Li, Y., 2020. Clause vivification by unit propagation in CDCL SAT solvers. Artificial Intelligence 279, 103197.

Li, C.M., Xu, Z., Coll, J., Manyà, F., Habet, D., He, K., 2021. Combining clause learning and branch and bound for MaxSAT. In: Twenty-seventh International Conference on Principles and Practice of Constraint Programming. CP 2021, pp. 38:1-18.

Li, C.M., Xu, Z., Coll, J., Manyà, F., Habet, D., He, K., 2022. Boosting branch-and-bound MaxSAT solvers with clause learning. AI Commun. 35 (2), 131-151.

Luo, M., Li, C., Xiao, F., Manyà, F., Lü, Z., 2017. An effective learnt clause minimization approach for CDCL SAT solvers. In: Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence. IJCAI 2017, pp. 703-711.

Mangal, R., Zhang, X., Kamath, A., Nori, A., Naik, M., 2016. Scaling relational inference using proofs and refutations. In: Proceedings of the AAAI Conference on Artificial Intelligence, vol. 30, pp. 3278-3286.

Manquinho, V.M., Silva, J.P.M., Planes, J., 2009. Algorithms for weighted boolean optimization. In: Theory and Applications of Satisfiability Testing. SAT 2009, Springer, pp. 495-508.

Manyà, F., Negrete, S., Roig, C., Soler, J.R., 2020. Solving the team composition problem in a classroom. Fundam. Inform. 174 (1), 83-101.

Marques-Silva, J., Argelich, J., Graça, A., Lynce, I., 2011. Boolean lexicographic optimization: algorithms & applications. Ann. Mat. Artif. Intell. 62 (3-4), 317-343.

Marques-Silva, J., Lynce, I., Malik, S., 2021. Conflict-driven clause learning SAT solvers. In: Handbook of Satisfiability, second ed. IOS Press, pp. 929-991.

Marques-Silva, J., Manquinho, V.M., 2008. Towards more effective unsatisfiability-based maximum satisfiability algorithms. In: Theory and Applications of Satisfiability Testing. SAT 2008, Springer, pp. 225-230.

Martin, R., 2017. ASP to MaxSAT: Metro, shiftdesign, timetabling and biorepair. In: Proceedings of the MaxSAT Evaluation 2017. p. 27.

Martins, R., Manquinho, V.M., Lynce, I., 2014. Open-WBO: A modular MaxSAT solver. In: Theory and Applications of Satisfiability Testing - SAT 2014. In: LNCS, vol. 8561, Springer, pp. 438-445.

MSE, 2024. MaxSAT evaluation website. https://maxsat-evaluations.github.io. (Accessed October 2024).

Narodytska, N., Bacchus, F., 2014. Maximum satisfiability using core-guided MaxSAT resolution. Proceedings of the AAAI Conference on Artificial Intelligence 28 (1), 2717-2723.

Nieuwenhuis, R., Oliveras, A., Rodríguez-Carbonell, E., Zhao, R., 2024. Speeding up pseudo-boolean propagation. SAT 2024, In: 27th International Conference on Theory and Applications of Satisfiability Testing, vol. 305, pp. 22:1-22:18.

Papadimitriou, C.H., 1994. Computational Complexity. Addison-Wesley.

Paxian, T., Becker, B., 2020. Pacose: An iterative SAT-based MaxSAT solver. In: MaxSAT Evaluation 2020: Solver and Benchmark Descriptions. p. 12.

Piotrów, M., 2022. Uwrmaxsat entering the maxsat evaluation 2022. In: MaxSAT Evaluation 2022. pp. 21-22.

Saikko, P., Berg, J., Järvisalo, M., 2016. LMHS: a SAT-IP hybrid MaxSAT solver. In: Theory and Applications of Satisfiability Testing. SAT 2016, In: LNCS, vol. 9710, Springer, pp. 539-546.

Vandesande, D., Coll, J., Li, C.M., Bogaerts, B., 2024. Certified branch-and-bound maxsat solving. First Int. Work. Discret. Optim. Soft Constraints URL https://we b-genobioinfo.toulouse.inrae.fr/~degivry/soft2024/final/CollSoft2024.pdf.

Zha, A., 2020. QMaxSAT in MaxSAT evaluation 2018. In: Proceedings of the MaxSAT Evaluation 2020. p. 16.

Zhang, L., Bacchus, F., 2012. MAXSAT heuristics for cost optimal planning. In: Proceedings of the 26th AAAI Conference on Artificial Intelligence. pp. 1846-1852.

Zheng, J., He, K., Zhou, J., Jin, Y., Li, C., Manyà, F., 2022. BandMaxSAT: A local search MaxSAT solver with multi-armed bandit. In: Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence. IJCAI 2022, pp. 1901-1907.