Next: Evolutionary Local Search Up: An Adaptive Evolutionary Algorithm Previous: An Adaptive Evolutionary Algorithm


Introduction

The satisfiability problem is a well-known NP-hard problem with relevant practical applications (cf., e.g. [3]).

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.



Next: Evolutionary Local Search Up: An Adaptive Evolutionary Algorithm Previous: An Adaptive Evolutionary Algorithm
Claudio Rossi
1999-11-30