Exploiting the Structure of Unsatisfiable Cores in MaxSAT

1 Introduction

Maximum Satisfiability (MaxSAT) is an optimization version of the well-known Satisfiability (SAT) problem. Recently, we have seen the successful application of MaxSAT techniques to solve several industrial or real combinatorial optimization problems: software package upgrade, debugging of hardware designs, fault localization in C code, bioinformatics, course timetabling, planing, scheduling, routing, electronic markets, combinatorial auctions, etc. See [Ans´otegui et al., 2013b; Morgado et al., 2013] for citations.

Solving exactly combinatorial optimization problems, i.e., finding and certifying the best possible assignment, can be NP-hard from a computational point of view. However, many industrial problems are slightly beyond the reach of state-ofthe-art techniques, and for many real domains we are often interested on improving in a reasonable time the best current assignment. Notice that even a small gain in the quality of the assignment can lead to important practical consequences for real domains.

This seems to suggest we should focus on developing incomplete algorithms for industrial problems. The experience achieved from the international SAT and MaxSAT competitions, shows us that the right research avenue is to focus first on improving complete or exact algorithms. Then, with the proper modifications, we can get an incomplete algorithm. Besides, we can always incorporate our complete algorithm into incomplete approaches such as Large Neighborhood Search [Shaw, 1998]. In LNS, we heuristically dive

∗Research partially supported by the Ministerio de Econom´ıa y Competividad research project TASSAT2: TIN2013-48031-C4-4-P and Google Faculty Research Award program.

Joel Gab`as

DIEI, Univ. of Lleida, Spain jgabas@diei.udl.es

into promising regions of the search space (neighborhoods) that are explored with complete solvers.

The aim of this paper is to improve and combine effectively and efficiently techniques from complete state-of-theart solvers MaxSAT solvers. In particular, we pay special attention to how to exploit the structure of the unsatisfiable cores in a MaxSAT instance. Finally, develop a complete algorithm that can be used in an incomplete approach.

In the MaxSAT community, we find two main classes of complete algorithms: branch and bound [Heras et al., 2007; Li et al., 2009; K¨ugel, 2010] and SAT-based [Ans´otegui et al., 2013b; Morgado et al., 2013]. SAT-based approaches clearly dominate on industrial instances. SAT-based MaxSAT algorithms reformulate a MaxSAT instance into a sequence of SAT instances. By solving these SAT instances the MaxSAT problem can be solved. Intuitively, the SAT instances encode whether it is possible to find an assignment to the MaxSAT instances with a cost less than or equal to a certain k. The sequence is built in increasing order of k and it can be split into two parts. The instances in the first part are all unsatisfiable while the instances in the second one are all satisfiable. The value of k where the first satisfiable instance is located gives us the optimum of the MaxSAT instance. This transition from unsatisfiable to satisfiable SAT instances is usually associated with an easy-hard-easy pattern in terms of the hardness of the SAT instances [Shen and Zhang, 2003].

By solving the unsatisfiable SAT instances MaxSAT solvers refine the lower bound, while by solving satisfiable instances they refine the upper bound. Within SAT-based MaxSAT algorithms we find two main classes: (i) those that refine the lower bound, and guide the search with the unsatisfiable cores obtained from unsatisfiable SAT instances (core-guided algorithms) and, (ii) those that refine the upper bound, and guide the search with the satisfiable assignments obtained from satisfiable SAT instances (model-guided algorithms). Both approaches have strengths and weaknesses and there have been already some hybrid approaches [Morgado et al., 2012; Ans´otegui and Gab`as, 2013].

SAT-based MaxSAT solvers use Pseudo-Boolean (PB) constraints to create the SAT instances in the sequence. It is known that efficiency of SAT-based MaxSAT solvers heavily depends on how complex are these PB constraints, and how efficiently we manage them. Respect complexity, our current approach, as in [Andres et al., 2012; Morgado et al., 2014], only adds cardinality (Card) constraints (PB constraints with coefficients equal to 1) even if the MaxSAT instance is weighted. Respect management, unlike [Morgado et al., 2014; Narodytska and Bacchus, 2014; Martins et al., 2014], where Card constraints are incrementally constructed, our best approach does not use yet these incremental strategies for Card constraints. It exploits the structure of the unsatisfiable cores to produce a more efficient encoding for the Card constraints.

