Seminar: Satisfiability Checking

Instructors

Prof. Dr. Erika Ábrahám, Gereon Kremer, Francesco Leofante, Johanna Nellen, Stefan Schupp

Contents

The focus of this seminar is automatic satisfiability checking of formulas. Here we consider several logics, e.g., pure propositional logic, but also extensions like quantified boolean formulas or SAT modulo theories. We will discuss both techniques for efficient satisfiability checking and practical applications in program verification.

Prerequisites

  • Participants should have knowledge in satisfiability checking and/or program verification or related areas (for example from courses on “Satisfiability Checking”, “Modeling and Analysis of Hybrid Systems”, “Logic Programming”, “Functional Programming”, or “Term Rewriting”)
  • Interest in algorithmic aspects and practical applications of logical formalisms

Date

The seminar will take place as a block seminar in our seminar room (4201b). The date will is to be determined. We have a series of strict deadlines before that:

  • Contacted your supervisor to obtain and discuss your literature
  • Read and understand your primary sources, if needed, obtain more literature. Discuss a rough sketch of your seminar paper with your supervisor.
  • Complete your seminar paper (10 pages including title and references) and send it to your supervisor.
  • Prepare your talk and send your slides to your supervisor.
  • Send an electronic version of your seminar paper to your supervisor such that it can be made available on the web page of the seminar.

Initial Meeting

There will be an initial meeting in our seminar room (4201b).

Topics

Below you find a preliminary list with all seminar topics and a link to a corresponding paper. The topic distribution will be done in the initial meeting.

  Topic
1 Minimal Unsatisfiable Cores (Gereon)
2 Difference Logic (Rebecca)
3 Subtropical Satisfiability (Stefan)
4 Linearization (Erika)
5 Interval Constraint Propagation (Johanna)
6 Model-Constructing Satisfiability (Erika)
7 SMT Solver for Verifying Deep Neural Networks (Francesco)
8 Encoding Planning Problems into SMT (Francesco)

introduction

Requirements

Your seminar paper should have 10 pages and be written in either English or German. Do not provide an index or table of contents, but attach a list of references. We will not correct any papers with more than 5 spelling or grammar mistakes on a single page, so please use an automated spell checker! Please follow the ethical guidelines for scientific writing (German, English).

Templates

You can find templates for your paper here. Using them is optional.

Further Details and Questions

For further details please contact Gereon Kremer.