Computing the Why-Provenance for Datalog Queries via SAT Solvers


  • Marco Calautti University of Milan
  • Ester Livshits University of Edinburgh
  • Andreas Pieris University of Edinburgh University of Cyprus
  • Markus Schneider University of Edinburgh



KRR: Computational Complexity of Reasoning, KRR: Knowledge Representation Languages, KRR: Ontologies, KRR: Other Foundations of Knowledge Representation & Reasoning


Explaining an answer to a Datalog query is an essential task towards Explainable AI, especially nowadays where Datalog plays a critical role in the development of ontology-based applications. A well-established approach for explaining a query answer is the so-called why-provenance, which essentially collects all the subsets of the input database that can be used to obtain that answer via some derivation process, typically represented as a proof tree. It is well known, however, that computing the why-provenance for Datalog queries is computationally expensive, and thus, very few attempts can be found in the literature. The goal of this work is to demonstrate how off-the-shelf SAT solvers can be exploited towards an efficient computation of the why-provenance for Datalog queries. Interestingly, our SAT-based approach allows us to build the why-provenance in an incremental fashion, that is, one explanation at a time, which is much more useful in a practical context than the one-shot computation of the whole set of explanations as done by existing approaches.



How to Cite

Calautti, M., Livshits, E., Pieris, A., & Schneider, M. (2024). Computing the Why-Provenance for Datalog Queries via SAT Solvers. Proceedings of the AAAI Conference on Artificial Intelligence, 38(9), 10459-10466.



AAAI Technical Track on Knowledge Representation and Reasoning