Long Guo
email: guo@cril.fr

Youssef Hamadi
email: youssefh@microsoft.com

Lakhdar Sais
email: sais@cril.fr

Diversification and Intensification in Parallel SAT Solving

Keywords: Satisfiability, SAT and CSP, Search

In this paper, we explore the two well-known principles of diversification and intensification in portfolio-based parallel SAT solving. These dual concepts play an important role in several search algorithms including local search, and appear to be a key point in modern parallel SAT solvers. To study their tradeoff, we define two roles for the computational units. Some of them classified as Masters perform an original search strategy, ensuring diversification. The remaining units, classified as Slaves are there to intensify their master's strategy. Several important questions have to be answered. The first one is what information should be given to a slave in order to intensify a given search effort? The second one is, how often, a subordinated unit has to receive such information? Finally, the question of finding the number of subordinated units along their connections with the search efforts has to be answered. Our results lead to an original intensification strategy which outperforms the best parallel SAT solver, and solves some open SAT instances.

Introduction

In addition to the traditional hardware and software verification fields, SAT solvers are gaining popularity in new domains. For instance they are also used for general theorem proving and computational biology. This widespread adoption is the result of the efficiency gains made during the last decade [START_REF]Handbook of Satisfiability[END_REF]. Indeed, industrial instances with hundred of thousand of variables and millions of clauses are now solved within a few minutes. This impressive progress can be related to both the algorithmic improvements and to the ability of SAT solvers to exploit the hidden structures 1 of such instances. However, new applications are always more challenging with instances of increasing size and complexity, while the gains traditionally given by low level algorithmic adjustments are now stalling. As a result, a large number of industrial instances from the last competitions remain challenging for all the available SAT solvers. Fortunately, the previous comes at a time where the generalization of multicore hardware gives parallel processing capabilities to standard PCs. While in general it is important for existing applications to exploit these new hardwares, for SAT solvers, this becomes crucial.

Many parallel SAT solvers have been previously proposed. Most of them are based on the divide-and-conquer principle. They either divide the search space using for example guiding-paths or the formula itself using decomposition techniques. The main problem behind these approaches rises in the difficulty to get workload balanced between the different processing units. Portfolio-based parallel SAT solving has been recently introduced [START_REF] Hamadi | ManySAT: a parallel SAT solver[END_REF]. It avoids the previous problem by letting several DPLL engines compete and cooperate to be the first to solve a given instance. Each solver works on the original formula, and search spaces are not split or decomposed anymore. To be efficient, the portfolio has to use diversified search engines. This maximizes the chance of having one of them solving the problem. However, when clause sharing is added, diversification has to be restricted in order to maximize the impact of a foreign clause whose relevance is more important in a similar or related search effort.

Therefore, a challenging question is to maintain a good and relevant "distance" between the parts of the search space explored by the different search efforts which is equivalent to the finding of a good diversification and intensification tradeoff. This question heavily depends on the problem instance. On hard ones it might be more convenient to direct the search towards building the same and common proof (intensification), whereas on easy ones diversifying it might be the way towards finding a short proof.

Taking this in mind, we propose to study the diversification/intensification tradeoff in a parallel SAT portfolio. We define two roles for the computational units. Some of them classified as Masters perform an original search strategy, ensuring diversification. The remaining ones, classified as Slaves are there to intensify their master's strategy. Doing so, several important questions have to be answered. The first one is what information should be given to a unit in order to intensify a given search effort? The second one is, how often, a subordinated unit has to receive such information? Finally, the question of finding the number of subordinated units along their connections with original search efforts has to be answered.

In the following, Section two describes the internals of modern SAT solvers, and the architecture of a portfolio-based parallel SAT engine. Section three studies the best way to intensify a given search strategy. Section four, considers the different diversification/intensification tradeoffs in a portfolio. Section five, presents our experimental results. Finally, before the general conclusion, section six presents the related works.

Technical Background

In this section, we first introduce the most salient computational features of modern SAT solvers. Then, we describe a typical portfolio based parallel SAT solver.

Modern SAT Solvers

Modern SAT solvers [START_REF] Moskewicz | Chaff: Engineering an efficient SAT solver[END_REF][START_REF] Eén | An extensible sat-solver[END_REF], are based on classical DPLL search procedure [START_REF] Davis | A machine program for theorem-proving[END_REF] combined with (i) restart policies [START_REF] Gomes | Boosting combinatorial search through randomization[END_REF][START_REF] Kautz | Dynamic restart policies[END_REF], (ii) activity-based variable selection heuristics (VSIDS-like) [START_REF] Moskewicz | Chaff: Engineering an efficient SAT solver[END_REF], and (iii) clause learning [START_REF] Marques-Silva | GRASP -A New Search Algorithm for Satisfiability[END_REF]. The interaction of these three components being performed through efficient data structures (e.g., Watched literals [START_REF] Moskewicz | Chaff: Engineering an efficient SAT solver[END_REF]).

Modern SAT solvers are especially efficient with "structured" SAT instances coming from industrial applications. On these problems, Selman et al. [START_REF] Gomes | Heavy-tail phenomena in satisfiability and constraint satisfaction[END_REF] have identified a heavy tailed phenomenon, i.e., different variable orderings often lead to dramatic differences in solving time. This explains the introduction of restart policies in modern SAT solvers, which attempt to discover a good variable ordering. VSIDS and other variants of activity-based heuristics [START_REF] Brisoux | Improving backtrack search for SAT by means of redundancy[END_REF], on the other hand, were introduced to avoid thrashing and to focus the search: when dealing with instances of large size, these heuristics direct the search to the most constrained parts of the formula. Restarts and VSIDS play complementary roles since the first component reorders assumptions and compacts the assumptions stack while the second allows for more intensification. Conflict Driven Clause Learning (CDCL) is the third component, leading to non-chronological backtracking. In CDCL a central data-structure is the implication graph, which records the partial assignment under construction made of the successive decision literals (chosen variable with either positive or negative polarity) with their propagations [START_REF] Marques-Silva | GRASP -A New Search Algorithm for Satisfiability[END_REF]. Each time a conflict is encountered (say at level i) a conflict clause or nogood is learnt thanks to a bottom up traversal of the implication graph. Such a traversal can be seen as a resolution derivation starting from the two implications of the conflicting variable. The next resolvent is generated, from the previous one and another clause from the implication graph. Such linear resolution derivation stops when the current resolvent (α ∨ a), contains only one literal a from the current conflict level, called an asserting literal. The node in the graph labeled with ¬a is called the first Unique Implication Point (first-UIP). This traversal or resolution process is also used to update the activity of related variables, allowing VSIDS to always select the most active variable as the new decision point. The learnt conflict clause (α ∨ a), called asserting clause, is added to the learnt data base and the algorithm backtracks non chronologically to level j < i.

Modern SAT solvers can now handle propositional satisfiability problems with hundreds of thousands of variables or more. However, it is now recognized (see the recent SAT competitions) that the performances of the modern SAT solvers evolve in a marginal way. More precisely, on the industrial benchmarks category usually proposed to the annual SAT Races and/or SAT Competitions, many instances remain open (not solved by any solver within a reasonable amount of time). Consequently, new approaches are clearly needed to solve these challenging industrial problems.

ManySAT: a Parallel SAT Solver

ManySAT is a DPLL-engine which includes all the classical features like two-watchedliteral, unit propagation, activity-based decision heuristics, lemma deletion strategies, and clause learning. In addition to the classical first-UIP scheme [START_REF] Zhang | Efficient conflict driven learning in boolean satisfiability solver[END_REF], it incorporates a new technique which extends the implication graph used during conflict-analysis to exploit the satisfied clauses of a formula [START_REF] Audemard | A generalized framework for conflict analysis[END_REF]. Unlike others parallel SAT solvers, ManySAT does not implement a divide-and-conquer strategy based on some dynamic partitioning of the search space. At contrary, it uses a portfolio philosophy which lets several sequential DPLLs compete and cooperate to be the first to solve the common instance. These DPLLs are differentiated in many ways. They use different and complementary restart strategies, VSIDS, polarity heuristics, and learning schemes. Additionally, all the DPLLs are exchanging learnt clauses up to some size limit.

This solver finished first in the parallel tracks of the 2008 and 2009 SAT Race and Competition (industrial categories).

Towards a Good Intensification Strategy

In this section, we first determine the relevant knowledge to be passed from a Master to a Slave in order to intensify the search. Secondly, we address the frequency of such directed intensification.

To this end, we consider a simple system with two computing units, respectively a Master (M) and a Slave (S) (see Figure 1). The role of the Master is to invoke the Slave for search intensification (dotted blue arrow in the Figure 1). By intensification we mean that the slave would explore "differently" around the search space explored by the Master. Consequently, the clauses learnt by the Master and the Slave are relevant to each other and shared in both direction (plain line in the Figure 1). To explore differently around a given search effort, several kind of knowledge can be considered. Suppose that the Master is currently at a given state S M = (F, D M , Γ M ), where F is the original SAT instance, D M the set of decision literals, and Γ M the learnt database. In the following, from a given state S M , we derive three different characterizations of the Master search effort.

We use the Figure 2, to illustrate such characterizations. It represents a current state S M corresponding to the branch leading to the last conflict k. The decisions made in the last branch are x 1 , x 2 ,. . ., x n k . The boxes give a partial view of the implication graph obtained on the last k conflicts derived after the assignment of the last decisions x n k , x n k-1 , . . ., and x 1 . The learnt clauses are

(α n k ∨ a k ), (α n k-1 ∨ a k-1 ), . . ., (α n1 ∨ a 1 )
where a k , a k-1 , . . ., and a 1 are the asserting literals corresponding to the first-UIP ¬a k , ¬a k-1 , . . ., and ¬a 1 .

The first characterization of the Master search effort uses the current set of decisions D M (in short decision list). Using such decisions, the Slave can build the whole or a subset of the current partial assignment of the Master depending if all the asserting clauses generated by M are passed to S. Since the activity of the variables are not passed to the Slave, it shall explore the same area in a different way.

The second one, uses the sequence A M =< a k , a k-1 , . . . , a 2 , a 1 > (in short asserting set) of the Master asserting literals associated to the clauses learnt before

¬a k s k s k-1 x 2 x 1 ¬a 1 ¬a k-1 x i x nk x n1
x nk-1

