Christophe Lecoutre
email: lecoutre@cril.fr

Lakhdar Saïs
email: sais@cril.fr

Sébastien Tabary
email: tabary@cril.fr

Vincent Vidal
email: vincent.vidal@onera.fr

Reasoning from Last Conflict(s) in Constraint Programming

Constraint programming is a popular paradigm to deal with combinatorial problems in artificial intelligence. Backtracking algorithms, applied to constraint networks, are commonly used but suffer from thrashing, i.e. the fact of repeatedly exploring similar subtrees during search. An extensive literature has been devoted to prevent thrashing, often classified into look-ahead (constraint propagation and search heuristics) and lookback (intelligent backtracking and learning) approaches. In this paper, we present an original look-ahead approach that allows to guide backtrack search toward sources of conflicts and, as a side effect, to obtain a behavior similar to a backjumping technique. The principle is the following: after each conflict, the last assigned variable is selected in priority, so long as the constraint network cannot be made consistent. This allows us to find, following the current partial instantiation from the leaf to the root of the search tree, the culprit decision that prevents the last variable from being assigned. This way of reasoning can easily be grafted to many variations of backtracking algorithms and represents an original mechanism to reduce thrashing. Moreover, we show that this approach can be generalized so as to collect a (small) set of incompatible variables that are together responsible for the last conflict. Experiments over a wide range of benchmarks demonstrate the effectiveness of this approach in both constraint satisfaction and automated artificial intelligence planning.

Introduction

The backtracking algorithm (BT) is a central algorithm for solving instances of the constraint satisfaction problem (CSP). A CSP instance is represented by a constraint network, and solving it usually involves finding one solution or proving that none exists. BT performs a depth-first search, successively instantiating the variables of the constraint network in order to build a solution, and backtracking, when necessary, in order to escape from dead-ends. Many works have been devoted to improve its forward and backward phases by introducing look-ahead and look-back schemes. The forward phase consists of the processing to perform when the algorithm must instantiate a new variable. One has to decide which variable assignment to perform and which propagation effort to apply. The backward phase consists of the processing to perform when the algorithm must backtrack after encountering a dead-end. One has to decide how far to backtrack and, potentially, what to learn from the dead-end.

The relationship between look-ahead and look-back schemes has been the topic of many studies. Typically, all the efforts made by researchers to propose and experiment sophisticated look-back and look-ahead schemes are related to thrashing. Thrashing is the fact of repeatedly exploring the same (fruitless) subtrees during search. Sometimes, thrashing can be prevented by the use of an appropriate search heuristic or by an important propagation effort, and sometimes, it can be explained by some bad choices made earlier during search.

Early in the 90's, the Forward-Checking (FC) algorithm, which maintains during search a partial form of a property called arc consistency (which allows to identify and remove some inconsistent values), associated with the dom variable ordering heuristic [START_REF] Haralick | Increasing tree search efficiency for constraint satisfaction problems[END_REF] and the look-back Conflict-directed BackJumping (CBJ) technique [START_REF] Prosser | Hybrid algorithms for the constraint satisfaction problems[END_REF], was considered as the most efficient approach to solve CSP instances. Then, Sabin and Freuder [START_REF] Sabin | Contradicting conventional wisdom in constraint satisfaction[END_REF] (re-)introduced the MAC algorithm which fully maintains arc consistency during search, while simply using chronological backtracking. This algorithm was shown to be more efficient than FC and FC-CBJ, and CBJ was considered as useless to MAC, especially, when associated with a good variable ordering heuristic [START_REF] Bessiere | MAC and combined heuristics: two reasons to forsake FC (and CBJ?) on hard problems[END_REF].

Then, it became unclear whether both paradigms were orthogonal, i.e. counterproductive one to the other, or not. First, incorporating CSP look-back techniques (such as CBJ) to the "Davis-Putnam" procedure for the propositional satisfiability problem (SAT) renders the solution of many large instances derived from real-world problems easier [START_REF] Bayardo | Using CSP look-back techniques to solve real-world SAT instances[END_REF]. Second, while it is confirmed by theoretical results [START_REF] Chen | Conflict-directed backjumping revisited[END_REF] that the more advanced the forward phase is, the more useless the backward phase is, some experiments on hard, structured problems show that adding CBJ to MAC can still present significant improvements. Third, refining the look-back techniques [START_REF] Ginsberg | Dynamic backtracking[END_REF][START_REF] Bacchus | Extending Forward Checking[END_REF][START_REF] Jussien | Maintaining arc-consistency within dynamic backtracking[END_REF] by associating a so-called eliminating explanation (or conflict set) with every value rather than with every variable gives to the search algorithm a more powerful backjumping capability. The empirical results in [START_REF] Bacchus | Extending Forward Checking[END_REF][START_REF] Jussien | Maintaining arc-consistency within dynamic backtracking[END_REF] show that MAC can be outperformed by algorithms embedding such look-back techniques.

More recently, the adaptive heuristic dom/wdeg has been introduced [START_REF] Boussemart | Boosting systematic search by weighting constraints[END_REF].

This heuristic is able to orientate backtrack search towards inconsistent or hard parts of a constraint network by weighting constraints involved in conflicts. As search progresses, the weight of constraints difficult to satisfy becomes more and more important, and this particularly helps the heuristic to select variables appearing in the hard parts of the network. It does respect the fail-first principle: "To succeed, try first where you are most likely to fail" [START_REF] Haralick | Increasing tree search efficiency for constraint satisfaction problems[END_REF]. The new conflictdirected heuristic dom/wdeg is a very simple way to reduce thrashing [START_REF] Boussemart | Boosting systematic search by weighting constraints[END_REF][START_REF] Hulubei | Search heuristics and heavy-tailed behaviour[END_REF][START_REF] Lecoutre | Backjump-based techniques versus conflict-directed heuristics[END_REF].

Even with an efficient look-ahead technique, there still remains situations where thrashing occurs. Consequently, one can still be interested in looking for the reason of each encountered dead-end as finding the ideal ordering of variables is intractable in practice. A dead-end corresponds to a sequence of decisions (variable assignments) that cannot be extended to a solution. A deadend is detected after enforcing a given property (e.g. arc consistency), and the set of decisions in this sequence is called a nogood. It may happen that a subset of decisions of the sequence forms a conflict, i.e. is a nogood itself. It is then relevant (to prevent thrashing) to identify such a conflict set and to consider its most recent decision called the culprit decision. Indeed, once such a decision has been identified, we know that it is possible to safely backtrack up to it -this is the role of look-back techniques such as CBJ and DBT1 (Dynamic Backtracking) [START_REF] Ginsberg | Dynamic backtracking[END_REF].

In this paper, an extended revised version of [START_REF] Lecoutre | Last conflict-based reasonning[END_REF], we propose a general scheme to identify a culprit decision from any sequence of decisions leading to a dead-end through the use of a pre-established set of variables, called testing-set. The principle is to determine the largest prefix of the sequence, from which it is possible to instantiate all variables of the testing-set without yielding a domain wipe-out2 , when enforcing a given consistency. One simple policy that can be envisioned to instantiate this general scheme is to consider, after each encountered conflict, the variable involved in the last taken decision as the unique variable in the testing-set. This is what we call last-conflict based reasoning (LC).

LC is an original approach that allows to (indirectly) backtrack to the culprit decision of the last encountered dead-end. To achieve it, the last assigned variable X before reaching a dead-end becomes in priority the next variable to be selected as long as the successive assignments that involve it render the network inconsistent. In other words, considering that a backtracking algorithm maintains a consistency φ (e.g. arc consistency) during search, the variable ordering heuristic is violated, until a backtrack to the culprit decision occurs and a singleton φ-consistent value for X is found (i.e. a value can be assigned to X without immediately leading to a dead-end after applying φ).

We show that LC can be generalized by successively adding to the current testing-set the variable involved in the last detected culprit decision. The idea is to build a testing-set that may help backtracking higher in the search tree. With this mechanism, our intention is to identify a (small) set of incompatible variables, involved in decisions of the current branch, with many interleaved irrelevant decisions. LC allows to avoid the useless exploration of many subtrees.

Interestingly enough, contrary to sophisticated backjumping techniques, our approach can be very easily grafted to any backtrack search algorithm with a simple array (only a variable for the basic use of LC) as additional data structure. Also, this approach can be efficiently exploited in different application domains 3 . In particular, the experiments that we have conducted with respect to constraint satisfaction and automated planning [START_REF] Ghallab | Automated Planning, Theory and Practice[END_REF] demonstrate the general effectiveness of last-conflict based reasoning.

The paper is organized as follows. After some preliminary definitions (Section 2), we introduce the principle of nogood identification through testing-sets (Section 3). Then, we present a way of reasoning based on the exploitation of the last encountered conflict (Section 4) as well as its generalization to several conflicts (Section 5). Next, we provide (Section 6) the results of a vast experimentation that we have conducted with respect to two domains: constraint satisfaction and automated planning, before some conclusions and prospects.

Technical Background

A constraint network (CN) P is a pair (X , C ) where X is a finite set of n variables and C a finite set of e constraints. Each variable X ∈ X has an associated domain, denoted by dom(X), which contains the set of values allowed for X. Each constraint C ∈ C involves an ordered subset of variables of X , called scope of C and denoted by scp(C), and has an associated relation, denoted by rel(C), which contains the set of tuples allowed for its variables. The arity of a constraint is the number of variables it involves. A constraint is binary if its arity is 2, and non-binary if its arity is strictly greater than 2. A binary constraint network is a network only involving binary constraints while a non-binary constraint network is a network involving at least one non-binary constraint.

