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.
Course Prerequisites
The course is basic, no special prerequisites are assumed, beyond generic high school level skills.
Teaching Methods
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.
Assessment Methods
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.
Texts
Teachers notes are available for the course. Comprehensive textbook: Aaron R. Bradley, Zohar Manna"The Calculus of Computation", Springer 2007.
Contents
Propositional logic, truth tables, SAT problems. Resolution Calculus. 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.
