Christophe Lecoutre
email: lecoutre@cril.fr

Olivier Roussel
email: roussel@cril.fr

Failed Value Consistencies for Constraint Satisfaction

In constraint satisfaction, basic inferences rely on some properties of constraint networks, called consistencies, that allow the identification of inconsistent instantiations (also called nogoods). Two main families of consistencies have been introduced so far: those that permit us to reason from variables such as (i, j)-consistency and those that permit us to reason from constraints such as relational (i, j)-consistency. This paper introduces a new family of consistencies based on the concept of failed value (a value pruned during search). This family is orthogonal to previous ones.

Introduction

Any user of a constraint solver ideally expects the system to be robust and clever enough to automatically identify all relevant properties of a problem instance. These properties typically depend on the structure of the instance and can help solving it. Some of the approaches to reach that goal are inferences from strong consistencies, adaptive heuristics, nogood recording and automatic symmetry breaking. They permit an efficient exploration of the search space, learning much useful information before or during search so as to avoid exploring fruitless combinations of values of variables.

Usually, backtrack search is used for solving instances of the Constraint Satisfaction Problem (CSP). Backtrack search combines a depth-first exploration to instantiate variables and a backtracking mechanism to deal with encountered dead-ends. During search, some values are proved to be inconsistent, i.e. not to participate to any solution -we call them failed values. Interestingly, it is known [START_REF] Freuder | Using inferred disjunctive constraints to decompose constraint satisfaction problems[END_REF] that failed values "convey" some information: given a satisfiable binary CSP instance P , for any pair (x, a) where x is a variable of P and a a value in the domain of x, if there is no solution containing a for x, then there is necessarily a variable y = x which is assigned a value b such that (y, b) is not compatible with (x, a). It is then possible to dynamically and iteratively decompose problem instances [START_REF] Freuder | Using inferred disjunctive constraints to decompose constraint satisfaction problems[END_REF][START_REF] Bennaceur | A decomposition technique for solving Max-CSP[END_REF].

In this paper, we propose to exploit failed values in a different manner. By locally reasoning from failed values, we show that some inferences can be performed within reasonable complexities. In particular, we develop a new family of domain-filtering consistencies based on failed values and show that they are complementary to (incomparable with) usual ones. They contribute to prune the search space and also offer a lazy detection of a generalized form of the substitutability relation. Algorithms checking or enforcing consistencies based on failed values can be naturally grafted to any constraint propagation engine in order to reinforce the filtering strength of the search algorithm. This approach may represent an interesting contribution to the quest for robust solvers.

After recalling some technical background, two basic consistencies, called FVC and AFVC and based on failed values, are presented. Next, algorithms for checking FVC and enforcing AFVC are introduced, and AFVC is compared to substitutability and usual consistencies. Finally, before presenting some preliminary experimental results, we show that an entire class of consistencies based on failed values can be naturally defined.

Technical Background

A constraint network (CN) P is composed of a finite set of n variables, denoted by vars(P ), and a finite set of e constraints, denoted by cons(P ). Each variable x has an associated domain, denoted by dom(x), that contains the finite set of values that can be assigned to x. Each constraint c involves a set of variables, called the scope of c and denoted by scp(c). It is defined by a relation, denoted by rel(c), which contains the set of tuples allowed for the variables involved in c. A binary constraint involves exactly 2 variables, and a non-binary constraint strictly more than 2 variables. For a binary constraint c xy such that scp(c xy ) = {x, y}, if (a, b) ∈ rel(c xy ), we say that (x, a) and (y, b) are compatible. We also say that (x, a) and (y, b) are compatible if there is no binary constraint between x and y.

In this paper, we shall consider given an initial CN P init and a current CN P derived from P init by potentially reducing variable domains. The initial domain of a variable x is denoted by dom init (x) whereas the current domain is denoted by dom P (x) or more simply by dom(x). A (current) value of P is a pair (x, a) with x ∈ vars(P ) and a ∈ dom(x). For any variable x, we always have dom(x) ⊆ dom init (x) and denote this fact by P P init . More generally, given two CNs P and P ′ , we note P ′ P iff P and P ′ are defined on the same set of variables and the same set of constraints, and for every variable x in vars(P ) = vars(P ′ ), we have dom P ′ (x) ⊆ dom P (x). P ′ ≺ P iff P ′ P and there exists a variable x such that dom P ′ (x) ⊂ dom P (x).

An instantiation I of a set X = {x 1 , . . . , x k } of variables is a set {(x 1 , a 1 ), . . . , (x k , a k )} such that ∀i, a i ∈ dom init (x i ) ; the set X of variables occurring in I is denoted by vars(I) and each value a i is denoted by I[x i ]. An instantiation I on a CN P is an instantiation of a set X ⊆ vars(P ) ; it is complete if vars(I) = vars(P ), partial otherwise. I is valid on P iff ∀(x, a) ∈ I, a ∈ dom(x) (= dom P (x)). I[x/a] is the instantiation obtained from I by replacing the value assigned to x in I by a. An instantiation I covers a constraint c iff scp(c) ⊆ vars(I), and satisfies a constraint c with scp(c) = {x 1 , . . . , x r } iff a) I covers c and b) the tuple (a 1 , . . . , a r ), such that ∀i, a i = I[x i ], is allowed by c, i.e. (a 1 , . . . , a r ) ∈ rel(c). An instantiation I on a CN P is locally consistent iff a) I is valid on P and b) every constraint of P covered by I is satisfied by I. It is locally inconsistent otherwise. A solution of P is a complete instantiation on P that is locally consistent. An instantiation I on a CN P is globally inconsistent, or a nogood, iff it cannot be extended to a solution of P . It is globally consistent otherwise.

A CN is said to be satisfiable iff it admits at least one solution. The Constraint Satisfaction Problem (CSP) is the NP-complete task of determining whether a given CN is satisfiable or not. A CSP instance is defined by a CN which is solved either by finding a solution or by proving unsatisfiability. To solve a CSP instance, a depth-first search algorithm with backtracking can be applied, where at each step of the search, a variable assignment is performed followed by a filtering process called constraint propagation. Typically, constraint propagation algorithms are based on some properties of CNs that allow us to identify and remove some values which cannot occur in any solution. Such properties are called domain-filtering consistencies [START_REF] Debruyne | Domain filtering consistencies[END_REF][START_REF] Bessiere | Domain filtering consistencies for non-binary constraints[END_REF].

Let us introduce some classical consistencies. An instantiation I on P is a support (resp. a conflict) for a value (x, a) on a constraint c involving x iff I is valid, I[x] = a and I satisfies (resp. does not satisfy) c. A value (x, a) of P is GAC-consistent (GAC stands for Generalized Arc Consistency) iff there exists a support for (x, a) on every constraint of P involving x. P is GAC-consistent iff every value of P is GACconsistent. For binary CNs, GAC is referred to as AC (Arc Consistency). For any CN P , we know that there exists a greatest GAC-consistent network, denoted by GAC (P ) and called the GAC-closure of P , which is equivalent to P and such that GAC (P ) P . When the domain of a variable of P is empty, P is clearly unsatisfiable, which is denoted by P = ⊥. The CN P | x=a is obtained from P by removing every value b = a from dom(x). A value (x, a) of P is SAC-consistent (SAC stands for Singleton Arc Consistent) iff GAC (P | x=a ) = ⊥. P is SAC-consistent iff every value of P is SACconsistent.

Any domain-filtering consistency allows us to identify and remove inconsistent values. In order to compare the pruning capability of different consistencies, we can introduce a preorder [START_REF] Debruyne | Domain filtering consistencies[END_REF]. Let φ and ψ be two consistencies. φ is stronger than ψ, denoted by φ ψ, iff whenever φ holds on a CN P , ψ also holds on P . φ is strictly stronger than ψ, denoted by φ ⊲ ψ iff φ ψ and there exists at least one CN P such that ψ holds on P but not φ. When some consistencies cannot be ordered (none is stronger that the other), we say that they are incomparable. For classical domain-filtering consistencies defined on binary CNs, we have: SAC ⊲ MaxRPC ⊲ PIC ⊲ AC (MaxRPC and PIC are respectively Max-Restricted Path Consistency and Path Inverse Consistency, see [START_REF] Bessiere | Constraint propagation[END_REF]).