As we have mentioned, the algorithm we present is able to produce upper bounds during the search process. We also use these upper bounds to extend a very effective technique used in SAT solvers called phase saving [Pipatsrisawat and Darwiche, 2007] to MaxSAT.

Finally, we show an extensive experimental investigation on industrial instances. From the results, we can conclude that our approach outperforms clearly both in terms of robustness and number of solved instances the winners of the international MaxSAT Evaluation 2014 (MSE14) at the complete and incomplete tracks.

This paper proceeds as follows. Section 2 introduces some preliminary concepts. Section 3 presents the complete MaxSAT algorithm. Section 4 discusses how to encode efficiently in SAT the Card constraints generated by the MaxSAT algorithm. Section 5 explains how to exploit the upper bounds generated by the MaxSAT algorithm. Section 6 shows the experimental evaluation. Finally, Section 7 concludes.

2 Preliminaries

Definition 1 A literal l is either a Boolean variable x or its negation x. A clause c is a disjunction of literals. A SAT formula is a set of clauses that represents a Boolean formula in Conjunctive Normal Form (CNF), i.e. a conjunction of clauses.

Definition 2 A weighted clause is an ordered pair 〈c,w〉, where c is a clause and w is a natural number or infinity (indicating the cost of falsifying c, see Definitions 4 and 5). If w is infinite the clause is hard, otherwise it is soft.

Definition 3 A Weighted Partial MaxSAT (WPMS) formula is an ordered multiset of weighted clauses:

where the first s clauses are soft and the last h clauses are hard. The presence of soft clauses with different weights makes the formula Weighted and the presence of hard clauses makes it Partial. The ordered multiset of weights of the soft clauses in the formula is noted as w(ϕ). The top weight of the formula is noted as W(ϕ), and defined as W(ϕ) = ∑ w(ϕ) + 1. By ϕS we refer the set of soft clauses and by ϕH to the set of hard clauses. Finally, the set of variables occurring in the formula is noted as var(ϕ).

Example 1 Given the following WPMS formula: ϕ = 〈〈x1, 5〉, 〈x2, 3〉, 〈x3, 3〉, 〈x1 ∨ x2,∞〉, 〈x1 ∨ x3,∞〉, 〈x2 ∨ x3,∞〉〉, we have that w(ϕ) = 〈5, 3, 3〉, W(ϕ) = 12, ϕS = 〈〈x1, 5〉, 〈x2, 3〉, 〈x3, 3〉〉, ϕH = 〈〈x1 ∨ x2,∞〉, 〈x1 ∨ x3, ∞〉, 〈x2 ∨ x3, ∞〉〉 and var(ϕ) = {x1, x2, x3}.

Definition 4 An assignment for a set of Boolean variables X is a function I : X → {0, 1}, that can be extended to literals, (weighted) clauses, SAT formulas and WPMS formulas as follows:

We will refer to the value returned by an assignment I on a weighted clause or a WPMS formula as the cost of I.

Definition 5 We say that an assignment I satisfies a clause or a SAT formula if the value returned by I is equal to 1. In the case of SAT formulas, we will refer also to this assignment as a satisfying assignment or solution. Otherwise, if the value returned by I is equal to 0, we say that I falsifies the clause or the SAT formula.

Definition 6 The SAT problem for a SAT formula ϕ is the problem of finding a solution for ϕ. If a solution exists the formula is satisfiable, otherwise it is unsatisfiable.

Definition 7 Given an unsatisfiable SAT formula ϕ, an unsatisfiable core ϕC is a subset of clauses ϕC ⊆ ϕ that is also unsatisfiable.

