02. – 07. Februar 2020, Dagstuhl-Seminar 20061

SAT and Interactions


Olaf Beyersdorff (Universität Jena, DE)
Uwe Egly (TU Wien, AT)
Meena Mahajan (Institute of Mathematical Sciences – Chennai, IN)
Claudia Nalon (University of Brasilia, BR)

Auskunft zu diesem Dagstuhl-Seminar erteilt

Dagstuhl Service Team


Gemeinsame Dokumente
Dagstuhl's Impact: Dokumente verfügbar
Programm des Dagstuhl-Seminars [pdf]


The problem of deciding whether a propositional formula is satisfiable (SAT) is one of the most fundamental problems in computer science, both theoretically and practically. Its theoretical significance derives from the Cook-Levin Theorem, identifying SAT as the first NP-complete problem. Since then SAT has become a reference for an enormous variety of complexity statements, among them the celebrated P vs NP problem: one of seven milliondollar Clay Millennium Problems. Due to its NP hardness, SAT has been classically perceived as an intractable problem, and indeed, unless P=NP, no polynomial-time algorithm for SAT exists.

There are many generalisations of the SAT problem to further logics, including quantified Boolean formulas (QBFs) and modal and temporal logics. These logics present even harder satisfiability problems as they are associated with complexity classes such as PSPACE, which encompasses NP. However, QBFs, modal and temporal logics can express many practically relevant problems far more succinctly, thus applying to more real-world problems from artificial intelligence, bioinformatics, verification, and planning.

Due to its practical implications, intensive research has been performed on how to solve SAT problems in an automated fashion. The last decade has seen the development of practically efficient algorithms for SAT, QBFs and further logics and their implementation as solvers, which successfully solve huge industrial instances.

The main aim of this Dagstuhl Seminar is to bring together researchers from different areas of activity in SAT, including computational and proof complexity, SAT and QBF solving, and modal, temporal and further nonclassical logics, so that they can communicate state-of-the-art advances and embark on a systematic interaction that will enhance the synergy between the different areas.

Motivation text license
  Creative Commons BY 3.0 DE
  Olaf Beyersdorff, Uwe Egly, Meena Mahajan, and Claudia Nalon

Dagstuhl-Seminar Series


  • Data Structures / Algorithms / Complexity


  • Satisfiability problems
  • Computational and proof complexity
  • Combinatorics
  • Solvers for satisfiability problems
  • Non-classical logics


In der Reihe Dagstuhl Reports werden alle Dagstuhl-Seminare und Dagstuhl-Perspektiven-Workshops dokumentiert. Die Organisatoren stellen zusammen mit dem Collector des Seminars einen Bericht zusammen, der die Beiträge der Autoren zusammenfasst und um eine Zusammenfassung ergänzt.


Download Übersichtsflyer (PDF).


Es besteht weiterhin die Möglichkeit, eine umfassende Kollektion begutachteter Arbeiten in der Reihe Dagstuhl Follow-Ups zu publizieren.

Dagstuhl's Impact

Bitte informieren Sie uns, wenn eine Veröffentlichung ausgehend von
Ihrem Seminar entsteht. Derartige Veröffentlichungen werden von uns in der Rubrik Dagstuhl's Impact separat aufgelistet  und im Erdgeschoss der Bibliothek präsentiert.