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

Bertrand Mazure
email: mazure@cril.fr

Lakhdar Saïs
email: sais@cril.fr

Lj-2}

Local autarkies searching for the dynamic partition of CNF formulae

In this paper an original dynamic partition of formulae in Conjunctive Normal Form (CNF) is presented. It is based on the autarky concept first introduced by Monien and Speckenmeyer and further investigated by Kullmann and Van Gelder. Intuitively, an autarky is a partial assignment satisfying some clauses while not affecting any literal in any other clause, leading to a partition of the CNF formula. Autarkies can play a dramatic role in the efficiency of modern SAT solvers. The approach in this paper aims to dynamically extend the current partial assignment to a local autarky thanks to an inference rule based on unit propagation. More precisely, at each node of the search tree, it is checked whether the current decision literal can be made monotone by subsuming all the clauses where it appears negatively. The formal framework is detailed and its technical features discussed.

Introduction

The SAT problem, i.e., the problem of checking whether a set of Boolean clauses is satisfiable or not, is central in many computer science and artificial intelligence domains, including e.g. constraint satisfaction problems (CSP), planning, non-monotonic reasoning and VLSI correctness checking. Today, SAT has gained a considerable audience with the advent of a new generation of SAT solvers able to solve large complex instances encoding real-world applications. These solvers also appear to provide crucial base-building blocks for various other problem-solving technologies, like SMT solving, theorem proving, model finding and QBF solving.

These solvers, called 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 the standard unit propagation technique [START_REF] Davis | A machine program for theorem-proving[END_REF] combined in a smart way with efficient data structures, together 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] Brisoux | Improving backtrack search for SAT by means of redundancy[END_REF][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][START_REF] Bayardo | Using CSP look-back techniques to solve real-world SAT instances[END_REF][START_REF] Moskewicz | Chaff: Engineering an efficient SAT solver[END_REF]. Modern SAT solvers can be interpreted as extended versions of the well-known DPLL-like (short for Davis, Putnam, Logemann and Loveland) procedure augmented with these various enhancements. Let us stress that the well-known resolution rule still plays a dramatic role in the efficiency of modern SAT solvers which can be understood as a particular form of general resolution [START_REF] Beame | Understanding the power of clause learning[END_REF]. These lookback-based SAT solvers are particularly efficient on SAT instances encoding practical applications. Other lookahead-based SAT solvers are designed using efficient local processing techniques and variable branching heuristics (e.g. Satz [START_REF] Chu | Heuristics based on unit propagation for satisfiability problems[END_REF], kcnfs [START_REF] Dubois | A backbone-search heuristic for efficient solving of hard 3-SAT formulae[END_REF], March-DL [START_REF] Marijn | March dl: Adding adaptive heuristics and a new branching strategy[END_REF]). This last family of solvers are particularly efficient on random and crafted SAT instances.

The recent dramatic breakthrough in solving complex industrial SAT instances can often be related to the presence of hidden structures exploited in a smart way by the SAT solvers. Indeed, such instances are very suitable for decomposition-based techniques. However, most of the decomposition techniques are much time consuming. Light divide-and-conquer approaches have been proposed previously, using for example structure-based variable ordering heuristics to recursively decompose the SAT instances [START_REF] Huang | A structure-based variable ordering heuristic for SAT[END_REF]. In [START_REF] Li | Guiding real-world SAT solving with dynamic hypergraph separator decomposition[END_REF], a dynamic decomposition method based on hypergraph separators is proposed. The authors give a nice integration of the separator decomposition into variable ordering of a modern SAT solver that speedups the search on real-world SAT instances. Other approaches are based on the exploitation of autarky assignments originally proposed by Monien and Speckenmeyer [START_REF] Monien | Solving satisfiability in less than 2 n steps[END_REF] and further investigated by Kullmann [START_REF] Kullmann | Investigations on autark assignments[END_REF] and Van Gelder [START_REF] Van Gelder | Autarky pruning in propositional model elimination reduces failure redundancy[END_REF]. More recently, Liffton and Sakallah [START_REF] Mark | Searching for autarkies to trim unsatisfiable clause sets[END_REF] proposed a novel algorithm that searches for autarkies directly using a standard satisability solver and explore the potential of trimming autarkies in minimal unsatisable subsets (MUS) and minimal correction subsets (MCS) extraction flows. Let us stress that the dynamic exploitation of autarkies assignments in DPLLlike search procedures actually goes back to Oxusoff's and Rauzy's work [START_REF] Oxusoff | L'évaluation sémantique en calcul propositionnel[END_REF]. In their paper, these latter authors pro-posed several variable branching heuristics to dynamically partition the CNF formula into disjoint sets of clauses. More precisely, the proposed variable ordering heuristics aim to partition the formula: the next variable to assign is selected in such a way that its assignment leads to a new sub-formula included in previous ones at the same branch of the tree. The approach that will be presented in this paper follows this idea but is heuristic-independent. More precisely, let x be the next variable to assign, the proposed approach tries to subsume the clauses where ¬x appears and then deduce that such a literal is monotone 1 . This clearly extends the local autarky assignments, using subclause deduction. Indeed, a partial assignment that is not a local autarky can be transformed into a local autarky.

The paper is organized as follows. After some preliminary definitions and notations, basic and local autarkies, Oxusoff's and Rauzy's dynamic approach are described in section 3. Then our generalized local autarkies are formally presented in section 4. Finally, we conclude by introducing several promising perspectives opened by this framework.

Technical background

Preliminary definitions and notations

A CNF formula Σ is a set (interpreted conjunctively) of clauses, where a clause is a disjunction of literals. A literal is a positive (x) or negated (¬x) propositional variable. The two literals x and ¬x are called complementary. We note by l the complementary literal of l. For a set of literals L, L is defined as { l | l ∈ L}. A unit clause is a clause containing only one literal (called unit literal), while a binary clause contains exactly two literals. The empty clause, noted ⊥, is interpreted as f alse (unsatisfiable), whereas the empty CNF formula, noted ⊤, is interpreted as true (satisfiable). We define the size |Σ| of a CNF formula Σ as c∈Σ |c|, where |c| is the number of literals in c. The number of clauses in Σ is denoted C Σ .

The set of variables occurring in Σ is noted V Σ . A set of literals is complete if it contains one literal for each variable in V Σ , and fundamental if it does not contain complementary literals. An assignment ρ of a Boolean formula Σ is a function that associates a value ρ(x) ∈ {f alse, true} to some of the variables x ∈ V Σ . ρ is complete if it assigns a value to every x ∈ V Σ , and partial otherwise. An assignment is alternatively represented by a fundamental set of literals, in the obvious way. A model of a formula Σ is an assignment ρ that makes the formula true; noted ρ Σ.

The following notations will also be used throughout the paper:

1 A monotone literal is a literal that occurs either positively or negatively in the CNF formula (but not in both polarities).

• Σ| x will denote the formula obtained from Σ by assigning x the truth-value true. Formally Σ|