A solution to a constraint network is the assignment of a value to each variable such that all the constraints are satisfied. A constraint network is said to be satisfiable if and only if it admits at least one solution. The Constraint Satisfaction Problem (CSP) is the NP-hard task of determining whether a given constraint network is satisfiable or not. A CSP instance is then defined by a constraint network, and solving it involves either finding one solution or proving its unsatisfiability. To solve a CSP instance, the constraint network is processed using inference or search methods [START_REF] Dechter | Constraint processing[END_REF][START_REF] Lecoutre | Constraint networks: techniques and algorithms[END_REF]. In the context of many search algorithms and some inference algorithms, decisions must be taken. Even if other forms of decisions exist (e.g. domain splitting), we introduce the classical ones: Definition 1. Let P = (X , C ) be a constraint network. A decision δ on P is either an assignment X = a (also called a positive decision) or a refutation X = a (also called a negative decision) where X ∈ X and a ∈ dom(X).

The variable involved in a decision δ is denoted by var(δ). Of course, ¬(X = a) is equivalent to X = a and ¬(X = a) is equivalent to X = a. When decisions are taken, one obtains simplified constraint networks, i.e. networks with some variables whose domain has been reduced. Definition 2. Let P be a constraint network and ∆ be a set of decisions on P . P | ∆ is the constraint network obtained from P such that:

• for every positive decision X = a ∈ ∆, all values but a are removed from dom(X), i.e. dom(X) becomes dom(X) ∩ {a};

• for every negative decision X = a ∈ ∆, a is removed from dom(X), i.e. dom(X) becomes dom(X) \ {a}.

In the following two subsections, we introduce some background about the inference (consistency enforcing) and search methods to which we will refer later.

Consistencies

Usually, the domains of the variables of a given constraint network are reduced by removing inconsistent values, i.e. values that cannot occur in any solution. In particular, it is possible to filter domains by considering some properties of constraint networks. These properties are called domain-filtering consistencies [START_REF] Debruyne | Domain filtering consistencies[END_REF], and generalized arc consistency (GAC) remains the central one. By exploiting consistencies (and more generally, inference approaches), the problem can be simplified (and even, sometimes solved) while preserving solutions.

Given a consistency φ, a constraint network P is said to be φ-consistent if and only if the property φ holds on P . Enforcing a domain-filtering consistency φ on a constraint network means taking into account inconsistent values (removing them from domains) identified by φ in order to make the constraint network φ-consistent. The new obtained constraint network, denoted by φ(P ), is called the φ-closure4 of P . If there exists a variable with an empty domain in φ(P ) then P is clearly unsatisfiable, denoted by φ(P ) = ⊥.

Given an ordered set {X 1 , . . . , X k } of k variables and a k-tuple τ = (a 1 , . . . , a k ) of values, a i will be denoted by τ [i] and also τ [X i ] by abuse of notation. If C is a k-ary constraint such that scp(C) = {X 1 , . . . , X k }, then the k-tuple τ is said to be:

• an allowed tuple of C iff τ ∈ rel(C); • a valid tuple of C iff ∀X ∈ scp(C), τ [X] ∈ dom(X); • a support on C iff τ is a valid allowed tuple of C.
A pair (X, a) with X ∈ X and a ∈ dom(X) is called a value (of P ). A tuple τ is a support for a value (X, a) on C if and only if X ∈ scp(C) and τ is a support on C such that τ [X] = a. Definition 3. Let P be a constraint network.

• A value (X, a) of P is generalized arc-consistent, or GAC-consistent, iff for every constraint C involving X, there exists a support for (X, a) on C.

• A variable X of P is GAC-consistent iff ∀a ∈ dom(X), (X, a) is GACconsistent.

• P is GAC-consistent iff every variable of P is GAC-consistent.

For binary constraint networks, generalized arc consistency is simply called arc consistency (AC). To enforce (G)AC on a given constraint network, many algorithms have been proposed. For example, AC2001 [START_REF] Bessiere | An optimal coarse-grained arc consistency algorithm[END_REF] is an optimal generic algorithm that enforces AC on binary constraint networks: its worst-case time complexity is O(ed 2 ) where e is the number of constraints and d is the greatest domain size.

On the other hand, many other domain-filtering consistencies have been introduced and studied in the literature. Singleton arc consistency (SAC) [START_REF] Debruyne | Some practical filtering techniques for the constraint satisfaction problem[END_REF] is one such consistency which is stronger than AC: it means that SAC can identify more inconsistent values than AC. SAC guarantees that enforcing arc consistency after performing any variable assignment does not show unsatisfiability, i.e., does not entail a domain wipe-out. Note that to simplify, whether a given constraint network P is binary or non-binary, the constraint network obtained after enforcing (generalized) arc consistency on P will be denoted by GAC (P ). Definition 4. Let P be a constraint network.

• A value (X, a) of P is singleton arc-consistent, or SAC-consistent, iff GAC (P | X=a ) = ⊥.

• A variable X of P is SAC-consistent iff ∀a ∈ dom(X), (X, a) is SACconsistent.

• P is SAC-consistent iff every variable of P is SAC-consistent.

More generally, considering any domain-filtering consistency φ, singleton φconsistency can be defined similarly to SAC. For example, a value (X, a) of P is singleton φ-consistent if and only if φ(P | X=a ) = ⊥.

Backtrack Search Algorithms

MAC [START_REF] Sabin | Contradicting conventional wisdom in constraint satisfaction[END_REF] is the search algorithm which is considered as the most efficient generic complete approach to solve CSP instances. It simply maintains (generalized) arc consistency after each taken decision. A dead-end is encountered if the current network involves a variable with an empty domain (i.e. a domain wipe-out). When mentioning MAC, it is important to indicate which branching scheme is employed. Indeed, it is possible to consider binary (2-way) branching or nonbinary (d-way) branching. These two schemes are not equivalent as it has been shown that binary branching is more powerful (to refute unsatisfiable instances) than non-binary branching [START_REF] Hwang | 2-way vs d-way branching for CSP[END_REF]. With binary branching, at each step of the search, a pair (X, a) is selected where X is an unassigned variable and a a value in dom(X), and two cases are considered: the assignment X = a and the refutation X = a. The MAC algorithm using binary branching can then be seen as building a binary tree. During search, i.e. when the tree is being built, we can make the difference between an opened node, for which only one case has been considered, and a closed node, for which both cases have been considered (i.e. explored). Classically, MAC always starts by assigning variables before refuting values.

The order in which variables are assigned by a backtrack search algorithm has been recognized as a key issue for a long time. Using different variable ordering heuristics to solve the same CSP instance can lead to drastically different results in terms of efficiency. In this paper, we focus on some representative variable ordering heuristics. The well-known dynamic heuristic dom [START_REF] Haralick | Increasing tree search efficiency for constraint satisfaction problems[END_REF] selects, at each step of the search, one of the variables with the smallest domain size. To break ties, which correspond to sets of variables that are considered as equivalent by the heuristic, one can use the dynamic degree of each variable, which corresponds to the number of constraints involving it as well as (at least) another unassigned variable. This is the heuristic called bz [START_REF] Brelaz | New methods to color the vertices of a graph[END_REF]. By directly combining domain sizes and dynamic variable degrees, one obtains dom/ddeg [START_REF] Bessiere | MAC and combined heuristics: two reasons to forsake FC (and CBJ?) on hard problems[END_REF] which can substantially improve the search performance on some problems. Finally, in [START_REF] Boussemart | Boosting systematic search by weighting constraints[END_REF], the heuristic dom/wdeg has been introduced. The principle is to associate with each constraint of the problem a counter which is incremented whenever the constraint is involved in a dead-end. Hence, wdeg that refers to the weighted degree of a variable corresponds to the sum of the weights of the constraints involving this variable as well as (at least) another unassigned variable.

On the other hand, two well-known non-chronological backtracking algorithms are conflict-directed backjumping (CBJ) [START_REF] Prosser | Hybrid algorithms for the constraint satisfaction problems[END_REF] and dynamic backtracking (DBT) [START_REF] Ginsberg | Dynamic backtracking[END_REF]. The idea of these look-back algorithms is to jump back to a variable assignment that must be reconsidered as it is suspected to be the most recent reason (culprit) of the dead-end. While BT systematically backtracks to the previously assigned variable, CBJ and DBT can identify a meaningful culprit decision by exploiting eliminating explanations. Of course, these different techniques can be combined; we obtain for example MAC-CBJ [START_REF] Prosser | MAC-CBJ: maintaining arc consistency with conflict-directed backjumping[END_REF] and MAC-DBT [START_REF] Jussien | Maintaining arc-consistency within dynamic backtracking[END_REF].

Nogood Identification through Testing-sets

In this section, we present a general approach to identify a nogood from a socalled dead-end sequence of decisions through a testing-set which corresponds to a pre-established set of variables. The principle is to determine the largest prefix of the sequence from which it is possible to instantiate all variables of the testing-set without yielding a domain wipe-out when enforcing a consistency. The objective is to identify a nogood, smaller than the one corresponding to the dead-end sequence, by carefully selecting the testing-set.

First, we formally introduce the notion of nogoods. Our definition includes both positive and negative decisions as in [START_REF] Focacci | Global cut framework for removing symmetries[END_REF][START_REF] Katsirelos | Generalized nogoods in CSPs[END_REF]. Definition 5. Let P be a constraint network and ∆ be a set of decisions on P .

• ∆ is a nogood of P iff P | ∆ is unsatisfiable.

• ∆ is a minimal nogood of P iff ∄∆ ′ ⊂ ∆ such that ∆ ′ is a nogood of P .

In some cases, a nogood can be obtained from a sequence of decisions. Such a sequence is called a dead-end sequence. Definition 6. Let P be a constraint network and Σ = δ 1 , . . . , δ i be a sequence of decisions on P . Σ is said to be a dead-end sequence of P iff {δ 1 , . . . , δ i } is a nogood of P .

