A MaxSAT Algorithm Using Cardinality Constraints of Bounded Size

1 Introduction

MaxSAT is the optimization variant of the satisfiability problem for propositional formulas. In its most general formulation, also known as Weighted Partial MaxSAT [Cha et al., 1997], the input formula is partitioned into hard and soft clauses, where soft clauses are associated with a weight. Hard clauses must necessarily be satisfied, while soft clauses should be possibly satisfied. In fact, the goal is to find an assignment satisfying hard clauses and minimizing the total weight of unsatisfied soft clauses. The research in this field is active as many industrial instances, originated by real-world problems [Morgado et al., 2013] such as routing [Xu et al., 2003] and reasoning over biological networks [Guerra and Lynce, 2012], still represent a challenge for modern solvers [Argelich et al., 2014]. Several MaxSAT algorithms were proposed, also in terms of broader frameworks [Bacchus et al., 2014; Marques-Silva and Janota, 2014]. Nowadays, the most promising algorithms work by iteratively checking satisfiability of a formula that is properly modified during the search until a satisfying assignment is found, which eventually results in an optimum solution. In more detail, the check does not distinguish between hard and soft clauses, and each inconsistency is associated with a set of unsatisfiable clauses, referred to as unsatisfiable core in the literature. Soft clauses in an unsatisfiable core are thus relaxed by adding fresh variables. Clauses or cardinality constraints are also introduced in order to minimize the effect of the relaxation.

∗This work was partially supported by MIUR within project "SILAB BA2KNOW - Business Analitycs to Know", and by Regione Calabria, POR Calabria FESR 2007-2013, within project "ITravel PLUS" and project "KnowRex". Mario Alviano was partly supported by the National Group for Scientific Computation (GNCSINDAM), and by Finanziamento Giovani Ricercatori UNICAL.

Several core-guided strategies were proposed for implementing such a relaxation step. Among them are approaches that introduce a cardinality constraint, possibly encoded in clauses [E´en and S¨orensson, 2006; Roussel and Manquinho, 2009], and those that add clauses resulting fromMaxSAT resolution [Larrosa and Heras, 2005]. Two prominent examples of algorithms based on these strategies are OLL [Andres et al., 2012] and PMRES [Narodytska and Bacchus, 2014], implemented in solvers that had excellent results in the 2014 MaxSAT Evaluation [Argelich et al., 2014]. In particular, OLL is used by CLASP and MSCG [Morgado et al., 2014], and PMRES is implemented by EVA. However, besides pros there are also cons, as will be clarified soon.

OLL introduces a cardinality constraint for enforcing that at most one soft clause in the core can be unsatisfied in a solution. If such a constraint cannot be satisfied then a core containing the new constraint is detected. In this case, the algorithm introduces another constraint for enforcing that at most two soft clauses in the first core can be unsatisfied in a solution, and so on. Hence, a first drawback of OLL is that it may introduce several constraints for handling one core, possibly slowing down the propagation. Such a drawback was overcome by MSCG thanks to a smart translation into a sorting network that compactly represents all constraints possibly introduced by OLL for handling one core. However, even within this smart encoding, adding cardinality constraints may increase exponentially the number of refutations in subsequent checks [Bacchus and Narodytska, 2014].

PMRES introduces clauses of bounded size resulting from MaxSAT resolution. Essentially, two soft clauses are replaced by two new soft formulas being the disjunction and the conjunction of the original clauses. The conjunction is encoded in clauses, and the variable associated with its satisfaction is resolved with another soft clause in the core, so that the process is repeated hierarchically for all clauses in the core. However, even if on the one hand this process inhibits the exponential grow up on the number of refutations, on the other hand several variables introduced by PMRES for processing a core can jointly be part of a new core, and this event is influenced by the order in which soft clauses are processed.

