# boosting_mcses_enumeration__3c2365bd.pdf

Boosting MCSes Enumeration

Eric Gr egoire, Yacine Izza, Jean-Marie Lagniez CRIL - Universit e d Artois & CNRS, Lens, France {gregoire,izza,lagniez}@cril.fr

The enumeration of all Maximal Satisﬁable Subsets (MSSes) or all Minimal Correction Subsets (MCSes) of an unsatisﬁable CNF Boolean formula is a useful and sometimes necessary step for solving a variety of important A.I. issues. Although the number of different MCSes of a CNF Boolean formula is exponential in the worst case, it remains low in many practical situations; this makes the tentative enumeration possibly successful in these latter cases. In the paper, a technique is introduced that boosts the currently most efﬁcient practical approaches to enumerate MCSes. It implements a model rotation paradigm that allows the set of MCSes to be computed in an heuristically efﬁcient way.

1 Introduction

Computing one maximal1 satisﬁable subset of clauses, noted MSS, within an unsatisﬁable CNF Boolean formula is a cornerstone task in various A.I. domains ranging from modelbased diagnosis (see e.g., the seminal work in [Reiter, 1987], a readings book [Hamscher et al., 1992] or some more recent research work in [Felfernig et al., 2012; Marques-Silva et al., 2015]) to various paradigms of belief change (see e.g., [Ferm e and Hansson, 2011] for a survey of the ﬁeld). In the Boolean setting, reasoning in a credulous [Reiter, 1980] way about contradictory information represented by an unsatisﬁable CNF Σ can amount to reasoning about one MSS of Σ. Interpreted as a set of constraints, an unsatisﬁable CNF formula Σ represents an over-constrained problem [Meseguer et al., 2003] for which no solution exists. When Φ is one maximal satisﬁable subset of Σ and when Ψ is deﬁned as Σ \ Φ, Ψ is one minimal subset of Σ such that dropping Ψ from the problem makes this one become feasible. Accordingly, Ψ is sometimes called a minimal correction subset of Σ (hence the interchangeable notations MCS and Co-MSS for this concept). In the worst case, the computation of an MSS or an MCS is a hard computational task since the basic problem of checking whether a set of clauses forms one MCS is DP-complete [Chen and Toda, 1995], which is also the complexity of the SAT-UNSAT problem. However, in many prac-

1We always consider set-inclusion maximality in this paper.

tical situations, computing one MSS is routinely performed by SAT-based tools (see e.g., [Marques-Silva et al., 2013; Gr egoire et al., 2014; Bacchus et al., 2014; Menc ıa et al., 2015; 2016] among others). The enumeration of all MCSes or all MSSes of Σ is even more computationally challenging. This task is a useful and sometimes necessary step in order to implement some forms of skeptical reasoning in abstract argumentation [Lagniez et al., 2015] or in the presence of contradictions, which is a general issue that can be traced back to early seminal works about nonmonotonic logics [Bobrow, 1980]. It plays also a role in infeasibility analysis of a set of clauses, as the computation of all minimal unsatisﬁable subsets, in short MUSes, can rely on the success of this enumeration (see e.g., [Lifﬁton and Sakallah, 2008; Gr egoire et al., 2007; Nadel et al., 2014; Bacchus and Katsirelos, 2015; 2016; Previti and Marques-Silva, 2013; Lifﬁton et al., 2016] among others). Although the number of different MCSes of the same formula is exponential in the worst case, it remains low in many practical situations; this makes the tentative enumeration of all MCSes possibly successful in these latter cases. In the paper, a technique is introduced that boosts the currently most efﬁcient practical techniques to enumerate the MCSes of an unsatisﬁable Boolean formula Σ. It is based on a form of so-called model rotation paradigm [Belov and Marques-Silva, 2011a; Nadel et al., 2014; Bacchus and Katsirelos, 2015]. We show that it allows the set of MCSes of Σ to be computed in an heuristically efﬁcient way. The paper is organized as follows. The technical background and the well-known MSS and MCS concepts are brieﬂy reviewed in the preliminaries. In section 3, the key paradigms of transition clauses and clause selectors are recalled; their roles are illustrated through the basic linear search for one MCS. Section 4 presents a basic MCSes enumeration algorithm before an original advanced one is step-by-step described in section 5. In section 6, the use of model rotation in this latter algorithm is explained. Then, we present our extensive experimental study. Promising paths for further research are brieﬂy introduced in the conclusion.

2 Technical Background We consider a standard language of formulas L of Boolean logic. , , and represent the negation, disjunction, conjunction and material implication connectives, respectively.

Proceedings of the Twenty-Seventh International Joint Conference on Artiﬁcial Intelligence (IJCAI-18)

