Boosting a Complete Technique to Find MSS and MUS Thanks to a Local Search Oracle

1 Introduction

This last decade, the SAT problem, namely the issue of checking whether a set of Boolean clauses is satisfiable or not, has received much attention from the AI research community. Indeed, SAT appears to be a cornerstone in many domains, like e.g. nonmonotonic reasoning, automated reasoning, modelbased diagnosis, planning and knowledge bases verification and validation. However, only knowing that a SAT instance is unsatisfiable is often not satisfactory since we might prefer knowing what goes wrong with the instance when this latter one is expected to be satisfiable.

In this respect, the MUS (Minimally Unsatisfiable Subformula) concept can be crucial since a MUS can be seen as an irreducible cause for infeasibility. Indeed, a MUS is an unsatisfiable set of clauses that is such that any of its subsets is satisfiable. It thus provides one explanation for unsatisfiability that cannot be made shorter in terms of the number of involved clauses. Restoring the satisfiability of an instance cannot be done without fixing all its MUS.

Unfortunately, a same instance can exhibit several MUS. Actually, the number of these MUS can be exponential since a n-clauses SAT instance can exhibit Cn/2 n MUS in the worst case. Moreover, computing MUS is intractable in the general case. Indeed, checking whether a set of clauses is a MUS or not is DP-complete [Papadimitriou and Wolfe, 1988] and checking whether a formula belongs to the set (clutter) of MUS of an unsatisfiable SAT instance or not, is in Σp2

[Eiter and Gottlob, 1992]. Fortunately, the number of MUS remains often tractable in real-life applications. For example, in model-based diagnosis [Hamscher et al., 1992], it is often assumed that single faults occur most often, which can entail small numbers of MUS.

A dual concept is the notion of Maximal Satisfiable Subset (MSS) of a SAT instance, and the complement of a MSS in a SAT instance is called a CoMSS. The complete sets of MUS and MSS are an implicit encoding of the other [Liffiton and Sakallah, 2005]. Specifically, a CoMSS is a hitting set of the set of MUS and represent minimal sets of clauses that should be dropped in order to restore consistency. In this paper, we are interested in exhaustive approaches to compute these correlated concepts in the Boolean clausal framework.

Recently, several approaches have been proposed to approximate or compute MUS and MSS, both in the Boolean framework and for other types of constraints. Some of them concern specific classes of clauses or remain tractable for small instances, only. Among them, let us mention the approach in [Bruni, 2005], where it is shown how a MUS can be extracted in polynomial time through linear programming techniques for clauses exhibiting a so-called integral property. However, only restrictive classes of clauses obey such a property (mainly Horn, renamable Horn, extended Horn, balanced and matched ones). Let us also mention [B¨uning, 2000; Davydov et al., 1998; Fleischner et al., 2002], which are other important studies in the complexity and the algorithmic aspects of extracting MUS for specific classes of clauses. In [Bruni, 2003], an approach is proposed that approximates MUS by means of an adaptative search guided by clauses hardness. In [Zhang and Malik, 2003] a technique is described, that extracts MUS by learning nogoods involved in the derivation of the empty clause by resolution. In [Lynce and Marques-Silva, 2004], a complete and exhaustive technique to extract smallest MUS is introduced. In [Oh et al., 2004], a DPLL-oriented approach has been presented that is based on a marked clauses concept to allow one to approximate MUS. In [Gr´egoire et al., 2006a], a heuristic-based incomplete approach to compute MUS has been introduced, which outperforms competing ones from a computational point of view.

Interestingly, in [Gr´egoire et al., 2006b] the same authors have introduced a concept of inconsistent cover to circumvent the possible intractable number of MUS, and presented a technique to compute such covers. Roughly, an inconsistent cover of an unsatisfiable SAT instance represents a set of MUS that covers enough independent causes of inconsistency that would allow the instance to regain consistency if they were repaired. Although an inconsistent cover does not provide us with the set of all MUS that may be present in a formula, it does however provide us with a series of minimal explanations of inconsistency that are sufficient to explain and potentially "fix" enough causes of inconsistency in order for the whole instance to regain consistency.

