On Computing Minimal Correction Subsets

1 Introduction

A set of constraints is over-constrained if the constraints cannot be simultaneously satisfied [Meseguer et al., 2003]. For over-constrained problems, one is often interested in finding a maximal set of constraints that can be satisfied or, equivalently, a minimal set of constraints that need to be relaxed (among those constraints that can be relaxed) (e.g. [Junker, 2004]). A related objective is to compute a minimal subset of constraints that explains why the initial set of constraints cannot be simultaneously satisfied. For Boolean formulas, the former are referred to as Minimal Correction Subsets (MCSes) and the latter as Minimally Unsatisfiable Subsets (MUSes) (e.g. [Liffiton and Sakallah, 2008]) 1 . Motivated

1 Although this paper addresses Boolean formulas, the work can be lifted to more general constraints.

Mikolas Janota

INESC-ID, Portugal mikolas.janota@gmail.com

Anton Belov

CASL/UCD, Ireland anton.belov@ucd.ie

by the seminal work of Reiter [Reiter, 1987], several important results relating MCSes and MUSes have been established [Birnbaum and Lozinskii, 2003; Bailey and Stuckey, 2005; Liffiton and Sakallah, 2008], including the well-known minimal hitting set duality between MCSes and MUSes.

The identification of MCSes finds many practical applications. For example, the MCS with the smallest number of clauses (or smallest weight) represents the solution of the Maximum Satisfiability (MaxSAT) problem. Another example is to enumerate MCSes and use minimal hitting set duality for computing the MUSes of a formula (e.g. [Bailey and Stuckey, 2005; Liffiton and Sakallah, 2008]). One additional example is the computation of minimal models (e.g. [BenEliyahu and Dechter, 1996; Soh and Inoue, 2010]). This paper shows that MCSes can also be used for effectively approximating the solution of the MaxSAT problem.

Different approaches have been proposed over the years for computing MCSes. Earlier work proposed modifications to the basic Boolean Satisfiability (SAT) DPLL algorithm [Birnbaum and Lozinskii, 2003]. This work was later shown to be inefficient in practice when compared with an approach based on MaxSAT [Liffiton and Sakallah, 2008]. A different solution consists of iteratively calling a SAT solver [Bailey and Stuckey, 2005]. Results in [Liffiton and Sakallah, 2008] indicate that the MaxSAT approach is more efficient. However, recent work [N¨ohrer et al., 2012] proposes important optimizations. An alternative approach was recently developed in the context of model-based diagnosis [Felfernig et al., 2012]. This recent algorithm, FASTDIAG, adapts the QUICKXPLAIN algorithm [Junker, 2004] for finding MUSes. Finally, MCSes can also be computed with SAT with preferences, e.g. [Rosa et al., 2010]. As the experimental results in this paper show, although acceptably efficient for MCS enumeration, existing MCS computation algorithms can be fairly inefficient when computing single MCSes for harder instances. A single MCS can, for example, be used for approximating the solution for very hard instances of MaxSAT, i.e. instances for which tight upper bounds (on the cost of falsified clauses) are currently unknown. In these cases, existing algorithms for computing MCSes are ineffective.

This paper develops new techniques for improving recent MCS computation algorithms [Bailey and Stuckey, 2005; N¨ohrer et al., 2012; Felfernig et al., 2012]. Moreover, the paper develops a new algorithm for computing MCSes that is inspired by the work of [Birnbaum and Lozinskii, 2003]. This new algorithm also exploits the proposed novel techniques. The paper conducts an extensive experimental evaluation, organized according to three different scenarios. The first scenario evaluates raw performance when computing a single MCS. The second scenario evaluates how each algorithm performs when enumerating all MCSes. To conclude, the third scenario evaluates the enumeration of MCSes (within a time bound) to approximate MaxSAT. The experimental results demonstrate that the new algorithms significantly outperform the existing state of the art in several ways. First, the new algorithms allow computing MCSes for problem instances for which existing approaches are unable to. Second, the new algorithms are capable of enumerating all the MCSes for problem instances for which existing approaches are unable to. Finally, the new algorithms are shown to consistently outperform incomplete algorithms for MaxSAT, providing better quality bounds than what had been achieved until now.