Definition 8 A SAT algorithm for the SAT problem, takes as input a SAT formula ϕ and returns an assignment I such that I(ϕ) = 1 if the formula is satisfiable. Otherwise, it returns an unsatisfiable core ϕC.

Given unlimited resources of time and memory, we say that a SAT algorithm is complete if it terminates for any SAT formula. Otherwise, it is incomplete.

Definition 9 The optimal cost (or optimum) of a WPMS formula ϕ is cost(ϕ) = min{I(ϕ) | I : var(ϕ) → {0, 1}} and an optimal assignment is an assignment I such that I(ϕ) = cost(ϕ). We will refer to this assignment as a solution for ϕ if I(ϕ) ̸=∞. Any cost above (below) cost(ϕ) is called an upper (lower) bound for ϕ.

Example 2 Given the WPMS formula ϕ of Example 1, we have that cost(ϕ) = min{6, 8, 11,∞} = 6 and the optimal assignment I maps 〈x1, x2, x3〉 to 〈1, 0, 0〉.

Definition 10 The Weighted Partial MaxSAT problem for a WPMS formula ϕ is the problem of finding a solution for ϕ. If a solution does not exist the formula is unsatisfiable.

Definition 11 A WPMS algorithm for the WPMS problem, takes as input a WPMS formula ϕ and returns an assignment I, such that, I(ϕ) ≥ cost(ϕ).

Given unlimited resources of time and memory, we say that a WPMS algorithm is complete or exact if for any input WPMS formula ϕ and returned I, I(ϕ) = cost(ϕ). Otherwise, we say it is incomplete.

Definition 12 An integer linear Pseudo-Boolean (PB) constraint is an inequality of the form w1x1 + · · · +wnxn op k, where op ∈ {≤,≥,=,>,<}, k and wi are integer coefficients, and xi are Boolean variables. A PB at-most constraint is a PB constraint where op is ≤. A cardinality (Card) constraint is a PB constraint where the coefficients wi are equal to 1.

3 WPM3MaxSAT Algorithm

Algorithm 1: WPM3

Function sat(ϕ, AM, wstrat)

1 ϕk := ϕH ∪ {ci ∨ bi} 〈ci ,wi〉∈ϕS ∪ { CNF (Aj , kj ) ∨ aj , aj 〈Aj ,kj ,wj 〉∈AM,wj≥wstrat } 2 〈st, ϕkC , I〉 := satsolver(ϕk ) 3 C := {j | {aj} ∩ϕkC ̸= ∅} 4 return 〈st,C, I〉

Function optimize(ϕ, AM)

In this section, we present the WPM3 complete algorithm for the MaxSAT problem. Given an input WPMS formula ϕ, WPM3 solves the formula by testing the satisfiability of a sequence of SAT instances ϕk where 0 ≤ k ≤ W(ϕ). Each SAT instance ϕk encodes whether there is an assignment to ϕ with a cost ≤ k. Notice that SAT instances with k < cost(ϕ) are unsatisfiable, otherwise they are satisfiable. The optimum corresponds to the k of the first satisfiable SAT instance.

Roughly speaking, from every unsatisfiable SAT instance the algorithm finds and keeps an unsatisfiable core. WPM3 is designed to be aware of the global structure of theses cores. This is used both for producing more efficient cardinality (Card) constraint encodings (see Section 4) and focus the search on subproblems of the input MaxSAT instance.

The algorithm maintains a set of soft at-most Card constraints AM. We note these constraints as 〈A, k,w〉, where A is an ordered multiset of indexes of the original soft clauses, k indicates at most how many clauses from A can be falsified, and w is the cost for falsifying this soft constraint. The at-most constraints are used to do not accept those solutions whose cost exceeds the current k, where k = ∑〈Aj,kj,wj〉∈AM kj · wj. Moreover, the algorithm guarantees that k ≤ cost(ϕ). The idea of maintaining multiple atmost Card constraints instead of a single one was originally introduced in [Ans´otegui et al., 2009a] for PM2 algorithm. Notice that from the AM set the global core structure can be obtained.