Next, we introduce the notions of culprit decision and culprit subsequence. The culprit decision of a dead-end sequence Σ = δ 1 , . . . , δ i wrt a testingset S of variables and a consistency φ is the rightmost decision δ j in Σ such that δ 1 , . . . , δ j cannot be extended by instantiating all variables of S, without detecting an inconsistency with φ. More formally, it is defined as follows:

Definition 7. Let P = (X , C ) be a constraint network, Σ = δ 1 , . . . , δ i be a sequence of decisions on P , φ be a consistency and S = {X 1 , . . . , X r } ⊆ X .

• A pivot of Σ wrt φ and S is a decision δ j ∈ Σ such that ∃a 1 ∈ dom(X 1 ), . . . , ∃a r ∈ dom(X r ) | φ(P | {δ1,...,δj-1,¬δj ,X1=a1,...,Xr=ar} ) = ⊥.

• The rightmost pivot subsequence of Σ wrt φ and S is either the empty sequence if there is no pivot of Σ wrt φ and S, or the sequence δ 1 , . . . , δ j where δ j is the rightmost pivot of Σ wrt φ and S.

If Σ is a dead-end sequence then the rightmost pivot (if it exists) of Σ wrt φ and S is called the culprit decision of Σ wrt φ and S, and the rightmost pivot subsequence of Σ wrt φ and S is called the culprit subsequence of Σ wrt φ and S. S is called a testing-set.

Note that a variable may be involved both in a decision of the sequence Σ and in the testing-set S. For example, Σ may contain the negative decision X = a while X being in S; X still has to be assigned (with a value different from a). Intuitively, one can expect that a culprit subsequence corresponds to a nogood. This is stated by the following proposition.

Proposition 1. Let P = (X , C ) be a constraint network, Σ = δ 1 , . . . , δ i be a dead-end sequence of P , φ be a consistency and S ⊆ X be a testing-set. The set of decisions contained in the culprit subsequence of Σ wrt φ and S is a nogood of P .

Proof. Let S = {X 1 , . . . , X r } ⊆ X be the testing-set and let δ 1 , . . . , δ j be the (non-empty) culprit subsequence of Σ. Let us demonstrate by induction that for all integers k such that j ≤ k ≤ i, the following hypothesis H(k) holds: H(k): {δ 1 , . . . , δ k } is a nogood First, let us show that H(i) holds. We know that {δ 1 , . . . , δ i } is a nogood by hypothesis, since Σ is a dead-end sequence. Then, let us show that, for j < k ≤ i, if H(k) holds then H(k -1) also holds. As k > j and H(k) holds, we know that {δ 1 , . . . , δ k-1 , δ k } is a nogood. Furthermore, δ k is not a pivot of Σ (since k > j and δ j is the culprit decision of Σ). Hence, by Definition 7, we know that ∀a 1 ∈ dom(X 1 ), . . . , ∀a r ∈ dom(X r ), φ(P | {δ1,...,δ k-1 ,¬δ k ,X1=a1,...,Xr=ar} ) = ⊥. As a result, the set {δ 1 , . . . , δ k-1 , ¬δ k } is a nogood. By resolution [START_REF] Mitchell | Resolution and constraint satisfaction[END_REF], from {δ 1 , . . . , δ k-1 , δ k } and {δ 1 , . . . , δ k-1 , ¬δ k } being nogoods, we deduce that {δ 1 , . . . , δ k-1 } is a nogood. So, H(k -1) holds. For an empty culprit subsequence, we can easily adapt the previous reasoning to deduce that ∅ is a nogood.

It is important to note that the new identified nogood may correspond to the original one. This is the case when the culprit decision of a sequence Σ = δ 1 , . . . , δ i is δ i . On the other hand, when the culprit subsequence of Σ is empty, this means that P is unsatisfiable.

At this stage, one may wonder how Proposition 1 can be used in practice. When a conflict is encountered during a backtrack search, this means that a nogood has been identified: it corresponds to the set of decisions taken all along the current branch. One can then imagine to detect smaller nogoods using Proposition 1 in order to "backjump" in the search tree. There are as many ways to achieve that task as different testing-sets. The backjumping capability will depend upon the policy adopted to define the testing-sets. Different policies can thus be introduced to identify the source of the conflicts and so to reduce thrashing (as discussed in Section 4.2).

Reasoning from the Last Conflict

From now on, we consider a backtrack search algorithm (e.g. MAC) that uses a binary branching scheme and embeds an inference operator enforcing a consistency φ at each node of the search tree. One simple policy that can be applied to instantiate the general scheme presented in the previous section is to consider, after each encountered conflict (i.e. each time an inconsistency is detected after enforcing φ, which emphasizes a dead-end sequence), the variable involved in the last taken decision as forming the current testing-set. This is what we call last-conflict based reasoning (LC).

Principle

We first introduce the notion of LC-subsequence. It corresponds to a culprit subsequence identified by last-conflict based reasoning. Definition 8. Let P be a constraint network, Σ = δ 1 , . . . , δ i be a dead-end sequence of P and φ be a consistency. The LC-subsequence of Σ wrt φ is the culprit subsequence of Σ wrt φ and {X i } where X i = var(δ i ). The testing-set

{X i } is called the LC-testing-set of Σ.
In other words, the LC-subsequence of a sequence of decisions Σ (leading to an inconsistency) ends with the most recent decision such that, when negated, there exists a value that can be assigned, without yielding an inconsistency via φ, to the variable involved in the last decision of Σ. Note that the culprit decision δ j of Σ may be a negative decision and, also, the last decision of Σ. If j = i, this simply means that we can find another value in the domain of the variable involved in the last decision of Σ which is compatible with all other decisions of Σ. More precisely, if δ i is the culprit decision of Σ and δ i is a negative decision X i = a i , then we necessarily have φ(P | {δ1,...,δi-1,Xi=ai} ) = ⊥. On the other hand, if δ i is the culprit decision of Σ and δ i is a positive decision X i = a i then there exists a value

a ′ i = a i in dom(X i ) such that φ(P | {δ1,...,δi-1,Xi =ai,Xi=a ′ i } ) = ⊥.
LC allows identification of nogoods as shown by the following proposition.

Proposition 2. Let P be a constraint network, Σ be a dead-end sequence of P and φ be a consistency. The set of decisions contained in the LC-subsequence

X j = a j ⊥ X j = a j X i ¹ 1 = a i - 1 X i = a i X i ¹ 1 = a i ¹ 1 Xi Xi Xi LC 1 LC 1 ¹testing¹set = {X i } X i = a i Figure 1:
Reasoning from the last conflict illustrated with a partial search tree. A consistency φ is maintained at each node. A triangle labelled with a variable X and drawn using a solid base line (resp. a dotted base line) represents the fact that no (resp. a) singleton φ-consistent value exists for X.

of Σ wrt φ is a nogood of P .

Proof. Let δ i be the last decision of Σ and X i = var(δ i ). From Definition 8, the LC-subsequence of Σ wrt φ is the culprit subsequence of Σ wrt φ and {X i }.

We deduce our result from Proposition 1 with S = {X i }.

Note that the set of decisions contained in an LC-subsequence may not be a minimal nogood. Importantly, after each conflict encountered in a search tree, an LC-subsequence can be identified so as to safely backjump to its last decision. More specifically, the identification and exploitation of such nogoods can be easily embedded into a backtrack search algorithm thanks to a simple modification of the variable ordering heuristic. In practice, last-conflict based reasoning will be exploited only when a dead-end is reached from an opened node of the search tree, that is to say, from a positive decision since when a binary branching scheme is used, positive decisions are taken first. It means that LC will be used if and only if δ i (the last decision of the sequence mentioned in Definition 8) is a positive decision. To implement LC, it is then sufficient (i) to register the variable whose assignment to a given value directly leads to an inconsistency, and (ii) always to prefer this variable in subsequent decisions (so long as it is unassigned) over the choice proposed by the underlying heuristic -whatever heuristic is used. Notice that LC does not require any additional space cost.

Figure 1 illustrates last-conflict based reasoning. The leftmost branch on this figure corresponds to the positive decisions X 1 = a 1 , . . ., X i = a i , such that X i = a i leads to a conflict. With φ denoting the consistency maintained during search, we have: φ(P | X1=a1,...,Xi=ai ) = ⊥. At this point, X i is registered by LC for future use, i.e. the testing-set is {X i }, and a i is removed from dom(X i ), i.e. X i = a i . Then, instead of pursuing the search with a new selected variable, X i is chosen to be assigned with a new value. In our illustration, this leads once again to a conflict, this value is removed from dom(X i ), and the process loops until all values are removed from dom(X i ), leading to a domain wipeout (symbolized by a triangle labelled with X i whose base is drawn using a solid line). The algorithm then backtracks to the assignment X i-1 = a i-1 , going to the right branch X i-1 = a i-1 . As X i is still recorded by LC, it is selected in priority, and all values of dom(X i ) are proved here to be singleton φ-inconsistent. The algorithm finally backtracks to the decision X j = a j , going to the right branch X j = a j . Then, as {X i } is still an active LC-testing-set, X i is preferred again and the values of dom(X i ) are tested. But, as one of them does not lead to a conflict (symbolized by a triangle labelled with X i whose base is drawn using a dotted line), the search can continue with a new assignment for X i . The variable X i is then unregistered (the testing-set becomes empty), and the choice for subsequent decisions is left to the underlying heuristic, until the next conflict occurs. As a more concrete example, consider a constraint network with the variables {X 0 , X 1 , X 2 , X 3 , X 4 , X 5 , X 6 } and the constraints

