Contents

Propositional satisfiability is the problem of determining, for a formula of propositional logic, whether there is an assignment of truth values to its variables for which that formula evaluates to true. In the 90’s, a technology called SAT solving has become impressively powerful, being able to check the satisfiability of huge real-world propositional logic problems with millions of clauses.

Based on this success, the question raised whether these technologies could be somehow extended to check also quantifier-free first-order logic formulas over different theories for satisfiability. This would be very helpful as a lot of real-world problems cannot be conveniently encoded in propositional logic. This was the motivation for the development of so-called Satisfiability Modulo Theories (SMT) solvers.

In this seminar we follow up on topics related to SAT and SMT solving, covering mathematical background, algorithmic aspects as well as the usage of SAT and SMT solvers to solve problems from different application domains.

Prerequisites

Participants should have completed the courses on “Algorithms and Data Structures” and “Mathematical Logic”, and they should have some knowledge in formal methods (for example from courses on “Satisfiability Checking”, “Modeling and Analysis of Hybrid Systems” or “Model Checking”).

Contact: László Antal