We start (line 1) by adding to AM a soft at-most constraint for each original soft clause. Then, the algorithm will iterate (line 2) till it is able to determine cost(ϕ). This will happen if it detects that the set of hard clauses is unsatisfiable (line 8, cost(ϕ) = ∞) or when it is able to generate the first satisfiable instance (line 5, cost(ϕ) = k = I(ϕ)). We obviate for the moment the role of wstat and we consider it is ∞ for the first iteration and min({wj}) wj ∈w(AM),wj ̸=0 for the rest.

Function sat (line 3) builds the SAT instance ϕk at the current iteration and sends it to the SAT solver. ϕk is constructed through the union of the following sets expressed as SAT clauses: (i) the set of hard clauses, (ii) the reification to variables bi of soft clauses, (iii) the reification to variables aj of the translation into CNF of the at-most constraints in AM, and finally (iv) the unit clauses aj. The new bi variables are true if the respective original soft clause becomes false. They are used to encode the at-most constraints which restrict the number of falsified soft clauses. The new aj variables are true if the respective at-most constraint becomes false. The unit clauses aj encode that we would like to satisfy all the at-most constraints. If this is not possible, some of them will appear into the unsatisfiable core ϕkC .

To our best knowledge, the idea of introducing Card constraints as soft constraints in a core-guided algorithm was initially proposed in [Andres et al., 2012] for Answer Set Programming (ASP) optimization problems, and recently adapted to MaxSAT problems in [Morgado et al., 2014]. The approach in [Narodytska and Bacchus, 2014] (best solver for industrial instances at MSE14) also uses soft Card constraints. These approaches work locally and are not aware of the global core structure and therefore they can not exploit it.

Going back to WPM3 algorithm, if function sat returns satisfiable (st = SAT) (line 4), then we return the optimal assignment I and its cost (line 5). Otherwise (line 7), C is the set of indexes of at-most constraints involved into the last unsatisfiable core. If the core only involves original hard clauses, we can return unsatisfiable (line 8). If there are atmost constraints involved in the core, then, we need to relax some of them since they only allow assignments or solutions with a cost strictly less than cost(ϕ).

At this stage (lines 9-12), we need to relax the set of AM constraints, but guaranteeing we do not exceed cost(ϕ). Basically, we need to replace the set of at-most constraints AMC involved in the last core with a new set of at-most constraints which allows assignments with a higher cost.

Since we will only use Card constraints we first apply the idea described in the WPM1/WBO [Ans´otegui et al., 2009b; Manquinho et al., 2009] MaxSAT algorithms to deal with Weighted instances (lines 9-10). It basically prevents the algorithm to introduce PB constraints instead of Card constraints when the at-most constraints involved in the core have different weights. In this case, we compute the minimum weight wmin of the constraints in AMC (line 9), and replace every soft constraint 〈Aj , kj , wj 〉 by two copies with weights wj -wmin and wmin. The first set of copies will remain in AM (line 10) while the second will be replaced by the new at-most constraint 〈A, kA,wmin〉 (line 12). Notice we guarantee that ∑〈Aj,kj,wj〉∈AM | Aj | ·wj = ∑ w(ϕ).

Function optimize (line 11) allows to determine which is the new ϕk we will test. This function, basically, solves exactly the subproblem that involves the new at-most constraint we will generate on the original soft clauses, and the hard clauses. The result is the set of indexes of original soft clauses A of the new at-most constraint (notice that and index can be repeated) and the number of clauses kA that we will at most allow to be falsified. To our best knowledge, the idea of solving a subproblem of the original optimization instance ϕ was originally applied for MaxSAT in WPM2 algorithm [Ansotegui et al., 2010]. In [Davies and Bacchus, 2011] a similar approach is applied calling a MIP solver to solve the subproblem. Recently, in [Ans´otegui et al., 2013a], this process is extended and named as cover optimization. The best strategy reported consists on refining iteratively the upper bound on the subproblem using the model-guided MaxSAT algorithm in [Berre, 2006]. We apply it within function optimize, although depending on the particular family of instances other strategies or algorithms can have better performance. At this point we have increased k by (kA-∑〈Aj,kj,wj〉∈AMC kj)·wmin towards cost(ϕ). Otherwise, without the optimize step, we can only increase k by wmin.

