SAT COMPETITION 2020

L’Équipe de l’UDs Sacrée Vice-Championne du Monde de Math-Info

Dschang,UDs/SIC-17/07/20.Rodrigue Konan Tchinda, doctorant en Informatique, et attente de soutenance, à la Faculté des Sciences, et Clémentin Tayou Djamegni, chef de 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 2020. Les deux lauréats ont remporté à Alghero, en Italy, le deuxième prix, médaille d’argent, de la piste « Parallel Track SAT » de la « SAT COMPETITION 2020 », juste derrière l’équipe française constituée de Vincent Vallade, Ludovic Le Frioux, Souheib Baarir, Julien Sopena et Fabrice Kordon, du Laboratoire d’Informatique de Paris 6 (LIP 6), Campus Pierre et Marie Curie,  Sorbonne Université, et devant l’équipe chinoise constituée de Zhihui Li, Guanfeng Wu, Yanh Xu et Qingshan Chen, de School of Computer Science and Engineering, University of New South Wales (UNSW), Sydney, Australia, de School of Information Science and Technology, Southwest Jiaotong University, Chengdu 610031, Sichuan, P.R. China, et de National-Local Joint Engineering Laboratory of System Credibility Automatic Verification, Southwest Jiaotong University, Chengdu 610031, Sichuan, P.R. China. L’équipe française était conduite par Prof Fabrice Kordon, Directeur du LIP6. La compétition SAT confronte chaque année au niveau mondial les solveurs 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 du concours (https://satcompetition.github.io/2020/), 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. 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 souvent de l’ordre de  quelques millions de contraintes portant sur des centaines de milliers de variables. A la SAT  Competition 2020, 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.

L’étudiant et son maître ont proposé à ce concours international un solveur dans la piste « Parallel Track SAT ». Le solveur de l’Université de Dschang, baptisé  ExMapleLCMDistChronoBT, a été classé 2e, remportant ainsi le deuxième prix de cette piste. Ce solveur est une évolution du solveur  parallèle de l’équipe de l’UDs qui avait qui n’avait pas remporté de prix (classé 4e) à la SAT COMPETITION 2018.

La piste « Parallel Track SAT » à la particularité de requérir des compétences pointues en intelligence artificiel et en calcul parallèle.  L’intelligence artificielle est une branche de l’informatique qui étudie l’ensemble des techniques permettant aux machines de simuler l’intelligence naturelle, c’est à dire d’accomplir des tâches et de résoudre des problèmes normalement réservés aux humains et à certains animaux. La simulation de l’intelligence naturelle impliquent généralement des algorithmes complexes et gourmands en termes de consommation des ressources de calcul et mémoire. De ce fait, les temps simulation de l’intelligence naturelle sont souvent inacceptables/prohibitifs sur les ordinateurs séquentiels. Or, la puissance de calcul des ordinateurs séquentiels est limitée par des contraintes physiques telles que la nature des composants électroniques et la vitesse de propagation des signaux. Devant ces contraintes physiques et face aux besoins de ressources de calcul et mémoire de plus en plus élevées pour la résolution des problèmes complexes, le parallélisme apparaît comme une solution réaliste et prometteuse. Le calcul parallèle est basé sur le  paradigme  « l’union fait la force ». Ce paradigme se traduit concrètement par la duplication des unités de calcul et mémoire. Les machines massivement parallèles sont constitués d’un très grand nombre de processeurs, ce nombre allant d’au moins cent processeurs à quelques dizaines de milliers.

Ainsi que l’affirme Prof Tayou, si 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/), 2019 à Pragues (https://www.univ-dschang.org/sat-race-2019/) et 2020 à Alghero ont fait leurs travaux à l’Université de Dschang. L’étudiant, en particulier, n’a pas encore eu l’occasion de faire le laboratoire dans une quelconque université ou centre de recherche étranger. De plus, c’est la première fois qu’une équipe africaine se hisse à ce niveau dans le classement mondial de référence sur SAT.

Parmi les responsables de l’organisation de l’édition 2020 se trouvaient d’imminents chercheurs dont les contributions dans la résolution de SAT sont des plus significatives :Marijn Heule (Carnegie Mellon University at Pittsburgh, USA), Matti Jarvisalo (University of Helsinki, Finland), Martin Suda (Czech Technical University in Prague, Czech Republic), Markus Iser (Karlsruhe Institute of Technology, Germany),Tomas Balyo (CAS Software Karlsruhe, Germany) et Nils Froleyks (Johannes Kepler University, Linz).