Projet ANR-15-CE40-0017 – SATAS : SAT comme Service
Programme : Fondements du numérique (DS0704) 2015
Année de financement : 2015
Coordinateur du projet : Monsieur Laurent Simon (Laboratoire bordelais de recherche en informatique)
Partenaires : Laboratoire public; Laboratoire public; Laboratoire public
Montant : 398994.0 euros
Date de début : 2015
Durée : 42 mois
Résumé : Le projet SATaS est un projet ambitieux, qui propose de réaliser des avancées significatives dans l’état de l’art de la résolution du problème SAT, dans les environnements massivement parallèles (“Many Integrated Component” (MIC) et “Cloud computing”). Le projet se focalise notamment sur les problèmes applicatifs que ce type de solution impose. L'objectif final est de fournir une interface SAT en tant que service dans le “cloud”. 
De nombreuses applications critiques se basent aujourd’hui sur les progrès reçents obtenus autour de la résolution pratique de SAT et SAT incrémental. La position centrale de ce problème en informatique permet de faire rejaillir tout progrès obtenu à de nombreux problèmes liés, qu’ils soient plus académiques (Optimisation en Pseudo-Booléens, Satisfaction de Contraintes, Optimisation de contraintes, raisonnement en Intelligence Artificielle, etc…) ou plus liés aux challenges de l’industrie (Bounded Model Checking [Biere’09], Model Checking avec Invariants [Bradley’12], BioInformatique, Analyse Cryptographique, Analyse Statique de code, etc…). Dans ce contexte, la recherche Française a toujours été l’une des forces en pointe. Elle est à l’origine de nombreux succès ces dernières années, et a été fortement présente depuis le tout début (Moteurs SAT, Solveurs CDCL (Conflict Driven Clause Learning) , SAT Parallèle, Survey Propagation, Recherche Tabou, MaxSAT, MinSAT). Cependant, depuis quelques années, le paysage informatique est en train de changer en profondeur, principalement en raison des architectures massivement parallèles (Many Integrated Components, Cloud, etc…). Il y a un risque important, étant données les fortes pressions académiques et industrielles sur ce sujet, que la recherche Française perde sa position privilégiée.
Notre projet propose d’étendre encore la puissance des solveurs SAT grâce à une série d’innovations autour de leur utilisation dans le cadre massivement parallèle.  Notre solution permettra d’attaquer des problèmes de première importance, considérés aujourd’hui comme hors d’atteinte, tout en facilitant grandement leur utilisation. Cela permettra aussi de réduire considérablement les coûts d’un déploiement massif d’un solveur parallèle en proposant un service de paiement “à la consommation”. Nous sommes bien conscient de nous attaquer ici à de nombreux challenges (tant du point de vue SAT que du point de vue Cloud), mais nous avons pris soin dans ce projet de le jalonner de résultats quasi garantis pour en contre-balancer les risques.
Notre plan de travail s’articule autour d’idées fortement innovantes. Nous proposons par exemple d’introduire des structures de données n’ayant pas les mêmes garanties de complétude que les structures actuelles pour la détection des propagations mais tournées intégralement vers le partage efficace de mémoire entre solveurs (la complétude finale du solveur étant quant à elle bien entendu garantie). Nous proposons aussi de nouvelles méthodes de décomposition de problèmes en nous basant sur l’étude de la preuve par résolution que ces derniers génèrent, ou encore sur le passé du solveur sur un problème donné, ce qui tranche clairement avec les méthodes de décomposition habituelles. D’autres tâches traiteront de la consommation énergétique des solveurs SAT ou encore de la parallélisation de SAT dans le cadre incrémental. Enfin, le dernier axe de recherche se focalise bien entendu sur le “cloud” et consiste à proposer une API SAT afin qu’un service SAT puisse être déployé (SAT as a Service), avec tous les challenges que cela implique, autant du point de vue SAT que du point de vue Cloud.