Consistencies based on Failed Values

In this section, we present two new basic consistencies. The first identifies nogoods of any size whereas the second identifies inconsistent values (i.e. nogoods of size 1). These two consistencies are based on failed values which are simply values proved to be inconsistent (e.g. during search). Failed values "convey" some information: Lemma 1 (directly derived from [START_REF] Freuder | Using inferred disjunctive constraints to decompose constraint satisfaction problems[END_REF]). If a value (x, a) of a CN P is globally inconsistent then every solution S of P is such that S[x/a] violates at least one constraint of P involving x.

Proof. S[x/a] is not a solution of P since (x, a) is globally inconsistent. This means that at least one constraint of P is not satisfied by S[x/a]. But we know that every constraint c of P that does not involve x is satisfied by S[x/a] because the restriction of S[x/a] over scp(c) is exactly the restriction of S over scp(c). Consequently, at least one constraint of P involving x is not satisfied by S[x/a].

2

If P is a binary CN, then every solution of P contains a value for a variable y = x which is not compatible with (x, a). A failed value is defined as follows:

Definition 1. Let P and P ′ be two CNs such that P ′ ≺ P . A failed value of P ′ with respect to P is a value (x, a) of P such that P | x=a is unsatisfiable and a / ∈ dom P ′ (x) .

In practice, a failed value is a value pruned from a CN because it has been proved to be inconsistent. At any time during search, a failed value can be identified by inference and/or search methods [START_REF] Dechter | Constraint processing[END_REF][START_REF] Lecoutre | Constraint networks: techniques and algorithms[END_REF]. For example, if P init | x=a is shown to be unsatisfiable, clearly, a can be removed from dom init (x). We then obtain a smaller CN P with (x, a) being a failed value of P (with respect to P init ). However, note that failed values can be defined with respect to any intermediate CN reached during search. We need now to introduce conflict sets.

Definition 2. Let P be a CN, x be a variable of P and a ∈ dom init (x).

-The conflict set of (x, a) on a constraint c of P involving x, denoted by χ P (c, x, a), is the set of valid instantiations

I of scp(c) \ {x} on P such that I ∪ {(x, a)} does not satisfy c. -The conflict set of (x, a) on P is χ P (x, a) = ∪ c∈cons(P )|x∈scp(c) χ P (c, x, a).
For every conflict set χ, vars(χ) = ∪ I∈χ vars(I). When possible, we simplify χ P (x, a) into χ(x, a). Note that a failed value verified by an instantiation is not necessarily covered by it. However, it is shown below that when a failed value is covered by an instantiation but not verified, a nogood is identified. FVC (Failed Value Consistency) is a general nogood-identifying consistency.

Definition 4. Let P be a constraint network.

-A valid instantiation I on P is FVC-consistent for a failed value (x, a) of P iff either (x, a) is not covered by I or (x, a) is verified by I. -A valid instantiation I on P is FVC-consistent iff it is FVC-consistent for every failed value of P ; otherwise, I is said to be FVC-inconsistent.

Assume that (w, c) in Figure 1 is a failed value.

I = {(x, a), (y, c), (z, c)} is an instantiation that verifies (w, c) because I contains {(y, c), (z, c)} ∈ χ(w, c). I ′ = {(x, a)} does not verify (w, c) but is FVC-consistent for (w, c) because (w, c) is not covered by I ′ . I ′′ = {(x, a), (y, a), (z, a)} is FVC-inconsistent because (w, c
) is both covered by I ′′ and not verified by I ′′ .

Proposition 1. Any FVC-inconsistent instantiation is globally inconsistent.

Proof. Without any loss of generality, we consider here that I is a valid instantiation on a constraint network P that is FVC-inconsistent for a failed value (x, a) of P with respect to P init ; we have P ≺ P init . We know that there is no solution of P init involving (x, a) because (x, a) is a failed value of P wrt P init . We can even say more: for every solution S of P init , the complete instantiation S[x/a] is not a solution because at least one constraint involving x is violated (see Lemma 1). Because I is FVC-inconsistent for (x, a), we know that I covers vars(χ P (x, a)) and (x, a) is not verified by I. This means that it is not possible to extend I into a complete instantiation I ′ on P such that I ′ [x/a] violates at least one constraint involving x. Every solution of P is a solution of P init (since P ≺ P init ) and every solution S of P init is such that S[x/a] violates at least one constraint involving x. We can deduce that I is globally inconsistent.

2

Otherwise stated, some nogoods can be identified via deleted values (that are themselves nogoods). These nogoods are not necessarily of size 1. For example, in Figure 2 there is a failed value (w, a) and three binary constraints involving w. Any valid instantiation of {x, y, z} is globally inconsistent if it only contains values compatible with (w, a). In other words, every tuple in

C x × C y × C z is a nogood (of size 3).
Interestingly, inference can be conducted differently by reasoning between each value and each failed value (through its conflict set). More precisely, we can define a related domain-filtering consistency, called Arc Failed Value Consistency (AFVC). -A value (x, a) of P is AFVC-consistent iff (x, a) is AFVC-consistent for every failed value of P ; otherwise, (x, a) is said to be AFVC-inconsistent. -P is AFVC-consistent iff every value of P is AFVC-consistent.

For the first item above, note that we may have x = y. In this case, necessarily, we have a = b since (x, a) is a current value whereas (y, b) is a pruned one. Note that AFVC can be regarded as a local consistency since it suffices to reason from the conflict set of each failed value. In particular for binary constraints, a value (x, a) is AFVC-consistent for a failed value (y, b) iff (x, a) is compatible with a valid value in χ(y, b). The AFVC algorithm given in Section 4 is based on this simple observation.

Proposition 2. Any AFVC-inconsistent value is globally inconsistent.

Proof. Let (x, a) be a current value of P that is AFVC-inconsistent for a failed value (y, b) of P . Suppose that there exists a solution S of P such that S[x] = a. Necessarily, as (x, a) is AFVC-inconsistent for (y, b), S[y/b] cannot violate any constraint involving y, and consequently is a solution of P . This contradicts the fact that (y, b) is globally inconsistent (since it is a failed value), and consequently our hypothesis. We can deduce that (x, a) is globally inconsistent.

2

As an illustration, let us consider the CN (partially) depicted in Figure 3. This CN can be completed (see dots) so that some classical consistencies hold (e.g. arc consistency). We assume here that (w, a) is a failed value and χ(w, a) = {{(x, a)}, {(y, c)}}. Restricted to nogoods of size 1, FVC is strictly weaker than AFVC (the proof is omitted). We have:

Proposition 3. Let (x, a) be a value of P . If I = {(x, a)} is FVC-inconsistent then (x, a) is AFVC-inconsistent.
Finally, one can show that AFVC verifies certain properties (e.g. see [START_REF] Apt | Principles of Constraint Programming[END_REF][START_REF] Bessiere | Constraint propagation[END_REF][START_REF] Lecoutre | Constraint networks: techniques and algorithms[END_REF]) that permits us to define the AFVC-closure. Proposition 4. For any CN P , there exists a greatest AFVC-consistent CN equivalent to P , called the AFVC-closure of P and denoted by AFVC (P ), such that AFVC (P ) P .

AFVC (P ) can be obtained by iteratively removing, in any order, values that are not AFVC-consistent.

Algorithms for FVC and AFVC

We propose to embed filtering algorithms based on failed values within MAC (Maintaining Arc Consistency) [START_REF] Sabin | Contradicting conventional wisdom in constraint satisfaction[END_REF]. MAC is a backtrack search algorithm that develops a binary search tree: at each node, an uninstantiated variable x is selected, a value a in dom(x) is selected, a left subtree starting with a branch labelled with the positive decision x = a (variable assignment) is first explored and a right subtree starting with a branch labelled with the negative decision x = a (value refutation) is later explored. The consistency enforced at each node is GAC.