s 1 ⊥ ⊥ (α k-1 ∨ a k-1 ) (α k ∨ a k ) a k-1 (α 1 ∨ a 1 )
⊥ Fig. 2. A partial view of the Master search tree the current state S M . The sequence is ordered from the latest to the oldest conflict. By branching on the ordered sequence A M using the same polarity, the Slave is able to construct a partial assignment involving the most recent asserting literals learnt from the Master unit. Let us recall that an asserting literal a i is part of the Master learnt clause (α ∨ a i ). As the Slave branches on a i , future conflicts analysis involving a i , might lead to learnt clauses containing ¬a i . More generally, invoking the Slave using A M pushes it to learn more relevant clauses, connected by resolution (contains complementary literals) to the most recent clauses learned by M . This is clearly an intensification process, as the clauses learnt by S involve the most important literals of M , and lead in some way to a more constructive resolution proof thanks to the complementary shared literals between M 's learnt clauses, and the future clauses that will be learnt by S.

The last one, uses the sequence of ordered sets C M =< s k , s k-1 , . . . , s 2 , s 1 > of literals collected during the Master conflict analysis (in short conf lict sets). The set s k represents the set of literals collected during the last conflict analysis. More precisely, the literals in s k correspond to the nodes of the implication graph located between the conflict side and the the first-UIP node ¬a k (see the Figure 2). Moreover, the set s k includes a literal of the conflicting variable and the literal labeling the first-UIP node ¬a k . It can be defined as s k =< y k1 , y k2 , . . . , y km >, where y k1 corresponds to the literal of the first-UIP node ¬a k and y km to the literal of the conflict variable as it appears in the partial interpretation. The aim of considering this sequence of sets is to intensify the search by directing S around the same conflicts.

We can remark that, the sequence A M and C M might contain redundant literals (the same literal occurs several times). As the Slave S assign such literals according to the defined ordering, S chooses the next unassigned literal in the ordering. To compare the relevance of the previously defined intensification strategies, we conducted the following experiments on the 2009 SAT Competition industrial category. We use ManySAT with two computing units (see figure 1) sharing clauses of size less or equal to 8. The Master S invokes the Slave S at each restart and transmits at the same time the intensification knowledge. For the Master M we used a rapid restart strategy. It is widely admitted that rapid restarts lead to better learning [START_REF] Biere | Adaptive restart strategies for conflict driven sat solvers[END_REF] or to learnt clauses of small width [START_REF] Pipatsrisawat | Width-based restart policies for clause-learning satisfiability solvers[END_REF]. Additionally, rapid restarts provide frequent intensification of the Slave leading to a tight synchronization of the search efforts.

Let us note that, the Slave do not implement any restart strategy. It restarts when invoked by the Master.

The Figure 3, shows the experimental comparison using the above three intensification strategies (decision list, asserting set, and conf lict sets). As we can observe, directing the search using conf lict sets gives the best results. The number of solved instances using the decision list, asserting set and conf lict sets are 201, 207 and 212 respectively. In the rest of this paper, we use conf lict sets as the intensification strategy.

Towards a Good Search Tradeoff

This section explores the diversification and intensification tradeoff. We are using the ManySAT architecture which is represented by a clique of four computational units interacting through clause sharing [START_REF] Hamadi | ManySAT: a parallel SAT solver[END_REF] up to size 8. These units represent a fully diversified set of strategies. In order to add some intensification, we propose to extend this architecture and to partition the units between Masters and Slaves. If we allow a Slave to intensify its own search effort through another Slave, we have a total of seven possible configurations. They are presented in Figure 4. In this Figure, dotted lines represents the Master/Slave relationships. Remark that when a unit has to provide intensification directives to several Slaves, it alternates its guidance between them, i.e., round-table. Moreover, when a configuration contains chain(s) of Slaves, (see (d), (f), and (g) in the Figure ), the intensification of a Slave of level i is triggered by the Slave of level i -1.

Experiments

Our tests were done on Intel Xeon quadcore machines with 32GB of RAM running at 2.66 Ghz. For each instance, we used a timeout of 4 hours of CPU time which corresponds to a 1 hour timeout per computational unit (core). Our Master/Slave roles and their different configurations were implemented on top of the original ManySAT. This solver was also used as a baseline for comparison. We used the conf lict sets intensification strategy.

We used the 292 industrial instances of the 2009 SAT competition to compare our different algorithms. The Table 1 summarizes our results. The first column presents the method, i.e., the original ManySAT (first line) or ManySAT extended with one of our seven diversification/intensification topology (see Figure 4). In the second column, the first number represents the overall number of SAT instances solved by the associated method, the second number (in parenthesis) gives the number of instances found SAT by a Slave. The third column gives similar information for UNSAT problems. The column four, gives the overall number of instances solved, again the parenthesis gives the number solved by one of the Slaves. Finally, the last two columns give respectively, the total time (cumulated), and the average time in seconds. The average is calculated over the overall set of 292 instances, using the 1 hour timeout when an instance is not solved.

Method

This Table shows that the vast majority of our topology-based extensions are superior to the original ManySAT. This algorithm solves 212 problems whereas the best topology (c) solves 221. Remarkably, all the topologies are able to solve more UN-SAT problems than ManySAT. This unsurprisingly shows that adding intensification, is more beneficial on this last category of problems. Indeed, our intensification strategy increases the relevance of the learnt clauses exchanged between masters and slaves, since unsatisfiable instances are mainly solved by resolution, improving the quality of the learnt clauses increases the performances on UNSAT problems.

When we compare the results achieved by our different topologies. It seems that balancing the tradeoff between 2 Slaves and 2 Masters works better (topo. b, c, and d). Among them, balancing the slaves to the masters gives the most efficient results i.e., topology c. The Table 2 highlights the results achieved by our best topology (c) against ManySAT on three complete families of problems. We can see that our best topology outperforms ManySAT on all these problems. Even more importantly, our algorithm allowed the resolution of two open instances (9dlx vliw at b iq8, and 9dlx vliw at b iq9), proved UNSAT for the first time.

The Figure 5, presents cumulated time results for ManySAT and for our best topology on the whole set of problems. On easy and medium problems, (solved in less than 10 minutes), the algorithms have the same behavior. On the other hand, when the problems become more difficult, the new technique exhibits an important improvement, and solves 9 more instances.

PMSat uses a master-slave scenario to implement a classical divide-and-conquer search [START_REF] Gil | PMSat: a parallel version of minisat[END_REF]. The user of the solver can select among several partitioning heuristics. Learnt clauses are shared between workers, and can also be used to stop efforts related to search spaces that have been proven irrelevant. PMSat runs on networks of computer through an MPI implementation.

[21], uses a standard divide-and-conquer approach based on guiding-paths. However, it exploits the knowledge on these paths to improve clause sharing. Indeed, clauses can be large with respect to some static limit, but when considered with the knowledge of the guiding path of a particular thread, a clause can become small and therefore highly relevant. This allows pMiniSat to extend the sharing of clauses since a large clause can become small in another search context.

Conclusion

We have explored the two well-known principles of diversification and intensification in portfolio-based parallel SAT solving. These dual concepts play an important role in several search algorithms including local search, and appear to be a key point in modern parallel SAT solvers. To study their tradeoff, we defined two roles for the computational units. Some of them classified as Masters perform an original search strategy, ensuring diversification. The remaining units, classified as Slaves are there to intensify their master's strategy.

Several important questions have been addressed. The first one is what information should be given to a slave in order to intensify a given search effort? It appeared that passing the set of literals found during previous conflict analysis gives the best results. This strategy aims at directing the slave towards conflicts highly related to the master's conflicts, allowing masters and slaves to share highly relevant clauses.

The second one is, how often, a subordinated unit has to receive such information? We have decided to exploit the restart policy of a master to refresh the information given to its slave(s). As shown in other works, rapid restarts lead to better learning [START_REF] Biere | Adaptive restart strategies for conflict driven sat solvers[END_REF] or to learnt clauses of small width [START_REF] Pipatsrisawat | Width-based restart policies for clause-learning satisfiability solvers[END_REF]. Therefore, a rapid restarts strategy on the master node reinforces the interests of the clauses shared with its slaves. In our context it allows frequent intensification of a Slave leading to a tight synchronization of the search efforts.

Finally, the question of finding the number of subordinated units along their connections with the search efforts had to be answered. Our tests have shown that balancing the set of nodes between Masters and Slaves roles, and balancing the slaves to the masters gives the best results. In particular, our best topology solves 9 more industrial instances than the actual best solver, ManySAT. The results have also demonstrated the relative performance of the intensification strategy on UNSAT problems. Remarkably, our new strategy was able to close the 9dlx vliw at b iq* family by finding the proofs of unsatisfiability for two open instances.

As future work, we would like to dynamically adapt the topology and roles in a portfolio based on the perceived hardness of a given instance. This should benefit to hard UNSAT proofs were several units could be used for intensification, and similarly help the quick discovery of satisfiable assignments.

Fig. 1 .

 1 Fig. 1. Intensification topology

Fig. 3 .

 3 Fig. 3. Three intensification strategies

Fig. 4 .

 4 Fig. 4. Diversification/Intensification topologies

Table 1 .

 1 2009 SAT Competition, Industrials: overall results

		# SAT # UNSAT	Total Tot. time Avg. time
	ManySAT	87	125	212 329338	1127
	Topo. (a)	86 (7) 133 (49) 219 (56) 311545	1066
	Topo. (b) 84 (28) 130 (73) 214 (101) 324900	1112
	Topo. (c) 89 (23) 132 (74) 221 (97) 307419	1052
	Topo. (d) 87 (25) 132 (67) 219 (92) 315795	1081
	Topo. (e) 86 (45) 131 (109) 217 (154) 323501	1107
	Topo. (f) 82 (44) 128 (102) 210 (146) 339640	1163
	Topo. (g) 80 (45) 126 (107) 206 (152) 343233	1175

Table 2 .

 2 2009 SAT Competition, Industrials: time (s) results on three families

	Instance	Status ManySAT Topology (c)
	9dlx vliw at b iq1	UNSAT	87.3	7.6
	9dlx vliw at b iq2	UNSAT	256.3	31.9
	9dlx vliw at b iq3	UNSAT	605.8	103.2
	9dlx vliw at b iq4	UNSAT	1106	163.5
	9dlx vliw at b iq5	UNSAT	2490	313.1
	9dlx vliw at b iq6	UNSAT	-	735.6
	9dlx vliw at b iq7	UNSAT	-	983
	9dlx vliw at b iq8	UNSAT	-	1807.6
	9dlx vliw at b iq9	UNSAT	-	2640.9
	velev-pipe-sat-1.0-b10	SAT	4.8	3.6
	velev-engi-uns-1.0-4nd UNSAT	5	4.8
	velev-live-uns-2.0-ebuf UNSAT	6.9	6.8
	velev-pipe-sat-1.0-b7	SAT	47.3	5.1
	velev-pipe-o-uns-1.1-6 UNSAT	61.9	31.4
	velev-pipe-o-uns-1.0-7 UNSAT	159.9	110.2
	velev-pipe-uns-1.0-8	UNSAT	262.2	88.9
	velev-vliw-uns-4.0-9C1 UNSAT	314.6	236.6
	velev-vliw-uns-4.0-9-i1 UNSAT	-	1307.8
	goldb-heqc-term1mul UNSAT	21.8	4.8
	goldb-heqc-i10mul	UNSAT	39.5	24.1
	goldb-heqc-alu4mul	UNSAT	46.2	42.6
	goldb-heqc-dalumul	UNSAT	380.3	36.2
	goldb-heqc-frg1mul	UNSAT	2566	63.8
	goldb-heqc-x1mul	UNSAT	-	226.9