The paper is organized as follows. Section 2 introduces the definitions used throughout the paper. A brief overview of algorithms for computing MCSes is provided in Section 3. Sections 4 and 5 present the main contributions of the paper. The experimental evaluation is presented in Section 6. The paper concludes in Section 7.

2 Preliminaries

Standard definitions for propositional logic are assumed (e.g. [Biere et al., 2009]). Formulas are defined over a set of Boolean variables X = {x1, . . . , xn}, and are represented in Conjunctive Normal Form (CNF). A CNF formula is a conjunction of disjunctions of literals (clauses), and a literal is either a variable or its negation. A CNF formula can also be interpreted as a set of sets of literals. Both representations are used interchangeably. CNF formulas are denoted by letters with calligraphic fonts, e.g. F, S, U, C, T , etc. When necessary, subscripts are used. Clauses are represented by c or ci, i = 1, . . . ,m, where m = |F|. For a formula T and a range i..j, where T is viewed as a sequence 〈c1, c2, . . . , c|T |〉, Ti..j denotes the clauses in the range i..j, i.e. {ci, ci+1, . . . , cj} for j ≥ i, or ∅ if j < i.

A truth assignment is a mapping µ : X → {0, 1}. In this paper assignments are always complete, i.e. the mapping is total. Assignments are extended to clauses and to formulas, where the valuation of a clause (or a formula) is obtained by standard logic operations. Thus, µ(c) and µ(F) denote, respectively, the valuation of clause c and of formula F.

The algorithms described in the paper use extensively SAT solver calls. These can be viewed as calls to a SAT oracle that can return more information than the standard true/false outcome. A SAT solver call is denoted by (st, µ, V) ← SAT(F), where st denotes the outcome (i.e. true or false) and the remaining (optional) arguments denote, respectively, the computed model (if the outcome is true) and the computed unsatisfiable subformula (if the outcome is false).

The following definitions serve to characterize unsatisfi-

Function BLS(F) Global: none 1 (S, U) ← InitialAssignment(F) 2 foreach c ∈ U do 3 if SAT(S ∪ {c}) then S ← S ∪ {c} 4 5 return F \ S // MCS of F

able subformulas, and are used throughout.

Definition 1 M ⊆ F is a Minimally Unsatisfiable Subset (MUS) of F iff M is unsatisfiable and ∀c ∈M,M\ {c} is satisfiable.

Definition 2 C ⊆ F is a Minimal Correction Subset (MCS) iff F\C is satisfiable and ∀c ∈ C, F\(C\{c}) is unsatisfiable.

Definition 3 S ⊆ F is a Maximal Satisfiable Subset (MSS) iff S is satisfiable and ∀c ∈ F \ S, F ∪ {c} is unsatisfiable.

It is well-known that for an MCS C, F \ C denotes an MSS of F (e.g. [Liffiton and Sakallah, 2008]). Given a formula F, an unsatisfiable subformula (or core) [Zhang and Malik, 2003] of F is any subset U of F that is also unsatisfiable. Hence, an unsatisfiable core contains one or more MUSes.

