Les paramètres des Algorithmes Evolutionnaires (AEs) ont une forte influence sur leur capacité à produire de bons résultats. Ces paramètres définissent les aspects structuraux et comportementaux de l'AE, comme la définition des composants qui seront inclus (e.g., l'ensemble d'opérateurs à utiliser, le codage, le schéma de sélection) ou la façon dont ces composants seront employés (e.g., le taux d'application des opérateurs). La paramétrisation des AEs a ´et´e longtemps un domaine de spécialistes, et même si de nombreuses études ont abordé le problème de la paramétrisation, il existe un déficit d'approches génériques qui puissent être appliquées à une grande variété d'AEs d'une manière simple. Cette thèse traite le problème de la conception d'un contrôleur générique, qui puisse être inclus dans n'importe quel AE avec un minimum d'efforts. Ceci est accompli en incorporant un composant d'apprentissage adaptatif, qui surveille l'état de la recherche et modifie les valeurs des paramètres. Le contrôleur se focalise sur les objectifs communs à tout EA, i.e., la maximisation de la diversité de la population et de la qualité des individus, afin de maintenir un équilibre convenable entre l'exploration et l'exploitation. Des nombreuses configurations des mécanismes d'apprentissage et d'ajustement ont ´et´e essayées et analysées, en utilisant AEs différents qui résolvent des problèmes combinatoires connus. Les bons résultats obtenus suggèrent que notre objectif de construire un contrôleur générique et facile à utiliser constitue une approche encourageante.

Au fil des années, un nombre croissant de méthodes de résolution ont été proposées afin de traiter des problèmes plus grands et plus complexes. Parmi ces méthodes, les métaheuristiques sont largement utilisées dans le monde académique et industriel afin de résoudre efficacement des problèmes d'optimisation et de satisfaction de contraintes. Toutefois la conception de métaheuristiques de plus en plus performantes produit souvent des systèmes fortement complexes dont l'utilisation demande une expertise non négligeable aussi bien du problème lui-même que de la façon de paramétrer la méthode de résolution. Concevoir des algorithmes de recherche autonomes est donc une question importante. Cette thèse traite du problème de la gestion et de la sélection d'opérateurs dans le contexte de la recherche locale, au sein d'un contrôleur générique. Celui a pour but de pouvoir être réutilisé facilement pour traiter différents problèmes. Nous nous attachons donc à concevoir des méthodes simples et robustes. La sélection des opérateurs se base sur un apprentissage des performances antérieures de chaque opérateur afin de déterminer les opérateurs vraisemblablement les plus bénéfiques à chaque pas de la recherche. Pour effectuer ces choix, le contrôleur se base sur la capacité des opérateurs à améliorer la qualité des solutions ainsi que sur la faculté de produire des solutions qui diffèrent de celles déjà obtenues. Les méthodes proposées sont testées sur différents problèmes théoriques et pratiques d'optimisation combinatoire et de satisfaction de contraintes. Les résultats obtenus montrent qu'il est possible d'obtenir des résultats corrects avec des méthodes simples. Les mécanismes adaptatifs proposés se révèlent robustes sur différents problèmes.

La génération de stratégies pour les solveurs en Satisfiabilité Modulo des Théories (SMT) nécessite des outils théoriques et pratiques qui permettent aux utilisateurs d’exercer un contrôle stratégique sur les aspects heuristiques fondamentaux des solveurs de SMT, tout en garantissant leur performance. Nous nous intéressons dans cette thèse au solveur Z3 , l’un des plus efficaces lors des compétitions SMT (SMT-COMP). Dans les solveurs SMT, la définition d’une stratégie repose sur un ensemble de composants et paramètres pouvant être agencés et configurés afin de guider la recherche d’une preuve de (in)satisfiabilité d’une instance donnée. Dans cette thèse, nous abordons ce défi en définissant un cadre pour la génération autonome de stratégies pour Z3, c’est-à-dire un algorithme qui permet de construire automatiquement des stratégies sans faire appel à des connaissances d’expertes. Ce cadre général utilise une approche évolutionnaire (programmation génétique), incluant un système à base de règles. Ces règles formalisent la modification de stratégies par des principes de réécriture, les algorithmes évolutionnaires servant de moteur pour les appliquer. Cette couche intermédiaire permettra d’appliquer n’importe quel algorithme ou opérateur sans qu’il soit nécessaire de modifier sa structure, afin d’introduire de nouvelles informations sur les stratégies. Des expérimentations sont menées sur les jeux classiques de la compétition SMT-COMP. / The Strategy Challenge in Satisfiability Modulo Theories (SMT) claims to build theoretical and practical tools allowing users to exert strategic control over core heuristic aspects of high-performance SMT solvers. In this work, we focus in Z3 Theorem Prover: one of the most efficient SMT solver according to the SMT Competition, SMT-COMP. In SMT solvers, the definition of a strategy relies on a set of tools that can be scheduled and configured in order to guide the search for a (un)satisfiability proof of a given instance. In this thesis, we address the Strategy Challenge in SMT defining a framework for the autonomous generation of strategies in Z3, i.e. a practical system to automatically generate SMT strategies without the use of expert knowledge. This framework is applied through an incremental evolutionary approach starting from basic algorithms to more complex genetic constructions. This framework formalise strategies modification as rewriting rules, where algorithms acts as enginess to apply them. This intermediate layer, will allow apply any algorithm or operator with no need to being structurally modified, in order to introduce new information in strategies. Validation is done through experiments on classic benchmarks of the SMT-COMP.