DS0704 - Fondements du numérique

SAT As a Service – SATAS

Submission summary

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.

Project coordination

Laurent Simon (Laboratoire bordelais de recherche en informatique)

The author of this summary is the project coordinator, who is responsible for the content of this summary. The ANR declines any responsibility as for its contents.


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

Help of the ANR 398,993 euros
Beginning and duration of the scientific project: September 2015 - 42 Months

Useful links

Explorez notre base de projets financés



ANR makes available its datasets on funded projects, click here to find more.

Sign up for the latest news:
Subscribe to our newsletter