For binary CNs, an immediate solution to make use of FVC is to post, for each failed value (x, a), a non-binary constraint whose scope is vars(χ(x, a)): its associated relation forbids any instantiation FVC-inconsistent for (x, a). For our example in Figure 2, we would obtain a ternary constraint c xyz such that rel(c xyz ) = dom(x)×dom(y)× dom(z) \ C x × C y × C z . Interestingly, one may conceive efficient filtering algorithms (propagators) to enforce GAC on such constraints. However, this approach is intrusive and its generalization to non-binary CNs is rather complex. This is why we propose a weakened approach for the general case: checking FVC at each node of the search tree by checking that no identified failed value is currently covered and unverified. To identify failed values during search, it suffices to keep the set F of negative decisions labelling the current branch (i.e. the branch leading from the root of the search tree to the current node). Note that failed values that correspond to values removed when enforcing GAC can be discarded because these failed values are always verified (as long as no domain wipe-out occurs): for each of these values, there exists a constraint with only conflicts.

To check FVC, Algorithm 1 is called. For each failed value, we seek a conflict; seekConflict(c, x, a) seeks a conflict for (x, a) on c. When a conflict is found for a failed value (x, a), it is stored in a backtrack-stable data structure called res; this plays the role of residues as in [START_REF] Lecoutre | A study of residual supports in arc consistency[END_REF] when establishing GAC. The validity of the residual conflict is first tested at line 3. When no conflict exists for a failed value, f alse is returned, We now propose an algorithm to enforce the domain-filtering consistency AFVC on binary constraint networks. Given a binary CN P with a set of failed values F , the procedure enforceAFVC (see Algorithm 2) computes AFVC (P ) and returns f alse when a domain wipe-out occurs. The data structures are as follows. For each failed value (x, a), χ(x, a) is considered to be an array of values indexed from 1 to length(χ(x, a)). These values correspond to the instantiations (of size 1 since P is binary) in the conflict set of (x, a). The 2-dimensional array last maps each pair composed of a failed value (x, a) in F and a value (y, b) of P to an an integer corresponding to the index of the most recent value found in χ(x, a) that is present in P and compatible with (y, b): last[(x, a)][(y, b)] indicates the position of the last found (so-called) AFVC-support for (y, b) on (x, a). For each value (z, c) of P , S(z, c) is a list storing the pairs (failed value,value) for which (z, c) is the last found AFVC-support. Structures S and last are inspired from those used in AC6 and AC2001 (see e.g. [START_REF] Bessiere | Constraint propagation[END_REF]).

Certainly, dynamically computing (or updating) conflict sets at each node would be prohibitive. This is why we consider that conflict sets are computed for the initial problem instance by the call initialize(P init ). In practice, it may be worthwhile to bound the number of failed values and/or to bound the maximum size of conflict sets by a constant in order to concentrate only on promising failed values. If both are bound, the complexity becomes O(nd). The algorithm presented above can be easily adapted to be used at each node of the search tree developed by MAC (the complexity remains the same for a branch of the search tree).

Substitutability and Usual Consistencies

Neighborhood substitutability is a weak form of substitutability [START_REF] Freuder | Eliminating interchangeable values in constraint satisfaction problems[END_REF] that can be related to consistencies based on failed values. A value a ∈ dom(x) is neighborhood substitutable for a value b ∈ dom(x) iff for every constraint c involving x and every support I for (x, b) on c, I[x/a] is a support for (x, a) on c. For example, it can be exploited as a reduction operator by applying a convergent sequence of neighborhood substitution deletions [START_REF] Cooper | Fundamental properties of neighbourhood substitution in constraint satisfaction problems[END_REF]. We have the following interesting proposition. Proof. The definition of neighborhood substitutability can be reformulated as: (x, a) is neighborhood substitutable for (x, b) iff χ(x, a) ⊆ χ(x, b). If (x, a) is a failed value of P , then it is not possible to extend (x, b) into a consistent instantiation that verifies (x, a). (x, b) is then AFVC-inconsistent.

2

AFVC can be seen as a lazy dynamic mechanism to detect values that can be substituted (and are globally inconsistent). Importantly, it allows us to identify inconsistent values for which no neighborhood substitutable value exists. Indeed, a value (x, b) is AFVC-inconsistent if the conflict set of (x, b) is included in the conflict set of a failed value. However, whereas only values for the same variable are considered for neighborhood substitutability, AFVC is more general. An illustration is given in Figure 3: (w,a) is substitutable for (w, b) but not for (z, a) since w = z.

Interestingly, AFVC is incomparable with most of the domain-filtering consistencies. More precisely, it is incomparable with "usual" consistencies, i.e. local consistencies φ that do not rely on failed values and that verify the four basic properties: a) φ holds on any CN only involving entailed constraints (a constraint is entailed on P iff it is satisfied by every valid instantiation on its scope), b) φ holds on any CN iff it holds on each of its connected sub-networks, c) there exist unsatisfiable CNs where φ holds and d) there exist some CNs where φ does not hold. For example, (G)AC, SAC, PIC, . . . are "usual" but global consistency (defined as: any locally consistent instantiation can be extended to a solution) is not usual. Proposition 6. AFVC is incomparable with usual consistencies.

Proof. Let us consider a "usual" local consistency φ. Let us consider a (satisfiable) CN P 1 that only contains entailed constraints, a CN P 2 , unsatisfiable but φ-consistent, on a separate set of variables, and the problem P = P 1 ∪ P 2 . Since P 2 is unsatisfiable, any value (x, a) of P 1 can be identified as a failed value (e.g. after search). We now assume that (x, a) is a failed value of P 1 . Since P 1 contains only entailed constraints, χ(x, a) = ∅ and therefore, no instantiation can verify (x, a). Thus, P is not AFVCconsistent. In contrast, φ holds on P (by hypothesis), hence φ ⊲ AFVC. Besides, AFVC ⊲ φ: it suffices to choose a CN P with no failed value such that φ does not hold. Consequently, AFVC and φ are incomparable. 2

A Hierarchy of Consistencies

In [START_REF] Freuder | A sufficient condition for backtrack-bounded search[END_REF], Freuder introduced the general class of (i, j)-consistencies. Informally, a constraint network is (i, j)-consistent iff every locally consistent instantiation of a set of i variables can be extended to a locally consistent instantiation involving any j additional variables. Arc consistency, path consistency [START_REF] Montanari | Network of constraints : Fundamental properties and applications to picture processing[END_REF][START_REF] Mackworth | Consistency in networks of relations[END_REF] and path inverse consistency (PIC) [START_REF] Freuder | Neighborhood inverse consistency preprocessing[END_REF] all belong to this class since they correspond to (1, 1)-consistency, (2, 1)consistency and (1, 2)-consistency, respectively. Another important class of consistencies defined in terms of (existing) constraints is that of relational (i, m)-consistencies [START_REF] Dechter | Local and global relational consistency[END_REF]. Informally, a constraint network is relational (i, m)-consistent iff for every set C of m constraints and every set X ⊆ Y of i variables, where Y = ∪ c∈C scp(c), every locally consistent instantiation of X can be extended to a valid instantiation of Y satisfying each constraint of C. Generalized arc consistency and relational path-inverseconsistency [START_REF] Bessiere | Domain filtering consistencies for non-binary constraints[END_REF] respectively correspond to relational (1, 1)-consistency and relational (1, 2)-consistency.

