| Page précédente | LERIA | Faculté des Sciences | Université d'Angers | |
L'algorithme GASAT [1,7] hybride une méthode génétique et une méthode de recherche locale.
Les opérateurs de base de l'algorithme génétique de GASAT sont un opérateur de sélection, une condition d'insertion et un opérateur de croisement [3,4]. Différentes études m'ont permis de déterminer la taille adéquate de la population afin que GASAT obtienne des résultats de bonne qualité en un temps raisonnable. Les deux nouveaux croisements spécifiquement développés pour les problèmes de satisfiabilité fournissent de bons résultats. Basés sur la structure des clauses de l'instance étudiée, ils permettent de diversifier la recherche en fournissant des individus avec de bonnes propriétés se trouvant dans des zones prometteuses de l'espace de recherche. Ces zones nécessitent une intensification de la recherche qui est effectuée par une méthode de recherche locale.
La méthode de recherche locale utilisé dans GASAT est une méthode tabou. À cette méthode de base, deux mécanismes spécifiquement développés pour les problèmes de satisfiabilité ont été ajoutés et permettent de mieux guider la recherche [2,5]. Le premier mécanisme (ACVF) intensifie la recherche en réduisant le voisinage et le second (mécanisme de diversification) permet de légèrement diversifier la recherche en identifiant des clause-butoirs et en s'assurant qu'elles soient satisfaites. Les expériences ont montré que l'utilisation conjointe de ces deux mécanismes permet d'améliorer la méthode tabou de base sur la majorité des instances. Cependant, pour les instances aléatoires, le mécanisme de diversification seul fournit de meilleurs résultats que la combinaison des deux.
Les deux parties de GASAT sont complémentaires et permettent d'explorer l'espace de recherche de manière diversifiée tout en intensifiant sur des zones prometteuses de manière efficace. GASAT a été évalué sur de nombreuses instances. Il a été comparé à des algorithmes évolutionnaires comme FlipGA et deux algorithmes de recherche locale : Walksat et UnitWalk . Les résultats obtenus lors des expériences sont très prometteurs et ses performances ont été confirmées durant la compétition SAT 2004 [6] au cours de laquelle GASAT à fini quatrième pour les instances aléatoires sur cinquante-cinq algorithmes testés et, à ce titre, est le premier algorithme mémétique à être concurrentiel lors de telles compétitions.