Given a boolean formula, one has to find
an instantiation of its variables that makes the formula true.
Recall that a boolean formula is
a conjunction of clauses, where
a clause is a disjunction of literals;
a literal is a boolean variable or its
negation, and a boolean variable is
a variable which can assume only the
values *true, false*.
When all the clauses have the same number *K*
of literals the problem is also called K-SAT.
The SAT problem has been extensively studied and many
exact and heuristic algorithms for SAT have been introduced
[2,3].
Efficient heuristic algorithms for SAT include algorithms
based on local search (cf. [2,3]) as well as approaches
based on evolutionary computation (e.g., [1,4,5,9]).

The aim of this paper is to show how the integration of a local search meta-heuristic into a simple evolutionary algorithm yields a rather powerful hybrid evolutionary algorithm for solving hard SAT problems.

In our method a simple (1+1) steady-state evolutionary algorithm with preservative selection strategy is used to explore the search space, while a local search procedure is used for the exploitation of the search space. Moreover, a meta-heuristic similar to the one employed in TABU search [6] is used for adapting the value of the mutation rate during the execution, for prohibiting the exploration/exploitation of specific regions of the search space, and for re-starting the execution from a new search point when the search strategy does not show any progress in the recent past.

Extensive experiments conducted on benchmark instances from the literature support the effectiveness of this approach.