Solvers Principles and Architectures


Master level course, 4 ECTS. ENS Rennes 2017/18 (sif)


Syllabus

We attempt to draw the common principles behind a wide range of “solvers” abstracting away momentarily the underlying involved theories. By solver we intend a computer program or algorithm that solves a specific class of problems such as Boolean satisfiability, linear optimization or ideal membership problems. Such solvers are ubiquitous nowadays and are used widely far beyond the community of computer scientists and software engineers. The non existence of decision procedures or the intrinsic high complexity of certain problems do not prevent developing such solvers. On the contrary, they often help better understanding the tackled problems. The main objective of this course is to help students apprehend and somehow deconstruct a given solver into its main components and layers (architecture) as well as its computational paradigms (recursive, sequential, parallel, randomized etc.). We will in addition highlight important implementation aspects such as data structures and heuristics. Indeed, many solvers owe much of their success to smart programming than theoretical breakthroughs. All along the course, recent notable applications of various typical solvers will be discussed as to highlight their broad impact.

Keywords SAT/SMT Solvers, Convex Optimisation, Interior Point Methods, Numerical Methods, Symbolic Computation

Pre-requisite

Licence in mathematics or theoretical computer science or equivalent degree. Basic notions in logic, calculus, linear and abstract algebra, combinatorics and graph algorithms will be required.

Expected Outcome

The main objective of the course would be to reduce as much as possible the opacity of a large class of nowadays routinely used solvers.

Roadmap

  • September 18th. Lecture 0: General Introduction [slides]
  • September 25th. Lecture 1: SAT Solvers [slides]
  • September 27th. Lecture 2: CDCL SAT [slides]
  • October 4th. Lecture 3: BDD and Basic Theories (by David Monniaux). [slides]
  • October 5th. Lecture 4: SMT Solving: DPLL(T) and Beyond (by David Monniaux). [slides]
  • October 9th. Lecture 5: NP-Completeness
  • October 11th. Presentations
  • October 23rd. Lecture 6: Convex Optimization: Simplex Algorithms [slides]
  • October 25th. Presentations
  • November 6th. Lecture 7: Quantifier Elimination (by Assia Mahboubi) [slides]
  • November 8th. Lecture 8: Interior Point Methods/SemiDefinite Programming [slides]
  • November 13th. Presentations

Evaluation

The final score will be composed of three marks:

  1. A research paper to read, summarize and present
  2. A written exam: November 15th, 4:15 – 6:15 PM
  3. A project: a problem/puzzle to solve
    • Proposals by October 31st
    • Paper by the December 11th Latex Template
    • Expected Sections: Introduction, Approach, Results, Related Work, Conclusion

Assignments

  • November 13th
    • BORDAIS Benjamin. The Lagrangian Relaxation Method for Solving Integer Programming Problems [paper]
    • CHAMBRE Mathieu. Solving Non-Linear Arithmetic [paper]
    • PARREAUX Julie. Large-Scale Machine Learning with Stochastic Gradient Descent [paper]
    • THIBAULT Jérémy. An Interior-Point Method for Large-Scale L1-Regularized Least Squares [paper]
  • October 25th
    • BLANLEUIL Arthur. A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses [paper]
    • BIHEL Simon. Lazy Satisfiability Modulo Theories (Chapter6) [paper1][paper2]
    • MARI Thomas. Integrating Simplex with DPLL(T) [paper]
    • HUTIN Rémi. How to Compute Worst-Case Execution Time by Optimization Modulo Theory and a Clever Encoding of Program Semantics [paper]
  • October 11th
    • BAUTISTA Santiago. Conflict Learning and General Resolution [paper]
    • BLANCHE Alexandre. Abstract Satisfaction [paper]
    • DANIEL Lesly-Ann. 2-Literal Watching vs. Head/Tail lists [paper1][paper2]
    • THIBAULT Joan. The Stålmarck’s Method [paper]

Seminar

  • October 5th. 2PM. Markov Room. INRIA. Cell Morphing: From Array Programs to Array-Free Horn Clauses. David Monniaux. [talk]

Internships

Internships (4 to 6 months) on related topics are available.
If interested, let me know as soon as possible.

Further Readings

  • SAT Papers and book Chapters
    • J.P. Marques-Silva and K.A. Sakallah. GRASP: a search algorithm for propositional satisfiability. IEEE Transactions on Computers. 1999 [pdf]
    • Moskewicz et al. Chaff: Engineering an Efficient SAT Solver. DAC 2001. [pdf]
    • Zack Newsham et al. SATGraf: Visualizing the Evolution of SAT Formula Structure in Solvers. SAT 2015 [pdf]
    • Hadi Katebi et al. Empirical Study of the Anatomy of Modern Sat Solvers. SAT 2011 [pdf]
    • Marques-Silva, Lynce and Malik. Conflict-Driven Clause Learning SAT Solvers. Chapter 4 of the Handbook of Satisfiability [pdf]
    • D. Knuth draft on SAT Solvers [tarball]
  • SMT
    • De moura and Bjorrner. Satisfiability modulo theories: introduction and applications. Communications of the ACM 2011. [pdf]
    • Nieuwenhuis, Oliveras, and Tinelli. Solving SAT and SAT Modulo Theories: From an abstract Davis–Putnam–Logemann–Loveland procedure to DPLL(T). JACM 2006. [pdf]
    • Barrett, Sebastiani, Seshia and Tinelli. Satisfiability Modulo Theories. Chapter 26 of the Handbook of Satisfiability. [pdf]
  • NP-Completeness
    • Michael R. Garey and David S. Johnson. Computers and intractability: a guide to the theory of NP-Completeness

Office Hours

  • Thursday 2–4 PM (Inria)
  • For any request/question, feel free to email me (see address below)