{X 1 = X 4 , X 1 = X 5 , X 1 = X 6 , X 4 = X 5 , X 4 = X 6 , X 5 = X 6 }.
Here, we have a clique of binary dis-equality constraints composed of four variables {X 1 , X 4 , X 5 , X 6 }, the domain of each one being {0, 1, 2}, and three variables {X 0 , X 2 , X 3 } involved in no constraint, the domain of each one being {0, 1}. Even if the introduction of isolated variables seems to be quite particular, it can be justified by the fact that it may happen during search (after some decisions have been taken). This phenomenon, and more generally the presence of several connected components, frequently occurs when solving structured instances. Figure 2 depicts the search tree built by MAC where variables and values are selected in lexicographic order, which is used here to facilitate understanding of the example. In this figure, each leaf corresponds to a direct failure, after enforcing arc consistency; MAC explores 68 nodes to prove the unsatisfiability of this problem. Figure 3 depicts the search tree built by MAC-LC 1 using the same lexicographic order, where LC 1 denotes the implementation of last-conflict based reasoning, as presented above. This time, MAC-LC 1 only explores 21 nodes. Indeed, reasoning from the last conflict allows search to focus on the hard part of the network (i.e. the clique).

By using an operator that enforces φ to identify LC-subsequences as described above, we obtain the following complexity result. Proposition 3. Let P be a constraint network, φ be a consistency and Σ = δ 1 , . . . , δ i be a dead-end sequence of P . The worst-case time complexity of computing the LC-subsequence of Σ wrt φ is O(idγ) where γ is the worst-case time complexity of enforcing φ.

Proof. The worst case happens when the computed LC-subsequence of Σ is empty. In this case, this means that, for each decision, we check the singleton φ-consistency of X i . Checking the singleton φ-consistency of a variable corresponds to at most d calls to an algorithm enforcing φ, where d is the greatest domain size. Thus, the total worst-case time complexity is id times the complexity of the φ-enforcing algorithm, denoted by γ. We obtain O(idγ).

When LC is embedded in MAC, we obtain the following complexity.

Corollary 1. Let P be a binary constraint network and Σ = δ 1 , . . . , δ i be a dead-end sequence of decisions that corresponds to a branch built by MAC. Assuming that the current LC-testing-set is {var(δ i )}, the worst-case time complexity, for MAC-LC 1 , to backtrack up to the last decision of the LC-subsequence of Σ wrt AC is O(end 3 ).

Proof. First, we know, as positive decisions are performed first by MAC, that the number of opened nodes in a branch of the search tree is at most n. Second, for each closed node, we do not have to check the singleton arc consistency of X i since we have to directly backtrack. So, using an optimal AC algorithm in O(ed 2 ), we obtain an overall complexity in O(end 3 ).

Preventing thrashing using LC

Thrashing is a phenomenon that deserves to be carefully studied because an algorithm subject to thrashing can be very inefficient. We know that whenever a value is removed from the domain of a variable, it is possible to compute an explanation of this removal by collecting the decisions (i.e. variable assignments in our case) that entailed removing this value. By recording such so-called eliminating explanations and exploiting this information, one can hope to backjump to a level where a culprit variable will be re-assigned, this way, avoiding thrashing.

In some cases, no pertinent culprit variable(s) can be identified by a backjumping technique although thrashing occurs. For example, let us consider some unsatisfiable instances of the queens-knights problem as proposed in [START_REF] Boussemart | Boosting systematic search by weighting constraints[END_REF]. When the queens subproblem and the knights subproblem are merged without any interaction (there is no constraint involving both a queen variable and a knight variable as in the qk-25-25-5-add instance), MAC combined with a non-chronological backtracking technique such as CBJ or DBT is able to prove the unsatisfiability of the problem from the unsatisfiability of the knights subproblem (by backtracking up to the root of the search tree). When the two subproblems are merged with an interaction (queens and knights cannot be put on the same square as in the qk-25-25-5-mul instance), MAC-CBJ and MAC-DBT become subject to thrashing (when a standard variable ordering heuristic such as dom, bz or dom/ddeg is used) because the last assigned queen variable is considered as participating to the reason of the failure. The problem is that, even if there exists different eliminating explanations for a removed value, only the first one is recorded. One can still imagine to improve existing backjumping algorithms by updating eliminating explanations, computing new ones [START_REF] Junker | QuickXplain: preferred explanations and relaxations for overconstrained problems[END_REF] or managing several explanations [START_REF] Schiex | Stubborness: a possible enhancement for backjumping and nogood recording[END_REF][START_REF] Ouis | k-relevant explanations for constraint programming[END_REF]. However, this is far beyond the scope of this paper.

Reasoning from the last conflict is a new way of reducing thrashing, while still being a look-ahead technique. Indeed, guiding search to the last decision of a culprit subsequence behaves similarly to using a form of backjumping to that decision.

Table 1 illustrates the thrashing prevention capability of LC on the two instances mentioned above. Clearly, MAC, MAC-CBJ and MAC-DBT cannot prevent thrashing for the qk-25-25-5-mul instance as, within 2 hours, the instance remains unsolved (even when other standard heuristics are used). On the other hand, in about 1 minute, MAC-LC 1 can prove the unsatisfiability of this instance. The reason is that all values in the domain of knight variables are singleton arc-inconsistent. When such a variable is reached, LC guides search up to the root of the search tree.

A Generalization: Reasoning from Last Conflicts

A generalization of the last conflict policy, previously introduced, can now be envisioned. As before, after each conflict, the testing-set is initially composed of the variable involved in the last taken decision. However, it is also updated

Principle

To define testing-sets, the policy previously introduced can be generalized as follows. At each dead-end the testing-set initially consists, as before, of the variable X i involved in the most recent decision δ i . When the culprit decision δ j is identified, the variable X j involved in δ j is included in the testing-set. The new testing-set {X i , X j } may help backtracking nearer the root of the search tree. Of course, this form of reasoning can be extended recursively. This mechanism is intended to identify a (small) set of incompatible variables involved in decisions of the current branch, although these may be interleaved with many irrelevant decisions. We now formalize this approach before illustrating it.

Definition 9. Let P be a constraint network, Σ be a dead-end sequence of P and φ be a consistency. We recursively define the k th LC-testing-set and the k th LCsubsequence of Σ wrt φ, respectively called LC k -testing-set and LC k -subsequence and denoted by S k and Σ k , as follows:

• For k = 1, S 1 and Σ 1 respectively correspond to the LC-testing-set of Σ and the LC-subsequence of Σ wrt φ.

• For k > 1, if Σ k-1 = , then S k = S k-1 and Σ k = Σ k-1 . Otherwise, S k = S k-1 ∪{X k-1 } where X k-1 is the variable involved in the last decision of Σ k-1 and Σ k is the rightmost pivot subsequence of Σ k-1 wrt φ and S k .
The following proposition is a generalization of Proposition 2, and can be demonstrated by induction on k. Proposition 4. Let P be a constraint network, Σ be a dead-end sequence of P and φ be a consistency. For any k ≥ 1, the set of decisions contained in Σ k , which is the LC k -subsequence of Σ wrt φ, is a nogood of P .

Proof. Let us demonstrate by induction that for all integers k ≥ 1, the following hypothesis, denoted H(k), holds: H(k): the set of decisions contained in Σ k is a nogood First, let us show that H(1) holds. From Proposition 2, we know that the set of decisions contained in Σ 1 is a nogood. Then, let us show that, for k > 1, if H(k -1) holds then H(k) also holds. As k > 1 and H(k -1) holds, we know that the set of decisions contained in Σ k-1 is a nogood and, consequently, Σ k-1 is a dead-end sequence. Using Definition 7, we know that the rightmost pivot subsequence Σ k is a culprit subsequence. Hence, using Proposition 1, we deduce that the set of decisions contained in Σ k is a nogood.

For any k > 1 and any given dead-end sequence Σ, LC k will denote the process that consists in computing the LC k -subsequence Σ k of Σ. When computing Σ k , we may have Σ k = Σ k-1 meaning that the original nogood has been reduced k times (and S k is composed of k distinct variables). However, a fixed point may be reached at a level 1 ≤ j < k, meaning that Σ j = Σ j+1 and either j = 1 or Σ j = Σ j-1 . The fixed point is reached when the current testing set is composed of j + 1 variables: no new variable can be added to the testing set because the identified culprit decision is the last decision of the current dead-end sequence.

In practice, we will use the generalized version of LC in the context of a backtrack search. If a fixed point is reached at a level j < k, the process of lastconflict based reasoning is stopped and the choice of subsequent decisions is left to the underlying heuristic until the next conflict occurs. On the other hand, we will restrict pivots to be positive decisions, only. Indeed, it is not relevant to consider a negative decision X = a as a pivot because it would consist in building a third branch within the MAC search tree identical to the first one. The subtree under the opposite decision X = a has already been refuted, since positive decisions are taken first.

As an illustration, Figure 4 depicts a partial view of a search tree. The leftmost branch corresponds to a dead-end sequence of decisions Σ. By definition, the LC 1 -testing-set of Σ is only composed of the variable X i (which is involved in the last decision of Σ). So, the algorithm assigns X i in priority in order to identify the culprit decision of Σ (and the LC 1 -subsequence). In our illustration, no value in dom(X i ) is found to be singleton φ-consistent until the algorithm backtracks up to the positive decision X j = a j . This decision is then identified as the culprit decision of Σ, and so, in order to compute the LC 2 -subsequence, the LC 2 -testing-set is built by adding X j to the LC 1 -testing-set. From now, X i and X j will be assigned in priority. The LC 2 -subsequence is identified when backtracking to the decision X k = a k . Indeed, from X k = a k , it is possible to instantiate the two variables of the LC 2 -testing-set. Then, X k is added to the LC 2 -testing-set, but as the variables of this new testing-set can now be assigned, last-conflict reasoning is stopped because a fixed point is reached (at level 2) and search continues as usual.

