Solvers Principles and Architectures


Master level course, 4 ECTS. UR1 / ENS Rennes 2018/19 (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

General Introduction [slides]

Part 1: Anatomy of SAT/SMT Solvers [slides (SAT),slides (SMT)]]

  • September 17th. Lecture 1: Propositional Logic (Room B12D-i60)
  • September 19th. Lecture 2: DPLL/CDCL Solvers (Room B12D-i60)
  • October 1st. Lecture 3: SAT Modulo Theories (Room B12D-i53)
  • October 3rd. Presentations (Room B12D-i57)

Part 2: Convex Optimization [slides]

  • October 8th. Lecture 4: Linear Programming (Simplex Algorithm) (Room B12D-i51)
  • October 10th. Seminar 1: First steps in the formalization of convex polyhedra in Coq. By Xavier Allamigeon [slides] (Room B12D-i51)
  • October 15th. Lecture 5: Interior Point Methods (Room B12D-i53)
  • October 17th. Lecture 6: SemiDefinite Programming (Room B12D-i53)
  • October 22th. Presentations (Room B12D-i58)

Part 3: Quantifier Elimination

  • October 24th. Lecture 7: Quantifiers Over Real Closed Fields (Room B12D-i58)
  • November 5th. Seminar 2: Certified Convex Programming. By Victor Magron [slides] [Maple Worksheet] (Room B12D-i53)
  • November 7th. Lecture 8: Cylindrical Algebraic Decomposition (Room B02B-E110)
  • November 12th. Presentations (Room B02B-E110)

  • November 14th. Final Exam (Room B12D-i58)

Evaluation

The final score will be composed of three marks:

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

Assignments

  • Due date November 12th.
    • BARBIER Guillaume. On SAT Modulo Theories and Optimization Problems. [paper]
    • BELLIER Dylan. An Interior-Point Method for Large-Scale L1-Regularized Least Squares [paper]
    • CLEMENT Emily (PhD). ongoing work
    • HENRY Léo (PhD). ongoing work
    • JOUVE Jean. Large-Scale Machine Learning with Stochastic Gradient Descent [paper]
    • KOSKAS Nathan. Solving Non-Linear Arithmetic [paper]
    • LEGRAN-DUCHESNE Clément. Global Optimization with Polynomials and the Problem of Moments [paper]
    • THOMAS Bastien. The Lagrangian Relaxation Method for Solving Integer Programming Problems [paper]
  • Due date October 22nd.
    • BAUDON Thais. Integrating Simplex with DPLL(T) [paper]
    • GOUGEON Quentin. A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses [paper]
    • LE BON Kévin (PhD). ongoing work
    • MESCOFF Guillaume. Constraint Programming: In Pursuit of the Holy Grail [paper]
    • PEIGNIER Joshua. dReal: An SMT Solver for Nonlinear Theories over the Reals [paper]
    • SINGH Rituraj (PhD). ongoing work
  • Due date October 3rd.
    • BARRIERE Aurèle. Conflict Learning and General Resolution [paper]
    • FERRY Corentin. Symbolic model checking using SAT procedures instead of BDDs [paper]
    • FREIRE Marco. The Stålmarck’s Method [paper]
    • LEQUEN Arnaud. A New Metho d for Solving Hard Satisfiability Problems [paper]
    • LEGRAND LIXON Clément. 2-Literal Watching vs. Head/Tail lists [paper1][paper2]
    • MIRLIAZ Solène. Abstract Satisfaction [paper]

Seminars

  1. October 10th. 4PM. Room: B12D-i51 (ISTIC).
    • Speaker: Xavier Allamigeon [slides]
    • Title: First steps in the formalization of convex polyhedra in Coq.
    • Abstract: We present the foundations of our project “Coq-Polyhedra” aiming at formalizing convex polyhedra in the proof assistant Coq. The originality of our approach lies in the fact that our formalization is carried out in an effective way, in the sense that the basic predicates over polyhedra (emptiness, boundedness, membership, etc) are defined by means of Coq programs. All these predicates are then proven to correspond to the usual logical statements. To this end, we make an extensive use of the Boolean reflection methodology which was developed in the proof of Feit-Thompson Theorem by Gonthier et al. Our effective approach allows to overcome the intuitionistic nature of the logic used by Coq, and is made possible by implementing the simplex method (Phase I and Phase II) inside the proof assistant. Termination is proved by using the lexicographic pivot rule of Dantzig et al. In this way, we easily arrive at the proof of important results on polyhedra, such as several versions of Farkas Lemma, duality theorem of linear programming, separation from convex hulls, Minkowski Theorem, etc. We finally report on recent progress on the formalization of faces. This is joint work with Ricardo D. Katz (CIFASIS-CONICET, Argentina).
  2. November 5th. 4PM. Room B12D-i53 (ISTIC).
    • Speaker: Victor Magron [slides] [Maple Worksheet]
    • Title: Certifying Non-negativity with Lasserre’s Hierarchy and Semidefinite Programming.
    • Abstract: Certification and validation of computational results is a major issue for modern sciences raising challenging problems at the interplay of mathematics and computational aspects of computer science. One can emphasize in this context several applications arising in the design of modern cyber-physical systems with a crucial need of certification and information extraction. In particular, one tries to avoid incidents such as the Patriot missile crash in 1991, the FDIV Pentium bug in 1994 or more recently the collision of Google’s self-driving car in 2016. These issues give rise to many mathematical problems. Polynomial optimization (which consists in computing the infimum of a polynomial function under algebraic constraints) is one of the most important, difficult and challenging one. The emergence of this exciting new field goes back to the last decade and has led to striking developments from a cross fertilization between (real) algebraic geometry, applied mathematics, theoretical computer science and engineering. The backbone of this powerful methodology is the “moment-SOS” approach, also known as “Lasserre hierarchy”. In the first part of this talk, I will introduce Lasserre’s hierarchy and explain how to handle polynomial optimization problems while relying on numerical optimization and semidefinite programming. In the second part of this talk, I will explain how to construct exact non-negativity certificates with hybrid symbolic-numeric algorithms. The presentation will include modern motivating applications as well as software demonstration with the RealCertify package.

Previous Exams

Internships

Internships (4 to 6 months) on related topics are available.

  • Formalisation des polyèdres dans l’assistant de preuve Coq [pdf]
  • Extracting Information from Moments: Christoffel Polynomial and Gibbs Phenomenon [pdf]
  • Exact Certificates for Noncommutative Polynomial Optimization [pdf]
  • Exact Semidefinite Approximations of Continuous Reachable Sets [pdf]

The TCS Group at KTH Royal Institute of Technology invites applications for a PhD position in CS focusing on algorithms for solving the Boolean satisfiability problem (SAT) very efficiently for large classes of instances, and on analyzing and understanding such algorithms. [More here]

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)