These latter techniques are incomplete ones in the sense that they do not necessarily deliver all MUS. However, in some application domains, it can be necessary to find the set of all MUS, because diagnosing infeasibility is hard, if not impossible, without a complete view of its causes [Liffiton and Sakallah, 2005]. Obviously enough, such techniques can only remain tractable provided that the number of MUS remains itself tractable. Likewise, the number of MSS and CoMSS can be exponential in the worst case. It should be noted that many domains in Artificial Intelligence like belief revision (e.g. [Bessant et al., 2001]) involve conceptual approaches to handle unsatisfiability that can require the complete sets of MUS, MSS, and CoMSS to be computed in the worst case, even when additional epistemological ingredients like stratification are introduced in the logical framework.

In this paper, the focus is on complete techniques. We introduce a new complete technique to compute all MUS, MSS and CoMSS of a SAT instance, provided obvious tractability limitations. It improves the currently most efficient complete technique, namely Liffiton and Sakallah'one [Liffiton and Sakallah, 2005] (in short L&S), which in turn was shown more competitive than previous approaches by Bailey and Stuckey [Bailey and Stuckey, 2005], and by de la Banda, Stuckey and Wazny [de la Banda et al., 2003], which were introduced in somewhat different contexts.

Our approach exhibits two main features. First, it is a hybridization of the L&S complete approach with a local search pretreatment. A local search technique is indeed used as an oracle to find potential CoMSS of the SAT instance, which are themselves hitting sets of MUS. We show that such a hybridization can yield exponential efficiency gains. Second, the efficiency of the approach relies on the crucial concept of critical clause, which appears to be a powerful ingredient of our technique to locate MUS.

The rest of the paper is organized as follows. First, the reader is provided with the necessary background about SAT, MUS and the dual concepts of MSS and CoMSS. Then, Liffiton and Sakallah's exhaustive approach is briefly presented. In Section 4, we show how this technique can be valuably hybridized with a local search pretreatment, making use of the critical clause concept. It is shown how this pretreatment can be theoretically valuable from a computational point of view. In Section 5, we compare this new approach with L&S.

2 Background

In this section, we provide the reader with the basic background about SAT, MUS, MSS and CoMSS.

Let L be the Boolean logical language built on a finite set of Boolean variables, noted a, b, c, etc. The ∧, ∨, ¬ and ⇒ symbols represent the standard conjunctive, disjunctive, negation and material implication connectives, respectively.

Formulas and clauses will be noted using upper-case letters such as C. Sets of formulas will be represented using Greek letters like Γ or Σ. An interpretation is a truth assignment function that assigns values from {true, false} to every Boolean variable. A formula is satisfiable when there is at least one interpretation (called model) that satisfies it, i.e. that makes it become true. An interpretation will be noted by upper-case letters like I and will be represented by the set of literals that it satisfies. Actually, any formula in L can be represented (while preserving satisfiability) using a set (interpreted as a conjunction) of clauses, where a clause is a finite disjunction of literals, where a literal is a Boolean variable that is possibly negated. SAT is the NP-complete problem that consists in checking whether a set of Boolean clauses is satisfiable or not, i.e. whether there exists an interpretation that satisfies all clauses in the set or not.

When a SAT instance is unsatisfiable, it exhibits at least one Minimally Unsatisfiable Subformula, in short one MUS.

Definition 1. A MUS Γ of a SAT instance Σ is a set of clauses s.t. Γ ⊆ Σ, Γ is unsatisfiable and ∀Δ ⊂ Γ, Δ is satisfiable.

Example 1. Let Σ = {a, ¬c, ¬b ∨ ¬a, b, ¬b ∨ c}. Σ exhibits two MUS, namely {a, b, ¬b ∨ ¬a} and {¬c, b, ¬b ∨ c}.

