Algorithm 3: fix Input: α a clause Output: Σ a CNF, Ic a complete interpretation, Ip a partial interpretation Result: *UNSAT* if unsatisfiable is proven, *UNKNOWN* otherwise 1 γ ← /0; 2 E ← {x| x¯ ∈ α}; 3 **while** (E 6= /0) and (α = /0) do 4 Ip ← Ip ∪ {x} tel que x ∈ E ;
5 γ ← BCP();
6 E ← E \ {x ∈ E | x ∈ Ip or x¯ ∈ Ip};
7 if γ 6= /0 **then**
8 β =conflictAnalysis(Σ,Ip,γ);
9 bl =computeBackjumpingLevel(γ,Ip );
10 if (bl < 0) **then return** *UNSAT*;
11 Σ ← Σ∪ {β};
12 ρ ← {x ∈ Ic| x¯ ∈ Ip};
13 Ic ← Ic \ {x¯| x ∈ ρ} ∪ρ; 14 **return** *UNKONWN*;
proved. Otherwise, the obtained nogood is added to the clause database (lines 7–11). Then, the complete interpretation Ic is updated with the help of the partial one (note that Ip and Ic can not differ).

## 6 Experiments

Experimental results reported in this section were obtained on a Xeon 3.2 GHz with 2 GByte of RAM. The CPU time is limited to 1200 seconds.

Our approach is compared with:
- three SLS methods:
1. classical WSAT [29], i.e. using random walk strategy

2. RSAPS [21] 3. ADAPTG2 [24]
- two recent hybrid methods submitted at the last SAT competition in 2009:

1. HYBRIDGM [2]
2. HYBRID1 [24]
- and two complete methods:

1. CLS a local search method completed by adding resolution process [10]
2. MINISAT [8] a well-known CDCL solver.
Instances used are taken from the last SAT competitions (www.satcompetition.org). They are divided into three different categories: crafted (1439 instances), industrial (1305) and random (2172). All instances are preprocessed with SatElite [7].