x = {c | c ∈ Σ, {x, ¬x} ∩ c = ∅} ∪ {c\{¬x} | c ∈ Σ, ¬x

DPLL search

DPLL [START_REF] Davis | A machine program for theorem-proving[END_REF] is a tree-based backtrack search procedure; at each node of the search tree, the assigned literals (both the decision literal and the propagated ones) are labeled with the same decision level starting from 1 and increased at each decision (or branching). After backtracking, some variables are unassigned, and the current decision level is decreased accordingly. At the ith level, the current partial assignment ρ can be represented as a sequence of decision-propagation steps of the form (x i k ), x i k1 , x i k2 , . . . , x i kn k where the first literal x i k corresponds to the decision literal x k assigned at the ith level and each x i kj for 1 ≤ j ≤ n k represents unit propagated literals at the ith level. Let x ∈ ρ, we note δ(x) the assignment level of x.

Autarky assignments

The autarky concept has been introduced in [START_REF] Monien | Solving satisfiability in less than 2 n steps[END_REF]. Definition 1 Let Σ be a CNF formula and ρ a partial assignment. ρ is an autarky if

Σ| ρ ⊆ Σ i.e. ∀c ∈ Σ, ρ ∩ c = ∅ or ρ ∩ c = ∅.
For a CNF formula, computing an autarky when it exists is clearly (F)NP-complete. However, autarkies can be used to improve the efficiency of SAT solvers [START_REF] Van Gelder | Autarky pruning in propositional model elimination reduces failure redundancy[END_REF][START_REF] Kullmann | Investigations on autark assignments[END_REF]. Indeed, the refutation of Σ| ρ leads to the proof of the unsatisfiability of Σ. Following definition 1, the property prop:inclusion can be obtained.

Property 1 If ρ is an autarky of the CNF formula

Σ then Σ Σ| ρ . 2nd inclusion between Σ and Σ|{l 1 ,¬l2,l3,l4} 1st inclusion between Σ|{l 1 } et Σ|{l 1 ,¬l2,l3} Σ is proved unsatisfiable Σ Σ|l 1 l1 ⊥ l2 Σ|{l 1 ,¬l2} ¬l2 Σ|{l 1 ,¬l2,l3} l3 Σ|{l 1,¬l2,l3,l4} l4 Σ|{l 1,¬l2,l3,l4,l5} l5 ⊥ l6 ⊥ ¬l6 Σ|{l 1,¬l2,l3,l4,¬l5}

DPLL search tree and local autarkies

In [START_REF] Jeannicot | évaluation sémantique en calcul propositionnel : une propriété de coupure pour rendre plus efficace la procédure de davis et putnam[END_REF][START_REF] Oxusoff | L'évaluation sémantique en calcul propositionnel[END_REF] the authors exploit this property to prune the search tree of DPLL-like procedures. To this end, a local autarky concept is defined and exploited.

Definition 2 A partial assignment ρ = {l 0 , . . . , l i } of a CNF formula Σ is a local autarky if ∃ρ ′ = {l 0 , . . . , l j } with j < i such that Σ| ρ ⊆ Σ| ρ ′ .
Property 1 also applies for local autarkies. Indeed, from Definition 2 and Property 1, Σ| ρ ′ Σ| ρ can be deduced. This can be used to prune the search tree of the DPLL algorithm. Indeed, if ρ is a local autarky with respect to the partial assignment ρ ′ then Σ| ρ ′ is satisfiable if and only if Σ| ρ is satisfiable. All branches not explored between ρ ′ and ρ can be pruned if Σ ρ is proved unsatisfiable.

The following example illustrates this property.

Example 1 Let Σ = {(l 1 ∨ l 2 ∨ ¬l 4 ), (¬l 1 ∨ l 4 ), (¬l 1 ∨ l 2 ∨ l 3
), (¬l 2 ), (l 5 ∨ l 6 ), (l 5 ∨ ¬l 6 ), (¬l 5 ∨ l 6 ), (¬l 5 ∨ ¬l 6 )}.

The search tree of the DPLL algorithm represented in Figure 1 is obtained thanks to the exploitation of local autarkies. This corresponds to the application of the local autarky pruning rule as defined by Jeannicot et al. in [10]. In the following example, the unit and monotone literals propagated during search are not mentioned for clarity reasons.

From the search tree, the following formulae associated to the different nodes are obtained:

• Σ| {l1} = {(l 4 ), (l 2 ∨ l 3 ), (¬l 2 ), (l 5 ∨ l 6 ), (l 5 ∨ ¬l 6 ), (¬l 5 ∨ l 6 ), (¬l 5 ∨ ¬l 6 )}
• Σ| {l1,¬l2} = {(l 4 ), (l 3 ), (l 5 ∨ l 6 ), (l 5 ∨ ¬l 6 ), (¬l 5 ∨ l 6 ), (¬l 5 ∨ ¬l 6 )}

• Σ| {l1,¬l2,l3} = {(l 4 ), (l 5 ∨ l 6 ), (l 5 ∨ ¬l 6 ), (¬l 5 ∨ l 6 ), (¬l 5 ∨ ¬l 6 )}

• Σ| {l1,¬l2,l3,l4} = {(l 5 ∨l 6 ), (l 5 ∨¬l 6 ), (¬l 5 ∨l 6 ), (¬l 5 ∨ ¬l 6 )}

• Σ| {l1,¬l2,l3,l4,l5} = {(l 6 ), (¬l 6 )}

• Σ| {l1,¬l2,l3,l4,¬l5} = {(l 6 ), (¬l 6 )}

Consequently, the following inclusion holds:

Σ| {l1,¬l2,l3} ⊂ Σ| {l1,¬l2} Σ| {l1,¬l2,l3} ⊂ Σ| {l1}
First application of pruning rules of local autarky

Σ| {l1,¬l2,l3,l4} ⊂ Σ| {l1,¬l2,l3} Σ| {l1,¬l2,l3,l4} ⊂ Σ| {l1,¬l2} Σ| {l1,¬l2,l3,l4} ⊂ Σ| {l1} Σ| {l1,¬l2,l3,l4} ⊂ Σ    

Second application of pruning rules of local autarky

Clearly, the local autarky pruning rule is a generalization of the monotone literal pruning one. Indeed, if l is a monotone literal, then Σ| l is the formula obtained from Σ where all clauses containing l are removed. In consequence Σ| l ⊂ Σ and {l} is a local autarky for Σ. Using the pruning rule based on local autarky allows the simplification by means of the monotone literal rule. Let us note that monotone literals are not exploited in modern SAT solvers that exploit lazy data structures like watched literals. In other words, the occurrence number of a given literal at each node of the search tree is not recorded or updated.

At a given level i of the search tree, finding the smallest level j < i such that Σ| {l0,...,li} is included in Σ| {x0,x1,...,xj } is computationally hard. However the following property allows an incremental detection that ensures the best pruning.

Property 2 ([20])

If Σ| {l0,...,li} ⊆ Σ| {l0,...,lj } with j < i, then Σ| {l0,...,li} is also included in Σ| {l0,...,xj+1} , Σ| {l0,...,lj+2} , . . . , and Σ| {l0,...,li-1} .

To avoid useless inclusion tests, it is more convenient to use the following corollary.

Corollary 1 If Σ| {l0,...,li} ⊂ Σ| {l0,...,lj } , then Σ| {l0,...,li} is not included in all the following formulas: Σ| {l0,...,lj-1} , Σ| {l0,...,lj-2} , . . . , Σ| {l0} and Σ.

The efficiency of the detection of the greatest value ij, called a partition, depends only on the efficiency of the inclusion test between two formulas associated to two consecutive nodes in the current branch of the search tree. This test can be performed efficiently using adapted data structures.

Finally, to ensure that all inclusions are detected, it is necessary to remove subsumed clauses during the DPLL procedure, as illustrated by the following example.

Example 2 Let Σ = {(¬l 1 ∨ l 3 ), (l 2 ∨ l 4 ), (¬l 2 ∨ l 3 ∨ l 4 )},
and

Σ| {l1} = {(l 3 ), (l 2 ∨ l 4 ), (¬l 2 ∨ l 3 ∨ l 4 )} Σ| {l1,l2} = {(l 3 ), (l 3 ∨ l 4 )}
In this case no inclusion is detected. But if the subsumed clauses are removed from Σ| {l1,l2} , then Σ| {l1,l2} = {(l 3 )} ⊂ Σ| {l1} .

The subsumption test can be achieved efficiently using for example the recent approach by Lintao Zhang [START_REF] Zhang | On subsumption removal and on-the-fly CNF simplification[END_REF].

In the next section, a generalization of the (local) autarky assignments is introduced.

Generalized (local) autarky

The generalization is obtained by substituting the syntactical inclusion operation (⊂) by the semantic logical consequence relationship ( ) in Definitions 1 and 2.

Proposition 1 (Generalized (local) autarky) Let Σ be a CNF formula, ρ = {l 0 , . . . , l j , . . . , l i } is a generalized local autarky if there exists ρ ′ = {l 0 , . . . , l j } such that

Σ| ρ ′ Σ| ρ . If ρ ′ = ∅ then ρ is a generalized autarky.
This is clearly a generalization of the previous concept, because if Ω ⊂ Σ then Σ Ω while the converse is false, as illustrated by the following example.

Example 3 Let Σ = {(a ∨ b ∨ c), (¬a ∨ b)} and Ω = Σ| ¬a = {(b ∨ c)}, clearly Σ Ω but Ω ⊂ Σ.
The most important feature of local autarkies is the incremental detection which ensures the greatest inclusion or partition (see Property 2). This property is preserved for the generalized autarky assignments.

Property 3 If Σ| {l0,...,lj } Σ| {l0,...,lj ,...,li} , then Σ| {l0,...,lj ,...,li} is a logical consequence of all the following formulae: Σ| {l0,...,lj+1} , Σ| {l0,...,lj+2} , . . . and Σ| {l0,...,li-1} .

As before, the following corollary avoids useless logical consequence tests (CoNP-Complete) in order to compute the greatest partition.

Corollary 2 If Σ| {l0,...,lj } Σ| {l0,...,lj ,...,li} , then Σ| {l0,...,li} is not a logical consequence of the following formulae: Σ| {l0,...,lj-1} , Σ| {l0,...,lj-2} , . . . , Σ| {l0} and Σ.

We have seen that the propagation of monotone literals is a special case of the local autarky detection. The following property shows that the classical unit propagation is also a special case of the generalized local autarkies.

Property 4

Let Σ be a CNF formula and l a literal occurring in a unit clause of Σ, we have Σ Σ| {l} .

By extension, it can be shown that:

Corollary 3 Let Σ a CNF formula, Σ Σ * .
More generally, if Σ l with l a literal of the CNF formula Σ, then Σ Σ| {l} . This means that the detection of generalized local autarkies includes the propagation due to any implied literal.

The use of generalized local autarkies within a DPLL algorithm can be achieved in the same way than for local autarkies. Unfortunately, if the test of inclusion can be computed efficiently for local autarkies, the detection of generalized autarkies requests a CoNP-complete test.

Generalized (local) autarky modulo unit propagation

In order to pratically exploit the generalized local autarkies, it is necessary to weaken the deductive relation that is used. Accordingly, the full consequence relationship ( ) is weakened down to the mere unit propagation rule ( * ), which can be computed in linear-time.

Definition 3 Let Σ and Ω be two sets of clauses, Ω is a deductive consequence of Σ restricted to unit propagation, noted Σ * Ω, if and only if ∀c ∈ Ω, Σ * c.

Clearly, if Σ * Ω then Σ Ω. In consequence, Proposition 1 can be adapted to introduce the generalized local autarky modulo unit propagation.

Proposition 2 (Generalized (local) autarky modulo unit propagation)

Let Σ be a CNF formula, ρ = {l 0 , . . . , l j , . . . , l i } is a generalized local autarky modulo unit propagation if there exists ρ ′ = {l 0 , . . . , l j } such that Σ| ρ ′ * Σ| ρ . If ρ ′ = ∅ then ρ is a generalized autarky modulo unit propagation.

Earlier in the paper, it has been shown that the propagations of monotone, unit and more generally implied literals are special cases of local autarky detection. Likewise, the detection of local autarky modulo unit propagation automatically computes the propagations of monotone and unit literals, too. The following property proves useful in that respect:

Property 5 Let Σ and Ω be two CNF formulae. If Ω ⊆ Σ, then Σ * Ω.
This property is easily proved. Indeed, each clause c of Ω is present in Σ, also (Σ| c) * = ⊥ because the clause c of Σ is reduced to an empty clause by the propagation of c. In consequence, for each clause c of Ω Σ * c and by definition Σ * Ω. The converse is false, as illustrated by the following example.

Example 4 Let

Σ = {(a ∨ b ∨ c), (a ∨ ¬b), (b ∨ ¬c), (c ∨ ¬a)} and Ω = Σ| b = {(a), (c ∨ ¬a)}, we have Σ * Ω but Ω ⊂ Σ.
So, Property 5 ensures that all classical local autarkies are also detected by generalized local autarkies modulo unit propagation. In consequence, the simplification of monotone literals is implicitly included during the detection of generalized local autarkies modulo unit propagation. Similarly, the simplification by unit propagation is a special case of generalized local autarkies modulo unit propagations (Property 6).

Property 6

For any set of clauses Σ, Σ * Σ * .

Compared with generalized autarkies, only the simplification by the implied literals are not included in the generalized autarkies modulo unit propagation, as illustrated by the following example:

Example 5 Let Σ = {(a ∨ b ∨ c), (a ∨ b ∨ ¬c), (a ∨ ¬b ∨ ¬c), (¬a ∨ b ∨ ¬c), (¬a ∨ ¬b ∨ c), (a ∨ ¬b ∨ c)}. We have Σ a but Σ * a.
However, the restriction has been introduced to ensure that generalized (local) autarkies modulo unit propagation can be computed in polynomial time. Its implementation in a DPLL-like procedure is discussed in the next section.

Some useful properties and implementation

In this section, some practical properties about the generalized (local) autarkies modulo unit propagation are presented. More precisely, it is shown how the detection of these kinds of autarkies can be computed efficiently during the computation of a DPLL-like algorithm.

The first property is about the time complexity of deduction restricted to unit propagation.

Property 7 Let Σ and Ω be two sets of clauses. Checking

Σ * Ω is in O(C Ω × (|Σ| + |c|)) where c is the longest clause of Ω.
Unfortunately a polynomial-time complexity does not guarantee practical efficiency. In this respect, we also reduce in a significant way the number of unit propagations that are needed to detect local autarkies modulo unit propagation.

Property 8 Let Σ a set of clauses and l a literal. Σ * Σ| l if and only if ∀c ∈ Σ such that l ∈ c, Σ * c.

The above property suggests that after the assignment of a literal l, clauses containing ¬l need to be checked, only.

From properties 7 and 8, the following corollary is easily obtained:

Corollary 4 Let Σ be a set of clauses and l a literal. Checking Σ * Σ| l is in O(Occ( l)×C Σ ) where Occ( l) is the number of occurrences of l in Σ. This corollary shows that detecting a generalized local autarky modulo unit propagation between two consecutive nodes of a DPLL-like algorithm is a simple task that is very cheap w.r.t. time-complexity. However, there can exist generalized local autarkies modulo unit propagation between two non-consecutive nodes. The following property and its corollary show how useless tests can be avoided and that an incremental detection is possible.

Property 9 Let Σ be a set of clauses and {l 0 , . . . , l j , . . . , l i } a set of literals. If Σ| {l0,...,lj } * Σ| {l0,...,lj ,...,li} , then Σ| {l0,...,lj ,lj+1} * Σ| {l0,...,lj ,...,li} , Σ| {l0,...,lj ,lj+1,lj+2}

Detecting generalized local autarkies modulo unit propagation between two non-consecutive nodes of a DPLL-like algorithm depends on such a detection between two consecutive nodes. Accordingly, we insert this detection process within a DPLL-like procedure. It is performed during the backtrack step. Compared with a forward detection, this method avoids the useless unit propagations when the developed branch is proved unsatisfiable. The following algorithms describe this detection process (see Algorithm 2) and its integration within a DPLL-like procedure (see Algorithm 1).

Algorithm 1 details the DPLL-autark function which is a DPLL-like algorithm using the simplification by the generalized (local) autarkies modulo unit propagation. In this algorithm, the UnitPropagation and DecisionHeuristic functions are the DPLL-like solvers usual ones. All kinds of decision heuristics (MOMS [START_REF] Jeroslow | Solving propositional satisfiability problems[END_REF], VSIDS [START_REF] Moskewicz | Chaff: Engineering an efficient SAT solver[END_REF], etc.) can be used within DPLL-autark. When a call to the AutarkyModuloUP function is made, the Σ| l branch has been already explored and proved unsatisfiable. If Σ * Σ| l then the Σ|l branch can be pruned since Algorithm 2: AutarkyModuloUP input : a set of clauses Σ and a literal l such that Σ| l has been proved unsatisfiable output: true if Σ|l is satisfiable, false otherwise (Σ|l) * ←UnitPropagation(Σ ∧ ( l)); autarkyFound ←true; an autarky is detected. The AutrakyModuloUP function computes this test and, depending on the result, it either explores or prune the branch. This function is detailed in Algorithm 2.

2.5 // Σ * Σ| l iff ∀c = ( l ∨ c ′ ) ∈ Σ, Σ * c ′ foreach c ∈ Σ s.t. c = ( l ∨ l 1 ∨ l 2 ∨ • • • ∨ l n ) do 2.6 if UnitPropagation((Σ|l) * ∧ ( l1 ) ∧ 2.7 ( l2 ) ∧ • • • ∧ ( ln ))= ⊥ then (Σ|l) * ←(Σ|l) * ∧ (l 1 ∨ l 2 ∨ • • • ∨ l n );
For efficiency reasons, Algorithm 2 begins with the unit propagation of l. Indeed, each clause tested during the verification of Σ * Σ l implies the unit literal l. In order to avoid several propagations of l, the propagation of l is done once at the beginning of the procedure (see line 2.1).

When a clause c ′ = (l 1 ∨ l 2 ∨ • • • ∨ l n ) is proved to be a logical consequence through unit propagation of (Σ|l) * , it is added to (Σ|l) * (see line 2.8). These additional clauses speed up the computation of all unit propagations done during the rest of the procedure and reduce the size of the subtree built during the exploration of the branch Σ|l when no autarky has been detected. Note that these additions are performed in constant space. Indeed, the c ′ clause is obtained from a c clause of Σ that contains l. This c clause is satisfied during the unit propagation of l at the beginning of the procedure. The addition of c ′ can be done with a simple removal of the l literal from c. This process can be achieved in constant time and space with an adequate data structure.

Finally, even if the generalized local autarky modulo unit propagation is not detected, this approach is able to produce several sub-clauses. It is also possible to stop the detection as soon as Σ * Σ| l is proved (at the line 2.10). We believe that the spent time to produce sub-clauses is offset by the time saved to explore a smaller sub-tree. Two versions can be derived, one that only checks for generalized local autarkies modulo unit propagation and an other one that additionally produces sub-clauses. In the future, we plan to implement these two versions in order to measure and com- Table 1. Levels of literals of the search tree depicted in Fig. 2.

pare their practical strengths.

Local autarkies and implication levels

In the previous algorithm, only the current branch of DPLL can be cut when an autarky is found. It could be interesting to cut several branches to process a nonchronological backtracking like it is done in modern implementations of DPLL. In this section, it is shown that this goal can be reached by computing the largest jump with respect to an order of unit propagations. The standard concepts of level for a literal (section 2.2) and implication graph (Definition 5) are used in that respect.

We recall that δ(l) the level of a given literal l is given by the number of branches not explored before its assignment.

All assigned literals between two calls of the decision heuristics have the same level, as illustrated in the next example. An unassigned literal has an infinite level. In Table 1, the level of all literals at each node of the search tree depicted in Figure 2 is detailed.

Definition 4

Let Σ be a CNF formula, {l 1 , l 2 , . . . , l i } a partial assignment of Σ and c a clause of Σ| {l1,l2,...,li} . The level of c, noted δ(c), is defined in the following way:

• If c ∈ Σ, δ(c) = 0 ; • Else δ(c) = max{δ(l) s.t. l ∈ c et l ∈ {l 1 , l 2 , . . . , l i }}
The clause level matches the level of the last literal of the clause assigned to false.

The fundamental process to detect a generalized autarky modulo unit propagation consists in checking whether a clause is implied by unit propagation. The sequence of generated implications can be depicted by an acyclic oriented graph, called implication graph. Usually such a graph is used in all CDCL (conflict-driven clauses learning) approaches to learn clauses. It was first introduced in [START_REF] Marques-Silva | GRASP -A New Search Algorithm for Satisfiability[END_REF].

Definition 5 An implication graph, noted G = (V, A) is a graph such that:

1. V is the set of vertices where each vertex, noted s(l), is an assigned literal during unit propagation; 2. A is the set of edges. For a vertex s(l i ) the set of predecessors is defined by the vertices {s(l 1 ), . . . , s(l i-1 ), s(l i+1 ), . . . , s(l n )} if there exists a clause c = ( l1 , . . . , li-1 , l i , li+1 , . . . , ln ) and a current partial assignment ρ such that {l 1 , . . . , l i-1 , l i+1 , . . . , l n } ⊆ ρ. Each arc s(l j ), s(l i ) is labeled by c.

The roots of the implication graph representing the implication of a given clause by unit propagation are the vertices labelled by the negation of each literal of the clause. By construction, it is straightforward that this graph is acyclic. The goal is to compute the minimum levels of implication of the clauses that are used during the detection of the generalized local autarkies modulo unit propagation. So a value, noted η(l), is associated to each vertex of the graph in the following way:

• Roots vertices have a null value;

• Let a vertex s(l) and {s(l 1,1 ), . . . , s(l 1,m ), s(l 2,1 ), . . . , s(l 2,n ), . . . , s(l k,1 ), . . . , s(l k,p )} its set of predecessors such that s(l 1,1 ), s(l) , . . . , s(l 1,m ), s(l) are labelled by c 1 , s(l 2,1 ), s(l) , . . . , s(l 2,n ), s(l) are labelled by c 2 , . . . , and s(l k,1 ), s(l) , . . . , s(l k,p ), s(l) are labelled by c k , then

η(s(a)) = 0 η(s(b)) = 0 η(s(c)) = 8 η(s(d)) = 3 η(s(e)) = 0 η(s(f )) = 9 η(s(g)) = 6 η(s(i)) = 3 η(s(h)) = 3 η(s( l)) = 4 η(s(k)) = 3 η(s( k)) = 4
So, the implication level of the clause (ā, b) is equal to max(η(s(k)), η(s( k))) = 4.

Thus, it is possible to compute an implication level for all the clauses used in the detection of generalized local autarkies modulo unit propagation. A level can be assigned to the detected autarky. It is defined as the greatest implication level computed for each implied clause. In consequence, if the level of the autarky is j, it is possible to backjump safely up to this decision level. Indeed, for a sub-formula Σ i obtained from Σ and a partial assignment {l 0 , . . . , l j , . . . , l i }, if all the clauses of Σ i are implied modulo unit propagation at level k ≤ j, then Σ j * Σ i . All branches between j and the current level i are pruned.

Furthermore, even when no autarky is found, we have seen that the clauses that are proved to be implied during the autarky detection, are added to the formula. These clauses are added only until the current decision level is achieved. Since its minimal implication level has been computed, it is possible to keep the implied clauses until backtracking to their corresponding levels. This will reduce the size of search tree even more.

Conclusion

This paper presents a formal framework for the detection and use of autarky assignments, with the goal to im-prove the efficiency of SAT solvers. Several contributions about the generalization of classical autarkies have been provided. The first one introduces the concept of autarky modulo unit propagation, which extends the usual definition by substituting the syntactical inclusion operation by a semantic-one based on unit propagation. It has also been proved that propagating unit literals are special cases of this generalization. A second extension introduces the concept of implication level, aiming at detecting larger partitions. Interestingly enough, when no generalized local autarky can be found, the approach is able to produce several sub-clauses from the formula. Each implied clause can be exploited in order to reduce the search space until backtracking to its corresponding implication level. Finally, it is shown how these different approaches could be integrated in DPLL-like SAT solvers.

As future works, we plan to investigate how to integrate and implement the approach in modern SAT solvers. This might prove very succesful for efficiently solving industrialrelated SAT instances. It is well-known that many of these instances can be partitioned into several disconnected components after assigning a small set of variables. Another interesting path of research would be to design powerful clauses ordering heuristics for searching for local autarkies modulo unit propagation.

Figure 1 .

 1 Figure 1. DPLL search tree and local autarkies

Algorithm 1 : 1 . 1 if Σ * = ⊥ then return false; 1 . 2 else 5 if

 111125 DPLL-autark input : A CNF formula Σ output: true if Σ is satisfiable, false Σ * ←UnitPropagation(Σ); if Σ * = ∅ then return true; DPLL-autark(Σ * ∧ (l)) then return true;

2 . 1 if

 21 (Σ|l) * = ⊥ then return false; 2.2 else if (Σ|l) * = ∅ then return true;

Example 6

 6 Let Σ be the CNF formula built on the following 14 clauses: c 1 : (¬a ∨ c) c 6 : (¬b ∨ e) c 11 : (¬i ∨ l ∨ ¬k) c 2 : (¬a ∨ d) c 7 : (¬e ∨ i) c 12 : (¬i ∨ ¬l) c 3 : (¬b ∨ d) c 8 : (¬e ∨ h) c 13 : (¬k ∨ ¬l) c 4 : (¬d ∨ f ) c 9 : (¬g ∨ h ∨ ¬f ) c 14 : (c ∨ e) c 5 : (¬d ∨ g) c 10 : (¬h ∨ k) The implication graph corresponding to the implication by unit propagation of the clause (ā ∨ b) is depicted in Fig. 3.

3 . 7

 37 Implication graph representing an implication of a clause by unit propagation η(s(l)) = min[max(δ(c 1 ), η(s(l 1,1 )), . . . , η(s(l 1,m ))), . . . , max(δ(c k ), η(s(l k,1 )), . . . , η(s(l k,p )))]. Example Let us consider the same CNF formula as in example 6 together with the following clause levels: δ(c 1 ) = 8 δ(c 5 ) = 6 δ(c 9 ) = 12 δ(c 13 ) = 7 δ(c 2 ) = 3 δ(c 6 ) = 0 δ(c 10 ) = 2 δ(c 14 ) = 5 δ(c 3 ) = 7 δ(c 7 ) = 3 δ(c 11 ) = 1 δ(c 4 ) = 9 δ(c 8 ) = 3 δ(c 12 ) = 4 For each vertex of the implication graph depicted in Fig. 3, the following values are obtained:

  = (Σ| x ) * where x is the literal appearing in a unit clause of Σ. A clause c is deduced by unit propaga-tion from Σ, noted Σ * c, if (Σ| c) * =⊥.Let c 1 and c 2 be two clauses of a formula Σ. We say that c 1 (respectively c 2 ) subsumes (respectively is subsumed by) c 2 (respectively by c 1 ) iff c 1 ⊆ c 2 . If c 1 subsumes c 2 , then c 1 c 2 (the converse is not true). Also Σ and Σc 2 are equivalent with respect to satisfiability.

	∈ c}
	(that is: the clauses containing x are removed;
	and those containing ¬x are simplified). This no-
	tation is extended to assignments: given an as-
	signment ρ = {x 1 , . . . , x n }, Σ| ρ is defined as
	(. . . ((Σ| x1 )| x2 ) . . . | xn ).
	• Σ * denotes the formula Σ closed under unit propaga-
	tion, defined recursively as follows: (1) Σ * = Σ if Σ
	does not contain any unit clause, (2) Σ * =⊥ if Σ con-
	tains two unit-clauses {x} and {¬x}, (3) otherwise,
	Σ