A literal is either a Boolean variable or its negation. A clause is a formula that consists of a disjunction of literals. A CNF (clausal normal form) formula is a conjunction (also represented as a set) of clauses. α, β, . . . and Σ, , Φ, Ψ, . . . denote formulas and sets of formulas, respectively. An interpretation µ assigns values from {0, 1} to every Boolean variable, and, following usual compositional rules, to all formulas of L. A formula α is satisﬁable iff there exists at least one interpretation µ that satisﬁes α; µ is then called a model of α. Accordingly, µ satisﬁes a non-empty clause α when there exists at least one literal of α that is assigned 1 by µ; µ satisﬁes a CNF Σ iff µ satisﬁes all clauses of Σ. Any formula of L can be rewritten under an equisatisﬁable CNF formula. The core, MUS, MSS and MCS cross-related concepts are deﬁned as follows. Let Σ be a CNF formula.

Deﬁnition 1. (Core) A CNF Σ is a core of Σ iff Σ Σ and Σ is unsatisﬁable.

Deﬁnition 2. (MUS) A minimal unsatisﬁable subset (in short, MUS) Υ of Σ is a core of Σ such that α Υ, Υ \ {α} is satisﬁable.

When a CNF Σ is unsatisﬁable, it can be split into one MSS, i.e., one maximal satisﬁable subset of Σ, and its settheoretical complement in Σ, namely, one minimal correction subset, for short one MCS, of Σ.

Deﬁnition 3. (MSS) A maximal satisﬁable subset (in short, MSS) Φ of Σ is a subset Φ Σ that is satisﬁable and such that α Σ \ Φ, Φ {α} is unsatisﬁable.

Deﬁnition 4. (MCS) A minimal correction subset (in short MCS, also called Co-MSS) Ψ of Σ is a set Ψ Σ whose complement in Σ, i.e., Σ \ Ψ, is an MSS of Σ.

Example 1. Let Σ be an unsatisﬁable CNF formed by a set of clauses {α1, α2, α3, α4, α5, α6}, where α1 = a b, α2 = a b, α3 = a b, α4 = a b, α5 = b, α6 = b. The MCSes of Σ are {α1, α6}, {α2, α6}, {α3, α5} and {α4, α5}. The MUSes of Σ are {α1, α2, α3, α4}, {α1, α2, α5}, {α3, α4, α6} and {α5, α6}.

Notice that one MSS of Σ can be interpreted as one approximate solution of Max-SAT on Σ, since maximality in MSS is about set-inclusion vs. cardinality. The currently most efﬁcient approaches and tools to compute one MSS are described in [Gr egoire et al., 2014] and [Menc ıa et al., 2015; 2016]. The MSS and MCS paradigms can be extended into the socalled Partial-MSS and Partial-MCS concepts in order to handle the situation where Σ = Σ1, Σ2 , where Σ1 and Σ2 are sets of hard and soft clauses, respectively: hard clauses are required to belong to any Partial-MSS of Σ; they thus do not belong to any Partial-MCS of Σ. In the sequel, Σ1 and Σ2 always denote sets of hard and soft clauses, respectively. Notice that when Σ1 is unsatisﬁable, Partial-MSSes of Σ do not exist. In all the other cases, there always exists at least one Partial-MCS of Σ that is included in Σ2. Moreover, every Partial-MCS of Σ1, Σ2 is an MCS of Σ1 Σ2. Conversely, every MCS of Σ1 Σ2 that does not satisfy Σ1 is not a Partial MCS of Σ1, Σ2 .

3 Basic Linear Search for one MCS

State-of-the-art MCS extractors often make use of so-called clause selectors as follows. Each clause α of Σ is augmented with its own (negated) selector, namely a fresh new literal sα. This yields a new (relaxed) CNF formula ΣS. A clause α sα in ΣS is thus activated (resp., deactivated) when the literal sα (resp., sα) is set to 1. Selectors play the role of assumptions that can be activated/deactivated during the same search while useful information can be recorded at each step. Especially, when Σ is shown unsatisﬁable under some such assumptions, modern SAT solvers can often extract a subset of the assumptions that causes Σ to be unsatisﬁable [E en and S orensson, 2003; Lagniez and Biere, 2013; Audemard et al., 2013]. We will exploit this feature in the MCSes enumeration algorithm. In the rest of the paper, we often implicitly refer to ΣS and make no ontological difference between the selectors and the other literals in ΣS. The concept of transition clause (in short, TC) is also often a key paradigm for the currently most efﬁcient approaches to compute one MUS [Gr egoire et al., 2007; Previti and Marques-Silva, 2013], one MSS or one MCS [Gr egoire et al., 2014].

Deﬁnition 5. (Transition Clause) A clause α Σ is a transition clause (in short, TC) of Σ when, at the same time, Σ is unsatisﬁable and Σ \ {α} is satisﬁable.

