It is crucial to note that such an operation could increase the objective function value: it is the case when all neighbours have a greater value. Then, this mechanism allows to escape from local minimum.

However, the main drawback is that at the next step, one goes back in the same local minimum. To avoid this, heuristic needs memory for the last explored positions to be forbidden. These positions are *tabu*.

Already explored positions are stored in a queue (usually called *tabu list*) of a given length which is a parameter of the method. This list must contain complete positions, which can be prohibitive. To go round this, one can store only previous actions, associated to values of the objective function. The length parameter is very important. A lot of work have been done to provide optimal length, statically [26] or dynamically [3].

We propose to keep the set of tabu variables by using a partial interpretation computed with unit propagation engine. When a variable becomes tabu, it is assigned in the CDCL solver part and propagated. Then, resulting interpretation is used as a tabu list. There are two advantages: firstly, the length of the tabu list is dynamic, it depends of unit propagation and backjumping. Secondly, unit propagation allows to catch some functional dependencies in the tabu list.

## 4.2 Unsat Instances

First of all, note that if an instance is unsatisfiable then, whatever is the complete interpretation, a falsified clause exists. Furthermore, if an instance is unsatisfiable, then it contains at least one MUS. This MUS,
i.e. a subset of clauses of the formula, is often smaller than the global formula and, then, can contain less variables. Then, in the case of unsatisfiable formula, it is advantageous to focus the search on such variables.

In the frame of MUS detection, Gr´egoire *et al.* [13, 15] shown that local search provides good heuristics, concerning inconsistent kernel detection. These methods use properties 2 and 3 in order to balance clauses which could be part of a MUS.

The proposed method in this paper is based on this principle. When a local minimum is reached, property 2 assures that the set of clauses falsified by current interpretation are critical. Given that such clauses could be part of a MUS, we choose one of them to make it totally true. Therefore only the variables of a kernel are expected to be taken into account.

## 5 Implementation

As explicated in the previous section, the core of our solver SATHYS is the local search component. It is based on an iterative search process that in each step moves from one point to a neighbouring one until discovering a solution. At each step it tries to reduce the number of falsified clauses. When it is not possible, a local minimum is reached. In that case, the CDCL part is called. It chooses a falsified clause and assigns all of its literals such that the clause becomes totally valid. All literals of the chosen clause are decision nodes. Of course unit propagation is achieved. In this manner, it escapes from the local minimum and the SLS part of the hybrid solver can be used again. Note that all variables assigned by the CDCL part are fixed and can not be flipped by the SLS solver. Of course, during the CDCL process, a conflict can occur. In that case, conflict analysis is performed, a clause is learnt and a backjump is done.

Then, some of fixed variables become free and can be flipped again. This conflict analysis makes the solver able to prove unsatisfiability.

Algorithm 2 takes a CNF formula Σ in parameter and returns SAT or UNSAT. It is based on WSATlike algorithms. Two variables are used. A complete interpretation Ic for the local search engine (ini-