Treating explicitly the new at-most constraint (line 12) and its relation to the constraints it substitutes is fundamental, not only for function optimize, but also to encode more efficient Card constraints (see Section 4). In contrast, this information, the global core structure, is not explicitly present in recent approaches as [Morgado et al., 2014; Narodytska and Bacchus, 2014] and therefore harder to be exploited efficiently.

During this description, we have obviated the role of wstrat (lines 5 and 6). It corresponds to the application of the stratified approach introduced in [Ansotegui et al., 2009c]. The stratified approach consists in sending to the SAT solver only a subset of the soft clauses, i.e., those with a weight ≥ wstrat. Function decrease updates conveniently wstrat. This can help to reduce the size of the unsatisfiable cores, produce simpler at-most constraints and progress faster to the optimum. We also apply hardening techniques like the ones described in [Ans´otegui et al., 2012; Morgado et al., 2012; Ans´otegui et al., 2013a].

4 Efficient Card Constraints for MaxSAT

In the last decade, we have seen many contributions on how to encode efficiently PB and Card constraints into SAT [Bailleux and Boufkhad, 2003; Sinz, 2005; E´en and S¨orensson, 2006; Bailleux et al., 2009; As´ın et al., 2011]. The goal is to achieve an arc-consistent encoding (i.e., with good propagation properties) as small as possible.

Since WPM3 only uses Card constraints, let us consider the Card constraint: b1 + · · · + bn ≤ k. From the sake of clarity, the encoder is split into two black boxes: the sum and the operator op (in our case representing ≤). The sum takes as input a list of n variables [b1, . . . , bn] and returns a set of SAT clauses S and a list of m variables [o1, . . . , om]. The operator takes as input the o variables and integer k and returns a set of SAT clauses OP . The encoding of the Card constraint into SAT corresponds to the union S ∪ OP .

In our case, we use the Cardinality Networks encoding in [As´ın et al., 2011]. There, m = k + 1 and the sum builds a SAT formula such that if i of the input b variables are set to true then the first i of the output o variables are set to true and the rest to false. Therefore, op returns the unit clause ok+1.

Our first observation is that it is crucial for the efficiency of the MaxSAT solver in which order the b variables are fed into the sum. In previous MaxSAT solvers, the order of the b variables was not taken into account. They were just added in the same order of their respective soft clauses.

However, the b variables should be added taking into account the structure of the unsatisfiable cores. In particular, variables belonging to the same core should be as close as possible. In our algorithm the set A in an at-most constraint 〈A, k,w〉 is ordered. In line 1 of function optimize (see Section 3) when we generate the set A of the new at most constraint, we concatenate the sets of b variables of the at-most constraints that it replaces. Respect to latest advances in MaxSAT [Morgado et al., 2014; Narodytska and Bacchus, 2014] a deeper explanation of their efficiency could be that these algorithms implicitly preserve the order.

Our second observation has to do again with the structure of the unsatisfiable cores we have detected so far. As we have just commented, the new at-most constraint 〈A, kA,wmin〉 (line 12 of WPM3) replaces/merges other at-most constraints. In the end, we can consider that there is a tree structure that represents how we have merged the unsatisfiable cores and where the root node is the new at-most constraint. Instead of creating a Cardinality Network for the new constraint we can reproduce this tree structure. We basically reproduce the totalizer encoding proposed originally in [Bailleux and Boufkhad, 2003]. The leaf nodes join the at-most constraints related with a single soft clause of the input formula (i.e., with k = 0) that appeared in the same core. The leaf nodes are encoded with Cardinality Networks.