By structure, we understand the dependencies between variables, which can often appear through Boolean functions. One particular example being the well known notion of backdoors.

Previous Work

We present here the most noticeable approaches related to parallel SAT solving.

In [START_REF] Jurkowiak | A parallelization scheme based on work stealing for a class of sat solvers[END_REF] a parallelization scheme for a class of SAT solvers based on the DPLL procedure is presented. The scheme uses a dynamic load-balancing mechanism based on work-stealing techniques to deal with the irregularity of SAT problems. PSatz is the parallel version of the well known Satz solver. Gradsat [START_REF] Chrabakh | GrADSAT: A parallel sat solver for the grid[END_REF] is based on zChaff. It uses a master-slave model and the notion of guiding-paths to split the search space and to dynamically spread the load between clients. Learned clauses are exchanged between all clients if they are smaller than a predefined limit on the number of literals. A client incorporates a foreign clause when it backtracks to level 1 (top-level).

[17] uses an architecture similar to Gradsat. However, a client incorporates a foreign clause if it is not subsumed by the current guiding-path constraints. Practically, clause sharing is implemented by mobile-agents. This approach is supposed to scale well on computational grids.

In [START_REF] Böhm | A fast parallel sat-solver -efficient workload balancing[END_REF], the input formula is dynamically divided into disjoint subformulas. Each subformula is solved by a sequential SAT-solver running on a particular processor. The algorithm uses optimized data structures to modify Boolean formulas. Additionally workload balancing algorithms are used to achieve a uniform distribution of workload among the processors.

MiraXT [START_REF] Lewis | Multithreaded sat solving[END_REF], is designed for shared memory multiprocessors systems. It uses a divide and conquer approach where threads share a unique clause database which represents the original and the learnt clauses. When a new clause is learnt by a thread, it uses a lock to safely update the common database. Read access can be done in parallel.


Gilles Audemard
email: audemard@cril.fr

Jean-Marie Lagniez
email: lagniez@cril.fr

Bertrand Mazure
email: mazure@cril.fr

Lakhdar Saïs
email: sais@cril.fr

Boosting local search thanks to CDCL

In this paper, a novel hybrid and complete approach for propositional satisfiability, called SATHYS (Sat Hybrid Solver), is introduced. It efficiently combines the strength of both local search and CDCL based SAT solvers. Considering the consistent partial assignment under construction by the CDCL SAT solver, local search is used to extend it to a model of the Boolean formula, while the CDCL component is used by the local search one as a strategy to escape from a local minimum. Additionally, both solvers heavily cooperate thanks to relevant information gathered during search. Experimentations on SAT instances taken from the last competitions demonstrate the efficiency and the robustness of our hybrid solver with respect to the state-of-the-art CDCL based, local search and hybrid SAT solvers.

Introduction

The SAT problem, namely the issue of checking whether a Boolean formula in Conjunctive Normal Form (CNF) is satisfiable or not, is a central issue in many artificial intelligence and computer science domains, including hardware and software verification, planning, cryptography and bioinformatics. These last two decades, many approaches have been proposed to solve large application SAT instances, based on logically complete or incomplete methods. Both stochastic local search (SLS) techniques [START_REF] Selman | Noise strategies for improving local search[END_REF][START_REF] Selman | An empirical study of greedy local search for satisfiability testing[END_REF][START_REF] Hirsch | Unitwalk: A new SAT solver that uses local search guided by unit clause elimination[END_REF] and elaborate variants of the DPLL procedure [START_REF] Davis | A machine program for theorem-proving[END_REF], commonly named modern SAT solvers [START_REF] Moskewicz | Chaff: Engineering an efficient SAT solver[END_REF][START_REF] Een | An extensible SAT-solver[END_REF], can now solve many families of hard SAT instances. Based on different paradigms, these two kinds of approaches admit complementary behavior in terms of performances. Modern SAT or CDCL (Conflict Driven Clause Learning) solvers are particularly efficient on application benchmarks while local search performs better on random SAT instances. Stochastic Local search (Algorithm 2) and modern SAT solvers (Algorithm 1) are recognized as two important search paradigms. Their differences arise in the way the search space is explored. In SLS, the algorithm explores the search space in a non systematic way starting from a complete assignment and moving to another complete assignment by inverting the truth value of a chosen variable (this is a flip). After a fixed number of flips, another complete assignment is generated, and the process is repeated. Modern SAT solvers explore the search space in a systematic way by developing a search tree, where at each node the current partial assignment is extended by assigning a selected variable and propagating unit literals. In SLS, the search process can lead to a local minimum, in this case several strategies are designed to escape from such minimum. In modern SAT solvers, the process can lead to a conflict and in this case several learning strategies are designed for resolving such a conflict [START_REF] Zhang | Efficient conflict driven learning in boolean satisfiability solver[END_REF].

Combining stochastic local search and conflict driven clause learning solvers is clearly a challenging issue as stated by Selman et al. [START_REF] Selman | Ten challenges in propositional reasoning and search[END_REF] in 1997 (challenge 7) and in 2003 [START_REF] Kautz | Ten challenges redux: Recent progress in propositional reasoning and search[END_REF]. Such a combination might exploit the strength of both approaches and might result in a new but more efficient hybrid SAT solver. Several attempts have been made these last years [START_REF]Handbook of Satisfiability[END_REF] and different hybrid solvers have been designed leading to real progress towards the resolution of this challenging issue (see section 5). However, the challenge remains open as the performance of these proposed hybrid solvers is far from those of the CDCL based solvers particularly on application instances. Our goal in this paper is to design a hybrid SLS/CDCL solver that outperforms the local search techniques, while significantly reducing the gap with CDCL based solvers particularly on application category.

In this paper, we propose a new hybridization of local search and modern SAT solver, named SATHYS (Sat Hybrid Solver). In our approach, both components heavily cooperate through relevant information gathered during search. More precisely, our hybrid solver alternatively performs the search process using local search and CDCL based SAT solvers. On the one hand, at each node of the search tree, the local search component is used to extend to the model, the current (consistent) partial assignment built by the CDCL based component. On the other hand, the CDCL part is conditionally invoked by the local search component when a local minimum is encountered. Each solver benefits from the other in several ways. First, each time a local minimum is reached, the local search technique updates the activity of the boundary variables [START_REF] Goldberg | Boundary points and resolution[END_REF]. The idea is to direct the CDCL search towards boundary points proven to be important by Goldberg in [START_REF] Goldberg | Boundary points and resolution[END_REF]. Secondly, the polarities of the literals involved in the best complete assignment found during local search are exploited by the CDCL component. From the other side, the CDCL solver shares with local search the current partial assignment together with the learnt clauses. The originality of our proposed hybrid SAT solver arises in alternating search of both components while exchanging relevant information.

The rest of the paper is organized as follows. Section 2 introduces some definitions and notations. Then, we present CDCL and SLS solvers in a unified way. Section 3 describes our new hybrid solver. In Section 4 we provide some experimental comparison with different SAT solvers including the CDCL solver MINISAT and several well known SLS and hybrid solvers. Before concluding, section 5 discusses the related works.

Technical Background

Preliminary definitions and notations

Let V = {x 1 , ..., x n } be a set of propositional variables, a literal ℓ is either a positive x i or a negative variable x i . The two literals x and x are said complementary. We denote by ℓ the complementary literal of ℓ. A clause c i = (ℓ 1 ∨ . . . ∨ ℓ ni ) is a disjunction of literals. A unit clause is a clause with only one literal, called unit literal. A formula Σ = (c 1 ∧. . .∧c m ) is in conjunctive normal form (CNF) as it is a conjunction of clauses. The set of variables involved in Σ will be noted V Σ . An interpretation I of a Boolean formula Σ associates a truth value I(x) ∈ {f alse, true} to some variables x ∈ V Σ . I is complete if it assigns a truth value to every x ∈ V Σ , and partial otherwise. A complete (resp. partial) interpretation will be noted I c (resp. I p ). A clause, a CNF formula and an interpretation can be represented using sets.

It should say that a clause β is falsified (resp. satisfied) by I if ∀ℓ ∈ β (resp. ∃ℓ ∈ β), β is falsified (resp. satisfied) by ℓ under I. Σ |ℓ denotes the formula simplified by the assignment of the literal ℓ to true, that is Σ |ℓ = {α \ {ℓ} such that α ∈ Σ and ℓ ∈ α}. This notation can be extended to an interpretation. Let I = {ℓ 1 , ..., ℓ n } be an interpretation,

Σ | I = (...(Σ| ℓ1 )...| ℓn ).
A model of a formula Σ, noted I |= Σ, is an interpretation I such that ∀c ∈ Σ, c is satisfied by I. On the contrary, an interpretation I is called a nogood of Σ, noted I |= Σ, if ∃c ∈ β such that c is falsified by I.

SAT is the problem of checking whether a CNF formula admits a model or not. If the answer is positive, then the formula is called satisfiable, else it is called unsatisfiable.

CDCL solvers

CDCL based SAT solvers (Algorithm 1), generally referred as modern SAT solvers [START_REF] Moskewicz | Chaff: Engineering an efficient SAT solver[END_REF], are based on classical unit propagation (lines 2, 14 and 15) efficiently combined through incremental data structures, restart policies (line 15) [START_REF] Gomes | Boosting combinatorial search through randomization[END_REF], activity-based variable selection heuristics (VSIDS-like) (line 12) [START_REF] Moskewicz | Chaff: Engineering an efficient SAT solver[END_REF], and clause learning (line 6) [START_REF] Silva | Grasp -a new search algorithm for satisfiability[END_REF].

