Combining Clause Learning and Branch and Bound for MaxSAT (Extended Abstract)

1 Introduction

The Maximum satisfiability problem (MaxSAT) is an optimization version of the satisfiability problem (SAT). The goal of MaxSAT is to find an assignment that satisfies the maximum number of clauses in a given multiset. If we distinguish between hard and soft clauses, we have Partial MaxSAT and its goal is to satisfy all the hard clauses and the maximum number of soft clauses. This paper considers both MaxSAT and Partial MaxSAT.

SAT and MaxSAT share many features, but in practice solving MaxSAT is much harder than solving SAT. Indeed, since several clauses can be falsified in a MaxSAT solution, some fundamental SAT techniques such as unit propagation cannot be used in MaxSAT as they are used in SAT. Despite this difficulty, thanks to the huge efforts of the scientific community, it is currently possible to solve many challenging real-world and academic NP-hard optimization problems encoded as MaxSAT instances. For this reason, MaxSAT has received a growing interest from academy and industry in recent years.

∗This is an extended abstract of a paper that won the Best Paper Award at the 27th International Conference on Principles and Practice of Constraint Programming (CP 2021).

We distinguish two types of exact MaxSAT algorithms: Branch-and-Bound (BnB) algorithms [Li and Many`a, 2021], which directly tackle MaxSAT with a bounding procedure but without unit propagation and clause learning; and SATbased algorithms [Bacchus et al., 2021], which transform MaxSAT into a sequence of SAT instances that are solved with a Conflict-Driven Clause Learning (CDCL) SAT solver.

SAT-based MaxSAT solvers are usually much better than BnB MaxSAT solvers in solving many real-world optimization problems because they indirectly exploit clause learning via the SAT solver. Unfortunately, it is hard for a BnB solver to exploit clause learning. In a CDCL SAT solver, a backtracking happens only when a clause is falsified, from which a sequence of resolution steps is performed to learn a clause explaining the backtracking. However, a BnB MaxSAT solver also needs to backtrack when it computes a lower bound equal to the upper bound [Li et al., 2007]. In this case, no clause is explicitly falsified, making it hard to learn a clause. Probably because of this difficulty, there has been no advance allowing to significantly speed up BnB MaxSAT solvers in recent 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, because the one in current BnB MaxSAT solvers is not adequate for large instances. This approach is implemented in a new BnB MaxSAT solver, called MaxCDCL. The experimental results show that MaxCDCL is among the top 5 out of a total of 15 exact solvers in the 2020 MaxSAT Evaluation, solving several instances that other solvers cannot solve. Furthermore, MaxCDCL, when combined with the best existing solvers, solves the highest number of instances from different MaxSAT Evaluations. More importantly, our results refute the prevailing opinion stating that, although BnB is a powerful technique in combinatorial optimization, it is not really useful for MaxSAT.

This paper is an extended abstract of [Li et al., 2021]. The original paper contains additional experiments and a more detailed description of MaxCDCL, including techniques and implementation details that have a high impact on the performance of the solver.

2 MaxCDCL: A BnB AlgorithmUsing CDCL for MaxSAT

This section describes the general structure of MaxCDCL and the two most relevant techniques of MaxCDCL: the combination of BnB and clause learning, and the new bounding procedure.

We first review some basic concepts: A Partial MaxSAT instance ϕ is formed by a multiset of hard and soft clauses, where a clause is a disjunction of literals and a literal is a propositional variable x or its negation ¬x. An assignment for ϕ assigns either true (1) or false (0) to each variable of ϕ, satisfies a clause if some literal is true, and falsifies a clause if all its literals are false. A clause is unit if all literals are false but one is unassigned. Partial MaxSAT is to find an assignment that satisfies all the hard clauses and the maximum number of soft clauses. SAT is Partial MaxSAT without soft clauses and (unweighted) MaxSAT is Partial MaxSAT without hard clauses.

2.1 General Structure of MaxCDCL

MaxCDCL represents the input partial MaxSAT instance using two sets: H and S. Set H contains the input hard clauses and set S contains a new literal y for each input soft clause sc after adding the hard clauses encoding y ↔ sc to H. We say that y is a soft literal because it is satisfied if and only if the corresponding soft clause is satisfied. The cost of a solution is the number of falsified soft clauses and is equal to |falseS|, where falseS denotes the set of falsified soft literals.

MaxCDCL is a generalization of the CDCL SAT algorithm. Roughly speaking, a CDCL SAT solver explores a search tree by alternating a search phase, where literals are assigned until either a solution or a conflict is found, and a learning phase that is executed after finding a conflict to learn a new clause. Unit Propagation (UP) is the main inference rule applied during the search: if there is a unit clause in H, its unassigned literal l must be set to 1. UP is applied during the search until a clause is falsified (a conflict is found) or no more unit clauses remain in H. If UP terminates 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. A solution is found when all the variables are assigned without finding a conflict.

Following the BnB procedure, MaxCDCL tries to find a solution whose cost is smaller than a given upper bound UB. When a solution is found, the UB is decreased by taking as value the cost of this solution. During the search, MaxCDCL distinguishes between hard and soft conflicts. A hard conflict occurs when the current partial assignment falsifies a hard clause. A soft conflict occurs when the current partial assignment cannot be extended to a complete one falsifying fewer than UB soft clauses. MaxCDCL extends the CDCL SAT solver by also learning a hard clause from each discovered soft conflict.

Concretely, when UP does not falsify any hard clause, it calls, under certain conditions, a lookahead (LA) procedure to compute a lower bound LB of the number of soft literals that will be falsified if the current partial assignment is extended. If a soft conflict is discovered, i.e., if LB≥UB, it is analyzed to learn a clause for backtracking. Moreover, if no soft conflict is discovered, but LB = UB-1, MaxCDCL satisfies every free soft literal y not involved in the computation of LB by applying a procedure called hardening.

2.2 Combining Lookahead and Clause Learning

A subset of soft literals Si = {y1, . . . , y|Si|}, where |Si| ≥ 1, is inconsistent if they cannot be simultaneously satisfied. This inconsistency can be represented by the hard clause ¬y1 ∨ · · ·∨¬y|Si|. 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.

Example 1. Let H = {¬y1 ∨ x1 ∨ ¬x2, ¬x1 ∨ ¬x3 ∨ ¬x4, ¬y2 ∨ x3, ¬y3 ∨ x5}, where y1, y2 and y3 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 {x2 = 1, x4 = 1}, the subset of soft literals {y1, y2} is a local core implied by the partial assignment. We write the implication by H∪{x2, x4} → ¬y1∨¬y2.

Proposition 1 provides the foundation of our approach in the general case.

Proposition 1. Let H be a set of hard clauses, S = {y1, . . . , y|S|} be the set of all soft literals, k be an integer, and Li = {li1, . . . , li|Li|} (1 ≤ i ≤ k) be a set of literals. If, for every i (1 ≤ i ≤ k), H ∪ Li implies a local core Si = {zi1, . . . , zi|Si|} ⊂ S (i.e., H ∪ Li → ¬zi1 ∨ · · · ∨ ¬zi|Si|), and Si and Sj are disjoint for any j ̸= i such that 1 ≤ j ≤ k, then every assignment that satisfies H ∪ {¬y1 + · · · + ¬y|S| < k} also satisfies the clause ¬l11 ∨ · · · ∨ ¬l1|L1| ∨ · · · ∨ ¬lk1 ∨ · · · ∨ ¬lk|Lk|.

Given a partial assignment F of H, the application of Proposition 1 consists in first detecting a local core Si and then identifying the smallest Li ⊂ F such that H ∪ Li implies Si. If k is the current upper bound UB and k disjoint local cores are detected, a soft conflict is discovered, and the clause ¬l11 ∨ · · · ∨¬l1|L1| ∨ · · · ∨¬lk1 ∨ · · · ∨¬lk|Lk|, which is implied by H ∪{¬y1 +· · ·+¬y|S| < k} and is falsified by the current partial assignment, can be considered an implicit clause explaining the soft conflict. This clause can be further analyzed with standard SAT conflict analysis techniques to learn a clause to be explicitly added to H to prevent the same soft conflict in the future, exactly as in the hard conflict case.

The detection of a local core Si is implemented by using UP in a lookahead procedure as in existing BnB MaxSAT solvers [Li et al., 2009; Li et al., 2005; Li et al., 2006]. The advantage of this procedure is that Si is minimal w.r.t. UP, in the sense that UP cannot detect any local core that is a proper subset of Si under the same partial assignment [Li et al., 2010]. This advantage is essential for our approach, because MaxCDCL needs to learn clauses of good quality from the detected local cores. The other existing BnB MaxSAT solvers [Abram´e and Habet, 2014; Heras et al., 2008; Kuegel, 2010; Li et al., 2007] detect disjoint local cores, but instead of explaining them with a learnt clause they simply backtrack, which is very different fromMaxCDCL.

2.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 0.01, lookahead is applied for probing purposes. The mean avgp and the standard deviation devp of the number of detected 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.

3 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:

MSE19∪20: The union of all the instances used in the complete unweighted track of the MaxSAT Evaluations (MSE) 2019 and 2020, considering a total of 1000 distinct instances. MC: A subset of the Master Collection of instances from the MaxSAT evaluations held until 2019 1 , which contains 76 subfamilies of (partial) MaxSAT instances. 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.

The cutoff time is one hour (3600s) per instance as in the MaxSAT Evaluation. For MaxCDCL and its variants, this includes 60 seconds to find a feasible upper bound UBf with SatLike (version 3.0) [Cai and Lei, 2020].

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. Finally, 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.

1 www.cs.toronto.edu/maxsat-lib/maxsat-instances/masterset/unweighted/

3.1 MaxCDCL Components

Table 1 compares MaxCDCL with the following variants:

MaxCDCL\LA. MaxCDCL without lookahead, i.e., soft conflicts are only detected when |falseS|=UB.

MaxCDCL\harden. MaxCDCL without hardening.

MaxCDCLalwaysLA. MaxCDCL with lookahead at every branch without using the probing strategy of Section 2.3.

In Table 1, columns "#solv" give the number of solved instances and columns "avg" give the mean time in seconds (including the 60s 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 the selective and adaptive application of lookahead. The absence of any of these components leaves a significant number of instances out of reach of MaxCDCL.

3.2 Comparison with Top 5 Solvers inMSE2020

A total of 15 solvers competed in the complete unweighted track of MSE2020 [Bacchus et al., 2020]. We consider the top 5 solvers: MaxHS (mhs in short) [Bacchus, 2020], EvalMaxSAT (eval in short) [Avellaneda, 2020], RC2-B (rc2 in short) [Ignatiev et al., 2019], open-wbo-res-mergesat-v2 (Open-WBO or owbo in short) [Martins et al., 2014], and UWrMaxSAT (uwr in short) [Piotr´ow, 2020]. We executed the versions used in MSE2020 in all the experiments. Table 2 shows the results for MSE19∪20 and MC, respectively.

We observe that MaxCDCL solves more instances than two and four top 5 solvers in MSE19∪20 and MC, respectively. More importantly, MaxCDCL solves a significant number of instances that other solvers cannot solve. For example, MaxCDCL solves 116 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 can solve: 16 instances in MSE19∪20 and 67 instances in MC. These results show that the existing MaxSAT solvers can solve similar classes of instances. However, 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 in a broad community.

3.3 CombiningMaxCDCL with Existing Solvers

Given two deterministic solvers X and Y , the easiest way to try to solve more instances than X and Y alone within a time limit T is to combine X and Y by running X within a time limit T/2, and then Y from scratch within the remaining time T/2 if the instance is not solved by X. Table 3 shows the results of all possible pairwise combinations of the top 5 solvers in MSE2020 and MaxCDCL (mcdcl) for T = 3600s.

Combining any of the top 5 solvers with MaxCDCL solves more instances than this solver and MaxCDCL alone within 3600s, while this is not always true when combining two top 5 solvers. 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 (785 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 only solves 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 MaxHS alone, and 57 instances more than the best combination without MaxCDCL.

4 Conclusion

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 performance of MaxCDCL comes from a careful configuration combining clause learning and BnB, including hardening based on local core detection and the selective and adaptive application of lookahead.

Unlike SAT-based MaxSAT solvers, which use a CDCL SAT solver as a black box and do not interfere in the internal operations of the SAT solver, MaxCDCL itself can be considered a SAT solver extended to handle soft conflicts. Also, unlike model-guided SAT-based solvers, MaxCDCL computes a lower bound LB of the number of soft clauses that will be falsified (but are not yet falsified), and therefore it can backtrack much earlier. MaxCDCL, core-guided or MHS-guided MaxSAT solvers all identify cores. However, the latter only identify global cores (i.e., the cores that do not depend on any partial assignment), while MaxCDCL detects local cores by using UP under a partial assignment to derive a soft conflict for learning a clause and backtracking early.

MaxCDCL is ranked among the top 5 exact MaxSAT solvers in MSE2020. 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 current MaxSAT techniques cannot solve.

The proposed approach opens new and promising research directions, including the exploitation of the relationships between SAT and MaxSAT, the adaptation of the MaxCDCL approach to other problems such as pseudo-Boolean optimization and Max-CSP, or the extension of MaxCDCL to weighted MaxSAT.

Acknowledgments

This work has been partially funded by the French Agence Nationale de la Recherche, reference ANR-19-CHIA0013-01, and project PID2019-111544GB-C21 funded by MCIN/AEI/10.13039/501100011033, and partially supported by Archimedes Institute, Aix-Marseille University. F. Many`a was supported by mobility grant PRX21/00488 of the Ministerio de Universidades. We thank the Universit´e de Picardie Jules Verne for providing the Matrics Platform.