A dual concept is the notion of Maximal Satisfiable Subset (MSS) of a SAT instance.

Definition 2. A MSS Γ of a SAT instance Σ is a set of clauses s.t. Γ ⊆ Σ, Γ is satisfiable and ∀Δ ⊆ (Σ \ Γ) s.t. Δ ̸= ∅, Γ ∪ Δ is unsatisfiable.

The set-theoretical complement of a MSS w.r.t. a SAT instance is called a CoMSS.

Definition 3. The CoMSS of a MSS Γ of a SAT instance Σ is given by Σ \ Γ.

Example 2. Let us consider the formula Σ from the previous example. Σ exhibits five CoMSS: {b}, {¬c, a}, {¬c, ¬b∨¬a}, {¬b ∨ c, ¬b ∨ ¬a} and {¬b ∨ c, a}.

As shown by several authors [Liffiton and Sakallah, 2005], these concepts are correlated. Mainly, a CoMSS contains at least one clause from each MUS. Actually, a CoMSS is an irreducible hitting set of the set of MUS. In a dual way, every MUS of a SAT instance is an irreducible hitting set of the CoMSS. Accordingly, as emphasized by [Liffiton and Sakallah, 2005] although MINIMAL-HITTING-SET is a NP-hard problem, irreducibility is a less strict requirement than minimal cardinality. Actually, a MUS can be generated in polynomial time from the set of CoMSS.

3 Liffiton and Sakallah's Exhaustive Approach

Liffiton and Sakallah's approach [Liffiton and Sakallah, 2005] to compute all MUS (in short L&S) is based on the strong duality between MUS and MSS. To the best of our knowledge, it is currently the most efficient one. First it computes all MSS before it extracts the corresponding set of MUS. Here, the focus is on L&S first step since we shall improve it and adopt the second step as such.

L&S is integrated with a modern SAT solver and takes advantage of it. Roughly, every ith clause Ci = x1 ∨ ... ∨ xm of the SAT instance is augmented with a negated clause selector variable yi to yield C′ i = x1 ∨ ... ∨ xm ∨ ¬yi. While solving these new clauses, assigning yi to false has the effect of disabling or removing Ci from the instance. Accordingly, a MSS can be obtained by finding a satisfying assignment with a minimal number of yi variables assigned false. The algorithm makes use of a sliding objective approach allowing for an incremental search. A bound on the number of yi that may be assigned to false is set. For each value of the bound, starting at 0 and incrementing by 1, an exhaustive search is performed for all satisfiable assignments to the augmented formula C′ i , which will find all CoMSS having their size equal to the bound. Whenever one solution is found, it is recorded, and a corresponding clause forcing out that solution (and any supersets of it) is inserted. This blocking clause is a disjunction of the yi variables for the clauses in that CoMSS.

Before beginning the search with the next bound, the algorithm checks that the new instance augmented with all the blocking clauses is still satisfiable without any bound on the yi variables. If this formula is unsatisfiable, the entire set of CoMSS has been found and the algorithm terminates.

The second part of the algorithm computes the complete set of MUS from the set of CoMSS in a direct way. The approach that we shall introduce will include this second step as such.

4 Local Search and Critical Clauses

In this section, it is shown how the aforementioned exhaustive search algorithm can be improved in a dramatic manner by hybridizing it with an initial local search step, which provides valuable oracles for the subsequent exhaustive search process. We shall call the new approach HYCAM (HYbridization for Computing All Mus).

First, let us motivate our approach in an intuitive manner. Clearly, a (fast) initial local search run for satisfiability on the initial instance might encounter some actual MSS. Whenever this phenomenon happens, it can prove valuable to record the corresponding CoMSS in order to avoid computing them during the subsequent exhaustive search. Moreover, rather than checking whether we are faced with an actual MSS or not, it can prove useful to record the corresponding candidate CoMSS that will be checked later during the exhaustive search. Obviously enough, we must study which interpretations encountered during the local search process yield candidate MSS and criteria must be defined in order to record a limited number of potentially candidate CoMSS only. In this respect, a concept of critical clause will prove extremely valuable in the sense that it allows us to state necessary conditions for being a CoMSS that can be checked quickly. When all the remaining candidate CoMSS are recorded, the incremental approach by Liffiton and Sakallah allows us to exploit this information in a very valuable and efficient way. Let us describe this in a more detailed manner.