Let us consider again the example introduced in Section 4.1 and the search trees (see Figures 2 and3) built by MAC and MAC-LC 1 . This time, Figure 5 represents the search tree built by MAC-LC 2 . We recall that with MAC-LC 2 , the testing-sets may contain up to two variables. Here, after the first conflict (leftmost branch), the testing-set is initialized with {X 4 } and when the singleton

X k = a k X j = a j ⊥ X j = a j X k = a k X i ¹ 1 = a i - 1 X i = a i X j ¹ 1 = a j ¹ 1 X i ¹ 1 = a i ¹ 1 X j ¹ 1 = a j ¹ 1 Xi Xi Xi Xj Xi Xj Xi Xj Xk Ä 1 Ä 2 Ä 2 ¹Ø ×Ø Ò ¹× Ø= {X i , X j } Ä 1 ¹Ø ×Ø Ò ¹× Ø= {X i } X i = a i
Figure 4: Generalized reasoning from the last conflict illustrated with a partial search tree. A consistency φ is maintained at each node. A triangle labelled with a variable X and drawn using a solid base line (resp. a dotted base line) represents the fact that no (resp. a) singleton φ-consistent value exists for X. one can expect to identify the pawn incompatible variables and to use them as LC p-2 -testing-set. Table 2 presents the results obtained with MAC equipped with LC reasoning (LC k with k ∈ [START_REF] Bacchus | Extending Forward Checking[END_REF][START_REF] Brelaz | New methods to color the vertices of a graph[END_REF]) or not (LC 0 ) on instances qp-12-p with p ranging from 4 to 9. The size of the chessboard was set to 12 × 12 and the time limit was 2 hours. As expected, to solve an instance qp-12-p, it is better to use LC p-2 as variables that correspond to pawns can be collected by this approach. Note that if we use LC k with k ≥ p -2, whatever k is, the number of nodes does not change (significantly). If k < p -2, solving the problem is more difficult: one can only identify a subset of the p -2 incompatible variables. Reasoning from last conflicts can be implemented by slight modifications of a classical backtrack search algorithm (see function solve described in Algorithm 1) and its associated variable selection procedure (see function selectV ariable, Algorithm 2). The function solve works the following way. First, an inference operator establishing a consistency φ such as AC is applied on a constraint network P (line 1). To simplify the presentation, we suppose here that φ is a domain filtering consistency at least as strong as the partial form of arc consistency established (maintained) by the FC algorithm [START_REF] Haralick | Increasing tree search efficiency for constraint satisfaction problems[END_REF]. If the resulting constraint network is trivially inconsistent (a variable has an empty domain), solve returns f alse (lines 2-3). Else, if the domain of all variables in P is reduced to only one value, a solution is found and solve returns true (lines 4-5). If P is not proved inconsistent by φ and there remains several possible values for at least one variable, a new decision has to be taken. A variable X Algorithm 2: selectV ariable() Input: a constraint network P Output: a variable X to be used for branching

Implementation Details

foreach X ∈ testingSet do 1 if |dom(X)| > 1 then 2 return X 3 if candidate = null ∧ |dom(candidate)| > 1 then 4 X ← candidate 5 testingSet ← testingSet ∪ {X} 6 else 7 X ← variableOrderingHeuristic.selectV ariable(P )) 8 testingSet ← ∅ 9 candidate ← null 10 return X 11
is thus selected by a call to selectV ariable (line 6), and a value a is picked from dom(X) by a call to selectV alue. Two branches are then successively explored by recursive calls to solve: the assignment X = a (lines 8-9) and the refutation X = a (line 12). Between these two calls, two lines have been introduced (lines 10-11) in order to manage LC. We will discuss them below.

Apart from these two lines, most of the modifications lie in selectV ariable, Algorithm 2. Classically, this function selects the best variable to be assigned thanks to the given variable ordering heuristic implemented by the function variableOrderingHeuristic.selectV ariable. The algorithm we propose here modifies this selection mechanism to reflect the different possible states of search:

1. Some variables have been collected in a testing-set, and we look for an instantiation of them which is consistent with the current node of the search tree. Variables of this testing-set are then preferred over all other variables (lines 1-3), until the domains of the variables in the testing-set are all reduced to singletons. The order in which the variables of the testing-set are picked is not crucial, as the maximal size of a testing-set is limited by k and is kept relatively low in practice. This step can be viewed as a complete local exploration of a small subtree until the variables of the testing-set are all assigned (their domains are reduced to singletons).

2. When all variables of a testing-set are assigned, there may exist a candidate variable to be added to the testing-set (lines 4-5). In that case, the variable candidate corresponds to a variable whose domain contains more than one value. This candidate has been pointed out in the function solve (lines 10-11), just before the refutation of a given value from its domain, under the following conditions:

• Firstly, there was no candidate yet (candidate = null). This happens when a conflict has been encountered under the assignment X = a in the left branch: variables of the testing-set are going to be explored in the right branch under the refutation X = a, and X will then be potentially added later to the testing-set.

• Secondly, the maximal size k of a testing-set has not been reached (|testingSet| < k).

• Thirdly, X must not be already present in the testing-set (X / ∈ testingSet). X ∈ testingSet may happen when X has just been entered into the testing-set and search focuses on it.

A candidate will enter the testing-set only if an instantiation of the variables currently in the testing-set is found. If no instantiation of the testingset can be found, the candidate is not added to the testing-set and will be replaced by another one after having backtracked higher in the search tree.

3. If an instantiation of the testing-set has already been found (possibly, the testing-set being empty) and if there is no candidate or the candidate is already assigned, then the classical heuristic chooses a new variable to assign, and the testing-set is emptied.

Experiments

In order to show the practical interest of the approach described in this paper, we have conducted an extensive experimentation on a cluster of Xeon 3.0GHz with 1GiB of RAM under Linux, with respect to two research domains: constraint satisfaction and automated artificial intelligence planning. To do this, we have respectively equipped the constraint solver Abscon [START_REF] Lecoutre | Abscon 109: a generic CSP solver[END_REF] and the planner CPT [START_REF] Vidal | Branching and pruning: an optimal temporal POCL planner based on constraint programming[END_REF] with last-conflict based reasoning.

Results with the CSP solver Abscon

We first present the results obtained with the solver Abscon. For our experimentation, we have used MAC (using chronological backtracking) and studied the impact of LC wrt various variable ordering heuristics (dom/ddeg, dom/wdeg, bz ). Recall that LC 0 denotes MAC alone and LC k denotes the approach that consists in computing LC k -subsequences, i.e. the generalized last-conflict based approach where at most k variables are collected. Performance is measured in terms of the number of visited nodes (nodes) and the CPU time in seconds. Importantly, all CSP instances that have been experimented come from the second constraint solver competition5 where they can be downloaded. First, we experimented LC 1 and LC 2 on different series of random problems. Seven classes of binary instances near crossover points have been generated following Model D [START_REF] Smith | Locating the phase transition in binary constraint satisfaction problems[END_REF][START_REF] Gent | Random constraint satisfaction: flaws and structure[END_REF]. For each class n, d, e, t , the number of variables n is 40, the domain size d lies between 8 and 180, the number of constraints e lies between 753 and 84 (so the density is between 0.96 and 0.1) and the tightness t lies between 0.1 and 0.9. Here, tightness t is the probability that a pair of values is disallowed by a relation. The first class 40, 8, 753, 0.1 corresponds to dense instances involving constraints of low tightness whereas the seventh one 40, 180, 84, 0.9 corresponds to sparse instances involving constraints of high tightness. It is important to note that a significant sampling of domain sizes, densities and tightnesses is provided. Two series of random instances generated using Model RB [START_REF] Xu | Exact phase transitions in random constraint satisfaction problems[END_REF] and forced to be satisfiable as described in [START_REF] Xu | Random constraint satisfaction: easy generation of hard (satisfiable) instances[END_REF] were also tested. We finally experimented the series of "geometric" instances proposed by R. Wallace. Constraint relations are generated in the same way as for homogeneous random CSP instances, but instead of a density parameter, a "distance" parameter is used.

The results that we have obtained are given in Table 3. The number of unsolved instances within 20 minutes is given into brackets, in this case the CPU time must be considered as a lower bound. Broadly, using LC on random instances is penalizing because these instances do not contain any structure. MAC alone is better than LC 1 , itself being better than LC 2 . However on series geom and classes 40, 80, 103, 0.8 and 40, 180, 84, 0.9 , this is less obvious. Indeed, one can consider that such instances have a little structure. This is true for the geom instances by construction, and also for the random instances of the two classes 40, 80, 103, 0.8 and 40, 180, 84, 0.9 since their constraint graph is sparse.

Tables 4 and5 show the practical interest of LC 1 and LC 2 on structured instances. Table 4 reports results on classical series of academic instances from the literature: graph coloring, job-shop scheduling, quasi-group completion problem, aim and ehi SAT instances converted to CSP. (h) scen11-f8 series of instances issued from real-world problems:

• The frequency assignment problem with polarization constraints (FAPP) is an optimization problem that was part of the ROADEF'2001 challenge 6 . In this problem, there are constraints concerning frequencies and polarization of radio links. Progressive relaxation of these constraints is explored: the relaxation level is between 0 (no relaxation) and 10 (maximum relaxation). Progressive relaxation produces eleven CSP instances from any single original FAPP optimization instance.

• The radio link frequency assignment problem (RLFAP) is the task of assigning frequencies to a set of radio links satisfying a large number of constraints and using as few distinct frequencies as possible. In 1993, the CELAR (the French "centre d'electronique de l'armement") built a suite of simplified versions of radio link frequency assignment problems starting from data on a real network [START_REF] Cabon | Radio Link Frequency Assignment[END_REF]. Series of binary RLFAP instances are identified as either scen or graph.

