Curriculum M1 MPRI at ENS Paris-Saclay

TAIS: Tools for AI: Solvers

Description: This course introduces the key tools of automated reasoning, a field aimed at automatically learning and generating new knowledge based on a logical representation of systems. The course covers algorithms for deciding the satisfiability of formulas within various fragments of first-order logic—such as propositional logic, equality constraints between terms, and linear arithmetic over reals and integers—which are used in program verification and synthesis. It also examines the combination of these algorithms via the Nelson-Oppen principle, as well as constraint programming. Theoretical concepts will be applied to problem-solving using existing tools (CVC, Z3) and to the implementation of new decision procedures.

Outline:

  1. Recap of the SAT problem: DPLL algorithm; clause learning with the CDCL algorithm.
  2. Algorithms for SMT (Satisfiability Modulo Theories): CDCL(T) algorithm.
  3. Theories involving equality and uninterpreted functions: union-find, congruence closures (or congruence graphs).
  4. Theories for linear arithmetic over the rationals: Simplex, Fourier-Motzkin.
  5. Theories for Presburger arithmetic and bit-vectors.
  6. Theories of arrays and pointers.
  7. Combination of theories: Nelson-Oppen and Tinelli-Zarba algorithms.


References:

  • Daniel Kroening et Ofer Strichman. Decision Procedures : An Algorithmic Point of View. Springer, 2016. isbn : 978-3-662-57065-4.
  • Armin Biere, Hans van Maaren et Toby Walsh, éd. Handbook of Satisfiability. 2nd Ed. SAGE Publications, 2021
  • Web site of instructors ...