ISR 2024 – Track C

SAT/SMT Solving and Applications in Rewriting

Lecturer

René Thiemann   University of Innsbruck

Course Description

In the last two decades, SAT and SMT solvers have become indispensable to solve a wide variety of tasks that have long been considered intractable, ranging from software and hardware verification to planning and scheduling problems, model checking, ... and rewriting! This lecture covers basic notions and algorithms in SAT and SMT solving, and illustrates its applications to solve problems from the area of rewriting. These include finding reduction orders based on LPO, KBO or polynomial interpretations, e.g. for termination analysis or for disproving reachability and confluence. The last lecture gives an introduction to logically constrained term rewrite systems (LCTRSs). This recent rewriting formalism uses SMT reasoning as a backend, and can be used to model problems highly relevant in program verification. Between the lectures, students are also encouraged to solve small problems themselves by encoding them into SAT/SMT.

Content

1. SAT solving: LPO encoding, propositional logic, DPLL, and CDCL.
      1-up    4-up
2. SMT solving: KBO encoding, lazy vs. eager SMT solving, DPLL(T), LRA and LIA
      1-up    4-up
3. SMT solving: polynomial interpretations encoding, bit-vector arithmetic, certification
      1-up    4-up
4. SMT solving: reachability and confluence, introduction to logically constrained rewriting
      1-up    4-up