DIPARTIMENTO DI MATEMATICA 'FELICE CASORATI'
Corso di studio
Primo Semestre (04/10/2021 - 14/01/2022)
52 ore di attività frontale
SCRITTO E ORALE CONGIUNTI
The course is basic, no special prerequisites are assumed, beyond generic high school level skills.
During the course, students need to acquire the capability of formalizing various kinds of problems (constraint satisfaction problems, planning problems, verification tasks) using symbolic logic language. They are supposed also to learn how to solve such problems by running appropriate tools like SMT solvers. At the same time, they will acquire information about the theoretical foundations of DPLL procedure and its extension modulo theories.
Programma e contenuti
Propositional logic, truth tables, SAT problems.
DPLL procedure, with heuristics
(backjumping, learning); DIMACS standard.
First order languages, Tarski semantics. Ground resolution and Herbrand theorem.
DPLL modulo theories; congruence closure, other examples of decision procedures. Combination of decision procedures. SMT-LIB2 standard. Applications to verification and planning. A Python interface for Z3.
The course will alternate traditional lectures and computer activities. Theoretical foundations will be carefully explained by the teacher, using both slides and blackboard. During lab classes, students will be supposed to be able to formalize problems, translate them into common standards (DIMACS, SMT-LIB2) and finally run the specification files using the Z3 solver.
Testi di riferimento
Teachers notes are in preparation and will be ready for the course.
Aaron R. Bradley, Zohar Manna"The Calculus of Computation", Springer 2007.
Modalità verifica apprendimento
Comprehensive examination, including:
- questions in quiz style;
- questions concerning theoretical foundations;
- exercises aiming at verifying the familiarity with logical calculi and algorithms;
- exercises requiring the production of executable files in the SMT-LIB2 standard;
- oral examination (if needed in order to adjust the final score)
Obiettivi Agenda 2030 per lo sviluppo sostenibile