insights of our method. In section 5, we give the details and algorithms of SATHYS. Before a conclusion, section 6 provides different experiments.

## 2 Preliminary Definitions And Technical Background 2.1 Definitions

Let us give some necessary definitions and notations. Let V = {x1...xn} be a set of boolean variables, a literal ℓ is a variable xi or its negation ¯xi. A clause is a disjunction of literals ci = (ℓ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 Σ = (c1 ∧ c2...∧ cm). 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.

- The negation of a formula Γ is denoted Γ¯

- Σ|ℓ denotes the formula Σ simplified by the assignment of the literal ℓ to true. This notation is extended to interpretations: Let P = {ℓ1,..., ℓn} be an interpretation, Σ|P = (...(Σ|ℓ1
)...|ℓn
) ;
- Σ
∗ denotes the formula Σ simplified by unit propagation;
- |=∗ denotes logic deduction by unit propagation: Σ |=∗ l means that the literal x is deducted by unit propagation from Σ i.e. (Σ∧ ¯ℓ)
∗ = ⊥ . One notes Σ |=∗ ⊥ if the formula is unsatisfiable by unit propagation.

- η[x,ci,cj] denotes the *resolvent* between a clause ci containing the literal x and cj a clause containing the opposite literal ¬x. In other words η[x,ci,cj] = ci ∪cj\{x,¬x}. A resolvent is called tautological when it contains opposite literals.

## 2.2 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 can not provide a general algorithm of local search solver. For more details, the reader will refer to [19].

## 2.3 Cdcl Solvers

Algorithm 1 shows the general scheme of a CDCL solver (due to lack of space, we can not provide details for all subroutines). A typical branch of a CDCL solver is a sequence of decisions, followed by propagations, repeated until a conflict is reached. Each decision literal (lines 18–20) is assigned at a given decision level (dl), deducted literals (by unit propagation) have the same decision level. If all variables