A local search algorithm is thus run on the initial SAT instance. The goal is to record as many candidate CoMSS as

Algorithm 1: Local Search approximation

Input: a CNF formula Σ Output: Set of candidate CoMSS begin 1 candidates ←- ∅ ; #fail ←- 0 ; 2 I ←- generate random interpretation() ; 3 while (#fail < PRESET #FAILURES AUTHORIZED) do 4 newcandidates ←- FALSE ; 5 for j = 1 to #FLIPS do 6 Let Δ be the set of falsified clauses by I ; 7 if ∀C ∈ Δ, C is critical 8 and Δ is not implied in candidates then 9 removeAllSetImplied(Δ,candidates) ; 10 candidates ←- Δ ∪ candidates ; 11 newcandidates ←- TRUE ; 12 flip(I) ; 13 if not(newcandidates) then #fail ←- #fail + 1; 14 return candidates ; 15 end 16

Algorithm 2: The HYCAM algorithm

Input: a CNF formula Σ Output: All MSS of Σ begin 1 cand ←- LS approximation(Σ) ; k ←- 0 ; 2 Σy ←- addSelectorClauses(Σ) ; MSS ←- ∅ ; 3 while SAT(Σy) do 4 removeAllSetImplied({Σ\C|C ∈MSS},cand) ; 5 Σy ←- addBlockingClausesOfSize(k,cand) ; 6 MSS ←- MSS ∪ {Σ\C|C ∈ cand and |C| = k} ; 7 MSS ←- MSS ∪ SAT with bound(k,Σy ) ; 8 k ←- k + 1 ; 9 returnMSS ; 10 end 11

possible, based on the intuitive heuristics that local search often converges towards local minima, which could translate possibly good approximations of MSS. A straightforward approach would consist in recording for each visited interpretation the set of unsatisfied clauses. Obviously enough, we do not need to record supersets of already recorded candidate CoMSS since they cannot be actual CoMSS as they are not minimal with respect to set-theoretic inclusion. More generally, we have adapted the technique proposed by Zhang in [Zhang, 2005] to sets of clauses in order to record the currently smaller candidate CoMSS among the already encountered series of sets of unsatisfied clauses. Now, crucial ingredients in our approach are the concepts of once-satisfied and critical clauses. The latter concept has already proved valuable for locating MUS and inconsistent covers using an incomplete technique based on local search [Gr´egoire et al., 2006a; 2006b].

Definition 4. A clause C is once-satisfied by an interpretation I iff exactly one literal of C is satisfied by I. A clause C that is falsified by the interpretation I is critical w.r.t. I iff the opposite of each literal of C belongs to at least one once-satisfied clause by I.

Intuitively, a critical clause is thus a falsified clause that requires at least another one to be falsified in order to become satisfied, performing a flip. Property 1 shows how this concept allows us to eliminate wrong candidate CoMSS.

Property 1. Let Σ be a SAT instance and let I be an interpretation. Let Γ be a non-empty subset of Σ s.t. all clauses of Γ are all falsified by I. When at least one clause of Γ is not critical w.r.t. I, then Γ is not a CoMSS of Σ.

Proof. By definition, when a clause Cf of Γ is not critical w.r.t. I, there exists at least one literal c ∈ Cf whose truthvalue can be inversed (i.e. flipped) without falsifying any other clause of Σ. Accordingly, Γ is not minimal and cannot be a CoMSS of Σ.

In practice, testing whether all falsified clauses are critical or not can be performed quickly and prevents many sets of clauses to be recorded as candidate CoMSS. Using these features, the local search run on the initial SAT instance yields a series of candidate CoMSS. This information proves valuable and allows us to boost L&S complete search.

