Literal-Based MCS Extraction

1 Introduction

For over-constrained systems [Jampel et al., 1996], i.e. sets of inconsistent constraints, a Maximal Satisfiable Subset (MSS) denotes a maximal set of constraints that are consistent. A Minimal Correction Subset (MCS, or co-MSS) is the complement of an MSS, i.e. it is a set-wise minimal set of constraints whose removal renders the system consistent. MSSes/MCSes find an ever increasing number of practical applications, representing an essential tool in the analysis of over-constrained systems [Junker, 2004; Felfernig et al., 2012]. One concrete example is Maximum Satisfiability (MaxSAT), since a maximum set of satisfiable constraints is the largest MSS (and so corresponds to the smallest MCS). MCSes are also related with Minimal Unsatisfiable Subsets (MUSes), by a well-known minimal hitting set duality property [Reiter, 1987]. Thus, enumeration of MCSes often serves for computing the MUSes of an over-constrained system. Additional application domains include the computation of minimal models [Ben-Eliyahu and Dechter, 1996] and interactive constraint satisfaction and configuration [O'Callaghan et al., 2005], among many others.

∗We are grateful to Marijn Heule for his feedback. This work is partially supported by SFI PI grant BEACON (09/IN.1/I2618), by FCT grant POLARIS (PTDC/EIA-CCO/123051/2010), and by national funds through FCT with reference UID/CEC/50021/2013.

A number of MCS extraction and enumeration algorithms have been proposed in recent years [O'Callaghan et al., 2005; Bailey and Stuckey, 2005; Liffiton and Sakallah, 2008; Felfernig et al., 2012; N¨ohrer et al., 2012; Marques-Silva et al., 2013a; Gr´egoire et al., 2014; Bacchus et al., 2014], resulting in ever more efficient algorithms, capable of solving increasingly more challenging problem instances. The number and significance of applications of MCS extraction and enumeration motivates investigating more efficient algorithms.

This paper builds on recent work in the domain of Boolean satisfiability [Marques-Silva et al., 2013a; Gr´egoire et al., 2014; Bacchus et al., 2014], and proposes a finer-grained view of the MCS extraction problem, by reasoning in terms of literals instead of clauses. This alternative view, inspired by a fundamental relationship between MCSes and backbones of propositional formulas, enables for developing a novel MCS extraction algorithm, whose query complexity can be characterized in terms of the number of variables in the formula.

Moreover, recent work has shown that restricted enumeration of MCSes is effective at approximating MaxSAT. This paper extends this earlier work, by developing a set of new techniques which enable far better approximation quality.

Experimental results, obtained on representative problem instances, demonstrate that the new MCS extraction algorithm consistently outperforms the approaches that currently represent the state of the art. In addition, the results confirm that MaxSAT approximation by restricted MCS enumeration can provide high-quality solutions within short run times.

The paper is organized as follows. Section 2 introduces the notation and the definitions used in the paper. Section 3 provides a brief account of earlier work. The novel MCS extraction algorithm is detailed in Section 4, and the new techniques for approximating MaxSAT are described in Section 5. Section 6 is devoted to the experimental study. Section 7 concludes the paper, and identifies research directions.

2 Background

We assume familiarity with propositional logic [Biere et al., 2009] and consider propositional Boolean formulas in Conjunctive Normal Form (CNF). A CNF formula F is defined over a set of Boolean variables X = {x1, ..., xn} as a conjunction of clauses (c1 ∧ ... ∧cm). A clause ci is a disjunction of literals (li1 ∨ ... ∨ liki ) and a literal l is either a variable x or its negation ¬x. We refer to the set of literals appearing in F as L(F). Formulas can be alternatively represented as sets of clauses, and clauses as sets of literals. Occasionally, expressions of the form ∨L will be used to indicate a clause made of the literals in a set L.

A truth assignment, or interpretation, is a mapping µ : X → {0, 1}. If all the variables in X are assigned a truth value, µ is referred to as a complete assignment. Interpretations can be also seen as conjunctions or sets of literals. Truth valuations are lifted to clauses and formulas as follows: µ satisfies a clause c if it contains at least one of its literals, whereas µ falsifies c if it contains the complements of all its literals. Given a formula F, µ satisfies F (written µ⊨F) if it satisfies all its clauses, being µ referred to as a model of F.

Given two formulas F and G, F entails G (written F ⊨G) iff all the models of F are also models of G. F and G are equivalent (written F ≡ G) iff F ⊨G and G ⊨F.

A formula F is satisfiable (F ̸ ⊨⊥) if there exists a model for it. Otherwise it is unsatisfiable (F ⊨⊥). SAT is the decision problem of determining the satisfiability of a propositional formula. This problem is NP-complete [Cook, 1971].

An important function problem is computing the backbone of F [Monasson et al., 1999; Kilby et al., 2005], defined as the set of literals appearing in all its models.

Definition 1 The backbone B(F) ⊆ L(F) of F is the set of all literals l such that F ⊨ l.

A number of algorithms have been proposed for computing backbones [Janota et al., 2015].

Given an unsatisfiable formula F, the following subsets represent different notions regarding (set-wise) minimal unsatisfiability and maximal satisfiability [Liffiton and Sakallah, 2008; Marques-Silva et al., 2013a]:

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

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

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

Note that an MSS is the complement of an MCS. MUSes and MCSes are closely related by the well-known hitting set duality [Reiter, 1987; Bailey and Stuckey, 2005; Birnbaum and Lozinskii, 2003; Slaney, 2014]: Every MCS (MUS) is an irreducible hitting set of all MUSes (MCSes) of the formula. In the worst case, there can be an exponential number of MUSes and MCSes [Liffiton and Sakallah, 2008; O'Sullivan et al., 2007]. Besides, MCSes are related to the MaxSAT problem, which consists in finding an assignment satisfying as many clauses as possible. The smallest MCS (largest MSS) represents an optimal solution to MaxSAT.

Formulas may be partitioned into sets of hard and soft clauses, i.e., F = {FH,FS}. Hard clauses must be satisfied, while soft clauses can be relaxed if necessary. Thus, an MCS will be a subset of FS. Clauses may also have (positive integer) weights. These elements define different versions of the MaxSAT problem. It is said partial if FH ̸= ∅ (otherwise it is plain), and weighted if there are weights different from 1. MaxSAT is then the problem of computing an assignment minimizing the weighted sum of the soft clauses it falsifies.

3 RelatedWork

Stemming from the influential work of [Reiter, 1987], computing MCSes has been the subject of a considerable body of research in the fields of model-based diagnosis, constraint satisfaction and Boolean satisfiability.

Most modern methods rely on iteratively making calls to a complete solver to check the satisfiability of different subformulas. In general, these algorithms handle a partition {S, U, C} of F, where S is a satisfiable subformula, C contains clauses proved to be inconsistent with S (i.e. ∀c ∈ C, S ∪ {c}⊨⊥), and U consists of the remaining clauses of F. Usually, a first call to the solver computes a complete assignment µ satisfying FH. This serves to initialize the partition with S (resp. U) containing the clauses satisfied (resp. falsified) by µ, and C as the empty set. Note FH ⊆ S. Eventually, S (C) will be an MSS (MCS) of F and U will become empty.

The simplest algorithm, LINEAR SEARCH [Bailey and Stuckey, 2005], removes one clause c from U at a time and calls the solver on S ∪ {c}. If it is satisfiable c is added to S. Otherwise, it is added to C. Other approaches include DICHOTOMIC SEARCH ([O'Callaghan et al., 2005; Li et al., 2013]), FASTDIAG ([Felfernig et al., 2012]), which mimics the divide-and-conquer QUICKXPLAIN algorithm for MUS extraction [Junker, 2004], or PROGRESSION ([Menc´ıa and Marques-Silva, 2014; Marques-Silva et al., 2013b]).

These algorithms can be enhanced with optimizations, such as exploiting models of satisfiable subformulas ([N¨ohrer et al., 2012]), which consists in moving from U to S all the clauses satisfied by the model obtained after a satisfiable call. Other optimizations are the use of backbone literals and disjoint unsatisfiable cores ([Marques-Silva et al., 2013a]). Some of these techniques are also used by the three best performing algorithms, described below.

Motivated by the work of [Birnbaum and Lozinskii, 2003], the CLAUSED algorithm (CLD) [Marques-Silva et al., 2013a] works differently from the previous methods. It checks whether S can be extended with some clause in U, calling the solver on S ∪ {D}, where D = ∨L(U) is a clause expressing the disjunction of the clauses in U. If it is satisfiable, CLD updates S and U from the computed model and repeats the process until it gets an unsatisfiable call, indicating that the clauses still in U constitute an MCS.

CMP (Computational Method for Partitioning) [Gr´egoire et al., 2014] is a recent algorithm that exploits the fact that an MCS is a minimal hitting set of all MUSes. It iteratively searches for transition clauses, those that belong to all

Table 1: Complexity of MCS extractors: m = |FS| and k (p) is the size of the largest (smallest) MCS of F.

Algorithm Query complexity

MUSes of a given subformula, adding them to the MCS. CMP works with an auxiliary set X ⊆ U such that S ∪ X ⊨⊥ is known. Initially X = U and, repeatedly until U becomes empty, it selects a clause c ∈ X and calls the solver on S ∪ (X \ {c}). If it is satisfiable, S and U are updated exploiting the computed model, c is moved to the MCS C and X is reset to U in order to look for the next transition clause. Otherwise, c is removed from X . Despite its quadratic worstcase complexity, CMP was shown very effective in practice. As other algorithms, CMP is enhanced with optimizations, including some new ones. One of them consists in making a call, in a way similar to CLD, at the beginning of each iteration. This is done by a procedure termed extendSatPart, which checks the satisfiability of S ∪ {∨L(X)}. If it is satisfiable, S is extended with the satisfied clauses and X and U are filtered accordingly. Otherwise, all the clauses in X are moved to C and X is set to U. So, regardless of the outcome of the solver, the extendSatPart procedure removes at least one clause from U. One in every two calls CMP makes to the solver is made inside this procedure, so it requires at most 2 ×m calls. This yields the following new result:

Proposition 1 CMP using the extendSatPart procedure has a query complexity of O(m), with m = |FS|.

Finally, building on previous work on SAT with preferences [Rosa et al., 2010], Relaxation Search (RS) [Bacchus et al., 2014] is a new general algorithm to handle optional clauses that can be used to extract MCSes. It consists in using a modified SAT solver so that preferences in the variable selection heuristic can be expressed. An MCS is computed by making a single call on an alternative satisfiability problem consisting of (i) the hard clauses together with (ii) for each soft clause ci, the clauses resulting from ¬ci ↔ bi, where bi is a fresh Boolean variable. The solver is set to first branch on the bi variables preferring to set them to false, i.e., activating the associated soft clauses. If the set of hard clauses is satisfiable, it will always return a model, an MCS being the soft clauses ci such that its associated variable bi was set to true.

Except for RS, the algorithms presented herein make a worst-case number of calls depending on the number of soft clauses in F, as summarized in Table 1. In contrast, RS requires a dedicated solver, which is called once.

4 Literal-BasedMCS Extraction

This section first investigates the relationship between MCSes and backbones, which enables a novel viewpoint of the MCS extraction problem. Then, it introduces a new algorithm that exploits these results.

4.1 MCSes, MSSes and Backbones

In [Marques-Silva et al., 2013a], the authors introduced a technique termed backbone literals. This technique was derived from the observation that, whenever a clause c is proven to belong to the MCS being extracted, i.e. S ∪ {c}⊨⊥, the complements of its literals are backbone literals of all the MSSes containing S. Backbone literals can then be added to the working formula as unit clauses, so that each future call to the SAT solver is expected to be easier.

A deeper analysis reveals a closer relationship between the backbone of an MSS and its corresponding MCS. This is illustrated in the following result.

Proposition 2 Let S ⊂ F be an MSS of F, C = F \ S an MCS and c ∈ F. Then, c ∈ C if and only if B(S) falsifies c.

Proof. Both parts are proved by contradiction.

(If ). Suppose c /∈ C. Then c ∈ S and so S ≡ S ∪ {c}. As B(S) falsifies c, ∀l ∈ c, ¬l ∈ B(S), so ∀l ∈ c, S ⊨¬l, and thus S ∪ {c} ⊨⊥, contradicting the satisfiability of S.

(Only if ). Suppose c ∈ C is not falsified by B(S). Then there exists a literal l ∈ c such that ¬l ̸∈ B(S), that is, S ⊭¬l. So, there exists an assignment µ such that µ⊨S ∪ {l}, so µ⊨S ∪ {c} holds, contradicting the maximality (resp. minimality) of S (resp. C). ✷

Proposition 2 suggests the possibility to compute an MCS by identifying the subset of the backbone literals of the MSS that falsifies the MCS. The next results will be useful to compute these backbone literals and the MSS at the same time.

Proposition 3 Let S ′ ⊆ S, where S is an MSS of F. Then B(S ′ ) ⊆ B(S).

Proof. Let l ∈ B(S ′ ), i.e. S ′ ⊨ l. As S ′ ⊆ S, due to monotonicity of logical entailment, S ⊨S ′ ⊨ l. So l ∈ B(S). ✷

Proposition 4 Let B ⊆ B(S ′ ), with S ′ ⊆ S and S an MSS of F. If c ∈ F \ S ′ is falsified by B, then c belongs to the MCS C = F \ S.

Proof. Firstly, by Proposition 3, B ⊆ B(S). Then as B falsifies c, B(S) falsifies c, so by Proposition 2, c ∈ C. ✷

4.2 LBX: ANewMCS Extraction Algorithm

The results above allow us to devise a new MCS extraction algorithm that iterates over the literals of F searching for backbone literals of subsequent satisfiable subformulas. This method, termed Literal-Based eXtractor (LBX), is depicted in Algorithm 1. Besides the sets of clauses S and U, it works with two sets of literals: L, containing candidates to be tested, and B, with those known to belong to B(S).

Similarly to previous approaches, LBX first initializes the partition {S, U} from a complete assignment. As the MCS will not contain any clause in S, it suffices to test the literals in U, and so L is initialized with L(U). Then, LBX enters a loop where a literal l is selected and removed from L at a time and the solver is called on S ∪ B ∪ {l}. Note that adding B

does not alter the outcome, but has the potential of easing the SAT problem. If it is satisfiable, S and U are updated from the computed model and all the literals that are no longer in U are filtered out from L. Otherwise, ¬l is added to B as a backbone literal. LBX terminates when L becomes empty, returning the MCS F \ S.

LBX can exploit the structure of the formula by selecting the literal l ∈ L having most occurrences in U, so that, if the call is satisfiable, more clauses could be expected to be removed from U, reducing L to a greater extent. Regardless of this choice, LBX is guaranteed to return an MCS within a number of calls bounded by the number of variables.

Proposition 5 LBX always returns an MCS of F and has a query complexity given by O(|X|).

Proof. (Sketch)

(Termination and Complexity). As, initially, F is split from a complete assignment, |L| ≤ |X|. Then, at each iteration, at least one literal is removed from L. Hence, LBX always terminates making no more than |X| + 1 satisfiability tests. (Correctness). We show that, upon termination, S constitutes an MSS of F. To this aim, it suffices to note that at the beginning of every iteration the following invariant holds: S is a satisfiable subformula, U = F \ S and for all l ∈ L(U) \ L, ¬l ∈ B. Eventually, L = ∅ and so, for all l ∈ L(U), ¬l ∈ B. Therefore, B ⊆ B(S) falsifies every c ∈ U. Thus, by Proposition 4, U is contained in all the MCSes not containing any clause in S. Since U = F \ S, it is minimal and constitutes an MCS, and so S an MSS of F. ✷

LBX admits some further refinements. First, as F is unsatisfiable, there are situations where some backbone literals can be detected without making a call to the SAT solver. This happens at any step of the algorithm where B does not falsify yet any clause in F and there exists a literal l that is included in all the clauses of U. Then, we can add ¬l to B. This is a direct consequence of the following more general property.

Proposition 6 Let S ⊂ F be a satisfiable subformula, and X ⊆ F \ S such that S ∪X ⊨⊥. If there exists l ∈ L(X) s.t. l ∈ c for all c ∈ X, then ¬l ∈ B(S).

Proof. Suppose ¬l ̸∈ B(S). Then S ∪ l ⊭⊥ and, since l belongs to all the clauses in X , S∪X ⊭⊥, a contradiction. ✷

On the other hand, LBX can also incorporate an optimization similar to the extendSatPart procedure used in CMP. This consists in issuing, at the beginning of each iteration, a call on S∪B∪{∨L}. If it is satisfiable, S, U and L are updated exploiting the model as before. Otherwise, it means that the complements of all the literals in L are backbone literals of S, thus L becomes empty, leading LBX to termination. It can be easily proved that this call changes neither the correctness, not the query complexity result from Proposition 5, as every call results in at least one literal being removed from L . Furthermore, a similar reasoning that led to Proposition 1, reveals that using this technique introduces an independent new upper bound on the number of calls LBX would need to perform, which allows us to conclude that it has a query complexity of O(min{m, |X|}), with m = |FS|.

Function LBX(F) (S, U) ← InitialAssignment(F) (L, B) ← (L(U), ∅) while L ̸= ∅ do l ← RemoveLiteral(L) (st, µ) = SAT(S ∪ B ∪ {l}) if st then (S, U) ← UpdateSatClauses(µ, S, U) L ← L ∩ L(U ) else B ← B ∪ {¬l} return F \ S // MCS of F Algorithm 1: Literal-Based eXtractor (LBX)

Finally, it is worth mentioning that LBX presents an important advantage from a technical point of view. Literals can be tested using assumptions, so an incremental SAT solver can be interfaced without the need of creating fresh Boolean variables as clause selectors. This may result in a more effective use of propagation and clause learning.

5 MaxSAT Approximation

Enumerating MCSes represents a promising way of approximating MaxSAT [Marques-Silva et al., 2013a]. Arguably, an MCS constitutes a form of local optimal solution, as it is not possible to satisfy any of its clauses without falsifying at least one contained in the respective MSS. So, the average quality of the solutions associated to MCSes can be expected to be higher than that of just random assignments satisfying FH. MCS enumeration is done by iteratively running an MCS extraction algorithm over F, which is augmented with the hard clause ∨L(C) after computing the MCS C. This way, C is blocked, preventing the algorithm from finding it again. The process is repeated until FH ⊨⊥, meaning that all the MCSes have been enumerated, and the best solution found, corresponding to a cost-min MCS, represents a proven optimum.

This section presents three techniques for improving MCSbased MaxSAT approximation. These introduce a heuristic component for making a selective enumeration of MCSes and avoid the computation of some MCSes that cannot improve the current best solution. Here, w(c) denotes the weight of the clause c, w(X) the sum of the weights of the clauses in X and UB the cost of the best solution found so far.

Literal Selection Heuristic

LBX makes a series of non-deterministic choices regarding the literal in L it selects at each iteration. The first technique defines a selection policy aimed at biasing the process towards MCSes with small costs. For this purpose, it selects the literal resulting from the expression argmax{∑(l∈c;c∈U) w(c); l ∈ L}, i.e. for each literal it computes an aggregated weight as the sum of the weights of the clauses in U it appears in, selecting that with the maximum value. Ties are broken arbitrarily. Note that in the case of unweighted formulas, the selected literal would be the one with most occurrences in U. This technique contributes moderately to guiding the search, as LBX exploits models adding the satisfied clauses to the MSS under construction. However, deactivating this feature would deteriorate its performance, and so its ability to enumerate a large number of MCSes in a short time. The next technique aims to achieve a proper balance to this respect.

Stratified MCS Extraction

The second technique exploits the fact that MCSes can be computed in a recursive manner by initially splitting the set of soft clauses as FS = {FS1 , ..., FSk }. Then, C = ∪(i=1..k)Ci is an MCS of F, where C1 is an MCS of FH ∪ FS1 and, for i = 2..k, Ci is an MCS of FH ∪∪(j=1..i-1)(FSj \ Cj) ∪FSi . This result can be exploited to establish preferences regarding the kind of MCSes to be computed first. Motivated by the work of [Ans´otegui et al., 2012], we define the partition so that clauses with the same weight are included in the same subset, and subsets with largest weights are processed first in the MCS extraction process. This way, the MCS extractor is forced to try to first satisfy clauses with larger weights, as no clause in a subset is considered until all the preceding subsets have been completely processed.

Search Space Pruning

The third technique stems from the observation that we can avoid the enumeration of some MCSes without losing the possibility of finding an optimal solution to MaxSAT. This is a direct consequence of the following result:

Proposition 7 Let C be an MCS of F and C ′ ⊆ C a subset s.t. w(C ′ ) ≥ UB. Adding to FH the clause ∨L(C′ ) (blocking C ′ ) does not prevent an MCS enumerator from finding any MCS whose cost is less than UB.

Proof. Adding ∨L(C′ ) to FH guarantees that from then on, all the computed MSSes will contain at least one clause from C ′ . Also, every MCS improving UB cannot contain C'. ✷

This can be exploited in two ways: First, it allows us to stop the computation of an MCS whenever its cost exceeds UB. Second, we can always block a subset, avoiding the computation of all the MCSes containing it, which cannot lead to improving UB. After computing an MCS C, or part of it exceeding UB, we compute its cost-minimum subset C ′ ⊆ C such that w(C ′ ) ≥ UB and add the hard clause ∨L(C′ ) to F.

6 Experimental Study

This experimental study evaluates the proposed Literal-Based eXtractor algorithm (LBX) with respect to the state of the art. It consists of two parts; the first one devoted to computing one MCS and the second one to MaxSAT approximation. LBX includes the refinements described at the end of Section 4.2. The experiments were run on a Linux cluster (2 GHz, 64bits), with a memory limit of 4 GB. LBX 1 was implemented in C++ interfacing Minisat 2.2 [E´en and S¨orensson, 2003].

6.1 MCS Extraction

Regarding MCS extraction, we compare LBX with CLD, which was the best-performing algorithm in [Marques-Silva et al., 2013a], RS [Bacchus et al., 2014] and CMP (with all its optimizations) [Gr´egoire et al., 2014]. In all cases, the original binaries provided by the authors were run according to their instructions. The time limit was set to 1800 seconds.

1 Available at http://logos.ucd.ie/wiki/doku.php?id=lbx

We considered three sets of unsatisfiable instances: The first one, ijcai13-bench, contains 866 instances taken from [Marques-Silva et al., 2013a], both plain and partial formulas. The second one, proposed in [Gr´egoire et al., 2014], includes 295 plain instances from the 2011 MUS competition. Finally, as most of these instances were solved swiftly by all the algorithms we propose a new set of hard instances. It contains all the instances from the 2014 MaxSAT evaluation 2 as well as from other sources 3 such that either CMP or LBX took more than 90s to solve, filtering out those where none of these algorithms was able to complete a single call to the SAT solver. The resulting set, maxsat-bench, contains 179 instances.

Table 2 reports, for each algorithm and benchmark set, the number of instances solved by the time limit. Figures 1 and 2 show, respectively, the running times of the methods on the combination of ijcai13-bench and mus-bench and on the maxsat-bench sets of instances. VBS (Virtual Best Solver) emulates a parallel portfolio including all the algorithms.

In the first two sets, LBX is the best method, closely followed by CMP, which is clearly better than RS and CLD. LBX is able to solve 3 more instances than CMP, and many more than both RS and CLD. Also, Fig. 1 shows clear differences in the running times in favor of LBX over CMP.

The results from the third benchmark show more important differences. As we can observe in Figure 2, LBX performs significantly better than any other algorithm. Remarkably, LBX is able to solve 35, 63 and 68 more instances than CMP, RS and CLD respectively.

Finally, VBS, to which LBX contributes substantially, confirms the conclusion of previous works that a portfolio can lead to improvements. It results in a reduction of the running times and in the ability to solve some more instances.

6.2 MaxSAT Approximation

The second series of experiments compare LBX, using the techniques presented in Section 5, with three state-of-the-art MaxSAT approximation methods: CLD (in approximation mode), which was shown to outperform IROTS [Tompkins and Hoos, 2004] and SAT4J [Le Berre and Parrain, 2010], Dist [Cai et al., 2014], which ranked first in the (weighted) partial crafted incomplete tracks in the 2014 MaxSAT evaluation and wpm2014.in (WPM), which ranked first in the (weighted) partial industrial tracks.

2 http://www.maxsat.udl.cat/14/index.html

3 Additionally it includes a few partial MaxSAT instances created for over-approximating the backbone of satisfiable formulas (taken from [Janota et al., 2015]).

The comparison takes place on instances that may be very hard for exact solvers. So, for each crafted and industrial sets of benchmarks of the 2014 MaxSAT evaluation, we considered the instances such that the winner of the respective complete track took more than 500 seconds (or aborted in 30 min.). These exact solvers are Eva [Narodytska and Bacchus, 2014], ISAC+ [Ans´otegui et al., 2014] and Open-WBO [Martins et al., 2014]. In these experiments, the approximation algorithms were given a time limit of 60 seconds.

Table 3 reports, for each benchmark set, a comparison of LBX with the three mentioned algorithms. L, D and W (for Lose, Draw and Win) show, respectively, the number of instances where LBX returned a worse, equal or better solution than the method it is compared to by the time limit. We include BC (for Best Complete), that comprises the best upper bound returned by the winner of the respective complete track by a time limit of 30 min. The last columns (# WINS) show the number of instances each method reached the best solution found by all the algorithms (excluding BC).

The results reveal that LBX is very effective at approximating MaxSAT. It reaches better solutions for more instances than any other method in most sets, in many cases by far. The only exception is the pms-crafted set, where LBX shows a slightly worse behavior than Dist. Moreover, according to # WINS, LBX ranks first in three sets and second in the remaining two. Also, regardless of the instances being weighted or unweighted, LBX outperforms any other method, so it is quite instances stable. Overall, the ratio W/L ranges between 2.3 (for Dist) to 5.2 (for BC), which indicates that, compared to any other method, LBX returns better solutions many more times than worse solutions. Finally, it sums 2.42, 1.76 and 1.7 times more # WINS than CLD, WPM and Dist respectively.

Figure 2: Running times frommaxsat instances.

7 Conclusions

MCS extraction is a fundamental step in the analysis of overconstrained systems, finding many applications in AI. This paper develops a novel algorithm (LBX) that exploits the tight relationship between MCSes and backbones of propositional formulas. Moreover, the paper develops novel insights on how to approximate MaxSAT with restricted MCS enumeration. The experimental results demonstrate that the novel MCS extraction algorithm outperforms what are currently the best performing approaches. In addition, they confirm that restricted MCS enumeration represents an effective approach for MaxSAT approximation, yielding for most (hard) problem instances, high-quality solutions within a small run time.

One natural research direction is to deploy the novel LBX algorithm in the growing range of applications of MCSes. Also, new literal-based algorithms could be devised by building on different strategies (e.g. dichotomic search). Finally, the results motivate further research on additional techniques for MCS-based MaxSAT approximation.