DS0704 - Fondements du numérique

SAT comme Service – SATAS

Résumé de soumission

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.

Coordinateur du projet

Monsieur Laurent Simon (Laboratoire bordelais de recherche en informatique)

L'auteur de ce résumé est le coordinateur du projet, qui est responsable du contenu de ce résumé. L'ANR décline par conséquent toute responsabilité quant à son contenu.

Partenaire

Inria Inria Lille - Nord Europe
LaBRI Laboratoire bordelais de recherche en informatique
CRIL Centre de Recherche en Informatique de Lens

Aide de l'ANR 398 993 euros
Début et durée du projet scientifique : septembre 2015 - 42 Mois

Liens utiles

Inscrivez-vous à notre newsletter
pour recevoir nos actualités
S'inscrire à notre newsletter