L&S is incremental in the sense that it computes CoMSS of increasing sizes, progressively. After n iterations have been performed, all CoMSS of cardinality lower or equal than n have been obtained. Accordingly, if we have recorded candidate CoMSS containing n + 1 clauses, and if they are not supersets of already obtained CoMSS, we are sure that they are actual CoMSS. In this respect, we do not need to search them, and their corresponding blocking clauses can be inserted directly. Moreover, we do not need to perform the SAT test at the end of the n-th iteration, since we are then aware of the existence of larger CoMSS.

It is also easy to show that the insertion of these blocking clauses can allow both NP-complete and CoNP-complete tests to be avoided. Let us illustrate this on an example.

Example 3. Let Σ be the following unsatisfiable SAT instance and let Σ′ be the corresponding augmented SAT instance using L&S clauses selector variables yi.

Σ is an unsatisfiable SAT instance made of 13 clauses and making use of 5 variables. It exhibits 3 MUS, which are illustrated in Figure 1, and admits 19 MSS. Assume that both L&S and HYCAM are run on this instance. Its clauses are augmented by the ¬yi negated clause selector variables. Assume also that the local search performed by HYCAM provides 4 candidate CoMSS: {C5}, {C3,C2}, {C0,C1,C2} and {C3, C8, C10}.

If the branching variables are chosen based on the lexical order, then a and b are assigned to true and C5 is falsified. Thus, L&S tries to prove that this clause forms a CoMSS, which requires a NP-complete test (because it has to find a model of Σ\{¬a ∨ ¬b} ∪ {a, b}). On the contrary, when HYCAM is run, the blocking clause y5 is added before the first iteration of the complete algorithm is performed, since the local search has already delivered this CoMSS. In consequence, when a and b are assigned true, the DPLL-algorithm backtracks immediately as the {y5, ¬y5} unsatisfiable set has been obtained, without requiring any further NP-complete test.

Similarly, the introduction of additional clause selector variables by HYCAM can reduce the number of CoNPcomplete tests. For example, let us assume that e is the first branching variable, that e is assigned false and that the next variables are selected according to the lexical order. When a and b are assigned true, L&S tries to prove that {C5} is a CoMSS. Since ¬e is tautological consequence of Σ\{¬a ∨ ¬b} ∪ {a, b}, no model exists for Σ\{¬a ∨ ¬b} ∪ {a, b, ¬e}. Clearly, such a test is in CoNP. Thanks to the previously delivered candidate CoMSS, HYCAM avoids this part of the search space to be explored. Indeed, since we know that {C5} is a CoMSS, when a and b are assigned true, no further CoNP tests are performed with respect to this partial assignment.

In fact, from a computational point of vue, the preliminary non-expensive local search eliminates nodes in the search tree, avoiding both NP and CoNP tests.

5 Experimental Evaluation

HYCAM has been implemented and compared to L&S from a practical point of view. For both algorithms, the complete search step is based on the use of MiniSat [E´en and S¨orensson, 2004], which is currently one of the best modern SAT solvers. As a case study, we used Walksat [Kautz and Selman, 2004] for the local search pretreatment. The number of flips and tries of Walksat is related to the number of candidate CoMSS already found. For each try, a small number of flips is performed. If no new candidate is found during a try then a counter is incremented. When this counter exceeds a threshold (experimentally set to 30), we consider that no new candidate could be found by the local search. This way to end the local search pretreatment offers a good trade-off between the number of candidates found and the time spent. Besides, for all experiments, the time consumed by the local search step was less than 5% of the global time. All our experimental studies have been conducted on Intel Xeon 3GHz under Linux CentOS 4.1. (kernel 2.6.9) with a RAM memory size of 2Go. In the following, a time-out limit has been set to 3 CPU hours.