Thus, when a clause α is a TC of Σ, α (resp., Σ \ {α}) is an MCS (resp., MSS) of Σ. Moreover, if α is a TC of Σ then α belongs to every MUS of Σ. Although Σ might not contain any TC, state-of-the-art MCS-ﬁnding tools often take advantage of TCes in the following way. Starting from the empty set, they iteratively and greedily construct a set Σ : at each step, clauses from Σ that have not been considered so far are inserted one by one in Σ until Σ becomes unsatisﬁable. The last considered clause is a TC for Σ and is introduced in the MCS under construction. The corresponding linear search algorithm for computing one MCS is called BLS. State-of-the-art MCSﬁnding tools [Gr egoire et al., 2014; Bacchus et al., 2014; Marques-Silva et al., 2013] have grafted various improvements to this algorithm skeleton; they take advantage of disjoint cores, computed models, the exploitation of the disjunction of the clauses of the MCS under construction and backbone literals, mainly. In the rest of the paper, we refer to improved versions of BLS that include subsets of these additional features: they are noted ELS for Enhanced Linear Search. ELS is easily adapted in such a way that it computes one Partial-MCS: the hard clauses are initially inserted in the MSS without selectors. An initial call to a SAT solver is necessary to check whether the set of the hard clauses is unsatisﬁable: in the positive case, an empty set needs to be returned. In the following, when we refer to a Partial-MCS-ﬁnding algorithm, we consider a procedure with a set of hard clauses Σ1 and a set of soft clauses Σ2 as input parameters: namely, Extract Partial MCS(Σ1, Σ2).

Proceedings of the Twenty-Seventh International Joint Conference on Artiﬁcial Intelligence (IJCAI-18)

4 MCSes Enumeration

Alg. 1 describes the typical skeleton of usual current approaches [Lifﬁton and Sakallah, 2008; Lifﬁton et al., 2016; Marques-Silva et al., 2013] to enumerate all MCSes: each time one MCS is found, an additional clause is created. Its role is to prevent the same MCS from being computed again. It is made of the disjunction of all the selectors of the clauses in the discovered MCS. In Alg. 1, the blocking clauses are inserted in a set . Partial-MCSes of (ΣS , S) are computed while MCSes still exist, or, equivalently, while ΣS is satisﬁable. Clearly, the time-consuming part of this algorithm lies in the multiple calls to a SAT oracle in the routine extracting one Partial-MCS. In this respect, [Previti et al., 2017] has proposed to enhance the algorithm by recording, for caching purpose, the cores discovered during the successive computations of the different MCSes: this yields the currently most efﬁcient MCSes enumeration algorithm, noted mcscache-els in this paper. In the next section, we propose another approach to decrease the number of calls to a SAT oracle; it is compatible with the caching technique. In the experimental section, we show that the proposed approach outperforms mcscache-els. Moreover, when combined with the caching technique, it yields an even more efﬁcient algorithm. It is based on properties of transition clauses and on the so-called recursive model rotation paradigm; both are described in the next two sections.

Algorithm 1: Enum-ELS (Enumerate All MCSes Computed with the Extract Partial MCS procedure);

Input : an unsatisﬁable CNF formula Σ Output : all MCSes of Σ

ΣS {α sα|α Σ} ; // with sα fresh variables 1 S {sα|α Σ }; // a set of selectors 2 ; 3 while ΣS is satisﬁable do 4

M Extract Partial MCS(ΣS , S); 5 output(M ); 6 (W sα M sα) ; // blocking clauses 7

5 More MCSes Thanks to Transition Clauses

First, the next property shows that any transition clause (in short, TC) α of an unsatisﬁable subset Σ Σ can be the starting point of a family of MCSes of Σ, where each member of this family contains α. This family is shown to capture the MCSes of Σ that are made of α together with any Partial-MCS of Σ \ {α}, Σ \ Σ ,

Property 1. Let Σ be an unsatisﬁable CNF formula and let Σ Σ such that Σ contains at least one TC α. For all Partial-MCSes Γ that can be built from Σ \ {α}, Σ \ Σ , Γ {α} is an MCS of Σ.

The previous property is easily adapted to address the case where Partial-MCSes are targeted, as the following corollary shows.

Corollary 1. Let Σ1, Σ2 be a couple of CNF formulas such that Σ1 is satisﬁable and Σ1 Σ2 is unsatisﬁable. Assume that Σ 2 Σ2 is such that Σ1 Σ 2 contains at least one TC α of Σ 2. For all Partial-MCSes Γ that can be built from Σ1 Σ 2 \ {α}, Σ2 \ Σ 2 , we have that Γ {α} is a Partial MCS of Σ1, Σ2 .

Now assume that we compute several TCes for a given subformula CNF Σ Σ. For each TC, it is possible to recursively apply the previous corollary in order to compute several Partial-MCSes. Moreover, the following property ensures that all these Partial-MCSes are different.

Property 2. Let Σ1, Σ2 be a couple of CNF formulas such that Σ1 is satisﬁable and Σ1 Σ2 is unsatisﬁable. Assume that Σ 2 Σ2 is such that Σ1 Σ 2 contains at least two different TCes α1 and α2 that occur in Σ 2. Then, for all Partial-MCSes Γ1 and Γ2 that can be built from Σ1 Σ 2\{α1}, Σ2\Σ 2 and Σ1 Σ 2\{α2}, Σ2\Σ 2 , respectively, we have that Γ1 {α1} and Γ2 {α2} are different Partial-MCSes of Σ1, Σ2 .

