Boosting branch-and-bound MaxSAT solvers with clause learning

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

MaxSAT branch & bound CDCL

1. 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.

2. Preliminaries

A propositional variable x can take values 0 or 1 (false or true). A literal is a variable x or its negation $\neg x$ . A clause is a disjunction $l_{1} \lor \dots \lor l_{k}$ of k literals. A propositional formula in Conjunctive Normal Form (CNF) is a conjunction $c_{1} \land \dots \land c_{m}$ (or a set ${c_{1}, \dots, c_{m}}$ ) of m clauses. An assignment to the propositional variables satisfies a literal x if $x = 1$ , and satisfies a literal $\neg x$ if $x = 0$ . A literal x or $\neg x$ is assigned if x is assigned a value, otherwise it is free. An assignment is complete if all the variables are assigned a value, otherwise it is partial. A (partial) assignment is usually represented by a (sub)set of satisfied literals. A clause is satisfied if at least one of its literals is satisfied. A CNF is satisfied if all its clauses are satisfied. The Boolean satisfiability (SAT) problem for a CNF ϕ is to determine whether there exists an assignment that satisfies ϕ.

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 ${l}$ in ϕ, literal l must be satisfied (i.e., set to 1). Then, any clause containing l is removed from ϕ, and all the occurrences of $\neg l$ in clauses of ϕ are (implicitly) removed. UP is applied during the search until an empty clause (conflict) is found or no unit clause exists in ϕ. If UP finishes without finding a conflict, a new literal is picked following a heuristic and is set to 1 (we make a decision), and UP is applied again. If all the variables are assigned without finding a conflict, ϕ is satisfiable. The decision level of an assigned literal is the number of decisions made before being assigned. When a conflict is found, a conflict analysis is performed on the implication graph to derive a new clause explaining the conflict.

Fig. 1.

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@ $dl$ , where l is a literal set to 1 and $dl$ is its decision level. The negations of the literals of incoming edges of a node $l @ ld$ represent the reason (clause) why UP has set $l = 1$ . For instance, node $x_{12} @ 5$ is propagated due to clause $\neg x_{6} \lor \neg x_{4} \lor x_{12}$ (i.e., $x_{6} \land x_{4} \to x_{12}$ ), given that $x_{4}$ and $x_{6}$ have been set to 1. A node without incoming edges represents a decision. All decisions are painted in grey, and the last one is dashed. A conflicting clause is represented by incoming edges to □; in this example, clause $\neg x_{3} \lor \neg x_{35}$ . A Unique Implication Point (UIP) is a node of the implication graph that belongs to all paths from the last decision to the conflict. Figure 1 contains three UIPs: the last decision $x_{4}$ , and literals $x_{13}$ and $x_{25}$ . The most used learning schema in CDCL SAT solvers is called first UIP (1UIP), guided by the closest UIP to the conflict in the implication graph.

Concretely, when a conflict is found in the decision level $dl$ (i.e., $dl$ decisions were made before the conflict is found), a node is said active if it is in a path from 1UIP to the conflict. In other words, the active nodes are those nodes that lead to the conflict in the decision level $dl$ . For example, in Fig. 1, a conflict is found in the decision level 5, and $x_{25} @ 5$ , $x_{3} @ 5$ and $x_{35} @ 5$ are active nodes. The 1UIP learning schema identifies, in each path from a node in a decision level lower than $dl$ to an active node, the last literal in the lower decision level. The new learnt clause is composed of the negation of these literals and the 1UIP. For instance, in Fig. 1, clause $\neg x_{8} \lor x_{11} \lor \neg x_{25}$ is learnt, because there are two paths from lower decision levels to a node in a path from the 1UIP $x_{25} @ 5$ to the conflict, in which $x_{8}$ and $\neg x_{11}$ are the last literals in lower decision levels, respectively.

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.

3. Related work

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.

4. 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 ( $UB$ ), which is the best solution found so far for a complete assignment, with the lower bound ( $LB$ ), which is the sum of the number of clauses which are unsatisfied by the current partial assignment plus an underestimation of the number of clauses that will become unsatisfied if the current partial assignment is completed. If $LB ⩾ UB$ , the algorithm prunes the subtree below the current node and backtracks chronologically to a higher level in the search tree. If $LB < UB$ , the algorithm tries to find a better solution by extending the current partial assignment by instantiating one more variable. The optimal number of unsatisfied clauses in the input MaxSAT instance is the value that $UB$ takes after exploring the entire search tree. Note that BnB solves MaxSAT by finding a solution that minimizes the number of unsatisfied clauses. An assignment that minimizes the number of unsatisfied clauses also maximizes the number of satisfied clauses.

Algorithm 1:

A basic branch and bound algorithm for MaxSAT

Algorithm 1 shows the pseudo-code of a basic solver for MaxSAT, using the following notation:

$simplifyFormula (ϕ)$ is a procedure that transforms ϕ into an equivalent and simpler instance by applying inference rules.

$# emptyClauses (ϕ)$ is a function that returns the number of empty clauses in ϕ.

$LB$ is a lower bound of the minimum number of unsatisfied clauses in ϕ if the current partial assignment is extended to a complete assignment. We assume that its initial value is 0.

$underestimation (ϕ)$ is a function that returns an underestimation of the minimum number of non-empty clauses in ϕ that will become unsatisfied if the current partial assignment is extended to a complete assignment.

$UB$ is an upper bound of the number of unsatisfied clauses in an optimal solution. An elementary initial value for UB is the total number of clauses in the input formula, or the number of clauses that are unsatisfied by an arbitrary truth assignment. Nevertheless, most of the solvers take as initial upper bound the number of unsatisfied clauses that can be detected by executing the input formula in a local search solver during a short period of time.

$selectVariable (ϕ)$ is a function that returns a variable of ϕ following an heuristic.

$ϕ_{x}$ ( $ϕ_{\bar{x}}$ ) is the formula obtained by setting the variable x to true (false).

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.

