Soutenance mémoire
Le contexte général des travaux de thèse de ce manuscrit s’inscrit dans celui de l’intelligence artificielle et plus précisément la programmation par contraintes (CP). Ce paradigme de « programmation » a émergé au cours des années 70 (Mackworth (1977)), et s’est montré particulièrement efficace pour résoudre de nombreuses familles de problèmes combinatoires difficiles. Un problème combinatoire est un problème dont les instances, pour être résolues, nécessitent d’évaluer un nombre de combinaisons croissant de manière exponentielle avec leurs tailles. On trouve des problèmes combinatoires dans de nombreuses situations de la vie courante (calcul d’emploi du temps, calcul de trajets, résolution de jeux, etc.) et dans de nombreuses applications industrielles (vérification de circuits, placement d’antennes relais, etc.).
Le programmation par contraintes s’inscrit pleinement dans le contexte de recherche contemporain. En effet, CP a de nombreuses applications avec d’autres champs de recherche et/ou l’industrie. Un des exemples notables de ces dernières années est l’atterrisseur Philae, de la sonde spatiale Rosetta, qui s’est posé sur la comète 67P/Churyumov-Gerasimenko en 2014. Lors de son réveil en août 2015, un outil piloté par un système de programmation par contraintes a permis à ce laboratoire robot de gérer ses ressources limitées (Simonin et al. (2015)) ; les deux grandes limites étant l’énergie disponible ainsi que la mémoire embarquée. Les expériences effectuées par Philae ont été planifiées à l’aide de la programmation par contraintes, avec comme contrainte d’obtenir un temps de calcul d’un nouveau plan pour Philae relativement rapide. L’approche de planification par programmation par contraintes, grâce à de nouveaux propagateurs et contraintes globales, a permis de réduire le temps de calcul d’un plan de plusieurs heures à quelques secondes. Calculer et vérifier les plans dans un délai raisonnable était extrêmement important dans ce contexte mais cela reste vrai dans le cas général où un utilisateur préfère obtenir le plus rapidement possible une réponse à un problème donné.
Les problèmes combinatoires ne comportent pas toujours de solutions. Cela signifie qu’il faut parcourir l’ensemble des combinaisons avant de pouvoir conclure qu’aucune solution n’existe. En pratique, toutes les combinaisons possibles ne peuvent pas être explorées (pour des problèmes de taille relativement importante). De nombreuses techniques ont été proposées dans l’optique de réduire le nombre de combinaisons testées avant de trouver une solution voire de prouver qu’aucune n’existe. Ici, nous nous intéressons aux approches dites complètes qui ont pour vocation d’effectuer une recherche exhaustive et donc théoriquement, d’explorer tout l’arbre de recherche dans le pire cas. Il existe une autre approche afin de trouver une solution : l’exploration incomplète. Elle permet de parcourir des parties de l’espace de recherche jugées comme intéressantes. Ce type d’approche doit être guidée par des heuristiques afin de sélectionner les parties prometteuses qui seront explorées. De plus, comme celle-ci ne parcourt pas la totalité de l’espace, prouver qu’il n’existe pas de solution est en général impossible.
Dans un environnement de recherche complète nous voulons trouver une solution ou prouver qu’il n’existe pas de solution de manière efficace. Cela signifie qu’il nous faut explorer l’arbre de recherche de manière parcimonieuse. Pour cela, des techniques ont été proposées afin de guider la recherche vers des endroits prometteurs de manière heuristique ; ou au contraire, vers des parties de l’arbre de recherche qui ont une grande chance de ne contenir aucune solution afin d’élaguer l’arbre plus efficacement. Cela est généralement fait dans un contexte où les redémarrages (relancer la recherche régulièrement à partir du début) sont utilisés, conjointement aux nogoods, des instanciations partielles qui ne peuvent pas être étendues vers des solutions.
Le cadre CSP se situe au cœur de la programmation par contraintes, et le problème de satisfaction booléenne (SAT) est un problème particulier du problème de satisfaction de contraintes qui trouve de nombreuses applications, par exemple, en planification et vérification de circuits. Le problème SAT se limite aux variables binaires contrairement à CSP où les variables ont des domaines finis de taille quelconque (variables discrètes). Concernant le type de contraintes (booléennes) pouvant être gérées, le problème SAT implique uniquement des clauses, c’est-à-dire des disjonctions de littéraux (variables booléennes et leurs négations), qui peuvent être également représentées sous forme de sommes positives (sum(xi) > 0). Malgré ces limites, la force de ce paradigme réside dans ses méthodes de résolution et ses solveurs extrêmement performants. Dans le cas général, il nous faut choisir entre l’expressivité de CSP et la puissance de SAT.
Le but global des travaux présentés dans ce manuscrit est de cerner et formaliser des informations qui permettent une recherche plus efficace, notamment dans un environnement hybride SAT/CSP. Ces travaux s’inscrivent dans une politique de recherche contemporaine car applicable au contexte de l’optimisation et de la résolution parallèle ou distribuée. En effet, à l’heure de la multiplicité des machines, résoudre de manière parallèle ou distribuée un problème devient monnaie courante. Trouver des informations et une façon de les représenter permet de les partager. De plus, une meilleure utilisation de ces informations permet, par conséquent, d’améliorer l’efficacité de la recherche.
Au cours de la dernière décennie, la communauté de l’intelligence artificielle a consacré de nombreux efforts à la conception d’algorithmes généraux de résolution de problèmes de satisfaction de contraintes discrets (Rossi et al. (2006)). Les approches classiques en matière de résolution générale CSP reposent sur des méthodes complètes intégrant des procédures de filtrage, des méthodes heuristiques et des mécanismes d’apprentissage. Même pour les approches de l’état de l’art, plusieurs problèmes sont hors de portée. En effet, décider si un CSP est satisfiable est un problème NP-complet (Mackworth (1977)). C’est pour cette raison que de nouvelles approches doivent être proposées et évaluées. Cependant, la mise en œuvre d’une nouvelle technique dans un solveur CSP nécessite généralement une connaissance approfondie du solveur. De plus, pour être acceptée par la communauté, une nouvelle technique doit être comparée à des méthodes de l’état de l’art, ce qui implique qu’elles doivent être soigneusement mises en œuvre.
Les progrès impressionnants réalisés en SAT au cours des deux dernières décennies l’ont été grâce à l’enregistrement de nogoods (apprentissage de clauses) dans le cadre d’une politique de redémarrage renforcée par une structure de données paresseuse très efficace (Moskewicz et al. (2001)). L’intérêt pratique de l’apprentissage de clauses a crû avec la mise à disposition d’instances réelles volumineuses (applications pratiques) comportant une structure et présentant des phénomènes dits heavy-tailed. L’apprentissage de clauses en SAT est un exemple de technique fructueuse dérivée de l’intersection de la recherche à la fois en programmation par contraintes et en SAT. En effet, l’enregistrement de nogood (Dechter (1990)) et le retour arrière non chronologique dirigé par les conflits (Prosser (1993)) ont été introduits à l’origine pour CSP et ont ensuite été importés dans les solveurs SAT (Marques-Silva et Sakallah (1996), Jr. et Schrag (1997), Marques-Silva et Sakallah (1999)). Les progrès réalisés dans le cadre SAT ont suscité un regain d’intérêt de la communauté CSP pour l’enregistrement de nogood dans les années 2000 (Katsirelos et Bacchus (2003), Lecoutre et al. (2009)). Cependant, une partie des approches modernes proposées nécessitent l’utilisation d’un solveur SAT externe. Dans ce cas, le problème est entièrement encodé en CNF (Soh et al. (2017)) où il est traduit de manière incrémentale, voire paresseuse (Ohrimenko et al. (2007; 2009)). Mais, dans les deux cas, le solveur SAT a la priorité sur le solveur CP (exception faite pour la nouvelle architecture de la génération paresseuse de clauses, Feydy et Stuckey (2009)).
Le manuscrit est découpé en deux parties. La première partie contient les notions et définitions de l’état de l’art ainsi que les notations utilisées. Elle traite à la fois de la programmation par contraintes et de l’apprentissage d’information dans ce contexte, puis du problème de satisfaction booléenne et enfin de l’hybridation de ces deux paradigmes.
|
Table des matières
Introduction générale
I État de l’art
Chapitre 1 Programmation par contraintes
1.1 Réseaux de contraintes
1.2 Cohérence et résolution
1.2.1 Filtrage et cohérence
1.2.1.1 Cohérence d’arc
1.2.1.2 Cohérence de chemin
1.2.1.3 Propagateurs
1.2.2 Méthodes de résolution
1.2.2.1 Backtrack
1.2.2.2 Forward Checking (FC) et Maintaining Arc Consistency (MAC)
1.3 Heuristiques
1.3.1 Choix de valeur
1.3.2 Choix de variable
1.3.2.1 Heuristiques statiques
1.3.2.2 Heuristiques dynamiques
1.3.2.3 Heuristiques adaptatives
1.4 Conclusion
Chapitre 2 Apprentissage en programmation par contraintes
2.1 Nogoods standards
2.2 Enregistrement et exploitation des nogoods
2.3 Negative last decision nogoods
2.3.1 Découverte et enregistrement
2.3.2 Minimisation des nld-nogoods
2.4 Increasing nogoods
2.4.1 La contrainte globale IncNG
2.4.2 IncNG adapté aux redémarrages
2.4.3 Algorithme de filtrage de la contrainte globale IncNG
2.4.4 Minimisation des nogoods dans la contrainte globale IncNG
2.5 Conclusion
Chapitre 3 Le problème SAT
3.1 Logique propositionnelle
3.2 Principe de résolution
3.3 DPLL
3.4 CDCL
3.4.1 Analyse de conflits
3.4.2 Structure de données
3.4.3 Heuristiques
3.4.4 Réduction de la base de clauses apprises
3.4.5 Redémarrages
3.5 Conclusion
Conclusion générale
Télécharger le rapport complet
