Résumé

Cette thèse s’inscrit dans le domaine de la programmation par contraintes (CP), un des paradigmes les plus efficaces pour résoudre de nombreux problèmes (de nature combinatoire) en IA. Nous nous sommes intéressés à l’amélioration des techniques de résolution CSP (problème de satisfaction de contraintes), notamment dans un contexte hybride en utilisant la puissance des moteurs d’inférence SAT (problème de satisfaction booléenne). Nous avons ainsi développé plusieurs techniques concernant l’analyse de conflits afin d’extraire des informations utiles pour la résolution, grâce à une analyse fine suivie d’une forme d’apprentissage. Pour atteindre cet objectif, nous avons dans un premier temps renforcé la portée (puissance) des instanciations partielles incohérentes (nogoods) enregistrées par le système de résolution en proposant plusieurs règles permettant de les combiner. De plus, nous avons intégré un moteur de résolution SAT au sein d’un système CP reposant sur la notion d’explications paresseuses. L’utilisation d’un moteur SAT est motivée par leur grande efficacité à produire et à manipuler des formes simples de nogoods sous forme clausale. Le logiciel NACRE, moteur générique de raisonnement, est le résultat de ce travail ; il a notamment été conçu pour être un solveur hybride, résolvant les problèmes de satisfaction de contraintes à l’aide de méthodes dédiées ou inspirées de SAT. Notre approche générique (c’est-à-dire, valide quelque soit le problème traité) s’est avérée très efficace en pratique (NACRE a gagné 2 médailles d’or aux compétitions XCSP 2018 et 2019). Dans l’objectif d’enrichir l’hybridation SAT/CP, nous avons conduit une étude sur la qualité des clauses produites par le moteur SAT. Celle-ci nous permis de proposer de nouvelles méthodes de réduction de base de clauses, de minimisation ainsi que de nouvelles heuristiques de recherche.