The latter property allows us to derive and justify the original recursive Algorithm 2, called TC-MCS, for Transition Clauses-Based Enumeration of MCSes. This algorithm extends ELS by computing not just one but several MCSes in a recursive way by means of a model rotation method (lines 7-12, Alg. 2). Its input is a couple of CNF formulas Σ1 ΣS 2 , U ; the output is a set of Partial-MCSes for this couple. Remember that U is the set of selectors corresponding to the clauses that have not been assigned so far to either an MCS or an MSS under construction. We assume that Σ1 is satisﬁable and thus, that Σ1 ΣS 2 is satisﬁable. ΣS 2 is actually built from Σ2 using selectors as explained earlier. Notice that hard clauses do not need selectors as they must always be satisﬁed and thus be activated. The Partial-MCSes of Σ1, Σ2 are derived directly from the Partial-MCSes of Σ1 ΣS 2 , S , where S is the set of unit clauses corresponding to all selectors. The algorithm starts by checking if U is empty. In the positive case, the procedure returns since the set of Partial MCSes of Σ1 ΣS 2 , U is empty as Σ1 ΣS 2 is always satisﬁable by construction. This is also the non-recursive step. Otherwise, the set of computed Partial-MCSes Θ and the set of selectors M + are initialized to the empty set. Remember that M + records the selectors corresponding to the clauses that can be activated when Σ1 ΣS 2 M + is satisﬁable. sα is initialized to , i.e., the tautology. Next, the loop (lines 3 6) incrementally augments M + with a sequence of sα, which are removed from U. This process is iterated while U is not empty and, at the same time, while sα is not a TC of Σ1 ΣS 2 M + {sα}. sα is a TC when Σ1 ΣS 2 M + {sα} becomes unsatisﬁable. Indeed, all the selectors inserted so far in M + have guaranteed that Σ1 ΣS 2 M + remained satisﬁable. Thus, when an incoming sα makes the formula become unsatisﬁable, this selector sα is a TC. At the end of the loop, two cases can occur: (1) sα M +. In this case, M + has captured all the selectors from U and the input formula was actually satisﬁable. Accordingly, the empty set is returned; (2) sα / M + and thus sα is a TC. In this case, we look for a core Γ of the current unsatisﬁable formula Σ1 ΣS 2 M + {sα} (line 8). It is easy to

Proceedings of the Twenty-Seventh International Joint Conference on Artiﬁcial Intelligence (IJCAI-18)

see that sα belongs to Γ and it is a TC of Γ. As already mentioned, modern SAT solvers return as a byproduct a core that is often smaller than the formula that is shown unsatisﬁable. We choose to use this core instead of the latter formula since the core often contains more TCes. It is easy to prove by contradiction that every TC is present in the core. Once a core is extracted, a method is called in order to identify TCes belonging to the core. In the next section, we present an approach to achieve this process, but for the moment, we just assume that TCes are extracted. Notice that we have no guarantee that this approach is efﬁcient and identiﬁes sα as a TC. For this reason, we directly add sα into T, i.e., the set of transitions clauses, in order to ensure the termination of the algorithm. Then, for each identiﬁed TC sβ (T M +) we recursively call the function with Σ1 ΣS 2 (Γ\{ sβ}), U (M +\Γ) as input. It is easy to show that these parameters match the conditions stated in Corollary 1. Accordingly, all the Partial-MCSes that we can compute from Σ1 ΣS 2 (Γ\{ sβ}), U (M +\Γ) can be augmented with sβ to yield a Partial-MCS of the input formula.

Algorithm 2: TC-MCS ( Σ1 ΣS 2 , U );

Input : Σ1 ΣS 2 , U a couple of CNF formulas Output : Θ a set of Partial-MCSes of Σ1 ΣS 2 , U

if U = then return ; 1 Θ ; M + ; sα ; 2 while U = and Σ1 ΣS 2 M + {sα} is satisﬁable do 3

M + M + {sα}; 4 sα choose sα U; 5 U U \ {sα}; 6

if sα / M + then 7

Γ Core(Σ1 ΣS 2 M + {sα}); 8 T {sα} Find-TC(Γ); 9 foreach sβ T M + do 10

Ω TC-M CS( Σ1 ΣS 2 (Γ\{ sβ}), U (M + \Γ) ); 11 Θ Θ (β Ω); 12

return Θ; 13

TC-MCS ( Σ1 ΣS 2 , U ) can be inserted in Alg. 1 to yield a new enumeration algorithm for MCSes, depicted in Alg. 3.

Algorithm 3: Enum-ELS-RMR;

Input : an unsatisﬁable CNF formula Σ Output : all MCSes of Σ

ΣS {α sα|α Σ} ; // with sα fresh variables 1 S {sα|α Σ } ; // a set of selectors 2 ; 3 while ΣS is satisﬁable do 4

Θ TC-MCS ( ΣS , S ); 5 foreach M Θ do 6

output(M ); 7 (W sα M sα) ; // blocking clauses 8

6 Using Model Rotation

