Deux médailles d’or pour l’équipe COALA du LIS à la compétition SAT 2021
La résolution d’un problème demande tout d’abord de le formuler, ce qui peut se faire sous la forme d’un problème de satisfaisabilité booléenne (SAT). Basée sur la logique propositionnelle, cette approche est de plus en plus prisée par les mondes académiques et industriels. Des chercheurs de l’équipe Contraintes algorithmes et applications (COALA) du Laboratoire d'Informatique et Systèmes (LIS - CNRS/Aix-Marseille Université) ont remporté deux médailles d’or lors de la compétition internationale SAT 2021, où leur solveur Kissat-MAB a particulièrement brillé par sa capacité à prouver l’existence de solutions aux problèmes SAT.
Dans quelle mesure peut-on résoudre un problème en le transformant en une série de questions, auxquelles on répondrait seulement par vrai ou par faux ? Cette approche est désignée sous le nom du problème de satisfaisabilité booléenne, abrégé en problème SAT. Ce problème est à la fois important en intelligence artificielle et pour la théorie de la complexité, une branche de l’informatique théorique qui scrute le temps et les ressources nécessaires à un algorithme pour remplir sa mission.
De nombreux défis de l’industrie sont abordés de cette manière : vérification et conception de circuits intégrés et de logiciels, cryptographie, bio-informatique, etc. Le problème SAT est également employé dans le monde de la recherche pour traiter des problèmes académiques, tels que la planification et le calcul de décompositions (hyper)arborescente d’un graphe.
« SAT permet de modéliser très simplement divers problèmes : les variables n’ont que deux états possibles, vrai ou faux, sur lesquels s’expriment des contraintes (clauses), explique Djamal Habet, professeur à Aix-Marseille Université et membre du LIS dans l’équipe Contraintes algorithmes et applications (COALA). En revanche, les instances du problème SAT peuvent être difficiles à résoudre, c’est-à-dire déterminer si elles possèdent bien une solution, au point que, dans le pire des cas, leur résolution nécessite un temps exponentiel. »
On emploie alors un solveur, un algorithme chargé de déterminer l’existence d’une solution et de trouver la valeur des variables. Plus la machine sur laquelle le solveur est exécuté est puissante, et plus cela va vite. Soulignons cependant que l’amélioration des algorithmes et des techniques de résolution employées a eu un effet bien plus déterminant sur les performances des solveurs SAT.
La conception de solveurs SAT est devenue une des spécialités de l’équipe COALA du LIS. Leur dernière contribution, Kissat-MAB, se démarque par l’emploi d’une heuristique de branchement original. « Du point de vue de l’intelligence artificielle, les heuristiques permettent de représenter une forme d’intuition capable d’aider l’algorithme à remplir sa mission », précise Cyril Terrioux, maître de conférences à Aix-Marseille Université et membre de l’équipe COALA au LIS.
« La manière la plus naïve de résoudre une instance SAT est de tester toutes les valeurs possibles, ce qui est clairement inefficace car cela nécessite un temps de calcul qui croît exponentiellement avec le nombre de variables, poursuit Djamal Habet. Tout mauvais choix lors de cette exploration est susceptible d’allonger la durée de la résolution. Avec Kissat-MAB, nous proposons une combinaison basée sur l’apprentissage automatique de deux heuristiques de branchement. Elle permet de sélectionner la variable de décision la plus pertinente possible à chaque étape d’un algorithme de type CDCL1 . »
Cette approche, utilisant l’apprentissage par renforcement, facilite la résolution du problème SAT. Après la publication d’un article scientifique dans la conférence internationale de référence CP 2021 sur cette méthode, Kissat-MAB a été présenté à l’édition 2021 de la prestigieuse compétition internationale SAT. Il y a remporté deux médailles d’or, en particulier dans la catégorie reine, face à une quarantaine de solveurs participant à cette vingtième édition.
- 1Conflict-driven clause learning.
Des partenaires académiques et industriels soumettent des jeux de données liées à des problèmes qu’ils ont déjà modélisés. Les solveurs sont testés sur la vitesse à laquelle ils résolvent l’instance SAT tout en donnant le certificat correspondant, si une réponse est donnée. Les compétiteurs peuvent choisir entre plusieurs catégories. Kissat-MAB a remporté une première médaille d’or dans la « SAT and UNSAT Main Track », dans laquelle les instances possèdent ou non des solutions, ainsi qu’une deuxième médaille d’or dans la « SAT Main Track » consacrée aux instances possédant une solution.
« La compétition est tellement rude que, chaque année, on devance de peu le solveur qui a gagné l’édition précédente, décrit Sami Cherif, doctorant au LIS sous la direction de Djamal Habet. Ce n’est pas simple d’améliorer des solveurs déjà compétitifs, mais c’est important d’inciter les gens à chercher la performance en utilisant également toute la théorie qu’il y a derrière le problème SAT. »