Exploiting subproblem optimization in SAT-based MaxSAT algorithms

Abstract

The Maximum Satisfiability (MaxSAT) problem is an optimization variant of the Satisfiability (SAT) problem. Several combinatorial optimization problems can be translated into a MaxSAT formula. Among exact MaxSAT algorithms, SAT-based MaxSAT algorithms are the best performing approaches for real-world problems. We have extended the WPM2 algorithm by adding several improvements. In particular, we show that by solving some subproblems of the original MaxSAT instance we can dramatically increase the efficiency of WPM2. This led WPM2 to achieve the best overall results at the international MaxSAT Evaluation 2013 (MSE13) on industrial instances. Then, we present additional techniques and heuristics to further exploit the information retrieved from the resolution of the subproblems. We exhaustively analyze the impact of each improvement what contributes to our understanding of why they work. This architecture allows to convert exact algorithms into efficient incomplete algorithms. The resulting solver had the best results on industrial instances at the incomplete track of the latest international MSE.

1 Introduction

Combinatorial optimization problems arise in many domains: scheduling and planning, software and hardware verification, knowledge compilation, probabilistic modeling, bioinformatics, energy systems, smart cities, social networks, computational sustainability, etc. From a computational point of view, many optimization problems are NP-hard meaning that is unlikely that they admit a polynomial-time algorithm. The good news is that some real problems are already efficiently solved by state-of-the-art Constraint Programming techniques (Rossi et al. 2006) and many others are only slightly beyond the reach of these techniques.

