SAT Race 2019 

L’Équipe de l’UDs à nouveau sur le podium des champions mondiaux d’informatique

Dschang,SIC/UDs 27/07/19. Rodrigue Konan Tchinda, doctorant de 3^e année en informatique à 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 d’informatique au niveau international depuis le 12 juillet 2019. Les deux lauréats ont remporté à Lisbonne au Portugal, le prix de la sous-piste « UNSAT » de la « SAT Race  2019 », juste derrière Stepan Kochemazov, Oleg Zaikin, Victor Kondratiev, Alexander Semenov de la Matrosov Institute for System Dynamics and Control Theory of Siberian Branch of Russian Academy of Sciences de Russie et de la National Research Irkutsk State Technical University de Russie, et Md Solimul Chowdhury, Martin Müller et Jia-Huai You de l’Université d’Alberta au  Canada. La Compétition SAT confronte chaque année les solveurs proposées 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 (http://sat-race-2019.ciirc.cvut.cz), 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 informaticiens du monde entier, comme évènement satellite à la SAT Conférence 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 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 Race 2019, chaque solveur a été confronté à quatre cent instances, et reçu cinq mille secondes (environ 1h38mn) pour résoudre une instance. Ce qui fait un total de deux millions de secondes (environ vingt-trois jours) pour résoudre les quatre cent  instances. 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 quatre solveurs basés sur leurs techniques appelées PSIDS (Polarity State Independent Decaying Sum) et PADC (Periodic Aggressive learned clause Database Cleaning): PADC_MapleLCMDistChronoBT, PADC_Maple_LCM_Dist, PADC_MapleLCMDistChronoBT-nbIncRedDB_5_CT_0,et PSIDS_MapleLCMDistChronoBT.  L’édition 2019 a vu la participation de  55 solveurs tous concourant dans une seule piste elle-même subdivisée en trois sous-pistes : « SAT », « UNSAT » et « SAT+UNSAT ». Les sous-pistes « SAT » et « UNSAT » visaient à déterminer les meilleurs solveurs respectivement dans la résolution des instances satisfiables et insatisfiables tandis que la sous-piste « SAT+UNSAT » déterminait le meilleur dans la résolution générale indépendamment de la satisfiabilité ou l’insatisfiabilité des instances.

Les quatre solveurs de l’équipe de Dschang ont été classés respectivement vingtième, douzième, dixième et neuvième sur un total de cinquante-cinq solveurs dans la sous-piste « SAT+UNSAT ». Dans la sous-piste UNSAT, le quatrième solveur, PSIDS_MapleLCMDistChronoBT, a été classé 3^e  sur un effectif total de cinquante et cinq solveurs, remportant ainsi le troisième prix de cette sous-piste. 

Ainsi que l’affirme le Clémentin Tayou Djamegni, 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 (https://www.univ-dschang.org/sat-competition-2018/) et en 2019 ont fait leurs travaux à 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.

Parmi les responsables de l’organisation de l’édition 2019 se trouvaient d’imminents chercheurs dont les contributions dans la résolution de SAT sont des plus significatives : Marijn Heule (The University of Texas at Austin, USA), Matti Järvisalo (University of Helsinki, Finland) et Martin Suda (Czech Technical University in Prague, Czech Republic). Ceux-ci ont structuré la compétition en une unique piste, constituée de trois sous-pistes non révélées aux participants ni avant ni pendant la compétition, dont la sous-piste « UNSAT » à laquelle a pris part l’équipe de l’UDs. Contrairement aux autres pistes, la « UNSAT » a la particularité d’éprouver les solveurs sur leur aptitude à démontrer automatiquement l’insatisfiabilité d’un ensemble de contraintes en fournissant un certificat numérique dont la taille est généralement de l’ordre du Giga-octets./ CTD