Let us now explain how the Find-TC procedure (line 9 of Alg. 2) computes additional TCes. A naive method would consist in computing all the MCSes of Σ1 ΣS 2 M + {sα} that are singletons contained in M +. As this complete direct method can be too time-consuming, we propose an incomplete process to compute additional TCes, based on the so-called recursive model rotation paradigm [Belov and Marques-Silva, 2011b] noted rmr. This latter paradigm has been initially deﬁned in the context of computing one or several Minimal Unsatisﬁable Subsets (MUSes) of an unsatisﬁable CNF formula, where computing additional TCes in a fast way can also play a key role. As for [Bacchus and Katsirelos, 2015] where MUSes enumeration is targeted, we take advantage of the duality between MUSes and MCSes. However, we use the rmr paradigm for a very different task, which consists in enumerating MCSes. rmr is based on a model-theoretical perspective of TC: a TC of an unsatisﬁable CNF formula Σ is any clause α Σ such that there exists a complete interpretation µ of Σ that satisﬁes Σ \ {α} (and falsiﬁes α, otherwise the formula Σ would be satisﬁable). Starting from a model µ of Σ \ α, rmr consists in ﬂipping variables from α and checking if this new interpretation µ satisﬁes all the clauses of Σ except some α of Σ. In the positive case, α is marked as being a TC of Σ provided that it was not already marked as such, and the process is recursively repeated with µ and α . rmr can thus compute several TCes when a ﬁrst one is identiﬁed as such. In the search of one Partial-MCS, this situation occurs when we have shown that there exists a model µ of Σ1 ΣS 2 M + and proven that Σ1 ΣS 2 M + {sα} is unsatisﬁable. µ then plays the role of the initial interpretation and we keep the detected TCes belonging to {β Σ2 | sβ M +}, only. Finally, the set of selectors associated with the discovered TCes can be returned. It is important to note that we make sure that the clause selectors are never ﬂipped by the process. Although the rmr process is a polynomial one, it turns out that it can be time consuming in practice; it can actually reduce the practical efﬁciency of the enumeration algorithm. Such a situation occurs when the number of clauses contained in the set of blocking clauses becomes too large. To avoid such a drawback, we point out some sufﬁcient conditions to deprive clauses of of the rmr process. First, let us show the possible critical role of in the search for additional TCes. Consider ΣS, S with ΣS = { s1 a b, s2 a, s3 b}. Assume that one MCS, namely the singleton {s1}, has been computed, already. Thus, at this step = {s1}. Let us iterate the process and compute one more MCS and call TC-MCS on ΣS , S . Let us suppose that we stop the main loop of TC-MCS when M + = {s1, s2} and sα = s3. The condition in line 7 is satisﬁed; one core that is the complete formula is computed. Then, we search more TCes of ΣS S instead of ΣS S . In this case, it is easy to show that s1, s2, s3 are TCes and twice the same MCS will be computed. Obviously, a posteriori checking whether an MCS has already been computed by consulting can be too time-consuming. However, a useful feature is that ΣS and do not share

Proceedings of the Twenty-Seventh International Joint Conference on Artiﬁcial Intelligence (IJCAI-18)

literals. Indeed, is a set of positive clauses composed of selectors whereas these selectors occur negatively in ΣS. Accordingly, the satisﬁabilty of ΣS can be split into two independent sub-problems following a partition {P, N} of the set of selectors, where P and N denote the set of selectors that are positive and the set of negative ones, respectively. More precisely: Property 3. Let {P, N} be a partition of S, ΣS a CNF formula augmented with the set of selectors S and a CNF formula built on selector variables and formed of positive clauses, only. ΣS V s P s V s N s is satisﬁable if and only if ΣS V s P s and V s N s are satisﬁable. When an MCS is under construction we are implicitly computing a bi-partition {M +, M } of S such that ΣS V s M + s and V s M s are satisﬁable. The aim is then to move as many as possible selectors from M to M + while keeping both ΣS V s M + s and V s M s satisﬁable. It is easy to prove that if the bi-partition {M +, M } of S is such that ΣS V s M + s and V s M s are satisﬁable, then if we move one element s from M to M + such that ΣS V s M + {s } s is satisﬁable then V s M \{s } s is satisﬁable (as all the clauses of are positive, assigning one more positive selector cannot make the formula become unsatisﬁable). Let us stress that symmetric results can be obtained when one element is moved from M + to M . In order to avoid the need to consider in the rmr procedure, we propose the following process. First, compute a partition {M +, M } of S that satisﬁes ΣS V s M + s and V s M s. M + is then used as starting point to be evolved into an MSS and all the clauses of M are marked as being candidates for being a TC. Then, each time we augment M + with a new selector, we have that ΣS V s M + s is satisﬁable. Let us notice that, when we add an element to M +, in some sense we move this element from M to M +. Consequently, both ΣS V s M + s and V s M s are satisﬁable. In some sense, the marked selectors are responsible for the satisﬁability of . Thus, since M + is constructed such that ΣS V s M + s is satisﬁable, it becomes useless to check the satisﬁability of during the rmr process when we forbid the marked clauses to be selected as TCes.

