SATAS - SAT comme Service

Coordinateur : Laurent Simon (Laboratoire bordelais de recherche en informatique)
Partenaire : Inria Lille - Nord Europe CRIStAL

Équipe : Spirals du Groupe Thématique : GL.

Dates : 09/2015 - 03/2019

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.

Abstract :

The SATAS project is an ambitious project, which aims to advance the state of the art in massively parallel SAT solving with a particular eye to the applications driving progress in the field. The final goal of the project is to be able to provide a “pay as you go” interface to SAT solving services, with a particular focus on its power consumption. This project will extend the reach of SAT solving technologies, daily used in many critical and industrial applications, to new application areas, which were previously considered too hard, and lower the cost of deploying massively parallel SAT solvers on the cloud.
Many critical applications are daily relying on the recent and constant progress made around SAT and incremental SAT Solving. The central position of SAT in computer science makes most of its techniques pioneering and pushing the state of the art of many related academic fields (Pseudo-Boolean Optimization, Constraint Satisfaction Problems, Constraint Optimization ones, Reasoning in Artificial Intelligence, etc.) but also many industrial and critical problems (Bounded Model Checking [Biere’09], Model Checking with Invariants [Bradley’12], BioInformatics, Cryptanalysis, Static Code Analysis, etc.). The French research community has been one of the leading forces in the development of this success story over the recent years. It has been on the front of the SAT research since the very beginning : Core SAT engines, CDCL Solvers (Conflict-Driven Clause Learning), Parallel SAT, Survey Propagation (which has been proposed by French physicists), Tabu Search, MaxSAT, MinSAT. However, since a few years, the landscape is quickly changing, due to the birth of massively parallel architectures (Many Integrated Components, Clouds, etc.). There is a high risk, given the very important pressure around practical solving of SAT that has never been so high, that French researchers could lose their leadership in this time of algorithmic paradigm changes.
In this project, we aim at extending the reach of SAT solving technologies to new application areas, which were previously considered too hard, and lower the cost of deploying massively parallel SAT solvers by making it a “pay as you go” service. The scientific challenge behind this project is important and has clearly a high risk counterpart (both from a SAT and a Cloud perspective). However, it also has important return values and we carefully added almost-guaranteed results to balance the risks.
Our workplan is based on strong innovative ideas. For instance, we propose to study non-locking data structures for massive sharing of clauses, or to work on new way of decomposing the search by looking back at the solver past. We push forward our new envision of solvers, by considering them as proof-generators rather than backtrack searches algorithms. This will allow us to propose a speculative way of building proof that may get rid of some limitations of all current parallel solvers. At a lower level, we propose to study how an efficient data structure for sharing clause can be proposed. We will also work on all the scientific aspects of deploying search algorithms on the cloud (locality of virtual node, splitting and merging the search, running on a set of unknown architectures). Our project is, directly or not, addressing some important open problems in the field.