*

//

Cut (unit literal) //

Figure 2. Levels of literals in DPLL


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

Learning in local search *

In this paper a learning based local search approach for propositional satisfiability is presented. It is based on an original adaptation of the conflict driven clause learning (CDCL) scheme to local search. First an extended implication graph for complete assignments of the set of variables is proposed. Secondly, a unit propagation based technique for building and using such implication graph is designed. Finally, we show how this new learning scheme can be integrated to the state-of-the-art local search solver WSAT. Interestingly enough, the obtained local search approach is able to prove unsatisfiability. Experimental results show very good performances on many classes of SAT instances from the last SAT competitions.

Introduction

The SAT problem, namely the issue of checking whether a set of Boolean clauses is satisfiable or not, is a central issue in many computer science and artificial intelligence domains, like e.g. theorem proving, planning, nonmonotonic reasoning, VLSI correctness checking. These last two decades, many approaches have been proposed to solve large SAT instances, based on logically complete or incomplete. Both local-search techniques (e.g. [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 Davis-Putnam-Loveland-Logemann DPLL procedure [START_REF] Davis | A machine program for theorem-proving[END_REF] (e.g. [START_REF] Moskewicz | Chaff: Engineering an efficient SAT solver[END_REF][START_REF] Een | An extensible SAT-solver[END_REF]), called modern SAT solvers, can now solve many families of hard SAT instances. These two kinds of approaches present complementary features and performances. Modern SAT solvers are particularly efficient on the industrial SAT category while local search is better on random SAT instances. Consequently, enhancing the performances of local search approaches to the level of modern modern SAT solvers on the industrial category is really an important challenge. This * supported by ANR UNLOC project ANR08-BLAN-0289-01 challenge is stated by Bart Selman et al. in 1997 [START_REF] Selman | Ten challenges in propositional reasoning and search[END_REF] (challenge number 6 "Improve stochastic local search on structured problems by efficiently handling variable dependencies"). Another important issue (challenge number 5) also identified in [START_REF] Selman | Ten challenges in propositional reasoning and search[END_REF], is to design a practical stochastic local search procedure for proving unsatisfiability. The goal of this work, is to make a step towards the resolution of these two challenges. Our aim is to enhance the performances of SLS techniques on industrial SAT instances and to make such techniques able to prove unsatisfiability.

Let us first recall that some attempts towards these directions have been made recently. In [START_REF] Pham | Building structure into local search for SAT[END_REF] functional dependencies recognized using Ostrowski et al approach [START_REF] Grégoire | Automatic extraction of functional dependencies[END_REF] have been exploited in local search based techniques leading to interesting improvements particularly on crafted SAT instances (e.g. parity 32 instances). In [START_REF] Prestwich | Local search for unsatisfiability[END_REF][START_REF] Audemard | Gunsat: A greedy local search algorithm for unsatisfiability[END_REF] new local search for proving unsatisfiability have been proposed. In [START_REF] Cha | Adding new clauses for faster local search[END_REF], authors propose a stochastic local search solver which add resolvents between two clauses in order to leave local minimum. Such method has been improved by [START_REF] Fang | Complete local search for propositional satisfiability[END_REF][START_REF] Shen | Another complete local search method for SAT[END_REF]. However, all these different approaches are still premature and progress is needed for solving both challenges.

To go further in this direction, we propose to integrate learning from conflict, one of the most important component behind the efficiency of modern SAT solvers, to local search techniques. However, one of the main difference between DPLL-like and local search techniques that make such adaptation very challenging rises in the way search space is explored by both approaches. In DPLL one searches among partial assignments whereas in SLS search is done on complete assignments. Even if such difference is important, the two search paradigms actually admit many common features. One can connect for example the activity based heuristics (VSIDS) with weighting constraint as done in the break-out local search method [START_REF] Morris | The breakout method for escaping from local minima[END_REF], restarts in modern SAT solvers with tries in WSAT like algorithms.

In this paper, we propose to improve the methods proposed in [START_REF] Cha | Adding new clauses for faster local search[END_REF][START_REF] Fang | Complete local search for propositional satisfiability[END_REF][START_REF] Shen | Another complete local search method for SAT[END_REF] by integrating Conflict Driven Clause Learning (CDCL) with implication graph [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] to the stochastic local search framework. The goal is twofold. First, similarly to [START_REF] Cha | Adding new clauses for faster local search[END_REF][START_REF] Fang | Complete local search for propositional satisfiability[END_REF][START_REF] Shen | Another complete local search method for SAT[END_REF], we exploit such learning component as a strategy to escape from local minima. However our approach is more general as the conflict clause is generated using an implication graph, whereas in [START_REF] Cha | Adding new clauses for faster local search[END_REF][START_REF] Fang | Complete local search for propositional satisfiability[END_REF][START_REF] Shen | Another complete local search method for SAT[END_REF], such a clause is obtained using only one resolution step between two clauses. Secondly, like previous methods, the addition of new learnt clauses makes the local search solver able to prove unsatisfiability.

The rest of this paper is organized as follows. In section 2, after the introduction of some preliminary definitions and notations, local search algorithms and classical SAT conflict analysis are presented. In section 3, we describe our extension of the implication graph to complete assignments and introduce a unit propagation based approach for building such graph. Finally, we integrate such conflict analysis in WSAT-like algorithm [START_REF] Selman | Noise strategies for improving local search[END_REF]. In section 4 experimental results of our proposed approach are presented before concluding.

Preliminary definitions and technical background 2.1 Definitions

Let us give some necessary definitions and notations. Let V = {x 1 ...x n } be a set of boolean variables, a literal ℓ is a variable x i or its negation

x i . A clause is a disjunction of literals c i = (ℓ 1 ∨ ℓ 2 ... ∨ ℓ ni ). A unit clause is a clause with only one literal. A formula Σ is in conjunctive normal form (CNF) if it is a conjunction of clauses Σ = (c 1 ∧ c 2 ... ∧ c m ).
The set of literals appearing in Σ is denoted V Σ . An interpretation I of a formula Σ associates a value I(x) to variables in the formula. An interpretation is complete if it gives a value to each variable x ∈ V Σ , otherwise it is said partial. A clause, a CNF formula and an interpretation can be conveniently represented as sets. A model of a formula Σ, denoted I |= Σ, is an interpretation I which satisfies the formula Σ i.e. satisfies each clause of Σ. Then, we can define the SAT decision problem as follows: is there an assignment of values to the variables so that the CNF formula Σ is satisfied? Let us introduce some additional notations.

• An empty clause is represented by ⊥ and is unsatisfiable;

• the negation of a set of literals Γ = {ℓ 1 , ℓ • η[x, c i , c j ] denotes the resolvent between a clause c i containing the literal x and c j a clause containing the opposite literal x. In other words η[x, c i , c j ] = c i ∪ c j \{x, x}. A resolvent is called tautological when it contains opposite literals.

Local Search Algorithms

Local search algorithms for SAT problems use a stochastic walk over complete interpretations of Σ. At each step (or flip), they try to reduce the number of unsatisfiable clauses (usually called a descent). The next complete interpretation is chosen among the neighbours of the current one (they differ only on one literal value). A local minimum is reached when no descent is possible. One of the key point of stochastic local search algorithms is the method used to escape from local minimum. For lack of space, we cannot provide a general algorithm of local search solver. However, a modified version can be seen in algorithm 1. For more details, the reader will refer to [START_REF] Hoos | Stochastic Local Search: Foundations and Applications[END_REF].

Conflict Analysis and Implication Graph

Now, we introduce a fundamental data structure, called implication graph, used by complete CDCL solvers (Conflict Driven Clause Learning) for conflict analysis, nogood deduction and backjumping. Some of the following notations have been introduced in [START_REF] Audemard | A generalized framework for conflict analysis[END_REF].

A typical branch of a CDCL solver can be seen as sequences of decision-propagation. At decision level i, the current partial interpretation I is of the form

(x i k ), x i k1 , x i k2 , . . . , x i kn k
where the first literal x i k corresponds to the decision literal x k assigned at level i and each x i kj for 1 ≤ j ≤ n k corresponds to a propagated (unit) literal. Whenever a literal y is propagated, we keep a reference to the clause at the origin of the propagation of y, which we denote -→ cla(y). Of course It can exist more than one such clause, however we are taking into account only one of them, usually the first encountered one. The clause -→ cla(y) has, in this case, the form (x 1 ∨ • • • ∨ x n ∨ y) where every literal x i is false under the current partial assignment (I(x i ) = f alse, ∀i ∈ 1 . . . n), while I(y) = true. When a literal y is not obtained by propagation but comes from a decision, -→ cla(y) is undefined, which we note for convenience -→ cla(y) =⊥. When -→ cla(y) =⊥, we denote by exp(y)

the set {x | x ∈ -→ cla(y) \ {y}}, called set of explanations of y. In other words, if -→ cla(y) = (x 1 ∨ • • • ∨ x n ∨ y)
, then the explanations are the literals x i with which -→ cla(y) becomes the unit clause {y}. When -→ cla(y) is undefined we define exp(y) as the empty set.

The implication graph is a directed acyclic graph, it allows a representation of decision-propagations sequences. In such a graph, each vertex is associated to a literal and incoming edges of a vertex are the set of its explanations. Formally, we have: Definition 1 (Implication graph) Let Σ be a CNF formula and I p be a partial interpretation. An implication graph associated to Σ, I p and exp is G Ip Σ = (N ,A) where:

1. N = {x|x ∈ I p }, i.e. there is exactly one node for every literal, decision or implied;

2. A = {(x, y)|x ∈ I p , y ∈ I p , x ∈ exp(y)}.
Example 1 Let Σ = {φ 1 , ..., φ 11 } be a CNF formula such that.

φ 1 : (x 1 ∨ x 2 ∨ x 3 ) φ 2 : (x 1 ∨ x 4 ∨ x 5 ) φ 3 : (x 2 ∨ x 1 ) φ 4 : (x 4 ∨ x 7 ∨ x 6 ) φ 5 : (x 3 ∨ x 5 ) φ 6 : (x 5 ∨ x 7 ) φ 7 : (x 6 ∨ x 8 ) φ 8 : (x 7 ∨ x 8 ) φ 9 : (x 8 ∨ x 4 ) φ 10 : (x 1 ∨ x 8 ) φ 11 : (x 7 ∨ x 9 )
Let I p be the following partial interpretation As mentioned above, an implication graph allows nogoods extraction. These nogoods are built by a traversal of the implication graph starting from the top (the falsified clause). Different kinds of nogoods can be generated. One of the most used and efficient learning scheme is the first UIP (Unique Implication Point). In the following example, we show a construction of a first UIP. For more details and a formal presentation, the reader can refer to [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].

I p = { (x 1 2 ) (x 2 6 ) (x 3 9 ) x 3 7 x 3 4 x 3 5 x 3 3 x 3 1 x 3 1 }. The Current de- cision level is 3 and Σ |Ip |= * ⊥.

Example 2 Consider again example 1 and the same implication graph (Figure 1) associated to interpretation I p . To generate the first UIP, we perform resolution (starting from the conflict) between clauses encoded in the implication graph (implications):

• β 1 = η(x 3 1 , φ 1 , φ 2 ) = x 1 2 ∨ x 3 3 ∨ x 3 4 ∨ x 3 5 • β 2 = η(x 3 3 , β 1 , φ 5 ) = x 1 2 ∨ x 3 4 ∨ x 3 5 • β 3 = η(x 3 5 , β 2 , φ 6 ) = x 1 2 ∨ x 3 4 ∨ x 3 7 • β = η(x 3 4 , β 3 , φ 4 ) = x 1 2 ∨ x 2 6 ∨ x 3 7
The clause β contains only one literal from the last decision level (here level 3). Then, the process ends with the clause β, usually called an asserting clause. The literal x 3 7 is an asserting literal, and the node x 7 in the implication graph (see figure 1) is the first UIP.

Local search and conflict analysis 3.1 Conflict graph definition

In section 2.2, we mentioned that one of the key points behind the efficiency of local search algorithms is undoubtedly the strategy used to escape from local minima. In [START_REF] Cha | Adding new clauses for faster local search[END_REF][START_REF] Fang | Complete local search for propositional satisfiability[END_REF][START_REF] Shen | Another complete local search method for SAT[END_REF], authors proposed to add clauses obtained by resolution in order to leave such minimum. We propose to improve such a strategy by exploiting the implication graph built from a complete interpretation to generate and add nogoods to the clauses data base.

However, in local search framework, one has to deal with complete interpretations. Defining an implication graph in this case is clearly challenging. Indeed, there is no notion of levels or unit propagated literals. Furthermore, a complete interpretation can falsify more than one clause. In this section, we propose a new definition of implication graphs in stochastic local search framework. Before, we give some necessary definitions. Let us consider a CNF formula Σ and a complete interpretation I c . We say that the literal ℓ satisfies (resp. falsifies) a clause β ∈ Σ under • {z, z, ⊥} ⊆ N ;

I c if ℓ ∈ I c ∩ {x | x ∈ β} (resp. ℓ ∈ I c ∩ {x | x ∈ β}). We note L + Ic (β) (resp. L - Ic (β)),
• {γ 1 , . . . , γ l } ⊆ N ;

• {β 1 , . . . , β k } ⊆ N ; 2. • {(z, ⊥), (z, ⊥)} ⊆ A ; • {(β 1 , z), . . . , (β k , z)} ⊆ A ; • {(γ 1 , z), . . . , (γ k , z)} ⊆ A ; 3. ∀x ∈ N , if x = z and α = {y ∈ N | (y, x) ∈ A} |= ⊥ then α ∨ x ∈ Σ is once-satisfied on x.
Since for a given literal z, clauses like β and γ are not unique, then the conflict graph is not unique too. It is important to note that the existence of such a graph is not ensured. The following proposition gives necessary and sufficient conditions for the construction of the conflict graph.

Proposition 1 Let Σ be a CNF formula, I c a complete interpretation. The conflict graph G x Σ,Ic exists if and only if x and x appear respectively in a falsified clause and in a once-satisfied one.

Proof The proof of this proposition follows directly from the definition of the conflict graph.

Corollary 1 Let α ∈ Σ be a critical clause. ∀x ∈ α, it is possible to construct a conflict graph on x.

Proof By definition of a critical clause α ∈ Σ, we have ∀x ∈ α, ∃β ∈ Σ once-satisfied on x. From Proposition 1, it is obvious that ∀x ∈ α, it exists a conflict graph on x.

As shown in [START_REF] Grégoire | Extracting MUSes[END_REF], in a local minima all falsified clauses are necessarily critical. The corollary 1 ensures that, in this case, it is always possible to build a conflict graph. Then, we can use it in order to leave such local minimum. However, generating such nogoods is not obvious. Indeed, there is not notion of levels, the classical notion of conflict analysis and first UIP can not be extended. Furthermore, conflict graphs can contain cycles. In this case, the resolution step can produce tautological clauses which are obviously useless. To overcome these problems, we propose to transform conflict graph of a complete interpretation into a classical implication graph and then use classical learning to generate relevant nogoods.

Building Conflict Graph

To overcome problems introduced in previous section, we propose a first method, based on unit propagation. Starting from a complete interpretation I c , we build a partial interpretation I ′ by unit propagation where decision variables have the same value as in I c . This partial interpretation introduced formally in the following definition will help us to build the conflict graph.

Definition 5 (Derived partial interpretation)

Let Σ be a CNF formula, I c a complete interpretation. The derived partial interpretation of I , denoted I ′ , is incrementally build as follows:

• I ′ 0 = ∅ ; • I ′ i+1 = I ′ i ∪ {(x i+1 ), x 1 i+1 , ..., x k i+1 } such that x i+1 ∈ V Σ \ I ′ i and ∀j, 1 j k one has Σ | I ′ i ∪{x i+1 } |= * x j i+1 with x j i+1 ∈ I c ; • I ′ = I ′ i ∪ {(x i+1 ), x 1 i+1 , ..., x l i+1 } such that x i+1 ∈ V Σ \I ′ i and ∀j, 1 j l one has Σ | I ′ i ∪{x i+1 } |= * x j i+1 with x j i+1 ∈ I c for j = l and x l i+1 / ∈ I c .
The set of variables associated to the decision literals is called a conflict set. Furthermore, we call conflict variable the one associated to the literal x ∈ I ′ \ I. The literal x is also called a conflict literal.

Of course, the choice of the conflict set of variables is a heuristic choice and can lead to different derived partial interpretations.

Example 5 Let us consider again the CNF Σ of example 1 and the complete interpretation I c = {x 1 , . . . x 9 }. First, considering the decision variables in lexicographic ordering. We have:

• I ′ 0 = ∅ • I ′ 1 = {(x 1 ), x 1 2 , x 1 3 }
Then, the conflict variable is x 3 and the conflict set is limited to {x 1 }. Now, considering the inverse lexicographic ordering, the partial interpretation is:

• I ′ 0 = ∅ • I ′ 1 = {(x 1 9 ), x 1 7 , x 1 5 , x 3 1 } • I ′ 2 = {(x 1 9 ), x 1 7 , x 1 5 , x 3 1 , (x 2 8 ), x 2 6 , x 2 4 , x 2 1 , x 2 2 , x 2 2 }
the conflict variable is x 2 and the conflict set is {x 9 , x 8 }.

Complete interpretation is conflicting, so the derived partial interpretation will differ on, at least, one conflict literal. The following proposition asserts that it exists at least one conflict clause containing this literal. The conflict graph is then built on this literal.

Proposition 2 Let Σ be a CNF formula, I c a conflicting complete interpretation and I ′ a derived partial interpretation of I c . Let x be the conflict literal, then exp(x) ⊆ I c and the clause -→ cla(x) is falsified by I c .

Proof First, by construction of I ′ , it is obvious that exp(x) ⊆ I c . Indeed, suppose that exp(x) ⊆ I c then ∃y ∈ exp(x) such that y ∈ I c . By definition exp(x) ⊆ I ′ , so y ∈ I ′ , consequently the literal y is also a conflict literal. By construction of I ′ , it exists only one conflict literal, then y = x. This is impossible, because a propagated literal can not be included in its explanation. Secondly, we have to prove that I c |= -→ cla(x). Suppose -→ cla(x) is satisfied by I c . Note that x is a propagated literal, then it exists an explanation exp(x) and a clause

-→ cla(x) ∈ Σ such that -→ cla(x) = exp(x) ∨ x.
We know that exp(x) ⊆ I c , then exp(x) ⊆ I c . Since -→ cla(x) is satisfied by I c , it can be only satisfied by x. This is not possible because x ∈ I c .

The following proposition expresses the fact that all clauses (expect the falsified one) which are used to construct the graph are once-satisfied clauses. In the proposition 4, we show that the implication graph obtained with the partial derived interpretation can be extended in a conflict graph on the conflict literal. Then, with the help of this implication graph, it is possible to generate nogoods similarly to classical CDCL solvers [START_REF] Een | An extensible SAT-solver[END_REF]. Of course, these nogoods will be added to the clauses database.

Proposition 4 Let Σ be a CNF formula, I c a complete interpretation on Σ, I ′ a partial derived interpretation and x the conflict literal associated to I ′ . If ∃α ∈ Σ oncesatisfied by I c on x, then it is possible to extend the implication graph G I ′ Σ = (N , A) associated to I ′ to a conflict graph G x Σ,Ic = (N ′ , A ′ ) as follows:

• N ′ = N ∪ {y ∈ α \ x} ∪ {x, ⊥} ; • A ′ = A ∪ {(y, x)|y ∈ α \ x} ∪ {(x, ⊥), (x, ⊥)}.
Proof Before proving that G x Σ,Ic is a valid conflict graph, one has to identify clauses β = {β 1 , . . . , β k , z} ∈ Σ falsified by I c and γ = {γ 1 , . . . , γ l , z} ∈ Σ once-satisfied on z for I c . By hypothesis, clause α is once-satisfied by I c on x. Obviously, γ = α. By proposition 2, one can take β = -→ cla(x). Indeed, x ∈ -→ cla(x) and the clause -→ cla(x) is falsified by I c . The both clauses used for the construction of the conflict graph are now identified. To prove that G x Σ,Ic = (N ′ , A ′ ) is a conflict graph, one has to verify the following properties (see definition 4):

1.

• {x, x, ⊥} ⊆ N ′ . By hypothesis, one has {x, ⊥} ⊆ N ′ , We only need to prove that x ∈ N ′ . We know that x ∈ I ′ , by construction of

G I ′ Σ , then we have x ⊆ N . Since N ⊆ N ′ , then x ∈ N ′ ; • {γ 1 , . . . , γ l } ⊆ N ′ . We have {y ∈ α \ x} ⊆ N ′ and γ = α. Then {y ∈ γ \ x} ⊆ N ′ ; • {β 1 , . . . , β k } ⊆ N ′ . By hypothesis, β = -→ cla(x) = β 1 ∨ • • • ∨ β k ∨ x = exp(x) ∨ x. Then, exp(x) = {β 1 , . . . , β k }.
By proposition 2, one has exp(x) ⊆ I ′ , so exp(x) ⊆ N (see definition 1). Since N ⊆ N ′ , by transitivity, one has exp(x) ⊆ N ′ ; 2.

• {(x, ⊥), (x, ⊥)} ⊆ A ′ . By construction ;

• {(γ 1 , x), . . . , (γ k , x)} ⊆ A ′ . By construction ; Σ and G x Σ,Ic the previous property is verified.

• {(β 1 , x), . . . , (β k , x)} ⊆ A ′ .

Example 6 Let us take again example 1 and partial derived interpretations obtained in example 5. We can extend implication graphs associated to these interpretations in two conflict graphs depicted in Figures 3.a (lexicographic order) and 3.b (inverse lexicographic order).

Implementation

We propose to incorporate the conflict graph defined in previous section inside a WSAT like solver [START_REF] Selman | Noise strategies for improving local search[END_REF]. This is done when a local minima is reached. We name this method CDLS. During the construction of the partial derived interpretation, two cases might occur: Either a conflict is reached during unit propagation (see Figure 3.b) or not (see Figure 3.a). In the former, one uses the resulting implication graph, analyzes the conflict and extracts an assertive clause associated to the first UIP. In the latter, one extends the implication graph of the derived partial interpretation to a conflict graph and, in a similar way, an assertive clause is extracted. In both cases, assertive clauses are added to the clauses database of the formula. And, if the assertive clause is the empty one, the unsatisfiability of the formula is proved. Contrary to classical WSAT algorithm, one can flip a set of variables when a local minima is reached. These are variables whose values differ between complete interpretation and derived partial interpretation.

It is important to note that CDLS is not an hybrid algorithm like [START_REF] Fang | A new hybrid solution to boost SAT solver performance[END_REF][START_REF] Goldberg | A decision-making procedure for resolution-based SAT-solvers[END_REF]. It is a simple stochastic local search method. Unit propagation is only used to build the conflict graph, to analyze conflict graph and to extract nogoods. Algorithm 4 is the core or our proposed framework. It starts by selecting conflict variables set which allows to build the derived partial interpretation. This is done by Algorithm 3. It chooses variables in linked clauses to the falsified clause α in order to make the generated partial interpretation nearest to α. Then, this partial interpretation I p is constructed (line 4-7). Two cases might occur. In the former, a conflict is reached, classical conflict analysis is applied (line 9) and an assertive literal is flipped. In the latter, one can extracts the partial derived interpretation of I p and generates the associated conflict graph (line 12-14 and proposition 4). At this point, conflict analysis can be achieved. All variables with different values in both interpretations are then flipped.

Algorithm 1: CDLS

Input: Σ a CNF formula Output: SAT if Σ is satisfiable, U N SAT if Σ is unsatisfiable, else U N KN OW N for i ← 1 to M axT ries do 1 I c ← completePUInterpretation(Σ);

Experimental results

Experimental results reported in this section were obtained on a Xeon 3.2 GHz with 2 GByte of RAM. CPU time is limited to 1200 seconds. We compare CDLS to three classical incomplete local search methods, WSAT [START_REF] Selman | Noise strategies for improving local search[END_REF], RSAPS [START_REF] Hutter | Scaling and probabilistic smoothing: Efficient dynamic local search for SAT[END_REF] and ADAPTG2 [START_REF] Chu | Combining adaptive noise and look-ahead in local search for sat[END_REF] ; we also add CLS the complete local search solver proposed by [START_REF] Fang | Complete local search for propositional satisfiability[END_REF] and MINISAT [START_REF] Een | An extensible SAT-solver[END_REF] one of state-of-the-art CDCL solver. Instances used are taken from the last SAT competitions. They are divided into different categories: crafted (1439 instances), industrial (1305) and random (2172). All instances are preprocessed wih SatElite [START_REF] Eén | Effective preprocessing in SAT through variable and clause elimination[END_REF]. Indeed, it is well known resolution based preprocessors help, in a lot of cases, local search and complete ones [START_REF] Anbulagan | Boosting sls performance by incorporating resolution-based preprocessor[END_REF].

Table 4 summarizes the obtained results on this large number of instances. For more details on this experimental part, the reader can refer to http://www.cril.fr/ ˜lagniez/cdls. For each category and for each solver we report the number of solved instances. Of course, MIN-ISAT a state-of-the-art CDCL based complete solver is considered here, only to mention the gap between local search based techniques and complete modern SAT solvers on industrial and crafted instances. On random satisfiable instances, local search techniques generally outperform complete techniques.

Let us start to analyze the results obtained on the crafted category. Except for MINISAT, CDLS is very competitive and solves approximately the same number of instances than RSAPS and ADAPTG2. Furthermore, CDLS solves much more instances than WSAT, its built-in solver. Comparing to CLS, our solver is better, it solves more SAT and UNSAT instances. For industrial instances, CDLS solves two times more instances than other stochastic local search solvers and 232 unsatisfiable instances. It outperforms CLS, the other complete local search solver. So, conflict analysis allows to solve efficiently structured SAT and UNSAT instances. Finally, for the random category, we can note that CDLS and CLS are unable to solve unsatisfiable problems. As pointed by MINISAT results, learning is not the good approach to solve random instances.

A summary, our solver CDLS is much more efficient than other local search algorithms. It significantly improves WSAT, its built-in solver and CLS another complete local search approach. Even if MINISAT is the best solver on crafted and industrial instances, these first results are very encouraging and reduce the gap between local search based techniques and DPPL-like complete solvers.

Conclusion

In this paper, we propose a new approach to keep out local minimum when dealing with a stochastic local search solver. Our approach extends conflict analysis used by modern SAT solvers. With this extension, we significantly improved stochastic local search solvers. More interestingly, our approach is able to prove inconsistency of many SAT instances, and then it can be seen as an important step to the resolution of the challenge number 5 proposed by Selman et al. at IJCAI 1997. These first results are very promising. Our solver is able to solve a lot of unsatisfiable instances and it achieves interesting improvements of local search based techniques on structured SAT instances. In future works, we plan to improve heuristic choice for the conflict set. We also want to analyze and extract nogoods without the help of unit propagation. Finally, we plan to study other schemes for extracting relevant nogoods.

Figure 1

 1 represents the implication graph G Ip Σ associated to Σ, I p and exp (the set of explanations).

Figure 1 .

 1 Figure 1. Implication graph (example 1)

Example 3 Definition 4 (

 34 the set of literals satisfying (resp. falsifying) a clause β under I c . The following definitions were introduced in [11]. Definition 2 (once-satisfied clause) A clause β is said once-satisfied by an interpretation I c on literal z if L + Ic (β) = {z}. Definition 3 (critical and linked clauses) Let I c be a complete interpretation. A clause α is critical w.r.t. I c if |L + Ic (α)| = 0 (α is falsified) and ∀ℓ ∈ α, ∃α ′ ∈ Σ with ℓ ∈ α ′ and α ′ is an once-satisfied clause. Clauses α ′ are linked to α for the interpretation I c . Let Σ = (a∨b∨c)∧(a∨b)∧(b∨c)∧(c∨a) be a formula and I c = {a, b, c} an interpretation. The clause α 1 = (a ∨ b ∨ c) is critical. The other clauses of Σ are linked to α 1 for I c . Now, we can define conflict graph for complete interpretations. Conflict graph on z) Let Σ be a CNF formula, I c a complete interpretation falsifying Σ. Consider two clauses of Σ, β = {β 1 , . . . , β k , z} falsified by I c and γ = {γ 1 , . . . , γ l , z} once-satisfied on z, the conflict graph G z Σ,Ic = (N , A) is constructed in the following way: 1.

Example 4

 4 Consider again example 1. Let I c be a complete interpretation such that I c = {x 1 , . . . , x 9 }.

Figure 2 .

 2 Figure 2. Conflict graph constructed on variable x 1 (example 4)

Proposition 3

 3 Let Σ be a CNF formula, I c a complete conflicting interpretation, I ′ a derived partial interpretation and x the conflict literal associated to I ′ . Consider the implication graph G I ′ Σ = (N , A), then ∀y ∈ N \ {x} one has -→ cla(y) = ⊥ where -→ cla(y) is once-satisfied by I ′ on x. Proof One need to consider two cases: 1. y is a decision literal, then -→ cla(y) = ⊥ ; 2. y is a propagated literal. It exists -→ cla(y) ∈ Σ such that -→ cla(y) = exp(y) ∨ y. By construction of I ′ , one has x ∈ exp(y) and I ′ \ {x} ⊂ I c . Since y = x, one has {exp(y), y} ⊆ I ′ . By transitivity, one obtain {exp(y), y} ⊆ I c \ {x}. Then, the clause -→ cla(y) is once-satisfied by I c on y.

  One knows that exp(x) = {β 1 , . . . , β k } and {exp(x), x} ⊆ I ′ . By construction of A ′ and by definition 1, one has {(β 1 , x), . . . , (β k , x)} ⊆ A ⊆ A ′ ; 3. ∀x ∈ N , if x = z and α = {y ∈ N | (y, x) ∈ A} |= ⊥ then α ∨ x ∈ Σ and is once-satisfied on x. By proposition 3, ∀y ∈ N such that y = x and -→ cla(y) = ⊥, one has -→ cla(y) once-satisfied by I c on y. By construction of G I ′

Figure 3 .

 3 Figure 3. Conflict graph constructed with unit propagation (example 6)

2 for j ← 1 to M axF lips do 3 if I c |= Σ then 4 return SAT ; 5 Γ 6 while Γ = ∅ do 7 α ∈ Γ; 8 if ∃x ∈ α allowing a descent then 9 f 14 α 15 β 16 if β = ⊥ then 17 return UNSAT; 18 Σ ← Σ ∪ {β}; 19 return U N KN OW N ; 20 Algorithm 2 : 1 while Σ ′ = ∅ do 2 x 3 P 4 foreach y ∈ P do 5 if y ∈ P then 6 P ← P \ {y}; 7 Σ ′ ← Σ ′ |P ; 8 I 9 return I c ; 10 Algorithm 3 : 1 forall x ∈ α do 2 β 3 C 5 Algorithm

 2134567891415161718192021234567891031235 = {α ∈ Σ| I c |= α}; ∈ Σ such that I c |= α; ← conf lictAnalysisRL(Σ, I c , α); completePUInterpretation Input: Σ a CNF formula Output: I c a complete interpretation of Σ Σ ′ ← Σ; I c ← ∅; ∈ lit(Σ ′ ); ← {x} ∪ {y| Σ |x |= * y}; c ← I c ∪ P; conflictSet Input: Σ a CNF; I c a complete interpretation; α ∈ Σ a critical clause for I c . Output: C a conflict literals set C ← ∅; ∈ Σ once-satisfied on x; CDLS (see Algorithm 1) takes a CNF formula Σ as input and returns three different values (SAT , U N SAT or U N KN OW N ). It is based on WSAT algorithm. Note that initial complete interpretations are generated using unit propagation (line 2 of Algorithm 1 and Algorithm 2). In this way, local minimas are quickly reached and variables dependencies are taken into account i.e using unit propagation. Whenever a descent is possible, one flips a variable allowing it. When a local minima is reached, we analyze the conflict as explained previously. A nogood β is generated and added to the clause database.

Algorithm 4 : 2 E 3 x 4 β); 5 f 7 I 8 y 10 β

 423457810 conflictAnalysisRL Input: Σ a CNF; I c a complete interpretation; α ∈ Σ a critical clause for I c . Output: β a clause built on V Σ E ← conf lictSet(Σ, I c , α); γ ← ∅; I p ← ∅; 1 while (γ = ∅) and (I p ⊂ I c ) do ← E \ I p ; I p ← I p ∪ {x} such that ∈ E; γ ← BCP (); if γ = ∅ then / * CASE 1 * / ← f irstU IP (G Ip Σ lip(x) with x assertive literal ; ′ ← partial interpretation associated to I p ; ← conflict literal of I ′ ; 9 G y (Σ,I ′ ) ← extended conflict graph G I ′ Σ ; ← f irstU IP (G y (Σ,I ′ ) ); 11 forall x ∈ I p \ I c do f lip(x);

Table 1 . CDLS versus some other SAT solvers

 1

	12
	13	return β;
			Crafted	Industrial	Random
			sat unsat	sat unsat	sat unsat
	ADAPTG2	326	0 232	0 1111	0
	RSAPS	339	0 226	0 1071	0
	WSAT	259	0 206	0 1012	0
	CDLS	331	146 412	232	943	0
	CLS	235	75 227	102	690	0
	MINISAT	402	369 588	414	609	315