• The Swedish institute of computer science (SICS) has proposed a model of realistic radar surveillance 7 . The problem is to adjust the signal strength (from 0 to s) of a given number of fixed radars wrt six geographic sectors. Each cell of the geographic area of size p × p must be covered exactly by k radar stations, except for a number i of forbidden cells that must not be covered. Sets of 50 instances with non-binary constraints have been generated artificially; each series is denoted by radar-p-k-s-i.

Tables 4 and5 show that the efficiency of MAC combined with a standard heuristic (i.e. dom/ddeg, bz ) is increased when LC is used, both in terms of CPU time and number of solved instances. LC 2 is even better than LC 1 , especially on job-shop and RLFAP series. These instances are structured and a blind search (i.e. without analyzing the reasons of the conflicts) is subject to thrashing. As expected, last-conflict reasoning allows us to reduce the appearance of this phenomenon without modifying the general behavior of the heuristics. When the heuristic dom/wdeg is used, the results are less impressive since this heuristic already reduces thrashing.

In Table 6, we can observe the impact of LC on some representative instances from the second constraint solver competition. Results are mentioned for LC k with k ranging from 0 to 4, and the time limit was 1 hour. Once again, it clearly appears that using LC with a standard heuristic greatly improves the efficiency of the MAC algorithm. This is not always true when the dom/wdeg heuristic is used for the reasons previously mentioned. Note that some of these instances cannot be solved efficiently using a backjumping technique such as CBJ or DBT combined with a standard heuristic. This aspect has been shown in [START_REF] Lecoutre | Backjump-based techniques versus conflict-directed heuristics[END_REF]. Broadly, LC 2 and LC 3 offer the best trade-off.

We have also focused on the most difficult real-world instances that are currently available (see the results of the second and third constraint solver competitions). These instances are unsatisfiable and belong to the RLFAP series scen11-fX with X ∈ [START_REF] Bacchus | Extending Forward Checking[END_REF][START_REF] Cabon | Radio Link Frequency Assignment[END_REF]. Figures 6 and7 depict the CPU time required to solve these instances using LC k with k ranging from 0 to 8. Missing points mean that unsatisfiability is not proved within 48 hours. For example, MAC alone (LC 0 ) with dom/ddeg cannot solve any instance of this series within 48 hours. On these difficult structured instances, CPU time generally decreases with increasing values of k. This is particularly true for dom/ddeg (see Figure 6) but still observable with dom/wdeg (see Figure 7).

The overall results obtained on the full suite of instances used for the second constraint solver competition are given in Table 7. Each line of the table corresponds to a category of instances (academic, Boolean, patterned, . . . ). For each category, the number given between brackets represents the total number of instances of this category, and we provide the number of solved instances (within 20 minutes) using LC 0 and LC 1 and the heuristics bz, dom/ddeg and dom/wdeg. Whatever the heuristic is used, LC 1 allows to solve more instances than LC 0 on categories of structured instances (Academic, Boolean, Patterned, QuasiRandom and Real). As previously mentioned (see Table 3), LC 1 is not very efficient to solve instances of the random category. Finally, Figures 8 and9 depict the same results for dom/ddeg and dom/wdeg with scatter plots. Each dot represents an instance and its coordinates are defined by: on the horizontal axis, the CPU time required to solve the instance with MAC, and on the vertical axis, the CPU time required to solve the instance with MAC-LC 1 . Many dots are located on the right side of the graphs, which means that LC 1 solves more instances than LC 0 .

Results with the optimal temporal planner CPT

Reasoning from last-conflicts can be easily adapted to other research domains.

Here we discuss the adaptation of LC 1 to automated Artificial Intelligence planning, more precisely planning using a STRIPS formulation [START_REF] Fikes | STRIPS: A new approach to the application of theorem proving to problem solving[END_REF][START_REF] Ghallab | Automated Planning, Theory and Practice[END_REF]. The classical planning problem is the task of determining a sequence of actions (that is to say a plan), allowing the evolution from an initial state of the world to a final state satisfying a set of goals. A state is represented with a set of atoms, called fluents. STRIPS actions, classically represented by a triple of sets of fluentspreconditions, add effects, del effects -can make the current representation of the world evolve from one state to another one. An action can be applied to a state if its preconditions are satisfied into that state, and yields a new state by removing its del effects and inserting its add effects. Planning problems are defined using a representation language : PDDL [START_REF] Fox | PDDL2.1: An extension to PDDL for expressing temporal planning domains[END_REF], which has been developed for the international planning competitions8 held every two years. The temporal planning problem is an extension of the classical planning paradigm, where each action has a fixed execution time and allows some forms of concurrency between non-conflicting actions. The planner CPT [START_REF] Vidal | Branching and pruning: an optimal temporal POCL planner based on constraint programming[END_REF] is an optimal temporal planning system which combines a branching scheme based on Partial Order Causal Link (POCL) planning with powerful and sound pruning rules implemented as constraints. It minimizes the makespan of the plan, which is the overall execution time of that plan wrt action durations and ordering relations between them. CPT competed in the optimal tracks of the fourth and fifth international planning competitions, where it respectively got a second place and distinguished performance in temporal domains. The key novelty in CPT is its formulation of a planning problem as a constraint satisfaction problem involving the use of supports threats, precedence relations and mutex threats, to deal with actions that are not yet included in a partial plan. The adaptation of last-conflict reasoning (LC 1 ) to this kind of planning system is quite immediate. The choice for the inclusion of new instances of actions in a partial plan is expressed through support variables S(p, a) associated to couples precondition p -action a, whose domain is the set of actions that can produce the precondition p for the action a. The variable selection heuristic is modified in the same way as in Abscon: the last support variable involved in a conflict is selected in priority as long as a failure is detected.

