Raisonnement propositionel pour l'optimisation à grande échelle. Application à la mobilité via les énergies propres – Massal'IA

Le problème de la satisfiabilité d'une formule propositionnelle (SAT) est fondamental dans de nombreux domaines de l’Informatique et particulièrement en Intelligence Artificielle (IA). Du fait de ses capacités à représenter le raisonnement, SAT constitue une approche très compétitive pour la résolution de problèmes génériques, souvent utilisée pour traiter des problèmes de décision dans des domaines, comme la vérification, la bio-informatique, la cryptographie ou la planification, dans lesquels elle surpasse souvent des solveurs dédiés. Cette aptitude est liée à l'utilisation de techniques avancées dans les solveurs SAT basés sur l'apprentissage de clauses à partir des conflits (Conflict Driven Clause Learning, CDCL). Ces solveurs peuvent traiter des problèmes industriels avec des millions de variables. Récemment, l'utilisation de techniques d'apprentissage automatique a permis de développer des très puissantes heuristiques de branchement.

Avec le succès des solveurs SAT pour les problèmes de décision, la communauté s'est intéressée, depuis une vingtaine d'années, au formalisme Max-SAT, qui constitue aujourd'hui une approche compétitive pour les problèmes d'optimisation. Les efforts dans ce domaine ont conduit au développement d'une nouvelle génération de solveurs Max-SAT, ainsi qu'à leur application à des problèmes réels (industriels) d'optimisation dans des domaines tels que la vérification de circuits ou l'alignement de séquences.

On distingue deux sortes de solveurs Max-SAT. Les solveurs de type branch-and-bound (BnB) utilisent comme borne inférieure le nombre de sous-ensembles inconsistants disjoints et sont performants sur les problèmes aléatoires et certains problèmes académiques ou faits-mains. Les solveurs basés sur SAT traitent Max-SAT en résolvant une suite de problèmes SAT avec un solveur SAT et sont particulièrement efficaces sur les problèmes industriels. Malgré des progrès spectaculaires de ces solveurs, les deux classes se sont développées séparément. Max-SAT constitue un domaine de recherche reconnu, mais les performances des solveurs doivent encore être améliorées pour être applicables à des problèmes réels de très grandes tailles contenant des données complexes.

Le premier objectif de ce projet est de proposer une approche hybride faisant intervenir des solveurs Max-SAT de type BnB et ceux basés sur SAT en profitant ainsi des points forts de chaque classe. Le deuxième objectif est d'utiliser l'apprentissage automatique pour développer des heuristiques de branchement lors de la conception de solveurs hybrides. Enfin, le troisième objectif est l'application de ces nouveaux solveurs à des problèmes industriels. Pour cela, nous utiliserons et développerons des outils de l’IA (apprentissage automatique, réseaux Bayésiens...) pour construire un modèle de données. La résolution du problème Max-SAT dérivé de ce modèle fournira des solutions de bonnes qualités et exploitables.

Un partenaire majeur, Enedis, est impliqué dans ce projet. Leur objectif est d'aider au développement de la mobilité électrique dans la métropole Aix-Marseille Provence (AMPM) tout d'abord, puis dans la région Provence-Alpes-Côte d’Azur, et enfin sur tout le territoire français. Cette tâche est difficile, du fait que cela concerne les transports et l'environnement, avec pour conséquence la production et la gestion de grandes quantités d'informations parfois incertaines ou incomplètes, provenant de sources différentes et complexes, et susceptibles d'évoluer avec le temps. Par ailleurs, les problèmes sous-jacents sont combinatoires et difficiles à résoudre. L'enjeu scientifique dans ce contexte est fondamental en IA : proposer de nouveaux modèles de représentation de ces informations complexes, et concevoir de nouvelles méthodes de raisonnement et d’optimisation de la formalisation en Max-SAT de ces modèles.