Here, we propose a new general class of original consistencies, based on the concept of failed value. Definition 6 (Failed Value (i, f )-consistency). P is FV(i, f )-consistent iff for every set X of i variables of P and every set Y of f failed values of P , every locally consistent instantiation of X can be extended to a locally consistent instantiation verifying each failed value in Y . In order to show the practical interest of consistencies based on failed values, we have performed experiments with our constraint solver Abscon. On a computer equipped with a 3GHz processor and 2GB of RAM under Linux, MAC was employed with dom/ddeg and lexico as variable 2 and value ordering heuristics, as our baseline. We first compared, on binary instances, MAC with MAC embedding the procedure (see Algorithm 1) that checks FVC at each search step (denoted by MAC+FVC) and also with MAC embedding a function that enforces AFVC at each search step (denoted by MAC+AFVC). For our preliminary tests, we have implemented a less sophisticated version of Algorithm 2. This algorithm does enforce AFVC but is quite simpler (and theoretically less efficient) as it does not integrate last and S structures. Table 1 shows the results obtained on some binary instances 3 with these three backtrack search variants in terms of CPU time and number of visited nodes. Because dom/ddeg is a non-adaptive heuristic, we have the guarantee that MAC+FVC visits less nodes than MAC and that MAC+AFVC visits less nodes than MAC+FVC. In Table 1, for some instances, the number of visited nodes is significantly reduced when consistencies based on failed values are used. MAC+FVC is clearly the most efficient algorithm since it is usually better than MAC+AFVC and sometimes one order of magnitude faster than MAC alone. Interestingly, reasoning from failed values allows us to benefit from the structure (related to substitutability for graph coloring and job-shop instances) contained in these instances. On some other series of instances (not presented here) including random ones, MAC+FVC does not prune the search tree. However, we have observed that this is never penalizing in terms of CPU time. This is because the worst-case time complexity of checking FVC is limited and the number of failed values is usually small. Although one may be disappointed by the relative inefficiency of MAC+AFVC, one should consider that a non optimized AFVC algorithm has been used here and that many developments to control the complexity of AFVC (or even stronger consistencies) remain to be studied.

Table 2 shows the results obtained on some series of non-binary instances. Clearly, MAC+FVC outperforms MAC alone. Finally, note that MAC+FVC was used in Abscon during the third constraint solver competition 4 with good results.

Conclusion

In this paper, we have shown how values detected as globally inconsistent during search, and called failed values, can be useful to prune the search space through the introduction of a new class of consistencies that are orthogonal to the usual ones. Whereas FVC is a consistency that is cheap to check and that makes MAC more robust, AFVC and its direct extensions require further developments to determine the best way of controlling the enforcement of these new domain-filtering consistencies. We have also noticed that AFVC allows us to detect in a lazy manner a generalized form of neighborhood substitutability.

Although it is related to approaches that eliminate redundancies by posting constraints (for SAT) [START_REF] Purdom | Solving satisfiability with less searching[END_REF][START_REF] Gallo | Algorithms for testing the satisfiability of propositional formulae[END_REF] or decomposing problems [START_REF] Freuder | Using inferred disjunctive constraints to decompose constraint satisfaction problems[END_REF], this way of reasoning has been developed so as to yield a hierarchy of increasingly stronger consistencies. For binary constraint networks, failed values basically permit us to identify and exploit a form of nogood in the same spirit as generalized nogood in [START_REF] Katsirelos | Generalized nogoods in CSPs[END_REF], global cut seed in [START_REF] Focacci | Global cut framework for removing symmetries[END_REF], kernel [START_REF] Razgon | A CSP search algorithm with responsibility sets and kernels[END_REF] and partial state [START_REF] Lecoutre | Exploiting past and future: Pruning by inconsistent partial state dominance[END_REF]. We believe that identifying common properties to these different approaches is an exciting perspective.

Figure 1 Fig. 1 .Definition 3 .

 113 Fig. 1. Illustration of conflict sets.

Definition 5 .

 5 Let P be a constraint network.-A value (x, a) of P is AFVC-consistent for a failed value (y, b) of P iff (x, a) can be extended to a locally consistent instantiation verifying (y, b).

Fig. 2 .

 2 Fig. 2. A failed value (w, a), its compatible values in Cx, Cy and Cz and its incompatibles values in Ix, Iy and Iz.

Fig. 3 .

 3 Fig. 3. Illustration of AFVC

4 foreach 5 τ 6 if τ = nil then 7 res

 4567 function checkFailedValue(P : CN, (x, a): failed value):Boolean constraint c of P such that x ∈ scp(c) do ← seekConflict(c, x, a) P : CN, F : set of failed values):Boolean 12 begin 13 foreach failed value (x, a) ∈ F do 14 if ¬checkFailedValue(P, (x, a)) Checking FVC which forces the search algorithm to backtrack. The worst-case space complexity of this algorithm is O(nd) whereas its worst-case time complexity is O(|F |ed r-1 ) where |F | denotes the number of failed values in F , e the number of constraints, d the greatest domain size and r the greatest constraint arity. For binary constraint networks, the worst-case time complexity is only O(|F |ed).

1 begin 2 foreach 4 S 9 end 10 function 12 position

 12491012 The function enforceAFVC tries to identify an AFVC-support for each pair (failed value,value). If no support can be found for a value (y, b) on a failed value (x, a), b is removed from dom(y) and (y, b) is added to the propagation queue Q. Each removed value (z, c) ∈ Q is "propagated": a new sup-procedure initialize(P : binary CN) value (x, a) of P do 3 χ(x, a) ← ∅ (x, a) ← ∅ 5 foreach constraint cxy of P do 6 foreach tuple (a, b) ∈ dom(x) × dom(y) | (a, b) / ∈ rel(cxy) do 7 add (x, a) to χ(y, b) 8 add (y, b) to χ(x, a) seekAFVCSupport((x, a): failed value, (y, b): value): Boolean 11 begin ← last[(x, a)][(y, b)] + 1 13 while position ≤ length(χ(x, a)) do 14 (z, c) ← χ(x, a)[position] 15 if c ∈ dom(z) ∧ (y, b) and (z, c) are compatible then 16 last[(x, a)][(y, b)] ← position 17 add ((x, a), (y, b)) to S(z, c) P : binary CN, F : set of failed values): Boolean value (x, a) ∈ F do 26 foreach value (y, b) of P do 27 last[(x, a)][(y, b)] ← 0 28 if ¬seekAFVCSupport((x, a), (y, b)) then 29 remove b from dom(y) 30 if dom(y) = ∅ then 31 return false 32 add (y, b) to Q 33 while Q = ∅ do 34 pick and delete (z, c) from Q 35 foreach ((x, a), (y, b)) ∈ S(z, c) do 36 if b ∈ dom(y) ∧ ¬seekAFVCSupport((x, a), (y, b)) then 37 remove b from dom(y) Enforcing AFVC port must be found for each pair stored in S(z, c) (this is done from the last recorded position). The worst-case space and time complexities of enforceAFVC are O(nd(M + |F |)) and O(M |F |nd) respectively, where n is the number of variables, d the greatest domain size, |F | the number of failed values and M the maximum size of a conflict set (M = max (x,a)∈P init |χ(x, a)|). Indeed, the space required by χ arrays is O(ndM ), and that required by both last and S is O(|F |nd). On the other hand, the cumulated complexity of seekAFVCSupport for each pair (failed value,value) is O(M ), and there are O(|F |nd) different pairs. Note that initialize has a O(ed 2 ) time complexity but this is amortized since initialize is only called initially (for P init ). By definition, |F | < nd and M < nd hence M |F |nd < n 3 d 3 .

Proposition 5 .

 5 If a value (x, a) is neighborhood substitutable for a value (x, b) on a CN P ′ ≻ P , if (x, a) is a failed value of P and if (x, b) is a value of P then (x, b) is AFVC-inconsistent.

FromProposition 7 .Fig. 4 .

 74 Fig. 4. AFVC holds but neither SAFVC nor PIFVC holds.

Figure 5 Fig. 5 .

 55 Figure 5 summarizes the relations between domain-filtering consistencies based on failed values. Due to lack of space, proofs are omitted.

Table 1 .

 1 Impact of checking FVC and enforcing AFVC on binary instances.

			MAC	MAC+FVC	MAC+AFVC
	Instance	CPU	nodes	CPU	nodes	CPU	nodes
	Graph coloring
	1-fullins-4-4	106	7M 934	4.8	215, 812	5.6	110, 636
	2-fullins-4-4	10.7	177, 424	4.8	67, 924	2.3	12, 764
	2-insertions-4-3	10.5	455, 533	3.2	112, 886	5.4	62, 753
	2-insertions-5-3	3.1	7, 767	1.8	3, 494	2.4	2, 941
	Composed
	composed-25-5	178	10M 864	85	4M 838	148	2M 333
	composed-25-7	106	7M 934	4.78	215, 812	5.6	110, 636
	Job-shop
	os-taillard-4-100-1	84	1M 870	30.2	247, 383	83	206, 845
	os-taillard-4-100-3	7.6	147, 270	2.3	29, 698	3.0	17, 818
	os-taillard-4-95-2	7.5	195, 665	3.3	51, 957	19.7	41, 226
	Queen Attacking
	qa-5	7.5	318, 601	6.4	240, 495	10.0	238, 940
	qa-6	311	7M 703	259	5M 883	443	5M 576