The MaxSAT problem consists of finding an assignment that satisfies the maximum number of clauses of an unsatisfiable formula. Thus, a largest MSS represents a solution to the MaxSAT problem, which can also be represented as the smallest MCS. More general variants of the MaxSAT problem consider hard clauses (that must be satisfied) or weighted clauses (incurring a cost if not satisfied) (e.g. [Li and Many`a, 2009]). The algorithms described in this paper address CNF formulas where all clauses are soft, i.e. can be falsified (or relaxed). However, extensions to the more general case of formulas with hard (or weighted) clauses are immediate, and are highlighted when necessary.

3 RelatedWork

This section overviews work related with (or easily adapted to) computing MCSes of CNF formulas. A review of the large body of related work on model-based diagnosis (e.g. [Reiter, 1987] or, for recent references [Felfernig et al., 2012]) is omitted due to space constraints. In the area of constraints, the analysis of over-constrained problems (with soft constraints) is often associated with solving MaxCSP (e.g. [Jampel et al., 1996; Meseguer et al., 2003; 2006; van Hoeve, 2011]).

A simple approach for computing one MCS consists of a (linear) search through the clauses of the formula [Bailey and Stuckey, 2005]. This approach corresponds to Algorithm 1, where line 1 is replaced by the assignment U ← F. An immediate improvement is to start from an assignment that (preferably) falsifies as few clauses as possible [N¨ohrer et al., 2012]. This is illustrated by line 1 in Algorithm 1. Another improvement consists of adding to S all clauses satisfied at each SAT solver call [N¨ohrer et al., 2012]. This improvement is analyzed in greater detail in Section 4. In the worst case, linear search requires O(m) calls to a SAT solver. Observe that the extension to partial MaxSAT is easily achieved

Function BFD(R, T ⊆ R, hasD) Global: none 1 if hasD ∧ SAT(R) then return ∅ 2 3 if |T | = 1 then return T 4 5 m← ⌊ |T | 2 ⌋ 6 (T1, T2) ← (T1..m, Tm+1..|T |) 7 D2 ← BFD(R\ T1, T2, T1 ̸= ∅) 8 D1 ← BFD(R\ D2, T1,D2 ̸= ∅) 9 return D1 ∪ D2 // Clauses of MCS

by requiring the hard clauses to be included in set S initially. Thus, line 1 in Algorithm 1 involves a SAT solver call to guarantee that the hard clauses are satisfied. A similar solution is used in all algorithms described in the following sections. Moreover, enumeration of MCSes is implemented by blocking each computed MCS, with a hard clause that disables repeating the same MCS. This hard clause is defined as the disjunction of all the literals in the clauses of the MCS (see Section 5 for a justification). The same approach is assumed in all of the MCS algorithms described in this paper.

MaxSAT [Liffiton and Sakallah, 2008] represents the most widely used approach for computing MCSes, e.g. for MUS enumeration. In this approach, a new relaxation variable is added to each clause. These variables are then used for iteratively reducing the cost of the relaxation variables assigned value 1 (i.e. that relax clauses). This procedure terminates when the cost of the relaxation variables assigned value 1 cannot be further reduced. This represents a MaxSAT solution, and so it is an MCS of the original formula. Recent improvements to MaxSAT-based MCS enumeration are reported in [Morgado et al., 2012]. Despite very good results for MCS enumeration, the use of MaxSAT for computing MCSes has a few drawbacks. For example, since this approach requires solvingMaxSAT, it is inadequate for approximating the solution of hard MaxSAT instances.

Recent work in model-based diagnosis proposed the FASTDIAG algorithm [Felfernig et al., 2012]. This algorithm mimics the well-known QUICKXPLAIN algorithm [Junker, 2004]. However, whereas QUICKXPLAIN computes explanations, FASTDIAG computes diagnoses (or relaxations). Algorithm 2 details the organization of FASTDIAG. The algorithm accepts three arguments. The first argument is a set of clauses one aims to maximally satisfy, i.e. the reference set. The second argument represents the clauses that can be extracted when attempting to satisfy the clauses in the first argument, i.e. the target set. Finally, the third argument indicates whether a valid correction set already exists. If it does, then the clauses in the reference set can be checked for satisfiability. For plain MaxSAT, Algorithm 2 is initially called with sets R and T corresponding to all clauses in the formula. In contrast, for partial MaxSAT, the algorithm is initially called with set R corresponding to both the hard and soft clauses of the formula, and set T corresponding solely to the soft clauses. A similar solution is used in any the variant of the BFD algorithm described in the following sections.

Function DISJOINTUNSATISFIABLECORES(F) Output: µ: Assignment; F: Subformula; U: Disjoint cores 1 (U, st ) ← (∅, false) 2 while not st do 3 (st , µ, V) ← SAT(F) 4 if not st then 5 F ←F \ V 6 U ← U ∪ {V} 7 return (µ, F, U)

This algorithm has the same complexity as QUICKXPLAIN. If k is the size of the largest MCS, then the algorithm requires O(k+k log mk ) calls to a SAT solver in the worst case, where m = |F|. If the largest MCS is much smaller than the original formula (and often it is), then FASTDIAG can be expected to outperform linear search.

Approaches for computing MCSes that do not use repeated calls to a SAT solver are either based on modifying the DPLL SAT solver [Birnbaum and Lozinskii, 2003], or by adapting a CDCL SAT solver for implementing SAT with preferences [Rosa et al., 2010]. The work in [Birnbaum and Lozinskii, 2003] requires a fixed order of the variables, and standard SAT techniques cannot be used. These approaches were shown to be quite inefficient in [Liffiton and Sakallah, 2008]. The results in Section 6 show that the use of SAT with preferences is also ineffective in practice.

4 NewMCS Techniques

This section develops three techniques that serve to reduce the number of calls to a SAT solver and to simplify each call. The first one is based on finding a disjoint set of unsatisfiable cores. The second one exploits backbone literals (e.g. [Kilby et al., 2005]. Finally, the third one exploits clauses satisfied by satisfying assignments. The third technique is used in the recently proposed PICOMCS algorithm [N¨ohrer et al., 2012]. However, we show that the technique can be used with other algorithms for computing MCSes.

Algorithm 3 shows how a set of disjoint unsatisfiable cores can be computed. The following result is used when exploiting disjoint unsatisfiable cores for computing MCSes.

Proposition 1 Let F be unsatisfiable, and let P denote a partition of F as follows, P = {G, C1, . . . Cr}, where each Ci, i = 1, . . . , r is an unsatisfiable core of F. Then, r represents a lower bound on the size of any MCS of F.

Proof. Since P is a partition of F, the unsatisfiable cores are disjoint. Given any unsatisfiable core Ci, any MCS M of F must include at least one clause from each Ci, as otherwise Ci ⊆ F \ M, and so F \ M⊨⊥. Therefore, an MCS of F must include at least r clauses, and so r denotes a lower bound on the size of any MCS of F. ✷

Consider an unsatisfiable formula F and an assignment µ. Then µ induces a partition of F, {S, U}, where S denotes the satisfied clauses and U denotes the falsified clauses. Thus,

Proposition 2 There exist an MSS W and an MCS M of F such that S ⊆ W and U ⊇ M.

If F is partitioned into {G, C1, . . . , Cr}, such that G is satisfiable, and C1, . . . , Cr are disjoint unsatisfiable cores, then any assignment µ that satisfies G partitions each unsatisfiable core Ci into two disjoint sets Si and Ui of satisfied and falsified clauses, respectively. Let S = G ∪ ∪ri=1Si, with S ⊆ F, denote the clauses satisfied by some assignment µ. Clearly, by Proposition 2, S ⊆ W where W is an MSS of F. Set S is to be iteratively updated with additional clauses. Let S q denote the qth update, S ≡ S 0 ⊂ S 1 ⊂ . . . ⊂ S q ⊂ . . . ⊆ W, with the invariant that each set S q is satisfiable, and so represents a subset of an MSS W of F. The set of falsified clauses from unsatisfiable core C1 is U1 (with U1 ̸= ∅, since C1 is unsatisfiable). Next, consider each clause c in U1, taking into account that the clauses in S q must be satisfied. If S q ∪ {c} is satisfiable, then S q+1 = S q ∪ {c}. Otherwise, since S q ∪ {c} ⊨⊥, c must be included in any MCSMof F, such that the MSS W = F \M contains S q . After analyzing all clauses in U1, the clauses not added to some set S q must be included in any MCS M of F such that the MSS W = F \ M contains S q . The process is repeated for each unsatisfiable core, at each step either updating some satisfiable set S q with a clause c, and so S q+1 = S q ∪ {c}, such that S q+1 is satisfiable, or declaring c to be included in an MCS of F. Since any MCS F integrates at least one clause from each unsatisfiable core (Proposition 1), the above process can be terminated when |Ui| = 1, thus saving one SAT solver call. Each unsatisfiable core is said to be corrected locally, since it is analyzed separately. Given the above, disjoint unsatisfiable cores can be used for two purposes. First, to provide a lower bound on the size of any MCS. Second, an MCS can be constructed by correcting locally each unsatisfiable core. More importantly, all the algorithms described in this paper can either work on the complete formula F or on each core.

For enumerating MCSes, Algorithm 3 can be used iteratively, being required to satisfy the blocking clauses that prevent repeated MCSes (see Section 3). After enumerating all the MCSes identified by a set of disjoint unsatisfiable cores, additional disjoint unsatisfiable cores are computed, but previously computed ones are kept. The algorithm terminates when a computed unsatisfiable core is empty. This indicates that all MCSes have been enumerated. Moreover, the approach for using disjoint unsatisfiable cores for computing the next MCS remains unchanged.

The second technique exploits backbone literals [Kilby et al., 2005]. Let M be an MCS of F. Then, by definition of MCS, for any clause c ∈ M, c = (l1 ∨ l2 ∨ . . . ∨ lk), (F \M) ∪ {c}⊨⊥. Hence, F \M⊨¯ c, i.e. for each literal li ∈ c, F \M⊨¬li. Thus, ¬li is a backbone literal of F \M. Let L denote the set of clauses decided to be included in some MCS of F. Then for every MCS M of F such that L ⊆ M, the complements of the literals of each of the clauses of L represent backbone literals of F \M. As a result, any algorithm for MCS computation can exploit backbone literals, by adding the negation of each clause that is decided to be included in a MCS of F.

The third technique consists of exploiting clauses satisfied by models of subsets of F. Let F be split into a subset S of an MSS of F and a superset U of an MCS of F. Any MCS algorithm analyzes the clauses in U. For each such clause c, an

Function EFD(R, T ⊆ R, hasD) Global: S, B, U1, . . . , Ur 1 if hasD then 2 (st , µ) ← SAT(R ∪ S ∪ B) 3 if st then 4 UpdateSatisfiedClauses(µ) 5 return ∅ 6 if |T | = 1 then 7 UpdateBackboneLiterals(T ) 8 return T 9 m← ⌊ |T | 2 ⌋ 10 (T1, T2) ← (T1..m, Tm+1..|T |) 11 D2 ← EFD(R\ T1, T2 \ S, T1 ̸= ∅) 12 D1 ← EFD(R\ D2, T1 \ S,D2 ̸= ∅) 13 return D1 ∪ D2 // Clauses of MCS

MCS algorithm either decides there is an MSS that includes S ∪ {c}, and so c is added to S, or decides that S ∪ {c} is not contained in any MSS, and so c is added to a set L, representing a subset of an MCS of F. Now, suppose a SAT solver is called on S ∪ T , where T ⊆ U, and suppose the SAT solver returns a satisfying assignment µ. Moreover, let V denote a subset of U \ T of clauses satisfied by µ. Then, there must exist an MSS of F that includes S ∪T ∪V. Thus, all clauses in T ∪ V can be added to S. The technique of moving satisfied clauses to set S, and requiring them to continue to be satisfied is used in PICOMCS [N¨ohrer et al., 2012]. Below, we show that the technique can be used both in an enhanced version of FASTDIAG [Felfernig et al., 2012] and in the new MCS computation algorithm (see Section 5).

Algorithm 4 shows an enhanced version of FASTDIAG, EFD, which integrates the new techniques described in this section, and differs somewhat from BFD (see Algorithm 2). The algorithm uses a number of global sets of clauses. Set B contains the unit clauses representing already computed backbone literals, and set S denotes the current subset of an MSS of F. Sets U1, . . . , Ur represent the falsified clauses of each disjoint unsatisfiable core (if being used). Set B is updated each time a clause is added to the MCS (line 7). Set S is updated each time the SAT solver returns satisfiable (line 4). Both sets are used when calling the SAT solver (line 2). Moreover, the number of recursive calls is reduced by filtering the clauses in set S (lines 11 and 12). Finally, as remarked earlier, the handling of disjoint unsatisfiable cores requires no modifications; it suffices to invoke Algorithm 4 on the falsified clauses of each disjoint unsatisfiable core, i.e. Ui, while maintaining the global sets S and B, and aggregating the clauses from each core that cannot be added to S.

5 NewMCS Algorithm

This section develops a new algorithm for computing a single MCS. The algorithm exploits a (simple) observation from [Birnbaum and Lozinskii, 2003] (and used in algorithm AMC1 in [Birnbaum and Lozinskii, 2003]: the clauses falsified by any complete truth assignment do not have complemented literals. This remark forms the basis of Algorithm 5, the clause D based (or CLD) algorithm. Consider a truth as-

Function CLD(i) Input: i: Target unsatisfiable core Global: S, B, U1, . . . , Ur 1 st ← true 2 while st ∧ (|Ui| > 1) do 3 D ← (∨c∈Ui c) 4 (st , µ) ← SAT(S ∪ B ∪ {D}) 5 if st then 6 UpdateSatisfiedClauses(µ) 7 UpdateBackboneLiterals(Ui) 8 return Ui // Clauses of MCS

signment that splits the clauses in F into a set of satisfied clauses S and a set of falsified clauses Ui (assume i = 1, i.e. no disjoint cores considered). Given that the clauses in Ui do not have complemented literals, we can create their disjunction as a new clause D, and call a SAT solver on S ∪ {D}. If this formula is satisfiable, that means it is possible to satisfy at least one clause from Ui while satisfying all the clauses in S. Thus, S does not yet represent an MSS of F and Ui does not yet represent an MCS of F. In this case, the sets S and Ui are updated by removing from set Ui the satisfied clauses and moving them to set S. However, if the formula S∪{D} is unsatisfiable, then no additional clauses from Ui can be satisfied given S. Thus, S represents an MSS of F, and Ui represents an MCS of F (observe that disjoint cores are not being considered). Similarly to algorithm EFD, algorithm CLD integrates the techniques described in Section 4. The global sets S and B capture, respectively, satisfied clauses and backbones. These are updated the same way as in EFD. Moreover, CLD can also be readily used with disjoint unsatisfiable cores. Instead of considering a single set U of falsified clauses, Algorithm 5 is called for each set of falsified clauses associated with each unsatisfiable core, i.e. Ui. In the case no disjoint unsatisfiable cores are used, then the CLD can be started by first creating sets S and U (see line 1 in Algorithm 1).

If p is the size of the smallest MCS of F, then Algorithm 5 requires m-p+1 calls to a SAT solver, where m = |F|. This complexity result suggests that Algorithm 5 operates quite differently from both the linear search algorithm and FASTDIAG. This observation is substantiated by the results in Section 6. A possible downside is that the disjunction clause D may result in instances of SAT that are harder than for the other algorithms.

6 Experimental Evaluation

The algorithms proposed in this paper were implemented in the MCSLS tool 2 for MCS computation and enumeration. MCSLS is written in C++ and integrates Minisat 2.2 [E´en and S¨orensson, 2003] as the (incremental) SAT solver. The following algorithms have been implemented in MCSLS: BLS (Alg. 1); enhanced linear search, ELS (Alg. 1 with the techniques proposed in Section 4); CLD (Alg. 5 using disjoint unsatisfiable cores); BFD (Alg. 2); and EFD (Alg. 4 using disjoint unsatisfiable cores). All algorithms accept formulas with soft and (optionally) hard clauses. Thus, formulas are either considered plain MaxSAT or partial MaxSAT. Besides these algorithms, we also developed CAMUS2, an implementation of CAMUS that is able to solve partial MaxSAT instances. The following existing tools were included in the experiments: CAMUS [Liffiton and Sakallah, 2008; 2009], PICOMCS [N¨ohrer et al., 2012], NOPTSAT [Rosa et al., 2010], and HYCAM (only for enumeration) [Gr´egoire et al., 2007]. Most of the tools require formulas without hard clauses (i.e. plain CNF format), and so their evaluation is restricted to these formulas. All experiments were run on a Linux cluster, with a memory limit of 4GB for each process. The time limit was set depending on the experiment, as explained below. The problem instances used include a selection of smallsized industrial instances used in the SAT competitions (assuming all clauses are soft), and a selection of structured instances from MaxSAT evaluations (representing plain and partial MaxSAT instances). Additionally, instances representing the minimal model problem [Ben-Eliyahu and Dechter, 1996] were generated from satisfiable industrial instances. The resulting partial MaxSAT formulas are challenging for current MCS algorithms.

2 Available from http://logos.ucd.ie/wiki/doku.php?id=mcsls.

Three experiments were carried out. The first one evaluates the existing and the new MCS algorithms on computing a single MCS. The second experiment evaluates these algorithms on enumerating all MCSes. The set of instances differs from the first experiment, since these need to be simpler. The final experiment compares one of the new algorithms with incomplete MaxSAT solvers, with the objective of evaluating the effectiveness of approximating MaxSAT solutions.

1 MCS. This experiment evaluates the raw performance for computing a single MCS. Preliminary experiments were executed to select instances (a total of 866) for which computing a single MCS was difficult (i.e. time consuming or not possible at all) for at least one of the tools. Table 1 shows the total number of instances for which each algorithm was able to compute one MCS within a time limit of 30 minutes. Existing tools (CAMUS/CAMUS2, PICOMCS and NOPTSAT) do not match the performance of the best performing tools, i.e. ELS, EFD and CLD. CLD is the best performing algorithm, being able to solve 8 more instances than the second best, ELS. The cactus plot in Figure 1 shows the running times for the best performing algorithms. Note that the running times for ELS, EFD and CLD are similar for most instances, with the exception of less than 20 instances. Both BLS and BFD perform significantly worse than their respective enhanced versions. BLS is orders of magnitude slower than ELS. As a result, it is not shown in Figure 1. BFD is significantly slower than EFD, in most cases by more than a factor of 2. These results indicate that the new techniques are paramount for improving the performance of MCS algorithms. The cactus plot also shows a VBS (Virtual Best Solver) that includes ELS, EFD and CLD. The performance gains of the VBS compared to the other algorithms is quite significant; it confirms that these algorithms complement each other, and motivates investigating portfolio solutions for computing MCSes.

MCS enumeration. This experiment evaluates the performance of the different algorithms for enumerating all MCSes. Preliminary experiments were executed to select a set of 775 problem instances, simpler than for one MCS. Enumeration of all MCSes was possible for around 50% of the instances with at least one of the approaches. Table 2 shows the total number of instances for which each algorithm was able to compute all MCSes within a time limit of 60 minutes. As can be observed, for the plain MaxSAT case, NOPTSAT performs significantly worse than the other approaches. The new algorithms have a slight performance edge over PICOMCS. The cactus plot in Figure 2 shows the running times for the best performing algorithms. Among these, CLD, BLS and ELS are the most efficient. BLS and ELS can solve 5 and 10 more instances than CLD, respectively. However, CLD is substantially faster for most instances. For 440 instances, CLD clearly outperforms the other approaches. This behavior is highlighted in the scatter plot of Figure 3 which compares the running times of CLD against ELS, and shows performance gains that in some cases exceed an order magnitude. The performance gap between CLD and the remaining algorithms is even larger. The cactus plot also shows a VBS of the same set of algorithms as above. Although not as significant as for the single MCS case, the performance gains also justify a portfolio approach.

One of the benchmark suites considered in this experiment is DC [Sinz et al., 2003]. This suite consists of 84 instances from an automotive product configuration problem, and has been extensively studied in recent work on MCS/MUS enumeration [Liffiton and Sakallah, 2008; 2009]. For the DC benchmark suite, CLD is able to solve 51 instances, whereas the remaining approaches solve 49, and NOPTSAT solves 37. The two instances first solved by CLD correspond to C210 FW SZ 128 (284429 MCSes) and C210 FS SZ 103 (347685 MCSes).

MaxSAT Approximation. This experiment evaluates the enumeration of MCSes (within a time bound) to approximate MaxSAT. In some scenarios, it is necessary to quickly get a good quality solution for the MaxSAT problem, rather than waiting for a complete method to find the optimum solution. The size of the smallest computed MCS (within a given time limit) corresponds to a (non-optimal) MaxSAT solution which is compared to the solutions computed by SAT4J [Le Berre and Parrain, 2010] and IROTS [Tompkins and Hoos, 2004], two approximation tools submitted to the MaxSAT Evaluation 2012 3 . SAT4J is a complete method based on iteratively calling a SAT solver and refining an upper bound. IROTS is an stochastic local search algorithm for MaxSAT.

For this experiment, the CLD algorithm was selected among the best performing algorithms for computing 1 MCS and for MCS enumeration. Nevertheless, any of the other proposed algorithms could be have been considered. In this experiment CLD was executed in enumeration mode and the size of the smallest MCS computed within the time limit corresponds to a (non-optimal) MaxSAT solution. CLD, SAT4J and IROTS were executed with a time limit of 120 seconds. Similar results were obtained for other time limits.

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

The 866 problem instances used for computing a single MCS were used in this experiment. Of these, SAT4J can find the optimum within the time limit for 306 instances. Since the optimum can be found within a small timeout, these instances are discarded. The results for the remaining 560 instances are summarized in Table 3. The first column shows which two solvers are being compared (CLD vs SAT4J, and CLD vs IROTS). The following columns consider the subsets of instances: (i) for which both SAT4J and IROTS can produce a valid upper bound within the time limit; (ii) for which only SAT4J (or (iii) only IROTS) produces a valid upper bound; and finally (iv) for which neither SAT4J nor IROTS can produce a valid upper bound (column ∅). Note that IROTS can return assignments that do not satisfy all hard clauses. These assignments are discarded as invalid upper bounds. The table shows how many times the MaxSAT approximation computed by CLD is better (W=win), is the same (D=draw) or is worse (L=loss) against the approximation computed by either SAT4J or IROTS. The last row shows the number of instances for which CLD times out without producing an approximation. The results indicate that CLD produces more accurate approximations in 6.09 (2.36) times more cases than SAT4J (IROTS). Thus, we conclude that CLD provides quite competitive approximations. It should be noted that CLD and the remaining MCS enumerators rely on calling a SAT solver, and for some instances it may not find any MCS within the time limit (as shown in Table 3, CLD times out for 74 instances). However, SAT4J and (IROTS) time out on even more instances, 219+68

and 115+68, respectively. Finally, it should be pointed out that a more detailed analysis of the actual quality of the computed MaxSAT approximations is harder to do, since these are instance-dependent.

7 Conclusions

This paper studies the problem of computing minimal correction subsets of unsatisfiable CNF formulas, and makes the following main contributions. First, the paper proposes novel techniques for improving the performance of MCS computation algorithms. These include exploiting disjoint unsatisfiable cores and backbone literals. Second, the paper shows how these techniques can be integrated into existing MCS computation algorithms. Third, and finally, the paper develops a novel algorithm for computing MCSes. The experimental results indicate that the new techniques and algorithms significantly improve over existing algorithms, solving instances that could not be solved before, both for computing a single MCS and for enumerating MCSes. More importantly, the paper shows that the new algorithms for computing MCSes are effective at approximating the solution of (partial) MaxSAT instances. The experimental results indicate that, given a fixed timeout, computing MCSes provides better quality bounds than other incomplete approaches [Tompkins and Hoos, 2004; Le Berre and Parrain, 2010].

Future research work will address further improvements to the new algorithms, including selecting the algorithm to use depending on the size of each target unsatisfiable core. Motivated by the results of the VBS, that solely integrates the algorithms proposed in this paper, additional work includes developing a portfolio approach [Xu et al., 2008; Kadioglu et al., 2011] based on the new MCS algorithms. Another line of work is to exploit recently proposed algorithms for the minimal set over monotone predicate (MSMP) problem, and their specialization for MCSes [Marques-Silva et al., 2013]. Finally, one additional line of work is the integration of the new algorithms for computing MCSes in recent approaches for partial MUS enumeration [Previti and Marques-Silva, 2013; Liffiton and Malik, 2013].

Acknowledgements.

The authors would like to thank the anonymous reviewers for the insightful comments. This work is partially supported by the SFI PI grant BEACON (09/IN.1/I2618), by the FCT grants ATTEST (CMU-PT/ELE/0009/2009) and POLARIS (PTDC/EIA-CCO/123051/2010), and by INESC-ID multiannual funding from the PIDDAC program funds.