Boosting MCSes Enumeration

1 Introduction

Computing one maximal 1 satisfiable subset of clauses, noted MSS, within an unsatisfiable 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 field). In the Boolean setting, reasoning in a credulous [Reiter, 1980] way about contradictory information represented by an unsatisfiable CNF Σ can amount to reasoning about one MSS of Σ. Interpreted as a set of constraints, an unsatisfiable CNF formula Σ represents an over-constrained problem [Meseguer et al., 2003] for which no solution exists. When Φ is one maximal satisfiable subset of Σ and when Ψ is defined 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 practical 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).

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

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 unsatisfiable subsets, in short MUSes, can rely on the success of this enumeration (see e.g., [Liffiton and Sakallah, 2008; Gr´egoire et al., 2007; Nadel et al., 2014; Bacchus and Katsirelos, 2015; 2016; Previti and Marques-Silva, 2013; Liffiton 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 efficient practical techniques to enumerate the MCSes of an unsatisfiable 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 efficient way.

The paper is organized as follows. The technical background and the well-known MSS and MCS concepts are briefly 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 briefly 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.

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 satisfiable iff there exists at least one interpretation µ that satisfies α; µ is then called a model of α. Accordingly, µ satisfies a non-empty clause α when there exists at least one literal of α that is assigned 1 by µ; µ satisfies a CNF Σ iff µ satisfies all clauses of Σ. Any formula of L can be rewritten under an equisatisfiable CNF formula.

The core, MUS, MSS and MCS cross-related concepts are defined as follows. Let Σ be a CNF formula.

Definition 1. (Core) A CNF Σ′ is a core of Σ iff Σ′ ⊆ Σ and Σ′ is unsatisfiable.

Definition 2. (MUS) Aminimal unsatisfiable subset (in short, MUS) Υ of Σ is a core of Σ such that ∀α ∈ Υ, Υ \ {α} is satisfiable.

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

Definition 3. (MSS) A maximal satisfiable subset (in short, MSS) Φ of Σ is a subset Φ ⊆ Σ that is satisfiable and such that ∀α ∈ Σ \ Φ, Φ ∪ {α} is unsatisfiable.

Definition 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 unsatisfiable 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 efficient 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 unsatisfiable, 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 PartialMCS 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 unsatisfiable under some such assumptions, modern SAT solvers can often extract a subset of the assumptions that causes Σ′ to be unsatisfiable [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 efficient 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].

Definition 5. (Transition Clause) A clause α ∈ Σ is a transition clause (in short, TC) of Σ when, at the same time, Σ is unsatisfiable and Σ \ {α} is satisfiable.

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-finding 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 unsatisfiable. 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 MCSfinding 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 unsatisfiable: in the positive case, an empty set needs to be returned. In the following, when we refer to a Partial-MCS-finding algorithm, we consider a procedure with a set of hard clauses Σ1 and a set of soft clauses Σ2 as input parameters: namely, ExtractPartialMCS(Σ1, Σ2).

4 MCSes Enumeration

Alg. 1 describes the typical skeleton of usual current approaches [Liffiton and Sakallah, 2008; Liffiton 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 satisfiable.

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 efficient 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 efficient 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 ExtractPartialMCS procedure); Input : an unsatisfiable CNF formula Σ Output : all MCSes of Σ ΣS ← {α ∨ ¬sα|α ∈ Σ} ; // with sα fresh variables 1 S ← {sα|α ∈ Σ }; // a set of selectors 2 ∆ ← ∅; 3 while ΣS ∪ ∆ is satisfiable do 4 M - ← ExtractPartialMCS(ΣS ∪ ∆, S); 5 output(M -); 6 ∆←∆∪ (∨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 unsatisfiable 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 unsatisfiable 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 satisfiable and Σ1 ∪ Σ2 is unsatisfiable. 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 PartialMCS 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 satisfiable and Σ1∪Σ2 is unsatisfiable. 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 TransitionClauses-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 ∪ ΣS2 ,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 satisfiable and thus, that Σ1∪ΣS2 is satisfiable. ΣS2 is actually built from Σ2 using selectors as explained earlier. Notice that hard clauses do not need selectors as they must always be satisfied and thus be activated. The Partial-MCSes of 〈Σ1,Σ2〉 are derived directly from the Partial-MCSes of 〈Σ1 ∪ ΣS2 , 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 PartialMCSes of 〈Σ1 ∪ ΣS2 ,U〉 is empty as Σ1 ∪ ΣS2 is always satisfiable 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 ∪ ΣS2 ∪M + is satisfiable. 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 ∪ ΣS2 ∪M + ∪ {sα}. sα is a TC when Σ1 ∪ ΣS2 ∪M + ∪ {sα} becomes unsatisfiable. Indeed, all the selectors inserted so far in M + have guaranteed that Σ1 ∪ ΣS2 ∪M + remained satisfiable. Thus, when an incoming sα makes the formula become unsatisfiable, 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 satisfiable. 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 unsatisfiable formula Σ1∪ΣS2 ∪M + ∪{sα} (line 8). It is easy to 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 unsatisfiable. 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 efficient and identifies 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 identified TC sβ ∈ (T ∩M +) we recursively call the function with 〈Σ1∪ΣS2 ∪(Γ\{¬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 ∪ΣS2 ∪(Γ\{¬sβ}), U ∪(M + \Γ)〉 can be augmented with sβ to yield a Partial-MCS of the input formula.

Algorithm 2: TC-MCS (〈Σ1 ∪ ΣS2 , U〉);

Input : 〈Σ1 ∪ΣS2 ,U〉 a couple of CNF formulas Output : Θ a set of Partial-MCSes of 〈Σ1 ∪ΣS2 ,U〉 if U = ∅ then return ∅; 1 Θ ← ∅; M + ← ∅; sα ← ⊤; 2 while U ̸= ∅ and Σ1 ∪ΣS2 ∪M + ∪ {sα} is satisfiable do 3 M + ← M + ∪ {sα}; 4 sα ← choose sα ∈ U; 5 U ← U \ {sα}; 6 if sα /∈M + then 7 Γ ← Core(Σ1 ∪ ΣS2 ∪ M + ∪ {sα}); 8 T ← {sα}∪ Find-TC(Γ); 9 foreach sβ ∈ T ∩M + do 10 Ω ← TC-M C S(〈Σ1 ∪ ΣS2 ∪ (Γ \ {¬sβ }), U ∪ (M + \ Γ)〉); 11 Θ ← Θ ∪ (β × Ω); 12

13

return Θ;

TC-MCS (〈Σ1 ∪ ΣS2 , 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 unsatisfiable CNF formula Σ Output : all MCSes of Σ ΣS ← {α ∨ ¬sα|α ∈ Σ} ; // with sα fresh variables 1 S ← {sα|α ∈ Σ } ; // a set of selectors 2 ∆ ← ∅; 3 while ΣS ∪ ∆ is satisfiable do 4 Θ ←TC-MCS (〈ΣS ∪ ∆, S〉); 5 foreach M - ∈ Θ do 6 output(M -); 7 ∆←∆∪ (∨sα∈M- sα) ; // blocking clauses 8

6 UsingModel 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 ∪ΣS2 ∪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 defined in the context of computing one or several Minimal Unsatisfiable Subsets (MUSes) of an unsatisfiable 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 unsatisfiable CNF formula Σ is any clause α ∈ Σ such that there exists a complete interpretation µ of Σ that satisfies Σ \ {α} (and falsifies α, otherwise the formula Σ would be satisfiable). Starting from a model µ of Σ \ α, rmr consists in flipping variables from α and checking if this new interpretation µ′ satisfies 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 first one is identified as such. In the search of one Partial-MCS, this situation occurs when we have shown that there exists a model µ of Σ1 ∪ΣS2 ∪M + and proven that Σ1 ∪ΣS2 ∪M + ∪ {sα} is unsatisfiable. µ 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 flipped 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 efficiency 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 sufficient 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 satisfied; 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 literals. Indeed, ∆ is a set of positive clauses composed of selectors whereas these selectors occur negatively in ΣS . Accordingly, the satisfiabilty 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 ∪ ∆ ∪ ∧s∈P s ∪ ∧s∈N ¬s is satisfiable if and only if ΣS ∪ ∧s∈P s and ∆∪ ∧s∈N ¬s are satisfiable.

When an MCS is under construction we are implicitly computing a bi-partition {M +,M -} of S such that ΣS ∪ ∧s∈M+ s and ∆∪ ∧s∈M- ¬s are satisfiable. The aim is then to move as many as possible selectors from M - to M + while keeping both ΣS ∪ ∧s∈M+ s and ∆∪ ∧s∈M- ¬s satisfiable. It is easy to prove that if the bi-partition {M +,M -} of S is such that ΣS ∪ ∧s∈M+ s and ∆ ∪ ∧s∈M- ¬s are satisfiable, then if we move one element s′ from M - to M + such that ΣS ∪ ∧s∈M+∪{s′ } s is satisfiable then ∆ ∪ ∧s∈M-\{s′ } ¬s is satisfiable (as all the clauses of ∆ are positive, assigning one more positive selector cannot make the formula become unsatisfiable). Let us stress that symmetric results can be obtained when one element is moved fromM + 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 satisfies ΣS ∪ ∧s∈M+ s and ∆ ∪ ∧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 ∪ ∧s∈M+ s is satisfiable. Let us notice that, when we add an element to M +, in some sense we "move" this element fromM - to M +. Consequently, both ΣS ∪∧s∈M+ s and ∆∪∧s∈M- ¬s are satisfiable. In some sense, the marked selectors are responsible for the satisfiability of ∆. Thus, since M + is constructed such that ΣS ∪ ∧s∈M+ s is satisfiable, it becomes useless to check the satisfiability 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 PartialMax-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 CentOS. 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.

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 significant for the instances with the largest numbers of MCSes.

8 Conclusion and Perspectives

In this paper, we have enhanced the most efficient tool to enumerate all the minimal correction subsets (MCSes) of a Boolean CNF formula. Although the number of MCSes can 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 unsatisfiability remain low. Indeed, there exists a hitting set correspondence between the set of MCSes and the set of MUSes, namely of minimal unsatisfiable 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 first compute all MCSes before they compute MUSes from them can clearly benefit from these improvements obtained in the MCSes enumeration task. We believe that this study opens other various paths for further research, too. Specifically, 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 conflicting information can amount to computing the intersection of all maximal satisfiable subsets (MSSes), new progress in enumerating all MSSes, and thus all MCSes, can prove valuable for implementing such forms of reasoning.

9 Proofs

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

Σ \ ((Γ ∪ {α}) \ {β}) is satisfiable.

Assume (1). As Γ is defined as a Partial-MCS of 〈Σ′ \ {α}, Σ \ Σ′ 〉, we have that Γ is an MCS of (Σ \ {α}). Thus, (Σ \ {α}) \ Γ is satisfiable. This entails that ((Σ \ {α}) ∪ {α}) \ (Γ ∪ {α}) is satisfiable. This latter formula can be simplified into Σ \ (Γ ∪ {α}), which is thus also satisfiable. 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 unsatisfiable. This entails that ((Σ \ {α}) ∪ {α}) \ ((Γ \ {β}) ∪ {α}) is unsatisfiable. Because we supposed β ̸= α, we have (Γ \ {β}) ∪ {α} = (Γ ∪ {α}) \ {β}. Consequently, Σ \ ((Γ ∪ {α}) \ {β}) is unsatisfiable. 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 satisfiable according to assumption (2). Since Σ′ ⊆ Σ, we also have Σ′ \ Γ is satisfiable. Since Σ′ ∩ Γ = ∅ we have that Σ′ is satisfiable. This contradicts the hypothesis that asserts that Σ′ is an unsatisfiable 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 sufficient to show that α1 /∈ Γ2. By definition of a PartialMCS, 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 ∪∆∪ ∧s∈P s∪ ∧s∈N ¬s then ΣS ∪ ∧s∈P s and ∆∪ ∧s∈N ¬s are satisfiable and vice versa. (⇒) Straightforward. (⇐) If ΣS ∪ ∧s∈P s and ∆ ∪ ∧s∈N ¬s are both satisfiable, then there exists a model µ that satisfies ΣS ∪ ∧s∈P s. By definition of ΣS , whatever the satisfiable interpretation considered is, it is always possible to flip 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 µNP 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 µNP is a model of ΣS ∪ ∧s∈P s. Now, let us prove that µNP is a model of ∆ ∪ ∧s∈N ¬s too. By construction, ∆ only contains positive clauses composed of selectors. Then, whatever the model of ∆ ∪ ∧s∈N ¬s considered is, it is always possible to flip the truth value of some selectors from 0 to 1 and keep this interpretation as a model of ∆. Thus, since all models of ∆ ∪ ∧s∈N ¬s must satisfy ∧s∈N ¬s, we can construct the interpretation ∧s∈N ¬s ∧ ∧s∈P s that satisfies ∆∪ ∧s∈N ¬s. Thus, since ∆ is only constructed on selector variables, it is easy to show that µNP also satisfies ∆∪ ∧s∈N ¬s. Consequently, µNP satisfies ΣS ∪ ∆ ∪ ∧s∈P s ∪ ∧s∈N ¬s.

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.