Abstract
The Maximum Satisfiability Problem, or MaxSAT, offers a suitable problem solving formalism for combinatorial optimization problems. Nevertheless, MaxSAT solvers implementing the Branch-and-Bound (BnB) scheme have not succeeded in solving challenging real-world optimization problems. It is widely believed that BnB MaxSAT solvers are only superior on random and some specific crafted instances. At the same time, SAT-based MaxSAT solvers perform particularly well on real-world instances. To overcome this shortcoming of BnB MaxSAT solvers, this paper proposes a new BnB MaxSAT solver called MaxCDCL. The main feature of MaxCDCL is the combination of clause learning of soft conflicts and an efficient bounding procedure. Moreover, the paper reports on an experimental investigation showing that MaxCDCL is competitive when compared with the best performing solvers of the 2020 MaxSAT Evaluation. MaxCDCL performs very well on real-world instances, and solves a number of instances that other solvers cannot solve. Furthermore, MaxCDCL, when combined with the best performing MaxSAT solvers, solves the highest number of instances of a collection from all the MaxSAT evaluations held so far.
Keywords
Introduction
The Maximum satisfiability problem (MaxSAT) is an optimization version of the satisfiability problem (SAT) and offers a suitable problem solving formalism for combinatorial optimization problems thanks to the availability of fast solvers. MaxSAT solvers are divided into two categories: exact algorithms, which return optimal solutions and prove their optimality, and heuristic algorithms, which quickly find solutions of good quality without guaranteeing their optimality.
This paper focuses on exact algorithms for MaxSAT and, more specifically, focuses on Branch-and-Bound (BnB) MaxSAT solvers [37]. The first modern BnB MaxSAT solvers [4,18] inspired a new generation of BnB MaxSAT solvers like MaxSatz [40], MiniMaxSat [27], Ahmaxsat [1,20] and Akmaxsat [30]. These solvers produced excellent performance improvements thanks to adding local propagation based on MaxSAT resolution refinements [26,35,40] and incorporating lower bound computation methods that detect disjoint inconsistent subsets with unit progation [38,39]. Nevertheless, they were not as powerful on real-world instances as the SAT-based MaxSAT solvers developed since 2006 [15] after the seminal work of Fu and Malik [24]. Thus, the prevailing opinion in the community is that BnB MaxSAT solvers only perform well on random and some specific crafted instances.
In our view, the lack of clause learning in BnB MaxSAT solvers might explain their poor performance on real-world instances. Unfortunately, it is difficult to exploit clause learning in BnB MaxSAT solvers. In CDCL (Conflict-Driven Clause Learning) SAT solvers, backtracking occurs when a conflict is detected, and then a clause is learnt from a sequence of resolution steps. However, BnB MaxSAT solvers also need to backtrack when the solver computes a lower bound equal to the upper bound. In this case, no clause is explicitly unsatisfied, making it hard to learn a clause. Probably due to this difficulty, no significant progress has been made to speed up BnB MaxSAT solvers in the past few years, as illustrated by their absence in the annual MaxSAT Evaluation since 2017.
This paper proposes an original approach that allows a BnB MaxSAT solver to learn a clause when it computes a lower bound equal to the upper bound, together with a new bounding procedure that is especially well suited for large instances. This approach is implemented in a new BnB MaxSAT solver called MaxCDCL, which combines the new bounding procedure and clause learning. The experimental results show that MaxCDCL is competitive when compared with the best performing solvers of the 2020 MaxSAT Evaluation. MaxCDCL performs very well on real-world instances, and solves a number of instances that other solvers cannot solve. Furthermore, MaxCDCL, when combined with the best performing MaxSAT solvers, solves the highest number of instances of a collection from all the MaxSAT evaluations held so far.
This paper is an extended version of [34], presented at CP-2021, that describes an earlier version of MaxCDCL. It is organized as follows: Section 2 presents the preliminaries. Section 3 reviews state-of-the-art MaxSAT solvers. Section 4 describes the basic scheme of the state-of-the-art BnB MaxSAT solvers. Section 5 describes MaxCDCL. Section 6 empirically evaluates and analyzes MaxCDCL. Section 7 presents the concluding remarks.
Preliminaries
A propositional variable x can take values 0 or 1 (false or true). A literal is a variable x or its negation
MaxSAT is the problem of finding an assignment that satisfies the maximum number of clauses in a given multiset of clauses. In Partial MaxSAT, there are hard and soft clauses, and the goal is to satisfy all the hard clauses and the maximum number of soft clauses. In Weighted (Partial) MaxSAT, each soft clause has a cost to pay if it is violated. This paper considers MaxSAT and Partial MaxSAT, but not Weighted MaxSAT and Weighted Partial MaxSAT.
The state-of-the-art SAT solvers implement the CDCL algorithm. CDCL alternates a search phase, where literals are assigned until either a solution or a conflict is found, and a learning phase, which is executed after finding a conflict in order to learn a new clause. Unit Propagation (UP) is the main inference rule applied during the search: If there is a unit clause

