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 of-the-shelf SAT solvers can be exploited towards an eficient 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.
Datalog has emerged in the 1980s as a logic-based query language from Logic Programming and
has been extensively studied since then [
As for any other query language, explaining why a result to a Datalog query is obtained
is crucial towards transparent data-intensive applications. A well-established approach for
providing such explanations to query answers is the so-called why-provenance [
Despite its wide acceptance, why-provenance for Datalog queries comes with two weaknesses:
it is computationally very expensive, and it may provide counterintuitive explanations. The
ifrst weakness is manifested by the fact that, although why-provenance for Datalog queries
has been around for decades, only a couple of works have considered implementing it for
recursive queries [
The main goal of this work is to tackle the two weaknesses of why-provenance for Datalog queries discussed above. In particular, we place our work in the more practical setting of on-demand why-provenance, and target an eficient implementation that provides conceptually meaningful explanations for the given query answer.
We consider the disjoint countably infinite sets C and V of constants and variables, respectively. We may refer to constants and variables as terms. For brevity, given an integer > 0, we may write [] for the set of integers {1, . . . , }.
Relational Databases. A schema S is a finite set of relation names (or predicates) with associated arity. We write / to say that has arity ≥ 0; we may write ar() for . A (relational) atom over S is an expression of the form (¯), where / ∈ S and ¯ is an -tuple of terms. By abuse of notation, we may treat tuples as the set of their elements. A fact is an atom that mentions only constants. A database over S is a finite set of facts over S. The active domain of a database , denoted dom(), is the set of constants in .
Syntax and Semantics of Datalog Programs. A (Datalog) rule over a schema S is an expression of the form
0(¯0) :– 1(¯1), . . . , (¯) for ≥ 1, where (¯) is a (constant-free) relational atom over S for ∈ {0, . . . , }, and each variable in ¯0 occurs in ¯ for some ∈ []. We refer to 0(¯0) as the head of , denoted head( ), and to the expression that appears on the right of the :– symbol as the body of , denoted body( ), which we may treat as the set of its atoms.
A Datalog program over a schema S is defined as a finite set Σ of Datalog rules over S. A predicate occurring in Σ is called extensional if there is no rule in Σ having in its head, and intensional if there exists at least one rule in Σ with in its head. The extensional (database) schema of Σ , denoted edb(Σ) , is the set of all extensional predicates in Σ , while the intensional schema of Σ , denoted idb(Σ) , is the set of all intensional predicates in Σ . Note that, by definition, edb(Σ) ∩ idb(Σ) = ∅. The schema of Σ , denoted sch(Σ) , is the set edb(Σ) ∪ idb(Σ) , which is in general a subset of S since some predicates of S may not appear in Σ .
An elegant property of Datalog programs is that they have three equivalent semantics:
model-theoretic, fixpoint, and proof-theoretic [
Definition 2.1. (Proof Tree) Consider a Datalog program Σ , a database over edb(Σ) , and a fact over sch(Σ) . A proof tree of w.r.t. and Σ is a finite labeled rooted tree = (, , ), with : → base(, Σ) , such that: 1. If ∈ is the root, then () = . 2. If ∈ is a leaf, then () ∈ . 3. If ∈ is a node with ≥ 1 children 1, . . . , , then there is a rule 0(¯0) :– 1(¯1), . . . , (¯) ∈ Σ and a function ℎ : ⋃︀∈[] ¯ → C such that () = 0(ℎ(¯0)), and () = (ℎ(¯)) for each ∈ [].
Essentially, a proof tree of a fact w.r.t. and Σ indicates that we can derive starting from end executing the rules of Σ . Now, given a Datalog program Σ and a database over sch(Σ) , the semantics of Σ on is Σ( ) = { | there is a proof tree of w.r.t. and Σ }. That is, the set of facts that can be proven using and Σ .
Datalog Queries. It is now straightforward to recall the syntax and the semantics of Datalog queries. A Datalog query is a pair = (Σ , ), where Σ is a Datalog program and a predicate of idb(Σ) . Now, for a database over edb(Σ) , the answer to over is defined as the set () = {︁¯ ∈ dom()ar() | (¯) ∈ Σ( )}︁ , that is, the set of tuples ¯ of dom()ar() such that the fact (¯) can be derived using and Σ . Why-Provenance for Datalog Queries. As discussed in the introduction, why-provenance is a standard way of explaining query results. It essentially collects all the subsets of the database (without unnecessary atoms) that allow to prove (or derive) a query result. We now formalize this simple idea.
Given a proof tree = (, , ) (of some fact w.r.t. some database and Datalog program), the support of is the set support( ) = { () | ∈ is a leaf of }, which is essentially the set of facts that label the leaves of the proof tree . Note that support( ) is a subset of the underlying database since, by definition, the leaves of a proof tree are labeled with database atoms. The formal definition of why-provenance for Datalog queries follows. Definition 2.2. (Why-Provenance for Datalog) Consider a Datalog query = (Σ , ), a database over edb(Σ) , and a tuple ¯ ∈ dom()ar(). The why-provenance of ¯ w.r.t. and is defined as the family of sets of facts
why(¯, , ) = {support( ) | is a proof tree of (¯) w.r.t. and Σ }.
Intuitively speaking, a set of facts ′ ⊆ that belongs to why(¯, , ) should be understood as a reason why the tuple ¯ is an answer to the query over the database , i.e., ′ explains why ¯ ∈ (). In particular, all the facts of ′ are used in order to derive ¯ as an answer.
The standard notion of why-provenance defined above relies on arbitrary proof trees. However,
as discussed in [
= {(), (), (, , ), (, , ), (, , )}.
The following is a proof tree of the fact () w.r.t. and Σ that is non-recursive and (hereditary) minimal-depth, but it sufers from the ambiguity issue described above:
A(d) A(c)
A(c)
T (c, c, d) A(a) A(a) T (a, a, c)
A(b) A(b) T (b, b, c) S(a) S(a)
S(b) S(b) Indeed, there are two nodes labeled with the fact (), but their subtrees difer, and thus, it is ambiguous how () is derived. Hence, the database , which belongs to the why-provenance of () w.r.t. and due to the above proof tree, might be classified as a counterintuitive explanation since it does not correspond to an intuitive derivation process where each fact is derived once due to a unique reason. Indeed, the intuitive explanations that one expects are the following: is accessible from via (i.e., the subset {(), (, , ), (, , )} of ), or is accessible from via (i.e., the subset {(), (, , ), (, , )} of ).
This leads to the class of unambiguous proof trees, where all occurrences of a fact must be proved via the same derivation. Two rooted trees = (, , ) and ′ = ( ′, ′, ′) are isomorphic, denoted ≈ ′, if there exists a bijection ℎ : → ′ such that, for each ∈ , () = ′(ℎ()), and for each , ∈ , (, ) ∈ if (ℎ(), ℎ()) ∈ ′. Let [] be the subtree of the proof tree rooted at node . The formal definition of unambiguous proof trees follows.
Definition 3.2. (Unambiguous Proof Tree) Consider a Datalog program Σ , a database over edb(Σ) , and a fact over sch(Σ) . An unambiguous proof tree of w.r.t. and Σ is a proof tree = (, , ) of w.r.t. and Σ such that, for all , ∈ , () = () implies [] ≈ [].
Why-provenance relative to unambiguous proof trees is defined in the obvious way: for a Datalog query = (Σ , ), a database over edb(Σ) , and a tuple ¯ ∈ dom()ar(), the why-provenance of ¯ w.r.t. and relative to unambiguous proof trees is the family of sets of facts
{support( ) | is an unambiguous proof tree of (¯) w.r.t. and Σ }, denoted whyUN(¯, , ). The main concern of this work is to eficiently compute the whyprovenance of a tuple relative to unambiguous proof trees. To this end, we are going to exploit of-the-shelf SAT solvers and report encouraging results; this is the subject of the next two sections. To the best of our knowledge, this is the first time that SAT solvers are used for computing the why-provenance. Let us stress that focusing on unambiguous proof trees, apart from their conceptual advantage discussed above, was crucial towards our encouraging results as it is unclear how a SAT-based implementation can be made practical for arbitrary proof trees.
In this section, we show that the why-provenance of a tuple relative to unambiguous proof trees can be extracted from the satisfying truth assignments of a Boolean formula. Compactly Representing Unambiguous Proof Trees. The construction of the Boolean formula relies on a characterization of the existence of an unambiguous proof tree of a fact w.r.t. and Σ via the existence of a so-called compressed directed acyclic graph (DAG) of w.r.t. and Σ , which, intuitively speaking, is a compact representation of an unambiguous proof tree of w.r.t. and Σ ; this is needed, as an unambiguous proof tree can be exponentially large in the size of . We proceed to formalize the notion of compressed DAG and give the characterization in question. Recall that a DAG is rooted if it has exactly one node, the root, with no incoming edges. A node of is a leaf if it has no outgoing edges.
Definition 4.1. (Compressed DAG) Consider a Datalog program Σ , a database over edb(Σ) , and a fact over sch(Σ) . A compressed DAG of w.r.t. and Σ is a rooted DAG = (, ), with ⊆ base(, Σ) , such that: 1. The root of is . 2. If ∈ is a leaf node, then ∈ . 3. If ∈ has ≥ 1 outgoing edges (, 1), . . . , (, ), then there is a rule 0(¯0) :– 1(¯1), . . . , (¯) ∈ Σ and a function ℎ : ⋃︀∈[] ¯ → C such that = 0(ℎ(¯0)) and { }∈[] = {(ℎ(¯)) | ∈ []}.
For a compressed DAG = (, ), the support of is defined analogously to the support of a proof tree, that is, support() = { ∈ | is a leaf of }. The desired characterization follows.
Proposition 4.2. For a Datalog program Σ , a database over edb(Σ) , a fact over sch(Σ) , and a database ′ ⊆ , the following are equivalent: 1. There exists an unambiguous proof tree of w.r.t. and Σ such that support( ) = ′. 2. There exists a compressed DAG of w.r.t. and Σ such that support() = ′.
Note that the above characterization relies on the fact that we focus on unambiguous proof trees. More precisely, unambiguity allows us to use a single node in the compressed DAG as a representative for all the (possibly exponentially many) nodes in the proof tree labelled with the same fact.
The Boolean Formula. Fix a Datalog query = (Σ , ), a database over edb(Σ) , and a tuple ¯ ∈ dom()ar(). We construct in polynomial time in a Boolean formula (¯,,) such that the why-provenance of ¯ w.r.t. and relative to unambiguous proof trees can be computed from the truth assignments that make (¯,,) true.
Among the Boolean variables of (¯,,), we also have the disjoint sets of variables and , where each variable in corresponds to a possible node of some compressed DAG of (¯) w.r.t. and Σ , while each variable in corresponds to a possible edge between two nodes of some compressed DAG of (¯) w.r.t. and Σ . The key idea is that the variables of and that become true via a satisfying truth assignment of (¯,,), induce the nodes and the edges of a compressed DAG for (¯) w.r.t. and Σ , which, by Proposition 4.2, implies that support() ∈ whyUN(¯, , ). The Boolean formula (¯,,) is a conjunction of the form graph ∧ root ∧ proof ∧ acyclic , where graph is in charge of guaranteeing consistency between the truth assignments of the variables in and the variables in , i.e., if an edge between two nodes is part of , then the two nodes must belong to as well. The formula root guarantees that the atom (¯) is a node of , is the root of , and no other node of can be the root (i.e., must have at least one incoming edge). The formula proof is in charge of guaranteeing that, whenever an intensional atom is a node of , then it must have the correct children in . Finally, acyclic is in charge of checking that , namely the graph whose edges correspond to the true variables in , is acyclic. We can prove the following crucial result about the above Boolean formula:
Scenario
TClosure [
Doctors [
Galen [
CSDA [
Databases bitcoin(235K), facebook(88.2K)
1(100K) 1(26.5K), 2(30.5K), 3(67K), 4(82K) 1(68K), 2(340K), 3(680K), 4(3.4M), 5(6.8M) httpd(10M), postgresql(34.8M), linux(44M)
Recursive #Rules ✓ 2 ✗ 6 ✓ 14 ✓ 2 ✓ 2 Proposition 4.3. Consider a Datalog query = (Σ , ), a database over edb(Σ) , and a tuple ¯ ∈ dom()ar(). It holds that: • (¯,,) is in CNF and can be constructed in polynomial time w.r.t. . • There is a one-to-one correspondence between the members of whyUN(¯, , ) and the satisfying assignments of (¯,,). • Each member of whyUN(¯, , ) can be recovered from a satisfying assignment of (¯,,) in polynomial time w.r.t. the size of (¯,,).
Proposition 4.3 provides a way for computing the why-provenance of a tuple relative to unambiguous proof trees via of-the-shelf SAT solvers. But how does this machinery behave when applied in a practical context? In particular, we are interested in the incremental computation of the why-provenance by enumerating its members, which is more useful in practice than computing the whole set at once.
This is achieved by adapting a standard technique from the SAT literature for enumerating the satisfying assignments of a Boolean formula, called blocking clause. After asking the SAT solver for an arbitrary satisfying assignment of (¯,,), we output the member of whyUN(¯, , ), denoted db( ), corresponding to , and then construct a “blocking” clause db( ) which expresses that no other satisfying assignment ′ should give rise to the same member of the why-provenance. This will exclude the previously computed explanations from the computation. We keep adding such blocking clauses each time we get a new member of the why-provenance until the formula is unsatisfiable.
We now proceed to experimentally evaluate the SAT-based approach discussed above. To this end, we consider a variety of scenarios from the Datalog literature consisting of a query = (Σ , ) and a family of databases over edb(Σ) . All the scenarios are summarized in Table 1.
Experimental Setup. For each scenario consisting of the query = (Σ , ) and the family of
databases , and for each ∈ , we have computed () using DLV [
Experimental Results and Take-Home Messages. Concerning the construction of the formula, in most of the scenarios, the runtime is in the order of some seconds, and we have observed that almost all the time is spent for computing the intermediate data structures, needed to build the formula. Considering the more demanding scenarios Andersen and CSDA, the total time is in the order of some minutes. Note, however, that it would be similarly demanding even for query answering.
For the incremental computation of the why-provenance, we considered the time between the current member of the why-provenance and the next (the delay). All delays are in the order of milliseconds. Hence, once the formula is built, incrementally computing the members of the why-provenance is extremely fast.
We also compared our SAT-based approach with the one of [
We observed that our SAT-based implementation consistently outperforms the rule-based one. In particular, for the Galen scenario, in most cases, the rule-based implementation does not ifnish in less than 5 minutes, with the worst case occurring with the largest database, where 41 out of the 100 runs time out.
From our analysis, it is clear that our future eforts should focus on improving the construction
of the Boolean formula. Since proof trees describe a finite reasoning process, it will be interesting
to understand how they can be adapted to other rule-based formalisms with finite reasoning, in
order to apply our SAT-based approach, such as logic programs with finite stable models [
This work was funded by the European Union - Next Generation EU under the MUR PRIN-PNRR grant P2022KHTX7 “DISTORT”, and by the EPSRC grant EP/S003800/1 “EQUID”. rules: An experimental study, VLDB 16 (2023) 2858–2870. [23] M. Calautti, G. Gottlob, A. Pieris, Chase termination for guarded existential rules, in:
PODS, 2015, pp. 91–103. [24] M. Arenas, L. E. Bertossi, J. Chomicki, Consistent query answers in inconsistent databases, in: PODS, 1999, pp. 68–79. [25] M. Calautti, M. Console, A. Pieris, Counting database repairs under primary keys revisited, in: PODS, 2019, pp. 104–118. [26] M. Calautti, S. Greco, C. Molinaro, I. Trubitsyna, Preference-based inconsistency-tolerant query answering under existential rules, AI 312 (2022) 103772. [27] M. Calautti, L. Caroprese, S. Greco, C. Molinaro, I. Trubitsyna, E. Zumpano, Existential active integrity constraints, ESWA 168 (2021) 114297. [28] M. Calautti, M. Console, A. Pieris, Benchmarking approximate consistent query answering, in: PODS, 2021, pp. 233–246.