Table 2 .

 2 Impact of checking FVC on non-binary instances.

			MAC	MAC+FVC
	Instance	CPU	nodes	CPU	nodes
	Dimacs
	hole-08	5.8	0M 699	1.9	0M 177
	hole-09	80	9M 062	16	1M 753
	aim-100-1-6-sat-3	21.4	3M 173	5.01	0M 505
	aim-100-1-6-sat-4	160	22M 400	47.1	5M 292
	Renault-mod
	renault-mod-15	505	1M 969	118	0M 511
	renault-mod-18	1, 193	6M 812	253	1M 419
	renault-mod-43	796	4M 221	23	0M 127
	renault-mod-45	85.5	0M 591	15.5	89, 494

In each figure of this paper, solid (resp. dashed) edges represent allowed (resp. forbidden) tuples. The absence of edges between two variables means that there is no binary constraint involving them.

Using dom/wdeg does not guarantee exploring the same search tree when additional filtering is performed. This is why we have chosen dom/ddeg.

Available at http://www.cril.fr/ ˜lecoutre/research/benchmarks/

See http://www.cril.univ-artois.fr/CPAI08/


Cédric Piette
email: piette@cril.fr

Youssef Hamadi
email: youssefh@microsoft.com

Lakhdar Saïs
email: sais@cril.fr

Efficient Combination of Decision Procedure for MUS Computation

In recent years, the problem of extracting a MUS (Minimal Unsatisfiable Subformula) from an unsatisfiable CNF has received much attention. Indeed, when a Boolean formula is proved unsatisfiable, it does not necessarily mean that all its clauses take part to the inconsistency; a small subset of them can be conflicting and make the whole set without any solution. Localizing a MUS can thus be extremely valuable, since it enables to circumscribe a minimal set of constraints that represents a cause for the infeasibility of the CNF. In this paper, we introduce a novel, original framework for computing a MUS. Whereas most of the existing approaches are based on complete algorithms, we propose an approach that makes use of both local and complete searches. Our combination is empirically evaluated against the current best techniques on a large set of benchmarks.

Introduction

The concept of Minimally Unsatisfiable Subformula (MUS for short) proves more and more valuable in many applications of SAT, such as bounded model checking (see e.g. [START_REF] Mcmillan | Automatic abstraction without counterexamples[END_REF][START_REF] Gupta | Iterative abstraction using SAT-based BMC with proof analysis[END_REF]) or knowledge-base validation. Indeed, when a Boolean formula is proved unsatisfiable, it does not necessarily mean that all its clauses take part to the inconsistency; a small subset of them can be conflicting and make the whole set without any solution. Localizing a MUS can thus be extremely valuable, since it enables to circumscribe a minimal set of constraints that represents a cause for the infeasibility of a CNF formula. For instance, in [START_REF] Bryant | Deciding bit-vector arithmetic with abstraction[END_REF], an abstraction-based approach for deciding the satisfiability of finite-precision bit-vector is presented. Roughly, this method consists in generating an under-approximation such that if this latter one is satisfiable, so is the original problem. In the opposite case, an approximation of MUS (also called core) of this CNF formula is computed for generating an over-approximation whose unsatisfiability proves that the original problem has no solution. Experimental results clearly show that this way is more efficient than running a complete DPLL-like procedure on the whole original formula.

SAT solving has made a wonderful progress in the recent years, and some problems considered out-of-reach a decade ago can now be solved in a few seconds. A natural consequence of those algorithmic improvements is the modeling of larger problems whose reasons for unsatisfiability can be very difficult to catch. One way to explain inconsistency is to extract a Minimally Unsatisfiable Subformula, which represents an irreducible (w.r.t. the involved clauses) cause of the unsatisfiability. With the recent increase in formulae sizes, the problem of extracting one or several MUS has received much attention these last years. However, the current approaches which are based on complete search algorithms (DPLLs) often deliver an unsatisfiable subformula, which is not guaranteed to be minimal. Among these techniques, let us mention AMUSE [START_REF] Oh | AMUSE: a minimally-unsatisfiable subformula extractor[END_REF] which consists in marking clauses during the exploration of a DPLL-related search tree. Another technique called zCore [START_REF] Zhang | Extracting small unsatisfiable cores from unsatisfiable boolean formula[END_REF], the core extractor related to the well-known solver zChaff, is able to localize an unsatisfiable subformula by analyzing the resolution graph of a complete search procedure. Indeed, the source clauses from which is derived the empty one by the resolution process, simulated by modern solvers, forms a non-minimal core of the CNF formula.

More recently, a new technique called AOMUS [START_REF] Gregoire | Extracting MUSes[END_REF] has also been introduced. It makes an original use of local search and relies on a so-called critical clause concept, to progressively focus on the difficult parts of a problem. This allows AOMUS to compute the upper-approximation of a MUS. Finally, an approach based on a serie of redundancy checks is presented in [START_REF] Van Maaren | Finding guaranteed MUSes fast[END_REF]. Let us also note that the problem of finding a Minimal Unsatisfiable Core (MUC) in the CSP framework is also the subject of many publications [START_REF] Hemery | Extracting MUCs from constraint networks[END_REF][START_REF] Junker | QuickXplain: Preferred explanations and relaxations for overconstrained problems[END_REF].

Although these approaches are based on different algorithmic principles, they are destructive by nature, in the sense that they consider the whole formula to remove parts which have been shown useless in a particular proof of unsatisfiability. In this paper, we are concerned with a new constructive framework. Indeed, this approach starts without any clause and builds a core by adding some particular clauses regularly, until an unsatisfiable set of clauses (which represents an approximated MUS) has been obtained. This framework makes an incomplete search -in charge of delivering sets of models -and an exhaustive technique act together. This can be opposed to destructive approaches which often imply the ability to prove a CNF unsat before starting a core extraction process. For applications like MaxSat solving through detection of cores [START_REF] Marques-Silva | Algorithms for maximum satisfiability using unsatisfiable cores[END_REF], this could be an issue, though. Our constructive method does not suffer from this drawback, as it only requires to check the unsatisfiability of the discovered core instead of repetitively proving the whole CNF and some of its suformulae inconsistent.

To reduce the number of calls to a complete DPLL solver, our combination exploits the power of stochastic local search (SLS) for both finding models (proving the consistency of the current subformula) and for selecting the set of relevant clauses that might be added to the current subformula. A call to a complete solver is only done when the SLS method is not able to prove the consistency of the formula.

The paper is organized as follows. After some preliminary definitions and notations about SAT and MUS, we describe in section 3 the constructive framework. In section 4, an implementation of the framework is presented and experimented in section 5. Finally, we conclude by providing some interesting future lines of research.

Technical Beackground

Let L be the propositional language of formulas defined in the usual inductive way from a set P of propositional symbols (represented using plain letters like a, b, c, etc.), the Boolean constants ⊤ and ⊥, and the standard connectives ¬, ∧, ∨, ⇒ and ⇔. A SAT instance is a propositional formula in conjunctive normal form (CNF for short), i.e. a conjunction of clauses, where a clause is a disjunction of literals, a literal being a possibly negated propositional variable.

An interpretation is a function that assigns values from {true, f alse} to every Boolean variable. An interpretation is called model w.r.t. a particular CNF if it satisfies this formula, namely if this interpretation makes it true. SAT is the well-known NP-complete problem that consists in deciding whether a propositional CNF is satisfiable or not, i.e. whether the formula admits at least one model. In this paper, CNF formulae are represented using a set (interpreted as a conjunction) of clauses, where a clause is a set (interpreted as a disjunction) of literals.

