SAT COMPETITION 2021

La démystification : l’UDs première équipe africaine sacrée double championne du monde de Math-Info

Bandjoun,SIC/UDs-03/07/21.Rodrigue Konan Tchinda, enseignant – chercheur et Clémentin Tayou Djamegni, chef du Département de Génie Informatique à l’Institut Universitaire de Technologie Fotso Victor de l’Université de Dschang, font à nouveau partie des champions de math-info au niveau international depuis le 09 juillet 2021. Les deux lauréats ont remporté à Barcelone, en Espagne, deux médailles d’or et une médaille de bronze, notamment le premier prix de chacune des pistes  « Parallel Track SAT » et « Main Track UNSAT »,  et le troisième prix de la piste  « Parallel Track ALL » de la « SAT COMPETITION 2021 ».

Dans la piste « Parallel Track SAT », les deux lauréats ont remporté le titre de champion respectivement devant Norbert Manthey de « International Center for Computational Logic, Germany » et Dominik Schreiber de « Karlsruhe Institute of Technology, Germany et de Institute of Theoretical Informatics, Algorithm Engineering, Germany ».

Quant à la piste « Main Track UNSAT », les deux lauréats ont remporté le titre de champion respectivement devant l’équipe chinoise constituée de Xindi Zhang et Shaowei Cai de « Institute of Software, Chinese Academy of Sciences », et de Zhihan Chen de « School of Automation, Chongqing University, China », et l’équipe australienne dirigée par Armin Biere de « Institute for Formal Models and Verification, Johannes Kepler University, Austria ».

Sur la piste « Parallel Track ALL », les deux lauréats ont remporté le titre de deuxième vice-champion derrière  l’équipe franco-canadienne constituée de  six chercheurs du « Laboratoire d’Informatique de Paris 6 (LIP 6), Campus Pierre et Marie Curie,  Sorbonne Université », Vincent Vallade, Ludovic Le Frioux, Razvan Oanea, Souheib Baarir, Julien Sopena, et Fabrice Kordon, et de deux chercheurs de « University of Waterloo, Canada », Saeed Nejati  et Vijay Ganesh, et l’équipe allemande dirigée par Dominik Schreiber.  L’équipe franco-canadienne était coachée conjointement par Prof  Fabrice Kordon, Directeur du LIP6, et  Prof Vijay Ganesh,  Directeur du « Waterloo Artificial Intelligence Institute, Canada ». La compétition SAT met aux prises chaque année au niveau mondial les solveurs SAT, programmes informatiques de résolution du problème SAT,  proposés par les chercheurs dans l’objectif de repousser les limites de la science et de la technologie par la créativité et l’innovation.

Selon le site officiel de ce concours international (https://satcompetition.github.io/2021/), la Compétition SAT (baptisée « 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, comme évènement satellite à la « SAT Conference » qui se tient annuellement. Il porte sur la résolution d’un problème classique de l’intelligence artificielle dit de  satisfiabilité propositionnelle. La difficulté est de démontrer automatiquement soit la satisfiabilité, soit l’insatisfiabilité d’un ensemble de contraintes appelé instance dans un temps raisonnable et en utilisant une taille raisonnable de mémoire informatique. C’est pourquoi les solveurs sont évalués sur leurs capacités à résoudre efficacement des ensembles de contraintes dans une limite de ressources fixée portant sur le temps et la mémoire. La complexité d’une instance est souvent prohibitive puisqu’elle est généralement de l’ordre de  quelques millions de contraintes portant sur des centaines de milliers de variables. A la SAT  Competition 2021, comme lors des éditions précédentes, chaque solveur a été confronté à  plusieurs instances pendant près d’un mois. Chaque solveur est tenu de fournir à chaque fois un certificat numérique attestant de la validité de sa réponse. Ce certificat est vérifié par un programme indépendant afin de déterminer si la réponse fournie par le solveur est correcte. Tout solveur produisant une mauvaise réponse ou un mauvais certificat pour sa réponse est éliminé de la compétition. Après avoir confronté les solveurs  à des problèmes difficiles pendant environ un mois, un programme indépendant évalue automatiquement les performances des solveurs et les classe en fonction des meilleurs temps mis et mémoire utilisé. Le nombre de solveurs ayant concouru est de 64. C’est à ce concours-là que Dr. Konan et Prof Tayou se sont présentés.

Les deux chercheurs de l’IUT-FV ont proposé  à ce concours international deux principaux solveurs, notamment   PaKis et hKis_unsat.  Le solveur hKis_unsat est une évolution du solveur  de l’équipe de l’UDs qui avait remporté le troisième prix de la piste  « UNSAT » de la « SAT Race  2019 ». C’est ce solveur qui a remporté le premier prix de la piste « Main Track UNSAT ».  Le solveur  PaKis  est une évolution du solveur parallèle de l’équipe de l’UDs qui avait remporté le deuxième prix de la piste « Parallel Track SAT » de la « SAT COMPETITION 2020 » et d’un autre solveur parallèle de l’équipe de l’UDs qui avait remporté de prix (classé 4e) à la SAT COMPETITION 2018. C’est  ce solveur qui a remporté le premier prix de la piste « Parallel Track SAT »  et le troisième prix de la piste  « Parallel Track ALL ».

Ainsi que l’affirment les deux double-champions, ceux qui occupent généralement une place au podium dans cette compétition sont des chercheurs issus des laboratoires des pays dits développés. L’on remarque que les deux camerounais qui y ont accédé en 2018 à Oxford (https://www.univ-dschang.org/sat-competition-2018/), en 2019 à Pragues (https://www.univ-dschang.org/sat-race-2019/), en 2020 Alghero (https://www.univ-dschang.org/sat-competition-2020/)  et en 2021 à Barcelone ont fait leurs travaux de recherche  à l’Université de Dschang.  De plus, à la SAT Compétition, c’est par l’équipe de l’UDs que l’Afrique a obtenu ses deux premières médailles de bronze, en 2018 et en 2019, sa première médaille d’argent en 2020, ses deux premières médailles d’or et sa troisième médaille de bronze en 2021