A new algorithm for processing unsatisfiable cores, namely ONE, is introduced in this paper. ONE is inspired by OLL but has the advantage of introducing exactly one cardinality constraint for each detected core, which also means that it is simpler to implement. In fact, while new constraints must be added by OLL when a previously introduced constraint belongs to some unsatisfiable core, the constraint added by the new algorithm does not require special treatments in subsequent satisfiability checks. Actually, this is also the case for the variant of OLL using sorting networks, as implemented in MSCG, but the algorithm presented here does not interdict the use of native pseudo-Boolean solvers, which may be an advantage for sufficiently small constraints.

The generalization of ONE, called K, is motivated by the exponential grow up on the number of refutations due to the addition of cardinality constraint. In this second form, a parameter bounds the size of cardinality constraints introduced for handling cores. The processed core is indeed partitioned in sets of bounded size, and each partition is associated with a cardinality constraint. It is interesting to observe that K also generalizes PMRES, which is obtained for the smallest allowed value of the parameter.

ONE and K have been implemented in a new pseudoBoolean solver extending GLUCOSE [Audemard and Simon, 2009], and their performance have been assessed on the industrial instances of the 2014 MaxSAT Evaluation. Several values of the parameter bounding the size of cardinality constraints were tested, many of which resulted in a performance comparable with state-of-the-art solvers such as EVA and MSCG. Actually, when constraints are bound to contain at most 48 literals, MAXINO solves 12 instances more than EVA and 17 more than MSCG. Also the average execution time benefits of the new algorithm on many tested instances. Prototype and formal proofs are available online at the following link: http://alviano.net/software/maxino/.

2 Background

Let V be a countable set of propositional variables. A cost function w is a function w : V → N associating each variable x with its cost w(x). A literal is either a variable x, or its negation ¬x. The complement of a literal ℓ is denoted ℓ, i.e., x = ¬x and ¬x = x for all x ∈ V. A pseudo-Boolean constraint, or simply constraint, is of the following form:

where n ≥ 1, k ≥ 0, ai ≥ 1 and ℓi is a literal, for all i ∈ [1..n]. If a1 = · · · = an = 1 then (1) is a cardinality constraint. If in addition k = 1 then (1) is also called clause and possibly denoted as a disjunction ℓ1 ∨ · · · ∨ ℓn, or as an implication ℓ1 ∧· · ·∧ℓn-1 → ℓn. A propositional theory φ is a set of constraints. If all constraints in φ are clauses, φ is also called propositional formula. The set of variables occurring in φ is denoted vars(φ).

An interpretation I is a function I : V → {T, F} associating each variable x with a Boolean truth value I(x). An interpretation I is also denoted as the set {x ∈ V | I(x) = T}.

Algorithm 1: Core-guided MaxSAT algorithm

Input : A consistent formula φ, a cost function w(·) Output: An optimum model I of φ, and its cost 1 begin 2 lower bound := 0; 3 (sat , I, C) := Solve(φ∪{x ∈ vars(φ) | w(x)≥1}); 4 if sat then return (I, lower bound); 5 lower bound := lower bound +minx∈C w(x); 6 for x ∈ C do w(x) := w(x) - minx∈C w(x); 7 φ = ProcessCore(φ,w,C); 8 goto 3;

Two sets S, S′ of interpretations are equivalent with respect to a context V ⊆ V, denoted S ≡V S′ , if {I ∩ V | I ∈ S} = {I ∩ V | I ∈ S′}. Relation |= is inductively defined as follows: For a variable x ∈ V, I |= x if x ∈ I, and I |= ¬x if x /∈ I. For a constraint c of the form (1), I |= c if the following inequality is satisfied:

For a theory φ, I |= φ if I |= c for all c ∈ φ. If I |= φ then I is a model of φ. The cost of I is defined as follows:

A theory φ is consistent if φ has at least one model, otherwise φ is inconsistent and each subset C of φ being inconsistent is called an unsatisfiable core of φ. A model I of φ is optimum with respect to a cost function w if there is no J ⊆ V such that J |= φ and w(J) < w(I). The set of optimum models of φ with respect to w is denoted O(φ, w).

