ISR 2024 – Track C

SAT/SMT Solving and Applications in Rewriting

Lecturer

Sarah Winkler   Free University of Bolzano – Bozen

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 or polynomial interpretations, discovering abstract rewrite systems that witness desired properties, and disproving reachability. 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. During the lecture, students are also encouraged to solve small problems themselves by encoding them into SAT/SMT.

Content

1. SAT solving: propositional logic, DPLL, and CDCL.


2. SMT solving: lazy vs. eager SMT solving, DPLL(T), congruence closure.


3. SMT with arithmetic: solving LRA by Fourier-Motzkin elimination and Simplex.


4. Logically constrained rewriting: formalism, termination and reachability problems, applications.