7 Experimental Study We have implemented all our algorithms in C++ and used Minisat http://minisat.se/ as backend SAT solver. We have selected the 866 benchmarks used in [Previti et al., 2017; Marques-Silva et al., 2013]: 269 instances are plain Max-SAT ones and the remaining 597 are Partial Max-SAT ones. We have enriched this experimental setting by also considering a second series of plain Max-SAT benchmarks made of the instances from the MUS competition http://www.satcompetition.org/2011. Some of these instances were already present in the benchmarks proposed by [Previti et al., 2017]. As we only kept the new ones, 1090 benchmarks were considered in total: 493 of them are plain Max-SAT instances and 597 are Partial-Max-SAT ones. All experimentations have been conducted on Intel Xeon E52643 (3.30GHz) processors with 64Gb memory on Linux

Cent OS. Time-out was set to 1800 seconds for each run of an algorithm on an instance; memory-out was set to 8 Gb for each such run. All data, results and software used in the experimentations are available from http://www.cril.fr/enumcs. First, we compared our own implementation of Enum-ELS-RMR (Alg. 4) with the same algorithm deprived of rmr. Our version of ELS included the exploitation of computed models [Gr egoire et al., 2014], as well as of backbone literals [Marques-Silva et al., 2013]. The comparison was made in terms of the total number of computed MCSes for each benchmark instance. As shown by Fig. 1 the rmr paradigm allowed us to compute more (or the same number) of MCSes for every plain Max-SAT benchmark instance. The same result was obtained for most Partial-Max-SAT benchmarks, too.

Partial-Max-SAT benchmarks

Max-SAT benchmarks

Figure 1: Enum-ELS-RMR vs. Enum-ELS

Then, we combined the caching technique with Enum-ELS-RMR, giving rise to Enum-ELS-RMR-Cache. Following the recommendation of [Previti et al., 2017], we did not include the backbone feature in ELS since it might slow down the caching technique. Enum-ELS-RMR-Cache allowed a largest number of MCSes to be computed, most often (Fig. 2). Noticeably, it appeared that the instances for which Enum-ELS-RMR-Cache delivered a smaller number of MCSes where such that Enum-ELS-Cache already produced a smaller number of MCSes than Enum-ELS-RMR. Also, introducing the caching method leads to more memoryout conclusions. These two last points can be explained by the fact that, as already pointed out in [Previti et al., 2017], the caching memory can become too large to handle. Finally, we have compared the mcscache-els tool from [Previti et al., 2017], which implements the caching technique on a state-of-the-art version of Enum-ELS, with Enum-ELS-RMR-Cache. Fig. 3 clearly shows that Enum-ELS-RMR-Cache outperforms mcscache-els for almost all benchmarks and the difference between both approaches is generally even more signiﬁcant for the instances with the largest numbers of MCSes.

8 Conclusion and Perspectives In this paper, we have enhanced the most efﬁcient tool to enumerate all the minimal correction subsets (MCSes) of a Boolean CNF formula. Although the number of MCSes can

Proceedings of the Twenty-Seventh International Joint Conference on Artiﬁcial Intelligence (IJCAI-18)

Partial-Max-SAT benchmarks

Max-SAT benchmarks

Figure 2: Enum-ELS-RMR-Cache vs. Enum-ELS-RMR

Partial-Max-SAT benchmarks

Max-SAT benchmarks

Figure 3: Enum-ELS-RMR-Cache vs. mcscache-els

be exponential in the worst case, it remains low in many reallife problems, especially in problems for which the number and the cardinality of the different minimal sources of unsatisﬁability remain low. Indeed, there exists a hitting set correspondence between the set of MCSes and the set of MUSes, namely of minimal unsatisﬁable subsets. Accordingly, computational progress made in enumerating all MCSes of CNF formulas when their number of MCSes is large opens new perspectives for enumerating all MUSes for the same formula. Indeed, the approches for listing all MUSes that ﬁrst compute all MCSes before they compute MUSes from them can clearly beneﬁt from these improvements obtained in the MCSes enumeration task. We believe that this study opens other various paths for further research, too. Speciﬁcally, Property 3 opens the way for some parallelization of the enumeration task. It could be interesting to extend rmr using forms of local search to detect additional TCes. Also, we plan to adapt this study to the enumeration of all preferred MCSes when the clauses of Σ obey some preference pre-orderings. Finally, as skeptical reasoning in the presence of conﬂicting information can amount to computing the intersection of all maximal satisﬁable subsets (MSSes), new progress in enumerating all MSSes, and thus all MCSes, can prove valuable for implementing such forms of reasoning.

Proof of Property 1. By contradiction. Let us assume that Γ {α} is not an MCS of Σ. That means that either (1) Σ \ (Γ {α}) is unsatisﬁable or (2) β Γ {α} such that