The relaxation of a clause c, denoted relax (c), is the clause c∨¬rc, where rc is a fresh variable, i.e., a variable not occurring elsewhere. The computational problem analyzed in this paper is Weighted Partial MaxSAT (WPMS): Given a formula φh ∪φs , and a function ws : φs → N+, compute an optimum model of φh ∪{relax(c) | c ∈ φs} with respect to a cost function w such that w(rc) = ws (c) for all c ∈ φs , and w(x) = 0 for all other variables. If ws (c) = 1 for all c ∈ φs then the computational problem is called Partial MaxSAT (PMS), and if in addition φh = ∅ then it is referred to as MaxSAT (MS).

3 Core-guided Algorithm

Algorithms for computing solutions of the computational problems introduced in the previous section are presented here. To simplify the presentation, algorithms will be given for an input comprising a formula φ and a cost function w : V → N, obtained as described in the previous section and with the additional assumption that φ is consistent.

3.1 The Basic Algorithm ONE

An abstract procedure for computing an optimum model of φ is reported in Algorithm 1. It uses an external function Solve for searching a model or an unsatisfiable core of a formula

Function ProcessCore(φ, w, C)

1 begin

2 Let C = {x0, . . . , xn}, where n ≥ 0; 3 Let r1, . . . , rn be fresh variables; 4 for i ∈ [1..n] do w(ri) := minx∈C w(x); 5 φ := φ ∪ {x0 + · · · +xn +¬r1 + · · · +¬rn ≥ n}; 6 for i ∈ [1..n - 1] do φ := φ ∪ {ri → ri+1};

φ′ obtained by extending φ with unary clauses of the form x, where x is a variable with positive cost (line 3). In more detail, the output of Solve(φ′ ) is either (T, I,-) in case I |= φ′ , or (F,-,C) if there is an unsatisfiable core φ′′ of φ′ such that φ′′ ∩ {x ∈ vars(φ) | w(x) ≥ 1} = C.

In case function Solve returns (F,-,C), the minimum cost associated with variables in C is computed, i.e., minx∈C w(x). The core actually provides evidence that the cost of any model of φ must be greater or equal to this value. Hence, a lower bound is stored and updated during the execution of the algorithm. Initially, its value is 0 (line 2), and it is increased by minx∈C w(x) whenever function Solve returns an unsatisfiable core C (line 5). Quantity minx∈C w(x) is then removed from the cost of all variables in C (line 6), and a total cost of (|C| - 1) · minx∈C w(x) is equally distributed to |C| - 1 new variables r1, . . . , rn by function ProcessCore (line 4 of the function). Such a function can implement one of several strategies. The one reported here is new and uses a constraint to enforce the satisfaction of as many as possible variables in the set C = {x0, . . . , xn} (line 5). If n of these variables can be assigned T in a model of φ, then all new variables r1, . . . , rn can be assigned T as well. On the other hand, if only n-1 variables in {x0, . . . , xn} can be assigned T in a model of φ, then one variable among r1, . . . , rn must be assigned F in order to satisfy the constraint. Actually, clauses of the form ri → ri+1 ensure that such a variable must be r1 (line 6). By generalizing the previous argument, formalized later in Lemma 1, it is possible to conclude that if only m ∈ [0..n - 1] variables in {x0, . . . , xn} can be assigned T in a model of φ, then variables r1, . . . , rn-m must be assigned F in order to satisfy the constraint.

The algorithm then continues to search for an optimum model, processing unsatisfiable cores as they are identified and incrementing the lower bound accordingly. Finally, when a model I is returned by function Solve, the algorithm terminates, and outputs I and the current lower bound.

