Éric Grégoire
email: gregoire@cril.fr

Jean-Marie Lagniez
email: lagniez@cril.fr

Bertrand Mazure
email: mazure@cril.fr

A CSP solver focusing on FAC variables ⋆

The contribution of this paper is twofold. On the one hand, it introduces a concept of FAC variables in discrete Constraint Satisfaction Problems (CSPs). FAC variables can be discovered by local search techniques and powerfully exploited by MAC-based methods. On the other hand, a novel synergetic combination schema between local search paradigms, generalized arcconsistency and MAC-based algorithms is presented. By orchestrating a multipleway flow of information between these various fully integrated search components, it often proves more competitive than the usual techniques on most classes of instances.

Introduction

These last decades, many research efforts have been devoted in the Artificial Intelligence community to the design of general algorithms and solvers for discrete Constraint Satisfaction Problems (in short, CSPs). Tracing back to the seminal work on simulated annealing by Kirkpatrick et al. [START_REF] Kirkpatrick | Optimization by simulated annealing[END_REF], stochastic local-search approaches (SLS) were investigated successfully in early pioneering works, mainly based on the so-called minconflicts heuristic developed by Minton et al. [START_REF] Minton | Minimizing conflicts: A heuristic repair method for constraint satisfaction and scheduling problems[END_REF]. They were considered powerful paradigms for CSPs -and their specific SAT case-in light of the results by e.g. Gu [START_REF] Gu | Design efficient local search algorithms[END_REF], Selman et al. [START_REF] Selman | A new method for solving hard satisfiability problems[END_REF] and Cheeseman et al. [START_REF] Cheeseman | Where the really hard problems are[END_REF].

However, apart from the specific SAT domain and with only a few exceptions (e.g. [START_REF] Galinier | Tabu search for maximal constraint satisfaction problems[END_REF], [START_REF] Jussien | Combining constraint programming and local search to design new powerful heuristics[END_REF], [START_REF] Eisenberg | Making the breakout algorithm complete using systematic search[END_REF], [START_REF] Eisenberg | Using the breakout algorithm to identify hard and unsolvable subproblems[END_REF]), the current mainstream approaches to general CSPs solving rely on complete methods that do not include SLS components as main tools (e.g., Abscon [START_REF] Merchez | Abscon: A prototype to solve CSPs with abstraction[END_REF][START_REF] Lecoutre | Abscon 112: towards more robustness[END_REF], Choco [START_REF] Team | Choco: an open source Java constraint programming library[END_REF], Mistral [START_REF] Hébrard | [END_REF], Sugar [START_REF] Tamura | Compiling finite linear CSP into SAT[END_REF], etc.). One reason lies in the fact that SLS is not an exhaustive search paradigm and does not allow by itself to prove the absence of any solution for a CSP. Moreover, SLS often entails significant computations and search-space explorations that advanced complete techniques are expected to attempt to avoid, at least partially. Finally, it is sometimes (but wrongly) believed that SLS should merely be devoted to situations where solutions are densely distributed throughout the state space, justifying some possible random aspects in the search.

On the contrary, this paper shows that complete and SLS techniques for solving CSPs can benefit one another. More precisely, it presents a synergetic combination of local search and elements of complete techniques that often outperforms the usual complete, SLS, or basic hybrid approaches involving (generalized) arc-consistency and SLS, in the following sense. This method is not only complete, it is also robust in the sense that it solves both satisfiable or unsatisfiable (structured or random) CSPs instances quite indifferently. Actually, our comprehensive experimental studies show that it solves more instances than the currently existing techniques.

One key issue is that the SLS computation that is guided as much as possible towards the most difficult subparts of the CSP can provide powerful oracles and information when some further steps of a complete search are required. Although this latter idea was already exploited in some previous works in the SAT domain [START_REF] Mazure | Boosting complete techniques thanks to local search methods[END_REF], it is refined here thanks to an original concept of FAC variables. FAC variables of a CSP, as Falsified in All Constraints, are variables occurring in all falsified constraints under some intrepretation, and thus in at least one constraint per minimal core (also called MUC, for Minimal Unsatisfiable Core) of the CSP when such cores exist. Interestingly, SLS often allows FAC variables to be detected efficiently and complete MAC-based techniques focusing first on FAC variables can have their efficiency boosted on many instances. Likewise, e.g. powerful heuristics (especially the dom/wdeg [START_REF] Boussemart | Boosting systematic search by weighting constraints[END_REF]) developed within complete CSP techniques can play an essential role in the SLS computation. Actually, the proposed method, called FAC-SOLVER, is an elaborate imbrication of SLS and steps of complete techniques that orchestrates a multiple-way flow of information between various fully integrated search components.

The paper is organized as follows. In the next Section, some basic technical background about CSPs is provided. Then, the FAC variable concept is presented. In Section 4, the architecture of the FAC-SOLVER method is presented globally, before each component is detailed. Comprehensive experimental studies are discussed in Section 5. In the conclusion, the focus is on perspectives and promising paths for future research.

CSPs Technical Background

A CSP or Constraint Network CN is a pair X , C where X is a finite set of n variables s.t. each variable X of X is associated with a finite set dom(X) of candidate values for X. C is a finite set of m constraints on variables from X s.t. each constraint C in C is associated with one relation rel(C) indicating the set of tuples of authorized values for the variables occurring in C. An assignment I of CN associates a value I(X) ∈ dom(X) to every variable X ∈ X . We note f alse(X , C, I) the set of variables that appear in at least one falsified constraint under the assignment I. X , C | X=v is the resulting CSP obtained from the CSP X , C by reducing dom(X) to the singleton {v} while X , C | X =v is obtained by deleting the v value in dom(X). We say that the assignment I is a local minimum for CN when no single change of value of any variable leads to a decrease of the total number of falsified constraints of CN .

Solving a constraint network CN consists in checking whether CN admits at least one assignment that satisfies all constraints of CN and in delivering such an assignment in the positive case.

In the following, we consider both binary and non-binary constraints. Most current complete approaches to solve constraints networks are based on algorithms implementing maintaining arc consistency techniques (in short, MAC) [START_REF] Sabin | Contradicting conventional wisdom in constraint satisfaction[END_REF]. Roughly, these techniques perform a depth-first search procedure with backtracking, while maintaining some forms of local (Generalized Arc) Consistency (in short GAC and AC), which are filtering techniques expelling detected forbidden values (see e.g. [START_REF] Mackworth | Consistency in networks of relations[END_REF][START_REF] Bessière | An optimal coarse-grained arc consistency algorithm[END_REF][START_REF] Lecoutre | A study of residual supports in arc consistency[END_REF]).

FAC variables

One key factor of the efficiency of the FAC-SOLVER approach relies on the following FAC (Falsified in All Constraints) variable concept. Definition 1. Let CN be a constraint network under an assignment I. A FAC variable is a variable occurring in every falsified constraint of CN under I.

This concept can be related to the notion of boundary point introduced by Goldberg in the SAT domain [START_REF] Goldberg | Boundary points and resolution[END_REF]. For a CNF formula, a variable is boundary under an assignment of all propositional variables if this variable belongs to all clauses that are falsified by the assignment. This definition is similar to the FAC one, but we have adopted an alternative name for a simple reason: in the CSP context, this kind of variables is not at the so-called "boundary", i.e., a situation where it is sufficient to inverse the truth value of a boundary variable to satisfy all falsified clauses. A FAC variable in the SAT domain thus draws a boundary line between satisfiabiliy and unsatisfiability of a part of the formula. In CSP, changing the value of a FAC variable does not ensure that constraints become satisfied. Accordingly, the notion of boundary as underlied by Goldberg cannot be applied in theCSP domain. For this reason we have decided to not use the same name. Nevertheless some interesting properties of boundary are preserved which can help understand the possible role of FAC variables for solving unsatisfiable CSPs.

Property 1. Any FAC variable X of CN occurs in at least one constraint per MUC of CN when CN is unsatisfiable. Indeed, under any assignment I, any MUC contains at least one falsified constraint. Thus, if a variable occurs within all constraints that are falsified under I, it occurs within at least one constraint per MUC.

Property 2. Unsatisfiable CSPs that exhibit at least two MUCs sharing no variable do not possess any FAC variable.

FAC variables can play a key role in the inconsistency of a CSP since they are involved in all of its unresolvable minimal sets of conflicting constraints. Accordingly, focusing a MAC-based search component first on FAC variables (when they exist) might thus help.

In the worst case, checking whether a constraint belongs to at least one MUC, belongs to the Σ p 2 complexity class [START_REF] Eiter | On the complexity of propositional knowledge base revision, updates and counterfactuals[END_REF]. Moreover, a CSP can possess an exponential number of MUCs. Thus, detecting FAC variables by first computing all MUCs is untractable in the worst case. On the contrary, SLS provides a heuristic way to detect FAC variables at low cost. One direct but inefficient way to detect some of them would consist in looking for FAC variables for each assignment crossed by SLS. For efficiency reasons, we will look for FAC variables only for assignments that are local minima w.r.t. the number of currently falsified constraints of the CSP.

Satisfiable CSPs can also exhibit FAC variables. Interestingly, it appears that FAC variables can also be expected to play a positive role for solving those CSPs. Indeed, to some extent, these variables can also be expected to take part in the difficult part of those CSPs since they are involved in all falsified constraints under at least one assignment. Accordingly, it could be also useful to focus on them during a complete search.

Finally, it must be noted that when some variables are instantiated, a new CSP is actually created. FAC variables w.r.t. this new CSP can exist; they are not necessarily FAC variables w.r.t. the initial CSP.

