Speaker
Pascal Fontaine is an assistant professor at Université de Lorraine in Nancy, France. He belongs to the Inria group VeriDis, a joint team at LORIA and MPI Saarbrücken. He is one of the lead developers of the VeriT SMT solver.
Abstract
After a quick introduction to the problem of satisfiability in propositional logic (SAT), we investigate some of the main features in state-of-the-art SAT solvers: boolean propagation, conflict analysis, non-chronological backtracking, and decision heuristics. We then study how SAT solvers can be lifted to Satisfiability Modulo Theory, that is, to handle formulas with atoms that are not just propositional variables, but have a meaning defined by a theory. As an example, we will see how the congruence closure algorithm makes a decision procedure for conjunctions of literals in the language of equality and uninterpreted symbols, and how this decision procedure can be used in cooperation with a SAT solver to provide a procedure for the full quantifier-free fragment of first-order logic with equality. Then, we will see how decision procedures for conjunctions of literals can be combined, to build procedures for languages mixing symbols from several decidable theories. We will then quickly mention decision procedures for arithmetic, and how quantifiers are handled within SMT.
Slides available here.
Python will be used for exercises.