Example 1. Let φ be a formula equivalent to the theory {¬a + ¬b + ¬c + ¬d ≥ 2}, and let w be such that w(a) = w(b) = 1 and w(c) = w(d) = 2. Algorithm 1 searches for a model or an unsatisfiable core of φ ∪ {a, b, c, d}. Function Solve returns (F,-, {a, c, d}), and set {a, c, d} is processed: The lower bound is increased to 1, fresh variables r1, r2 are introduced, constraint a + c + d + ¬r1 + ¬r2 ≥ 2 and clause r1 → r2 are added to φ, and w becomes w(a) = 0, w(b) = w(c) = w(d) = w(r1) = w(r2) = 1. Function Solve is now invoked for φ ∪ {b, c, d, r1, r2}, and a new unsatisfiable core {b, c, d} is found and processed: The lower bound is increased to 2, fresh variables r3, r4 are introduced,

Function k-ProcessCore(φ, w, C)

1 begin // use constraints of size 2 · (k+1) 2 Let C = {x0, . . . , xn·k}, where n ≥ 0; 3 Let r1, . . . , rn·k be fresh variables; 4 for i ∈ [1..n · k] do w(ri) := minx∈C w(x); 5 Let c0 = x0, and c1, . . . , cn be fresh variables; 6 for i ∈ [1..n] do 7 φ := φ ∪ {ci-1 + x(i-1)k+1 + · · · + xi·k + ¬ci+¬r(i-1)k+1+· · ·+¬ri·k ≥ k+1}; 8 φ := φ ∪ {ci → r(i-1)k+1}; 9 for j ∈ [1..k - 1] do 10 φ := φ ∪ {r(i-1)k+j → r(i-1)k+j+1};

constraint b + c + d + ¬r3 + ¬r4 ≥ 2 and clause r3 → r4 are added to φ, and w becomes w(a) = w(b) = w(c) = w(d) = 0, w(r1) = w(r2) = w(r3) = w(r4) = 1. Theory φ ∪ {r1, r2, r3, r4} is now satisfiable, and function Solve returns (T, {c, d, r1, r2, r3, r4}, -). It is an optimum model of the original formula, and its cost is 2. ■

3.2 The Parametrized Algorithm K

A drawback of core-guided algorithms making use of cardinality constraints was reported in [Bacchus and Narodytska, 2014]. Actually, each ri introduced by function ProcessCore is associated with several assignments, which may become computationally expensive to refute in subsequent calls to function Solve when the cost of some ri is decreased to 0. In particular, note that in x0 + · · · +xn +¬r1 + · · · +¬rn ≥ n, variable r1 is associated with the satisfaction of x0 + · · · + xn = n, which is the case for n + 1 different interpretations of variables x0, . . . , xn. Similarly, r2 is associated with the satisfaction of x0 + · · · + xn = n - 1, i.e., with (n+1 2 ) different interpretations. For a generic i ∈ [1..n], ri is associated with x0 + · · · + xn = i, i.e., (n+1 i ) interpretations, which is an exponential number in general.

A different strategy for processing unsatisfiable cores, referred to as PMRES [Narodytska and Bacchus, 2014], introduces clauses of two and three literals instead of cardinality constraints. In fact, for a core {x0, . . . , xn}, PMRES produces, for all i ∈ [1..n], the following clauses:

where c0 = x0 and c1, . . . , cn are fresh variables with cost 0, and r1, . . . , rn are as in function ProcessCore. In a nutshell, the above clauses enforce the satisfaction of as many as possible of the following formulas: x0 ∨ x1, (x0 ∧ x1) ∨ x2, (x0 ∧ x1 ∧ x2) ∨ x3, and so on, where conjunctions are compactly represented by variables c1, . . . , cn. Actually, variable cn is not really introduced, but it is left here to simplify the presentation. Moreover, correctness of PMRES can be proved also if clauses of the form ci-1 ∧ xi → ci are replaced by clauses of the form ci → ri, as will be proved later.

By elaborating on the previous observations, a new characterization of PMRES in terms of cardinality constraints is provided below:

