SAT As a Service – SATAS

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.