Propositional Satisfiability (SAT) is the problem of deciding the satisfiability of a Boolean formula (and to a wider extent, to perform Boolean reasoning on possibly-huge expressions.) The ability of efficiently reasoning with Boolean values and operators is a core feature of many applications in various fields of Artificial Intelligence, Formal Verification and Digital Electronics, including, e.g., Automated Reasoning and Planning, Formal verification of Hardware and Software devices, Knowledge Representation and Reasoning. Satisfiability Modulo Theories (SMT) is the problem of deciding the satisfiability of a (typically quantifier-free) first-order formula with respect to some decidable first-order theory (e.g., those of linear arithmetic, Arrays, and Bit-Vectors) and of their combination. SMT is being recognized as increasingly important due to its applications in many domains in different communities. In the last decade we have witnessed a striking interest in SMT, with a boost in the performances of SMT solvers, which combine the power of SAT solvers with the expressivity of decision procedures for various theories of interest. This course aims at providing an overview of the main problems, techniques, functionalities and applications of SAT and SMT. We believe that this course will be of interest for students and researchers in many domains, ranging from Formal Verification, Digital Electronics, and various fields of Artificial Intelligence (e.g. Automated Reasoning, Planning, Knowledge Representation and Reasoning).