for all i ∈ [1..n]. In fact, the truth of ci implies the truth of ri because of ci → ri, and therefore also of ci-1 and xi because of the constraint. It is now evident that PMRES limits the exponential blow up on the number of refutations associated with new variables by limiting the size of constraints to a small, fixed constant. A natural question is thus whether the above formulation of PMRES can be combined somehow with the constraints and clauses introduced by function ProcessCore as presented in the previous section, in order to relax the limit on the size of constraints. A positive answer to this question is provided by function k-ProcessCore, where parameter k limits the size of cardinality constraints to be at most 2 · (k + 1). To simplify the presentation, the function is presented for a set C of exactly n · k + 1 variables, where n ≥ 0. Such an assumption does not limit anyhow the generality of the algorithm because any set of variables can be properly padded with fresh variables to reach the required cardinality, or more pragmatically the last added constraint may be properly modified for containing less literals. An example should better clarify how unsatisfiable cores are processed by the new function.

Example 2. Let C = {a, b, c, d, e}. Function ProcessCore would introduce a constraint of the form a+b+c+d+e+ ¬r1 + ¬r2 + ¬r3 + ¬r4 ≥ 4, and clauses r1 → r2, r2 → r3, r3 → r4. On the other hand, function 2-ProcessCore would introduce two constraints, a + b + c + ¬c1 + ¬r1 + ¬r2 ≥ 3 and c1 +d+e+¬c2 +¬r3 +¬r4 ≥ 3, and clauses c1 → r1, r1 → r2, c2 → r3 and r3 → r4. If instead C = {a, b, c, d}, the last constraint would be c1 +d+¬c2 +¬r3 ≥ 2. ■

Note that PMRES is essentially function 1-ProcessCore, while function ProcessCore is obtained for unbounded k, or more precisely for k > ∑x∈V w(x).

3.3 Correctness

In order to prove the correctness of Algorithm 1, the argument reported in Section 3.1 is first formalized.

Lemma 1. Let φ be a propositional theory, w be a cost function, and {x0, . . . , xn} ⊆ V be such that n ≥ 0 and w(xi) ≥ 1 for all i ∈ [0..n]. Let m = mini∈[0..n] w(xi), and r0, . . . , rn be fresh variables. Define φ′ and w′ as follows:

The following relation holds: O(φ, w) ≡vars(φ) O(φ′ , w′ ).

Correctness of the algorithm using function ProcessCore easily follows by noting that if set C = {x0, . . . , xn} is returned by function Solve, then x0 + · · · + xn = n + 1 cannot be satisfied, and therefore r0 must be assigned F in all models of the theory φ. Similarly, correctness when function k-ProcessCore is used can be established by iteratively applying Lemma 1 on chunks of set C. In more detail, if C = {x0, . . . , xn·k}, then the constraint and clauses added for i = 1 preserve optimum models. Moreover, variable r0 in Lemma 1 is variable c1 in the function, and it is essentially equivalent to the conjunction x0 ∧ · · · ∧ xn. This variable is then used in the subsequent constraint, following the idea of PMRES, and Lemma 1 can be applied again to prove that optimum models are preserved for all i ∈ [1..n]. As for ProcessCore, the unsatisfiable core returned by function Solve guarantees that at least one variable among x0, . . . , xn·k, and therefore cn, must be assigned F in any model of φ.

Theorem1. Algorithm1 is correct, that is, for any consistent formula φ and cost function w, it outputs a pair (I,w(I)), where I ∈ O(φ,w). Correctness holds also if function kProcessCore is used, for all k ≥ 1.

Since 1-ProcessCore is essentially PMRES, the following is a corollary of the above theorem:

Corollary 1. PMRES is correct also if clauses of the form ci-1 ∧ xi → ci are replaced by clauses of the form ci → ri.

4 Implementation and Evaluation

ONE and K have been implemented in MAXINO, a new pseudo-Boolean solver extending the single-thread version of GLUCOSE 4 [Audemard and Simon, 2009], and featuring additional evaluation techniques such as disjoint core analysis and, for weighted instances, stratification, hardening and Boolean multilevel optimization [Ans´otegui et al., 2009; 2013; Argelich et al., 2009]. To ease a comparison with stateof-the-art solvers, PMRES has been implemented as well according to [Narodytska and Bacchus, 2014].

