Solvers Principles and Architectures

Master level course, 4 ECTS. UR1 / ENS Rennes 2019/20 (sif)

Syllabus

A solver is 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 understand the core therories and concepts behind three important classes of problems and their related solvers, namely Boolean Satisfiability, Convex Optimization, and Quantifier Elimination.

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 tricks 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, Semi-Definite Programming, Quantifier Elimination

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 (tentative)

General Introduction

  • September 18th 5:15 PM (instead of 4:15 PM) for 1h only (Room B12D i-58) [slides]

Part 1: Anatomy of SAT/SMT Solvers [SAT,SMT,AI]

  • September 23rd. Lecture 1: Propositional Logic (Room B12D-i59)
  • September 25th. Lecture 2: DPLL/CDCL Solvers (Room B12D-i59)
  • September 30th. Lecture 3: SAT Modulo Theories (Room B12D-i58)
  • October 2nd. TD/Office hours (Room B12D-i58)

Part 2: Convex Optimization [slides]

  • October 7th. Lecture 4: Linear Programming (Simplex Algorithm) (Room B12D-i58)
  • October 9th. Lecture 5: Interior Point Methods (Room B12D-i58)
  • October 14th. Lecture 6: SemiDefinite Programming (Room B12D-i58)
  • October 16th. TD/Office hours (Room B12D-i58)

Part 3: Quantifier Elimination

  • October 21st. Lecture 7: Quantifiers Over Real Closed Fields (Room B12D-i58)

  • November 6th. Lecture 8: Cylindrical Algebraic Decomposition (Room B12D-i57)

  • November 13th. Final Exam (Room B12D-i57)

Evaluation

The final score will be composed of two marks:

  1. A written exam: November 13th, 4:15 – 6:15 PM
  2. A project: a problem/puzzle to understand and solve Selected Problems
    • Proposals by October 14th
    • Paper by November 30th (midnight) Latex Template
    • Expected Sections: Introduction, NP-completness, Solving and Results, Conclusion
    • Submission webpage: EasyChair

Assignments

TBA.

Seminars

November 4th. 4:15PM. Room: B12D-i57 (ISTIC).

Previous Exams

Internships

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

  • Exact Semidefinite Approximations of Continuous Reachable Sets [pdf]

Please come forward if interested.

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

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