ANR SATAS
SAT en tant que service
Projet impliquant les laboratoires CRIL, CRIStAL (Lille), INRA (Toulouse) et LaBri (Bordeaux, investigateur principal).
Le projet SATAS est un projet ambitieux, qui vise à faire avancer l’état de l’art dans la résolution massivement parallèle de SAT, avec un regard particulier sur les applications qui font progresser le domaine. L’objectif final du projet est de pouvoir fournir une interface “pay as you go” aux services de résolution de SAT, avec une attention particulière à la consommation d’énergie. Ce projet permettra d’étendre la portée des technologies de résolution SAT, utilisées quotidiennement dans de nombreuses applications critiques et industrielles, à de nouveaux domaines d’application, qui étaient auparavant considérés comme très difficiles, et de réduire le coût du déploiement de solveurs SAT massivement parallèles sur le cloud. De nombreuses applications critiques s’appuient quotidiennement sur les progrès récents et constants réalisés autour du SAT et de la résolution SAT incrémentale. la résolution SAT incrémentale. La position centrale de SAT dans l’informatique fait que la plupart de ses techniques sont pionnières et font avancer l’état de l’art dans de nombreux domaines académiques connexes (optimisation pseudo-booléenne, problèmes de satisfaction de contraintes, etc.), mais aussi de nombreux problèmes industriels et critiques (Vérification des Modèles Bornés [B iere'09] , Vérification des Modèles avec Invariants [B radley'12] , BioInformatique, Cryptanalyse, Analyse Statique de Code, etc.)
La communauté de recherche française a été l’un des principaux acteurs de cette réussite au cours des dernières années. Elle a été à l’avant-garde de la recherche sur le SAT depuis le tout début : moteurs SAT de base, solveurs CDCL(Conflict Driven Clause Learning), SAT parallèle, Recherche Tabou, MaxSAT,etc. Cependant, depuis quelques années, le paysage est en train de changer rapidement, en raison de la naissance d’architectures massivement parallèles (composants intégrés, Clouds, etc.). Il existe un risque élevé, étant donné la pression très importante autour de la résolution pratique du SAT qui n’a jamais été aussi élevée, que les chercheurs français perdent leur leadership en cette période de changements de paradigmes algorithmiques.
Dans ce projet, nous visons à étendre la portée des technologies de résolution SAT à de nouveaux domaines d’application, qui étaient auparavant considérés comme trop difficiles, et à réduire le coût de déploiement des solveurs SAT massivement parallèles en faisant un service “pay as go”. Le défi scientifique à l’origine de ce projet est important et présente clairement une contrepartie à haut risque (tant du point de vue SAT que du Cloud). Cependant, il présente également d’importantes valeurs de rendement et nous avons soigneusement ajouté des résultats presque garantis pour équilibrer les risques.
Notre plan de travail est basé sur des idées novatrices fortes. Par exemple, nous proposons d’étudier les structures de données non verrouillées pour le partage massif de clauses, ou de travailler sur une nouvelle façon de décomposer la recherche en regardant le passé du solveur. Nous mettons en avant notre nouvelle vision des solveurs, en les considérant comme des générateurs de preuves plutôt que des retour en arrière(backtrackers). Cela nous permettra de proposer une manière spéculative de construire des preuves qui pourrait se débarrasser de certaines limitations des solveurs parallèles actuels. A un niveau plus bas, nous étudions comment une structure de données efficace pour le partage de clause peut être proposée. Nous travaillerons également sur tous les aspects scientifiques du déploiement d’algorithmes de recherche sur le cloud (localité du nœud virtuel, division et fusion de la recherche, exécution sur un ensemble d’architectures inconnues). Notre projet permet de résoudre directement ou non d’importants problèmes ouverts dans ce domaine.
Visiter la page web du projet.