Extending the Synergies Between SAT and Description Logics
( 05. Sep – 10. Sep, 2021 )
- Joao Marques-Silva (CNRS - Toulouse, FR)
- Rafael Penaloza (University of Milano-Bicocca, IT)
- Uli Sattler (University of Manchester, GB)
- Michael Gerke (für wissenschaftliche Fragen)
- Susanne Bach-Bernhard (für administrative Fragen)
- Querying Inconsistent Prioritized Data with ORBITS : Algorithms, Implementation, and Experiments : article in KR 2022 - Bienvenu, Meghyn; Bourgaux, Camille - IJCAI, 2022. - pp. 523-532 - IJCAI, 2022. - pp. 523-532.
- Even Faster Conflicts and Lazier Reductions for String Solvers : article in LNCS 13372, CAV 2022 - Nötzli, Andres; Reynolds, Andrew; Barbosa, Haniel; Barrett, Clark; Tinelli, Cesare - Berlin : Springer, 2022. - pp. 220-241 - (Lecture notes in computer science ; 13372 : article).
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.
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.
- Meghyn Bienvenu (CNRS & University of Bordeaux) [dblp]
- Maria Paola Bonacina (University of Verona, IT) [dblp]
- Stefan Borgwardt (TU Dresden, DE) [dblp]
- Camille Bourgaux (CNRS & ENS - Paris, FR) [dblp]
- David Carral (INRIA - Sophia Antipolis, FR) [dblp]
- Aaron Eberhart (Kansas State University - Manhattan, US) [dblp]
- Jean-Marie Lagniez (CNRS, CRIL - Lens, FR) [dblp]
- Joao Marques-Silva (CNRS - Toulouse, FR) [dblp]
- Jordi Planes (University of Lleida, ES) [dblp]
- Anni-Yasmin Turhan (TU Dresden, DE) [dblp]
- Carlos Ansotegui (University of Lleida, ES) [dblp]
- Leopoldo Bertossi (Adolfo Ibáñez University - Santiago, CL) [dblp]
- Olaf Beyersdorff (Universität Jena, DE) [dblp]
- Emmanuel Hebrard (LAAS - Toulouse, FR) [dblp]
- Ian Horrocks (University of Oxford, GB) [dblp]
- Alexey Ignatiev (Monash University - Clayton, AU) [dblp]
- Matti Järvisalo (University of Helsinki, FI) [dblp]
- Oliver Kullmann (Swansea University, GB) [dblp]
- Carlos Mencia (University of Oviedo, ES) [dblp]
- Thomas Meyer (University of Cape Town, ZA) [dblp]
- Jakob Nordström (University of Copenhagen, DK & Lund University, SE) [dblp]
- Magdalena Ortiz (TU Wien, AT) [dblp]
- Ana Ozaki (University of Bergen, NO) [dblp]
- Rafael Penaloza (University of Milano-Bicocca, IT) [dblp]
- Francesco Ricca (University of Calabria, IT) [dblp]
- Uli Sattler (University of Manchester, GB) [dblp]
- Renate Schmidt (University of Manchester, GB) [dblp]
- Stefan Szeider (TU Wien, AT) [dblp]
- David Tena Cucala (University of Oxford, GB) [dblp]
- Cesare Tinelli (University of Iowa - Iowa City, US) [dblp]
- Renata Wassermann (University of Sao Paulo, BR) [dblp]
- artificial intelligence / robotics
- verification / logic
- propositional satisfiability
- description logics
- standard and non-standard inferences
- reasoning services