https://www.dagstuhl.de/21361

September 5 – 10 , 2021, Dagstuhl Seminar 21361

Extending the Synergies Between SAT and Description Logics

Organizers

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

For support, please contact

Dagstuhl Service Team

Documents

Dagstuhl Report, Volume 11, Issue 8 Dagstuhl Report
Aims & Scope
List of Participants
Shared Documents
Dagstuhl Seminar Schedule [pdf]

Summary

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.

Format

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

Classification

  • Artificial Intelligence / Robotics
  • Verification / Logic

Keywords

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

Documentation

In the series Dagstuhl Reports each Dagstuhl Seminar and Dagstuhl Perspectives Workshop is documented. The seminar organizers, in cooperation with the collector, prepare a report that includes contributions from the participants' talks together with a summary of the seminar.

 

Download overview leaflet (PDF).

Dagstuhl's Impact

Please inform us when a publication was published as a result from your seminar. These publications are listed in the category Dagstuhl's Impact and are presented on a special shelf on the ground floor of the library.

Publications

Furthermore, a comprehensive peer-reviewed collection of research papers can be published in the series Dagstuhl Follow-Ups.