Example 4 Imagine at-most constraint 〈A3, 5, 1〉 (root node) replaces at-most constraints 〈A1, 3, 1〉 and 〈A2, 1, 1〉 (child 1 and child 2). Let us see how we start constructing the tree. Children are processed recursively in the same way.

The advantage of preserving this structure, in contrast to having a single Card constraint, is that we can again exploit it to derive smaller encodings. In particular, we can restrict the sums of the nodes using the lower bounds of their siblings. The upper bound for a non root node is set to the difference between the upper bound of its parent and the sum of the lower bounds of its siblings. We apply this in a top-down update process.

Example 5 At example 4, the upper bound for the root node is 5. Child 1 (child 2) already contributes with a lower bound of 3 (1), therefore the new upper bound for child 1 (child 2) is 5 - 1 = 4 (5 - 3 = 2).

Function optimize can provide assignments Iub which are upper bounds (see Section 5) for the whole formula ϕ. Using this upper bound, we can set the upper bound for the root node which corresponds to the cost of the assignment Iub on the set of soft clauses related to it.

Finally, notice that for a given at-most constraint we build from scratch its SAT encoding when we feed it into the SAT solver. Recently, in [Martins et al., 2014] it has been proposed to build Card constraints incrementally. We will explore extending our approach in this sense. As we will see in Section 6, even without the incremental extension, our approach outperforms the rest of the solvers.

5 Upper Bounds and Phase Saving

In Section 3, we have described a complete core-guided algorithm that keeps increasing a lower bound towards the optimum. However, its design and, in particular, function optimize, which implements a model-guided MaxSAT algorithm, allows to produce upper bounds for ϕ during its execution. Whenever function optimize finds a new solution to the subproblem, we can just extend this solution to the rest of the formula and check its cost. We do this by considering that, those clauses in a undefined state under the solution to the subproblem, are falsified 1 . Function optimize keeps track of the assignment to the subproblem whose extension to the rest of the formula had the lowest cost. The cost of this assignment is an upper bound for the whole problem. We will refer to it as the best global assignment found by function optimize.

1 This can be improved looking at the structure of the undefined clauses.

We can exploit further the best global assignment we get from function optimize. State-of-the-art SAT solvers apply a technique called phase saving introduced in [Pipatsrisawat and Darwiche, 2007]. In SAT solvers, when nonchronological backtracking is applied due to a conflict, lots of variable assignments get lost and have to be revealed again during search. The idea is to avoid redoing this work by storing the phase of the variables when we find a conflict. Then, we assign to the next decision variables the stored polarity till we find a new conflict and update the polarities again. This technique has been shown to be quite effective. We can extend this idea to MaxSAT in the following way. Within function optimize we let the SAT solver apply phase saving in the regular way (line 5). Then, if the best global assignment found so far has the same cost for the subproblem as the solution found by function optimize, we store the polarity of the variables in the best global assignment. We use these polarities to guide the search of the SAT solver in line 3 of WPM3, disabling the regular phase saving that would be applied. In particular, we only store the polarities of the original variables in ϕ.

6 Experimental Results

We have evaluated our approach on the industrial instances from the MaxSAT Evaluation 2014 (MSE14) [Argelich et al., 2006 2014]. We run our experiments on a cluster featured with 2.6GHz processors and a memory limit of 3.5 GB. The instance set of MSE14 is divided into three categories depending on the variant of the MaxSAT problem: MaxSAT (MS), Partial MaxSAT (PMS) or Weighted Partial MaxSAT (WPMS). In each category, instances are grouped by families: 2 for MS, 22 for PMS and 8 for WPMS. Since families have different number of instances, we considered more fair to present the solvers ranked by mean family ratio of solved instances.

We provide results for the new wpm3 MaxSAT solver and the best solvers of the MSE14. We have excluded the MaxSAT solver ISAC+ [Ans´otegui et al., 2014], since it is a portfolio and our intention here is to compare ground solvers. The ground solvers with the best overall performance at MSE14 for industrial instances were: eva500a [Narodytska and Bacchus, 2014], mscg [Morgado et al., 2014] and open-wbo [Martins et al., 2014]. We also present results for an initial version we implemented within the or-tools package [Google, 2009] which is only core-guided.