Σ \ ((Γ {α}) \ {β}) is satisﬁable. Assume (1). As Γ is deﬁned as a Partial-MCS of Σ \ {α}, Σ \ Σ , we have that Γ is an MCS of (Σ \ {α}). Thus, (Σ \ {α}) \ Γ is satisﬁable. This entails that ((Σ \ {α}) {α}) \ (Γ {α}) is satisﬁable. This latter formula can be simpliﬁed into Σ \ (Γ {α}), which is thus also satisﬁable. This contradicts (1). Accordingly, (1) never occurs. Assume (2). Let us suppose that β Γ (then β = α). Since Γ is a Partial-MCS of Σ \ {α}, Σ \ Σ , we have that Γ is an MCS of Σ \ {α}. Thus, (Σ \ {α}) \ (Γ \ {β}) is unsatisﬁable. This entails that ((Σ \ {α}) {α}) \ ((Γ \ {β}) {α}) is unsatisﬁable. Because we supposed β = α, we have (Γ \ {β}) {α} = (Γ {α}) \ {β}. Consequently, Σ \ ((Γ {α}) \ {β}) is unsatisﬁable. This contradicts the assumption and thus β and α must be the same clause. Because Γ is a Partial-MCS of Σ \ {α}, Σ \ Σ , we have (Σ \ {α}) Γ = and Γ Σ \ Σ . By hypothesis α Σ , this means α / Γ and thus ((Σ \{α}) {α}) Γ = . Hence Σ Γ = . If β = α, then we have Σ \ ((Γ {α}) \ {α}) = Σ\Γ is satisﬁable according to assumption (2). Since Σ Σ, we also have Σ \ Γ is satisﬁable. Since Σ Γ = we have that Σ is satisﬁable. This contradicts the hypothesis that asserts that Σ is an unsatisﬁable subset of Σ. Proof of Corollary 1. Property 1 allows us to conclude that Γ {α} is an MCS of Σ1 (Σ 2 \{α}) (Σ2 \Σ 2) {α}, and thus of Σ1 Σ2. Since Γ {α} Σ2, we directly conclude that Γ {α} is a Partial-MCS of Σ1, Σ2 . Proof of Property 2. From Corollary 1 it is easy to show that Γ1 {α1} and Γ2 {α2} are both Partial-MCSes of Σ1, Σ2 . Now, let us show that these Partial-MCSes are different. It is sufﬁcient to show that α1 / Γ2. By deﬁnition of a Partial MCS, we have Γ2 Σ2 \ Σ 2. As α1 Σ 2, it is straightforward that α1 / Γ2 and then Γ1 {α1} = Γ2 {α2}. Proof of Property 3. Let us show that if ΣS V s P s V s N s then ΣS V s P s and V s N s are satisﬁable and vice versa. ( ) Straightforward. ( ) If ΣS V s P s and V s N s are both satisﬁable, then there exists a model µ that satisﬁes ΣS V s P s. By deﬁnition of ΣS, whatever the satisﬁable interpretation considered is, it is always possible to ﬂip the truth value of selectors from 1 to 0 and keep the resulting interpretation µP such that µP is a model of ΣS (this is possible because assigning a selector to 0 deactivates clauses of ΣS and then weakens this formula). Thus, since P N = , we can construct the interpretation µN P that is equivalent to µP except on the truth value of the selectors belonging to N where we force them to be assigned to 0. It is clear that µN P is a model of ΣS V s P s. Now, let us prove that µN P is a model of V s N s too. By construction, only contains positive clauses composed of selectors. Then, whatever the model of V s N s considered is, it is always possible to ﬂip the truth value of some selectors from 0 to 1 and keep this interpretation as a model of . Thus, since all models of V s N s must satisfy V s N s, we can construct the interpretation V s N s V s P s that satisﬁes V s N s. Thus, since is only constructed on selector variables, it is easy to show that µN P also satisﬁes V s N s. Consequently, µN P satisﬁes ΣS V s P s V s N s.

Proceedings of the Twenty-Seventh International Joint Conference on Artiﬁcial Intelligence (IJCAI-18)

Acknowledgments This work has been supported in part by the CPER DATA project funded by the Hauts-de-France Region. We thank the reviewers for their useful comments.