In the FAC-SOLVER method, all FAC variables that can be detected when local minima are reached during a SLS will be collected. When a MAC-based component must be run thereafter, it will focus first on the FAC variables in hope for an improved efficiency.

Using FAC variables in a further systematic search component appears to be a refinement of some heuristics e.g. used in the SAT framework and involving hybrid SLS-DPLL algorithms. For example, [START_REF] Mazure | Boosting complete techniques thanks to local search methods[END_REF] advocates to select the next variables to be assigned in a DPLL-based search for satisfiability among the variables belonging to the most often falsified clauses during a preliminary failed SLS, as those variables probably belong to minimal cores of the instance. Also [START_REF] Gégoire | Local-search extraction of muses[END_REF] recommends the use of critical clauses, i.e., falsified clauses during a failed SLS that are such that any flip of a variable causes at least another clause to be falsified. Critical clauses were also shown to often belong to minimal cores. Branching on variables occurring in them appeared to boost the further complete search process [START_REF] Audemard | Boosting local search thanks to CDCL[END_REF]. FAC variables do not only occur in one minimal core but in all of them. Branching on them might thus increase the efficiency of the search process even more significantly. The FAC-SOLVER method described in the next Section was intended to implement and check these ideas on a large panel of instances.

FAC-SOLVER Approach

The FAC-SOLVER approach deeply integrates three search components in a novel synergetic way: a SLS, a MAC and an hybrid solver, which is itself mixing SLS and GAC. These components interact in several ways and share all information about the current global search process. The global architecture of FAC-SOLVER is described in Figure 1. Roughly, the process starts with a call to one SLS solver, then in the case of failure a hybrid solver is run followed by a limited MAC. Calls between different components depend on dynamical threshold values for two variables that play a strategic role, namely SLSprogress and #conf licts.

Algorithm 1 describes the FAC solver. First, a call to GAC ensures arc-consistency (or delivers a final inconsistency proof) and leads to some possible filterings (lines 4-5). Next, while a solution is not found or the problem is not proved inconsistent, the solver sequentially performs the three components described in the next sections. The number of conflicts maxConf controls the restart associated to the Hybrid and MAC parts. It is initialized to 10 (line 2) and is geometrically increased at each iteration step of the

The SLS Component

Let us detail the SLS procedure first which is described in a simplified way in the algorithm named Procedure SLS. It is a random-walk local search procedure à la walksat [START_REF] Selman | Noise strategies for improving local search[END_REF] with a novelty escape strategy [START_REF] Mcallester | Evidence for invariants in local search[END_REF]. In parallel, this SLS also tries to detect FAC variables each time a local minimum is reached. The variable controlling the progress of the SLS is SLSprogress, which is increased in two situations: when the number of falsified constraints reaches a new minimum value (line 13) and when FAC variables are discovered (line 5). It is decreased when no FAC variable is discovered in a local minimum (line 6). This variable is intialized to 10.000 if the CSP is binary and to 1.000 otherwise. This way to estimate the progress of the SLS is inspired from the adaptative noise introduced by Hoos et al. in [START_REF] Hoos | An adaptive noise mechanism for walksat[END_REF]. When the SLS fails to prove the consistency of the CSP but seems rather stuck in its exploration, the SLSprogress < 0 test (line 7) allows the so-called Hybrid component to be activated, which will exploit in its turn all the information collected so-far. Intuitively, in addition to looking for an assignment satisfying the CSP, the SLS solver collects information about FAC variables. Due to the larger increment of the SLSprogress control variable when FAC variables are discovered, it focuses its exploration on assignments that are close to local minima involving FAC variables. The SLS procedure is also used by the hybrid component. When this procedure is called by the hybrid component, the SLS works on a sub-CSP that is downsized by the various calls to the FIX procedure which is described in the next section. At the opposite, during the initial local search, SLS is handling the full CSP.

Hybrid SLS-GAC Component

