Sous la direction de Chu-Min Li (OCIA), l’équipe a obtenu une victoire éclatante lors de la SAT Competition 2025. Ce succès s’inscrit dans la lignée des médailles d’or remportées en 2009, 2017 et 2022, témoignant ainsi de l’impact significatif des Grands Modèles de Langage (LLM) dans l’optimisation des algorithmes les plus complexes.
Le Problème SAT : Un Défi Fondamental
Le problème de la Satisfiabilité (SAT) est le premier problème à avoir été prouvé NP-complet, le plaçant au cœur de l'informatique théorique, des mathématiques, de l'intelligence artificielle et du génie logiciel.
L'impact du SAT est crucial dans l'industrie, avec des applications allant de la vérification de puces en EDA et la détection de vulnérabilités dans les systèmes d'exploitation, à la planification de chemins pour la robotique et l'optimisation financière.
La Compétition Internationale d'Algorithmes SAT, organisée depuis 1992 (cette année marquant sa 28e édition), est reconnue comme l'événement mondial le plus prestigieux et influent pour l'évaluation des solveurs SAT. L'édition 2025, qui s'est déroulée à l'Université de Glasgow, a attiré des équipes de haut niveau du monde entier.
L'Innovation Majeure : L'Algorithme AE-Kissat-MAB
Le succès de l'équipe repose sur le développement d'un cadre novateur permettant aux LLM d’améliorer les algorithmes SAT automatiquement.
L'un des algorithmes qui en résulte, AE-Kissat-MAB, a dominé la compétition, prouvant l'efficacité sans précédent de l'optimisation guidée par IA :
• Piste Principale (Main Track) : Réduction du temps de résolution moyen de 6,6 % par rapport au deuxième classé.
• Piste des Instances Satisfiables (SAT Track) : Réduction spectaculaire du temps de résolution moyen de 48,8 % par rapport au deuxième classé.
Ceci marque une première historique : c'est la première fois qu’un algorithme SAT amélioré par les LLM remporte une compétition de cette envergure. Cette performance est d'autant plus remarquable que les algorithmes SAT sont déjà considérés comme extrêmement complexes et hautement optimisés, rendant chaque amélioration marginale très difficile à obtenir.
Marijn Heule, président de la compétition SAT et professeur émérite à l'Université Carnegie Mellon, a salué cette avancée :
"AE-Kissat-MAB a réalisé une percée majeure dans la résolution des instances satisfiables."
Ces résultats ouvrent des directions de recherche critiques pour l'optimisation des algorithmes guidée par l'intelligence artificielle.
Date
06 déc 2025
Type