A CDCL based SAT solver is a sophisticated variant of the well known DPLL [START_REF] Davis | A machine program for theorem-proving[END_REF] procedure. At each node of the search tree, the assigned literals (the decision literal and the propagated ones) are labeled with the same decision level starting from 1 and increased at each decision (or branching step). After backtracking, some variables are unassigned and the current decision level is decreased accordingly. At level m, the current partial interpretation I p can be represented as an ordered sequence of decisionpropagation steps made at the different levels. We note I i p where i ≤ m, the partial interpretation I p restricted to the first i sequences of decision-propagation. An asserting level associated to a falsified clause α = (x ∨ β) under an interpretation I p (in short level(α, I p )) is defined as the level j such that α| I j p = x and x represents the asserting literal of α under I p Algorithm 1 describes the general skeleton of a CDCL based SAT solver. Let us briefly explain its main components. A more detailed description of modern SAT solvers can be found in [START_REF] Darwiche | Complete Algorithms[END_REF]. The algorithm initializes the learnt database Γ as the empty set (line 1), then unit propagation is applied on the original formula Σ (line 2). The function BCP (Σ) returns the set of propagated literals. The main loop contains several cases. First, if all variables are assigned then the formula is empty and I is a model of Σ (line 4). If the partial assignment I p is consistent, then a new decision variable is chosen and unit propagation is performed (lines 12, 13 and 14). Otherwise, a conflict is reached and a nogood (or a learnt clause) α is computed (line 6). If α is the empty clause, then the instance is proven unsatisfiable (line 8). Otherwise, α = (x ∨ β) and j the asserting level of α w.r.t. I p . After that, the clause α is added to the learnt database (line 9) and the algorithm backtracks to level j by computing a new partial interpretation I j p (line 10). At level j the asserting literal x ∈ α is propagated (line 14). Finally, the algorithm restarts if the cutoff value in terms of the number of conflicts is reached (line 15).

if (∅ ∈ Σ |Ip ) then 5 α=(x ∨ β) ← analyzeConf lict(Σ ∪ Γ, Ip); 6 j ← level(α, Ip); 7 if (α = ∅) then return UNSAT; 8 Γ ← Γ ∪ {α}; 9 Ip ← I j p ; 10 else 11 x ← chooseDecisionLiteral(Σ |Ip ); 12 Ip ← Ip ∪ {x}; 13 Ip ← Ip ∪ BCP ((Σ ∪ Γ ) |Ip ); 14 if (restart()) then Ip ← BCP (Σ ∪ Γ ); 15 2.

Local search solvers

Algorithm 2 gives the general scheme of a local search solver. It uses a stochastic walk over complete interpretations of Σ. At each step (or flip), it tries to reduce the number of falsified clauses (this step is usually called a descent). The next complete interpretation is chosen among the neighbors (interpretations that differ only by the truth value of one variable) of the current one (line 7). A local minimum is reached when no descent is possible. In such a case, a strategy is used in order to escape from this minimum (line 5). Like in CDCL solvers, sometimes a restart (called a try in SLS) is performed and a new complete interpretation is generated. However restarts in CDCL and SLS solvers have not exactly the same role. In the CDCL case, it is now well admitted that restarts are used to reorder variables, directing the solver to the same part of the search space using a different branch. On the other hand, restarts in SLS solvers are used in order to diversify the search by generating a new complete interpretation.

SATHYS: A novel Hybrid Approach

In this section, we present SATHYS, our hybrid solver for SAT which is available at http://www.cril.fr/ ˜lagniez/sathys. Before giving its formal description, we provide some intuitions and motivations behind the design of SATHYS.

Motivations

Recently, several works have shown that local search techniques provide relevant information for locating unsatisfiable cores [START_REF] Gregoire | Extracting MUSes[END_REF][START_REF] Gregoire | Local-search extraction of muses[END_REF]. Motivated by these results, we propose x ← chooseLitteralT oF lip(Σ, Ic);

7 f lip(Ic, x); 8 if (restart()) then Ic ← completeInterpretation(Σ); 9
a new hybridization scheme of SLS and CDCL solvers. In our hybrid approach, the two methods heavily interact and play complementary roles :

1. SLS directs the CDCL search towards the proof of unsatisfiability ; 2. CDCL directs the SLS search towards a model if it exists.

Let us briefly summarize these bidirectional interactions.

SLS → CDCL:

The SLS affects the CDCL solver at two different levels known to be important for the efficiency of satisfiability solvers. First, the activity of the variables usually maintained by CDCL are dynamically refined by the SLS component. This local search refinement of the activity-based heuristic (VSIDS) is achieved using the notion of boundary points introduced recently by E. Goldberg in [START_REF] Goldberg | Boundary points and resolution[END_REF]. A boundary point is a complete interpretation (point) I such that there exists at least one literal ℓ belonging to all clauses falsified by I. In [START_REF] Goldberg | Boundary points and resolution[END_REF], it was shown that focusing resolution on such kind of literals ℓ improves the proof quality by reducing the length of the refutation. From the recent work by Grégoire et al. [START_REF] Gregoire | Local-search extraction of muses[END_REF], we can also deduce that if the boundary point corresponds to a local minimum, then the literal ℓ belongs to at least one unsatisfiable core. Considering these two interesting features of boundary points, we exploit this notion to refine the activity of the clauses. When a local minimum is reached, updating the activity of the variables associated to literals appearing in all the falsified clauses by the boundary point might guide CDCL towards the most important part of the search space. Indeed, favoring the assignment of such literals aims to direct the search to unsatisfiable cores and might reduce the length of the resolution proof.

The second interaction level where SLS influences with CDCL is on the assignment polarity (f alse, true) of the chosen variable. More precisely, when the next variable to assign is chosen by CDCL, its polarity is taken from the best complete interpretation (in terms of the number of satisfied clauses) found by the SLS solver. Usually, in CDCL solvers such as Rsat [START_REF] Pipatsrisawat | A lightweight component caching scheme for satisfiability solvers[END_REF], the assignment polarity (or phase) follows a progress saving scheme. Each time a variable is assigned, its truth value is saved, and used as the polarity of the variable when such a variable is selected again.

CDCL → SLS: From CDCL to SLS, the current CDCL branch made of the set of decisions and propagations is provided to SLS. Using such a partial interpretation, the SLS solver tries to extend it into a model by focusing search on the remaining unassigned variables. In this way, local search exploits variable dependencies provided by the decisions and propagations of the CDCL solver. Let us recall that exploiting variable dependencies is identified as an important issue for the efficiency of local search based techniques [START_REF] Selman | Ten challenges in propositional reasoning and search[END_REF][START_REF] Kautz | Ten challenges redux: Recent progress in propositional reasoning and search[END_REF][START_REF] Pham | Building structure into local search for sat[END_REF]. On the other hand, as the CDCL solver is called when SLS reaches a local minimum, the new partial interpretation revised by CDCL contains several flipped variables. Consequently, from the local search side CDCL can be seen as a strategy that helps local search to escape from local minima.

Formal description

Even if the main core of the SATHYS hybrid solver is a local search based algorithm, the integration of the CDCL part leads to a complete hybrid solver able to prove both satisfiability and unsatisfiability. In this section, we give a detailed description of our approach as depicted by the Algorithm 3.