Table 1 shows our first experiment, where we evaluate the impact of each improvement on WPM3 (with a timeout of 1800 seconds). All the variations on WPM3 are implemented on top of the glucose SAT solver (version 3.0) [Audemard and Simon, 2009] . The different variations and corresponding implementations are named wpm3 with different subindexes. Subindex o stands for cover optimization (see Section 3). Regarding how Card constraints are encoded, t stands for core based tree, tk stands for core based tree with refinement of the k upper bound in sub-sums (see Section 4). Finally, p stands for phase saving extended to MaxSAT (see Section 5).

At the table, we present for each category and solver the mean ratio of solved instances per family and the total number of instances. We introduce results for wpm1/wbo [Ans´otegui et al., 2009b; Manquinho et al., 2009] and pm2 algorithms 2 . wpm3 can be considered as a hybridization of these two algorithms (see Section 3). As we can see, wpm3 clearly outperforms pm2. This is because, as described in Section 4, we build Card constraints taking into account the order imposed by the unsatisfiable cores. If we add the cover optimization technique, see wpm3o, then we get a version that would have ranked the first at MSE14 for industrial instances in terms of the total mean family ratio. The next two versions, wpm3t and wpm3tk, that further exploit the structure of the cores and improve the construction of the Card constraint, provide a total of 13 additional solved instances for PMS and 13 for WPMS. As we can see, the cover optimization technique always improves, in particular for Weighted instances at version wpm3tko. Finally, the extension of phase saving for MaxSAT improves the average running time, and it helps to solve 7 additional instances within the timeout.

Table 2 compares our best version wpm3tkop with the best performing complete solvers at MSE14 for industrial instances. Clearly, wpm3tkop dominates both on mean family ratio and total number of solved instances. A deeper analysis reveals that wpm3tkop has best ratio on 30 out of the 32 families that compose the categories, while eva500a (the second one) has best ratio on 20.

Our last experiment is presented in Table 3. Since wpm3tkop is able to produce upper bounds we also compared it with the best performing solvers wpm2014 and optimax 3 for industrial instances at the incomplete track of the MSE14. We also compared with other MaxSAT solvers that did not take part in the incomplete track but they are able to produce upper bounds: open-wbo [Martins et al., 2014] and qms [Koshimura et al., 2012]. We do not include eva500a, mscg or or-tools since they can not produce upper bounds.

2 pm2 algorithm is only designed for Partial MaxSAT instances

The timeout for the incomplete track at MSE is set to 300 seconds. For a given instance, the winners are the solvers that produce the best upper bound. The best solver is the one that won on more instances. Since these results give us a partial order, it can be misleading to report an overall winner. In table 3, we present the dominance relation between pairs of solvers on the three categories. For example, wpm3tkop (open-wbo) is able to obtain a better or equal upper bound than open-wbo (wpm3tkop) on 50 (45) ms instances, 556 (466) PMS instances and 394 (344) WPMS instances. As we can see, wpm3tkop practically dominates the rest of the solvers. The exception is qms on PMS where qms outperforms by 9 instances wpm3tkop. For this case, we extended the timeout to 1800 seconds. We found that wpm3tkop outperformed qms by 5 instances. This is somehow expected since wpm3tkop, within this timeout, solves to optimality 40 instances more than qms.

7 Conclusions

We have proposed a complete algorithm for MaxSAT that can be also used in an incomplete approach. We show how to combine several techniques. We have shown how that the design of the algorithm allows to exploit the structure of unsatisfiable cores in MaxSAT instances to build more efficient Card constraints. This opens a window to understand better the performance of the latest solvers and probably further improve them. Finally, we have shown that an extended notion of phase saving for MaxSAT is effective. Our resulting MaxSAT solver outperforms the winners for the complete and incomplete track at the last MaxSAT Evaluation.