4.1. Improving the lower bound with underestimations

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 $ϕ \land {x}$ and $ϕ \land {\bar{x}}$ . If UP derives a contradiction from $ϕ \land {x}$ and another contradiction from $ϕ \land {\bar{x}}$ , then the union of the two inconsistent subsets identified by UP, once we have removed the unit clauses x and $\bar{x}$ , is an inconsistent subset of ϕ. UP enhanced with failed literal detection does not need the occurrence of unit clauses in the input formula for deriving a contradiction. While UP only identifies unit refutations, UP enhanced with failed literal detection identifies non-unit refutations too. Since applying failed literal detection to each variable is time consuming, it is applied to a reduced number of variables in practice [39].

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 $ϕ \land {x}$ but not from $ϕ \land {\neg x}$ . In fact, this shows that $\neg x$ follows from ϕ. If $ϕ^{'}$ is the result of applying UP to $ϕ \land {\neg x}$ , then the algorithms tries to find another failed literal $x^{'}$ in $ϕ^{'}$ . If UP derives a contradiction from both $ϕ^{'} \land {x^{'}}$ and $ϕ^{'} \land {\neg x^{'}}$ , the algorithm stops and identifies an inconsistent subset. If UP derives a contradiction from $ϕ^{'} \land {x^{'}}$ but not from $ϕ^{'} \land {\neg x^{'}}$ , the same process is repeated on the formula resulting of applying UP to $ϕ^{'} \land {\neg x^{'}}$ until an inconsistent subset is detected or no more failed literals can be found.

4.2. 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 $ϕ^{'}$ . In the best case, inference rules produce new empty clauses in $ϕ^{'}$ that improve the lower bound. In contrast with the empty clauses derived when computing underestimations, the empty clauses derived with inference rules do not have to be recomputed at each node of the current subtree so that the lower bound computation is more incremental.

A MaxSAT inference rule is sound if it transforms an instance ϕ into an equivalent instance $ϕ^{'}$ . It is not sufficient to preserve satisfiability as in SAT, ϕ and $ϕ^{'}$ must have the same number of unsatisfied clauses for each possible assignment to be equivalent. Unfortunately, unit propagation, which is the most powerful inference technique applied in SAT solvers, is unsound for MaxSAT as the next example shows: The set of clauses ${x_{1}, \neg x_{1} \lor x_{2}, \neg x_{1} \lor \neg x_{2}, \neg x_{1} \lor x_{3}, \neg x_{1} \lor \neg x_{3}}$ has a minimum of one unsatisfied clause (setting $x_{1}$ to false), but two empty clauses are derived by applying unit propagation.

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 $\neg l$ are removed from the clauses in which $\neg l$ appears, but the existing unit clauses and the new unit clauses derived as a consequence of removing the occurrences of $\neg l$ are not propagated as in unit propagation. That inference is typically enhanced with the MaxSAT inference rules that we summarize in the rest of this section.

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 $\neg l$ appears, all the clauses containing $\neg l$ and all the occurrences of l are removed.

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 $\neg l$ , these two clauses are replaced with one empty clause.

The almost common clause rule [16]: If a MaxSAT instance contains a clause $x \lor D$ and a clause $\neg x \lor D$ , where D is a disjunction of literals, then both clauses are replaced with D. In practice, this rule is applied when D contains at most one literal.

The resolution rule applied in SAT (i.e., derive $D \lor D^{'}$ from $x \lor D$ and $\neg x \lor D^{'}$ ) is unsound for MaxSAT. Nevertheless, there exist a MaxSAT resolution rule that is complete, in the sense that if it is applied to a CNF formula ϕ following a specific strategy, it derives as many empty clauses as the minimum number of clauses of ϕ that can be unsatisfied [45,46]. Simple refinements of MaxSAT resolution that can be applied efficiently are implemented in BnB solvers like ahmaxsat [2], akmaxsat [30], MaxSatz [40], and MiniMaxSat [27].

5. 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.

5.1. General structure of MaxCDCL

Algorithm 2:

$MaxCDCL (H, S, UB)$ , a generic CDCL procedure with lookahead for MaxSAT

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 $sc$ after adding the hard clauses encoding $y \leftrightarrow sc$ to H. We refer to y as soft literal because it represents a soft clause (i.e., a soft literal is satisfied if and only if the corresponding soft clause is satisfied). To solve the MaxSAT instance, MaxCDCL is repeatedly called with $UB = 2^{0}, 2^{1}, 2^{2}, 2^{3}, \dots$ without exceeding $| S | + 1$ or ${UB}_{f} + 1$ , where ${UB}_{f}$ is a feasible upper bound computed by a heuristic solver with a short cutoff. This process stops when it obtains an assignment satisfying all clauses in H and unsatisfying fewer than UB soft literals in S. After that, MaxCDCL is repeatedly called with UB set to the number of unsatisfied soft literals in the previous call, until no better solution can be found.

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 $| cores |$ of the number of soft literals that will be unsatisfied if the current partial assignment is extended. If a soft conflict is discovered, i.e., if $| falseS | + | cores | ⩾ UB$ , it is analyzed to learn a clause for backtracking. Second, if no soft conflict is discovered, but it is discovered that the violation of any free soft literal y not used in $| cores |$ would result in a soft conflict, y is satisfied by a procedure called hardening.

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.

5.2. Combining lookahead and clause learning

A subset of soft literals $S_{i} = {y_{1}, \dots, y_{| S_{i} |}}$ is inconsistent if they cannot be simultaneously satisfied. This inconsistency can be represented by the hard clause $\neg y_{1} \lor \dots \lor \neg y_{| S_{i} |}$ . Note that $| S_{i} |$ can be 1. If the inconsistency is independent of any partial assignment, the subset is called a global core. Otherwise, the inconsistency is implied by a subset of literals and the inconsistent subset of soft literals is called a local core. The core-guided or MHS-guided SAT-based MaxSAT solvers only detect global cores to relax them, while our approach detects local cores, given a partial assignment, to discover a soft conflict.

Example 1.
Let $H = {\neg y_{1} \lor x_{1} \lor \neg x_{2}, \neg x_{1} \lor \neg x_{3} \lor \neg x_{4}, \neg y_{2} \lor x_{3}, \neg y_{3} \lor x_{5}}$ , where $y_{1}$ , $y_{2}$ and $y_{3}$ are soft literals. If no variable is assigned, all soft literals can be simultaneously satisfied. So, no global core exists. However, if the current partial assignment is ${x_{2} = 1, x_{4} = 1}$ , the subset of soft literals ${y_{1}, y_{2}}$ is a local core implied by the partial assignment. We write the implication by $H \cup {x_{2}, x_{4}} \to \neg y_{1} \lor \neg y_{2}$ .

Proposition 1 provides the foundation of our approach in the general case.
Proposition 1.
Let H be a set of hard clauses, let $S = {y_{1}, \dots, y_{| S |}}$ be the set of all soft literals, let k be an integer, and let $L_{i} = {l_{i 1}, \dots, l_{i | L_{i} |}}$ ( $1 ⩽ i ⩽ k$ ) be a set of literals. If, for each $L_{i}$ , $H \cup L_{i}$ implies a local core $S_{i} = {z_{i 1}, \dots, z_{i | S_{i} |}} \subset S$ (i.e., $H \cup L_{i} \to \neg z_{i 1} \lor \dots \lor \neg z_{i | S_{i} |}$ ), and $S_{i}$ and $S_{j}$ are disjoint ( $1 ⩽ i < j ⩽ k$ ), then each assignment that satisfies $H \cup {\neg y_{1} + \dots + \neg y_{| S |} < k}$ also satisfies the clause $\neg l_{11} \lor \dots \lor \neg l_{1 | L_{1} |} \lor \dots \lor \neg l_{k 1} \lor \dots \lor \neg l_{k | L_{k} |}$ .
Proof.
It is easy to see that $H \cup L_{1} \cup \dots \cup L_{k}$ implies $(\neg z_{11} \lor \dots \lor \neg z_{1 | S_{1} |}) \land \dots \land (\neg z_{k 1} \lor \dots \lor \neg z_{k | S_{k} |})$ , meaning that $H \cup L_{1} \cup \dots \cup L_{k}$ unsatisfies the constraint $\neg y_{1} + \dots + \neg y_{| S |} < k$ , because each clause $\neg z_{i 1} \lor \dots \lor \neg z_{i | S_{i} |}$ implies at least one different unsatisfied soft literal. Hence, any assignment satisfying $H \cup {\neg y_{1} + \dots + \neg y_{| S |} < k}$ must unsatisfy at least one literal in $L_{1} \cup \dots \cup L_{k}$ , and satisfy the clause $\neg l_{11} \lor \dots \lor \neg l_{1 | L_{1} |} \lor \dots \lor \neg l_{k 1} \lor \dots \lor \neg l_{k | L_{k} |}$ . Note that we use “z” (instead “y”) to denote a soft literal in a local core to avoid complex subscripts. □

Given a partial assignment F of H, the application of Proposition 1 consists in first detecting a local core $S_{i}$ and then identifying the smallest $L_{i} \subset F$ such that $H \cup L_{i}$ implies $S_{i}$ . We call $L_{i}$ the reason of $S_{i}$ . If k is the current upper bound UB and k disjoint local cores are detected, a soft conflict is discovered, and the clause $\neg l_{11} \lor \dots \lor \neg l_{1 | L_{1} |} \lor \dots \lor \neg l_{k 1} \lor \dots \lor \neg l_{k | L_{k} |}$ , which is implied by $H \cup {\neg y_{1} + \dots + \neg y_{| S |} < k}$ and is unsatisfied by the current partial assignment, can be considered an implicit clause explaining the soft conflict. This clause can be further analyzed using the 1UIP schema in line 9 of Algorithm 2 to learn a clause to be explicitly added to H to prevent the same soft conflict in the future as in the hard conflict case.

Algorithm 3:
$UPLA (H, S, UB, dl)$ , unit propagation followed by lookahead

The detection of a local core $S_{i}$ is implemented by using UP in a lookahead procedure as in existing BnB MaxSAT solvers [36,38,39]. The advantage of this procedure is that $S_{i}$ is minimal w.r.t. UP, in the sense that UP cannot detect any local core that is a proper subset of $S_{i}$ under the same partial assignment [36], which is essential for our approach, because MaxCDCL needs to learn clauses of good quality from the detected local cores. Recall that BnB MaxSAT solvers detect disjoint local cores but do not explain them. When a soft conflict is discovered, they simply backtrack without learning a hard clause from the soft conflict.

Concretely, MaxCDCL calls Algorithm 3 at decision level $dl$ with a partial assignment F, under which the already unsatisfied soft literals are stored in a set named $falseS$ . The lookahead procedure starts at line 5 in Algorithm 3 when no hard conflict is found, and terminates at line 7 or line 14. This procedure proceeds in decision level $dl + 1$ by maintaining a set of detected local cores ( $cores$ ). Each iteration of the loop (line 5) propagates a free soft literal y not occurring in $cores$ , until a clause h in H is unsatisfied or a soft literal $sl$ not occurring in $cores$ is unsatisfied (line 8). These unit propagations construct an implication graph G. The propagated free soft literals $y_{1}, y_{2}, \dots$ in the loop can be seen as temporary assumptions at decision level $dl + 1$ that have no incoming edge in G.

Inspecting G, let $z_{1}, \dots, z_{b}$ be the subset of literals $y_{1}, y_{2}, \dots$ at level $dl + 1$ and without incoming edge, from which there is a path to h or to $\neg sl$ . Then, ${z_{1}, \dots, z_{b}}$ (resp. ${z_{1}, \dots, z_{b}, sl}$ ) is a local core $S_{i}$ implied by the partial assignment F at decision level $dl$ . Based on G, we can also define $L_{i}$ as the set containing, from each path to h (resp. $\neg sl$ ), the last literal assigned before level $dl + 1$ . Clearly, $H \cup L_{i}$ implies $\neg z_{1} \lor \dots \lor \neg z_{b}$ (resp. $\neg z_{1} \lor \dots \lor \neg z_{b} \lor \neg sl$ ).

Note that, when $k = | falseS | + | cores | = UB$ in MaxCDCL, each already unsatisfied soft literal y in $falseS$ constitutes a local core $S_{i} = {y}$ not in $cores$ , implied by $H \cup {\neg y}$ (i.e. $L_{i} = {\neg y}$ ). Therefore we have UB disjoint local cores. According to Proposition 1, $\neg l_{11} \lor \dots \lor \neg l_{1 | L_{1} |} \lor \dots \lor \neg l_{k 1} \lor \neg l_{k 2} \lor \dots \lor \neg l_{k | L_{k} |}$ could be considered as an implicit clause in H, which is unsatisfied by the current partial assignment and is analyzed using the 1UIP schema in line 9 of Algorithm 2 to learn a clause as in the hard conflict case.

Fig. 2.
Implication graphs involved in the detection of $cores$ in Example 2. Grey nodes represent decisions or assumptions, and dashed nodes represent assignments made in the lookahead process.
Example 2.
Let $y_{1}, \dots, y_{7}$ be soft literals, and let H be formed by

$\neg y_{1} \lor y_{2} \lor \neg x_{2}$ $\neg y_{2} \lor \neg x_{3} \lor \neg x_{4}$ $\neg y_{2} \lor \neg y_{5} \lor x_{6}$ $\neg x_{1} \lor x_{4}$ $\neg y_{3} \lor x_{3}$

$\neg x_{6} \lor \neg x_{5} \lor y_{6}$ $\neg y_{6} \lor \neg x_{2} \lor x_{7}$ $\neg x_{7} \lor \neg y_{6}$ $\neg y_{4} \lor x_{8}$ $\neg y_{7} \lor x_{9}$

If no variable is assigned, all soft literals can be simultaneously satisfied. So, no global core exists. Let the current partial assignment be ${y_{7} = 0, x_{2} = 1, x_{1} = 1, x_{4} = 1, x_{5} = 1}$ , where $x_{4}$ is propagated due to $\neg x_{1} \lor x_{4}$ , and the other literals have been decided. Hence, $falseS = {y_{7}}$ and the current decision level is 4.

Assume that $UB = 3$ . We show how Algorithm 3 detects $cores$ and reaches UB by propagating the free soft literals $y_{1}, \dots, y_{6}$ , by means of Fig. 2.

After propagating $y_{1}$ , $y_{2}$ is satisfied and $y_{3}$ is unsatisfied. Hence, $sl = y_{3}$ is detected, the implication graph of Fig. 2A is obtained and the $core = {y_{1}, y_{3}}$ is detected at line 12 with $reason = {x_{2}, x_{4}}$ , because there are paths from $x_{2}$ and $x_{4}$ to $\neg y_{3}$ and the next literals to $x_{2}$ and $x_{4}$ in the paths are from decision level 5.

Since $y_{2}$ is not in $cores$ , it can be used to detect further cores. After propagating $y_{2}$ , $y_{4}$ , $y_{5}$ , the implication graph of Fig. 2B is obtained and the conflicting clause $h = {\neg x_{7} \lor \neg y_{6}}$ is detected. Then, the $core = {y_{2}, y_{5}}$ is detected at line 10 with $reason = {x_{2}, x_{5}}$ .

Since $| cores | + | falseS | = 2 + 1 = UB$ , a soft conflict is found at line 13 with $cores = {{y_{1}, y_{3}}, {y_{2}, y_{5}}}$ , $reasons = {x_{2}, x_{4}, x_{5}}$ and $falseS = {\neg y_{7}}$ . When analyzing the soft conflict at line 9 of Algorithm 2, as argued before, we can consider $cores = {{y_{1}, y_{3}}, {y_{2}, y_{5}}, {y_{7}}}$ and $reasons = {x_{2}, x_{4}, x_{5}, \neg y_{7}}$ . Then, according to Proposition 1, clause $\neg x_{2} \lor \neg x_{4} \lor \neg x_{5} \lor y_{7}$ is implied by $H \cup {\neg y_{1} + \dots + \neg y_{| S |} < 3}$ , which is unsatisfied at decision level 4 and can be analysed with the 1UIP scheme at level 4 to learn a new clause and backtrack. Note that a model-guided MaxSAT solver would not discover this soft conflict at this stage because $UB = 3$ but only one soft literal is falsified.

Proposition 1 also provides the basis for hardening. If $k = | falseS | + | cores | = UB - 1$ , for each free soft literal z not in the k local cores, $H \cup {\neg z}$ implies a new local core ${z}$ . The hardening procedure (line 14 in Algorithm 2) satisfies z with the reason $z \lor \neg l_{11} \lor \dots \lor \neg l_{1 | L_{1} |} \lor \dots \lor \neg l_{k 1} \lor \dots \lor \neg l_{k | L_{k} |}$ . Note that this hardening satisfies a fundamental requirement of CDCL SAT solvers: except the decision (i.e., branching) variables, the value of each variable must be explicitly associated with a reason. In contrast, although existing BnB MaxSAT solvers also implement hardening, no reason is associated with each hardening.

If $m = | H | + | S |$ , UP is in $O (m)$ for detecting one local core. Since the lookahead procedure detects at most UB cores, its whole complexity is in $O (m \times UB)$ .
5.3. A probing strategy for lookahead

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 $k = UB - | falseS |$ , the lookahead procedure has to detect k disjoint local cores to be successful. Generally, the greater the value of k, the lower the probability of lookahead to be successful.

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 $avgp$ and the standard deviation $devp$ of the number of detected disjoint local cores in a successful probing lookahead are computed to select the branches where lookahead is applied.

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 $avgp + coef * devp$ when $coef = 3$ . So, lookahead is not applied at the current branch when $k > avgp + coef * devp$ . However, since the probing may not get exact information and the values may not follow a perfect normal distribution, $coef$ is dynamically adjusted to maintain the success rate of lookahead between $lowRate$ and $highRate$ , where $lowRate$ and $highRate$ are parameters intuitively fixed to 0.6 and 0.75, respectively.

Concretely, $coef$ is initialized to 2 for each UB. At each probing, if the success rate of lookahead since the last probing is greater than $highRate$ , it is increased by 0.1; and if it is lower than $lowRate$ , it is decreased by 0.1. There are no lower and upper bounds on $coef$ . When it is too low so that no lookahead is performed between two probings, it is reset to 2.

5.4. 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.

5.5. 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 $var_inc$ . Initially, $var_inc$ is set to 1 and, after each conflict, is divided by a parameter usually set to 0.95 to give more importance to the next conflict. Note that VSIDS is a heuristic based on looking back, because it is based on the past conflicts.

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 $var_inc \times γ$ , where γ is a discount-rate parameter as in reinforcement learning that is empirically fixed to 0.1. The intuition of this modification is the following. A soft conflict is derived when UB local cores are detected. So a variable contributing to many local cores should be favoured to reach a soft conflict as early as possible. However, a local core represents only a component of a future possible soft conflict but not a soft conflict for sure. So the increase of the score of a variable contributing to a core should be discounted by γ.

5.6. 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 https://home.mis.u-picardie.fr/~cli/EnglishPage.html.

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 $S = {y_{1}, \dots, y_{| S |}}$ is the set of all soft literals. When $| S | \times (UB - 1) ⩽ 10^{4}$ , the sequential SAT encoding [19] of the cardinality constraint $\neg y_{1} + \neg y_{2} + \dots + \neg y_{| S |} < UB$ is added to the input instance before starting the search. MaxCDCL alternates LRB phases and VSIDS phases during the search as MapleCOMSPS_LRB. It uses the LRB and VSIDS heuristics modified as in Section 5.5, respectively. Each phase is limited to a number of unit propagations specified by the parameter $phaseLength$ , which is initialized to $2 \times 10^{7}$ and is doubled each cycle of LRB phase and VSIDS phase. In the VSIDS phase, the glucose restart strategy [11] is used; in the LRB phase, the Luby restart strategy [42] is used.

We plan to implement MaxCDCL on top of Kissat [17], the winner of the SAT2020 competition, which might further improve its performance.

5.7. Preprocessing

The SAT solver MapleCOMSPS_LRB inherits its preprocessing from MiniSAT. Roughly speaking, let x be a variable, let $B_{1}, \dots, B_{a}, D_{1}, \dots, D_{b}$ be disjunction of literals, let $H_{x}$ = ${x \lor B_{1}, \dots, x \lor B_{a}, \neg x \lor D_{1}, \dots, \neg x \lor D_{b}}$ be the set of all clauses containing x and $\neg x$ , and let $H_{noX}$ = ${B_{1} \lor D_{1}, \dots, B_{1} \lor D_{b}, \dots, B_{a} \lor D_{1}, \dots, B_{a} \lor D_{b}}$ after removing the tautologies (a clause is a tautology if it contains a literal and the negation of this literal). If the length of all clauses in $H_{noX}$ does not exceed α and $| H_{noX} | < | H_{x} | + β$ , where α and β are parameters fixed to 20 and 10000, respectively, then the preprocessing replaces $H_{x}$ by $H_{noX}$ , so that the resulting formula does not contain x any more. The soundness of this preprocessing follows from the fact that any solution of the original formula also satisfies the resulting formula, and any solution of the resulting formula can be extended by assigning a value to x to satisfy the clauses in $H_{x}$ .

The preprocessing is extended to MaxCDCL as follows:

A literal l is said to be pure in the input formula if $\neg l$ does not occur in the formula. If x ( $\neg x$ ) is a pure literal, then all soft and hard clauses containing x ( $\neg x$ ) are removed.

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.

5.8. Failed literal detection

A literal l is failed in the set of all hard clauses H if UP deduces an empty clause in $H \cup {l}$ . If l is a failed literal, then $\neg l$ should be satisfied. Before each minimization of learnt clauses, as in [43], MaxCDCL detects failed literals in H to simplify H as much as possible.

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 $H \cup {x}$ and $H \cup {\neg x}$ . If x ( $\neg x$ ) is a failed literal, $\neg x$ (x) is satisfied. Otherwise, if UP derives a literal l in both $H \cup {x}$ and $H \cup {\neg x}$ , then l is also satisfied. The detection is stopped when all the free variables have been detected or no literal is satisfied after detecting 1000 variables.

6. 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:

MSE19∪20: The union of all the instances used in the complete unweighted track of the MaxSAT Evaluations (MSE) 2019 and 2020, MSE19∪20 has a total of 1000 distinct instances.

MC: A subset of the Master Collection of instances from the MaxSAT evaluations held until 2019.2

²
www.cs.toronto.edu/maxsat-lib/maxsat-instances/master-set/unweighted/

It contains 16080 unweighted (partial) MaxSAT instances, classified into 51 families and 76 subfamilies. MC includes all the instances of the 63 subfamilies having 100 instances or less, and the first 100 instances as they occur in the natural order in each of the remaining 13 subfamilies, considering a total of 3614 instances. This selection provides a simple, deterministic and objective criterion that does not favor any solver, and the experiments can be easily reproduced. MC contains 726 instances that also belong to MSE19∪20.

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 ${UB}_{f}$ with SatLike (version 3.0). Note that MaxCDCL and its variants do not start the search from $UB = {UB}_{f}$ , but from $UB = 2^{0}$ , then $2^{1}, 2^{2}, \dots$ , until a feasible solution is found or $2^{i} > {UB}_{f}$ . In the latter case, UB is set to ${UB}_{f} + 1$ . Then, UB is gradually decreased until no better solution can be found (see Section 5.1).

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.

6.1. MaxCDCL components

Table 1 compares MaxCDCL with the following variants:

MaxCDCL ∖LA.

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 ∖harden.

MaxCDCL without hardening (i.e., lines 13 and 14 in Algorithm 2 are removed).

MaxCDCLalwaysLA.

MaxCDCL that looks ahead at each branch, i.e., the condition to lookahead is always satisfied in line 3 of Algorithm 3.

MaxCDCLioLA.

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 ∖VSIDSbyLA.

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 ∖prep.

MaxCDCL that does not perform the preprocessing described in Section 5.7.

MaxCDCL ∖FL.

MaxCDCL that does not perform the failed literal detection described in Section 5.8.

Table 1
Comparison of MaxCDCL with its variants for MSE19∪20 (left) and MC (right)

#solv avg #solv avg

MaxCDCL∖LA 505 255 s 2183 194 s

MaxCDCL∖harden 664 281 s 2878 194 s

MaxCDCLalwaysLA 681 249 s 2962 193 s

MaxCDCLioLA 704 268 s 2963 168 s

MaxCDCL∖prep 723 240 s 3003 165 s

MaxCDCL∖FL 724 220 s 3011 157 s

MaxCDCL∖VSIDSbyLA 724 268 s 3013 165 s

MaxCDCL 736 271 s 3031 168 s

	#solv	avg	#solv	avg
MaxCDCL∖LA	505	255 s	2183	194 s
MaxCDCL∖harden	664	281 s	2878	194 s
MaxCDCLalwaysLA	681	249 s	2962	193 s
MaxCDCLioLA	704	268 s	2963	168 s
MaxCDCL∖prep	723	240 s	3003	165 s
MaxCDCL∖FL	724	220 s	3011	157 s
MaxCDCL∖VSIDSbyLA	724	268 s	3013	165 s
MaxCDCL	736	271 s	3031	168 s

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.

Fig. 3.

Comparison of the success rate of lookahead procedure. Each point is a different instance of MSE19∪20. In the left-most plot, a point $(X, Y)$ for an instance means that the percentage of lookahead calls that detected a soft conflict on this instance is $X %$ with the probing strategy and $Y %$ when lookahead is always called. The plot in the center compares the percentage of lookaheads that triggered a hardening, and the plot at the right the percentage that either detected a soft conflict or hardening.

Fig. 4.

Cumulative distribution of the success rates of the lookahead method. A point $(X, Y)$ means that the success rate for $X %$ of the instances in MSE19∪20 is less or equal than $Y %$ , or that the rate for $(100 - X) %$ of the instances is at least $Y %$ . SoftC stands for soft conflict detection, harden for hardening, and all considers both cases as a success.

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., $| falseS | + | cores | = UB$ ), that enable hardening (i.e., $| falseS | + | cores | = UB - 1$ ), or either of the two cases (i.e., $| falseS | + | cores | ⩾ UB - 1$ ). The plots in Fig. 3 analyse these rates for every different instance of MSE19∪20 in comparison with MaxCDCLalwaysLA. We observe that the rates of soft conflict detection dramatically increase with the probing strategy, hence saving computation time of lookahead calls that do not result in a soft conflict. On the other hand, the rates of hardening decrease, which can be explained by the fact that the probing strategy is specialized to detect soft conflicts. In spite of this, the rates for the case $| falseS | + | cores | ⩾ UB - 1$ are still significantly better with the probing strategy, which means that overall the rate of useful lookahead is improved. Figure 4 shows the cumulative distribution of success rates and suggests similar conclusions. For instance, we observe that, with probing, the soft conflict detection rate is at least 80% for 20% of the instances, and the soft conflict detection rate is at least 50% for 60% of the instances. With MaxCDCLalwaysLA less than 5% of the instances have a rate greater than 50%.

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.

6.2. Comparison with the top 5 solvers in MSE2020

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.

Table 2
Results for MSE19∪20 (left) and MC (right) with top 5 solvers

#solv #opt avg #uniq #win #solv #opt avg #uniq #win

MaxHS 769 781 177 s 11 36 3037 3070 85.5 s 26 119

EvalMaxSAT 759 759 129 s 1 43 3002 3002 69.7 s 4 150

UWrMaxSAT 745 750 128 s 3 42 2969 2987 51.6 s 7 142

RC2-B 728 728 164 s 0 62 2948 2948 70.1 s 1 177

Open-WBO 695 696 157 s 3 71 2906 2912 89.7 s 4 194

MaxCDCL 736 749 271 s 16 – 3031 3069 168 s 68 –

	#solv	#opt	avg	#uniq	#win	#solv	#opt	avg	#uniq	#win
MaxHS	769	781	177 s	11	36	3037	3070	85.5 s	26	119
EvalMaxSAT	759	759	129 s	1	43	3002	3002	69.7 s	4	150
UWrMaxSAT	745	750	128 s	3	42	2969	2987	51.6 s	7	142
RC2-B	728	728	164 s	0	62	2948	2948	70.1 s	1	177
Open-WBO	695	696	157 s	3	71	2906	2912	89.7 s	4	194
MaxCDCL	736	749	271 s	16	–	3031	3069	168 s	68	–

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.

Table 3

Results for selected subfamilies of MC with remarkable differences

	#ins	maxhs	eval	uwr	rc2	owbo	mcdcl
des	100	99	100	100	96	88	70
extension-enforcement	40	20	21	30	20	18	30
kbtree	54	54	27	25	21	35	54
maxclique/sturctured	62	40	41	39	39	37	45
maxcut/dimacs_mod	62	19	15	23	11	11	45
maxcut/random	40	11	0	5	0	0	40
optic	65	49	42	28	32	23	19
uaq	92	74	76	74	75	68	84

6.3. Combining MaxCDCL with existing solvers

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 $T / 2$ , and then Y from scratch within the remaining time $T / 2$ if the instance is not solved by X.

Table 4
Results for MSE19∪20 (left) and MC (right). The entry in cell $(X, Y)$ for $X \neq Y$ 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 $(X, X)$ (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

Table 4 shows the results of all possible pairwise combinations of the top 5 solvers and MaxCDCL (mcdcl) in MSE2020 for $T = 3600$ s. Each cell $(X, Y)$ for $X \neq Y$ contains the number of instances solved by running solver X for 1800 s and then solver Y from scratch for 1800 s in MSE19∪20 (left) and MC (right). Each cell $(X, X)$ (in the diagonal in grey) contains the number of instances solved by X in 1800 s. Column X in the last row recalls the results of X with 3600 seconds. Combining any of the top 5 solvers with MaxCDCL solves more instances than this solver and MaxCDCL alone within 3600 s, while this is not always true when combining two top 5 solvers. For example, combining MaxHS and Open-WBO solves 763 instances in MSE19∪20 within 3600 s, while MaxHS alone solves 769 instances within 3600 s. This shows that MaxCDCL is more complementary with the top 5 solvers than other solvers.

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 ( $0 < T ⩽ 3600 s$ ), a curve gives the number of instances solved by a mono-solver or a combination of two solvers within T, where the number of instances solved by a combination X-Y of solvers X and Y within T is the number of instances solved by running X for $T / 2$ , and then Y for $T / 2$ . The solving time of a combination X-Y of solvers X and Y for an instance is twice the minimum solving time among X and Y. This simulates a parallel execution of X and Y by alternating them in small time periods. The plots clearly show the advantage of combining an existing solver with MaxCDCL, allowing to solve the highest number of instances within 3600 s, and the advantage becomes greater as the running time is increased.

Fig. 5.

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 $(N, T)$ in a curve for a mono-solver X, N is the number of instances solved by X in T seconds; and for each point $(N, T)$ in a curve for a combination X-Y of solvers X and Y, N is the number of instances solved by running X for $T / 2$ seconds followed by running Y for $T / 2$ seconds. The names of the solvers and combinations are listed in the order of the highest points of the corresponding curves from left to right for readability.

6.4. Comparison with a BnB solver

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

³
http://maxsat.ia.udl.cat/results/

where the best solvers in the industrial tracks obtained much better results than BnB solvers in the crafted Partial MaxSAT track. This behaviour suggests that the structure of these particular Partial MaxSAT instances is closer to the structure of industrial instances than to the structure of random instances, while the opposite happens with the MaxSAT crafted instances from MSE2016 which are all max-cut instances on random graphs.

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.

Table 5

Results for MSE16 and MSE19∪20

				ahmaxsat			MaxHS			MaxCDCL

			#ins	#solv	avg	#win	#solv	avg	#win	#solv	avg
MSE16	MS	random	454	259	744 s	0	1	3526 s	27	28	1441 s
		crafted	402	230	33.0 s	0	23	329 s	27	48	353 s
		industrial	55	0	–	36	44	387 s	1	36	394 s
		TOTAL	911	489	410 s	36	68	414 s	55	112	638 s
	PMS	random	210	209	148 s	0	83	1201 s	66	139	720 s
		crafted	678	369	242 s	275	632	72 s	15	644	134 s
		industrial	601	183	515 s	332	551	85 s	6	514	179 s
		TOTAL	1489	761	282 s	607	1266	152 s	87	1297	215 s
MSE19∪20			1000	270	422 s	483	769	177 s	36	736	271 s

7. Conclusions

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 $UB - 1$ of the number of soft clauses that can be unsatisfied. The difference lies in how to exploit this UB. Let $falseS$ denote the set of already unsatisfied soft clauses. On the one hand, model-guided MaxSAT solvers call a SAT solver after encoding UB into CNF. If no hard clause is unsatisfied, the SAT solver backtracks only after $| falseS | ⩾ UB$ , because no clause encoding UB is unsatisfied if $| falseS | < UB$ . On the other hand, MaxCDCL computes a lower bound LB of the number of soft clauses that will be unsatisfied (but not yet unsatisfied), and backtracks as soon as $LB + | falseS | ⩾ UB$ . Thus, MaxCDCL is able to backtrack much earlier than model-guided MaxSAT solvers.

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.

References

Abramé and

D.H.

Ahmaxsat , Description and evaluation of a branch and bound Max-SAT solver, J. Satisf. Boolean Model. Comput. 9 (2014), 89–128.

Abramé and

Habet , Efficient application of Max-SAT resolution on inconsistent subsets, in: Proceedings of the 20th International Conference on Principles and Practice of Constraint Programming, CP, Lyon, France, 2014, pp. 92–107. doi:10.1007/978-3-319-10428-7_10.

Abramé and

Habet , Learning nobetter clauses in Max-SAT branch and bound solvers, in: Proceedings of ICTAI 2016, 2016, pp. 452–459.

Alsinet ,

Manyà and

Planes , Improved branch and bound algorithms for Max-SAT, in: Proceedings of the 6th International Conference on the Theory and Applications of Satisfiability Testing, 2003.

Alsinet ,

Manyà and

Planes , Improved exact solver for weighted Max-SAT, in: Proceedings of the 8th International Conference on Theory and Applications of Satisfiability Testing, SAT-2005, St. Andrews, Scotland, LNCS, Vol. 3569, Springer, 2005, pp. 371–377.

Alsinet ,

Manyà and

Planes , An efficient solver for weighted Max-SAT, Journal of Global Optimization 41 (2008), 61–73. doi:10.1007/s10898-007-9166-9.

Ansótegui ,

M.L.

Bonet and

Levy , Solving (weighted) partial MaxSAT through satisfiability testing, in: Proceedings of SAT 2009, LNCS, Vol. 5584, Springer, 2009, pp. 427–440.

Ansótegui ,

M.L.

Bonet and

Levy , A new algorithm for weighted partial MaxSAT, in: Proceedings AAAI 2010, 2010, pp. 3–8.

Ansótegui ,

M.L.

Bonet and

Levy , SAT-based MaxSAT algorithms, Artificial Intelligence 196 (2013), 77–105. doi:10.1016/j.artint.2013.01.002.

10.

Ansótegui and

Gabàs , WPM3: An (in)complete algorithm for weighted partial MaxSAT, Artificial Intelligence 250 (2017), 37–57. doi:10.1016/j.artint.2017.05.003.

11.

Audemard and

Simon , Predicting learnt clauses quality in modern SAT solvers, in: Proceedings IJCAI 2009, 2009, pp. 399–404.

12.

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

13.

Bacchus ,

Berg ,

Järvisalo and

Martins , MaxSAT Evaluation 2020: Solver and Benchmark Descriptions, 2020.

14.

Bacchus ,

Hyttinen ,

Järvisalo and

Saikko , Reduced cost fixing in MaxSAT, in: Proceedings of CP 2017, LNCS, Springer, 2017, pp. 641–651.

15.

Bacchus ,

Järvisalo and

Ruben , Maximum satisfiability, in: Handbook of Satisfiability, 2nd edn, IOS Press, 2021, pp. 929–991.

16.

Bansal and

Raman , Upper bounds for MaxSat: Further improved, in: Proc 10th International Symposium on Algorithms and Computation, ISAAC’99, LNCS, Vol. 1741, Springer, Chennai, India, 1999, pp. 247–260.

17.

Biere ,

Fazekas ,

Fleury and

Heisinger , CaDiCaL, kissat, paracooba, plingeling and treengeling entering the SAT competition 2020, in: Proceedings of SAT Competition 2020: Solver and Benchmark Descriptions, 2020, p. 50.

18.

Borchers and

Furman , A two-phase exact algorithm for MAX-SAT and weighted MAX-SAT problems, Journal of Combinatorial Optimization 2 (1999), 299–306. doi:10.1023/A:1009725216438.

19.

Carsten , Towards an optimal CNF encoding of Boolean cardinality constraints, in: Proceedings of CP 2005, LNCS, Vol. 3709, Springer, 2005, pp. 827–831.

20.

M.S.

Cherif ,

Habet and

Abramé , Understanding the power of Max-SAT resolution through UP-resilience, Artificial Intelligence 289 (2020), 103397. doi:10.1016/j.artint.2020.103397.

21.

Davies and

Bacchus , Solving MAXSAT by solving a sequence of simpler SAT instances, in: Proceedings of CP 2011, Springer, 2011, pp. 225–239.

22.

Davies and

Bacchus , Exploiting the power of MIP solvers in MAXSAT, in: Proceedings of SAT 2013, Springer, 2013, pp. 166–181.

23.

Feng and

Bacchus , Clause size reduction with all-uip learning, in: Proceedings of SAT 2020, Springer LNCS, Vol. 12178, 2020, pp. 28–45.

24.

Fu and

Malik , On solving the partial MAX-SAT problem, in: Proceedings of the 9th International Conference on Theory and Applications of Satisfiability Testing, SAT-2006, LNCS, Vol. 4121, Springer, Seattle, USA, 2006, pp. 252–265. doi:10.1007/11814948_25.

25.

Gange ,

Berg ,

Demirović and

P.J.

Stuckey , Core-guided and core-boosted search for CP, in: Proceedings of CPAIOR 2020, 2020, pp. 205–221.

26.

Heras and

Larrosa , New inference rules for efficient Max-SAT solving, in: Proceedings of the National Conference on Artificial Intelligence, AAAI-2006, Boston/MA, USA, 2006, pp. 68–73.

27.

Heras ,

Larrosa and

Oliveras , MiniMaxSAT: An efficient weighted Max-SAT solver, Journal of Artificial Intelligence Research 31 (2008), 1–32. doi:10.1613/jair.2347.

28.

Ignatiev ,

Morgado and

Marques-Silva , RC2: An efficient maxsat solver, J. Satisf. Boolean Model. Comput. 11(1) (2019), 53–64.

29.

Koshimura ,

Zhang ,

Fujita and

Hasegawa , QMaxSAT: A partial Max-SAT solver, J. Satisf. Boolean Model. Comput. 8(1/2) (2012), 95–100.

30.

Kuegel , Improved exact solver for the weighted MAX-SAT problem, in: Proceedings of Workshop Pragmatics of SAT, POS-10, Edinburgh, UK, 2010, pp. 15–27.

31.

Le Berre and

Parrain , The Sat4j library, release 2.2, J. Satisf. Boolean Model. Comput. 7(2–3) (2010), 59–66.

32.

Lei and

Cai , Solving (weighted) partial MaxSAT by dynamic local search for SAT, in: Proceedings of IJCAI 2018, 2018, pp. 1346–1352. doi:10.24963/ijcai.2018/187.

33.

C.-M.

Li ,

Xiao ,

Luo ,

Manyà ,

Lü and

Li , Clause vivification by unit propagation in CDCL SAT solvers, Artificial Intelligence 279 (2020). doi:10.1016/j.artint.2019.103197.

34.

C.-M.

Li ,

Xu ,

Coll ,

Manyà ,

Habet and

He , Combining clause learning and branch and bound for MaxSAT, in: Proceedings of the 27th International Conference on Principles and Practice of Constraint Programming, CP, Montpellier, France (Virtual Conference), LIPIcs, Vol. 210, Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2021, pp. 38:1–38:18.

35.

C.M.

Li,

Manyà,

N.O.

Mohamedou and

Planes, Exploiting cycle structures in Max-SAT, in: Proceedings of the 12th International Conference on Theory and Applications of Satisfiability Testing, SAT-2009, LNCS, Vol. 5584, Springer, Swansea, UK, 2009, pp. 467–480. doi:10.1007/978-3-642-02777-2_43.

36.

C.M.

Li,

Manya,

N.O.

Mohamedou and

Planes, Resolution-based lower bounds in MaxSAT, Constraints 15(4) (2010), 456–484. doi:10.1007/s10601-010-9097-9.

37.

C.M.

Li and

Manyà , MaxSAT, hard and soft constraints, in: Handbook of Satisfiability, 2nd edn, IOS Press, 2021, pp. 903–927.

38.

C.M.

Li ,

Manyà and

Planes , Exploiting unit propagation to compute lower bounds in branch and bound Max-SAT solvers, in: Proceedings of the 11th International Conference on Principles and Practice of Constraint Programming, CP-2005, LNCS, Vol. 3709, Springer, Sitges, Spain, 2005, pp. 403–414.

39.

C.M.

Li ,

Manyà and

Planes , Detecting disjoint inconsistent subformulas for computing lower bounds for Max-SAT, in: Proceedings of the 21st National Conference on Artificial Intelligence, AAAI-2006, Boston/MA, USA, 2006, pp. 86–91.

40.

C.M.

Li ,

Manyà and

Planes , New inference rules for Max-SAT, Journal of Artificial Intelligence Research 30 (2007), 321–359. doi:10.1613/jair.2215.

41.

J.H.

Liang ,

Oh ,

Ganesh ,

Czarnecki and

Poupart , MapleCOMSPS, MapleCOMSPS LRB, MapleCOMSPS CHB, in: Proceedings of SAT Competition 2016: Solver and Benchmark Descriptions, 2016, pp. 52–53.

42.

Luby ,

Sinclair and

Zuckerman , Optimal speedup of Las Vegas algorithms, Information Processing Letters 47(4) (1993), 173–180. doi:10.1016/0020-0190(93)90029-9.

43.

Luo ,

C.-M.

Li ,

Xiao ,

Manyà and

Lü , An effective learnt clause minimization approach for CDCL SAT solvers, in: Proceedings of IJCAI 2017, 2017, pp. 703–711. doi:10.24963/ijcai.2017/98.

44.

V.M.

Manquinho ,

Marques-Silva and

Planes , Algorithms for weighted Boolean optimization, in: Proceedings of SAT 2009, LNCS, Vol. 5584, Springer, 2009, pp. 495–508.

45.

María , Bonet ,

Levy and

Manyà , A complete calculus for Max-SAT, in: Proceedings of the 9th International Conference on Theory and Applications of Satisfiability Testing, SAT-2006, LNCS, Vol. 4121, Springer, Seattle, USA, 2006, pp. 240–251. doi:10.1007/11814948_24.

46.

María , Bonet ,

Levy and

Manyà , Resolution for Max-SAT. Artificial Intelligence 171(8–9) (2007), 240–251.

47.

Marques-Silva and

V.M.

Manquinho , Towards more effective unsatisfiability-based maximum satisfiability algorithms, in: Proceedings of SAT 2008, LNCS, Vol. 4996, Springer, 2008, pp. 225–230.

48.

Martins ,

V.M.

Manquinho and

Lynce , Open-WBO: A modular MaxSAT solver, in: Proceedings of SAT 2014, LNCS, Vol. 8561, Springer, 2014, pp. 438–445.

49.

M.W.

Moskewicz ,

C.F.

Madigan ,

Zhao ,

Zhang and

S.M.

Chaff , Engineering an efficient SAT solver, in: Proceedings of DAC 2001, ACM, 2001, pp. 530–535.

50.

Narodytska and

Bacchus , Maximum satisfiability using core-guided MaxSAT resolution, in: Proceedings of AAAI 2014, 2014, pp. 2717–2723.

51.

Niedermeier and

Rossmanith , New upper bounds for maximum satisfiability, Journal of Algorithms 36 (2000), 63–88. doi:10.1006/jagm.2000.1075.

52.

Paxian and

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

53.

Saikko ,

Berg and

Järvisalo , LMHS: A SAT-IP hybrid MaxSAT solver, in: Proceedings of SAT 2016, LNCS, Vol. 9710, 2016, pp. 539–546.

54.

Shen and

Zhang , Study of lower bound functions for MAX-2-SAT, in: Proceedings of the 19th National Conference on Artificial Intelligence, AAAI-2004, San Jose/CA, USA, 2004, pp. 185–190.

55.

Stepan , Improving implementation of SAT competitions 2017–2019 winners, in: Proceedings of SAT 2020, LNCS, Vol. 12178, 2020, pp. 139–148.

56.

Trösser ,

De Givry and

Katsirelos , Relaxation-aware heuristics for exact optimization in graphical models, in: Prodeedings of CPAIOR 2020, Springer, 2020, pp. 475–491.

57.

Xing and

Zhang , An efficient exact algorithm for (weighted) maximum satisfiability, Artificial Intelligence 164(2) (2005), 47–80. doi:10.1016/j.artint.2005.01.004.

58.

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

$\neg y_{1} \lor y_{2} \lor \neg x_{2}$	$\neg y_{2} \lor \neg x_{3} \lor \neg x_{4}$	$\neg y_{2} \lor \neg y_{5} \lor x_{6}$	$\neg x_{1} \lor x_{4}$	$\neg y_{3} \lor x_{3}$
$\neg x_{6} \lor \neg x_{5} \lor y_{6}$	$\neg y_{6} \lor \neg x_{2} \lor x_{7}$	$\neg x_{7} \lor \neg y_{6}$	$\neg y_{4} \lor x_{8}$	$\neg y_{7} \lor x_{9}$

Boosting branch-and-bound MaxSAT solvers with clause learning

Abstract

Keywords

1. Introduction

2. Preliminaries

4. Branch-and-bound MaxSAT solvers

4.2. Improving the lower bound with inference

5. MaxCDCL: A BnB algorithm using CDCL for MaxSAT

5.1. General structure of MaxCDCL

5.4. Soft literal ordering in lookahead

5.5. Improving the VSIDS heuristic by lookahead

5.6. Implementation of MaxCDCL

1 The source code of MaxCDCL is available at https://home.mis.u-picardie.fr/~cli/EnglishPage.html.

5.8. Failed literal detection

6. Experimental evaluation

2 www.cs.toronto.edu/maxsat-lib/maxsat-instances/master-set/unweighted/

3 http://maxsat.ia.udl.cat/results/

Footnotes

Acknowledgements

References

¹
The source code of MaxCDCL is available at https://home.mis.u-picardie.fr/~cli/EnglishPage.html.

²
www.cs.toronto.edu/maxsat-lib/maxsat-instances/master-set/unweighted/

³
http://maxsat.ia.udl.cat/results/