First of all, the algorithm starts with an empty set of learnt clauses (Γ ) and a complete interpretation I c built by randomly extending the current partial interpretation I p obtained by propagating unit literals on the original formula (lines 2-3). Note that function BCP (Boolean Constraint Propagation) returns the set of propagated unit literals. After this initialization step local search process is performed. If there exists a neighboring interpretation (an interpretation that differs from I c by only the truth value of one variable x), that reduces the number of falsified clauses (descent phase), then the variable x is flipped, i.e. its truth value is reversed (lines [START_REF] Hutter | Scaling and probabilistic smoothing: Efficient dynamic local search for sat[END_REF][START_REF] Jussien | Local search with constraint propagation and conflict-based heuristics[END_REF]. It is important to note that only variables out of I p can be flipped. Indeed, the variables involved in I p are considered tabu during the local search step. This partial interpretation evolves during the search and is modified in the CDCL part of the algorithm (lines [START_REF] Ferris | Walksat as an informed heuristic to DPLL in SAT solving[END_REF][START_REF] Gableske | Satun: A complete hybrid sat solver[END_REF][START_REF] Gebser | Conflict-driven answer set solving[END_REF][START_REF] Goldberg | Boundary points and resolution[END_REF][START_REF] Gomes | Boosting combinatorial search through randomization[END_REF][START_REF] Gregoire | Extracting MUSes[END_REF][START_REF] Gregoire | Local-search extraction of muses[END_REF][START_REF] Habet | A hybrid approach for sat[END_REF][START_REF] Havens | A hybrid schema for systematic local search[END_REF]. However at each iteration of the loop (line 4), we have

I p ⊆ I c .
When a local minimum is reached (line 6), we select one of the two following strategies : (1) call the CDCL component of the solver (lines 11-19) or (2) apply any other repair strategy, like novelty [START_REF] Mcallester | Evidence for invariants in local search[END_REF] or rsaps [START_REF] Hutter | Scaling and probabilistic smoothing: Efficient dynamic local search for sat[END_REF], to escape from such local minima (lines 8-9). The selection between the two strategies is done using a condition based on the search progress SLSprogress that will be explained later.

Each time the CDCL part of the solver is called (lines 11-20), a decision literal ℓ is chosen (line 11). Then unit propagation is performed (line 12). If it leads to a contradiction (line 13), a classical analysis is performed, the learnt clause γ is added to the learnt database Γ before back-jumping to the level j. If the learnt clause is empty, then the the formula is proven unsatisfiable (line 16). As long as the current partial interpretation I p is not consistent, the process continues (see the loop line 13). At the end of this process, the consistent partial interpretation I p is extended to a complete one I c (line 20) and the local search component continues the search process. After each CDCL part, the partial interpretation I p is modified (line 19). Consequently, the fixed part of the complete interpretation I c is also modified. In this way, we derive a new strategy based on CDCL to escape from local minima. This process is repeated until the next restart (line 24). As long as a model is not found or the unsatisfiability of the formula is not proven the solver restarts the previous process with a new initial complete interpretation (lines 25-26).

In the following, we introduce some improvements embedded in our solver SATHYS.

Calling the CDCL oracle. The behavior of our hybrid method heavily depends on the value of the variable SLSprogress (see Algorithm 3, line 7). We use a similar mechanism as it is done in [START_REF] Hoos | An adaptive noise mechanism for walksat[END_REF]. When the local search engine reduces the MAXSAT value found in the current restart, this variable SLSprogress is increased. Our reasoning is that as long as SLS allows improvements i.e. increases the number of satisfied clauses, the execution of SLS is favored. Each time a local minimum is reached, the value of SLSprogress is decreased. By getting frequently stuck in local minima, it seems that the local search engine has a real difficulty to improve the current interpretation. In this case, we need to call the CDCL engine in order to escape from these local minima.

Activity based heuristic for CDCL. The heuristic used in the CDCL part of the Algorithm 3 is a slightly modified version of VSIDS [START_REF] Moskewicz | Chaff: Engineering an efficient SAT solver[END_REF]. Indeed, as usual, all weights of the variables are increased during the conflict analysis. Furthermore, when a local minimum is reached, we look for a boundary point and we increase the activity of the variable with one of its literals appearing in all the falsified clauses. In this way, and as explained above, our aim is to generate shorter resolution proofs.

Polarity of the decision literals. The polarity of the decision variable is known to be very important for the efficiency of SAT solvers. We propose here to use both engines in order to choose the best polarity for a given variable. At each restart, we store the interpretation associated to the current MAXSAT value and we modify it using progress saving [START_REF] Pipatsrisawat | A lightweight component caching scheme for satisfiability solvers[END_REF]. Then when a given decision variable is chosen by CDCL, its polarity is taken from the last memorized complete interpretation with the best MAXSAT value. Indeed, we focus the search near the MAXSAT value, so near a solution by taking into account dependencies between variables.

Experimental validation

In this section, we provide an experimental validation of our hybrid solver SATHYS. Like most other solvers, we use SatElite in a preprocessing step [START_REF] Eén | Effective preprocessing in SAT through variable and clause elimination[END_REF]. Instances from the SAT'09 competition are used as a test set. They are divided into three different categories: crafted (281 instances), application (292) and random (570). Let us note that these instances are carefully selected for the SAT competition because of their relevance. From the results of the last SAT competitions, one can have in mind that most of the state-of-the-art SAT solvers present very close performance in terms of the number of solved instances. For example, PRECOSAT [START_REF] Biere | PicoSAT essentials[END_REF] and GLUCOSE [START_REF] Audemard | Predicting learnt clauses quality in modern SAT solvers[END_REF] were ex-aequo in terms of the number of solved instances in the application category SAT +UNSAT).

The experimentation has been conducted on the same cluster as for last SAT 2009 competition (Intel Xeon 3GHz under Linux with a RAM memory size of 2GB). The time limit (time-out) has been set to 1200 CPU seconds.

Effectiveness of the collaboration

First of all, our goal is to highlight that our hybrid scheme is really relevant. To measure the relevance of the different improvements introduced to SATHYS (described in the previous sections), we compared SATHYS with the following variants:

-SATHYS nb : the VSIDS heuristic is not updated when a boundary point is discovered. 1. Comparison of different versions of the SATHYS solver. For each category, we provide the number of solved instances. The total number of solved instances on all categories is also given.

The Table 1 summarizes the obtained by the four versions of SATHYS solver. Not surprisingly, we can note that SATHYS nb is the best one on random instances. Indeed, random instances are globally unsatisfiable i.e. the unsatisfiable core tends to include all the clauses of the original formula. As the role of the activities (VSIDS) is to focus the search on the most important part of formula, this is clearly not relevant in case of random instances. Also, the boundary points are useless for this kind of instances.

Concerning SATHYS cdclAtEachLM , this version is the worst one. Indeed, too many calls of CDCL consumes clearly too much time. Moreover, as CDCL approaches are not well suited for random instances, calling CDCL penalizes SATHYS. We can note that the number of calls to the CDCL engine has an important impact on the performances of SATHYS. Consequently, fine-tuning the local search progress (SLSprogress) is crucial for the efficiency of our hybrid approach.

Concerning SATHYS noP olarity , this version obtains good performance on the crafted category. However, literals polarity seems to be a relevant criteria for application instances considered as the most important category by the SAT community.

In summary, the cooperation scheme designed in SATHYS and described in the previous section improves the robustness and the efficiency of our hybrid solver.

Comparison

In this section, we compare our solver against some of the well known SAT solvers. Many of them are considered as the state-of-the-art SAT solvers in at least one category of instances. We can note that four solvers considered in our comparative experiments have obtained a gold medal at the SAT competition in 2009 in different categories.

-Two SLS methods: WSAT [START_REF] Selman | Noise strategies for improving local search[END_REF] with rnovelty strategy and ADAPTG2 [START_REF] Li | Combining adaptive noise and look-ahead in local search for sat[END_REF].

-Two hybrid approaches: HYBRIDGM [START_REF] Balint | A novel approach to combine a SLS-and DPLL-solver for the satisfiability problem[END_REF] and HINOTOS [START_REF] Letombe | Improvements to hybrid incremental sat algorithms[END_REF].

-Five complete approaches: MINISAT [START_REF] Een | An extensible SAT-solver[END_REF], GLUCOSE [START_REF] Audemard | Predicting learnt clauses quality in modern SAT solvers[END_REF], PRECOSAT [START_REF] Biere | PicoSAT essentials[END_REF], RSAT [START_REF] Pipatsrisawat | A lightweight component caching scheme for satisfiability solvers[END_REF],

and CLASP [START_REF] Gebser | Conflict-driven answer set solving[END_REF]. -A portfolio solver : SATZILLA I [START_REF] Xu | Satzilla: Portfolio-based algorithm selection for sat[END_REF].

Table 2 summarizes the obtained results. Let us start this comparison with local search solvers. We can note that they perform better than SATHYS only in the random category of instances. This is not surprising since they are particularly suited to this kind of instances. On the other categories of instances, local search based techniques obtain bad results. As underlined during the SAT'09 competition, the main weak point of local search based solvers resides in their inefficiency on the application category. Improving local search based techniques on application category remains a very challenging issue. 2. SATHYS vs. some other SAT solvers. For each category and each solver, the number of solved instances is provided.

As the skeleton of our solver is an SLS technique, where the CDCL component can be considered as a strategy for escaping from local minima, the good performances of our hybrid solver provides real advances on this important issue.

Comparatively with other hybrid solvers, SATHYS is the best one w.r.t. in the application category. HYBRIDGM seems to be tuned for random instances whereas HINOTOS and SATHYS are comparable on crafted category. The results show clearly that our hybrid solver outperforms all the hybrid approaches.

SATHYS is very competitive with respect to the sate-of-the-art CDCL solvers in both crafted and application categories. To our best knowledge, it is the first time that an hybrid solver is able to obtain such promising results. On random instances, classical CDCL solvers present a very bad behavior. On this last category, clause learning and back-jumping are useless.

Interestingly enough, SATHYS is also very competitive with respect to the portfolio based solver SATZILLA. This portfolio uses CDCL, local search and lookahead solvers. In this approach, the different solvers are called independently.

To summarize, SATHYS is the first competitive solver on all the three categories of SAT instances (crafted, application and random). It is also the most robust one: it obtains the best overall results in terms of the total number of solved instances and it is often close to the first rank on each category.

The previous table provides information about the number of solved instances in the considered time limit. Also, we present the classical scatter plot in order to compare SATHYS with one of the best known hybrid solver HINOTOS, PRECOSAT (the stateof-the-art solver on application category), CLASP (the best solver on crafted category) and SATZILLA (it obtains the second best overall results behind SATHYS). In these curves, the y-axis represents the time (in log scale) of SATHYS and the x-axis the time of the other solver. So, a dot below the diagonal represents an instance where SATHYS is faster than the other solver. This is shown in Figure 1.

Analyzing these figures, we can conclude that SATHYS outperforms HINOTOS. However our approach is slightly slower than PRECOSAT, which is one of the best CDCL solvers. However, SATHYS solves more instances than PRECOSAT. Comparatively with CLASP, we can observe that our method obtains similar performance on application and crafted instances, but SATHYS is better on random instances. Finally, it is impossible to differentiate SATZILLA and SATHYS in terms of CPU time. Finally, we also want to hightlight that our solver is competitive on difficult hard SAT and UNSAT instances from crafted and application categories. Table 3 provides results on a selection of instances. Because of lack of space we do not report the results for each solver. However, to be as fair as possible, we also report the best result obtained in the competition over the 50 submitted solvers (BEST column). SATHYS is efficient on SAT as well as UNSAT instances.

In conclusion of this experimental comparison, SATHYS is a very efficient solver in three categories (crafted, application and random) and consequently, it is the most robust solver. From the above results, we can consider SATHYS as the first hybrid solver that brings real advances to three of the ten challenges proposed in [START_REF] Selman | Ten challenges in propositional reasoning and search[END_REF][START_REF] Kautz | Ten challenges redux: Recent progress in propositional reasoning and search[END_REF]:

-

Related work

We presents here the most noticeable approaches combining local search and DPLL based ones. They can be classified in three different categories depending on which of the two solvers is considered as the main core of the hybrid solver.

The first category includes those using DPLL as the main solver and SLS as an oracle. In [START_REF] Crawford | Solving satisfiability problems using a combination of systematic and local search[END_REF], SLS is used in a preprocessing step to derive a static variable ordering for DPLL. Weights representing the number of times each clause is falsified during the local search pretreatment is computed. The variable occurring most often in clauses with higher weights is selected first. The approach proposed in [START_REF] Mazure | Boosting complete techniques thanks to local search methods[END_REF] extends the previous one, while invoking SLS at each node of the search tree. The SLS oracle is used to both extend the current partial assignment to a model or to select the next variable to assign according to similar clause weighting process. Similarly to [START_REF] Mazure | Boosting complete techniques thanks to local search methods[END_REF], in [START_REF] Ferris | Walksat as an informed heuristic to DPLL in SAT solving[END_REF], the authors introduce some conditions to reduce the number of calls to SLS. The variables are dynamically ordered according to local-search statistics. In [START_REF] Havens | A hybrid schema for systematic local search[END_REF], an hybrid constraint solving schema which retains some systematicity of constructive search while incorporating the heuristic guidance and lack of commitment to variable assignment of local search. The proposed method backtracks through a space of complete but possibly inconsistent solutions while supporting the freedom to move arbitrarily under heuristic guidance. hybridGM is an incomplete SAT solver proposed in [START_REF] Balint | A novel approach to combine a SLS-and DPLL-solver for the satisfiability problem[END_REF] focusses the DPLLsearch around local minima with only one unsatisfied clause.

If a formula is satisfiable, chances are to find a satisfying assignment around such minima. hybridGM's DPLL component then completely checks these areas of the search space. SATUN [START_REF] Gableske | Satun: A complete hybrid sat solver[END_REF] an extension of hybridGM performs local search as it is done by hybridGM, but for a limited amount of time. The limit is set in a way that gives local search a reasonable chance to find a satisfying assignment. In case the formula is satisfiable, this will result in a performance competitive with the hybrid's SLS component. As soon as the limit is reached, the formula is expected to be unsatisfiable. SATUN's DPLL component will then perform a search on the complete search space of the formula to confirm that assumption.

The second category considers SLS as the main core of the hybrid solver. Among these approaches, we can cite the approach proposed in [START_REF] Habet | A hybrid approach for sat[END_REF], where DPLL is used to derive implications between literals. These implications are used to both simplify the formula and to compute dependency relations between literals used during the local search phase.

In [START_REF] Jussien | Local search with constraint propagation and conflict-based heuristics[END_REF] the algorithm starts with a partial or complete interpretation. At each step constraint propagation is applied. In case of conflict, a nogood is learnt and local search is applied to repair the current partial interpretation. Otherwise, the current consistent interpretation is extended in a classical way. In [START_REF] Kroc | Integrating systematic and local search paradigms: A new strategy for maxsat[END_REF], the authors propose an hybrid strategy based on shared memory, ideally suited for multi-core processor architectures. They particularly show that DPLL can provide highly effective guidance for a local search style solver for the MAXSAT problem. More precisely, DPLL shares its current partial assignment with SLS and a flip is not allowed if the variable is assigned with the same polarity by DPLL. The two solvers are run simultaneously on two different cores.

Finally, the last category contains hybrid solvers where both engines play an equal role. The hybrid solver HBISAT [START_REF] Fang | A new hybrid solution to boost SAT solver performance[END_REF] and its extended and improved version hinotos [START_REF] Letombe | Improvements to hybrid incremental sat algorithms[END_REF] belong to this category. In both approaches, a local search is used to identify a subset of clauses to be passed to a DPLL SAT solver through an incremental interface. In other words, the guided local search identifies incremental sets of clauses that are hard, and these clauses are subsequently added to the clause database of the DPLL-based solver. In addition, the solution obtained by the DPLL solver on the subset of clauses is fed back to the local search solver to jump over any locally optimal points.

Conclusion

In this paper a novel integration of SLS and CDCL based SAT solvers is introduced. This hybrid solver represents an original combination of both engines. The two components heavily cooperate towards proving the satisfiability or unsatisfiability of the SAT for-mula. Such strong cooperation lies in the exploitation of SLS for directing CDCL search towards unsatisfiability proof; and CDCL for escaping from SLS local minima. SATHYS, the resulting method, obtains very good results on a wide range of instances taken from the last competitions. These results show important performance improvements of the state-of-the-art SLS and hybrid SLS solvers particularly on crafted and application category. More interestingly, SATHYS significantly reduces the performance gap between SLS and CDCL solvers while becoming extremely competitive with most of the state-ofthe arts CDCL solvers on application instances. Consequently, SATHYS can be considered as the first successful hybrid SAT solver. A future work, we first plan to investigate how conflict driven clause learning can be adapted to local search based techniques. Secondly, as the cooperation scheme between the two solvers integrated in SATHYS is proven to be efficient, we plan to design a new parallel version of SATHYS in order to benefit from the computational resources of multicore based architectures.

Algorithm 1 : 1 Ip

 11 CDCL solverInput: a CNF formula Σ Output: SAT or UNSAT Γ ← ∅; |Ip = ∅) then return SAT;

4

 4

Algorithm 2 : 1 while (true) do 2 if 3 if a local minimum is reached then 4 x

 21234 Local Search solverInput: a CNF formula Σ Output: SAT Ic ← completeInterpretation(Σ) ; (Σ |Ic = ∅) then return SAT; ← chooseLitteralT oEscapeM inima(Σ, Ic);

Algorithm 3 : 5 if a local minimum is reached then 6 if (SLSprogress > 0) then 7 ℓ 16 Γ 17 Ip ← I j p ; 18 Ip 21 x

 356716171821 SATHYSInput: a CNF formula Σ Output: SAT or UNSAT Γ ← ∅;1 Ip ← BCP (Σ); 2 Ic ← Ip ∪ completeInterpretation(Σ |Ip ); 3 while (true) do 4 if (Σ |Ic = ∅) then return SAT; ← chooseLitteralT oEscapeLocalM inima(Σ |Ip , Ic); ∪ {ℓ} with ℓ ∈ Ip; 11 Ip ← Ip ∪ BCP ((Σ ∪ Γ ) |Ip ); 12 while (∅ ∈ (Σ ∪ Γ ) |Ip ) do 13 γ=(ℓ ∨ β) ← analyzeConf lict(Σ ∪ Γ, Ip); 14 j ← level(γ, Ip); 15 if (γ = ∅) then return UNSAT; ← Γ ∪ {γ}; ← Ip ∪ BCP ((Σ ∪ Γ ) |Ip ); 19 Ic ← Ip ∪ (Ic \ Ip);20 else ← chooseLitteralT oF lip(Σ |Ip , Ic); 22 f lip(Ic, ℓ); 23 if (restart()) then 24 Ip ← BCP (Σ ∪ Γ ); 25 Ic ← Ip ∪ completeInterpretation(Σ |Ip ) ;26

Fig. 1 .

 1 Fig. 1. Scatter plot: SATHYS vs. {PRECOSAT,HINOTOS,CLASP,SATZILLA }

Challenge 5 :

 5 Design a practical stochastic local search procedure for proving unsatisfiability; -Challenge 6: Improve stochastic local search on structured problems by efficiently handling variable dependencies; -Challenge 7: Demonstrate the successful combination of stochastic search and systematic search techniques, by the creation of a new algorithm that outperforms the best previous examples of both approaches.

  -SATHYS cdclAtEachLM : instead of using the variable SLSprogress we call the CDCL solver at each local minimum.-SATHYS noP olarity : Literal polarity are not updated with the MAXSAT interpretation.

	solver	Crafted Application Random total
	SATHYS	104	148	189	441
	SATHYS nb	103	144	191	438
	SATHYS cdclAtEachLM 101	141	8	250
	SATHYS noP olarity	106	142	188	436
	Table

Table 3 .

 3 Highlight results on a selection of instances. Results are reported in seconds.

		SAT BEST SATHYS HINOTOS GLUCOSE PRECOSAT CLASP SATZILLA
	q query 3 L100 coli	N	183	677	-	577	414	780	-
	post-c32s-col400-16	N	66	247	380	714	141	66	125
	countbitsarray02 32	N	926	1100	-	926	-	-	-
	maxxororand032	N	579	768	-	-	-	-	-
	minand128	N	16	71	219	26	26	23	212
	rpoc xits 08 UNSAT	N	154	1036	1115	398	159	-	589
	gt-ordering-unsat-gt-060	N	15	171	-	-	149	-	-
	9dlx vliw at b iq3	N	430	1137	-	-	-1095	430
	gss-19-s100	Y	38	641	-	611	-	-	38
	UCG-20-5p1	Y	413	835	-	-	537	-	-
	UTI-15-10p1	Y	392	935	-	392	-	-	1140
	gt-ordering-sat-gt-040	Y	15	6	-	-	149	-	-
	em 9 3 5 exp	Y	18	288	209	51	181	140	276
	ndhf xits 20	Y	1.6	180	-	-	249	-	75
	partial-10-15-s	Y	228	1092	-	-	-	-	-
	vmpc 30	Y	18	825	-	-	292	159	551
	velev-pipe-sat-1.0-b7	Y	14	294	-	-	343	-	87
	new-difficult-21-168-19-90 Y	0.1	141	-	-	-	370	416
	mod3block 3vars 9gates. . . Y	5.7	4.8	-	126	63	26	24
	rbsat-v945c61409g10	Y	21	362	-	898	147	150	933
	instance n8 i9 pp	Y	41	115	454	1117	800	-	421


Gilles Audemard
email: audemard@cril.fr

Jean-Marie Lagniez
email: lagniez@cril.fr

Bertrand Mazure
email: mazure@cril.fr

Lakhdar Saïs
email: sais@cril.fr

On Freezing and Reactivating Learnt Clauses

In this paper, we propose a new dynamic management policy of the learnt clause database in modern SAT solvers. It is based on a dynamic freezing and activation principle of the learnt clauses. At a given search state, using a relevant selection function, it activates the most promising learnt clauses while freezing irrelevant ones. In this way, clauses learned at previous steps can be frozen at the current step and might be activated again in future steps of the search process. Our strategy tries to exploit pieces of information gathered from the past to deduce the relevance of a given clause for the remaining search steps. This policy contrasts with all the well-known deletion strategies, where a given learned clause is definitely eliminated. Experiments on SAT instances taken from the last competitions demonstrate the efficiency of our proposed technique.

Introduction

The SAT problem, i.e. the problem of checking whether a set of Boolean clauses is satisfiable or not, is central to many domains of computer science and artificial intelligence (theorem proving, planning, non-monotonic reasoning, VLSI correctness checking or knowledge-base verification and validation). During the last two decades, SAT has gained considerable audience with the advent of a new generation of SAT solvers that are able to solve large instances encoding real-world applications. These solvers, called CDCL (Conflict Driven, Clause Learning) [START_REF] Moskewicz | Chaff: Engineering an efficient SAT solver[END_REF][START_REF] Een | An extensible SAT-solver[END_REF], are based on a nice combination of (i) clause learning [START_REF] Bayardo | Using csp look-back techniques to solve realworld sat instances[END_REF][START_REF] Marques-Silva | GRASP -A New Search Algorithm for Satisfiability[END_REF][START_REF] Zhang | Efficient conflict driven learning in boolean satisfiability solver[END_REF], (ii) VSIDS heuristics [START_REF] Moskewicz | Chaff: Engineering an efficient SAT solver[END_REF] and (iii) restart policies [START_REF] Gomes | Boosting combinatorial search through randomization[END_REF][START_REF] Huang | The effect of restarts on the efficiency of clause learning[END_REF], enhanced with efficient data structures (eg. Watched literals). On the theoretical side, K. Pipatsrisawat and A. Darwiche [START_REF] Pipatsrisawat | On the power of clause-learning sat solvers with restarts[END_REF] proved that modern SAT solvers formalized as a proof system are equivalent in strength to general resolution, if the search is restarted at each conflict. This result shows that resolution-based clause learning is an important component of modern SAT solvers, since it pushes forward DPLL-like procedures from tree-like to general resolution, a more powerful proof system. On the practical side, as the set of clauses that can be derived from conflicts is of exponential size in the worst case, several strategies have been designed to cope with this combinatorial explosion problem. To maintain a learnt clause database of polynomial size -and consequently perform unit propagation with reasonable cost -all these strategies dynamically reduce the learnt database by deleting clauses considered to be irrelevant to the next search steps. The most popular strategy considers a learnt clause as irrelevant if its activity or its involvement in recent conflict analysis is marginal. In [START_REF] Audemard | Predicting learnt clauses quality in modern SAT solvers[END_REF], a static measure called literal block distance (LBD, corresponding to the number of different levels involved in a given learnt clause) is used to quantify the quality of learnt clauses. Clauses with smaller LBD are considered as more relevant. Theoretically, the first unique implication point (UIP) scheme is shown to be optimal among schemes that learn an asserting clause in terms of LBD measure [START_REF] Audemard | A Generalized Framework for Conflitcs Analysis[END_REF]. The main drawback of these cleaning strategies is that they cannot avoid the elimination of relevant learnt clauses. Their irreversible elimination makes it possible that the same clause will be derived reapeatedly.

The problem of determining what is a useful learnt clause in advance remains very challenging and computationally hard. In this paper, we propose a new dynamic management policy of the learnt clause database in modern SAT solvers. It is based on a dynamic freezing and activation principle of the learnt clauses. At a given search state, it activates the most promising learnt clauses while freezing irrelevant ones. In this way, previously learned clauses can be discarded for the current step, but may be activated again in future steps of the search process. Our policy tries to exploit pieces of information gathered from the past to deduce the relevance of a given clause for the remaining search steps. This policy contrasts with all well-known deletion strategies, where a given learned clause is definitely eliminated. In this way, a clause can be useless at a given step and relevant at another step of the search process. The ideal is to freeze a learnt clause when it is not used and just to reactivate it at the time when it could play a role in the proof.

The next part of the paper is organized as follows: section 2 introduces necessary background. In section 3, we introduce a new relevance measure of learnt clauses, whereas in section 4, we present our dynamic freezing and activation strategy of learnt clauses. Before concluding, we present in section 5, an experimental comparison of our new dynamic learnt clauses management policy with the well known state-of-the-art reduction policies as well as state of the art solvers.

Definitions, notations and technical background

In this section, after some preliminary definitions and notations, we introduce the most salient computational features of modern SAT solvers.

A CNF formula Σ is a conjunction (interpreted as a set) of clauses, where a clause is a disjunction (interpreted as a set) of literals. A literal is a positive (x) or negative (¬x) Boolean variable. The two literals x and ¬x are called complementary. A unit clause is a clause with only one literal (called unit literal). An empty clause, is interpreted as false, while an empty CNF formula, is interpreted as true. A set of literals is complete if it contains one literal for each variable occurring in Σ and fundamental if it does not contain complementary literals. An interpretation I of a boolean formula Σ associates a value I(x) to some of the variables x appearing in Σ. An interpretation can be represented by a fundamental set of literals, in the obvious way. A model of a formula Σ is an interpretation I that satisfies the formula, i.e. that satisfies all clauses of the formula. Finally, SAT is the problem of deciding whether a given CNF formula Σ admits a model Let us now briefly describe the basic components of CDCL based SAT solvers [START_REF] Moskewicz | Chaff: Engineering an efficient SAT solver[END_REF][START_REF] Een | An extensible SAT-solver[END_REF]. To be exhaustive, these solvers incorporate unit propagation (enhanced by efficient and lazy data structures), variable activity based heuristic, literal polarity phase, clause learning, restarts and a learnt clause database reduction policy.

These main components are depicted by the general scheme given in Algorithm 1. At each step of the main loop, the algorithm performs unit propagation (line 3). In case of conflict (lines 4-8), a new asserting clause is derived by conflict analysis (line 4). If such a clause is empty, then the formula is answered unsatisfiable, otherwise it is added to the learnt clause database (line 5). If it is not time to restart, the algorithm backjumps to the assertion level of the learnt clause, i.e. the level where the learnt clause becomes unit (line 8), otherwise it backjumps to the root of the search. When the formula is closed under unit propagation without generating the empty clause, a new decision literal -if it exists -is selected and asserted in a new decision level (line 11), otherwise a model is found and the formula is answered to be satisfiable (line 10).

Finally, when it is time to reduce, the learnt clause database is cleaned (line 12). This component, usually omitted in the description of CDCL solvers, is clearly crucial to the solvers' performance. Indeed, keeping too many learnt clauses will slow down the unit propagation process, while deleting too many of them will break the overall learning benefit. Consequently, identifying good learnt clauses -relevant to the proof derivation -is clearly an important challenge. The first proposed quality measure follows the success of the activity based VSIDS heuristic. More precisely, a learnt clause is considered relevant to the proof, if it is involved more often in recent conflicts, i.e. usually used to derive asserting clauses. Clearly, this deletion strategy supposes that a useful clause in the past could be useful in the future. More recently, a more accurate measure called LBD is used to estimate the quality of a learnt clause leading to a better cleaning strategy than the previous one [START_REF] Audemard | Predicting learnt clauses quality in modern SAT solvers[END_REF]. This new measure is based on the number of different decision levels appearing in a learnt clause and is computed when the clause is learnt. Extensive experiments demonstrates that clauses with small LBD values are used more often than those with higher LBD ones.

Another feature of CDCL solvers recently proposed in [START_REF] Pipatsrisawat | A lightweight component caching scheme for satisfiability solvers[END_REF] concerns the literal polarity to be chosen when the next decision variable is selected thanks to the VSIDS heuristic. Usually, a default polarity (e.g. false) is defined and used each time a decision literal is assigned. Based on the observation that restarts and backjumping might lead to repetitive solving of same subformulas, Pipatsrisawat and Darwiche [START_REF] Pipatsrisawat | A lightweight component caching scheme for satisfiability solvers[END_REF] proposed to dynamically save for each variable the last used polarity. This literal polarity based heuristic, called progress saving, prevents the solver from solving the same satisfiable subformulas several times. These memorized polarities can be represented as a complete interpretation P. Each time a decision variable is chosen, its assignment polarity is selected from P. Consequently, P gives us at least the polarities of the decision literals. And each time a literal is assigned by the solver, its associated polarity is set in P.

In the next section, we exploit P (progress saving) to approximate the usefulness that one can expect in the near future from a learnt clause, in other words to measure the likelihood for a given clause to be part of the implication graph.

A new measure for identifying relevant learnt clauses

As mentioned above a CDCL-based SAT solver can be formulated as a resolution proof system [START_REF] Pipatsrisawat | On the power of clause-learning sat solvers with restarts[END_REF][START_REF] Beame | Towards understanding and harnessing the potential of clause learning[END_REF]. In practice, the main problem behind resolution-based techniques arises from their exponential space complexity. Consequently, the practical incarnation of modern SAT solvers can be seen as a resolution-based procedure with a deletion strategy. As a consequence, the completeness of modern SAT solvers is heavily connected to both the chosen deletion and restart policies. For example, if we use a restart with a static cutoff value and an aggressive deletion strategy, we cannot guarantee the completeness of the solver. For this reason one needs to be careful when designing a deletion strategy. Consequently, defining what is a relevant clause before completing the proof itself is of a great importance for the efficiency of the solver. However answering such a question is computationally hard and it is related to finding a proof of minimal size.

In this section we define a simple measure to identify the relevance of a given learnt clause and we experimentally show its effectiveness. Our measure is based on the progress saving polarity [START_REF] Pipatsrisawat | A lightweight component caching scheme for satisfiability solvers[END_REF] introduced in the previous section. This progress saving based quality measure, in short psm, is defined as follows: given a clause c and a complete set of literals P representing the current set of saved literals polarities, we define psm P (c) = |P ∩c|. This measure can be related to another one proposed in [START_REF] Moskewicz | Chaff: Engineering an efficient SAT solver[END_REF]. In this paper, a learnt clause was tagged useless, in the goal to delete it, if its number of unassigned literals has reached a predefined threshold.

First let us note that the psm measure is highly dynamic. Since the set P of saved literals polarities will evolve during search, the psm of a given clause will also evolve consequently. For example, when a clause is learnt, its psm value is equal to zero and becomes one after backjumping to the assertion level. It is also important to note that when a given learnt clause is at the origin of unit propagation, its psm value is also equal to one. These preliminary remarks suggest that clauses with small psm value are the most relevant to the near future of the search. Let I be the current partial interpretation and P be the current complete interpretation representing the current saved literals polarities, and c a learnt clause. As I ⊂ P, psm P (c) represents the number of literals that are assigned to true by I or that would be assigned to true by P\I. Consequently, a clause with a small psm value has a lot of chance to be unit propagated or to be falsified. On the contrary, a clause with a big psm value has a lot of chance to be satisfied by more than one literal and then to be irrelevant for the subsequent part of the search.

To analyze and to validate this assumption, experiments are conducted on some SAT instances. Figure 1 shows, for a sample of instances, the average number of times clauses with a given psm value are used during the unit propagation process. In this experiment, we consider a time sequence t k with k > 0 (the search starts at t 0 ) corresponding to the successive steps of the search where the learnt database is classically reduced. Let P t k and P t k+1 be the progress saving literal polarities at the steps t k and t k+1 respectively. Let us consider the time window between t k and t k+1 , when a given clause c from the learnt database is used for unit propagation, we compute psm = psm Pt k (c) and then α(psm) the number of times a clause with such psm value is used for propagation is increased by one. The average number of times a clause with a given psm value (x-axis) is used in unit propagation (y-axis), corresponds to α(psm) divided by the total number of times a learnt database is reduced.

As we can observe from Figure 1, learnt clauses with small psm value are used more often in the unit propagation process than those with higher psm value. If we look closer, we can see that the most used clauses are those with psm value around 10. Based on extensive experiments, we observed that on the majority of instances the distribution of psm values looks like those represented in the two upper curves of Figure 1.

This first experiment illustrates the relevance of clauses with small psm value. To compare it with previous learnt clauses quality measure, we integrate our psm measure to the learnt clauses reduction policy (clean(∆) -line 12) of MINISAT 2.2 which is the latest version of the well known solver MINISAT [START_REF] Een | An extensible SAT-solver[END_REF]. Similarly to previous approaches, each time a reduction is performed, the set of clauses is sorted according to the increasing order of psm value. When two clauses admit the same psm value, the one with the greatest activity (VSIDS) is preferred. Then the learnt database is reduced by half. Like other strategies, we keep the binary clauses in the learnt database.

In the sequel, all our experiments are conducted on a Quad-core Intel XEON X5550 with 32Gb of memory, using the 292 application instances of the SAT 2009 competition. The CPU time limit is set to 900 seconds.

For each solver, we indicate the number of solved instances (#Solved) with the number of satisfiable (#SAT) and unsatisfiable instances (#UNSAT) in brackets. We also give the average time in seconds (avg time) necessary to solve these instances.

Table 1 summarises the results obtained by MINISAT d [START_REF] Een | An extensible SAT-solver[END_REF], MINISAT d + LBD [START_REF] Audemard | Predicting learnt clauses quality in modern SAT solvers[END_REF] and MINISAT d +psm using the default time sequence (noted MINISAT d ) of MINISAT. As we can see, MINISAT d + psm obtains the best overall results and is the best on satisfiable instances. This first experiment shows the efficiency of our new measure psm using the default time reduction sequence of MINISAT. To make a fair comparison between these three approaches, we also present in Table 2 the results obtained using an aggressive cleaning policy as presented in [START_REF] Audemard | Predicting learnt clauses quality in modern SAT solvers[END_REF] (noted MINISAT a ). In this experiment the learnt database ∆ is reduced using the following time sequence, t 0 = 4000 conflicts and t k = t k-1 +300 conflicts for k > 0. Using aggressive (more frequent) cleaning time sequence, the result obtained by the LBD measure are better than those obtained by VSIDS like criterion and the psm measure.

As a summary, considering the classical reduction and deletion strategies, these first experiments clearly show that our measure is competitive with the two other wellknown measures using both aggressive and less aggressive cleaning policy. This measure will be used in next section in order to design a dynamic managment policy of learnt clauses.

Freeze and reactivate: a dynamic management policy

In section 3, we defined a new measure based on progress saving [START_REF] Pipatsrisawat | A lightweight component caching scheme for satisfiability solvers[END_REF] for identifying relevant learnt clauses. In this section, we describe our dynamic management policy of the learnt clause database. Our proposed framework is based on two important key points. First, the progress saving based measure is highly dynamic and evolves during search. Consequently, a clause might be considered irrelevant (high psm value) at a given step of the search and could become relevant (small psm value) in the future steps of the search. Secondly, determining if a given learnt clause will be involved again in the resolution proof is a computationally hard task. All the well-known management policies are not safe from regularly eliminating relevant learnt clauses. For both reasons, our proposed approach introduces an additional and new concept of frozen learnt clauses. A learnt clause considered as irrelevant at a given step can be frozen and reactivated when it is considered as useful again. More precisely, freezing (respectively activating) a clause means that the clause is disconnected (respectively attached) to the learnt database, and then it is not used during the search (respectively used).

This kind of management strategy cannot be defined using the other known measures such as activity and LBD-based ones. Indeed, the LBD value of a given clause is definitely set at the time of its generation and does not change during search, while the activity (VSIDS-based) measure is dynamic but can only be used to update the activity of learnt clauses currently in the database.

Let us now formally describe our new learnt clause management policy. First, as the psm value of a given clause is highly dynamic, we introduce a notion of deviation between two successive sets of progress saving polarities. Let V t k be the set of variables assigned by the solver between two consecutive time sequences (as defined in previous section) t k-1 and t k . The deviation d t k is defined as follows:

d t k = h(Pt k ,Pt k-1 ) |Vt k |
, where h is the usual hamming distance.

This deviation defined as a normalized hamming distance, gives us an outline of the evolution of progress saving polarities between two successive cleanings of the learnt database. A deviation tending to zero indicates that the solver explores around the same part of the search space whereas a value close to one indicates that the solver explores different part of the search space. To obtain a more precise view of the search behavior, we introduce another notion of minimal deviation d m t k = min{d ti |0 ≤ i ≤ k} at time step t k . Using this minimal deviation, we can now refine our psm measure. Indeed, let c be a clause to be evaluated at time step t k , if psm Pt k (c) > d m t k × |c| then the clause c is likely to be satisfied in a near future, otherwise it is likely to be involved in the propagation process.

Our approach depicted in Figure 2 is represented as a state diagram. At each cleaning t k , learnt clauses can move from a state to another one following some conditions.

First, a learnt clause c can be in one of the three following states:

1. Active state A: c is active and watched. 2. Frozen state F: c is frozen i.e. c is not watched 3. Dead state D: c is deleted.

Let us describe these different transitions:

-Each time a clause is learnt it enters the state A.

-A clause c ∈ A with a short LBD (lbd(c) ≤ 3 in the figure) remains in the state A until the end of the search process.

-A clause c ∈ A such that psm P t k (c) |c| > d m t k enters the frozen state F. -A clause c ∈ F such that psm Sn i (c) |c| ≤ d m ni enters the active state A.
-A clause c ∈ F not activated after k time steps is deleted. Similarly, a clause c ∈ A remaining active more than k steps without participating to the search is also deleted. In both cases, it enters the state D after k = 7 time steps in our experiments.

One of the main advantages of our approach comes from the fact that we can perform frequent cleaning of the learnt clause database without taking care of removing relevant clauses. So we choose a very aggressive policy. We set t 0 = 500 conflicts, and t k = t k-1 + 100 conflicts. We conducted some experiments to analyse the transfer of the clauses from the state A to the state F and vice versa. Figure 3 shows, for the same sample of instances as in the Figure 1, the number of deleted clauses, the number of transitions to the frozen state, the number of transitions to the active state, the number of active (or watched) learnt clauses and finally the number of frozen clauses. These data are represented by the y-axis, whereas the x-axis represents the cleaning operated at the time step t k . For clarity reasons, all curves have been smoothed. For all instances, the number of frozen clauses (F rozen) and the number of active clauses (Active) are relatively similar. The curve representing the number of clauses becoming active (F → A) is dominated by those representing the number of clauses becoming frozen (A → F). However, the two curves evolve similarly and they are closer on some instances (e.g. q query 3 l48 lambda) than on others (e.g. Aprove07 -25) . Finally, we can also observe that, at each cleaning time step, some clauses are definitively deleted (Dead). This section is divided in two parts. In the first, we compare our dynamic management policy (psm dym ) against the classical reduction approach with different quality measures (LBD, VSIDS like, psm). In the second experiment, we compare it with three state-of-the-art solvers: GLUCOSE which embeds LBD measure, a dynamic restart policy and some other features [START_REF] Audemard | Predicting learnt clauses quality in modern SAT solvers[END_REF], LINGELING which also embeds more powerful reasoning like blocked clause elimination [START_REF] Järvisalo | Blocked clause elimination[END_REF], and finally, CRYPTOMINISAT which adds many other features (e.g. vivification, reasoning on xor clauses. . . ). Descriptions of these solvers are available on the SATRACE 2010 website http://baldur.iti.uka. de/sat-race-2010. Except for LINGELING and CRYPTOMINISAT which embed preprocessing inside, the other solvers use SatElite for preprocessing [START_REF] Eén | Effective preprocessing in SAT through variable and clause elimination[END_REF].

In the first experiment, we use the same solver and the only difference is in the learnt clause management policy. In the second experiment, our aim is to compare our learnt clause management approach integrated in MINISAT 2.2 (MINISAT-psm dyn ) with the state-of-the-art SAT solvers. Source code and extensive experiments can be found at http://www.cril.fr/˜lagniez/ressource.html.

Comparison with different quality measures

We compare our dynamic policy, called MINISAT-psm dyn with the classic MINISAT, and MINISAT with learnt database reduction based on psm (MINISAT-psm) and on LBD (MINISAT-LBD) (like in section 3). Figure 4 summarizes the results. It contains three scatter plots corresponding to the comparison of MINISAT-psm dyn with the 3 others solvers. In such a plot, each dot corresponds to a given instance, the x-axis corresponds to the cpu time needed by the MINISAT, LBD or psm to solve the instance, whereas they axis corresponds to the cpu time needed by psm dyn to solve it. So, dots below the diagonal correspond to instances solved faster by MINISAT-psm dyn (SAT and UNSAT instances are differentiated). Figure 4 also contains a cactus plot related to the comparison of the 4 solvers.

It is quite clear that our freezing strategy outperforms the other strategies. It solves 189 instances (76 SAT and 113 UNSAT), which is significantly better than the other solvers (see Table 1). Furthermore, as we can see on the scatter plots, MINISAT-psm dyn solves instances faster than the others solvers.

Comparison with state of the art solvers

Conclusion

In this paper, we introduced a new measure for identifying relevant learnt clauses. The main advantage of this measure is that it is dynamic (unlike the LBD measure) and it can be computed even if clauses do not participate in the search process (unlike the VSIDS like measure). Thanks to this property, a new learnt clause database management framework has been proposed. It exploits a novel dynamic policy that activates the most promising learnt clauses while freezing irrelevant ones. This is in contrast with all the well-known deletion strategies, where a given learned clause is definitely eliminated. Experiments on SAT instances taken from the last competitions demonstrate the effectiveness of our approach.

As future work, we plan to exploit the evolution of the set of progress saving literal polarities in order to decide if cleaning has to be performed. Considering the connection GLUCOSE vs psm dyn LINGELING vs psm dyn between restarts and clause learning [START_REF] Pipatsrisawat | Width-based restart policies for clause-learning satisfiability solvers[END_REF], we plan to exploit this connection to improve our proposed leant database management approach.

Aknowledgements We would like to thank the anonymous reviewers for insightful comments

Fig. 1 .

 1 Fig. 1. Progress saving measure / relevance with respect to UP

Fig. 2 .

 2 Fig. 2. State diagram of a learnt clause.

Fig. 3 .

 3 Fig. 3. Evolution of the number of clauses in different states and number of state transfers

Figure 5 Fig. 4 .

 54 Figure 5 summarizes the comparison with state of the art solvers. It is structured as figure 4. Let us detail the number of solved instances by each solver: LINGELING solves 187 instances (77 SAT, 110 UNSAT), GLUCOSE 189 (70 SAT and 119 UNSAT) and CRYP-TOMINISAT 194 (74 SAT, 120 UNSAT).These results and the plots of Figure5show that our dynamic management policy is really competitive with state-of-the-art solvers (remember, it solves 189 instances (76 SAT and 113 UNSAT)). It does not even embed sophisticated components such as dynamic restart, etc.

Fig. 5 .

 5 Fig. 5. Comparison with state of the art solvers: GLUCOSE, LINGELING and CRYPTOMINISAT.

Table 1 .

 1 Results with the MINISAT default time cleaning sequence.

	Solver		#Solved (#SAT-#UNSAT) avg time
	MINISAT	d	174 (68 -106)	142
	MINISAT	d + psm 177 (73 -104)	130
	MINISAT	d + LBD 173 (71 -102 )	132
	Solver		#Solved (#SAT-#UNSAT) avg time
	MINISAT	a	162 (68 -94)	136
	MINISAT	a + psm 163 (70 -93)	140
	MINISAT	a + LBD 168 (72 -96)	128

Table 2 .

 2 Results with an aggressive time cleaning sequence.

⋆ This work is (partially) supported by ANR UNLOC project: ANR 08-BLAN-0289-01.