Table 8 shows the results obtained with CPT on some series of problems from the second and third international planning competitions (domains BlocksWorld, Depots, DriverLog, Logistics, Rovers, Satellite). Some of these domains (Satellite and Rovers) are also used in the fourth and fifth international planning competitions. Each series contains 500 problems generated using the problem generators implemented for the competitions, with diverse parameters. We have compared standard CPT (noted CPT in the table) with CPT embedding last-conflict reasoning (noted CPT-LC 1 in the table). The time limit was 30 minutes per instance and results have been compared in terms of number of solved instances (#-intances) and cumulated CPU time for instances solved by both methods. First note that CPT-LC 1 solves more instances in all problem series. Indeed, broadly, CPT-LC 1 solves 286 instances that CPT cannot solve. Moreover, the total time for solving instances of every series has been greatly improved.

Figure 10 depicts with a scatter plot the results described above. Each dot represents an instance. The coordinates of this dot are defined by: on the horizontal axis, the CPU time required to solve the instance with CPT and on the vertical axis, the CPU time required to solve the instance with CPT-LC 1 . CPT embedding last-conflict reasoning is clearly more efficient than standard CPT. Indeed most of the dots are located under the diagonal, that is to say solving a given instance with CPT-LC 1 is most often faster than with CPT. Moreover, note that many dots are located on the right hand side of the graph. These dots represent instances solved by CPT-LC 1 but not by CPT.

On instances from the fourth international planning competition 9 , the difference between CPT alone and CPT-LC 1 is generally less significant. Table 9 We have not included results from the fifth and sixth international planning competitions because (1) generators for the fifth do not produce plain STRIPS problems and no generator were available for the sixth, and (2) official instances are designed for suboptimal planners, so we could not get very significant results (instances are either too easy or too difficult).

9 only provides results on instances for which there is a substantial difference between the two approaches. On these instances, CPT-LC 1 behaves generally better than standard CPT.

Conclusion

In this paper, we have introduced the concept of reasoning from last conflicts that can be regarded as an original look-ahead approach which allows to guide search toward sources of conflicts. The principle is to select in priority the variable involved in the last conflict (i.e. the last assignment that failed) as long as the constraint network cannot be made consistent. This way of reasoning allows to reduce thrashing by backtracking to the most recent identified culprit decision of the last conflict and, as a consequence, simulates a backjumping effect by a form of lazy identification of culprit decisions. A generalization of this reasoning is also proposed, allowing the identification of more relevant culprit decisions (located higher in the search tree). This mechanism computes small sets of hard variables, called testing-sets, that are involved in decisions of the current branch and interleaved with many other irrelevant decisions. Consequently, search is improved by focusing on variables of testing-sets. Our method can be grafted to any search algorithm based on a depth-first exploration without any additional cost in space. The interest of this approach has been shown in practice by an extensive experimentation in both constraint satisfaction and automated artificial intelligence planning.

In our approach, the variable ordering heuristic is violated, until a backtrack to the culprit decision occurs and a singleton consistent value is found for each variable of the testing-set. However, an alternative is not to consider the found singleton consistent value as the next value to be assigned. In this case, the approach becomes a pure inference technique which corresponds to (partially) maintaining a singleton consistency (SAC, for example) on the variables of the testing-set (and so involved in the last conflict). This would be related to the "Quick Shaving" technique [START_REF] Lhomme | Quick shaving[END_REF] whose principle is to check, when a backtrack occurs at depth k, the consistency of values that were shavable (i.e. singleton arc-inconsistent) at depth k + 1.

Figure 6 :

 6 Figure 6: CPU time (y-axis) to solve the RLFAP instances of series scen11-fX with MAC-LC k , with k (x-axis) ranging from 0 to 8. The variable ordering heuristic is dom/ddeg and the time-out to solve each instance is 48 hours.

Figure 7 :

 7 Figure 7: CPU time (y-axis) to solve the RLFAP instances of series scen11-fX with MAC-LC k , with k (x-axis) ranging from 0 to 8. The variable ordering heuristic is dom/wdeg and the time-out to solve each instance is 48 hours.

Figure 8 :

 8 Figure 8: Pairwise comparison (CPU time) on the 3, 293 instances used as benchmarks of the second constraint solver competition. The variable ordering heuristic is dom/ddeg and the time-out to solve an instance is 20 minutes.

Figure 9 :

 9 Figure 9: Pairwise comparison (CPU time) on the 3, 293 instances used as benchmarks of the second constraint solver competition. The variable ordering heuristic is dom/wdeg and the time-out to solve an instance is 20 minutes.

Table 1 :

 1 Cost of running variants of MAC with bz as variable ordering heuristic (time-out is 2 hours)

	Instance		MAC	MAC-CBJ MAC-DBT MAC-LC 1
	qk-25-25-5-	CPU	> 2h	11.7	12.5	58.9
	add	nodes	-	703	691	10, 053
	qk-25-25-5-	CPU	> 2h	> 2h	> 2h	66.6
	mul	nodes	-	-	-	9, 922
	each time a culprit decision is identified.

Table 2 :

 2 Results obtained with MAC-LC k with k ∈ [0, 7], using bz and dom/wdeg as heuristics, on the queens-pawns problem.

	bz

Table 3 :

 3 Results obtained with MAC, MAC-LC 1 and MAC-LC 2 on random instances (time-out is 20 minutes).

				dom/ddeg			dom/wdeg			bz
			LC0	LC1	LC2	LC0	LC1	LC2	LC0	LC1	LC2
	Random instances from Model D (100 instances per series)
	40, 8, 753, 0.1	CPU nodes 45, 388 12.1	60.8 232K	85.3 326K 45, 393 10.5	55.6 241K	78.8 322K	12.1 45, 388	59.8 232K	83.4 326K
	40, 11, 414, 0.2	CPU nodes 58, 443 12.8	44.6 203K	59.7 266K 70, 560 14.6	54.2 253K	68.9 312K	16.0 73, 004	47.4 213K	60.8 280K
	40, 16, 250, 0.35	CPU nodes 59, 448 12.2	33.3 158K	44.1 215K 72, 556 14.5	35.9 182K	48.2 237K	21.0 104K	41.2 200K	47.6 233K
	40, 25, 180, 0.5	CPU nodes 82, 836 16.7	27.3 134K	41.2 205K 81, 921 17.0	34.7 173K	41.6 200K	46.7 238K	44.9 227K	44.2 225K
	40, 40, 135, 0.65	CPU nodes 52, 814 70, 113 11.8 15.3	23.2 110K 47, 665 72, 547 11.0 16.1	21.5 101K	52.21 242K	22.65 102K	26.02 123K
	40, 80, 103, 0.8	CPU nodes 49, 923 39, 926 67, 513 20, 994 34, 375 57, 227 13.9 10.9 16.2 6.45 9.62 14.0	129 (5) 487K 57, 115 74, 583 15.3 19.5
	40, 180, 84, 0.9	CPU nodes 55, 403 39, 281 79, 280 17, 348 29, 047 62, 003 21.7 15.8 26.3 8.48 11.9 19.8	111 (3) 317K 40, 407 61, 516 16.4 21.1
	Random forced instances from Model RB (5 instances per series)
	frb35-17	CPU nodes 15, 844 18, 983 21, 439 10, 160 18, 816 29, 564 4.30 5.01 5.52 3.26 4.94 7.39	6.39 24, 872 20, 518 22, 952 5.35 5.89
	frb40-19	CPU nodes	32.7 135K	111 463K	64.2 271K	25.3 103K	98.7 452K	126 564K	47.3 196K	106 447K	128 549K
	geom (100 instances per series)
	geom	CPU nodes 30, 847 76, 706 10.2 24.5	32.8 103K 21, 712 85, 865 6.92 27.4	34.3 41.6 (1) 115K 179K 85, 396 26.6	33.8 106K

Table 4 :

 4 Results obtained with MAC, MAC-LC 1 and MAC-LC 2 on academic and patterned instances (time-out is 20 minutes).

				dom/ddeg			dom/wdeg			bz
			LC0	LC1	LC2	LC0	LC1	LC2	LC0	LC1	LC2
	Aim (24 instances per series)
	aim-100	CPU nodes	636 (10) 9, 150K	30.2 428K	35.6 489K	0.60 3, 106	0.54 2, 485	0.53 647 (12) 2, 330 9, 488K	50.4 718K	50.2 718K
	aim-200	CPU nodes	977 (18) 737 (13) 740 (13) 12M 8, 455K 8, 598K	5.82 64, 798	4.75 52, 857	4.85 985 (18) 740 (14) 738 (14) 55, 387 12M 9, 071K 9, 165K
	Composed instances (10 instances per series)
	25-1-40	CPU nodes	1, 200 (10) 13M	0.51 74	0.54 74	0.51 161	0.53 74	0.49 74	0.47 4	0.42 4	0.48 4
	25-10-20	CPU nodes	27.1 272K	0.64 161	0.63 160	0.58 200	0.60 159	0.58 159	229 (1) 2, 599K	0.77 220	0.74 198
	Coloring instances (22 instances per series)
	dsjc/myciel	CPU	6.88	4.50	6.77	13.6	10.2	10.7	105	9.54	7.52
	. . .	nodes	41, 020	32, 046	38, 065	150K	110K	108K	1, 500K	93, 070	75, 256
	Sadeh job-shop instances (10 instances per series)
	e0ddr1-10	CPU nodes	960 (8) 9, 811K	548 (4) 5, 412K	501 (4) 4, 591K 4, 588K 4, 164K 4, 615K 511 (4) 445 (3) 498 (4)	720 (6) 6, 487K	600 (5) 5, 608K	492 (4) 4, 647K
	enddr1-10	CPU nodes	600 (5) 6, 535K	142 (1) 1, 345K	124 (1) 1, 191K 1, 101K 1, 127K 1, 162K 123 (1) 124 (1) 124 (1)	360 (3) 3, 162K	259 (2) 2, 274K	243 (2) 2, 270K
	Ehi instances (100 instances per series)
	ehi-85-297	CPU nodes	475 (13) 529K	0.91 557	0.62 281	0.87 1, 292	0.43 146	0.43 146	301 (8) 362K	0.69 311	0.53 172
	ehi-90-315	CPU nodes	601 (23) 616K	1.17 674	0.65 264	0.85 1, 210	0.44 140	0.48 402 (14) 140 431K	0.70 282	0.53 155
	QCP (15 instances per series)
	qcp-10-67	CPU nodes	98.2 1, 038K	0.56 885	0.50 366	0.47 171	0.52 169	0.47 168	80.3 897K	0.54 854	0.49 369
	qcp-15-120	CPU nodes	736 (7) 3, 377K	704 (7) 3, 594K	637 (6) 3, 334K	34.4 232K	36.5 254K	35.2 241K	727 (7) 3, 907K	729 (7) 3, 845K	628 (6) 3, 491K

Table 5 :

 5 Results obtained with MAC, MAC-LC 1 and MAC-LC 2 on real-world instances (time-out is 20 minutes per instance).

			dom/ddeg			dom/wdeg			bz
			LC0	LC1	LC2	LC0	LC1	LC2	LC0	LC1	LC2
	FAPP instances (11 instances per series)
	fapp02	CPU nodes	564 (5) 688K	8.03 582	7.71 415	9.14 966	7.51 369	7.42 337	318 (2) 244K	7.20 291	7.04 270
	fapp03	CPU nodes	115 (1) 9, 694	7.83 153	7.74 208	7.48 168	7.79 181	7.74 147	115 (1) 11, 023	8.41 237	8.09 211
	fapp04	CPU nodes	225 (2) 123K	9.60 297	9.79 364	12.0 738	9.15 319 1, 693 20.2	658 (6) 397K	96.8 17, 771	42.5 3, 836
	RLFAP Graphs (12 and 14 instances per series)
	graphMods	CPU nodes	800 (8) 1, 585K	315 (3) 858K	51.5 140K 5, 509 14, 601 2, 208 2.28 3.80 1.50 1, 000 (10) 2, 350K 1, 642K 303 (3)	2.53 3, 185
	graphs	CPU nodes	1.35 313	1.37 313	1.37 313	1.19 313	1.28 313	1.26 313	86.8 (1) 521K	1.59 497	1.46 378
	Radar surveillance (50 instances per series)
	radar-8-24-3-2	CPU nodes	408 (17) 4, 651K	1.70 14, 699	0.48 3, 085	0.18 122	0.17 106	0.16 107	210 (8) 2, 214K	0.84 5, 804	0.22 657
	radar-8-30-3-0	CPU nodes	423 (17) 24.8 (1) 4, 727K 141K 43, 635 8.03	0.21 219	0.19 209	0.21 213	101 (4) 1, 001K	0.94 6, 067 10, 217 1.92

Table 6 :

 6 Results obtained with MAC-LC k with k ∈ [0, 4], using bz and dom/wdeg as heuristics, on academic and real-world instances.

					bz					dom/wdeg
			LC 0	LC 1	LC 2	LC 3	LC 4	LC 0	LC 1	LC 2	LC 3	LC 4
	cc-7-7-3	CPU nodes	154 732K	36.1 171K	46.3 217K	42.0 198K	41.7 194K	23.6 131K	30.3 174K	26.6 146K	27.1 144K	30.9 165K
	cc-9-9-2	CPU nodes	89.9 216K	4.94 10, 823	4.68 10, 823	5.15 10, 823	5.13 10, 823	1.01 3, 387	1.00 3, 457	0.96 3, 457	0.98 3, 457	0.99 3, 457
	e0ddr2-1	CPU nodes	time-out	time-out	463 3, 052K	374 2, 471K	379 2, 757K	110 812K	281 2, 024K	191 1, 329K	272 2, 085K	724 5, 319K
	enddr1-10	CPU nodes	time-out	186 1, 472K	30.0 254K	34.9 282K	23.9 210K	20.4 141K	33.6 268K	31.9 261K	28.1 233K	24.5 184K
	fapp02-0250-5	CPU nodes	time-out	7.82 323	7.00 323	7.23 323	7.26 323	7.99 851	8.80 685	8.37 632	8.48 638	8.57 638
	fapp04-0300-5	CPU nodes	time-out	753 97, 127	344 32, 394	264 23, 368	315 28, 227	18.8 1, 734	9.74 353	9.67 332	10.5 318	14.2 1, 078
	langford-3-12	CPU nodes	25.7 157K	207 1, 186K	383 2, 086K	370 1, 837K	344 1, 548K	23.2 90, 122	120 441K	129 433K	108 416K	115 384K
	langford-4-12	CPU nodes	6.34 18, 608	29.2 94, 941	54.2 162K	61.4 172K	49.4 124K	5.22 12, 437	17.6 36, 742	18.6 39, 112	17.2 35, 844	16.2 33, 769
	qcp-15-120-12	CPU nodes	time-out	time-out	611 3, 206K	14.3 84, 304	94.9 477K	0.55 782	0.52 660	0.51 505	0.52 531	0.45 531
	qcp-20-187-11	CPU nodes	time-out	time-out	time-out	time-out	time-out	3.91 15, 992	1.46 4, 992	1.40 5, 083	1.25 3, 860	1.13 3, 753
	qa-5	CPU nodes	9.94 93, 677	3.62 31, 272	3.13 24, 995	1.96 16, 107	3.17 22, 937	1.42 10, 533	2.79 19, 482	2.19 14, 189	3.1 14, 990	2.13 14, 295
	qa-6	CPU nodes	time-out	290 1, 980K	401 2, 407K	195 1217K	420 2, 689K	130 769K	120 676K	143 760K	263 1, 450K	81.4 431K
	graph9-f10	CPU nodes	time-out	time-out	7.49 14, 661	5.54 15, 520	4.22 14, 950	1.53 2, 041	1.52 2, 693	1.49 2, 754	1.43 2, 477	1.63 3, 716
	scen11	CPU nodes	558 2, 456K	7.80 31, 793	2.32 5, 134	1.87 4, 103	2.61 5, 854	1.87 4, 540	7.47 35, 028	5.90 29, 465	4.86 21, 120	2.60 4, 948
	ruler-34-9-a3	CPU nodes	24.5 18, 230	14.2 8, 011	13.8 8, 296	15.2 9, 254	16.8 11, 066	13.2 9, 144	9.30 7, 740	9.57 8, 647	10.7 10, 671	12.5 12, 767
	ruler-34-9-a4	CPU nodes	83.8 55, 129	20.5 11, 159	35.5 22, 480	34.2 22, 908	30.1 20, 840	16.7 8, 723	17.5 9, 163	26.3 15, 645	24.1 15, 714	28.9 20, 536
	tsp-20-366	CPU nodes	12.6 26, 777	11.3 24, 013	6.09 12, 286	6.06 10, 444	4.61 7, 564	1.67 2, 029	1.77 2, 261	2.32 3, 063	1.35 1, 457	1.15 1, 175
	tsp-25-190	CPU nodes	78.0 147K	29.3 56, 091	213 336K	88.7 133K	272 404K	66.6 83, 894	118 133K	175 232K	205 246K	64.9 83, 311

Table 7 :

 7 Number of instances from the second constraint solver competition solved within 20 minutes, given by category.

		bz		dom/ddeg	dom/wdeg
		LC 0	LC 1	LC 0	LC 1	LC 0	LC 1
	Categories of structured instances
	ACAD (#242)	136	146	123	136	132	138
	BOOL (#660)	306	336	312	342	388	390
	P AT T (#846)	379	425	390	431	451	455
	QRN D (#400)	378	400	290	400	400	400
	REAL (#400)	291	319	292	322	326	330
	Category of random instances
	RAN D (#745)	520	490	535	498	539	493
	T otal (#3, 293) 2, 010 2, 116 1, 942 2, 129 2, 236 2, 206

  Table 5 reports results on

Table 8 :

 8 Number of instances solved for planning domains (500 instances per domain, time-out is 30 minutes) and total time for instances solved by both.

			CPT
			LC 0	LC 1	Both
	BlocksWorld	#-instances CPU	383 78, 333	417 42, 504	383 -
	Depots	#-instances CPU	338 40, 606	401 14, 978	338 -
	DriverLog	#-instances CPU	384 64, 704	439 14, 613	384 -
	Logistics	#-instances CPU	399 107, 552	462 45, 387	399 -
	Rovers	#-instances CPU	347 53, 245	396 26, 371	347 -
	Satellite	#-instances CPU	442 63, 406	464 41, 149	442 -

Table 9 :

 9 CPU time (in seconds) required by CPT and CPT-LC 1 to solve instances from the fourth international planning competition.

		CPT
		LC0	LC1
	PipesWorld/NoTankage-NonTemporal
	p08-net1-b12-g7	0.58	0.76
	p09-net1-b14-g6	174.00	121.00
	p13-net2-b12-g3	2.94	5.71
	p15-net2-b14-g4	527.96	1, 450.65
	p17-net2-b16-g5	25.44	94.57
	p21-net3-b12-g2	466.36	385.90
	p24-net3-b14-g5	425.08	159.02
	PipesWorld/NoTankage-Temporal-Deadlines-Compiled
	p09-p09-net1-b14-g6-dl	127.29	0.47
	p11-p11-net2-b10-g2-dl	-	435.82
	p13-p13-net2-b12-g3-dl	-	79.13
	p17-p17-net2-b16-g5-dl	189.30	-
	Promela/Optical-Telegraph
	p04-opt5	4.21	3.18
	p05-opt6	12.58	7.81
	p06-opt7	50.84	17.46
	p07-opt8	177.78	39.33
	p08-opt9	633.42	107.76
	p09-opt10	-	277.54
	p10-opt11	-	720.61
	p11-opt12	-	1, 740.76
	PSR/Small
	p22-s37-n3-l3-f30	48.31	9.11
	p31-s49-n4-l2-f30	312.82	282.06
	p33-s51-n4-l2-f70	1.04	0.40
	p35-s57-n5-l2-f30	1.33	0.69
	p46-s97-n5-l2-f30	-	253.37
	p47-s98-n5-l2-f50	4.63	1.90
	p48-s101-n5-l3-f30	763.24	45.85
	Satellite/Time
	p08-pfile8	3.35	1.59
	p09-pfile9	1.30	1.06
	p10-pfile10	70.56	0.95
	p14-pfile14	-	1, 563.55
	p15-pfile15	-	1, 205.17
	p17-pfile17	55.61	62.81
	p18-pfile18	12.27	7.49
	Satellite/Time-TimeWindows-Compiled
	p04-pfile4	42.66	24.71
	p07-pfile7	478.59	365.33
	p08-pfile8	7.80	1.14
	p09-pfile9	-	0.89
	p17-pfile17	103.81	74.99
	p18-pfile18	6.82	5.91

Strictly speaking, DBT does not backtrack but simply discards the culprit decision.

By domain wipe-out, we mean a domain that becomes empty.

It has also been implemented in the WCSP (Weighted CSP) platform toulbar2 (see http: //carlit.toulouse.inra.fr/cgi-bin/awki.cgi/ToolBarIntro).

We assume here that φ(P ) is unique. This is the case for usual consistencies[START_REF] Bessiere | Constraint propagation[END_REF].

http://www.cril.univ-artois.fr/CPAI06/

http://uma.ensta.fr/conf/roadef-2001-challenge/

www.ps.uni-sb.de/ ~walser/radar/radar.html

http://ipc.icaps-conference.org

Acknowledgments

This paper has been supported by the CNRS, the "Planevo" project and the "IUT de Lens".

Search tree built by MAC-LC 1 (21 explored nodes). Circled nodes identify variables forming testing-sets. They point to grey areas where a culprit subsequence is sought. arc-consistent value (X 4 , 0) is found (after decisions X 0 = 0 and X 1 = 0), the testing-set becomes {X 4 , X 1 }. As any instantiation of these two variables systematically leads to a failure (when enforcing arc consistency), MAC-LC 2 is able to efficiently prove the unsatisfiability of this instance: MAC-LC 2 only explores 16 nodes (to be compared with the 68 and 21 explored nodes of MAC and MAC-LC 1 ).

A Small Example

Let us also introduce a toy problem, called the pawns problem, which illustrates the capability of generalized last-conflict reasoning to circumscribe the difficult parts of problem instances. The pawns problem consists in putting p pawns on squares of a chessboard of size n × n such that no two pawns can be put on the same square and the distance between two of them must be strictly less than p -1. Here, in our modelling, each square of a chessboard is numbered from 1 to n × n and the distance between two squares is the absolute value of the difference of their numbers. Then, p variables represent the pawns of the problem and their domain represent the n × n squares of the chessboard. For p ≥ 2, this problem is unsatisfiable (since it is equivalent to put p pawns on p -1 squares). Interestingly, we can show that, during a search performed by MAC, we may have to instantiate up to p -3 variables. We can merge this problem with the classical queens problem: pawns and queens cannot be put on the same square. Instances of this new queens-pawns problem are then denoted by qp-n-p with p the number of pawns and n the number of queens. This problem (like the queens-knights problem) produces a lot of thrashing. Indeed, in the worst case, the unsatisfiability of the pawns problem must be proved for each solution of the queens problem. Using LC p-2 ,