Seminar: Satisfiability Checking

Instructors

Prof. Dr. Erika Ábrahám, Jasper Nalbach, Rebecca Haehn

Contents

The focus of this seminar is on algorithms for checking the satisfiability of logical formulas, SAT and SMT solvers implementing these algorithms, and the usage of these tools to solve logically encoded problems from other domains. We consider algorithms for different logics, for example propositional logic and different arithmetic theories. We also address specific topics in the context of SAT- and SMT-solving,  like for example the generation of explanations for unsatisfiability. There is a wide range of interesting applications, like combinatorial problems from planning or the verification of neural networks, from which we also include selected topics.

Prerequisites

  • Participants should have some knowledge in formal methods (for example from courses on “Satisfiability Checking” or “Modeling and Analysis of Hybrid Systems”)
  • Interest in mathematical and algorithmic aspects, and practical applications of logical formalisms