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 erteilt

Dagstuhl Service Team


Dagstuhl Report, Volume 11, Issue 8 Dagstuhl Report
Gemeinsame Dokumente
Programm des Dagstuhl-Seminars [pdf]


Propositional satisfiability (SAT) and Description Logics (DL) are two successful areas of computational logic where automated reasoning plays a fundamental role. Seen from a very abstract level, they can be thought as being part of the same family of logical formalisms attempting to represent knowledge from an application domain, and differentiated only by their expressivity and correspondent trade-off in reasoning complexity. However, the evolution of the two areas has diverged, mainly due to differences in their underlying goals and methods. While the DL community focused on introducing and fully understanding new constructors capable of expressing different facets of knowledge, the SAT community built highly-optimised solvers targeted for industrial-size problems.

Some recent work has permeated the boundaries between the two communities. It has been shown that some DL reasoning problems could be reduced to known SAT-related tasks. In turn, these reductions motivated new optimisations targeted to the specific shape of the problems constructed by them. The goal of this seminar was to bring together researchers from both communities to foster a deeper collaboration and mutual development. The primary goals were (i) to understand the tasks and methods from one community which could benefit the other, and (ii) to discuss the policies used within the communities to encourage specific advancements.

A relevant issue considered is how to promote the development and testing of DL reasoners. To try to answer this, we discussed the status of benchmarks in both communities, and the success stories from SAT competitions. A salient point was the issue, from the DL point of view, of the many variants that should be evaluated -- from the different languages, to the reasoning tasks considered. However, recent SAT competitions have also successfully handled many categories. One possible explanation for the wide availability of solvers capable of handling practical extensions of SAT (like MaxSAT and QBF) is the existence of solvers like MiniSAT, which allow for fast prototyping using SAT solvers as oracles. No analogous tool is available for DL reasoners.

The remaining of the seminar focused on novel and timely tasks which are currently under development in both communities, and where the best possibilities for collaborations are foreseen. Among them, we can mention methods for explaining the result from a solver, and proofs which can be used to automatically verify their correctness. We noted that the notion of an explanation is too wide, allowing for different interpretations which were presented as talks during the seminar. Each of these interpretations gives rise to distinct techniques. But interestingly, the core ideas are not necessarily specific to SAT or DLs. This last observation can lead to collaborations studying the problems from both points of view.

In addition to the longer talks whose abstracts accompany this document, other impromptu presentations were triggered by the previous discussions. One clear conclusion which can be taken from these engagements is that the potential for synergic growth between the areas is large and worth exploring.


Due to the COVID-19 situation, the seminar had to be held in a hybrid format. While this had the obvious disadvantage of limiting the social interactions and offline scientific discussions that characterise Dagstuhl seminars, it also allowed the participation of many who, by distance or travel limitations, would have not been able to attend.

Overall, the hybrid format meant having a more structured and linear program than originally planned for the seminar, but as mentioned already the results are promising.

Summary text license
  Creative Commons BY 4.0
  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).

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.


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