In recent decades, Satisfiability (SAT) solvers (Biere et al. 2009) have progressed spectacularly in performance thanks to better implementation techniques and conceptual enhancements, such as Conflict Driven Clause Learning-based algorithms, which are able to reduce the size of the search space significantly in many instances of real NP-Complete problems. Every year, the community celebrates competitions where the performance of all these solvers is compared, and every year we contemplate how the number of solvable problems increases, and how instances that were considered very difficult, become easy. Thanks to these advances, nowadays the best SAT solvers can tackle industrial problems with hundreds of thousands of variables and millions of clauses. We use the term industrial in the sense of practical or real-world applications. Some extensions of SAT that have also attracted the interest of the scientific community in recent years include: Pseudo-Boolean (PB) satisfiability, Satisfiability Modulo Theories (SMT), satisfiability of Quantified Boolean Formulas, Maximum Satisfiability (MaxSAT), Model Counting (#SAT), etc. There exist also solvers for all these extensions of SAT, and competitions where they are tested.

The MaxSAT problem is the optimization version of SAT. The idea behind this formalism is that sometimes not all the constraints of a problem can be satisfied, and we try to satisfy the maximum number of them. The MaxSAT problem can be further generalized to the Weighted Partial MaxSAT (WPMS) problem. In this case, we can divide the constraints into two groups: the clauses (constraints) that must be satisfied (hard), and the ones that may or may not be satisfied (soft). In the last group, we may associate different weights with the clauses, where the weight is the cost of falsifying the clause. The idea is that not all constraints are equally important. The addition of weights to clauses makes the instance Weighted, and the separation into hard and soft clauses makes the instance Partial. The WPMS problem is a natural combinatorial optimization problem, and it has been already applied in many domains (Ansótegui et al. 2013b; Morgado et al. 2013a).

In the MaxSAT community, we find two main classes of complete algorithms: branch and bound (Heras et al. 2007; Kügel 2010; Li et al. 2009; Lin and Su 2007; Lin et al. 2008) and SAT-based (Ansótegui et al. 2012; Davies and Bacchus 2011; Heras et al. 2011; Honjyo and Tanjo 2012; Koshimura et al. 2012; Martins et al. 2011, 2012; Morgado et al. 2012).

SAT-based approaches clearly dominate on industrial and some crafted instances, as we can see in the results of the international MaxSAT Evaluation (Argelich et al. 2006-2004). SAT-based MaxSAT algorithms basically reformulate a MaxSAT instance into a sequence of SAT instances. By solving these SAT instances the MaxSAT problem can be solved (see (Ansótegui et al. 2013b; Morgado et al. 2013a) for further information). Intuitively, this sequence is built such that it can be split into two parts where the instances in the first part are all unsatisfiable while the instances in the second one are all satisfiable. By locating the phase transition point, i.e., the last unsatisfiable instance and the first satisfiable instance, we can locate the optimum of the optimization problem. As we will see, once we solve an unsatisfiable SAT instance we can refine the lower bound, while when we solve a satisfiable SAT instance we can refine the upper bound. Among SAT-based MaxSAT algorithms we also find two main classes: (i) those that focus the search on refining the lower bound, and exploit the information of unsatisfiable cores and, (ii) those that focus the search on refining the upper bound, and exploit the information of the satisfiable assignments. Both approaches have strengths and weaknesses. Our current work aims to find an efficient balance between both approaches.

In this paper, we present the improved version of the SAT-based MaxSAT algorithm WPM2 (Ansotegui et al. 2010) (see Sect. 4) presented originally in Ansótegui et al. (2013a), a more detailed experimental analysis of the new algorithm, further improvements and an incomplete version. The aim of this paper is not only to present a method that performs well, but also to understand why this is the case. This way we will be able to identify the interaction with other future improvements in the field and whether they are complementary or not to this work.

In our experimental investigation, our reference point is the original WPM2 algorithm which solves 959 out of 2078 instances from the whole benchmark of industrial and crafted instances of the MSE13.

With respect to the improvements we have incorporated, first of all, we extend the original WPM2 algorithm by applying the stratification approach described in Ansótegui et al. (2012), what results in solving 100 additional instances. Second, we introduce a new criteria to decide when soft clauses can be hardened (Ansótegui et al. 2012; Morgado et al. 2012), that provides 68 additional solved instances. Finally, our most effective contribution is to introduce a new strategy that focuses search on solving subproblems of the original MaxSAT instance. In order to define these subproblems we use the information provided by the unsatisfiable cores we obtain during the solving process. The improved WPM2 algorithm is parametric on the approach we use to solve these subproblems. This allows to combine the strength of exploiting the information extracted from unsatisfiable cores and other optimization approaches. By solving these smaller optimization problems we get the most significant boost in our improved WPM2 algorithm. In particular, we experiment with an Integer Linear Programming (ILP) approach, corresponding to the strategy shown in Sect. 3, and three MaxSAT approaches: (i) refine the lower bound for these subproblems with the subsetsum function (Cormen et al. 2009; Ansotegui et al. 2010), (ii) refine the upper bound with the strategy applied in minisat+ (Eén and Sörensson 2006), SAT4J (Berre 2006), qmaxsat (Koshimura et al. 2012) or ShinMaxSat (Honjyo and Tanjo 2012), and (iii) a binary search scheme (Heras et al. 2011; Cimatti et al. 2010; Fu and Malik 2006) where the lower bound and upper bound are refined as in the previous approaches. The best performing approach in our experimental analysis is the second one and it allows to solve up to 296 additional instances. As a summary, the overall increase in performance we achieved so far compared to the original WPM2 is about 464 additional solved instances, or 48 % more. These improvements led WPM2 to be the overall best performing approach on the industrial instances of the MSE13.

To further explain the good results of our approach we include and extend the study originally presented in Ansotegui (2013a) on the structure of the unsatisfiable cores obtained during the search process of SAT-based algorithms (see Sect. 6). We explain how the improved WPM2 algorithm takes advantage of this structure.

We have also explored how we can exploit information retrieved from the subproblems that are solved. When the strategy used to optimize the subproblems is able to produce satisfying assignments, i.e., it refines the upper bound (see approaches (ii) and (iii) above), we can use these assignments as a heuristic to guide and boost the search. This improvement allows to solve 50 additional instances. The overall increase in performance compared to the original WPM2 is 514 additional solved instances. Actually, if we take into account the timeout of 7200 s (2 h) used in our experiments, we obtain an overall speed-up of about three orders of magnitude (see Sect. 6). Moreover, we show that high quality satisfying assignments can be obtained in a reasonably short time, giving us naturally an incomplete approach. Our experimental results confirm that the incomplete version of our exact improved WPM2 algorithm would have dominated the track for incomplete solvers at the MSE13. Furthermore, at MSE14, even though it was not the best complete approach, it dominates the others as incomplete.

From the perspective of coming up with an efficient implementation of our approach, it is obvious that SAT-based MaxSAT algorithms have to be implemented on top of an efficient solver based on SAT technology. This solver has to be capable of returning an unsatisfiable core when the input instance is unsatisfiable and a satisfying assignment when the instance is satisfiable. Moreover, SAT-based MaxSAT algorithms require the addition of linear PB constraints as a result of the reformulation process of the original problem into a sequence of SAT instances. These PB constraints are used to bound the cost of the optimal assignment. Currently, in most state-of-the-art SAT-based MaxSAT solvers, PB constraints are translated into SAT. However, there is no known SAT encoding which can guarantee the original propagation power of the constraint, i.e, what we call arc-consistency, while keeping the translation low in size. The best approach so far, has a cubic complexity (Bailleux et al. 2009). This can be a bottleneck for WPM2 (Ansotegui et al. 2010) and also for other algorithms such as, BINCD (Heras et al. 2011) or SAT4J (Berre 2006).

In order to treat PB constraints with specialized inference mechanisms and a moderate cost in size, while preserving the strength of SAT techniques for the rest of the problem, we use the SMT technology (Sebastiani 2007) (see Sect. 5). Related work in this sense can be found in Nieuwenhuis and Oliveras (2006). Also, in Ansótegui et al. (2011) a Weighted Constraint Satisfaction Problems (WCSP) solver implementing the original WPM1 (Ansotegui et al. 2009) algorithm is presented.

Finally, we have also seen the development of successful methods for solving combinatorial problems by applying techniques from Operations Research. Although the literature shows us that some NP-hard problems are more suitable for logic-based approaches while others are more efficiently solved with integer programming techniques, our current study would not be exhaustively conducted without showing the performance of integer programming techniques on MaxSAT problems. Actually, we can easily reformulate the WPMS problem into an ILP problem (see Sect. 3) and apply an ILP approach. We show that the ILP approach is not competitive on the industrial instances where a logic-based approach like the one proposed here is more efficient.

This paper proceeds as follows. Section 2 formally defines the main concepts that are used in the paper. Section 3 presents the translation of WPMS into ILP. Section 4 describes the WPM2 algorithm and the new improvements. Section 5 describes the SMT problem and discusses some implementation details of the SMT-based MaxSAT algorithms. Section 6 presents the experimental evaluation. Finally, Sect. 7 shows the conclusions and the future work.

2 Preliminaries

Definition 1

A literal l is either a Boolean variable x or its negation $\overline{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 5 and 6). 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:

$$\begin{aligned} \varphi =\langle (c_1,w_1),\dots ,(c_s,w_s), (c_{s+1},\infty ),\dots ,(c_{s+h},\infty )\rangle \end{aligned}$$

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(\varphi )$. The top weight of the formula is noted as $W(\varphi )$, and defined as $W(\varphi ) = \sum w(\varphi )+1$. The set of indexes of soft clauses is noted as $S(\varphi )$ and the set of indexes of hard clauses is noted as $H(\varphi )$. When it is clear to which formula $\varphi$ these soft (hard) clauses belong, we also refer to these sets of indexes as S (H). Finally, the set of variables occurring in the formula is noted as $\text{ var }(\varphi )$.

Example 1

Given the WPMS formula $\varphi = \langle (x_1,5), (x_2,3), (x_3,3), (\overline{x}_1 \vee \overline{x}_2,\infty ), (\overline{x}_1 \vee \overline{x}_3,\infty ), (\overline{x}_2 \vee \overline{x}_3,\infty ) \rangle$, we have that $w(\varphi ) = \langle 5,3,3\rangle$, $W(\varphi ) = 12$, $S(\varphi ) = \{ 1,2,3\}$, $H(\varphi ) = \{4,5,6\}$ and $\text{ var }(\varphi ) = \{x_1,x_2,x_3\}$.

Definition 4

Given a WPMS formula $\varphi$ and a set of indexes A, $\varphi _A$ is the WPMS formula that contains the clauses $(c_i,w_i)$ such that $i \in A$. By $\varphi _S$ we refer the set of soft clauses and by $\varphi _H$ to the set of hard clauses.

Example 2

Given the WPMS formula $\varphi$ of Example 1, we have that $\varphi _{\{1,3.5\}} = \langle (x_1,5), (x_3,3), (\overline{x}_1 \vee \overline{x}_3,\infty ) \rangle$, $\varphi _S = \langle (x_1,5), (x_2,3), (x_3,3) \rangle$ and $\varphi _H = \langle (\overline{x}_1 \vee \overline{x}_2,\infty ), (\overline{x}_1 \vee \overline{x}_3,\infty ), (\overline{x}_2 \vee \overline{x}_3,\infty ) \rangle$.

Definition 5

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

$$\begin{aligned} \begin{array}{l} \mathcal {I}(\overline{x}) = 1 - \mathcal {I}(x) \\ \mathcal {I}(l_1 \vee \ldots \vee l_m) = \max \{\mathcal {I}(l_1), \ldots , \mathcal {I}(l_m)\}\\ \mathcal {I}(\{c_1, \ldots , c_{n}\}) = \min \{\mathcal {I}(c_1), \ldots , \mathcal {I}(c_{n})\}\\ \mathcal {I}((c,w)) = w\,(1-\mathcal {I}(c))\\ \mathcal {I}(\langle (c_1,w_1), \ldots , (c_{s+h},w_{s+h})\rangle ) = \sum _{i=1}^{s+h} \mathcal {I}((c_i,w_i)) \end{array} \end{aligned}$$

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

Given a WPMS formula $\varphi$ and a set of indexes A, we will refer to $\mathcal {I}_A$ as an assignment for $\varphi _A$.

Definition 6

We say that an assignment $\mathcal {I}$ satisfies a clause or a SAT formula if the value returned by $\mathcal {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 $\mathcal {I}$ is equal to 0, we say that $\mathcal {I}$ falsifies the clause or the SAT formula.

Definition 7

The SAT problem for a SAT formula $\varphi$ is the problem of finding a solution for $\varphi$. If a solution exists the formula is satisfiable, otherwise it is unsatisfiable.

Definition 8

Given an unsatisfiable SAT formula $\varphi$, an unsatisfiable core $\varphi _C$ is a subset of clauses $\varphi _C\subseteq \varphi$ that is also unsatisfiable. A minimal unsatisfiable core is an unsatisfiable core such that any proper subset of it is satisfiable.

Example 3

Given the SAT formula: $\varphi = \{ (x_1), (x_2), (x_3), (\overline{x}_1 \vee \overline{x}_2), (\overline{x}_1 \vee \overline{x}_3), (\overline{x}_2 \vee \overline{x}_3) \}$ we have that $\{ (x_1), (x_2), (x_3), (\overline{x}_1 \vee \overline{x}_2) \} \subseteq \varphi$ is an unsatisfiable core and $\{ (x_1), (x_2), (\overline{x}_1 \vee \overline{x}_2) \} \subseteq \varphi$ is a minimal unsatisfiable core.

Definition 9

A SAT algorithm for the SAT problem, takes as input a SAT formula $\varphi$ and returns an assignment $\mathcal {I}$ such that $\mathcal {I}(\varphi ) = 1$ if the formula is satisfiable. Otherwise, it returns an unsatisfiable core $\varphi _C$.

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

Definition 10

The optimal cost (or optimum) of a WPMS formula $\varphi$ is cost$(\varphi )=\min \{\mathcal {I}(\varphi )\mid \mathcal {I}:\text{ var }(\varphi )\rightarrow \{0,1\}\}$ and an optimal assignment is an assignment $\mathcal {I}$ such that $\mathcal {I}(\varphi ) =$ cost$(\varphi )$. We will refer to this assignment as a solution for $\varphi$ if $\mathcal {I}(\varphi ) \ne \infty$. Any cost above (below) $cost(\varphi )$ is called an upper (lower) bound for $\varphi$.

Example 4

Given the WPMS formula $\varphi$ of Example 1, we have that cost$(\varphi )=\min \{6,8,11,\infty \} = 6$ and the optimal assignment $\mathcal {I}$ maps $\langle x_1,x_2,x_3 \rangle$ to $\langle 1,0,0 \rangle$.

Definition 11

The Weighted Partial MaxSAT problem for a WPMS formula $\varphi$ is the problem of finding a solution for $\varphi$. If a solution does not exist the formula is unsatisfiable.

Definition 12

A WPMS algorithm for the WPMS problem, takes as input a WPMS formula $\varphi$ and returns an assignment $\mathcal {I}$, such that, $\mathcal {I}(\varphi ) \ge cost(\varphi )$.

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

Definition 13

An integer linear Pseudo-Boolean (PB) constraint is an inequality of the form $w_1 x_1 + \dots + w_n x_n\ op\ k$, where $op\in \{ {\le }, {\ge }, {=}, {>},<\}$, k and $w_i$ are integer coefficients, and $x_i$ are Boolean variables. A cardinality constraint is a PB constraint where the coefficients $w_i$ are equal to 1. A PB At-Most (At-Least) constraint is a PB constraint where op is $\le$ ($\ge$).

Example 5

$5 x_1 + 3 x_2 + 3 x_3\ \le 6$ is a PB At-Most constraint and $5 x_1 + 3 x_2 + 3 x_3\ \ge 6$ is PB At-Least constraint.

3 Translation of weighted partial MaxSAT into ILP

In order to solve a WPMS problem, a first reasonable approach consists in reformulating the WPMS problem as an ILP problem and applying an ILP solver. Several encodings can be found in the literature (Li and Manyà 2009; Manquinho et al. 2009; Ansótegui and Gabàs 2013; Davies and Bacchus 2013).

Here, we describe the precise encoding we used in Ansótegui and Gabàs (2013). Given a WPMS formula, $\langle (c_1,w_1), \dots , (c_s,w_s), (c_{s+1}, \infty ), \dots ,$ $(c_{s+h}, \infty )\rangle$, we can translate it into an ILP instance, as follows:

$$\begin{aligned}&\text{ Minimize: } {\mathop {\sum }\nolimits _{1}^{s}} w_i\cdot b_i \\&\text{ Subject } \text{ to: }\\&ILP(\varphi '_H \cup \varphi '_S) \\&0 \le v_i \le 1, v_i \in var(\varphi '_H \cup \varphi '_S) \end{aligned}$$

The Minimize section of the ILP formulation defines the objective function of the problem. This corresponds to the aggregated cost of the falsified soft clauses in the WPMS formula we want to minimize. In order to identify which soft clauses are falsified by a given assignment to the original $x_i$ variables of the problem, we introduce an indicator variable $b_i$ for each soft clause $(c_i,w_i)$. These $b_i$ are also known as reification, relaxation or blocking variables.

The Subject to section includes the constraints that have to be satisfied under any assignment. This corresponds to the original set of hard clauses of the WPMS formula represented by $\varphi '_H = \cup _{j=s+1}^{s+h} c_j$, and the set of clauses connecting the soft clauses of the WPMS formula with their respective indicator variable represented by $\varphi '_S = \cup _{i=1}^{s} \mathop {C\!N\!F}\nolimits (\overline{c}_i \leftrightarrow b_i)$. Notice that by enforcing consistency, we ensure that $b_i$ is true iff the soft clause $c_i$ is falsified. Function $CNF(\varphi )$ transforms $\varphi$ into Conjunctive Normal Form while function $ILP(\varphi )$ maps every clause $c_i \in \varphi$ into a linear inequality with operator $>$. The left-hand side of that linear inequality corresponds to the sum of the literals in $c_i$ once mapped into integer terms, such that, literal $x(\overline{x})$ is mapped to integer term $x(1-x)$. The right-hand side corresponds to constant 0. After moving the constants to the right, the right-hand side corresponds to constant $-k$, where k is the number of negative literals in clause $c_i$. Finally, we add the bounding constraints that ensure that every integer variable in the ILP formulation has domain $\{0,1\}$. It can be easily seen that, since we are minimizing, the implication $b_i \rightarrow \overline{c}_i$ from $\overline{c}_i \leftrightarrow b_i$ is unnecessary. Notice that, by the same nature of the minimization problem, variables $b_i$ will be 0 (false) whenever it is possible and we do not need the part of the double implication that ensures that $c_i \rightarrow \overline{b}_i$, i.e., $b_i \rightarrow \overline{c}_i$.

Example 6

Given the WPMS formula $\varphi = \langle (x_1 \vee x_2,2),(x_1 \vee \overline{x}_2,3),(\overline{x}_1 \vee x_2,\infty ),(\overline{x}_1 \vee \overline{x}_2,\infty )\rangle$, the corresponding ILP formulation is:

4 Original WPM2 algorithm and improvements

In this section, we present the complete SAT-based MaxSAT algorithm WPM2 (Ansotegui et al. 2010) for the WPMS problem and how it has been improved.

At a high description level, given an input WPMS formula $\varphi$, the original WPM2 algorithm (Ansotegui et al. 2010), described in Algorithm 1, iteratively calls a SAT solver querying whether there is an assignment to $\varphi$ with a cost less than or equal to a certain k. The initial value of k is 0 and the last value is exactly the optimal cost of $\varphi$, i.e., $cost(\varphi )$. Notice that all SAT queries with a $k < cost(\varphi )$ must have a negative answer while all the queries with $k \ge cost(\varphi )$ must have a positive answer. Therefore, our optimization problem can be reformulated as identifying where the phase transition from negative answers to positive answers occurs.

More formally, the query sent to the SAT solver is a SAT formula $\varphi ^k$ that is satisfiable iff there is an assignment, say $\mathcal {I}$, such that $\mathcal {I}(\varphi ) \le k$. In order to construct such a formula, we need to detect which soft clauses are falsified under a certain assignment $\mathcal {I}$, sum up their cost and compare with k.

To detect if a clause is falsified, we extend every soft clause $(c_i, w_i)$ with a unique auxiliary Boolean indicator variable $b_i$ obtaining $(c_i \vee b_i, w_i)$. Notice that, if $c_i$ is false, then in order to maintain consistency $b_i$ must be true. Therefore, these $b_i$ variables work as indicator variables that become true if a clause $c_i$ is falsified.

To add the weights of the falsified soft clauses and compare the cost with k we use PB constraints that are translated into a SAT formula.

Example 7

Before we go into detail on algorithm WPM2, let us describe how a naive SAT-based MaxSAT algorithm would work. Let us consider a simple WPMS formula representing the Weak Pigeon-Hole Problem (Razborov 2001; Raz 2002) of 5 pigeons and 1 hole. Variable $x_i$ is true if the ith pigeon is in the hole.

$$\begin{aligned} \varphi = \langle (x_1,5), (x_2,5), (x_3,3), (x_4,3), (x_5,1)\ \rangle \ \cup \langle \mathop {C\!N\!F}\nolimits (\sum x_i \le 1, \infty )\rangle \end{aligned}$$

The weight of the soft clauses indicates the cost of not having the ith pigeon in the hole and the hard clauses indicate that at most one pigeon can be in the hole. A naive SAT-based MaxSAT solver would search for the optimal cost, solving a sequence of $\varphi ^k$ SAT instances which are satisfiable iff there is an assignment to $\varphi$, i.e., to the $x_i$ variables, with a cost less than or equal to k. In order to build such $\varphi ^k$ SAT instances, all the soft clauses are extended and the PB At-Most constraint, $5\cdot b_1+5\cdot b_2+3\cdot b_3+3\cdot b_4+1\cdot b_5 \le k$, is used to bound the aggregated cost of the falsified clauses.

$$\begin{aligned} \begin{array}{rl} \varphi ^k = \{ &{} (x_1\vee b_1), (x_2\vee b_2), (x_3\vee b_3), (x_4\vee b_4), (x_5\vee b_5)\ \}\ \cup \mathop {C\!N\!F}\nolimits (\sum x_i \le 1)\ \cup \\ &{}\mathop {C\!N\!F}\nolimits (5\cdot b_1+5\cdot b_2+3\cdot b_3+3\cdot b_4+1\cdot b_5 \le k)\ \end{array} \end{aligned}$$

Since $cost(\varphi )=12$, we know that the SAT instances between $\varphi ^0$ to $\varphi ^{11}$ are unsatisfiable, while the SAT instances between $\varphi ^{12}$ to $\varphi ^{18}$ (the top weight $W(\varphi ) = 18$) are satisfiable. A naive binary search between 0 and 18 would check the satisfiability of this sequence: $\varphi ^{9}$, $\varphi ^{13}$, $\varphi ^{11}$ and $\varphi ^{12}$. Since $\varphi ^{11}$ and $\varphi ^{12}$ are unsatisfiable and satisfiable, respectively, we have found the phase transition point and we can conclude that the optimal cost is 12.

The first characteristic of the original WPM2 algorithm is that it works with two sets of PB constraints: AM and AL. The set AM of PB (At-Most) constraints are used to bound the aggregated cost of the falsified soft clauses. In particular, AM is a set of PB constraints that bound the cost of non-overlapping subsets of soft clauses. More precisely, an $am \in AM$ is a PB constraint of the form $\sum _{i\in A}w_i\,b_i\le k$ where A is a subset of the indexes of the soft clauses, $b_i$ and $w_i$ are the corresponding indicator variables and weights of the ith soft clause and k the concrete bound for that subset of soft clauses. When describing algorithms, we will use the object oriented programming notation am.A and am.k to refer to the set A and integer k related to an At-Most constraint $am \in AM$. The idea of having multiple and smaller PB At-Most constraints instead of a single one was introduced in Ansótegui et al. (2009).

The set AL of PB (At-Least) constraints are used to impose that the aggregated cost of the falsified clauses in a given subset of soft clauses must be at least some natural number. These are redundant constraints and are not necessary for the soundness of the algorithm but help to improve the performance of the SAT solver. More precisely, an $al \in AL$ is a PB constraint of the form $\sum _{i\in A}w_i\,b_i\ge k$.

For the sake of space and readability, we will use the notation $\langle A, w(\varphi _A), \le , k \rangle$ and At-Most constraint instead of $\sum _{i\in A}w_i\,b_i \le k$ and PB At-Most constraint in the algorithms. Mutatis mutandis for the PB At-Least constraints.

In the following, we go into detail on the original WPM2 algorithm (Algorithm 1). First of all, we check whether the set of hard clauses ($\varphi _H$) is satisfiable (Algorithm 1 line 1). If it is unsatisfiable, we can already stop since there is no solution to $\varphi$. Otherwise, the main loop of the algorithm starts (Algorithm 1 line 3). Notice that we exit this loop iff the sat function returns satisfiable. In that case, we have found a solution.

The sat function (Algorithm 1 line 4) builds the SAT formula at the current iteration and sends it to the SAT solver. As we can see, a SAT formula $\varphi ^k$ is built by extending soft clauses with indicator variables and aggregating to $\varphi ^k$ the conversion to $\mathop {C\!N\!F}\nolimits$ of the PB constraints into the sets AL and AM (sat line 2). Actually, only a subset of the soft clauses is relaxed, i.e., extended with indicator variables $b_i$. In particular, those that have appeared previously in some unsatisfiable core. This is done because of efficiency issues.

The SAT solver outputs a triplet $\langle st, \varphi ^k_C, \mathcal {I} \rangle$ (sat line 3). If the SAT solver returns satisfiable ( $st=\text{ sat }$), $\varphi ^k_C$ is empty and $\mathcal {I}$ is the satisfying assignment (solution) found by the SAT solver. If the SAT solver returns unsatisfiable ($st=\text{ unsat }$), $\varphi ^k_C$ is the unsatisfiable core found by the solver and $\mathcal {I}$ is empty. Finally, the sat function returns the status, st, the indexes of the soft clauses in the unsatisfiable core C (sat line 4) if $st=\text{ unsat }$, and the satisfying assignment $\mathcal {I}$ if $st=\text{ sat }$.

When the sat function returns $st=\text{ sat }$ (Algorithm 1 line 5) we return the optimal cost and the optimal assignment (Algorithm 1 line 6) and the algorithm ends. When the sat function returns $st=\text{ unsat }$ (Algorithm 1 line 7) we analyze the unsatisfiable core returned by the solver and we compute, within the optimize function (Algorithm 1 line 8), which is the set of indexes of soft clauses and bound $\langle A,k \rangle$ to construct the new At-Most constraint $\langle A, w(\varphi _A),\le ,k \rangle$ and update the AL and AM sets (Algorithm 1 lines 9 and 10). Technically speaking, the AL constraints give lower bounds on $cost(\varphi )$, while the AM constraints enforce that all solutions of the set of constraints $AL\cup AM$ are the solutions of AL of minimal cost. This ensures that any solution returned by $sat(\varphi ,AL,AM)$, if there is any, has to be an optimal assignment of $\varphi$.

Within the optimize function, basically, we check which non-relaxed soft clauses and At-Most constraints on relaxed clauses are involved in the unsatisfiable core. The union of the indexes of all these clauses, set A (optimize line 1), gives us the indexes of the new At-Most constraint. Notice that the non-relaxed soft clauses involved in A will be relaxed in the next step within the sat function (sat line 2). In order to finish the building process of the new At-Most constraint, we have to compute its independent term k (optimize lines 2–6). Intuitively, the next k has to be the next lower bound candidate for the subproblem defined by the soft clauses related to A, i.e., $\varphi _A$ . Notice that the previous candidate was the sum of the k’s ($\sum ^{am \in AM}_{am.A \subseteq A} am.k$) of the At-Most constraints involved into the unsatisfiable core, which were proven by the SAT solver to be too restrictive. In order to obtain the next candidate, we need to find the minimum integer k that satisfies the next conditions: (i) k is a linear combination of the weights involved in $\varphi _A$, (ii) k is greater than or equal to $(\sum ^{am \in AM}_{am.A \subseteq A} am.k)+1$ and (iii) the new At-Most constraint $\langle A,w(\varphi _A),\le ,k \rangle$ is consistent with the set of constraints in AL.

As we can see in the optimize function, (i) and (ii) are enforced by the subsetsum function (optimize lines 2 and 6) while (iii) is checked by the sat function (optimize line 4). The main idea is that the subset sum problem (Cormen et al. 2009) is progressively solved until we get a solution that also satisfies the AL constraints.

Actually, the optimize function represents the following optimization problem:

$$\begin{aligned} \begin{array}{ll} \text{ Minimize } \sum _{i \in A} w_i\cdot b_i &{} \hbox {(i)}\\ \text{ Subject } \text{ to: }\\ \sum _{i \in A} w_i\cdot b_i \ge k' &{} \hbox {(ii)}\\ AL &{} \hbox {(iii)}\\ 0 \le b_i \le 1, i \in A \end{array} \end{aligned}$$

where $k'= (\sum ^{am \in AM}_{am.A \subseteq A} am.k)+1$. Notice that, by removing the AL constraints, we get the subset sum problem.

Finally, once we obtain $\langle A,k \rangle$ (Algorithm 1 line 8) to construct the new At-Most constraint $\langle A,w(\varphi _A),\le ,k \rangle$, we update the AL and AM sets. Basically, we replace in the AM set the At-Most constraints whose respective soft clauses are already considered in the new At-Most constraint (Algorithm 1 line 10). Notice that the new At-Most constraint enforces that the cost of any assignment to the subproblem $\varphi _A$ has at most cost k. Optionally, we extend the AL set with an additional redundant constraint stating that the cost of any assignment to the subproblem $\varphi _A$ has to be at least k (Algorithm 1 line 9).

For further information and detailed proofs on the soundness and completeness of the original WPM2 algorithm see Ansotegui et al. (2010).

Example 8

The original WPM2 algorithm performs the following iterations on the pigeon-hole formula presented in Example 7.

$$\begin{aligned} \varphi = \langle (x_1,5), (x_2,5), (x_3,3), (x_4,3), (x_5,1)\rangle \ \cup \ \langle \mathop {C\!N\!F}\nolimits (\sum x_i \le 1, \infty ) \rangle \end{aligned}$$

In the first iteration, the SAT formula $\varphi ^0$ is sent to the SAT solver within the sat function. The SAT solver certifies that it is unsatisfiable, and returns an unsatisfiable core (noted with dots $\bullet$) that involves the soft clauses 1 and 3, and the set of hard clauses. Semantically speaking, this core tells us that pigeons 1 and 3 can not be at the same time in the hole. The optimize function computes the new At-Most constraint ($5 b_1+3 b_3 \le 3$) that corresponds to the subproblem $\varphi _{\{1,3\}}$. Notice that the corresponding At-Most constraint for a subproblem restricts to k the aggregated cost of its falsified soft clauses. Obviously, the first optimal candidate k for $\varphi _{\{1,3\}}$ is 3 since we will try first to leave out the pigeon with the minimum weight. Then, the soft clauses are relaxed with an additional variable and the corresponding constraints are added to AL and AM. These changes (noted with triangles $\blacktriangleleft$) transform $\varphi ^0$ into $\varphi ^3$. The second iteration is similar to the first one, but with the soft clauses 2 and 4. The new At-Most constraint computed by the optimize function is ($5 b_2+3 b_4 \le 3$).

In the third iteration, we get an unsatisfiable core for $\varphi ^6$ with the soft clauses 1 and 2, the two At-Most constraints from previous subproblems and the set of hard clauses. The optimize function returns the subset of indexes that defines the new subproblem $\varphi _{\{1,2,3,4\}}$, with the soft clauses from the core and from the previous subproblems that intersect with it. It also returns the next optimal candidate for $\varphi _{\{1,2,3,4\}}$, $k=8$, which satisfies the three conditions: (i) it is a linear combination of the weights of $\varphi _{\{1,2,3,4\}}$, (ii) it is greater than or equal to the addition of the subsumed previous subproblem optimal candidates plus one $(3+3+1)$ and (iii) its corresponding At-Most constraint ($5 b_1+5 b_2+3 b_3+3 b_4 \le 8$) is consistent with the set of constraints in AL. We have to replace the two At-Most constraints involved in the core with the new one, that is less restrictive. Notice that the previous constraints only allowed the two pigeons with weight 3 to be out of the hole. On the other hand, the current constraint allows both one pigeon with weight 3 and one with weight 5 to be out of the hole. However, this is not enough to solve the subproblem since at-least three pigeons should be out of the hole.

In the fourth and the fifth iteration the sat function provides a core involving the soft clauses in $\varphi _{\{1,2,3,4\}}$. The optimize function provides new bounds 10 and 11, respectively. This last bound does allow three pigeons to be out of the hole. However, this is not yet enough to solve the whole problem.

In the sixth iteration, we get a core involving all the soft clauses, the At-Most constraint and the set of hard clauses. The At-Most constraint corresponding to subproblem $\varphi _{\{1,2,3,4\}}$, allows three pigeons out of the hole, but one is still in the hole. Since pigeon 5 is also in the hole, there is a conflict. We get the new constraint involving all the soft clauses and the new bound 12. In the seventh iteration, we get that $\varphi ^{12}$ is satisfiable and the original WPM2 algorithm ends. Notice that indeed 12 is the minimum cost that allows four pigeons out of the hole.

In what follows, we present how the original WPM2 algorithm can be improved by the application of the stratified approach, the hardening of soft clauses, the optimization of subproblems, and the exploitation of the assignments whose costs are upper bounds on the subproblems. The first three improvements were already applied in Ansótegui et al. (2013a).

Finally, we show that a collateral result of optimizing these subproblems by refining the upper bound is to turn the original WPM2 complete algorithm into an incomplete algorithm given a fixed amount of time or memory resources. We present the improvements in Algorithm 2 by extending Algorithm 1. The improvements are underlined.

4.1 Stratified approach

The first improvement corresponds to the stratified approach introduced in Ansótegui et al. (2012) for algorithm WPM1. The stratified approach (Algorithm 2 lines 2, 4, 7 and 9) consists in sending to the SAT solver only a subset of the soft clauses, i.e., $\varphi _M$ (Algorithm 2 line 4). For the sake of clarity, we will refer to this subset as a module. More precisely, a module M is the set of indexes of the clauses to be sent to the SAT solver. Therefore, when the sat function returns $st=\text{ sat }$, it means that we have solved the subproblem $\varphi _M$. If $\varphi _M$ is equal to $\varphi$, then we have solved the whole problem and we can finish (Algorithm 2 line 7). A crucial point is how we extend our current module. This action is performed by the newmodule function (Algorithm 2 line 9).

In our current approach, we follow the stratified strategy applied in Ansótegui et al. (2012). There, a module M is formed by the indexes of the clauses whose weight is greater than or equal to a certain weight $w_{max}$. Initially, $w_{max}$ is $\infty$. In order to extend the current module, we apply the diversity heuristic (Algorithm 2 line 9) which supplies us with an efficient method to calculate how we have to reduce the value of $w_{max}$. In particular, when there is a low diversity of weights in $w(\varphi \setminus \varphi _M)$, $w_{max}$ is decreased to $max\ w(\varphi \setminus \varphi _M)$, while when there is a high diversity of weights, $w_{max}$ decreases faster to keep the diversity of $w(\varphi \setminus \varphi _M)$ low. A similar approach with an alternative heuristic for grouping clauses can be found in Martins et al. (2012). In Morgado et al. (2013b), it is proposed to only consider in the working formula or the current module, those clauses that have been falsified by a satisfying assignment corresponding to an upper bound.

4.2 Clause hardening

The hardening of soft clauses in MaxSAT SAT-based solvers has been previously studied in Borchers and Furman (1998), Li et al. (2007), Larrosa et al. (2008), Heras et al. (2008), Marques-Silva et al. (2011), Ansótegui et al. (2012), and Morgado et al. (2012). Inspired by these works we study a hardening scheme for WPM2. While clause hardening was reported to have no positive effect in WPM1 (Ansótegui et al. 2012), we will see that it boosts efficiency in WPM2.

The clause hardening (Algorithm 2 lines 2,  8 and 11) consists in considering hard those soft clauses whose satisfiability we know does not need to be reconsidered. We need some lemma ensuring that falsifying those soft clauses would lead us to non-optimal assignments. In the case of WPM1, all soft clauses satisfying $w_i > W$, where $W = \sum \{w_i\mid (c_i,w_i)\in \varphi \wedge w_i < w_{max}\}$ is the sum of weights of clauses not sent to the SAT solver, can be hardened.

The correctness of this transformation is ensured by the following lemma:

Lemma 1

(Lemma 24 in Ansótegui et al. (2013b))

Let $\varphi _1=\{(c_1,w_1),\dots ,(c_s,w_s), (c_{s+1},\infty ),\dots ,(c_{s+h},\infty )\}$ be a MaxSAT formula with cost zero, let $\varphi _2=\{(c'_1,w'_1),\dots ,(c'_r,w'_r)\}$ be a MaxSAT formula without hard clauses and $W= \sum _{j=1}^{r}w'_j$. Let

$$\begin{aligned} \text{ harden }(w)=\left\{ \begin{array}{ll}w &{} \text{ if } w\le W\\ \infty &{} \text{ if } w> W\end{array}\right. \end{aligned}$$

and $\varphi _1'=\{(c_i,\text{ harden }(w_i))\mid (c_i,w_i)\in \varphi _1\}$. Then, cost$(\varphi _1\cup \varphi _2)=$cost$(\varphi '_1\cup \varphi _2)$, and any optimal assignment for $\varphi '_1\cup \varphi _2$ is an optimal assignment of $\varphi _1\cup \varphi _2$.

However, this lemma is not useful in the case of WPM2 because we do not proceed by transforming the formula, like in WPM1. Therefore, we generalize this lemma. For this, we need to introduce the notion of optimal candidate of a formula.

Definition 14

Given a WPMS formula $\varphi =\langle (c_1,w_1),\dots ,(c_s,w_s),$ $(c_{s+1},\infty ),\dots ,(c_{s+h},\infty )\rangle$, we say that k is an optimal candidate of $\varphi$ if there exists a subset $A\subseteq \{1,\dots ,s\}$ such that $\sum _{i\in A} w_i = k$.

Notice that, for any assignment $\mathcal {I}$ of the variables of $\varphi$, we have that $\mathcal {I}(\varphi )$ is an optimal candidate of $\varphi$. However, if k is an optimal candidate, there does not exist necessarily an assignment $\mathcal {I}$ satisfying $\mathcal {I}(\varphi )=k$. Notice also that, given $\varphi$ and k, finding the next optimal candidate, i.e., finding the smallest $k'>k$ such that $k'$ is an optimal candidate of $\varphi$ is equivalent to the subset sum problem.

Lemma 2

Let $\varphi _1\cup \varphi _2$ be a WPMS formula and $k_1$ and $k_2$ values such that: cost$(\varphi _1\cup \varphi _2)=k_1+k_2$ and any assignment $\mathcal {I}$ satisfies $\mathcal {I}(\varphi _1)\ge k_1$ and $\mathcal {I} (\varphi _2)\ge k_2$. Let $k'$ be the smallest possible optimal candidate of $\varphi _2$ such that $k'>k_2$. Let $\varphi _3$ be a set of soft clauses with $W=\sum \{w_i\mid (c_i,w_i)\in \varphi _3\}$.

Then, if $W < k'-k_2$, then any optimal assignment $\mathcal {I}'$ of $\varphi _1\cup \varphi _2\cup \varphi _3$ assigns $\mathcal {I}'(\varphi _2) = k_2$

Proof

Let $\mathcal {I}'$ be any optimal assignment of $\varphi _1\cup \varphi _2\cup \varphi _3$. On the one hand, as for any other assignment, we have $\mathcal {I}'(\varphi _2)\ge k_2$.

On the other hand, any of the optimal assignments $\mathcal {I}$ of $\varphi _1\cup \varphi _2$ can be extended (does not matter how) to the variables of $\text{ var }(\varphi _3)\setminus \text{ var }(\varphi _1\cup \varphi _2)$, such that

$$\begin{aligned} \mathcal {I}(\varphi _1\cup \varphi _2\cup \varphi _3) =\mathcal {I}(\varphi _1) +\mathcal {I}(\varphi _2)+\mathcal {I}(\varphi _3) \le k_1+k_2 + W < k_1 + k' \end{aligned}$$

(1)

Now, assume that $\mathcal {I}'(\varphi _2)\ne k_2$, then $\mathcal {I}'(\varphi _2)\ge k'$. As any other assignment, $\mathcal {I}'(\varphi _1)\ge k_1$. Hence, $\mathcal {I}'(\varphi _1\cup \varphi _2\cup \varphi _3)\ge k_1 + k'>\mathcal {I}(\varphi _1\cup \varphi _2\cup \varphi _3)$, but this contradicts the optimality of $\mathcal {I}'$. Therefore, $\mathcal {I}'(\varphi _2)= k_2$. $\square$

Example 9

It may seem that the condition of Lemma 2 is hard to satisfy unless $\varphi _1$ and $\varphi _2$ are over disjoint sets of variables. This is not the case, and here we present a simple example where $\varphi _1$ and $\varphi _2$ share variables and Lemma 2 holds:

$$\begin{aligned} \varphi _H = \mathop {C\!N\!F}\nolimits ( ((x_1+x_2 \le 1), \infty ), ((x_3+x_4 \le 1), \infty ),((x_1+x_2+x_3+x_4 \le 2), \infty ) ) \end{aligned}$$

$$\begin{aligned} \varphi _1 = \langle (x_1,1),(x_2,1) \rangle \cup \varphi _H \end{aligned}$$

$$\begin{aligned} \varphi _2 = \langle (x_3,1),(x_4,1) \rangle \cup \varphi _H \end{aligned}$$

$$\begin{aligned} \varphi _1 \cup \varphi _2 = \langle (x_1,1),(x_2,1),(x_3,1),(x_4,1) \rangle \cup \varphi _H \end{aligned}$$

Notice that the condition of Lemma 2 is satisfied for $\varphi _1$ and $\varphi _2$, since $k_1 = cost(\varphi _1) = 1$, $k_2 = cost(\varphi _2) = 1$ and $k_1 + k_2 = cost(\varphi _1 \cup \varphi _2) = 2$.

In order to apply this lemma we have to consider formulas $\varphi _1\cup \varphi _2$ ensuring cost$(\varphi _1\cup \varphi _2)=k_1+k_2$ and $\mathcal {I}(\varphi _1)\ge k_1$ and $\mathcal {I}(\varphi _2)\ge k_2$, for any assignment $\mathcal {I}$. This can be easily ensured, in the case of WPM2, if both $\varphi _1$ and $\varphi _2$ are subproblems. Then, we only have to check if the next optimal candidate $k'$ of $\varphi _2$ exceeds the previous one $k_2$ more than the sum W of the weights of the clauses not sent to the SAT solver. In such a case, we can consider all soft clauses of $\varphi _2$ and their corresponding AM constraint with $k_2$ as hard clauses. In other words, we do not need to recompute the optimal $k_2$ of $\varphi _2$.

The $harden(\varphi ,AM,M)$ function (Algorithm 2 line 8) returns the set of indexes of soft clauses $H'$ that needs to be considered hard based on the previous analysis according to: the current set of At-Most constraints AM, the next optimal candidates of these constraints and the sum of the weights W of soft clauses beyond the current $w_{max}$, i.e., not yet sent to the SAT solver.

Finally, in the optimize function (Algorithm 2 line 11) we introduce $H'$ since as we will see in the next subsection, we need to know which are all the hard clauses to this point of the execution.

4.3 Subproblem optimization

As we have mentioned earlier, one key point in WPM2 is how to compute $\langle A,k \rangle$ within the optimize function (Algorithm 2 line 11) to construct the new At-Most constraint ($\langle A,w(\varphi ),\ge ,k \rangle$). In the original WPM2 algorithm, the idea was to compute the next lower bound candidate, k, for the subproblem $\varphi _A$. We can go further and set k to the optimal cost of the subproblem $\varphi _{A \cup H}$, i.e., $k = cost(\varphi _{A \cup H})$.¹

In order to do this, while taking advantage of the AL constraints generated so far, we only have to extend the definition of the minimization problem corresponding to the original optimize function, by adding $\varphi _{A \cup H}$ to the Subject to section.

To solve $\varphi _{A \cup H}$, we can use any complete approach related to MaxSAT, such as, MaxSAT branch and bound algorithms, MaxSAT SAT-based algorithms, saturation under the MaxSAT resolution rule (Larrosa and Heras 2005; Bonet et al. 2006), or we can use other solving techniques such as PB solvers or ILP techniques, etc. Therefore the improved WPM2 algorithm is parametric on any suitable optimization solving approach. In this work, we experimented with an ILP approach, corresponding to the strategy shown in Sect. 3, and three MaxSAT approaches (new optimize line 5) that we describe in the next lines.

The first and natural approach consists in iteratively refining (increasing) the lower bound ($k = lb$) on $cost(\varphi _{A \cup H})$ by applying the subsetsum function as in the original WPM2 (new optimize lines 5 and 11). The procedure stops when lb satisfies the constraints $AL \cup \varphi _{A \cup H}$ (new optimize line 9). Notice that, since we have included $\varphi _{A \cup H}$ into the set of constraints, we will get an optimal assignment or solution for $\varphi _{A \cup H}$.

The second approach consists in iteratively refining (decreasing) the upper bound following the strategy applied in minisat+ (Eén and Sörensson 2006), SAT4J (Berre 2006), qmaxsat (Koshimura et al. 2012) or ShinMaxSat (Honjyo and Tanjo 2012). The upper bound ub is initially set to the top weight of $\varphi _A$. Then, we iteratively check whether there exists an assignment for $\varphi _{A \cup H}$ with cost $k = ub-1$. Whenever we get a satisfying assignment ($\mathcal {I}_A$) we update ub to $\mathcal {I}_A(\varphi _A)$, i.e., the sum of the weights $w_i$ of those soft clauses falsified under the satisfying assignment (new optimize line 5). Notice that since $\mathcal {I}_A$ is a satisfying assignment, it follows that $\mathcal {I}_A(\varphi _A) = \mathcal {I}_A(\varphi _{A \cup H})$. If we get an unsatisfiable answer, the previous upper bound ($\mathcal {I}_A(\varphi _A)$) is the optimal cost for $\varphi _{A \cup H}$ (new optimize lines 11 and 12 ).

The third approach applies a binary search scheme (Heras et al. 2011; Cimatti et al. 2010; Fu and Malik 2006) on k (new optimize line 5). We additionally refine the lower bound (lb) as in our first approach and the upper bound ($\mathcal {I}_A(\varphi _A)$) as in the second approach. The search ends when lb and $\mathcal {I}_A(\varphi _A)$ are equal (new optimize lines 9 and 11).

A final remark is that, if we combine this technique with the previous hardening technique, then we simply have to take into account the set of indexes of soft clauses $H'$ that became hard. As we can see in the new optimize function (Algorithm 2 line 11), we first compute the set A as in the original function, but excluding the soft clauses that became hard $H'$ (new optimize line 1). Then, we call the sat function but adding $\varphi _{A \cup H \cup H'}$ and the set of At-Most constraints involved in $H'$, i.e., $\{ am \in AM \}_{am.A \subseteq H'}$ (new optimize line 6).

The worst case complexity, in terms of the number of calls to the SAT solver, of the improved WPM2 algorithm is the number of times that the optimize function is called (bounded by the number of soft clauses) multiplied by the number of SAT calls needed in each call to the optimize function. This latter number is logarithmic on the sum of the weights of the clauses of the core if we use a binary search, hence essentially the number of clauses. Therefore, the worst case complexity, when using a binary search to solve the subproblems, is quadratic on the number of soft clauses.

In order to see that the number of calls to the optimize function is bounded by the number of clauses we just need to recall that WPM2 merges the At-Most constraints. Consider a binary tree where the soft clauses are the leaves, and the internal nodes represent the merges (calls to the optimize function). A binary tree of n leaves has n$-$1 internal nodes.

Solving all the subproblems exactly can be very costly since these are NP-hard problems. Notice that some of these subproblems can be integrated soon into another subproblem which we will also solve. A reasonable strategy would be to solve a subproblem when it appears for the second time, meaning that the associated k is not the optimal cost. However, in practice, we found that the more efficient strategy was to solve a subproblem only if it incorporates a previous subproblem.

Example 10

The improved WPM2 algorithm performs different iterations from the ones of the original WPM2 in Example 8 on the pigeon-hole formula presented in Example 7.

$$\begin{aligned} \varphi = \langle (x_1,5), (x_2,5), (x_3,3), (x_4,3), (x_5,1)\rangle \ \cup \ \langle \mathop {C\!N\!F}\nolimits (\sum x_i \le 1, \infty ) \rangle \end{aligned}$$

In contrast to the original, the improved WPM2 algorithm performs fewer calls to the sat function with an unsatisfiable response. Therefore, it performs fewer calls to the optimize function and fewer updates to AL and AM. Besides, the sat function deals with formulas $\varphi _M$ with fewer soft clauses and sets AL and AM with shorter constraints. We find the first difference in the first iteration where, applying the stratified approach, we consider only a subproblem $\varphi _M$ with those clauses whose weight $w_i \ge 5$. The first unsatisfiable core (noted with dots $\bullet$), involves the soft clauses 1 and 2, and the set of hard clauses. The optimize function computes the new At-Most constraint that corresponds to the subproblem $\varphi _{\{1,2\} \cup H}$. The optimal cost k for this subproblem is 5, since this is the weight of both pigeons. Notice that, applying the stratified approach, we get a better first lower bound for the formula. The soft clauses are relaxed and the corresponding constraints are added to AL and AM (noted with triangles $\blacktriangleleft$). In the second iteration, we get that $\varphi _M^5$ is satisfiable. Since $\varphi _M$ is not equal to $\varphi$, we compute a new module M with those clauses whose weight $w_i \ge 3$.

The third iteration is similar to the first one, but with the soft clauses 3 and 4.

It is in the fourth iteration where we can appreciate the impact of subproblem optimization. In Example 8, we needed three iterations to get the bound 11 for the At-Most constraint corresponding to the subproblem $\varphi _{\{1,2,3,4\}}$. Incorporating the hard clauses to the optimize function and solving the subproblem $\varphi _{\{1,2,3,4\}\cup H}$, we get directly the optimal cost 11 in just one iteration. In the fifth iteration, we get that $\varphi _M^5$ is satisfiable. As $\varphi _M$ is not equal to $\varphi$ we have to compute a new module again. Before doing that, we apply the hardening technique. We get that the soft clauses 1, 2, 3 and 4, and their corresponding At-Most constraint can be considered as hard ($H'$). This is because the current k of this At-Most constraint is 11 ($5+3+3$) and its next $k'$ candidate is 13 ($5+5+3$), while the addition of weights of those soft clauses not yet in M, i.e., $\{5\}$, is only 1. So, reconsidering this At-Most constraint would lead to an assignment with a higher cost than falsifying all the soft clauses not yet in M. Semantically speaking, the increase in cost of any non-allowed distribution of pigeons 1, 2, 3 and 4, is always higher than the cost of allowing the pigeon 5 to be out of the hole. After applying the hardening technique, we compute the new module M (clauses whose weight $w_i \ge 1$) that corresponds to the whole problem (i.e., in the next iteration with a satisfiable response from the sat function, we will have found the solution).

In the sixth iteration, the sat function returns a core with all the soft clauses, the At-Most constraint and the set of hard clauses. Applying the hardening technique, the soft clauses with indexes in $H'$ and the corresponding At-Most constraint are considered as hard. Therefore, the new At-Most constraint computed by the optimize function involves only the soft clause 5 and has the new bound $k=1$. In the seventh iteration, we get that $\varphi _M^{12}$ is satisfiable. Since $\varphi _M$ is equal to $\varphi$, 12 is the solution to the problem.

4.4 Exploiting satisfying assignments from subproblems

Whenever we obtain an upper bound or solution for a subproblem, we can obtain an upper bound for the whole problem. Consider $\varphi _{A \cup H}$, where A is a subset of the indexes of the soft clauses in a WPMS formula $\varphi$ and H the set of indexes of the hard clauses, as the subproblem we want to solve. According to the search strategy we use in the optimize function (see Sect. 4.3) we may obtain assignments $\mathcal {I}_{A}$ (Algorithm 2 line 6) that are upper bounds or directly a solution for $\varphi _{A \cup H}$. If we extend this assignment by assigning a random value in $\{0,1\}$ to every variable in $var(\varphi ) \setminus \text{ var }(\varphi _{A \cup H})$, then it is not difficult to see that $\mathcal {I}_{A}(\varphi ) \ge cost(\varphi )$, i.e., $\mathcal {I}_{A}(\varphi )$ is an upper bound for $\varphi$. Therefore, by comparing $\mathcal {I}_{A}(\varphi )$ with the cost of the best assignment found so far $\mathcal {I}_{S}(\varphi )$ (Algorithm 2 line 8), the improved WPM2 algorithm becomes naturally an incomplete approach. It is incomplete in the sense that it reports the assignment with the best cost found within restricted time and memory resources.

Also, due to the stratification approach, once we obtain a satisfying assignment $\mathcal {I}_M$ for a module M (Algorithm 2 line 4), we may have obtained a better upper bound for $\varphi$. Therefore, following the same idea, we update conveniently $\mathcal {I}_{S}$ (Algorithm 2 line 6) as in the optimize function.

Obviously, this incomplete approach makes sense if we are able to obtain quickly good quality upper bounds. We will show that this is the case in the experimental section (see Sect. 6). However, let us visualize the behavior of the improved WPM2 algorithm on a particular instance. In Fig. 1, we show the upper bounds $\mathcal {I}_A(\varphi )$ and lower bounds obtained during the execution of the improved WPM2 on an industrial Partial MaxSAT formula $\varphi$. The upper bound refinement strategy was used for the subproblem optimization phase.

Fig. 1

Upper and lower bounds obtained with the original and the improved WPM2

For the sake of comparison, we also show the lower bounds obtained with the original WPM2 algorithm. The objective is to show that the improved WPM2 algorithm not only is able to provide good upper bounds, it also converges faster to the optimal cost.

In the x-axis, we show the elapsed seconds of the search in a logarithmic scale. The y-axis correspond to the range of the objective function (from 0 to top weight). In the upper half (from optimum to top weight) we show the value of the obtained upper bounds and in the lower half (from optimum to 0) we show the value of the lower bounds.

As we can see, the original WPM2 does not provide any upper bound until the optimum is found. In contrast, the improved WPM2 does provide several upper bounds coming from the subproblem optimization phase.

Both algorithms provide lower bounds. Every lower bound update corresponds to a new k for a subproblem obtained after a call to the optimize function and is followed by a call to the sat function to check the satisfiability of the whole problem. Notice that the subproblem optimization occurs always between lower bound updates. In the improved WPM2 algorithm, during the subproblem optimization phase, the upper bound for the particular subproblem is always improved, i.e., it decreases. However, if we extend this assignment to the whole problem this monotonic behavior is not guaranteed. This is why, in Fig. 1, during the subproblem optimization phase, the upper bounds for the whole problem tend to decrease but can also increase.

With respect to the quality of these upper bounds, notice that, in less than 5 s, an upper bound very close to the optimum (less than 6 % error) is obtained. Also, an upper bound $\mathcal {I}_A(\varphi )$ equal to the optimal cost $cost(\varphi )$ (0 % error) is obtained in 132 s, earlier than the solution itself (226 s). This is interesting because it means that we can obtain very high quality assignments or even a solution before solving exactly the problem, i.e., certifying that there is no any other assignment with a lower cost.

Finally, we can see that, thanks to subproblem optimization, the improved WPM2 only needs 6 calls (lower bounds updates) on the whole problem, while the original WPM2 needs more than 40.

For more detailed information, we analyze the quality of upper bounds for all the instances of our experimentation in Sect. 6 (Figs. 2 and 3).

Fig. 2

Upper bound quality relative to the resolution time (at the top industrial instances, at the bottom crafted instances)

Fig. 3

Number of instances on which a certain upper bound quality is reached (at the top industrial instances, at the bottom crafted instances)

We can further exploit the satisfying assignments obtained during the search. In modern SAT solvers, the polarity of the decision variables is chosen according to the most recent polarity they were assigned in a previous partial assignment. This technique is called phase saving (Pipatsrisawat and Darwiche 2007) and its main goal is to avoid redoing work. Notice that, during backtracking, many variable assignments are undone and the suitable polarity needs to be revealed again during search.

In our SAT-based MaxSAT algorithms, we perform independent queries to a SAT solver. Therefore, some suitable information can be lost. For example, in Sect. 5 we discuss how to preserve learned clauses by using the SAT solvers in incremental mode. Here, the idea is to use the optimal assignment $\mathcal {I}_A$ for a subproblem $\varphi _{A \cup H}$ (Algorithm 2 line 11) to guide the search in the next call to the SAT solver. Basically, the set $\beta$ (Algorithm 2 line 12) is updated to contain the unit clauses that represent whether the ith soft clause was satisfied ($\overline{b}_i$) or falsified ($b_i$) by the $\mathcal {I}_A$ of the most recent subproblem it took part in. We expect assignments $\mathcal {I}_A$ to be more informed as search proceeds and therefore be able to guess the satisfaction status of soft clauses in optimal assignments for $\varphi$. In the sat function the set $\beta$ is appended to the set of clauses sent to the SAT solver (new sat line 2). Although this gives us extra propagation, it may be the case that our guess is wrong, therefore we iteratively call the SAT solver until no unit clause in $\beta$ is involved in the unsatisfiable core (new sat lines 3, 5 and 6). Notice that the unit clauses that do not appear in any core, do remain in the set $\beta$ providing us extra propagation power (Algorithm 2 line 4). Therefore, we use the optimal assignments from subproblems to guess the phase of the variables in an optimal assignment to the whole problem $\varphi$. In addition, we can also use the satisfying assignments $\mathcal {I}_A$, obtained within the subproblem optimization, to guide the search during this phase.

5 Engineering efficient SMT-based MaxSAT solvers

We have implemented both the last version of the WPM1 algorithm (Ansótegui et al. 2012) and the improved WPM2 algorithm on top of the Yices SMT solver (Dutertre and de Moura 2014).

An SMT formula is a generalization of a Boolean formula in which some propositional variables have been replaced by predicates with predefined assignments from background theories such as, e.g., linear integer arithmetic. For example, an SMT formula can contain clauses like $x_1 \vee x_2 \vee (b_1 + 2 \le b_1)$ and $(b_1 \ge 2 \cdot b_2 + 3 \cdot b_3)$, where $x_1$ and $x_2$ are Boolean variables and $b_1$, $b_2$ and $b_3$ are integer variables. Predicates over non-Boolean variables, such as linear integer inequalities, are evaluated according to the rules of a background theory. Leveraging the advances made in SAT solvers in the last decade, SMT solvers have proved to be competitive with classical decision methods in many areas. Most modern SMT solvers integrate a SAT solver with decision procedures (theory solvers) for sets of literals belonging to each theory. This way, we can hopefully get the best of both worlds: in particular, the efficiency of the SAT solver for the Boolean reasoning and the efficiency of special-purpose algorithms for the theory reasoning.

Another reasonable choice would be to use a PB solver, which can be seen as a particular case of an SMT solver specialized on the theory of PB constraints (Manquinho et al. 2009, 2010). However, if we also want to solve problems modeled with richer formalisms like WCSP, the SMT approach seems a better choice since we can take advantage of a wide range of theories (Ansótegui et al. 2011).

Among the theories considered in the SMT-LIB (Barrett et al. 2010) (SMT Library) we are interested in QF_LIA (Quantifier-Free Linear Integer Arithmetic). With the QF_LIA theory we can model the PB constraints that SAT-based MaxSAT algorithms generate during their execution. To this end, the PB variables can be declared as integer variables whose domain is $\{0,1\}$. Therefore, for the SMT-based MaxSAT algorithm, we just need to replace the conversions to $\mathop {C\!N\!F}\nolimits$ by the proper linear integer arithmetic predicates. As we can see in Example 11, the SMT-LIB language v2.0 is a standard language with a prefix notation where the operator is placed at the beginning of the predicates.

Example 11

Given the SAT instance of Example 8 Iteration 3, $\varphi ^6 = \{ (x_1\vee b_1 ), (x_2\vee b_2 ), (x_3\vee b_3 ), (x_4\vee b_4 ), (x_5)\ \}\ \cup \mathop {C\!N\!F}\nolimits (\sum x_i \le 1) \cup \mathop {C\!N\!F}\nolimits (5\cdot b_1+3\cdot b_3 \ge 3) \cup \mathop {C\!N\!F}\nolimits (5\cdot b_2+3\cdot b_4 \ge 3) \cup \mathop {C\!N\!F}\nolimits (5\cdot b_1+3\cdot b_3 \le 3) \cup \mathop {C\!N\!F}\nolimits (5\cdot b_2+3\cdot b_4 \le 3)$ The SMT instance $\varphi ^6$ in the SMT-LIB language v2.0 under QF_LIA (Barrett et al. 2010) would be as follows:

As suggested in Fu and Malik (2006) and Martins et al. (2011), we can preserve some learned lemmas from previous iterations that may help to reduce the search space. In order to do that, we execute the SMT solver in incremental mode. Within this mode, we can call the solve routine and add new clauses (assertions) on demand, while preserving learned lemmas. However, notice that our algorithms delete parts of the formula between iterations. For example, when we have to update the AM set in the WPM2 algorithm (see Sect. 4) by deleting some At-Most constraints. Therefore, we also have to take care of any learned lemma depending on them.

The Yices SMT solver gives the option of marking assertions as retractable. If the SMT solver does not support the deletion of assertions but supports the usage of assumptions, we can replace every retractable assertion c, with $a \rightarrow c$, where a is an assumption. Before each call, we activate the assumptions of assertions that have not been retracted by the algorithm. Notice that assertions that do have been retracted will have a pure literal ($\overline{a}$) such that a has not been activated. Therefore, the solver can safely set to false a, deactivating the clause. Moreover, any learned lemma on those assertions will also include $\overline{a}$. For example, Z3 and Mathsat SMT solvers do not allow to delete clauses, but they allow the use of assumptions.

From the point of view of incrementality it is also quite recommendable to reuse as much as possible the PB constraints we modify during the search, since we will also be able to reuse learned clauses depending on them. Pioneering works in this sense can be found in Bofill et al. (2013) and Andres et al. (2012). Our current implementation does not incorporate these complementary improvements, but it would certainly benefit from them.

6 Experimental results

In this section we present an intensive experimental investigation on the industrial and crafted instances of the MaxSAT Evaluation 2013 (MSE13) (Argelich et al. 2006-2004). We provide results for the improved WPM2 SMT-based MaxSAT solver and the best solvers of the MSE13. We run our experiments on a cluster with Intel Xeon CPU E7-8837 @ 2.67GHz processors and a memory limit of 3.5 GB. These are exactly the same specs as in the MSE13.

The instance set of the MSE13 is divided in four categories depending on the variant of the MaxSAT problem: MaxSAT (MS), Partial MaxSAT (PMS), Weighted MaxSAT (WMS) or WPMS. In addition, instances are further divided according to their nature into three subcategories: random, crafted or industrial (we are actually only interested in industrial and crafted). In each subcategory, instances are grouped by families.

We use the same set of instances for experiments on complete and incomplete solvers. The experimental results for complete and incomplete solvers are presented in Sects. 6.1 and 6.2, respectively.

6.1 Complete solvers

In this subsection, we analyze the performance of the improved WPM2 complete solver. First of all, we present the summarized results of the complete solvers at MSE13 in Tables 1 and 2. Second, we analyze the impact of each improvement on the original WPM2 algorithm in Table 3 (full detailed information in Tables 11 and 12). Then, we compare the results of the improved WPM2 solver with the best solvers of the MSE13 in Table 4 (full detailed information in Tables 13 and 14). Finally, in Tables 5 and  6, we further analyze the results of the improved WPM2 solver, discussing how it is able to exploit more efficiently the structure of the instances.

Table 1 MSE13 best solvers ordered by mean ratio of solved instances

Table 2 MSE13 best solvers

Tables 1 and 2 show the results of the MSE13 (with a timeout of 1800 s). Since families have different numbers of instances, we considered it was more fair to present the solvers ordered by mean family ratio of solved instances. In Table 1 we see the four best performing solvers on each industrial and crafted subcategory. In Table 2 we see the best performing solvers on the whole set of industrial and crafted instances. We have excluded $ISAC+$, since it is a portfolio based solver and our intention here is to compare ground solvers. Notice that $ISAC+$ already includes some of the ground solvers. The ground solvers with the best overall performance were: wpm2-$13*$ which actually corresponds to a WPM2 variation ($wpm2_{shua}*$ in Table 3), maxhs13 which consists in an hybrid SAT-ILP approach described in Davies and Bacchus (2011), qms2 which is based on an upper bound refinement described in Koshimura et al. (2012), optim-ni and msunc which implement the core-guided binary search algorithm described in Heras et al. (2011) and Morgado et al. (2012), pwbo2.3 which takes advantage of parallel processing as described in Martins et al. (2011), Martins et al. (2012), wpm1-2013 which is the SMT-based version of the improved WPM1 algorithm described in Ansótegui et al. (2012), ilp which translates WPMS into ILP and applies the MIP solver IBM-CPLEX studio124 as described in Sect. 3, and wmsz09 which implements a branch and bound algorithm described in Li et al. (2006), Li et al. (2007), Li et al. (2009). Further information about solvers and authors can be found in Argelich et al. (2006-2004).

We have completed the evaluation of the MSE13 by providing results of some solvers on those categories where originally they did not take part. For example, results of solvers wpm1-13 and wpm2-$13*$ have been added in the MS category. Results of solver qms2 have been also added to MS and WMS categories. We had to change the format of these instances so that qms2 could read them. These additional results do not change the overall performance, but they give the full picture.

From Table 2, we emphasize that the solver implementing the variation of the WPM2 algorithm (wpm2-$13*$) was already the best in family ratio of solved instances on the whole set of industrial and crafted instances at MSE13. Although it solved fewer instances than maxhs13 on the whole set, wpm2-$13*$ dominated both in family ratio and number of solved instances on the set of industrial instances.

Table 3 Impact of WPM2 improvements, compared on the industrial and crafted instances of MSE13 (number and mean ratio of solved instances)

Table 3 shows our first experiment, where we evaluate the impact of each improvement on the original WPM2 algorithm (with a timeout of 7200 s). All the variations on the WPM2 algorithm are implemented on top of the Yices SMT solver (version 1.0.29). The different variations (see Sect. 4) and corresponding implementations are named wpm2 with different subindexes. Subindex $_s$ stands for stratified approach and $_h$ for clause hardening. Regarding to how we perform the subproblem optimization, $_i$ stands for ILP translation, $_l$ stands for lower bound refinement based on subset sum, $_u$ for upper bound refinement based on satisfying truth assignment, and $_b$ for binary search. Subindex $_a$ stands for optimizing all the subproblems and $_c$ for optimizing only subproblems that contain already extended clauses. Finally, $_g$ stands for guiding the search with the optimal assignments from subproblems and $_o$ for guiding the search also with the satisfying assignments within the subproblem optimization.

Table 4 $wpm2_{shucgo}$ compared to MSE13 best complete solvers on the industrial and crafted instances of MSE13 (number and mean ratio of solved instances)

The original wpm2 has a performance of 47.6 % (959) family ratio (number) of solved instances. By using the stratified approach explained in Sect. 4.1 ($wpm2_{s}$) we solve some additional instances in all categories having the highest increase on WPMS crafted subcategory. Overall, we solve 100 more instances. By applying also the clause hardening explained in Sect. 4.2 ($wpm2_{sh}$) we solve 68 more instances, mainly on WPMS industrial subcategory. This last one, with 52.8 % (1127) family ratio (number) of solved instances, increases in performance by 5.2 % (168) compared to wpm2.

Regarding the different variations for optimizing the subproblems (see Sect. 4.3), we can see that optimizing the subproblems through ILP ($wpm2_{shia}$) is not competitive on industrial instances. It solves 236 fewer industrial instances than $wpm2_{sh}$. This is expected since, as we will see in Table 4, ilp-13, the approach based on a full translation to ILP, is also not competitive on industrial instances. On crafted instances it performs similar to the other subproblem optimization variations. It solves 169 more crafted instances than $wpm2_{sh}$, but it is not the best performing variation. Notice, however, that on MS and WPMS industrial subcategories solves more instances than ilp-13.

Optimizing subproblems by refining the lower bound ($wpm2_{shla}$), gives us some additional solved instances in all categories, having the highest increases on WPMS industrial subcategory (50) and on WPMS crafted subcategory (101). It is important to highlight that optimizing subproblems with subset sum, instead of applying the subset sum as in the original WPM2 algorithm, leads to a total increase of 173 solved instances compared to $wpm2_{sh}$.

Optimizing subproblems by refining the upper bound ($wpm2_{shua}*$), gives us an additional boost with respect to $wpm2_{shla}$. We get the highest increases in solved instances, on PMS industrial subcategory (22), and on WPMS crafted subcategory (56). Compared to $wpm2_{sh}$, we have a total increase of 273 solved instances. Notice that this variation is the one that competed in the MSE13 and is referred as wpm2-$13*$ in Tables 1, 2 and 4. Optimizing with binary search ($wpm2_{shba}$) has almost the same global performance as $wpm2_{shua}*$.

By optimizing only subproblems that do contain clauses that were already extended in previous iterations, we have an increase in family ratio and number of solved instances on all subproblem optimization variations. The upper bound refinement variation ($wpm2_{shuc}$) is the one with best performance, with 64.3 % (1423) family ratio (number) of solved instances. It increases in performance by 11.5 % (296) compared to $wpm2_{sh}$.

Finally, $wpm2_{shucg}$ is the result of extending the previous best variation ($wpm2_{shuc}$) by guiding the search with the optimal assignments from subproblems (see Sect. 4.4). This way, the number of solved instances increases by 28. By guiding the search also with the satisfying assignments within the subproblem optimization ($wpm2_{shucgo}$), the number of solved instances increases by 22 more, solving 50 more instances than $wpm2_{shuc}$. This last variation ($wpm2_{shucgo}$), with 65.7 % (1473) family ratio (number) of solved instances, increases in performance by 18.1 % (514) compared to wpm2. This is in percentage 138.0 % (153.6 %). Actually, if we take into account the timeout of 7200 s used in our experiments, we obtain an overall speed-up of 1573 (three orders of magnitude) with respect to wpm2. Basically, we compare the total run time of the solvers on all the instances. Not solved instances are assumed to contribute only with the timeout.

Table 4 shows our second experiment, where we compare the best variation of the improved WPM2 solver ($wpm2_{shucgo}$) with the best solvers of the MSE13 (with a timeout of 7200 s). In particular, we selected the best ground overall performing solvers presented in Table 2 and the best solvers for each subcategory in Table 1.

We see that $wpm2_{shucgo}$ is the best solver on the industrial set, both in family ratio and number of solved instances. On crafted instances, it is only the fifth in family ratio of solved instances. Although, on crafted instances, ilp is the first in family ratio of solved instances, as we have seen in Table 3, the variation which optimizes the subproblems through an ILP translation ($wpm2_{shia}$) does not improve the performance of the upper bound refinement variation ($wpm2_{shua*}$). We can conclude, however, that $wpm2_{shucgo}$ is the best in family ratio and number of solved instances across all industrial and crafted instances, and so the most robust followed by maxhs and qms2.

Table 5 $wpm2_{shucgo}$, certify-opt and sat4j on industrial instances

Table 6 $wpm2_{shucgo}$, certify-opt and sat4j on crafted instances

There can be several explanations for the good performance of $wpm2_{shucgo}$. In the following we extend the study presented in Ansotegui (2013b). One of this explanations is that SAT-based MaxSAT solvers are supposed to take advantage by exploiting the information (learned clauses, At-Least and At-Most constraints, etc) obtained from each SAT instance ($\varphi ^k$) into which the WPMS instance $\varphi$ is reformulated.

The conjecture is that this information makes easier the resolution of the SAT instances where k is closer to $cost(\varphi )$. In particular, those ones that are unsatisfiable which tend to be harder to solve. In order to test the plausibility of this conjecture, we introduce a new complete algorithm which takes as input the WPMS formula $\varphi$ and a cost that we initially set to $cost(\varphi )$. Therefore, this algorithm only needs to certify that the initial cost indeed corresponds to the cost of an optimal assignment. In particular, it just checks that $\varphi ^{cost(\varphi )-1}$ is unsatisfiable and $\varphi ^{cost(\varphi )}$ is satisfiable. We will refer to this algorithm as certify-opt.

In Tables 5 and 6, we compare certify-opt with the two basic search schemes of SAT-based MaxSAT solvers: (i) those that focus the search on refining the lower bound, and exploit the information of unsatisfiable cores (solver $wpm2_{shucgo}$) and, (ii) those that focus the search on refining the upper bound, and exploit the information of satisfying assignments (solver sat4j (Berre 2006)). All these approaches were implemented on top of the Yices SMT solver.

We experimented with the whole set of industrial and crafted instances from the MS, PMS, WMS and WPMS categories at the MSE13. Tables 5 and 6 show the results on industrial and crafted instances, respectively. In the tables, $\#$ stands for the total number of instances, $\#H$ and $\#S$ stand for the mean number of hard and soft clauses, respectively, and $\#*$ stands for the number of solved instances, within a timeout of 7200 s, for each solver.

The results of our experimentation show that sat4j does not have a better performance than certify-opt. Although certify-opt solves 25 more instances than sat4j, both solvers have almost the same overall performance. This can be explained because the upper bound refinement converges very quickly to the last satisfiable instance $\varphi ^{cost(\varphi )}$, but it does not take advantage from any information of the previous satisfiable instances ($\varphi ^k$ with $k \in [ cost(\varphi )+1, W(\varphi ) ]$) in order to solve more efficiently $\varphi ^{cost(\varphi )}$ and $\varphi ^{cost(\varphi )-1}$. The structure of these instances can be seen in example 7.

Regarding $wpm2_{shucgo}$, it performs much better than certify-opt. For crafted instances, it solves 144 more instances than certify-opt. The difference is more dramatic for industrial instances where it solves 555 more. One of the keys of its success seems to be that it only needs to extend with auxiliary variables those soft clauses that have appeared into an unsatisfiable core. In contrast, certify-opt or sat4j need to extend all the soft clauses. In the tables, $\%b$ shows the percentage of extended soft clauses during the search. As we can see, both certify-opt and sat4j always extend 100 % of the soft clauses, while $wpm2_{shucgo}$ only extends a part of them. In particular, on industrial instances, where the difference in performance is higher, it only extend 49.6 % of the soft clauses.

Another key point in the good performance of $wpm2_{shucgo}$ is that, the extended soft clauses in the last query are covered by various At-Most constraints instead of a single and larger one as in certify-opt or sat4j. This was proven to be more efficient in Ansótegui et al. (2009). In the tables, $\#AM$ stands for the number of At-Most constraints added during the search. When we go into detail in Table 5, in the last query of $wpm2_{shucgo}$ on industrial instances, the mean number of At-Most constraints is 212. In contrast, in Table 6, in the last query on crafted instances, the mean number of At-Most constraints is 28.7. This is also consistent with the better performance of $wpm2_{shucgo}$ on industrial instances.

6.2 Incomplete solvers

In this subsection, we analyze the performance of the improved WPM2 incomplete solver. We show the results that it would have obtained on the track for incomplete solvers at the MSE13 in Table 7 (full detailed information in Tables 15 and 16). We also discuss the quality of the upper bounds obtained during its execution on industrial and crafted instances in Figs. 2 and 3.

Table 7 $wpm2_{shucgo}$ incomplete compared to MSE13 incomplete solvers on the industrial and crafted instances of MSE13 (number and mean ratio of solved instances)

Table 7 shows our first experiment, where we compare the incomplete solver based on the improved WPM2 algorithm ($wpm2_{shucgo}$), with the best incomplete solvers of the MSE13. Results are presented following the same classification criteria as in the MSE13. For each instance, it is computed which are the solvers that obtain the best upper bound within 300 s (5 min). For each solver and subcategory we present the number of instances where the solver reported the best upper bound and the mean family ratio according to this number.

We can see that $wpm2_{shucgo}$ dominates on industrial instances, being the one that reaches the best upper bound 865 times. This is 120 more times than ccls, the second one. On crafted instances, both are dominated by optim, that in contrast performs not well on industrial instances. When we consider the whole set of industrial and crafted instances, $wpm2_{shucgo}$ is the best one 1384 times, 129 more times than the second one ccls.

In the following, we analyze the quality of upper bounds provided by $wpm2_{shucgo}$ on the whole set of industrial and crafted instances. In Fig. 2, we show the mean upper bound quality obtained during the resolution of the instances. Those instances not solved in 7200 s or solved in less than 60 s are discarded. Therefore, only 358 industrial and 129 crafted instances are taken into account. In x-axis we have the relative elapsed running time (100 % corresponds to the total time to solve the instance), and in y-axis we have the relative distance of the upper bounds to the optimum (an upper bound equal to the top weight or to the optimum, has a relative distance of 100 or 0 %, respectively). We refer to the relative distance to the optimum as the error in an upper bound (a small error means a high quality).

In the graphic at the top of Fig. 2, we have the experiments on the whole set of industrial instances (MS, PMS and WPMS categories), and on the two industrial families, with the best (WPMS upgradeability family) and the worst (PMS close solutions family) mean upper bound quality. In one third of the resolution time, the mean error in the upper bounds on the whole set of industrial instances is less than 10 % and in two thirds it is less than 6 %. In particular, for the WPMS upgradeability family, in 10 % of the resolution time the mean error is less than 1 %. Also, on some instances (PMS pbo-mcq family) the optimum (0 % error) is reached in one second while more than 1000 s are needed to certify it. On the other hand, for the PMS close solution family, in 90 % of the resolution time, the mean error is about 37 %.

In the graphic at the bottom of Fig. 2, we have the experiments on the whole set of crafted instances (MS, PMS, WMS and WPMS categories), and on the two crafted families, with the best (WPMS random-net family) and the worst (WMS CSG family) mean upper bound quality. In one third of the resolution time, the mean error in the upper bounds on the whole set of crafted instances is less than 4 % and in two thirds it is less than 2 %. In particular, for the WPMS random-net family, in 5 % of the resolution time the mean error is less than 1 %. On the other hand, for the WMS CSG family, in 10 % of the resolution time the mean error is 100 and in 90 % of the resolution time it is about 14 %.

It may seem that we get better results on crafted instances, however we should take into account that, the number of crafted instances solved by $wpm2_{shucgo}$ within 60 and 7200 run time seconds, is lower than the number of industrial instances. For some instances unsolved by $wpm2_{shucgo}$, we can consult the optimal cost found by other MaxSAT solvers (none dominates completely at the MSE13). This allows us to know which is the quality achieved by $wpm2_{shucgo}$ even if it was not able to solve the instance exactly.

In Fig. 3, we experimented with the industrial and crafted instances of MSE13 where any of the solvers in Table 4 was able to find the optimum.² We show the number of industrial and crafted instances, where $wpm2_{shucgo}$ reached an upper bound with a relative distance to the optimum (error) of less than 20, 5 and 0 % in a given elapsed run time. In x-axis we show the elapsed time from 0 to 7200 s, and in y-axis we show the number of instances.

In the graphic at the top of Fig. 3, we have the experiments on the industrial instances. We can see that, a high quality of upper bound is reached on a great number of instances in a relative short run time. From 20 to 5 % error, there is almost no difference. In 60 s, an upper bound with an error of less than 5 % is reached on 874 out of 1012 instances. In 300 s it is reached on 945 instances and in 7200 s on 973 instances. With respect to a 0 % error in the upper bound (optimum is not necessarily certified), in 60 s it is reached on 596 instances, in 300 s on 804 instances and in 7200 s on 881 instances.

In the graphic at the bottom of Fig. 3, we have the experiments on the crafted instances. Compared to what happens on the industrial set, there is a greater difference in number of instances, depending on the maximum error that we consider. We can see that, an upper bound with an error of less than 20 % is reached on 912 out of 952 instances in 60 s. However, the number of instances with less than a 5 % error in the upper bound is significantly lower, 704 instances in 60 s, 753 instances in 300 s and 822 instances in 7200 s. With respect to a 0 % error in the upper bound, the difference is even more important. In 60 s it is reached only on 464 instances, in 300 s only on 502 instances and in 7200 s only on 592 instances.

As a concluding remark, in 300 s (the timeout of the track for incomplete solvers at MSE13), $wpm2_{shucgo}$ has reached an upper bound with an error of less than 5 % on 945 out of 1012 industrial instances. This is consistent with the results in Table 7 where we have shown that $wpm2_{shucgo}$ has the best performance on industrial instances.

Table 8 Best complete solvers on the industrial and crafted instances at MSE14 (number and mean ratio of solved instances)

6.3 Results at MaxSAT evaluation 2014

In the previous subsections, we have analyzed and described in detail the impact of every improvement incorporated in wpm2. Here, we study the performance of the wpm2014 solver that took part in MSE14. This solver behaves exactly as $wpm2_{shuc}$ for (Partial) MaxSAT instances, and includes some efficiencies for Weighted (Partial) MaxSAT instances. In particular, we show that although this solver is not as competitive as the newest complete solvers, its incomplete version (as described in this article) ranked the first for the incomplete track.

Table 9 Best incomplete solvers on the industrial and crafted instances at MSE13 (number and mean ratio of solved instances)

The sets of instances at MSE14 are almost the same as the ones at MSE13. The main difference is that WMS families were integrated into the WPMS set. The classification criteria remains the same.

Table 8 summarizes the results for the best complete solvers on the whole set of industrial and crafted instances according to MSE14. We have excluded the portfolio $ISAC+$, since our main aim here is to compare algorithms and ground solvers. We have also included ilp, scip-ms and ahmaxsat-ls, which win in mean family ratio or number of solved instances on some crafted categories. On crafted instances, the best solver in mean family ratio (number) of solved instances is maxhs (ilp), and on the whole set, it is maxhs (eva500a).

On industrial instances, we can see that wpm2014 is the fourth one. The best three solvers on industrial instances were eva500a (Narodytska and Bacchus 2014), mscg (Morgado et al. 2014) and open-wbo (Martins et al. 2014). For open-wbo, we selected the best version for each category. To our best knowledge eva500a automatically detects the category and applies a predefined user parametrization. These three solvers are SAT-based MaxSAT solvers too. Without going into detail, we could say that the approaches of eva500a and mscg allow them to generate simpler PB constraints. Moreover, all three new solvers build incrementally these PB constraints, instead of generating them from scratch. In the case of open-wbo, PB constraints are explicitly built incrementally. In the case of eva500a and mscg this incrementality comes naturally as a result of the nature of the algorithm. These improvements are complementary to the approach of wpm2014 and therefore they could be incorporated. We can yet see that wpm2014 achieves the best ratio in WPMS instances.

Table 9 summarizes the results for the best incomplete solvers on the whole set of industrial and crafted instances according to MSE14. Clearly, wpm2014 dominates on industrial instances, and it is the best overall solver on industrial and crafted instances. For optimax (implementing the BCD algorithm (Morgado et al. 2012)), the second best solver for industrial instances, we also selected the best version for each category.

Since we are showing a partial order, we have also included the solvers that take part in all categories dist, ccls2014, ccmpa and ahmaxsat-ls, from which dist and ccls2014 win in mean family ratio or number of solved instances on some crafted categories.

Finally, we have decided to extend the results of the incomplete track of the MaxSAT Evaluation by comparing to wpm2014 the best complete solvers than can provide upper bounds but did not take part at the incomplete track: qms2 and open-wbo. We performed the comparison on industrial instances, where all these solvers were competitive.

In Table 10, we present the dominance relation between pairs of solvers on the the total (MS PMS WPMS) set of industrial instances. For example, wpm2014 (open-wbo) is able to obtain a better or equal upper bound than open-wbo (wpm2014) on 939 (857) industrial instances of which 51 (43) are MS, 498 (473) are PMS and 390 (341) are WPMS.

Table 10 Comparison as incomplete solvers of wpm2014, open-wbo and qms

On the whole set of industrial instances wpm2014 outperforms both open-wbo and qms2. Even though wpm2014 was not the best complete solver at MSE14, it dominates the other solvers as an incomplete approach. For PMS, we can see that qms2 is the best performing approach, but for MS and WPMS, wpm2014 performs better. Notice that qms2 is an efficient implementation of a SAT-based MaxSAT algorithm that mainly follows and upper-bound refinement strategy but unlike wpm2014 needs to place PB constraints on the whole set of soft clauses. So, if the subproblems represent most of the original instance, qms2 should be better, but if the subproblems cover only a small fraction, wpm2014 has advantages even with a less efficient approach for subproblems. Precisely, thanks to the insights of Table 5 in Sect. 6.1, we know that for PMS instances, $wpm2_{shucgo}$ (wpm2014) covers in average a $63.6~\%$ of the soft clauses, while for WPMS, it covers in average only a 33.9 %. This suggests that incorporating the efficiencies of qms2 into wpm2014 will certainly improve its performance on PMS instances and perhaps on WPMS instances too.

These results confirm that by applying the subproblem optimization technique and exploiting the satisfying assignments from subproblems, a complete MaxSAT solver can be used as an effective incomplete MaxSAT solver.

7 Conclusions and future work

True innovation in heuristic-search research is not achieved from yet another method that performs better than its competitors if there is no understanding as to why the method performs well (Sörensen 2015). Following this principle, we have provided a detailed analysis on how the improved WPM2 solver has experienced a significant boost on solving industrial instances, which is our ultimate goal.

In particular, the subproblem optimization approach and the exploitation of the satisfying assignments from subproblems seem to have the most clear impact on efficiency. Therefore, solving incrementally an optimization problem by solving some of its subproblems is a promising avenue. This way we can focus on a reduced portion of the instance, allowing us to use less complex PB constraints to solve the whole problem.

We have seen that SAT-based MaxSAT solvers are able to exploit the information derived from refining lower bounds and upper bounds. We have confirmed that this is not only crucial to locate quickly better upper bounds, also to certify efficiently that a given upper bound is the optimum.

Moreover, from a more practical point of view, we know that although many NP-hard problems can not be solved exactly, in industry they are mostly focused on obtaining better upper bounds. Therefore, completeness is not always a mandatory requirement to guarantee practical success. In this sense, we have shown how we can turn a complete solver into an efficient incomplete solver by extending the satisfying assignments from the subproblem optimization phases to the whole problem.

As shown in the experimental evaluation, the incomplete version of the improved WPM2 solver would have dominated on industrial instances the track for incomplete solvers at the MSE13. Furthermore, the solver wpm2014, which is just a more efficient implementation of the improved WPM2, was the best performing solver on industrial instances on the track for incomplete solvers at the MSE14.

As future work, we will study how to improve the interaction with the optimization of the subproblems. A portfolio that selects the most suitable optimization approach depending on the structure of the subproblems seems another way of achieving additional speed-ups.

From the point of view managing even more efficiently PB constraints, following recent works (Narodytska and Bacchus 2014; Morgado et al. 2014; Martins et al. 2014), it is also quite recommendable to use less complex PB constraints and reuse as much as possible of them when they are modified.

Finally, we have also shown that the SMT technology is an underlying efficient technology for solving the MaxSAT problem. A positive side effect is that our algorithm can be naturally extended to solve the MaxSMT problem.

Appendix

See Tables 11, 12, 13, 14, 15 and 16.

Table 11 Impact of WPM2 improvements, compared on the industrial instances of MSE13 (number and mean ratio of solved instances)

Table 12 Impact of WPM2 improvements, compared on the crafted instances of MSE13 (number and mean ratio of solved instances)

Table 13 $wpm2_{shucgo}$ compared to MSE13 best complete solvers on the industrial instances of MSE13 (number and mean ratio of solved instances)

Table 14 $wpm2_{shucgo}$ compared to MSE13 best complete solvers on the crafted instances of MSE13 (number and mean ratio of solved instances)

Table 15 $wpm2_{shucgo}$ incomplete compared to MSE13 incomplete solvers on the industrial instances of MSE13 (number and mean ratio of solved instances)

Table 16 $wpm2_{shucgo}$ incomplete compared to MSE13 incomplete solvers on the crafted instances of MSE13 (number and mean ratio of solved instances)