The performance of MAXINO was assessed on the industrial instances of the 2014 MaxSAT Evaluation [Argelich et al., 2014], which includes three tracks, namely MaxSAT (MS; 55 instances), Partial MaxSAT (PMS; 568 instances) and Weighted Partial MaxSAT (WPMS; 410 instances). The experiment was run on an Intel Xeon CPU 2.4 GHz with 16 GB of RAM. CPU and memory usage were limited to 1,800 seconds and 8 GB, respectively. MAXINO was compared with the (non-portfolio) solvers that better performed on industrial instances of the 2014 MaxSAT Evaluation, namely EVA 500a [Narodytska and Bacchus, 2014], OPENWBO 1.3.0 [Martins et al., 2014], MSCG [Ignatiev et al., 2014; Morgado et al., 2014] and CLASP 3.1.1 [Andres et al., 2012] (with options --opt-strategy=usc,1 --opt-sat --configuration=trendy). The comparison with EVA, CLASP and MSCG is of particular interest. In fact, EVA implements PMRES, while OLL is used by CLASP, and also by MSCG on weighted instances.

A summary of the result is reported in Table 1, where the best performance overall and in each track is emphasized in bold. In the table, PMRES is MAXINO running PMRES, ONE is MAXINO running ONE, and Kn is MAXINO running K with constraints of size at most n. As a general comment, it can be observed that MAXINO does not reach performance of stateof-the-art solvers neither with PMRES nor by ONE, which respectively solve 4 and 22 instances less than EVA. On the other hand, MAXINO has a performance boost when K is used, and in fact the tested versions solve at least 4 instances more than EVA, with a peak of 12 for K48 . Comparing with the other solvers, K48 solves 17, 38 and 55 more instances than MSCG, OPENWBO and CLASP, respectively. The same ranking is obtained if memory is limited to 3.5 GB as in the Evaluation, as the difference is of 4 instances for MSCG, 1 instance for CLASP and OPENWBO, and 2 instances for MAXINO.

Figure 1(a) is a cactus plot of the tested versions of MAXINO. Recall that a cactus plot reports for each solver the number of solved instances in a given time, producing an aggregated view of its overall performance. The performance of ONE is the first that deteriorate, followed by PMRES, while the several Kn can solve more instances and always in less time. Even if approximately the same good performance is achieved for all tested parameters, the line of K48 clearly indicate a leader in this group. It is also interesting to observe that the performance of MAXINO improves by 8 instances when PMRES is replaced with K16 , and even more instances are solved when the parameter is further increased, until a point in which the overall performance starts to deteriorate and is expected to align with ONE. Indeed, the benchmark was also run for K256 , K512 and K1,024 , which are not reported in the table, and the expected trend was observed as 880, 875 and 870 instances were solved, respectively.

Further comparisons with state-of-the-art solvers are shown in Figure 1. In particular, Figure 1(b) highlights that the overall performance of PMRES, EVA and MSCG are comparable, and are all overcome by K48 . The remaining cactus plots report the results track by track. Concerning MS, reported in Figure 1(c), the performance of K48 is overcome by OPENWBO, which solves the same number of instances but in less time. However, it is also true that K128 solves 1 instance more than K48 and OPENWBO, which can be explained by the fact that huge cores of up to 500,000 relaxing variables are detected for instances in this track. For such instances it seems to be preferable to introduce larger constraints, so that less constraints have to be added for processing a single core. Concerning PMS, K48 solves 5, 7, 11 and 23 instances more than OPENWBO, EVA, MSCG and CLASP, respectively. Figure 1(d) also shows that K48 is usually faster than EVA, MSCG and CLASP, while OPENWBO is more comparable in speed. Concerning WPMS, PMRES, K24 , K48 , K128 and EVA have the best performance in terms of solved instances, but Figure 1(e) highlights that K48 is around 5 time faster than EVA.

