SAT As a Service

The SATAS project started in 2016.

The project, founded by ANR, 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. Formally, the project is named "Projet ANR-15-CE40-0017" in the ANR naming convention.

Updated Dec. 2017

When SAT specialists meet Cloud specialists

Card image cap
INRIA Spiral Team (Lille)

Specialists for the Cloud, with a particular focus on power-aware Cloud deployement, for a new generation of energy efficient SAT solvers

Go to Spirals
Card image cap
CRIL (Lens)

A top A.I. lab in France, with SAT specialists (Glucose, SAT4J, ...), for designing the next generation of distributed SAT solvers, with some application driven goals on the cloud.

Go to the CRIL

Publications (so far)

  • A Recursive Shortcut for CEGAR: Application To The Modal Logic K Satisfiability Problem. J.-M. Lagniez, D. Le Berre, T. de Lima, V. Montmirail. IJCAI 2017: 674-680, 2017.
  • On Selecting Constraints for Replication in Model Checking G. Baud-Berthier and L. Simon. In International Conference on Tools for Artificial Intelligence (ICTAI), 2017.
  • On the Community Structure of Bounded Model Checking SAT Problems G. Baud-Berthier, J. Giráldez-Cru and L. Simon. In International Conference on Theory and Applications of Satisfiability Testing (SAT), 2017.
  • Seeking Practical CDCL Insights from Theoretical SAT Benchmarks. Jan Elffers, Jakob Nordstrom, Laurent Simon, Karem A. Sakallah, in Pragmatics of SAT Workshop, 2016.
  • An adaptive SAT solver. G. Audemard, J.-M. Lagniez, M. Szczepanski and S. Tabary. In principles and practices of Constraint Programming (CP). 2016.
  • A distributed version of Syrup. G. Audemard, J.-M. Lagniez, N. Szczepanski and S. Tabary. In International Conference on Theory and Applications of Satisfiability Testing (SAT), 2017.
  • WattsKit: Software-Defined Power Monitoring of Distributed Systems. M. Colmant, P. Felber, R. Rouvoy, L. Seinturier. In 17th IEEE/ACM International Symposium on Cluster, Cloud and Grid Computing (CCGrid), May 2017, Madrid, Spain. IEEE, pp.10.
  • GenPack: A Generational Scheduler for Cloud Data Centers. A. Havet, V. Schiavoni, P. Felber, M. Colmant, R. Rouvoy, et al. In 5th IEEE International Conference on Cloud Engineering (IC2E), Apr 2017, Vancouver, Canada. IEEE, pp.10.

Softwares (so far)

  • Glucose / Syrup 2017
  • D-Syrup
  • Ampharos
  • Docker image of Glucose
We plan to release all the sofwares here when the project is achieved. In the meanwhile you can contact the coordinator if you want binaries or source files.

The team

L. Simon (Coordinator, Labri), A. Denis (Inria, Bordeaux), R. Fossé (Funded PhD Student, Bordeaux), G. Audemard (CRIL Coordinator), D. Le Berre (CRIL), M. Samy Modeliar (CRIL), C. Piette (CRIL), J.-M. Lagniez (CRIL), J. Lonlac (Funded Post-Doc, CRIL), P. Merle (INRIA Lille Coordinator, SPirals), R. Rouvoy (Spirals), L. Seinturier (Spirals), G. Katsirelos (INRA Toulouse)