First, in Table 1a, we report experimental results about the computation of MSS on pigeon-hole and xor-chains benchmarks, which are globally unsatisfiable in the sense that removing any one of their clauses makes the instance become satisfiable. Obviously enough, such instances exhibit a number of CoMSS equals to their number of clauses, and the size of any of their CoMSS is one. A significant time gap can be observed in favor of HYCAM. The efficiency gain ratio is even more significant when the size of the instance increased. For these instances, the local search run often succeeds in finding all CoMSS, and the complete step often reduces to an unsatisfiability test. On the contrary, L&S explores many more nodes in the search space to deliver the CoMSS.

In Table 1b, experimental results on more difficult benchmarks from the annual SAT competition [SATLIB, 2000] are described. Their number of MSS is often exponential, and computing them often remains intractable. Accordingly, we have limited the search to CoMSS of restricted sizes, namely we have set a size limit to 5 clauses. As our experimental results illustrate, HYCAM outperforms L&S. For example, let us consider rand net40-30-10. This instance contains 5831 MSS (with the size of their corresponding CoMSS less than 5). L&S and HYCAM deliver this result in 1748 and 386 seconds, respectively. For the ca256 instance, HYCAM has extracted 9882 MSS in less than 5 minutes whereas L&S did not manage to produce this result within 3 hours. Let us note that HYCAM also delivers CoMSS made of 5 clauses after its computation is ended since we know that all sets of 5 falsified clauses recorded by the local search run and that are not supersets of the obtained smaller CoMSS are actually also CoMSS.

In Table 2, experimental results on hard instances to compute the complete set of MSS and MUS are reported. As explained above, both L&S and HYCAM approaches require all MSS to be obtained before MUS are computed. By allowing complete sets of MSS to be delivered in a shorter time, HYCAM allows the complete set of MUS to be computed for more instances and in a faster manner than L&S does. Obviously enough, when the number of MSS or MUS are exponential, computing and enumerating all of them remain intractable.

For instance, L&S was unable to compute all MSS of the php-012-011 instance within 3 hours CPU time, and could thus not discover its single MUS. HYCAM extracted it in 2597 seconds. On all instances exhibiting unique or a nonexponential number of MUS, HYCAM was clearly more efficient than L&S. For example, on the dlx2 aa instance, L&S and HYCAM discovered the 32 MUS within 3.12 and 0.94 seconds, respectively. Let us note that the additional time spent to compute all MUS from the set of MSS is often very small unless of course the number of MUS is exponential.

6 Conclusions and Future Research

Computing all MSS, CoMSS and MUS are highly intractable issues in the worst case. However, it can make sense to attempt to compute them for some real-life applications. In this paper, we have improved the currently most efficient exhaustive technique, namely Liffiton and Sakallah's method, in several ways. Our experimental results show dramatic efficiency gains for MSS, CoMSS and MUS extracting. One interesting feature of the approach lies in its anytime character for computing MSS. MSS of increasing sizes are computed gradually. Accordingly, we can put a bound on the maximum size of the CoMSS to be extracted, limiting the computing resources needed to extract them. To some extent, both L&S and HYCAM prove more adapted to extract complete sets of MSS and CoMSS than complete sets of MUS. Indeed, the procedure involves computing MSS (and thus CoMSS) first. In this respect, we agree with Liffiton and Sakallah that an interesting path for future research concerns the study of how MUS could be computed progressively from the growing set of extracted MSS.

Many artificial intelligence research areas have studied various problems involving the manipulation of MUS, MSS and CoMSS, like model-based diagnosis, belief revision, inconsistency handling in knowledge and belief bases, etc. These studies are often conducted from a conceptual point of view, or from a worst-case complexity point of view, only. We believe that the practical computational progresses as such as the ones obtained in this paper can prove valuable in handling these problems practically. In this respect, future research could concentrate on deriving specific algorithms for these AI issues, exploiting results like the ones described in this paper.

Acknowledgments

We thank Mark Liffiton for making his system available to us. This work has been supported in part by the R´egion Nord/Pasde-Calais.