An instance by instance comparison of K48 with EVA and MSCG, the state-of-the-art solvers that best performed, is reported in the scatter plots in Figure 1(f). In these plots a point (x, y) is reported for each instance, where x is the running time of EVA or MSCG, and y is the running time of K48 . It can be observed that K48 is generally much faster than EVA and MSCG, as the majority of points is located below the diagonal. In fact, K48 is faster than EVA and MSCG in respectively 758 and 672 instances, and slower only 133 and 198 times.

5 RelatedWork

The first core-guided algorithm for MaxSAT was introduced in the seminal work of [Fu and Malik, 2006], which originated the MSU family of algorithms [Marques-Silva and Manquinho, 2008; Marques-Silva and Planes, 2008], eventually extended to solve weighted instances [Manquinho et al., 2009; Ans´otegui et al., 2009]. The paper follows this line of research, and introduces two core-guided algorithms, namely ONE and K. ONE is inspired by OLL [Andres et al., 2012]. Intuitively, for an unsatisfiable core {x0, . . . , xn} (n ≥ 0), OLL introduces a cardinality constraint of the form x0 + · · · + xn + n · ¬r1 ≥ n, where r1 is a fresh variable whose weight is set to mini∈[0..n] w(xi). The idea here is that at least one variable in {x0, . . . , xn} must be assigned F, but there are still chances that n of them can be assigned T. If this is not the case and an unsatisfiable core containing variable r1 is detected, a new constraint x0 + · · · + xn + n · ¬r2 ≥ n - 1 is introduced in addition to the one associated with the new core. Hence, the weighted variable r2 is associated with the satisfaction of at least n-1 variables in {x0, . . . , xn}. Therefore, in general OLL may introduce n different constraints for a core of n - 1 variables. ONE instead always adds a single constraint for each detected core. A similar strategy was implemented in MSCG [Morgado et al., 2014], where a sorting network with input {x0, . . . , xn} and output {r1, . . . , rn} smartly encodes all constraints introduced by OLL.

K, instead, is inspired by PMRES [Narodytska and Bacchus, 2014], an algorithm based on MaxSAT resolution [Larrosa and Heras, 2005] overcoming the drawback associated with the exponential number of refutations that current algorithms based on cardinality constraints must face. Indeed, as discussed in Section 3.2, PMRES handles cores by means of clauses of two and three literals. However, by restating PMRES in terms of cardinality constraints, a more general algorithm emerges, which eventually results in the parametrized K. Actually, K combines the strengths of both PMRES and OLL. In fact, by bounding the size of constraints as in PMRES, K is not affected by the exponential increase of the number of refutations. Moreover, it can be observed empirically that OLL and ONE usually discover smaller cores than PMRES, which is due to the fact that several variables introduced by PMRES for processing a core can possibly be part of a new core, while this cannot happen for OLL and ONE.

6 Conclusion

ONE and K extend and generalize two successful core-guided algorithms, namely OLL and PMRES. ONE and K are implemented in MAXINO, a pseudo-Boolean solver extending GLUCOSE. Even if the solver itself is new, and therefore it does not have the maturity of state-of-the-art systems, it performed well on the industrial instances of the 2014 MaxSAT Evaluation. In fact, while the unbounded ONE performed worse than CLASP running OLL on unweighted instances, and the implementation of PMRES solved a few instances less than EVA, sensible performance gains have been observed for the parametrized K. It is interesting to note that such performance gains are obtained for several values of the parameter, which is an insight that usually the performance of OLL and similar algorithms deteriorates because of a few, huge cores. This may suggest, as a future work, a dynamic implementation of K, where the parameter is not fixed a priori but set on a percore basis, according to a function taking into account the size of the core. Configuration techniques such as those used by ISAC+ [Ans´otegui et al., 2014] may be also considered for this purpose. Finally, ONE and K will be extended to Answer Set Programming and implemented in the ASP solver WASP [Alviano et al., 2013; 2014].