When a CNF is satisfiable, most of the current approaches are able to provide a model, which is a certificate of its satisfiability. By opposite, in case of inconsistency, these approaches only ensure that no satisfying interpretation exists. However, this is not very informing. The user might prefer to localize, if there exists, a small part of the CNF which triggers the inconsistency of the whole problem. In this respect, the concept of MUS (Minimally Unsatisfiable Subformula) is extremely valuable.

Definition 1. Let Σ be a CNF formula. Γ is a MUS (Minimally Unsatisfiable Subformula) of Σ iff: 1. Γ ⊆ Σ; 2. Γ is unsatisfiable; 3. for each Γ ′ ⊂ Γ , Γ ′ is satisfiable.
Extracting of MUS from an unsatisfiable CNF is a highly complex problem. For instance, checking if a CNF is a MUS is DP-complete [START_REF] Papadimitriou | Computational Complexity[END_REF] (where DP is the class composed of the union of a language in NP and another one in CoNP), while checking whether a set of clauses belongs to at least one MUS of an unsatisfiable CNF is Σ p 2 -hard [START_REF] Eiter | On the complexity of propositional knowledge base revision, updates and counterfactual[END_REF]. Despite these not encouraging complexity results, many approaches for extracting a core (i.e. an approximated MUS) have already been proposed. In the next section, we propose a new constructive framework to extract cores from unsatisfiable formulae.

A Constructive Framework

Presentation

Most of the current approaches are destructive, in the sense that they consider the whole formula to progressively reduce it toward a core. In order to present the ideas of this new framework in comparison to the destructive one, we introduce here some notations that will be used in the remaining of this paper. First of all, let us denote Σ the CNF from which a MUS (or an approximation) is to be extracted. We also denote Γ another set of clauses which will contain the computed core. This set contains at any step of the procedure a subset of original formula Σ. Generally, the algorithms for computing a MUS are based on the iteration of the same function. So, let f be a function that takes Σ and Γ as input to produce a subformula Γ N .

With destructive methods, Γ is initially set to Σ. In addition, f is a function that takes Σ and Γ as input to produce a subformula Γ N of Γ , the most often by analyzing a proof of unsatisfiability. The resulting CNF Γ N is then a subset of Γ . This new CNF is then used as Γ with respect to f , to obtain a potentially even smaller CNF. This iteration is performed until the delivered formula is Γ itself, namely until a fix point is reached.

For the constructive method, we propose to start the computation considering Γ as the empty set, and to progressively add clauses from Σ in Γ . So, a core is built thanks to f which returns a superset Γ N of Γ which contains new clauses from Σ\Γ . This operation is repeated until Γ becomes unsatisfiable and represents a core for Σ. The following table summarizes the main differences between those general frameworks.

Constructive

Destructive

Initial Γ ∅ Σ f (Σ,Γ )=Γ N Γ ⊆ Γ N and Γ N ⊆ Σ Γ N ⊆ Γ Stopping Condition Γ is UNSAT f (Σ,Γ )=Γ
Actually, constructive procedures have already been studied for the problem of minimizing an unsatisfiable system toward a minimal one, in order to extract an exact cause of its infeasibility. For example, this approach is known for a long time in the mathematical programming [START_REF] Chinneck | Feasibility and viability[END_REF] and CSP [START_REF] De Siqueira | Explanation-based generalisation of failures[END_REF] communities. However, it is not used in practice any more, because of its complexity in the worst case. Indeed, by considering the number of calls to a complete procedure and denoting n the number of constraints of the CNF, and c n the number of constraints of the biggest MUS (in number of constraints), the constructive approach exhibits a worst case complexity in O(n × c n ), whereas the worst case complexities of destructive and dichotomic approaches are only O(n) and O(log(n) × c n ) [START_REF] Hemery | Extracting MUCs from constraint networks[END_REF], respectively.

Fortunately, this is only true for systematic complete procedures that aim at returning a minimal set of clauses; in this paper, we focus on approaches that aim at approximating a MUS (delivering an upper set of clauses). Consequently, they do not suffer from this bad complexity result. In the next section, we discuss about particular clauses that can be safely added to Γ without discarding any MUS of the formula.

The role of necessary clauses

In a recent study which aims at categorizing the clauses of a formula w.r.t. their role in its unsatisfiability [START_REF] Kullmann | Categorisation of clauses in conjunctive normal forms: Minimally unsatisfiable sub-clause-sets and the lean kernel[END_REF], different classes of clauses have been established. Roughly, a clause is called necessary if it belongs to all MUS of a formula. Clearly, those clauses participate to any proof of inconsistency, and removing any one of them makes the CNF recover satisfiability. A clause is potentially necessary if it is not a necessary clause but the removal of some particular clause(s) can make it necessary. Those clauses appear in at least one MUS of the formula. Finally, a clause which is neither necessary nor potentially necessary is never necessary and does not belong to any MUS. They can be used in a proof of unsatisfiability, but all of them can be removed from the CNF keeping it unsatisfiable.

Necessary clauses are computationally hard to be extracted: indeed, for an unsatisfiable CNF Σ and a clause c ∈ Σ, if Σ\{c} is satisfiable, then c is necessary with respect to Σ. A linear number of calls of a complete algorithm is thus needed to exhaustively extract all necessary clauses of a given CNF. Fortunately, an inexpensive technique [START_REF] Gregoire | Extracting MUSes[END_REF] can find them in an incomplete way. During the exploration of a local search for the satisfiability of Σ, if all its clauses are satisfied except one, the falsified clause is clearly necessary and is marked as protected. As necessary clauses represent global minima for the objective function of the local search, this notion proves really efficient for most of benchmarks, in an empirical point of view. Actually, most of the necessary clauses can be computed through the protected clause concept on many instances, but the approach cannot ensure they have all been delivered.

Nevertheless, an unsatisfiable CNF can exhibit no necessary clause. Indeed, containing two independent causes of unsatisfiability, namely two MUS with an empty intersection, is a sufficient condition for not exhibiting such clauses. However, most of realistic CNF which are expected to be satisfiable are not of this form. As said previously, a necessary clause of a formula belongs to any of its MUS and can therefore be safely added to Γ , in our constructive framework.

The main difference between destructive procedures is the strategy used to select the subset of clauses of Γ (represented previously by the function f ). With respect to a constructive policy, a lot of possible techniques can also be imagined for augmenting Γ . However, when f only considers particular clauses to be added, interesting properties can be established. The interest of such particular functions are described in the next section.

The non-redundancy property

Our technique is based on the following proposition, which is a straight consequence of the definition of MUS itself: Proposition 1. Let Σ be a CNF formula, and ω an interpretation of

Σ. ∀M ∈ Σ s.t. M is a MUS, ∃c ∈ M s.t. ω c.
Clearly enough, as a MUS is an irreductible unsatisfiable set of clauses, any interpretation of a formula falsifies at least one clause from each of its MUSes. Accordingly, when considering a large number of interpretations, the most often falsified clauses are heuristically a good approximation of clauses belonging to MUSes. The highest score clauses are then added to the growing core. Thus, we associate a score (initialized to 0) to each clause, and while a large number of interpretations are considered, the score of each falsified clause is increased by 1.

A lot of different constructive algorithms can be created, choosing various strategies to enumerate interpretations. Those ones can be randomly generated, but it appears reasonable to attempt to reduce the number of clauses falsified by the explored interpretations. Indeed, some falsified clauses may not appear in any MUS and are just "noise" for the heuristic. Attempting to reduce the number of falsified clauses limits this phenomenon. Hence, meta-heuristics designed for optimisation problems (simulated annealing, genetic algorithms, etc.) can be used in this context.

Moreover, if the scoring function only considers falsified clauses of Σ with respect to models of Γ , then the following proposition ensures that no clause redundant with Γ can be added to this set of clauses. Those redundant clauses are clearly superfluous when considering the growing core.

