Outils de déchargement automatique pour la coloration de graphes – TOAD

Ce projet de recherche vise à automatiser la génération et la vérification des preuves par déchargement en théorie des graphes, en particulier en coloration. Ce problème fondamental a de nombreuses applications concrètes par exemple en planification ou pour allouer des ressources. Un résultat majeur dans ce domaine est le théorème des quatre couleurs, qui affirme que tout graphe planaire peut être colorié avec quatre couleurs. Ce résultat a été prouvé par la méthode de déchargement, une technique permettant d'identifier des structures inévitables dans les graphes.

Ce projet vise à dépasser les limitations de cette méthode qui, bien que puissante, a tendance à produire des preuves longues et complexes. L'objectif est d'automatiser cette technique de preuve, traditionnellement très laborieuse, en développant un outil informatique capable de produire des preuves par déchargement, le but final étant de résoudre des problèmes ouverts majeurs en théorie des graphes. Contrairement aux prouveurs automatiques existants comme Coq ou DeepMind, cet outil générerait de manière autonome et efficace des preuves complètes et potentiellement longues.

Le projet a deux objectifs principaux. Tout d'abord, automatiser la recherche de règles de déchargement (actuellement conçues à la main par essai/erreur), en les modélisant par des programmes linéaires infinis puis en les simplifiant pour permettre leur résolution pratique. Le défi consiste à identifier les règles produisant de bons programmes, puis à réduire efficacement leur taille. Le deuxième objectif vise à automatiser le traitement des structures inévitables. Cette tâche, consistant en général à étendre des colorations partielles, est significativement plus difficile que le problème de coloration standard, mais doit néanmoins être résolue efficacement. Enfin, le projet explore deux extensions : le déchargement global et la méthode du potentiel, afin d'incorporer ces techniques à notre outil.