References [Audemard et al., 2013] Gilles Audemard, Jean-Marie Lagniez, and Laurent Simon. Improving glucose for incremental SAT solving with assumptions: Application to MUS extraction. In Proc. of SAT 2013, pages 309 317, 2013. [Bacchus and Katsirelos, 2015] Fahiem Bacchus and George Katsirelos. Using minimal correction sets to more efﬁciently compute minimal unsatisﬁable sets. In Proc. of CAV 2015, pages 70 86, 2015. [Bacchus and Katsirelos, 2016] Fahiem Bacchus and George Katsirelos. Finding a collection of muses incrementally. In Proc. of CPAIOR 2016, pages 35 44, 2016. [Bacchus et al., 2014] Fahiem Bacchus, Jessica Davies, Maria Tsimpoukelli, and George Katsirelos. Relaxation search: A simple way of managing optional clauses. In Proc. of AAAI 2014, pages 835 841, 2014. [Belov and Marques-Silva, 2011a] Anton Belov and Jo ao Marques-Silva. Accelerating MUS extraction with recursive model rotation. In Proc. of FMCAD 2011, pages 37 40, 2011. [Belov and Marques-Silva, 2011b] Anton Belov and Jo ao Marques-Silva. Accelerating MUS extraction with recursive model rotation. In Proc. of FMCAD 2011, pages 37 40, 2011. [Bobrow, 1980] Daniel G. Bobrow. Special issue non nonmonotonic logics. Artiﬁcial Intelligence, 13(1-2), 1980. [Chen and Toda, 1995] Zhi-Zhong Chen and Seinosuke Toda. The complexity of selecting maximal solutions. Information and Computation, 119(2):231 239, 1995. [E en and S orensson, 2003] Niklas E en and Niklas S orensson. An extensible SAT-solver. In Selected Revised Papers of the 6th Int. Conf. of SAT 2003, pages 502 518, 2003. [Felfernig et al., 2012] Alexander Felfernig, Monika Schubert, and Christoph Zehentner. An efﬁcient diagnosis algorithm for inconsistent constraint sets. AI EDAM, 26(1):53 62, 2012. [Ferm e and Hansson, 2011] Eduardo L. Ferm e and Sven Ove Hansson. AGM 25 years - twenty-ﬁve years of research in belief change. Journal of Philosophical Logic, 40(2):295 331, 2011. [Gr egoire et al., 2007] Eric Gr egoire, Bertrand Mazure, and C edric Piette. Boosting a complete technique to ﬁnd MSS and MUS thanks to a local search oracle. In Proc. of IJCAI 2007, pages 2300 2305, 2007. [Gr egoire et al., 2014] Eric Gr egoire, Jean-Marie Lagniez, and Bertrand Mazure. An experimentally efﬁcient method for (MSS, Co MSS) partitioning. In Proc. of (AAAI 2014), pages 2666 2673, 2014.

[Hamscher et al., 1992] Walter Hamscher, Luca Console, and Johan de Kleer. Readings in model-based diagnosis. Morgan Kaufmann, 1992. [Lagniez and Biere, 2013] Jean-Marie Lagniez and Armin Biere. Factoring out assumptions to speed up MUS extraction. In Proc. of SAT 2013, pages 276 292, 2013. [Lagniez et al., 2015] Jean-Marie Lagniez, Emmanuel Lonca, and Jean-Guy Mailly. Coquiaas: A constraintbased quick abstract argumentation solver. In Proc. of ICTAI 2015, pages 928 935, 2015. [Lifﬁton and Sakallah, 2008] Mark H. Lifﬁton and Karem A. Sakallah. Algorithms for computing minimal unsatisﬁable subsets of constraints. Journal of Automated Reasoning, 40(1):1 33, 2008. [Lifﬁton et al., 2016] Mark H. Lifﬁton, Alessandro Previti, Ammar Malik, and Joao Marques-Silva. Fast, ﬂexible MUS enumeration. Constraints, 21(2):223 250, 2016. [Marques-Silva et al., 2013] Jo ao Marques-Silva, Federico Heras, Mikol as Janota, Alessandro Previti, and Anton Belov. On computing minimal correction subsets. In Proc. of IJCAI 2013, pages 615 622, 2013. [Marques-Silva et al., 2015] Jo ao Marques-Silva, Mikol as Janota, Alexey Ignatiev, and Ant onio Morgado. Efﬁcient model based diagnosis with maximum satisﬁability. In Proc. of IJCAI 2015, pages 1966 1972, 2015. [Menc ıa et al., 2015] Carlos Menc ıa, Alessandro Previti, and Jo ao Marques-Silva. Literal-based MCS extraction. In Proc. of IJCAI 2015, pages 1973 1979, 2015. [Menc ıa et al., 2016] Carlos Menc ıa, Alexey Ignatiev, Alessandro Previti, and Joao Marques-Silva. MCS extraction with sublinear oracle queries. In Proc. of SAT 2016, pages 342 360, 2016. [Meseguer et al., 2003] Pedro Meseguer, Noureddine Bouhmala, Taouﬁk Bouzoubaa, Morten Irgens, and Mart ı S anchez-Fibla. Current approaches for solving overconstrained problems. Constraints, 8(1):9 39, 2003. [Nadel et al., 2014] Alexander Nadel, Vadim Ryvchin, and Ofer Strichman. Accelerated deletion-based extraction of minimal unsatisﬁable cores. Journal of Satisﬁability JSAT, 9:27 51, 2014. [Previti and Marques-Silva, 2013] Alessandro Previti and Jo ao Marques-Silva. Partial MUS enumeration. In Proc. of AAAI 2013, 2013. [Previti et al., 2017] Alessandro Previti, Carlos Menc ıa, Matti J arvisalo, and Joao Marques-Silva. Improving MCS enumeration via caching. In Proc. of SAT 2017, pages 184 194, 2017. [Reiter, 1980] Raymond Reiter. A logic for default reasoning. Artiﬁcial Intelligence, 13(1-2):81 132, 1980. [Reiter, 1987] Raymond Reiter. A theory of diagnosis from ﬁrst principles. Artiﬁcial Intelligence, 32(1):57 95, 1987.

Proceedings of the Twenty-Seventh International Joint Conference on Artiﬁcial Intelligence (IJCAI-18)