if f Sω (Σ, Γ ) ⊆ Γ ∪ {c ∈ Σ\Γ | ∃ω ∈ S ω s.t. ω Γ and ω c} then ∄c ∈ (f (Σ, Γ )\Γ ) such that Γ c.
Thus, within this condition, it is not possible for our constructive policy to add to the built core, the clauses which are redundant with Γ , namely clauses which "cover" the same part of the search space. This feature is obviously not shared by destructive methods. However, if f enables to add several clauses at the same time, a subset of them can clearly be redundant with another one in conjunction of Γ . Nevertheless, this is only possible for clauses added at the same time. The number of added clauses after each iteration can be tuned through the definition of f itself. If it is small, a bigger number of iterations would be necessary to construct a core, but this one would exhibit a good quality. In the opposite, with a big number of clauses added, only a few iterations are sufficient to obtain a core, but it will probably not be fine-grained. This property makes the constructive approaches very flexible, since it provides a parameter that represents a trade off between the quality of the obtained core and the time spent for its computation. Destructive approaches cannot propose to the user such a parameter. Let us illustrate the non-redundancy property through an example.

Example 1. Let Σ be a CNF formula made of 13 clauses, involving 4 variables such that:

Σ =                    c 1 : (¬a ∨ c ∨ d) c 2 : (a ∨ b ∨ c) c 3 : (¬a ∨ ¬b ∨ c) c 4 : (c ∨ ¬d) c 5 : (¬a ∨ ¬c ∨ d) c 6 : (¬b ∨ d) c 7 : (a ∨ ¬c ∨ d) c 8 : (a ∨ ¬b ∨ ¬c) c 9 : (b ∨ ¬c) c 10 : (¬b ∨ ¬c ∨ ¬d) c 11 : (a ∨ ¬c ∨ ¬d) c 12 : (a ∨ c ∨ d) c 13 : (¬a ∨ b ∨ ¬d)
The search space induced by those 4 variables is represented through a Karnaugh map in Figure 1a, together with each clause of Σ falsified by the different possible interpretations. Let us note that Σ is clearly unsatisfiable, since every interpretation is falsified by at least one clause of the CNF. As an example, ω 1 = {¬a, b, c, d} falsifies the clauses c 8 and c 10 .

Let us note that some interpretations are only falsified by a unique clause. For instance, ω 2 = {¬a, b, ¬c, d} is only violated by c 4 . Accordingly, this clause is necessary [START_REF] Kullmann | Categorisation of clauses in conjunctive normal forms: Minimally unsatisfiable sub-clause-sets and the lean kernel[END_REF], since without it, ω 2 would become a model of Σ. c 4 thus participates to all sources of inconsistency of Σ and belongs to all its MUS. Σ exhibits two other necessary clauses, which are c 1 and c 9 . Indeed, we can observe in Figure 1a that there exists at least one interpretation which is only "covered" (i.e. falsified) by one of these clauses.

Assume that those necessary clauses are first computed, as presented previously. Γ is then set to Γ = {c 1 , c 4 , c 9 }. Consequently, only the models of this latter CNF are now considered for selecting the other clauses of Σ. The set of models of Γ = {c 1 , c 4 , c 9 } is represented in Figure 1b using white cells, the interpretations that falsify this CNF being in gray. For instance, the clauses c 3 and c 13 cannot be added to Γ any more, since they are falsified iff at least one necessary clause is also falsified. Hence, they do not belongs to any MUS of Σ. With destructive methods, proofs of inconsistency can use these clauses which can then be present in the delivered core.

Thus, if f only considers the falsified clauses of Σ with respect to models of Γ , then c 12 would be candidate to the built core and in this case would also prevent c 2 and c 6 from being added in the future, since these latter clauses cannot be falsified w.r.t. a model of Γ ∪ {c 12 }.

However, if f enables to add simultaneously several clauses, c 2 and c 12 could be both added to Γ , whereas c 2 is a logical consequence of Γ ∪ {c 12 } (c 2 covers an underset of interpretations covered by Γ ∪ {c 12 } in Figure 1a). Moreover, the traditional approaches aiming at extracting a MUS, or an approximation, from an unsatisfiable CNF delivers an arbitrary one, based on the refutation proof obtained. However, a propositional formula can contain several MUS (actually an exponential number of MUS in the worst case), and the user might prefer to extract a core that contains specific information, or clauses. Such a computation can be very useful: as an example, in FPGA routing task, in order to check if a particular part of the circuit is involved in the inroutability of the layout. Classical approaches cannot perform such a computation, and the only way to do this until now was to use a complete procedure, namely an approach that computes the exhaustive set of MUS, like [START_REF] Gregoire | Boosting a complete technique to find mss and mus thanks to a local search oracle[END_REF] does, for instance.

The constructive policy which respects the non-redundancy property offers such a choice to the user by guiding a search toward a specific core. To this purpose, instead of starting the computation with the empty formula, it suffices to begin with the chosen clauses. Let us denote ∆ the set of clauses selected by the user to build a core. As shown previously, some clauses can be redundant w.r.t. the rest of the formula, and the constructive approach ensures that none of them can be added by the algorithm. Hence, by setting the first set of clauses to ∆, no other constraint redundant with it can be considered by the procedure. The following example shows the interest and the limitation of this kind of approach.

Example 2. Let us consider the CNF presented in the Example 1. Assume the user wants to compute a core involving the set of clauses {c 1 , c 3 , c 8 , c 12 }.

First, c 1 is a necessary clause, and thus belongs to all MUS/cores of Σ On the opposite, c 3 is a never necessary clause (w.r.t. the terminology of [START_REF] Kullmann | Categorisation of clauses in conjunctive normal forms: Minimally unsatisfiable sub-clause-sets and the lean kernel[END_REF]) and does not belongs to any MUS. Consequently, the user's choice implies a nonoptimal construction of core. c 8 and c 12 are potentially necessary clauses, and belong to at least one MUS of the CNF. By adding those clauses before the first iteration, assuming that the 3 necessary clauses are first detected, Γ contains the clauses {c 1 , c 3 , c 4 , c 8 , c 9 , c 12 }. Using this "partial core", the only clauses that can be falsified with respect to these models are c 5 , c 6 , c 10 and c 11 , and some of them will then be added to Γ to construct a core. If c 5 and c 11 are selected, the resulting core can only be minimized by removing c 3 and all the clauses chosen by the user (except this last one) do participate to the computed MUS. Unfortunately, the potential choice of c 6 and c 10 to start the core construction would make c 8 redundant, and not belong to all its MUS. This example shows the constructive approach's flexibility. It enables the enduser to guide the computation toward a specific core, and might be driven by the user's expertise on the problem. Clearly, the proposed process is not limited to the initial core, and different user-interactions during the construction of the core can be imagined. However, this is done without ensuring that the chosen clauses will actually be a part of all MUS of this core. We believe that this incomplete computation is a good tradeoff in front of the very high complexity of such a problem. Indeed, assuming P = N P , we cannot expect the development of an efficient complete procedure, since checking whether a formula belongs to the set of MUS of an unsatisfiable SAT instance is in Σ p 2 (a consequence of theorem 8.2 of [START_REF] Eiter | On the complexity of propositional knowledge base revision, updates and counterfactual[END_REF]). In the next section, we present a first implementation of this constructive approach which uses local search for adding new clauses to Γ .

A First Implementation: constructMUS

In this section, we present a particular implementation of the constructive framework that respects the non-redundancy property. The function f is based on local search for choosing clauses to be added. Initially, this stochastic technique is used for extracting protected clauses, and initialize Γ [START_REF] Gregoire | Extracting MUSes[END_REF].

We then perform multiple runs of a local search on Γ and consider the discovered models. We then consider the falsified clauses of Σ and increment a related score, initially set to 0 for each clause. As at least one clause of each set that could complement Γ to form a MUS is falsified, it suffices to consider the clauses that have obtained the highest score and add them to the approximation of the MUS. Accordingly, at the end of the incomplete procedure, Γ is augmented with these "high-score clauses" and these operations are repeated, searching models to the new set of clauses.

