Sat Competition

 Ce qu’il faut savoir

Selon son site officiel, la « SAT Competition », « SAT Race »  ou  « SAT Challenge » selon les années et les organisateurs, est un concours ouvert depuis 1992 aux meilleurs mathématiciens et informaticiens du monde entier. C’est un évènement satellite à la « SAT Conference » qui se tient annuellement. Le concours porte sur la résolution d’un problème classique de l’intelligence artificielle dit de  satisfiabilité propositionnelle. Cette approche dite de satisfiabilité propositionnelle permet de résoudre un problème après l’avoir transformé en une série de questions, auxquelles on répondrait seulement par vrai ou par faux.  Cette approche permet de modéliser de nombreux problèmes en contraintes booléennes, appelées clauses, constituées de variables ayant deux valeurs possibles, vrai ou faux. Les solveurs SAT sont alors utilisés pour déterminer automatiquement l’existence d’une solution ou pour démontrer automatiquement l’absence de solution. Au début des compétitions SAT, dans les années 90, les meilleurs solveurs pouvaient résoudre un problème limité à quelques centaines de variables, contre plusieurs centaines de milliers, voire millions aujourd’hui. Cette amélioration significative a été favorisée par deux facteurs notamment : l’accroissement des performances des ordinateurs (en termes de puissance de calcul et de capacité de mémorisation) et  l’intégration de diverses technologies issues de l’intelligence artificielle dans les solveurs,  telles que l’heuristique de branchement et  l’apprentissage par renforcement.

Avant le début de la compétition, des partenaires académiques et industriels soumettent aux organisateurs des jeux de données sur des problèmes qu’ils ont déjà modélisés. Pendant la compétition, qui dure en moyenne un mois, les solveurs sont évalués sur la vitesse à laquelle ils résolvent les instances SAT et la véracité de leurs réponses. Tout solveur produisant une mauvaise réponse  est éliminé. Un programme indépendant évalue automatiquement les performances des solveurs et les classe par piste et par ordre de mérite.

Le nombre de solveurs ayant concouru en 2022 est de 64. C’est à ce concours-là que Rodrigue Konan Tchinda et Clémentin Tayou Djamegni, respectivement enseignant–chercheur à l’UBa  et Chef du Département de Génie Informatique à l’IUT-FV de l’UDs, se sont présentés. Il convient de le noter, ceux qui occupent généralement une place au podium dans cette compétition sont affiliés aux laboratoires des pays dits développés. Pour la cinquième fois consécutive l’UDs accède au podium de cette compétition scientifique internationale.