05. – 10. September 2021, Dagstuhl-Seminar 21361

Extending the Synergies Between SAT and Description Logics


Joao Marques-Silva (CNRS – Toulouse, FR)
Rafael Penaloza (University of Milano-Bicocca, IT)
Uli Sattler (University of Manchester, GB)

Auskunft zu diesem Dagstuhl-Seminar erteilen

Susanne Bach-Bernhard zu administrativen Fragen

Michael Gerke zu wissenschaftlichen Fragen

Dagstuhl Reports

Wir bitten die Teilnehmer uns bei der notwendigen Dokumentation zu unterstützen und Abstracts zu ihrem Vortrag, Ergebnisse aus Arbeitsgruppen, etc. zur Veröffentlichung in unserer Serie Dagstuhl Reports einzureichen über unser
Dagstuhl Reports Submission System.


Gemeinsame Dokumente
Dagstuhl-Seminar Wiki
Programm des Dagstuhl-Seminars [pdf]

(Zum Einloggen bitte persönliche DOOR-Zugangsdaten verwenden)


Propositional satisfiability (SAT) and Description Logics (DL) are two successful areas of computational logic where automated reasoning plays a fundamental role. At an abstract level, they can all be considered part of the same family of logical formalisms, which can be used to represent knowledge of a domain, with their main difference being the expressivity of the formalism and the complexity of reasoning. Despite their similarities in intent and scope, SAT and DLs have evolved via different routes. While the DL community focused on understanding the precise computational complexity of reasoning in the different fragments it studies, the SAT community was building highly optimised solvers capable of dealing with industrial-size problems, and later adapting their techniques to variants of satisfiability. Although there have been attempts to produce highly efficient reasoners for DLs as well, dealing with problems that go beyond standard reasoning remains a challenge in this field.

This Dagstuhl Seminar aims to bring together researchers from the SAT and DL communities viewed in a wide sense, to discuss potential collaborations and develop deeper synergies between them, discovering how these communities can contribute to each other. Specifically, we intend to discuss which DL reasoning problems can be efficiently solved or optimised with the help of SAT techniques and tools, and how can the SAT community benefit from this cross-fertilisation. In the end, we aim to map a plan for new theoretical, technical, and industrial developments that are considered relevant from the discussions in the Seminar. Some of the open problems to be discussed are the theoretical extension of SAT-developed methods to handle reasoning in more expressive logics, and the practical aspect of designing and using adequate data structures for efficient implementations. Taking into account the expertise of the participants, and recent efforts in these directions, we will encourage discussions on standardisation and system connectivity.

Existing preliminary work has already shown the benefits of applying SAT-based methods for solving non-standard problems in DLs, but the topic needs a more thorough analysis. Indeed, it becomes increasingly clear that the DL and SAT communities have much to offer to each other with some potentially deep connections and advanced applications. However, a major obstacle is the lack of communication and (by extension) collaboration between the fields. Bridging the communities requires a common understanding of the vocabulary, problems, and goals that each aims for. Only then can the two areas construct a synergy for mutual growth and development.

This seminar is based on the idea that understanding is fundamental for collaboration and cooperation. After explaining the common grounds, we will try to answer how DLs and SAT can benefit each other. On the one hand, the experience of building industrial-strength tools can help the development of new DL reasoners. On the other hand, DL-based problems may provide new challenges for the SAT community to tackle. By bringing experts from both fields, we expect to spark discussions that lead to a closer relationship between them, and future collaborations at different levels. The Seminar is conceived as a seed for fruitful collaborations, leading to the identification of new research topics, building of consortia, and applications to research funds.

During the seminar, the participants will engage in various focus groups so that we can elicit different perspectives on a number of topics. We will also include a series of plenary talks complemented by breakout and coordination sessions focusing on specific issues. The program will include ample opportunities for one-on-one discussions and other social interactions.

Motivation text license
  Creative Commons BY 3.0 DE
  Joao Marques-Silva, Rafael Penaloza, and Uli Sattler


  • Artificial Intelligence / Robotics
  • Verification / Logic


  • Propositional satisfiability
  • Description logics
  • Standard and non-standard inferences
  • Reasoning services


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.