This process is iterated until no model can be found to the growing formula Γ . However, due to the incomplete nature of the local search, this computed set of clauses is not guaranteed to be unsatisfiable, even if in practice this case occurs quite often. To ensure the completeness of this algorithm, when the local search fails to find a model of Γ , we run a DPLL complete method on this formula. If Γ is proved unsatisfiable, then Γ is returned as the computed MUS approximation. Otherwise, a model ω which represents a certificate of the satisfiability of Γ , is discovered by the complete approach; in this case, the model is used by the local search as its first explored interpretation, ensuring at least one model will be discovered. Moreover, as local search has not found a model previously, this means that this part of the search space has probably not been explored by the incomplete method. Forcing the model as the seed enables to diversify the search, and to find other "close" models.

With these features, the proposed constructive algorithm is sound for the problem of extracting an unsatisfiable subformula from any CNF. This approach is synthesized in the Algorithm 1. As explained previously, the considered "core" Γ is initially set of the empty formula, and only clauses found necessary (in a very cheap way) through the protected clause concept (line 4) are added. A flag call_DP LL is set initially to f alse, which implies the computation of a sample of models of Γ by a local search call (line 14). The p most falsified clauses of the remaining part of the formula are added to Γ (lines [START_REF] Eén | Minisat home page[END_REF][START_REF] Mcmillan | Applications of Craig interpolants in model checking[END_REF]. Let us note that this parameter plays a role in the quality of the core and in the runtime of the procedure, since it provides the number of added clauses at each iteration. These operations are iterated until no model can be found by LS to Γ .

If no model is found by LS, then the flag call_DP LL is set to true (line 16) and a complete approach is run on Γ (line 8). If Γ is unsatisfiable, it is returned as the computed core; in the opposite case, a model is found by the procedure and is used as a "seed" in the next call of the local search (line 11). In the next section, this first implementation of the constructive framework is empirically evaluated.

Algorithm 1: construct_MUS

Input: an unsatisfiable CNF: Σ Output: a core of Σ: Γ begin 1 call_DP LL ← f alse ;

Experiments

In order to assess the ability of the proposed constructive framework to efficiently extract cores, we have implemented the ideas described in the previous sections, and compared them to three state-of-the-art approaches on various instances from SATLIB and the SAT competitions. As a case study, we have used the RSAPS [START_REF] Hutter | Scaling and probabilistic smoothing: Efficient dynamic local search for SAT[END_REF] local search. For the complete approach, Minisat [START_REF] Eén | Minisat home page[END_REF] has been chosen, since it is recognized by the community as one of the best complete solver. Based on empirical tuning, the parameter p of constructMUS procedure has been set to (1 + #cla Σ × 3%) and the flips limit devoted to the local search runs at each iteration of the algorithm has been set to ((1 + #cla Γ ) × 100), where #cla Σ is the number of clauses of Σ not added to Γ , and #cla Γ the number of clauses of the current sub-formula Γ .

We compare constructMUS to 3 state-of-the-art approaches: zCore [START_REF] Zhang | Extracting small unsatisfiable cores from unsatisfiable boolean formula[END_REF], AMUSE [START_REF] Oh | AMUSE: a minimally-unsatisfiable subformula extractor[END_REF] and AOMUS [START_REF] Gregoire | Extracting MUSes[END_REF]. The Table 1 reports these experiments. For each result, the size (in terms of number of clauses) of the delivered approximation of MUS is reported together with the time needed for the computation. Moreover, for those two values, the best obtained one is given in bold. All experiments have been 1: Experimental evaluation of a constructive implementation conducted on Pentium IV, 3 Ghz with 1 GB of memory, and for each tested benchmark, a 10,000 seconds timeout has been respected. First of all, only AMUSE cannot succeed to precisely localize in a few seconds the single MUS of the {23,42}.shuffled benchmarks, which come from bounded model checking. These ones actually encode formal verification of the open-source Sun PicoJava II microprocessor, and as emphasized in [START_REF] Mcmillan | Applications of Craig interpolants in model checking[END_REF], the discovered MUS enables to identify the relevant components of the system for the checked property. We also have performed some experimental tests on various benchmarks from the graph coloring problem ({3,4}col-*). On those CNFs, the finding of a core enables to localize a sub-graph that cannot be colored with the given number of colors, and make the whole problem infeasible. The constructive approach appears to be the best when we consider the size of the returned sub-formula. In addition, this result is obtained in a reasonable time, even if generally AMUSE provides a rougher core in a shorter time. As an example, for 4col100_9_8, constructMUS extracts a 1455-clause core in less than 6 minutes whereas zCore only localizes a core made of 1618 clauses in about one hour and a half. AMUSE and AOMUS provide sets of 1510 and 1502 clauses in 1 and 23 minutes, respectively. Let us note that on this family of benchmarks, our constructive method is systematically more accurate than the destructive ones.

More generally, our results show that this first implementation of the algorithm constructMUS delivers very satisfying results on various CNF, compared to state-of-the-art approaches (see e.g. hwb-*, gt-*). However, AOMUS appears to be a very good approach for some industrial problems (homer), while DPLLbased procedures are more adapted on various families, that the am_*_* one. Consulting the presented results, the developed approach is validated, but let us note that the four tested methods deliver orthogonal results with respect to the considered CNF. Each one of them appears the best appropriate technique for some families of benchmarks, but no one clearly outerperforms the others. Obviously, the fact that the result is here multi-criterion (size of the approximation and run time) is not helpful for the comparison.

In [START_REF] Gershman | Deriving small unsatisfiable cores with dominators[END_REF], it is suggested to use the notion of velocity, which is defined as the ratio between the size of the delivered core and the time needed for the computation. This element enables to know how many clauses are "eliminated" per second, then to know the best approach. However, this choice is not completely satisfying. Indeed, let us assume that a CNF formula exhibits 2 MUS that contain a different number of clauses. Is a method which extracts exactly the bigger MUS less efficient that another one which delivers roughly the smaller one (and then, a smaller set of clauses) ?

Deciding the best approach is still intrinsically a problem, that appears to be difficult to deal with objectively without considering any particular application domain. Nevertheless, the behaviour of our implementation appears to be very satisfying for various benchmarks, in comparison to the "best" current approaches. This added to its flexibility (parameter to control the precision, possibility to start with a guess) makes it very interesting as a new general framework for MUS extraction.

Conclusion

In this paper, an original framework called constructive has been presented for the problem of computing an approximated MUS, or core. The presented technique is based on a combination of a local search procedure and an exhaustive DPLL-like algorithm. It exhibits interesting features. For instance, it does not need to be able to solve the whole CNF for extracting a core; moreover, the pro-cedure gives rooms to user's expertise and allows him to guide the search toward a specific core. This is not possible with classical approaches that always compute arbitrary cores. Preliminary experiments show that in many cases, an instance of this framework proves competitive, and can outperform previous approaches. Particularly, our implementation delivers very satisfying results in terms of the size of core.

This first implementation opens many interesting perspectives. The concept of a critical clause, presented in [START_REF] Gregoire | Extracting MUSes[END_REF], has been proved useful for another localsearch-based extractor. This concept cannot be used as such, due to the nature of the approach, but a possible adaptation could improve the accuracy of the delivered core. Other hybridizations of this constructive framework, based for instance on a genetic algorithm for providing sets of models, are also planned as further works. Finally, a combination of a constructive and a destructive approaches could also be explored to combine the best of both worlds.

Proposition 2 .

 2 Let us consider the CNF formulae Σ, Γ and the function f Sω defined previously in the constructive context. f Sω depends on a set of explored interpretations S ω . The following proposition holds:

Fig. 1 :

 1 Fig. 1: Graphical representation of example 1

2 Γ ← ∅ ; 3 Γ 4 Σ ← Σ\Γ ; 5 while true do 6 if call_DP LL then 7 if 14 Sω 15 if 18 Φ 19 Γ ← Γ ∪ Φ ; 20 Σ

 2345671415181920 ← search_protected_clauses() ; ← LS_finds_models(Γ ,seed) ; Sω = ∅ then 16 call_DP LL ← true ; 17 else ← select_most_falsified_clauses(Σ, Sω, p) ; ← Σ\Φ ; 21 end 22