Example of implication graph.
Figure 1 shows an example of implication graph. It is a directed acyclic graph where each node represents an assignment l@
Concretely, when a conflict is found in the decision level
The learnt clause explains the conflict: when all its literals are unsatisfied, unit propagation reproduces the implication graph to derive the same conflict. So, adding the learnt clause prevents the same conflict in the future search. After learning a clause, CDCL backtracks to the second highest decision level of the learnt clause (level 4 in the above example). Unsatisfiability is determined when a conflict is found at decision level 0.
A major difference between MaxSAT and SAT is that each clause must be satisfied in a SAT solution while a soft clause can be unsatisfied in an optimal MaxSAT solution. Thus, a SAT solving technique must preserve satisfiability while a MaxSAT solving technique must preserve the minimum number of unsatisfied clauses. This implies that UP applied to soft unit clauses is unsound in MaxSAT because it does not preserve the minimum number of unsatisfied clauses. Despite this, the MaxSAT community has made enormous efforts to implement exact MaxSAT solvers with impressive performance over the last decade [15,37]. On the other hand, heuristic MaxSAT algorithms such as SatLike [32] have also been proposed.
Roughly speaking, we find two main groups of exact MaxSAT solvers: branch-and-bound (BnB) and SAT-based solvers. BnB MaxSAT solvers, described in detail in Section 4, implement the branch-and-bound scheme. At each node of the search tree, they apply some inference rules and compute a lower bound by detecting disjoint inconsistent subsets of soft clauses with unit propagation [37]. Representative BnB solvers are MaxSatz [40], MiniMaxSat [27], Ahmaxsat [1,20] and Akmaxsat [30]. Closely related to MaxSAT, we can find BnB solvers for the Weighted Constraint Satisfaction Problem (WCSP). Recently, a technique to improve BnB WCSP solving by avoiding branching on variables which are unlikely to increase the lower bound was presented [56].
SAT-based MaxSAT solvers proceed by reformulating the MaxSAT optimization problem into a sequence of SAT decision problems [15]. These solvers could still be divided into three subgroups: model-guided, core-guided and Minimum Hitting Sets (MHS-)guided. Model-guided approaches reduce the problem of deciding whether there exists an assignment for the MaxSAT instance with a cost less than or equal to a given k to SAT, and successively decrease k until an unsatisfiable SAT instance is found. Among such solvers we find SAT4J-Maxsat [31], QMaxSat [29,58], Open-WBO [48] or Pacose [52]. Core-guided and MHS-guided approaches consider a MaxSAT instance as a SAT instance and call a CDCL SAT solver to identify an unsatisfiable subset of soft clauses, called a core. Then, they relax this core and solve the relaxed instance with a CDCL SAT solver to identify another core, repeating this process until deriving a satisfiable instance. The difference between them is that core-guided solvers relax a core using cardinality constraints, while MHS-guided solvers remove one clause from each detected core so that the number of different clauses removed from the cores is minimized by solving a minimum hitting set instance with an integer programming solver. The solvers msu1.2 [47], WBO [44], Open-WBO [48], WPM1 [7], PM2 [9], WPM2 [8], WPM3 [10], Eva [50], and RC2 [28] are among the most representative core-guided solvers, and the solvers MHS [53] and MaxHS [12,14,21,22] are among the most representative MHS-guided solvers. Core-guided search has also been extended to constraint programming [25].
A common feature of SAT-based MaxSAT solvers is that they indirectly exploit conflict-driven clause learning by repeatedly calling a CDCL SAT solver. Nevertheless, BnB MaxSAT solvers cannot easily exploit clause learning, which might explain their poor performance on real-world optimization problems. A first attempt to incorporate clause learning in BnB MaxSAT solvers was proposed in [3]: when the number of unsatisfied soft clauses reaches the upper bound, the violation of these soft clauses is analyzed to learn a clause, but no clause is learnt when the lookahead procedure returns a lower bound equal to the upper bound. The results reported in [3] were not competitive.
Branch-and-bound MaxSAT solvers
The state-of-the-art BnB MaxSAT solvers implement variants of the following branch and bound (BnB) scheme: Given a MaxSAT instance ϕ, BnB explores the search tree that represents the space of all possible assignments for ϕ in a depth-first manner. At each node, BnB compares the upper bound (

A basic branch and bound algorithm for MaxSAT
Algorithm 1 shows the pseudo-code of a basic solver for MaxSAT, using the following notation:
Modern BnB MaxSAT solvers implement the basic algorithm augmented with powerful inference techniques, good quality lower bounds, clever variable selection heuristics, and efficient data structures. Partial BnB MaxSAT solvers are also augmented with learning of hard clauses and non-chronological backtracking.
The simplest method to compute a lower bound consists in just counting the number of clauses that are unsatisfied by the current partial assignment [18]. One step forward is to incorporate an underestimation of the number of clauses that will become unsatisfied if the current partial assignment is extended to a complete assignment. The best performing solvers use variants of UP [38], which is a method based on unit propagation.
In UP, the underestimation of the lower bound is the number of disjoint inconsistent subformulas that can be detected with unit propagation. UP works as follows: It applies unit propagation until a contradiction is derived. Then, UP identifies, by inspecting the implication graph, a subset of clauses from which a unit refutation can be constructed, and tries to identify new contradictions from the remaining clauses. The order in which unit clauses are propagated has a notable impact on the quality of the lower bound [39].
UP can be enhanced with failed literal detection as follows: Given a MaxSAT instance ϕ and a variable x occurring positively and negatively in ϕ, UP is applied to both
Nowadays, UP-based lower bounds are the prevailing approach to computing underestimations in branch-and-bound MaxSAT solvers like ahmaxsat [2], MaxSatz [40], and MiniMaxSat [27].
A variant of UP enhanced with failed literal detection was implemented in the solver akmaxsat [30]. It can be the case that UP derives a contradiction from
Improving the lower bound with inference
Another way to improve the quality of the lower bound consists in applying inference rules that transform a MaxSAT instance ϕ into an equivalent but simpler MaxSAT instance
A MaxSAT inference rule is sound if it transforms an instance ϕ into an equivalent instance
The amount of inference enforced by existing BnB MaxSAT solvers at each node of the proof tree is poor compared with the inference enforced by SAT solvers. The simplest inference enforced, when branching on a literal l, consists in applying the one-literal rule: The clauses containing l are removed from the instance and the occurrences of
The following are simple inference rules that have proved to be useful in a number of solvers [4–6,18,54,57]:
The pure literal rule [18]: If a literal only appears with either positive or negative polarity in a MaxSAT instance, all the clauses containing that literal are removed.
The dominating unit clause rule [51]: If the number of clauses (of any length) in which a literal l appears is not greater than the number of unit clauses in which
The complementary unit clause rule [51]: If a MaxSAT instance contains a unit clause with the literal l and a unit clause with the literal
The almost common clause rule [16]: If a MaxSAT instance contains a clause
The resolution rule applied in SAT (i.e., derive
MaxCDCL: A BnB algorithm using CDCL for MaxSAT
This section first presents the general structure of MaxCDCL, and then the different components of MaxCDCL. Compared with the MaxSAT solvers of Section 4, MaxCDCL inagurates a new generation of BnB MaxSAT solvers. At the same time, MaxCDCL opens new research directions in MaxSAT solving.
General structure of MaxCDCL

We distinguish between hard and soft conflicts in the MaxSAT context. A hard conflict occurs when the current partial assignment unsatisfies a hard clause, meaning that an unfeaasible solution has been detected. Given an upper bound UB, a soft conflict occurs when the current partial assignment cannot be extended to a complete one unsatisfying fewer than UB soft clauses. A CDCL SAT solver only considers hard conflicts, learns a hard clause from each hard conflict and backtracks. A BnB CDCL MaxSAT solver extends the CDCL SAT solver by also learning a hard clause from each discovered soft conflict and backtracks.
Algorithm 2 depicts MaxCDCL, which is the BnB CDCL MaxSAT solver proposed in this paper. Given a MaxSAT instance with a set of hard clauses and a set of soft clauses, MaxCDCL works with H and S. H contains the hard clauses and S contains a new literal y for each soft clause
MaxCDCL is like a CDCL SAT solver except for two points. First, when UP does not unsatisfy any hard clause in the UPLA procedure, it calls, under certain condition, a lookahead (LA) procedure to compute a lower bound
Note that model-guided MaxSAT solvers also set an UB in their search. However, they do not compute a lower bound to discover soft conflicts as MaxCDCL. Consequently, MaxCDCL is able to backtrack much earlier than model-guided MaxSAT solvers for a given UB. See the next subsection for details and illustrative examples.
A subset of soft literals
Let
Proposition 1 provides the foundation of our approach in the general case.
Let H be a set of hard clauses, let
It is easy to see that
Given a partial assignment F of H, the application of Proposition 1 consists in first detecting a local core

The detection of a local core
Concretely, MaxCDCL calls Algorithm 3 at decision level
Inspecting G, let
Note that, when

Implication graphs involved in the detection of
Let
If no variable is assigned, all soft literals can be simultaneously satisfied. So, no global core exists. Let the current partial assignment be
Assume that
After propagating
Since
Since
Proposition 1 also provides the basis for hardening. If
If
Existing BnB MaxSAT solvers usually tackle random or crafted instances of limited size and look ahead at each branch. However, such a treatment might be too costly and useless for large instances. If the lower bound is not tight enough to prune the current branch, the time spent to compute the lower bound is lost. When
MaxCDCL uses a probing strategy to determine if lookahead has to be applied at the current branch. With probability p, where p is a parameter intuitively fixed to 0.01, lookahead is applied for probing purpose. The mean
Inspired by the 68-95-99.7 rule in statistics, which says that the values within one (two, three) standard deviation of the mean account for about 68% (95%, 99.7%) of a normal data set, we reasonably assume that the number of cores detected in a successful lookahead is probably lower than
Concretely,
Soft literal ordering in lookahead
Existing BnB MaxSAT solvers such as MaxSatz usually propagate soft unit clauses in the ordering these clauses become unit, or in their ordering in the input formula when detecting disjoint cores [38]. MaxCDCL propagates first the soft literals in the cores detected in the previous lookahead. We selected this ordering for two intuitive reasons.
Before backtracking, a local core detected in the previous lookahead continues being a core. Re-detecting a previous local core allows obtaining a possibly smaller local core due to additional assignments.
After backtracking, re-detecting local cores in the previous soft conflict can allow detecting a new soft conflict sharing many local cores with the previous conflict. In this way, the clauses learnt from consecutive soft conflicts allow to intensify the search, because the clause learnt from a soft conflict is derived from the reasons of the detected cores.
The quality of a clause learnt from a soft conflict highly depends on the detected cores, which in turn highly depends on the soft literal ordering. How to improve the quality of the learnt clause by improving the soft literal ordering definitely deserves further investigation.
Improving the VSIDS heuristic by lookahead
When there is no unit clause, a CDCL SAT solver chooses a free literal l using a decision heuristic, satisfies l and then performs unit propagation. VSIDS [49] is one of the widely used decision heuristics: it initializes the score of each variable to 0 and then, at each conflict, increases the score of each variable in a path to the conflict in the implication graph by
VSIDS is also used in MaxCDCL by increasing the score of a variable in a soft or hard conflict as in a CDCL SAT solver, but is modified as follows by taking lookahead into account. Each time the lookahead procedure detects a local core, the score of the variables encountered when identifying the reason of the core (see Section 5.2) is increased by
Implementation of MaxCDCL
Since MaxCDCL can be considered as an extension of a CDCL SAT solver, it is implemented on top of the CDCL SAT solver MapleCOMSPS_LRB [41], winner of the application track of SAT competition 2016. We chose MapleCOMSPS_LRB because it was one of the best SAT solvers with deterministic behavior when we started this work in 2017. Nevertheless, some of the recent advances in SAT solving are incorporated, including:1
The source code of MaxCDCL is available at
The approach from [33,43] is applied to minimize the learnt clauses.
The clause size reduction with the all-UIP learning technique from [23] is applied to reduce the clauses learnt from soft conflicts. This technique is particularly useful for MaxCDCL because a clause learnt from a soft conflict is usually longer than a clause learnt from a hard conflict. The all-UIP technique allows to significantly reduce the size of a clause learnt from a soft conflict.
The learnt clause management technique proposed in [55] is incorporated into MaxCDCL, allowing to keep more learnt clauses in the clause database.
Assume that
We plan to implement MaxCDCL on top of Kissat [17], the winner of the SAT2020 competition, which might further improve its performance.
The SAT solver MapleCOMSPS_LRB inherits its preprocessing from MiniSAT. Roughly speaking, let x be a variable, let
The preprocessing is extended to MaxCDCL as follows:
A literal l is said to be pure in the input formula if
For each variable x not occurring in any soft clause, apply the preprocessing of MiniSAT in the same conditions (i.e. with the same parameters α and β).
Obviously, an optimal solution of the original formula is also an optimal solution of the simplified formula, and vice versa.
Failed literal detection
A literal l is failed in the set of all hard clauses H if UP deduces an empty clause in
Concretely, MaxCDCL repeatedly selects the free variable x with the highest VSIDS score (if it is in a VSIDS phase) or the highest LRB score (if it is in a LRB phase) that has not yet been detected, and then performs UP in
Experimental evaluation
We report on an experimental investigation to assess the performance of MaxCDCL. We ran all experiments with Intel Xeon CPUs E5-2680@2.40GHz under Linux with 32GB of memory, using the following benchmark sets unless otherwise stated:
The cutoff time is one hour (3600 s) per instance as in the MaxSAT Evaluation. For MaxCDCL and its variants, this time includes 60 seconds to find a feasible upper bound
The experiments are presented as follows. Firstly, we analyse the impact of the components implemented in MaxCDCL. Secondly, we compare the performance of MaxCDCL with that of the top 5 solvers in MSE2020. Thirdly, we show the complementarity of MaxCDCL with the top 5 solvers by comparing the number of instances solved using a portfolio solver with and without MaxCDCL. Finally, we compare MaxCDCL with a state-of-the-art BnB solver.
Table 1 compares MaxCDCL with the following variants:
MaxCDCL without lookahead, i.e. the condition to lookahead is never satisfied in line 3 of Algorithm 3. Note that after finding a feasible UB, MaxCDCL∖LA performs linear SAT-UNSAT search as a model-guided SAT-based MaxSAT solver.
MaxCDCL without hardening (i.e., lines 13 and 14 in Algorithm 2 are removed).
MaxCDCL that looks ahead at each branch, i.e., the condition to lookahead is always satisfied in line 3 of Algorithm 3.
MaxCDCL that, when detecting cores in lookahead, always propagates the soft literals in the ordering as the corresponding soft clauses occur in the input instance.
MaxCDCL that does not increase the VSIDS score of the variables contributing to a local core detected in lookahead as described in Section 5.5.
MaxCDCL that does not perform the preprocessing described in Section 5.7.
MaxCDCL that does not perform the failed literal detection described in Section 5.8.
Comparison of MaxCDCL with its variants for MSE19∪20 (left) and MC (right)
Comparison of MaxCDCL with its variants for MSE19∪20 (left) and MC (right)
In Table 1, columns “#solv” give the number of solved instances and columns “avg” give the mean time in seconds (including the 60 s used by SatLike) needed to solve these instances. These results indicate that a careful configuration combining clause learning and BnB is crucial for the performance of MaxCDCL, including hardening based on local core detection and clause learning, the selective and adaptive application of lookahead, and the ordering used to propagate the soft literals when detecting local cores. The lack of any of these components implies that a significant number of instances are out of reach of MaxCDCL. Without this configuration, MaxCDCL∖LA solves 231 instances less than MaxCDCL in MES19∪20 and 848 instances less than MaxCDCL in MC. Note that although the hardening of a soft literal requires a distinct learnt clause, it does not increase the total memory usage because it reduces the search space and therefore avoids many learnt clauses.
Recall that the most fundamental technique of the configuration is clause learning from soft conflicts. We computed the average length of a clause learnt from a soft (hard) conflict for each solved instance by MaxCDCL in MSE19∪20, and found that the median average length of a clause learnt from a soft (hard) conflict is 23.67 (19.2) among the 736 instances solved in the set. Note that the learnt clause length averaged across the 736 instances does not make sense because it is biased by few instances with very long learnt clause length.

Comparison of the success rate of lookahead procedure. Each point is a different instance of MSE19∪20. In the left-most plot, a point

Cumulative distribution of the success rates of the lookahead method. A point
The impact of the new probing strategy presented in Section 5.3 is illustrated in Figs 3 and 4. They analyse the rate of lookahead calls that detect a soft conflict (i.e.,
In addition, the comparison of MaxCDCL with MaxCDCL∖VSIDSbyLA suggests that the VSIDS heuristic might be improved by lookahead, indicating a promising research direction.
To complete this subsection, we mention the impact of two other components of MaxCDCL: (i) the computation of a feasible UB with the local search solver SatLike during preprocessing allows MaxCDCL to solve 10 additional instances in MSE19∪20 but slows down the solving time of other instances by 60 s; and (ii) the sequential cardinality constraint encoding is applied to about the 20% of the instances in MSE19∪20 for at least one UB. It helps solve 39 additional instances in MSE from highly symmetric problems such as drmx-at-most-k.
A total of 15 solvers competed in the complete unweighted track of MSE2020 [13]. We consider the top 5 solvers: MaxHS (mhs in short), which is MHS-guided; EvalMaxSAT (eval in short), RC2-B (rc2 in short) and open-wbo-res-mergesat-v2 (Open-WBO or owbo in short), which are core-guided; and UWrMaxSAT (uwr in short), which combines both core-guided and model-guided solving. We executed the versions used in MSE2020 in all the experiments.
Results for MSE19∪20 (left) and MC (right) with top 5 solvers
Results for MSE19∪20 (left) and MC (right) with top 5 solvers
Table 2 shows the results for MSE19∪20 and MC, respectively. Column “#opt” has the number of instances for which an optimal solution was found (even if optimality is not certified). Column “#uniq” has the number of instances that were only solved by the solver in the row. Column “#win” has the number of instances solved by MaxCDCL but not by the solver in the row. We observe that MaxCDCL solves more instances than two top 5 solvers in MSE19∪20 and four top 5 solvers in MC. More importantly, MaxCDCL solves a significant number of instances that other solvers cannot solve. For example, MaxCDCL solves 119 instances in MC that MaxHS does not solve. If we consider all the solvers together, there is also a significant number of instances solved by MaxCDCL that no other solver is able to solve: 16 instances in MSE19∪20 and 68 instances in MC. These results show that the existing MaxSAT solvers, especially the model-guided and core-guided ones, are able to solve similar kinds of instances. Nevertheless, MaxCDCL has the potential to solve new kinds of instances that are not solvable with the current MaxSAT techniques. It is important to note that MaxCDCL is far from being as optimized as the other solvers, which are the result of a process of continuous improvements since more than ten years.
We observe that the number of instances solved by MaxCDCL across the different subfamilies is usually similar to the number of instances solved by most of the considered solvers. Nevertheless, MaxCDCL shows a clear differentiated performance on only a few subfamilies. Table 3 contains the main subfamilies from MC where we observe significant differences in the number of solved instances. For each subfamily, we show the number of instances (#ins) and the number of instances solved by each solver. The instances uniquely solved by MaxCDCL mainly come from the maxclique, maxcut and uaq families. On the other hand, MaxCDCL shows a worse performance on the optic and des families. There are other families where MaxCDCL and another solver have a remarkably different performance. For example, MaxCDCL and MaxHS are superior on the kbtree family, and MaxCDCL and UWrMaxSAT are superior on the extension-enforcement family.
We also observe that our solver has a remarkable capacity to find optimal (certified or not) solutions, as shown in column “#opt” of Table 2. The number of optimal solutions found by MaxCDCL is closer to the number of optimal solutions found by MaxHS than to the number of solved instances (i.e., the optimal solution is found and certified). In particular, MaxCDCL solves 6 fewer instances than MaxHS, but only finds 1 fewer optimal solution than MaxHS in MC. Note that this count can only be done on the set of instances for which the optimal value is known, and therefore it was done on the subset of instances that were solved by at least one of the top-5 solvers or MaxCDCL. Also note that other techniques are often needed for core-based solvers to find suboptimal solutions; in particular, EvalMaxSAT and RC2-B only report certified optimal solutions.
Results for selected subfamilies of MC with remarkable differences
Given two deterministic solvers X and Y and a time limit T to solve an NP-hard problem such as MaxSAT, the simplest way to try to solve more instances than X and Y alone within the time limit T is to combine X and Y by running X within the time limit
Results for MSE19∪20 (left) and MC (right). The entry in cell
for
is the number of instances solved by running solver X for 1800 seconds, and then solver Y from scratch for 1800 seconds if the instance is not solved by X. The entry in cell
(in the diagonal in grey) is the number of instances solved by running solver X for 1800 seconds. Column X in the last row recalls the results of solver X with 3600 seconds. The best results are in bold
Results for MSE19∪20 (left) and MC (right). The entry in cell
Table 4 shows the results of all possible pairwise combinations of the top 5 solvers and MaxCDCL (mcdcl) in MSE2020 for
More importantly, MaxCDCL combined with the top 2 solvers, MaxHS and EvalMaxSAT, solves the highest numbers (784 and 786) of instances in MSE19∪20. This result is significantly better than that of MaxHS or EvalMaxSAT alone, and the best combination without MaxCDCL solves only 777 instances. The results are even more striking in MC, where the worst combination of MaxCDCL with a top 5 solver is better than any other combination not including MaxCDCL, and combining MaxHS and MaxCDCL gives the best results, solving 93 instances more than the previous best result achieved by MaxHS alone, and 57 instances more than the best combination without MaxCDCL.
Figure 5 shows cactus plots comparing the best two combinations of solvers with MaxCDCL, the best two combinations without MaxCDCL, as well as the best two mono-solvers, for MSE19∪20 (left) and MC (right). Other solvers and combinations are excluded for readability reasons. For any time T (

Cactus plots of the best two combinations with MaxCDCL (mcdcl in short), the best two without MaxCDCL, and the best two mono-solvers for MSE19∪20 (left) and MC (right). For each point
We compare MaxCDCL with ahmaxsat, which was the best BnB solver in the last MaxSAT evaluation (MSE2016) in which BnB solvers competed. We use the MSE2016 instances of the categories MaxSAT (MS) and partial MaxSAT (PMS). Each category has random, crafted, and industrial instances. Thus, we consider a total of 6 families. Besides, we use the set MSE19∪20 that contains instances from recent evaluations. For completeness, we also compare with MaxHS in this experiment. MaxHS is the best solver for both MSE19∪20 and MC.
The results are shown in Table 5, where the number of instances for each family is given in column “#ins”. We observe that ahmaxsat solves more random instances and crafted MaxSAT instances, while MaxHS has the worst performance on these instances. A learnt clause, for these instances with randomness and limited size, usually contains most of the variables of the instances and is hardly useful. So, the higher use of lower bounding methods and the lack of clause learning in ahmaxsat are adequate for them, and the higher use of lower bounding methods (like in MaxCDCLalwaysLA) does not improve MaxCDCL because of clause learning. However, ahmaxsat has poor performance on other instances in which MaxCDCL is clearly superior.
Interestingly, in contrast to crafted MaxSAT instances, MaxCDCL and MasHS are better than ahmaxsat in crafted Partial MaxSAT instances. This result is coherent with the results of MSE2016 ,3
Finally, we observe that the total number of MaxSAT and Partial MaxSAT instances from MSE2016 solved by MaxCDCL is greater than the total number of instances solved by MaxHS.
Results for MSE16 and MSE19∪20
We described MaxCDCL, a MaxSAT solver that combines, for the first time to the best of our knowledge, branch and bound and clause learning. The main differences of MaxCDCL with existing SAT-based MaxSAT solvers are the following:
SAT-based MaxSAT solvers use a CDCL SAT solver as a black box and do not interfere in the internal operations of the SAT solver when solving an instance, while MaxCDCL itself can be considered a SAT solver extended to handle soft conflicts.
Both MaxCDCL and model-guided MaxSAT solvers have an upper bound
MaxCDCL, core-guided or MHS-guided MaxSAT solvers all identify cores. However, a core-guided or MHS-guided MaxSAT solver only identifies global cores (i.e., the cores that do not depend on any partial assignment) in order to relax them, while MaxCDCL detects local cores by using UP under a partial assignment to derive a soft conflict for learning a clause and backtracking early. Note that identifying a global core is NP-hard while a local core is detected in polynomial time with UP.
The extensive experimental investigation shows that MaxCDCL is ranked among the top 5 exact MaxSAT solvers in the 2020 MaxSAT evaluation. Furthermore, it solves a significant number of instances that other solvers cannot solve, suggesting that combining BnB and clause learning has the potential to solve new kinds of instances that are not solvable with current MaxSAT techniques. More importantly, combining MaxCDCL with the existing solvers allows to solve the highest number of MaxSAT instances.
Detailed analyses indicate that the performance of MaxCDCL comes from a careful configuration combining clause learning and BnB, including hardening based on local core detection and clause learning, the selective and adaptive application of lookahead, and the ordering used to propagate the soft literals when detecting local cores.
We believe that the proposed approach opens new and promising research directions. For example: (1) improving the quality of the clauses learnt from soft conflicts by defining new soft literal orderings in lookahead; (2) exploiting the relationship of SAT and MaxSAT for improving SAT and MaxSAT solving; (3) adapting the approach of MaxCDCL to other problems such as pseudo-Boolean optimization and Max-CSP; (4) extending MaxCDCL to weighted MaxSAT, in which each soft clause is weighted. In the extension of MaxCDCL to weighted MaxSAT, each soft clause is represented by a weighted soft literal. A local core detected by lookahead is weighted with the minimum soft literal weight it contains, and the other weights are split to be used in other core detections. When the total weight of all detected local cores reaches UB, a soft conflict is discovered. The challenge here is that there can be more local cores to detect than in the unweighted case. Thus, the clause learnt from a soft conflict can be longer. Special strategies in clause and soft literal ordering should be designed to shorten the learnt clauses.
Footnotes
Acknowledgements
This work has been partially funded by the French Agence Nationale de la Recherche, reference ANR-19-CHIA-0013-01, and grant PID2019-111544GB-C2 funded by MCIN/AEI/10.13039/501100011033. This work has also been partially supported by Archimedes Institute, Aix-Marseille University. We thank the anonymous reviewers for their comments and suggestions that helped to improve the manuscript.
