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 will 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 will 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.

Creative Commons BY 3.0 DE

Joao Marques-Silva, Rafael Penaloza, and Uli Sattler