The hybrid component allows to focus on expected difficult subparts of the instance. This allows to get FAC variables that are linked to the (expected) most difficult subparts to satisfy. This component is described in Procedure Hybrid. Roughly, starting with the current assignment A provided by the SLS component, a variable in a violated constraint is selected and is assigned according to A (lines 4-5). The dom/wdeg heuristic [START_REF] Boussemart | Boosting systematic search by weighting constraints[END_REF] is used as a tiebreaker amongst the set of variables of a violated constraint. A call is made to the FIX procedure (line 6), which operates and propagates GAC (Generalized Arc-Consistency) filtering steps. This procedure detects also conflicts (i.e., empty domains for variables in X ) which trigger a backtrack on the last fixed variables (line [START_REF] Cheeseman | Where the really hard problems are[END_REF][START_REF]Third international CSP solver competition[END_REF][START_REF]Fourth international CSP solver competition[END_REF][START_REF] Eisenberg | Making the breakout algorithm complete using systematic search[END_REF][START_REF] Eisenberg | Using the breakout algorithm to identify hard and unsolvable subproblems[END_REF][START_REF] Eiter | On the complexity of propositional knowledge base revision, updates and counterfactuals[END_REF][START_REF] Galinier | Tabu search for maximal constraint satisfaction problems[END_REF][START_REF] Goldberg | Boundary points and resolution[END_REF]. The GAC version used in the solver is based on AC3 [START_REF] Mackworth | Consistency in networks of relations[END_REF]. The FIX procedure reduces the domain variables of X which is shared by all components. In fact, during the Hybrid procedure, SLS is still running but waits for decisions and does neither revise them nor the propagations done by the FIX procedure. The assignment A, used by SLS, is thus in part fixed by this hybridization. In some sense, those fixed variables are tabu for SLS.

The variable #conf measures the number of encountered conflicts. After the FIX procedure and when this number has become strictly larger than the dynamical max-Conf threshold, it is estimated that the hydrid component is stuck and a call to MAC is

Procedure SLS while ∃C ∈ C s.t. C is violated by A do 1 if a local minimum is reached then 2 if ∃ FAC variables then

MAC-based Component

The MAC-based component starts with the initial CSP with the exception of filterings computed at level 0 during the SLS and the calls to FIX (line 1). This procedure is a standard MAC algorithm except that the focus is on collected FAC variables. The heuristic used to selected variable is dom/wdeg. For the first choices (lines 8-9), the variable is selected amongst the FAC variables collected during the SLS procedure. The next choices (line 11) are made within all variables. The use of FAC variables only for the first choices can be explained by the fact that the dom/wdeg heuristics allows to focus on the same inconsistent part (i.e., on the same core) whereas fixing another FAC

Experimental Results

In order to assess the efficiency of FAC-SOLVER, we have considered benchmarks from the last CSP competitions [START_REF]Third international CSP solver competition[END_REF][START_REF]Fourth international CSP solver competition[END_REF], which include binary vs. non-binary, random vs. reallife, satisfiable vs. unsatisfiable CSP instances. They were classified according to four types: 635 CSPs made of binary constraints in extension (BIN-EXT), 696 CSPs made of binary constraints in intension (BIN-INT), 704 CSPs involving n-ary constraints in extension (N-EXT) and 716 instances of CSPs of n-ary constraints in intention (N-INT). We have run four methods on all those instances: namely, our own implementation of SLS Walksat+Novelty, of an hybrid method combining SLS and GAC, of MAC and FAC-SOLVER. All tests have been conducted on a Xeon 3.2 GHz (2 G RAM) under Linux 2.6. Time-out has been set to 1200 seconds while a space limit has been set to 900 Mbytes. Note that the MAC version used in the experimentations makes use of a geometric restart policy that is similar way to our solver. Similarly, the SLS solver (Walksat+Novelty) used in our experimental comparison uses the same novelty heuristic than our solver. Note that, the solved unsatisfiable instances by novelty have been solved by GAC on the initial instance.

Table 1 summarizes the results in terms of the numbers of satisfiable and unsatisfiable instances that were solved. In each horizontal "total"-line, the solver that solves the most instances has been emphasized in gray. The main result is that FAC-SOLVER managed to solve more instances than any of the other methods globally for either satisfiable (SAT) or unsatisfiable (UNSAT) instances, and considering the subclasses of instances separately, for three types of CSPs. For the last type (binary CSP in extension), let us stress that the best solver is different in each of the three columns (SAT, UNS(AT) and TOT(AL)) and in each case, the number of solved instances by FAC-SOLVER is very close to the best one.

In Figure 2, five scatter points diagrams are given for a more detailed analysis. In each of them, two of the methods are pairwise compared w.r.t. instances that were solved by at least one of them. The X-axis represents the computing times in seconds by FAC-SOLVER whereas the Y-axis provides the performance of the second method. Results are expressed in seconds and represented according to a logarithmic scale. Instances were divided within the four classes detailed above. We provide separate diagrams for SAT and UNSAT instances. FAC-SOLVER is not compared with Walk-sat+Novelty on UNSAT instances since these instances are out of scope for the latter technique. The main information that can be drawn from these diagrams is as follows.

-More instances are located on the Y=1200 line than on the X=1200 one. This shows, as Table 1 summarizes it, that FAC-SOLVER solves more instances than any of the other considered methods. -With the exceptions of UNSAT instances for MAC, there are more points located above the diagonals showing that FAC-SOLVER is generally more efficient than the other methods. Also, for UNSAT instances, the difference of time performance between pairs of methods is globally smaller than for SAT instances (points are less dispersed and are closer to the diagonal). FAC-SOLVER is generally more efficient than a mere combination of SLS and GAC. It is also more efficient than MAC on SAT instances (mainly due to the power of SLS). But there is no free lunch, the time spent on SLS by FAC-SOLVER on UNSAT instances leads to some small and very acceptable time overheads, compared with MAC. This is perhaps the price to pay to solve more unsatisfiable instances than MAC within the same price constraints, thanks to the collected information by SLS.

An important issue is the way according to which the efficiency of FAC-SOLVER might depend on the specific initial assignment selected by its SLS component. Actually, it appears that, on average, this dependency is weak and is not a serious troubling factor affecting the results. To show this robustness, we have selected 96 instances within the above benchmarks in a random fashion but according to their relative importance in each of the four classes of instances. For each of these instances, 50 successive runs of FAC-SOLVER have been conducted with a different initial (randomly generated) assignment. When an instance was solved by at least one run, it was also solved by the 49 other runs in 97 % of the situations, with a very low 2.52 seconds average deviation.

To show the importance of FAC variables, we have run our solver with and without computing and using the FAC variables. Table 2 provides typical results. The use of FAC variables allows more instances to be solved. Most of the time, the use of FAC variables can solve benchmarks more quickly. In rare cases, the use of FAC variables wastes time. This is because the solver wastes time to compute FAC variables that are not used when the instance is solved directly by the SLS solver or when the benchmarks is globally inconsistent. In this case, all variables are potentially FAC variables and their computation also wastes time.

Perspectives and Conclusions

In this paper a FAC variables concept has been introduced and investigated w.r.t. CSP solving. One goal of this study was to develop a CSP solving method that would at least match the efficiency of each best current approach on each class of traditional CSPs instances. In this respect, our experimental results show the extent to which this goal has been met.

One question that naturally arises is the extent to which the various findings and components implemented in FAC-SOLVER do actually take part in the increased efficiency. Actually, it appears that each finding and search component (FAC variables, use of dom/wdeg heuristic in SLS, hybrid method involving SLS and filtering techniques) were necessary to ensure the supremacy of the method. Especially, we have e.g. measured that FAC variables were detected in 56 % of the instances and that they play a crucial role even in consistent instances.

FAC-SOLVER remains a basic algorithm and could be fine-tuned in several ways. Especially, comprehensive experimental studies could allow to optimize its various control variables and factors, which we fixed quite arbitrarily. Moreover, our implementation does not include usual CSP simplification techniques like the exploitation of symmetries or global constraints. We believe that the integration of these techniques could also dramatically improve FAC-SOLVER. Also, it would be interesting to explore the relaxation of the FAC variable concept to encompass also variables that occur in most or some preferred falsified contraints (instead of all of them). This could prove useful for e.g. CSP instances containing non-overlapping MUCs. Finally, we believe that the FAC variable concept is a good trade-off between the effective computational cost spent by SLS to find some of them, and what would be the theoretically best branching variable for MAC-based algorithm giving rise to the shortest proofs. FAC variables are variables taking part in all unsatisfiable minimal subsets of constraints, which often appear to be the difficult parts of unsatisfiable CSPs. However, it is easy to find out unsatisfiable CSPs where FAC variables do not conceptually take part in the real causes of unsatisfiability but rather simply appear as variables occurring in all MUCs while, at the same time, they are not related to the actual conflicting information. Refining the FAC variable concept to better capture the essence of unsatisfiability while keeping efficient heuristics that can help finding them remains an exciting challenge.

Fig. 1 .

 1 Fig. 1. Interactions between FAC-SOLVER basic search components.

3 5 else 6 if 7 else 8 9 strategy ; else 10 Change 1 # 3 X

 567891013 add new FAC variables to Se; 4 SLSprogress ←-SLSprogress + 1000 ; SLSprogress ←-SLSprogress -1 ; SLSprogress < 0 then return; Change the value in A of one var. of X according to the novelty escape the value in A of one var. of X s.t. the number of violated constraints 11 decreases ; if A new best configuration is obtained then 12 SLSprogress ←-SLSprogress + 1000 ; 13 result ←true ; 14 made. When this threshold is not reached the search goes back to the SLS component, the collected filtering information being preserved. Procedure Hybrid level ←-0; conf ←-0 ; 2 while (#conf < maxConf ) do ←pick a variable according to dom/wdeg s.t. X appears in violated constraint 4 by A ; v ←the value of X in A ; 5 FIX(X, v) ; 6 if (result = f alse) then return ; 7 SLS() ;

8

 8

  (a) FAC-SOLVER vs. NOVELTY (b) FAC-SOLVER vs. SLS+GAC

Fig. 2 .

 2 Fig. 2. Pairwise comparisons between FAC-SOLVER and classical solvers: (a) (b) (c) satisfiable instances/(d) (e) unsatisfiable instances.

Fig. 2 .

 2 Fig. 2. Pairwise comparisons between FAC-SOLVER and classical solvers: (a) (b) (c) satisfiable instances/(d) (e) unsatisfiable instances (con't).

Fig. 2 .

 2 Fig. 2. Pairwise comparisons between FAC-SOLVER and classical solvers: (d) (e) unsatisfiable instances (con't).

Table 1 .

 1 Experimental results.

			NOVELTY	SLS+GAC		MAC		FAC-SOLVER
			SAT UNS TOT	SAT UNS TOT	SAT UNS TOT	SAT UNS TOT
		ACAD	7	0	7	7	2	9	7	2	9	7	2	9
	2-EXT	PATT 106 QRND 24 RAND 206	0 0 0	106 100 38 138 24 24 51 75 206 197 105 302 194 110 304 83 38 121 24 51 75	99 24 193 106 299 39 138 51 75
		REAL	6	0	6	7	0	7	7	0	7	7	0	7
		TOTAL 349 0	349 335 196 531 315 201 516	330 198 528
	2-INT	ACAD 38 BOOL 0 PATT 112	7 1 0	45 1 112 150 60 210 146 62 208 37 40 77 37 40 77 0 1 1 0 1 1	38 0 152 62 214 40 78 1 1
		REAL	47	74 121	74 102 176	75 103 178	75 103 178
		TOTAL 197 82 279 261 203 464 258 206 464	265 206 471
		BOOL	70	1	71	74	75 149	74	70 144	74	74 148
	N-EXT	PATT QRND 43 6 RAND 70	0 0 0	6 43 70	30 40 68	0 40 32 100 30 80	29 33 72	0 40 34 106 29 73	30 45 70	0 40 34 104 30 85
		REAL	41	29	70	45 114 159	47 115 162	47 115 162
		TOTAL 230 30 260 257 261 518 255 259 514	266 263 529
	N-INT	ACAD 40 BOOL 145 PATT 88	0 1 5	40 146 156 12 168 146 12 158 39 23 62 36 23 59 93 103 19 122 95 20 115	40 162 13 175 23 63 102 18 120
		REAL	85	2	87	152	3	155 150	3	153	152	3	155
		TOTAL 358	8	366 450 57 507 427 58 485	456 57	513
		TOTAL 1134 113 1247 1293 717 2010 1255 724 1979 1317 724 2041

Table 2 .

 2 Using or not FAC variables in FAC-SOLVER: typical results.

	Instance	SAT/UNSAT? time (FAC-SOLVER) time (FAC-SOLVER without
				FAC variables)
	uclid-elf-rf8	UNSAT	305.15	time out
	uclid-37s-smv	UNSAT	387.50	659.58
	par-16-5	SAT	168.87	329.06
	primes-10-40-2-7	SAT	891.01	time out
	primes-20-20-2-7	SAT	976.68	313.31
	queensKnights-100-5-add	UNSAT	1,120.18	time out
	queensKnights-100-5-mul	UNSAT	1,165.81	time out
	queensKnights-80-5-mul	UNSAT	343.68	time out
	rand-2-40-18	UNSAT	41.47	1.61

⋆ Part of this work was supported by the French Ministry of Higher Education and Research, Nord/Pas-de-Calais Regional Council and E.C. FEDER program through the 'Contrat de Projets État/Région (CPER) 2007-2013' and by the French National Research Agency (ANR) through the UNLOC and TUPLES projects.

Procedure FIX(X, v) dom(X) ←-{v} ;

12 variable can lead the search to be dispersed and slowing down the discovery of a small proof of inconsistency.

The weights used by the dom/wdeg heuristic are preserved from one iteration to the next one in Algorithm 1, and are shared by all search components.

Moreover, this MAC procedure does not necessarily perform a complete search since if the number of conflicts #conf becomes larger than the maxConf before a final decision is obtained, then the process goes back to the SLS component. In this latter case, the maxConf control variable is increased in a geometric manner.

As maxConf is increased whenever the MAC component fails, this component will eventually give a final result when this boundary becomes larger than the number of conflicts needed by MAC to solve the CSP. Accordingly, FAC-SOLVER is complete.

Procedure MAC Backjump(0) ; // backjump to level 0


Jean-François Condotta
email: condotta@cril.fr

Christophe Lecoutre
email: lecoutre@cril.fr

A Framework for Decision-based Consistencies

Consistencies are properties of constraint networks that can be enforced by appropriate algorithms to reduce the size of the search space to be explored. Recently, many consistencies built upon taking decisions (most often, variable assignments) and stronger than (generalized) arc consistency have been introduced. In this paper, our ambition is to present a clear picture of decision-based consistencies. We identify four general classes (or levels) of decision-based consistencies, denoted by S φ ∆ , E φ ∆ , B φ ∆ and D φ ∆ , study their relationships, and show that known consistencies are particular cases of these classes. Interestingly, this general framework provides us with a better insight into decision-based consistencies, and allows us to derive many new consistencies that can be directly integrated and compared with other ones.

Introduction

Consistencies are properties of constraint networks that can be used to make inferences. Such inferences are useful to filter the search space of problem instances. Most of the current constraint solvers interleave inference and search. Typically, they enforce generalized arc consistency (GAC), or one of its partial form, during the search of a solution. One avenue to make solvers more robust is to enforce strong consistencies, i.e., consistencies stronger than GAC. Whereas GAC corresponds to the strongest form of local reasoning when constraints are treated separately, strong consistencies necessarily involve several constraints (e.g., path inverse consistency [START_REF] Freuder | Neighborhood inverse consistency preprocessing[END_REF], max-restricted path consistency [START_REF] Debruyne | From restricted path consistency to max-restricted path consistency[END_REF] and their adaptations [START_REF] Stergiou | Inverse consistencies for non-binary constraints[END_REF] to non-binary constraints) or even the entire constraint network (e.g., singleton arc consistency [START_REF] Debruyne | Some practical filtering techniques for the constraint satisfaction problem[END_REF]).

A trend that emerges from recent works on strong consistencies is the resort to taking decisions before enforcing a well-known consistency (typically, GAC) and making some deductions. Among such decision-based consistencies, we find SAC (singleton arc consistency), partition-k-AC [START_REF] Bennaceur | Partition-k-AC: An efficient filtering technique combining domain partition and arc consistency[END_REF], weak-k-SAC [START_REF] Van Dongen | Beyond singleton arc consistency[END_REF], BiSAC [START_REF] Bessiere | Theoretical analysis of singleton arc consistency and its extensions[END_REF], and DC (dual consistency) [START_REF] Lecoutre | Second-order consistencies[END_REF]. Besides, a partial form of SAC, better known as shaving, has been introduced for a long time [START_REF] Carlier | Adjustments of heads and tails for the job-shop problem[END_REF][START_REF] Martin | A new approach to computing optimal schedules for the job-shop scheduling problem[END_REF] and is still an active subject of research [START_REF] Lhomme | Quick shaving[END_REF][START_REF] Szymanek | Constraint-level advice for shaving[END_REF]; when shaving systematically concerns the bounds of each variable domain, it is called BoundSAC [START_REF] Lecoutre | Maintaining singleton arc consistency[END_REF]. What makes decision-based consistencies particularly attractive is that they are (usually) easy to define and understand, and easy to implement since they are mainly based on two concepts (decision, propagation) already handled by constraint solvers. The increased interest perceived in the community for decision-based consistencies has motivated our study.

In this paper, our ambition is to present a clear picture of decision-based consistencies that can derive nogoods of size up to 2; i.e., inconsistent values or inconsistent pairs of values. The only restriction we impose is that decisions correspond to unary constraints. The four classes (or levels) of consistencies, denoted by S φ ∆ , E φ ∆ , B φ ∆ and D φ ∆ , that we introduce are built on top of a consistency φ and a so-called decision mapping ∆. These are quite general because:

1. ∆ allows us to introduce a specific set of decisions for every variable x and every possible (sub)domain of x, 2. decisions are membership decisions (of the form x ∈ D x where D x is a set of values taken from the initial domain of x) that generalize both variable assignments (of the form x = a) and value refutations (of the form x = a), 3. decisions may ignore some variables and/or values, and decisions may overlap each other, 4. φ is any well-behaved nogood-identifying consistency.

We study the relationships existing between them, including the case where ∆ covers every variable and every value. We also show that SAC, partitionk-AC, BiSAC and DC are particular cases of S φ ∆ , S φ ∆ +E φ ∆ (the two consistencies combined), B φ ∆ and D φ ∆ , respectively. BoundSAC, and many other forms of shaving, are also elements of the class S φ ∆ . The general framework we depict provides a better insight into decision-based consistencies while allowing many new combinations and comparisons of such consistencies. For example, the class of consistencies S φ ∆ induces a complete lattice where the partial order denotes the relative strength of every two consistencies.

Technical Background

This section provides technical background about constraint networks and consistencies, mainly taken from [START_REF] Apt | Principles of Constraint Programming[END_REF][START_REF] Dechter | Constraint processing[END_REF][START_REF] Bessiere | Constraint propagation[END_REF][START_REF] Lecoutre | Constraint networks: techniques and algorithms[END_REF].

Constraint Networks. 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 a domain which is the finite set of values that can be assigned to x. Each constraint c involves an ordered set of variables, called the scope of c and denoted by scp(c), and is defined by a relation which is the set of tuples allowed for the variables involved in c. The initial domain of a variable x is denoted by dom init (x) whereas the current domain of x (in the context of P ) is denoted by dom P (x), or more simply dom(x). Assuming that the initial domain of each variable is totally ordered, min(x) and max(x) will denote the smallest and greatest values in dom(x). The initial and current relations of a constraint c are denoted by rel init (c) and rel(c), respectively.

A constraint is universal iff rel init (c) = Π x∈scp(c) dom init (x). For simplicity, a pair (x, a) with x ∈ vars(P ) and a ∈ dom(x) is called a value of P , which is denoted by (x, a) ∈ P . A unary (resp., binary) constraint involves 1 (resp., 2) variable(s), and a non-binary one strictly more than 2 variables. Without any loss of generality, we only consider CNs that do not involve unary constraints, universal constraints and constraints of similar scope. The set of such CNs is denoted by P. An instantiation I of a set ). An instantiation I on a CN P is locally consistent iff (i) I is valid on P and (ii) every constraint of P covered by I is satisfied by I. A solution of P is a complete locally consistent instantiation on P ; sols(P ) denotes the set of solutions of P . An instantiation I on a CN P is globally inconsistent, or a nogood, iff it cannot be extended to a solution of P . Two CNs P and P ′ are equivalent iff vars(P ) = vars(P ′ ) and sols(P ) = sols(P ′ ).

X = {x 1 , . . . , x k } of variables is a set {(x 1 , a 1 ), . . ., (x k , a k )} such that ∀i ∈ 1..k, a i ∈ dom init (x i ); X is
The nogood representation of a CN is a set of nogoods, one for every value removed from the initial domain of a variable and one for every tuple forbidden by a constraint. More precisely, the nogood representation x of a variable x is the set

{(x, a)} | a ∈ dom(x) with dom(x) = dom init (x) \ dom(x).
The nogood representation c of a constraint c is {(x 1 , a 1 ) , . . . , (x r , a r )} | (a 1 , . . . , a r ) ∈ rel(c) , with scp(c) = {x 1 , . . . , x r } and rel(c) = Π x∈scp(c) dom init (x) \ rel(c). The nogood representation P of a CN P is ∪ x∈vars(P ) x ∪ ∪ c∈cons(P ) c . Based on nogood representations, a general partial order can be introduced to relate CNs. Let P and P ′ be two CNs such that vars(P ) = vars(P ′ ), we have P ′ P iff P ′ ⊇ P and we have P ′ ≺ P iff P ′ P . (P, ) is the partially ordered set (poset) considered in this paper. The search space of a CN can be reduced by a filtering process (called constraint propagation) based on some properties (called consistencies) that allow us to identify and record explicit nogoods in CNs; e.g., identified nogoods of size 1 correspond to inconsistent values that can be safely removed from variable domains. In P, there is only one manner to discard an instantiation from a given CN, or equivalently to "record" a new explicit nogood. Given a CN P in P, and an instantiation I on P , P \ I denotes the CN P ′ in P such that vars(P ′ ) = vars(P ) and P ′ = P ∪ {I}. P \ I is an operation that retracts I from P and builds a new CN. If I = {(x, a)}, we remove a from dom(x). If I corresponds to a tuple allowed by a constraint c of P , we remove this tuple from rel(c). Otherwise, we introduce a new constraint allowing all possible tuples (from initial domains) except the one that corresponds to I.

Consistencies. A consistency is a property defined on CNs. When a consistency φ holds on a CN P , we say that P is φ-consistent; if ψ is another consistency, P is φ+ψ-consistent iff P is both φ-consistent and ψ-consistent. A consistency φ is nogood-identifying iff the reason why a CN P is not φ-consistent is that some instantiations, which are not in P , are identified as globally inconsistent by φ; such instantiations are said to be φ-inconsistent. A kth-order consistency is a nogood-identifying consistency that allows the identification of nogoods of size k. A domain-filtering consistency [START_REF] Debruyne | Domain filtering consistencies[END_REF][START_REF] Bessiere | Domain filtering consistencies for nonbinary constraints[END_REF] is a first-order consistency. A nogoodidentifying consistency is well-behaved when for any CN P , the set {P ′ ∈ P | P ′ is φ-consistent and P ′ P } admits a greatest element, denoted by φ(P ), equivalent to P . Enforcing φ on a CN P means computing φ(P ). Any wellbehaved consistency φ is monotonic: for any two CNs P and P ′ , we have: P ′ P ⇒ φ(P ′ ) φ(P ). To compare the pruning capability of consistencies, we use a preorder. A consistency φ is stronger than (or equal to) a consistency ψ, denoted by φ ψ, iff whenever φ holds on a CN P , ψ also holds on P . φ is strictly stronger than ψ, denoted by φ ⊲ ψ, iff φ ψ and there is at least a CN P such that ψ holds on P but not φ. φ and ψ are equivalent, denoted by φ ≈ ψ, iff both φ ψ and ψ φ.

Now we introduce some concrete consistencies, starting with GAC (Generalized Arc Consistency). A value (x, a) of P is GAC-consistent iff for each constraint c of P involving x there exists a valid instantiation I of scp(c) such that I satisfies c and I[x] = a. P is GAC-consistent iff every value of P is GACconsistent. For binary constraints, GAC is often referred to as AC (Arc Consistency). Now, we introduce known consistencies based on decisions. When the domain of a variable of P is empty, P is unsatisfiable (i.e., sols(P ) = ∅), which is denoted by P = ⊥; to simplify, we consider that no value is present in a CN P such that P = ⊥. The CN P | x=a is obtained from P by removing every value [START_REF] Bennaceur | Partition-k-AC: An efficient filtering technique combining domain partition and arc consistency[END_REF]. A value (x, a) of P is BiSAC-consistent iff GAC (P ia | x=a ) = ⊥ where P ia is the CN obtained after removing every value (y, b) of P such that y = x and (x, a) / ∈ GAC(P | y=b ) [START_REF] Bessiere | Theoretical analysis of singleton arc consistency and its extensions[END_REF]. P is SAC-consistent (resp., 1-AC-consistent, BiSAC-consistent) iff every value of P is SAC-consistent (resp., 1-AC-consistent, BiSAC-consistent). P is BoundSACconsistent iff for every variable x, min(x) and max(x) are SAC-consistent [START_REF] Lecoutre | Maintaining singleton arc consistency[END_REF]. A decision-based second-order consistency is dual consistency (DC) defined as follows. A locally consistent instantiation {(x, a), (y, b)} on P , with y = x, is DC-consistent iff (y, b) ∈ GAC (P | x=a ) and (x, a) ∈ GAC (P | y=b ) [START_REF] Lecoutre | Conservative dual consistency[END_REF]. P is DC-consistent iff every locally consistent instantiation {(x, a), (y, b)} on P is DC-consistent. P is sDC-consistent (strong DC-consistent) iff P is GAC+DCconsistent, i.e. both GAC-consistent and DC-consistent. All consistencies mentioned above are well-behaved. Also, we know that sDC ⊲ BiSAC ⊲ 1-GAC ⊲ SAC ⊲ BoundSAC ⊲ GAC.

b = a from dom(x). A value (x, a) of P is SAC-consistent iff GAC (P | x=a ) = ⊥ [9]. A value (x, a) of P is 1-AC-consistent iff (x, a) is SAC-consistent and ∀y ∈ vars(P ) \ {x}, ∃b ∈ dom(y) | (x, a) ∈ GAC (P | y=b )

Decision-based Consistencies

In this section, we introduce decisions before presenting general classes of consistencies.

Decisions

A positive decision δ is a restriction on a variable x of the form x = a whereas a negative decision is a restriction of the form x = a, with a ∈ dom init (x). A membership decision is a decision of the form x ∈ D x , where x is a variable and D x ⊆ dom init (x) is a non-empty set of values; note that D x is not necessarily dom(x), the current domain of x. Membership decisions generalize both positive and negative decisions as a positive (resp., negative) decision x = a (resp., x = a) is equivalent to the membership decision x ∈ {a} (resp., x ∈ dom init (x) \ {a}). The variable involved in a decision δ is denoted by var(δ).

For a membership decision δ, we define P | δ to be the CN obtained (derived) from P such that, if δ denotes x ∈ D x and if x is a variable of P then each value b ∈ dom P (x) with b / ∈ D x is removed from dom P (x). If Γ is a set of decisions, P | Γ is obtained by restricting P by means of all decisions in Γ , and vars(Γ ) denotes the set of variables occurring in Γ . Enforcing a given well-behaved consistency φ after taking a decision δ on a CN P may be quite informative. As seen later, analyzing the CN φ(P | δ ) allows us to identify nogoods. Computing φ(P | δ ) in order to make such inferences is called a decision-based φ-check on P from δ, or more simply a decision-based check. For SAC, a decision-based check from a pair (x, a), usually called a singleton check, aims at comparing GAC(P | x=a ) with ⊥.

From now on, ∆ will denote a mapping, called decision mapping, that associates with every variable x and every possible domain dom x ⊆ dom init (x), a (possibly empty) set ∆(x, dom x ) of membership decisions on x such that for every decision x ∈ D x in ∆(x, dom x ), we have D x ⊆ dom x . For example, an illustrative decision mapping ∆ ex may be such that ∆ ex (x, {a, b, c, d}) = {x ∈ {a, b}, x ∈ {d}}. For the current domain of x, i.e., the domain of x in the context of a current CN P , ∆(x, dom(x)) = ∆(x, dom P (x)) will be simplified into ∆(x) when this is unambiguous. To simplify, we shall also refer to ∆ as the set of all "current" decisions w.r.t. P , i.e., ∆ will be considered as ∪ x∈vars(P ) ∆(x). This quite general definition of decision mapping will be considered as our basis to perform decision-based checks. Sometimes, we need to restrict sets of decisions in order to have each value occurring at least once in a decision. A set of decisions Γ on a variable x is said to be a cover of ∪ (x∈Dx)∈Γ D x . For example, ∆ ex (x, {a, b, c, d}), as defined above, is a cover of {a, b, d}. ∆ is a cover for (x, dom x ), where dom x ⊆ dom init (x), iff ∆(x, dom x ) is a cover of dom x . For example, ∆ ex is not a cover for (x, {a, b, c, d}). ∆ is a cover for x iff for every

dom x ⊆ dom init (x), ∆ is a cover for (x, dom x ). ∆ is covering iff for every variable x, ∆ is a cover for x.
As examples of decision mappings, we have for every variable x:

-∆ id (x) containing only x ∈ dom(x); -∆ = (x) containing x = a, ∀a ∈ dom(x); -∆ = (x) containing x = a, ∀a ∈ dom(x); -∆ bnd (x) containing x = min(x) and x = max(x); -∆ P2 (x) containing x ∈ D 1 x and x ∈ D 2
x where D 1 x and D 2 x resp. contain the first and last |dom(x)|/2 values of dom(x).

For example, if P is a CN such that vars(P ) = {x, y} with dom(x) = dom P (x) = {a, b, c} and dom(y) = dom P (y) = {a, b} then:

-∆ id (x) = {x ∈ {a, b, c}} and ∆ id (y) = {y ∈ {a, b}}; -∆ = (x) = {x = a, x = b, x = c} and ∆ = (y) = {y = a, y = b}; -∆ = (x) = {x = a, x = b, x = c} and ∆ = (y) = {y = a, y = b}; -∆ bnd (x) = {x = a, x = c} and ∆ bnd (y) = {y = a, y = b}; -∆ P2 (x) = {x ∈ {a, b}, x = c} and ∆ P2 (y) = {y = a, y = b}.
Note that, except for ∆ bnd , all these decision mappings are covering. Also, the reader should be aware of the dynamic nature of decision mappings. For example, if P ′ is obtained from P after removing a from dom P (x) then we have

∆ bnd (x, dom P ′ (x)) = {x = b, x = c}.

Two Classes of First-order Consistencies

Informally, a decision-based consistency is a property defined from the outcome of decision-based checks. From now on, we consider given a well-behaved nogoodidentifying consistency φ and a decision mapping ∆. A first kind of inferences is made possible by considering the effect of a decision-based check on the domain initially reduced by the decision that has been taken.

Definition 1 (Consistency S φ ∆ ). A value (x, a) of a CN P is S φ ∆ -consistent iff for every membership decision x ∈ D x in ∆(x) such that a ∈ D x , we have (x, a) ∈ φ(P | x∈Dx ).
The following result can be seen as a generalization of Property 1 in [START_REF] Bennaceur | Partition-k-AC: An efficient filtering technique combining domain partition and arc consistency[END_REF].

Proposition 1. Any S φ

∆ -inconsistent value is globally inconsistent. Proof. If (x, a) is an S φ ∆ -inconsistent value, then we know that there exists a decision x ∈ D x in ∆(x) such that a ∈ D x and (x, a) / ∈ φ(P | x∈Dx ). We deduce that x ∈ D x ∧ x = a cannot lead to a solution because φ is nogood-identifying. This simplifies into x = a being a nogood because a ∈ D x .

⊓ ⊔ SAC is equivalent to S GAC ∆ =

(because no value belongs to ⊥), and BoundSAC1 is equivalent to S GAC ∆ bnd . Note also that GAC is equivalent to S GAC ∆ id

. As a simple illustration of S φ ∆ , let us consider the five binary CNs depicted in Figure 1; each vertex denotes a value, each edge denotes an allowed tuple and each dotted vertex (resp., edge) means that the value (resp., tuple) is removed (resp., no more relevant). P 1 , P 2 , P 3 and P 4 are obtained from P by removing values that are S AC ∆ -inconsistent when ∆ is set to ∆ id , ∆ P2 , ∆ bnd and ∆ = , respectively. For example, for ∆ P2 , we find that (y, c) / ∈ AC (P | y∈{c,d} ). Note that the CN P 4 is also obtained when setting ∆ to ∆ = . In [START_REF] Bennaceur | Partition-k-AC: An efficient filtering technique combining domain partition and arc consistency[END_REF], it is also shown that inferences regarding values may be obtained by considering the result of several decision-based checks. This is generalized below. The idea is that a value (x, a) of P can be safely removed when there exist a variable y and a cover Γ ⊆ ∆(y) of dom(y) such that every decision-based check, performed from a decision in Γ , eliminates (x, a).

Definition 2 (Consistency E φ ∆ ). A value (x, a) of a CN P is E φ ∆ -consistent w.r.t. a variable y = x of P iff for every cover Γ of dom(y) such that Γ ⊆ ∆(y), there exists a decision y ∈ D y in Γ such that (x, a) ∈ φ(P | y∈Dy ). (x, a) is E φ ∆ -consistent iff (x, a) is E φ ∆ -consistent w.r.t. every variable y = x of P .
Proposition 2. Any E φ ∆ -inconsistent value is globally inconsistent. Proof. If (x, a) is an E φ ∆ -inconsistent value, then we know that there exists a variable y = x of P and a set Γ ⊆ ∆(y) such that (i) dom P (y) = ∪ (y∈Dy)∈Γ D y and (ii) every decision y ∈ D y in Γ entails (x, a) / ∈ φ(P | y∈Dy ). As Γ is a cover of dom(y), we infer that sols(P ) = ∪ (y∈Dy)∈Γ sols(P | y∈Dy ). Because φ preserves solutions, we have sols(P ) = ∪ (y∈Dy)∈Γ sols(φ(P | y∈Dy )). For every y ∈ D y in Γ , we know that (x, a) / ∈ φ(P | y∈Dy ). We deduce that (x, a) cannot be involved in any solution.

⊓ ⊔

As an illustration, let us consider the CN of Figure 1(a) and ∆(x) = {x ∈ {a, c}, x ∈ {b, d}}. We can show that (z, a) is E GAC

Classes Related to Nogoods of Size 2

Decision-based consistencies introduced above are clearly domain-filtering: they allow us to identify inconsistent values. However, decision-based consistencies are also naturally orientated towards identifying nogoods of size 2. NG2 (P ) φ ∆ denotes the set of nogoods of size 2 that can be directly derived from checks on P based on the consistency φ and the decision mapping ∆. From this set, together with a decision x ∈ D x , we obtain a set ND1 (P, x ∈ D x ) φ ∆ of negative decisions that can be used to make further inferences.

Proposition 3. Any B φ

∆ -inconsistent value is globally inconsistent. Proof. The proof is similar to that of Proposition 1. The only difference is that the network P is made smaller by removing some additional values by means of negative decisions. However, in the context of a decision x ∈ D x taken on P , the inferred negative decisions correspond to inconsistent values because they are derived from nogoods of size 2 (showing that elements of NG2 (P ) φ ∆ are nogoods is immediate).

⊓ ⊔

As an illustration of B φ ∆ , let us consider the binary CN P in Figure 2 Note that BiSAC [START_REF] Bessiere | Theoretical analysis of singleton arc consistency and its extensions[END_REF] is equivalent to B GAC ∆ =

. On the other hand, there is a 2-order consistency that can be naturally defined as follows.

Proposition 4. Any D φ

∆ -inconsistent instantiation is globally inconsistent.

Proof. D φ ∆ -inconsistent instantiations are exactly those in NG2 (P ) φ ∆ , which are nogoods.

⊓ ⊔ Note that DC [START_REF] Lecoutre | Second-order consistencies[END_REF] is equivalent to

D GAC ∆ =
, and recall that DC is equivalent to PC (Path Consistency) for binary CNs. D φ ∆ (being 2-order) is obviously incomparable with previously introduced domain-filtering consistencies. However, a natural practical approach is to benefit from decision-based checks to record both S φ ∆ -inconsistent values and D φ ∆ -inconsistent instantiations. This corresponds to the combined consistency S φ ∆ +D φ ∆ . As an illustration of D φ ∆ , let us consider again Figure 2. For φ = AC and ∆ = ∆ P2 = {x ∈ {a, b}, x = c, y ∈ {a, b}, y = c, z = a, z = b}, we have that P is S φ ∆ -consistent, not B φ ∆ -consistent and not D φ ∆ -consistent. Enforcing S φ ∆ + D φ ∆ on P yields the CN P ′ , which is also the strong DC-closure (here, AC+PC-closure) of P .

In this section, we study the relationships between the different classes of consistencies (as well as some of their combinations), and discuss refinements and well-behavedness of consistencies.

Relationships between Consistencies

From Definitions 1 and 4, it is immediate that any

S φ ∆ -inconsistent value is necessarily B φ ∆ -inconsistent. Proposition 5. B φ ∆ S φ ∆ .
In order to relate B φ

∆ with E φ ∆ , we need to consider covering sets of decisions.

Proposition 6. If ∆ is covering, B φ ∆ E φ ∆ . Proof. We show that every E φ ∆ -inconsistent value in a CN P is necessarily B φ ∆ - inconsistent. Assume that (x, a) is a E φ ∆ -inconsistent value.
It means that there exists a variable y = x of P and Γ ⊆ ∆(y) such that dom P (y) = ∪ (y∈Dy)∈Γ D y and every decision y ∈ D y in Γ is such that (x, a) / ∈ φ(P | y∈Dy ). We deduce that for every value b ∈ dom P (y), we have {(x, a), (y, b)} in NG2 (P ) φ ∆ . On the other hand, we know that there exists a decision x ∈ D x in ∆ such that a ∈ D x (since ∆ is covering). Hence, ND1 (P, x ∈ D x ) φ ∆ contains a negative decision y = b for each value in dom P (y). It follows that φ

(P | {x∈Dx}∪ND1 (P,x∈Dx) φ ∆ ) = ⊥, and (x, a) is B φ ∆ -inconsistent. ⊓ ⊔
As a corollary, we have B φ ∆ S φ ∆ + E φ ∆ when ∆ is covering. Note that there exist consistencies φ and decision mappings ∆ such that B φ ∆ is strictly stronger (⊲) than S φ

∆ and E φ ∆ (and also S φ ∆ +E φ ∆ ). For example, when φ = AC and ∆ = ∆ = , we have B φ ∆ = BiSAC, S φ ∆ = SAC and S φ ∆ + E φ ∆ = 1-AC, and we know that BiSAC ⊲ 1-AC [START_REF] Bessiere | Theoretical analysis of singleton arc consistency and its extensions[END_REF], and 1-AC ⊲ SAC [START_REF] Bennaceur | Partition-k-AC: An efficient filtering technique combining domain partition and arc consistency[END_REF].

Because D φ ∆ captures all 2-sized nogoods while S φ ∆ can eliminate inconsistent values, it follows that the joint use of these two consistencies is stronger than

B φ ∆ . Proposition 7. S φ ∆ +D φ ∆ B φ ∆ . Proof. Let P be a CN that is S φ ∆ +D φ ∆ -consistent. As P is S φ ∆ -consistent, for every decision x ∈ D x in ∆ and every a ∈ D x , we have (x, a) ∈ φ(P | x∈Dx ). But φ(P | x∈Dx ) = φ(P | {x∈Dx}∪ND1 (P,x∈Dx) φ ∆ ) since P being D φ ∆ -consistent entails NG2 (P ) φ ∆ = ∅ and ND1 (P, x ∈ D x ) φ ∆ = ∅. We deduce that P is B φ ∆ -consistent. ⊓ ⊔
One may expect that S φ ∆ φ. However, to guarantee this, we need both φ to be domain-filtering and ∆ to be covering, For example, S AC ∆ AC does not hold if for every dom x ⊆ dom init (x), we have ∆(x, dom x ) = ∅: it suffices to build a CN P with a value (x, a) being arc-inconsistent. Proof. Assume that (x, a) is a φ-inconsistent value of a CN P . This means that (x, a) / ∈ φ(P ). As ∆ is covering, there exists a decision x ∈ D x in ∆ with a ∈ D x . We know that P | x∈Dx P . By monotonicity of φ, φ(P | x∈Dx ) φ(P ). Since (x, a) / ∈ φ(P ), we deduce that (x, a) / ∈ φ(P | x∈Dx ). So, (x, a) is S φ ∆ -inconsistent, and S φ ∆ is stronger than φ.

⊓ ⊔

Figure 3 shows the relationships between the different classes of consistencies introduced so far. There are many ways to instantiate these classes because the choice of ∆ and φ is left open. If we consider binary CNs, and choose φ = AC and ∆ = ∆ = , we obtain known consistencies. We directly benefit from the relationships of Figure 3, and have just to prove strictness when it holds. Figure 4 shows this where an arrow denotes now ⊲ (instead of ). An extreme instantiation case is when ∆ = ∆ id and φ is domain-filtering. In this case, all consistencies collapse: we have

S φ ∆ id = E φ ∆ id = B φ ∆ id = D φ ∆ id = φ.
This means that our framework of decision-based consistencies is general enough to encompass all classical local consistencies. Although this is appealing for theoretical reasons (e.g., see Proposition 11 later), the main objective of decision-based consistencies remains to learn relevant nogoods from nontrivial decision-based checks.

S φ ∆ B φ ∆ S φ ∆ +D φ ∆ D φ ∆ S φ ∆ +E φ ∆ E φ ∆ φ Fig. 3.
Summary of the relationships between (classes of) consistencies. An arrow from ϕ to ψ means that ϕ ψ. A dashed (resp., dotted) arrow means that the relationship is guaranteed provided that ∆ is covering (resp., ∆ is covering and φ is domain-filtering).

SAC sDC DC

BiSAC 1 -AC E AC ∆ =
BoundSAC AC Fig. 4. Relationships between consistencies when φ = AC and ∆ = ∆ = (except for BoundSAC which is derived from ∆ bnd ). An arrow from ϕ to ψ means that ϕ ⊲ ψ.

Refinements

Now, we show that two consistencies of the same class can be naturally compared when a refinement connection exists between their decision mappings. Definition 6. A decision mapping ∆ ′ is a refinement of a decision mapping ∆ iff for each decision x ∈ D x in ∆ there exists a subset Γ ⊆ ∆ ′ (x) that is a cover of D x .

For example, {x ∈ {a, b}, x = c} is a refinement of {x ∈ {a, b, c}}, and {x ∈ {a, b}, x = c, y = a, y = b, y = c} is a refinement of {x ∈ {a, b, c}, y ∈ {a, b}, y ∈ {b, c}}. Unsurprisingly, using refined sets of decisions improves inference capability as shown by the following proposition. Proposition 9. If ∆ and ∆ ′ are two decision mappings such that ∆ ′ is a refinement of ∆, then X φ ∆ ′

X φ

∆ where X ∈ {S, E, B, D}. Proof. Due to lack of space, we only show that S φ ∆ ′ S φ ∆ . Assume that (x, a) is an S φ ∆ -inconsistent value of a CN P . This means that there exists a decision x ∈ D x in ∆(x) such that a ∈ D x and (x, a) / ∈ φ(P | x∈Dx ). We know, by hypothesis, that there exists a subset ). We deduce that there exists a decision

Γ ⊆ ∆ ′ (x) such that D x = ∪ (x∈D ′ x )∈Γ D ′ x . Hence, there exists (at least) a decision x ∈ D ′ x in Γ such that a ∈ D ′ x and D ′ x ⊆ D x . As D ′ x ⊆ D x ,
x ∈ D ′ x in ∆ ′ (x) such that a ∈ D ′ x and (x, a) / ∈ φ(P | x∈D ′′ x ). Then (x, a) is S φ ∆ ′ -inconsistent. We conclude that S φ ∆ ′ S φ ∆ . ⊓ ⊔
As a corollary, for any decision mapping ∆, we have:

X φ ∆ = X φ ∆ X φ ∆ id
where X ∈ {S, E, B, D}. In particular, if φ = GAC, we have

SAC = S GAC ∆ = S GAC ∆ S GAC ∆ id = GAC.

Because, consistencies S φ

∆ identify inconsistent values on the basis of a single decision, we obtain the two following results. In the spirit of our set view of decision mappings, for any two decision mappings ∆ 1 and ∆ 2 , ∆ 1 ∪ ∆ 2 is the decision mapping such that for every variable x and every dom x ⊆ dom init (x), (∆ 1 ∪ ∆ 2 )(x, dom x ) = ∆ 1 (x, dom x ) + ∆ 2 (x, dom x ).

Proposition 10. Let ∆ 1 and ∆ 2 be two decision mappings. We have S φ

∆ 1 + S φ ∆ 2 = S φ ∆ 1 ∪∆ 2 .
Proof. Let P be a CN and (x, a) be a value of

P . (x, a) is S φ ∆ 1 ∪∆ 2 -inconsistent ⇔ there exists a decision x ∈ D x in ∆ 1 ∪ ∆ 2 such that (x, a) / ∈ φ(P | x∈Dx ) ⇔ (x, a) is S φ ∆ 1 -inconsistent or (x, a) is S φ ∆ 2 -inconsistent ⇔ (x, a) is S φ ∆ 1 +S φ ∆ 2 -inconsistent. ⊓ ⊔ S φ
E = {S φ ∆ ∈ S φ : S φ ∆ S φ ∆ 1 and S φ ∆ S φ ∆ 2 }. Note that E = ∅ since S φ ∆ id ∈ E. Next, let us define S φ ∆ E such that ∆ E = S φ ∆ i ∈E ∆ i . For every S φ ∆ i ∈ E, ∆ E is a refinement ∆ i ,
i such that S φ ∆ i ∈ E and x ∈ D x is in ∆ i . By definition of E, we know that S φ ∆ i S φ ∆ 1 . Consequently, (x, a) is S φ ∆ i -consistent and (x, a) ∈ φ(P | x∈Dx ). This is a contradiction, so S φ ∆ S φ ∆ 1 . Similarly, we have S φ ∆ S φ ∆ 2 . Then S φ ∆ is the greatest lower bound of S φ ∆ 1 and S φ ∆ 2 .
⊓ ⊔

Well-behavedness

Finally, we are interested in well-behavedness of consistencies. Actually, in the general case, the consistencies S φ ∆ , E φ ∆ , B φ ∆ and D φ ∆ are not necessarily wellbehaved for (P, ). Consider as an illustration three CNs P , P 1 and P 2 which differ only by the domain of the variable x: dom P (x) = {a, b, c, d}, dom P1 (x) = {a, b, c} and dom P2 (x) = {d}. Now, consider a decision mapping ∆ defined for the variable x and the domains {a, b, c, d}, {a, b, c} and {d} by: ∆(x, {a, b, c, d}) = {x ∈ {a}}, ∆(x, {a, b, c}) = {x ∈ {a, b, c}} and ∆(x, {d}) = {x ∈ {d}}. Despite the fact that dom P (x) = dom P1 (x) ∪ dom P2 (x), one can see that the value (x, a) could be S φ ∆ -consistent in P 1 and P 2 , whereas S φ ∆ -inconsistent in P . With such a ∆, S φ ∆ is not guaranteed to be well-behaved. Nevertheless, there exist decision mappings for which consistencies are guaranteed to be well-behaved, at least those of the class S φ ∆ . Informally, a relevant decision mapping is a decision mapping that keeps its precision (in terms of decisions) when domains are restricted. Definition 7. A decision mapping ∆ is said to be relevant if and only if for any variable x, any two sets of values dom x and dom ′

x such that dom ′ x dom x ⊆ dom init (x) and any decision x ∈ D x in ∆(x, dom x ), we have:

D x ∩ dom ′ x = ∅ ⇒ ∃Γ ⊆ ∆(x, dom ′ x ) | D x ∩ dom ′ x = ∪ (x∈D ′ x )∈Γ D ′ x .
We can notice that ∆ id , ∆ = , ∆ = , ∆ bnd are relevant decision mappings. For our proposition, we need some additional definitions. A CN P ′ is a sub-CN of a CN P if P ′ can be obtained from P by simply removing certain values. If P 1 and P 2 are two CNs that only differ by the domains of their variables, then P = P 1 ∪ P 2 is the CN such that P 1 and P 2 are sub-CNs of P and for every variable x, dom P (x) = dom P1 (x) ∪ dom P2 (x).

Proposition 12. Let ∆ be a relevant decision mapping and let P , P 1 , and P 2 be three CNs such that P = P 1 ∪ P 2 . If P 1 and P 2 are S φ ∆ -consistent then P is S φ ∆ -consistent.

Proof. Let (x, a) be a value of P = P 1 ∪ P 2 . Let us show that this value is S φ ∆consistent. Consider a membership decision x ∈ D x in ∆(x, dom P (x)) such that a ∈ D x . We have to show that (x, a) ∈ φ(P | x∈Dx ). We know that dom P (x) = dom P1 (x) ∪ dom P2 (x). Hence, a ∈ dom P1 (x) or x ∈ dom P2 (x). Assume that a ∈ dom P1 (x) (the case a ∈ dom P2 (x) can be handled in a similar way). Since ∆ is a relevant decision mapping, there exists Γ ⊆ ∆(x, dom P1 (x)) such that D x ∩ dom P1 (x) = ∪ (x∈D ′

x )∈Γ D ′ x . It follows that there exists a decision x ∈ D 1

x in ∆(x, dom P1 (x)) such that a ∈ D 1 x and D 1 x ⊆ D x . From the fact that P 1 is S φ ∆ -consistent we know that (x, a) ∈ φ(P 1 | x∈D 1

x ). Since a ∈ D 1 x , D 1 x ⊆ D x and P 1 is a sub-CN of P we can assert that (x, a) ∈ φ(P | x∈Dx ). We conclude that (x, a) is a S φ ∆ -consistent value of P . ⊓ ⊔ Corollary 1. If ∆ is a relevant decision mapping then S φ ∆ is well-behaved.

Indeed, to obtain the closure of a CN P , it suffices to take the union of all sub-CNs of P which are S φ ∆ -consistent. Hence, the consistency S φ ∆ for which ∆ is a relevant decision mapping is well-behaved for (P, ).

Conclusion

In this paper, our aim was to give a precise picture of decision-based consistencies by developing a hierarchy of general classes. This general framework offers the user a vast range of new consistencies. Several issues have now to be addressed. First, me must determine the conditions under which overlapping between decisions may be beneficial. Overlapping allows us to cover domains while considering weak decisions (e.g., decisions in ∆ = ) that are quick to propagate, and might also be useful to tractability procedures (e.g., in situations where only some decisions lead to known tractable networks). Second, we must seek to elaborate dynamic procedures (heuristics) so as automatically select the right decision-based consistency (set of membership decisions) at each step of a backtrack search as in [START_REF] Stergiou | Heuristics for dynamically adapting propagation[END_REF]; many new combinations are permitted. Finally, bound consistencies and especially singleton checks on bounds may be revisited by checking several values at once (using intervals at bounds with the mechanism of detecting X φ ∆ -inconsistent values), so as to speed up the inference process in shaving procedures. These are some of the main perspectives.

  denoted by vars(I) and each 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 ). I is valid on P iff ∀(x, a) ∈ I, a ∈ dom(x). I covers a constraint c iff scp(c) ⊆ vars(I), and I satisfies a constraint c with scp(c) = {x 1 , . . . , x r } iff (i) I covers c and (ii) the tuple (I[x 1 ], . . . , I[x r ]) ∈ rel(c

Fig. 1 .

 1 Fig. 1. Illustration of S GAC ∆ .

∆-

  inconsistent because (z, a) / ∈ AC(P | x∈{a,c} ) and (z, a) / ∈ AC(P | x∈{b,d} ). The consistency P-k-AC, introduced in [2], corresponds to S φ ∆ +E φ ∆ where φ = AC and ∆ necessarily corresponds to a partition of each domain into pieces of size at most k.

Definition 3 .

 3 Let P be a CN and x ∈ D x be a membership decision in ∆(x). -NG2 (P ) φ x∈Dx denotes the set of locally consistent instantiations {(x, a), (y, b)} on P such that a ∈ D x and (y, b) / ∈ φ(P | x∈Dx ). -NG2 (P ) φ ∆ denotes the set ∪ δ∈∆ NG2 (P ) φ δ . -ND1 (P, x ∈ D x ) φ ∆ denotes the set of negative decisions y = b such that every value a ∈ D x is such that {(x, a), (y, b)} ∈ P or {(x, a), (y, b)} ∈ NG2 (P ) φ ∆\{x∈Dx } . From ND1 sets, we can define a new class B φ ∆ of consistencies. Definition 4 (Consistency B φ ∆ ). A value (x, a) of a CN P is B φ ∆ -consistent iff for every membership decision x ∈ D x in ∆(x) such that a ∈ D x , we have (x, a) ∈ φ(P | {x∈Dx}∪ND1 (P,x∈Dx) φ ∆ ).

Fig. 2 .

 2 Fig. 2. Illustration of B GAC∆

Definition 5 (

 5 Consistency D φ ∆ ). A locally consistent instantiation {(x, a), (y, b)} on a CN P is D φ ∆ -consistent iff for every membership decision x ∈ D x in ∆(x) such that a ∈ D x , (y, b) ∈ φ(P | x∈Dx ) and for every membership decision y ∈ D y in ∆(y) such that b ∈ D y , (x, a) ∈ φ(P | y∈Dy ).

Proposition 8 .

 8 If φ is domain-filtering and ∆ is covering, S φ ∆ φ.

  we have P | x∈D ′ x P | x∈Dx , and by monotonicity of φ, φ(P | x∈D ′ x ) φ(P | x∈Dx ). Consequently, (x, a) / ∈ φ(P | x∈Dx ) implies (x, a) / ∈ φ(P | x∈D ′ x

  denotes the set of equivalence classes modulo ≈ of the consistencies S φ ∆ that can be built from φ and all possible decision mappings ∆. It forms a complete lattice, in a similar way to what has been shown for qualitative constraint networks[START_REF] Condotta | A class of df-consistencies for qualitative constraint networks[END_REF].Proposition 11. (S φ , ) is a complete lattice with S φ ∆ = as greatest element and S φ ∆ id as least element.Proof. Let S φ ∆ 1 and S φ ∆ 2 be two consistencies in S φ . (Existence of binary joins) From Proposition 10, we can infer that S φ ∆ 1 ∪∆ 2 is the least upper bound of S φ ∆ 1 and S φ ∆ 2 . (Existence of binary meets) Let us define the set E as

  and so, from Proposition 9, we know that S φ ∆ E is an upper bound of E. We now prove by contradiction that S φ Suppose that there is a value (x, a) of a CN P that is S φ ∆ E -inconsistent and S φ ∆ 1 -consistent. This means that there exists a decision x ∈ D x in ∆(x) such that (x, a) / ∈ φ(P | x∈Dx ). From construction of ∆, we know that there exists a decision mapping ∆

	∆ E	S φ ∆ 1 .

Another related consistency is Existential SAC[START_REF] Lecoutre | Maintaining singleton arc consistency[END_REF], which guarantees that some value in the domain of each variable is SAC-consistent. However, there is no guarantee about the network obtained after checking Existential SAC due to the nondeterministic nature of this consistency. Existential SAC is not an element of S φ ∆ .

Acknowledgments

We would like to thank the anonymous reviewers for their valuable comments and suggestions. This work was supported by OSEO (project ISI PAJERO).


Gilles Audemard
email: audemard@cril.fr

Benoît Hoessen
email: hoessen@cril.fr

Saïd Jabbour
email: jabbour@cril.fr

Jean-Marie Lagniez
email: lagniez@cril.fr

Cédric Piette
email: piette@cril.fr

PeneLoPe, a parallel clause-freezer solver

This paper provides a short system description of our new portfolio-based solver called PeneLoPe, based on ManySat. Particularly, this solver focuses on collaboration between threads, providing different policies for exporting and importing learnt clauses between CDCL searches. Moreover, different restart strategies are also available, together with a deterministic mode.

I. OVERVIEW

PeneLoPe is a portfolio parallel SAT solver that uses the most effective techniques proposed in the sequential framework: unit propagation, lazy data structures, activity-based heuristics, progress saving for polarities, clause learning, etc. As for most of existing solvers, a first preprocessing step is achieved. For this step -which is typically sequential-we have chosen to make use of SatElite [START_REF] Eén | Effective preprocessing in SAT through variable and clause elimination[END_REF].

In addition, PeneLoPe includes a recent technique for its learnt clause database management. Roughly, this new approach follows this schema: each learnt clause c is periodically evaluated with a so-called psm measure [START_REF] Audemard | On freezeing and reactivating learnt clauses[END_REF], which is equal to the size of the set-theoretical intersection of the current interpretation and c. Clauses that exhibit a low psm are considered relevant. Indeed, the lower is a psm value, the more likely the related clause is about to unit-propagate some literal, or to be falsified. On the opposite, a clause with a large psm value has a lot of chance to be satisfied by many literals, making it irrelevant for the search in progress.

Thus, only clauses that exhibit a low psm are selected and currently used by the solver, the other clauses being frozen. When a clause is frozen, it is removed from the list of the watched literals of the solver, in order to avoid the computational over-cost of maintaining the data structure of the solver for this useless clause. Nevertheless, a frozen clause is not erased but it is kept in memory, since this clause may be useful in the next future of the search. As the current interpretation evolves, the set of learnt clauses actually used by the solver evolves, too. In this respect, the psm value is computed periodically, and sets of clauses are frozen or unfrozen with respect to their freshly computed new value.

Let P k be a sequence where P 0 = 500 and P i+1 = P i + 500 + 100 × i. A function "updateDB" is called each time the number of conflict reaches P i conflicts (where i ∈ [0..∞]). This function computes new psm values for every learnt clauses (frozen or activated). A clause that has a psm value less than a given limit l is activated in the next part of the search. If its psm does not hold this condition, then it is frozen. Moreover, a clause that is not activated after k (equal to 7 by default) time steps is deleted. Similarly, a clause remaining active more than k steps without participating to the search is also permanently deleted (see [START_REF] Audemard | On freezeing and reactivating learnt clauses[END_REF] for more details).

Besides the psm technique, PeneLoPe also makes use of the lbd value defined in [START_REF] Audemard | Predicting learnt clauses quality in modern SAT solvers[END_REF]. lbd is used to estimate the quality of a learnt clause. This new measure is based on the number of different decision levels appearing in a learnt clause and is computed when the clause is generated. Extensive experiments demonstrates that clauses with small lbd values are used more often than those with higher lbd ones. Note also that lbd of clauses can be recomputed when they are used for unit propagations, and updated if it becomes smaller. This update process is important to get many good clauses.

Given these recently defined heuristic values, we present in the next Section several strategies implemented in PeneLoPe.

II. DETAILLED FEATURES

PeneLoPe proposes a certain number of strategies regarding importation and exportation of learnt clauses, restarts, and the possibility of activating a deterministic mode.

Importing clause policy: When a clause is imported, we can consider different cases, depending on the moment the clause is attached for participating to the search.

• no-freeze: each imported clause is actually stored with the current learnt database of the thread, and will be evaluated (and possibly frozen) during the next call to updateDB. • freeze-all: each imported clause is frozen by default, and is only used later by the solver if it is evaluated relevant w.r.t. unfreezing conditions. • freeze: each imported clause is evaluated as it would have been if locally generated. If the clause is considered relevant, it is added to the learnt clauses, otherwise it is frozen. Exporting clause policy: Since PeneLoPe can freeze clauses, each thread can import more clauses than it would with a classical management of clauses, where all of them are attached. Then, we propose different strategies, more or less restrictive, to select which clauses have to be shared:

• unlimited: any generated clause is exported towards the different threads. • size limit: only clauses whose size is less than a given value are exported [START_REF] Hamadi | Control-based clause sharing in parallel SAT solving[END_REF]. • lbd limit: a given clause c is exported to other threads if its lbd value lbd(c) is less than a given limit value d (8 by default). Let us also note that the lbd value can vary over time, since it is computed with respect to the current interpretation. Therefore, as soon as lbd(c) is less than d, the clause is exported. Restarts policy: Beside exchange policies, we define two restart strategies.

• Luby: Let l i be the i th term of the Luby serie. The i th restart is achieved after l i × α conflicts (α is set to 100 by default).

• LBD [START_REF] Audemard | Predicting learnt clauses quality in modern SAT solvers[END_REF]: Let LBD g be the average value of the LBD of each learnt clause since the beginning. Let LBD 100 be the same value computed only for the last 100 generated learnt clause. With this policy, a restart is achieved as soon as LBD 100 ×α > LBD g (α is set to 0.7 by default).

In addition, the VSIDS score of variables that are unitpropagated thank for a learnt clause whose lbd is equal to 2 are increased, as detailled in [START_REF] Audemard | Predicting learnt clauses quality in modern SAT solvers[END_REF]. Furthermore, we have implemented in PeneLoPe a deterministic mode which ensures full reproducibility of the results for both runtime and reported solutions (model or refutation proof). Large experiments show that such mecanism does not affect significantly the solving process of portfolio solvers [START_REF] Hamadi | Deterministic parallel DPLL[END_REF]. Quite obviously, this mode can also be unactivated in PeneLoPe.

III. FINE TUNING PARAMETERS OF PE N ELOPE

PeneLoPe is designed to be fine-tuned in an easy way, namely without having to modify its source code. To this end, a configuration file (called configuration.ini, an example is provided in Figure 1) is proposed to describe the default behavior of each thread. This file actually contains numerous parameters that can be modified by the user before running the solver. For instance, besides export, import and restart strategies, one can choose the number of threads that the solver uses, the α factor if the Luby techniques is activated for the restart strategy, etc. Each policy and/or value can obviouly differ from one thread to the other, in order to ensure diversification.

1 n c o r e s = 8 2 d 3 ; 4 ; 5 ;[Fig. 1 .

 123451 Fig. 1. Configuration.ini file

ACKNOWLEDGMENT

PeneLoPe has been partially developped thank to the financial support of CNRS and OSEO, under the ISI project "Pajero".