Consider a Datalog program $\Sigma$, a database $D$ over
$\mathsf{edb}(\Sigma)$, and a fact $\alpha\in\Sigma(D)$. The integer
$\mathsf{min\text{-}dag\text{-}depth}(\alpha,D,\Sigma)$ can be computed in
polynomial time in $|D|$.

###### Proof.

The proof relies on the well-known immediate consequence operator for Datalog.
Roughly, the operator constructs in different steps all the facts that can be
derived starting from $D$ and applying the rules of $\Sigma$. In particular,
each fact is constructed “as early as possible”, and we are going to show that
the step at which a fact $\alpha$ is first obtained coincides with
$\mathsf{min\text{-}dag\text{-}depth}(\alpha,D,\Sigma)$.

A fact $R(\bar{t})$ is an immediate consequence of $D$ and $\Sigma$ if

  * •

$R(\bar{t})\in D$, or

  * •

there exists a Datalog rule
$R(\bar{x})\,\text{:--}\,R_{1}(\bar{x}_{1}),\ldots,R_{n}(\bar{x}_{n})$ in
$\Sigma$ and a function $h:\bigcup_{i\in[n]}\bar{x}_{i}\rightarrow\mathbf{C}$
such that $\\{R_{1}(h(\bar{x}_{1})),\ldots,R_{n}(h(\bar{x}_{n}))\\}\subseteq
D$ and $h(\bar{x})=\bar{t}$.

The immediate consequence operator for $\Sigma$ is defined as the function
$T_{\Sigma}$ from the set $S$ of databases over $\mathsf{sch}(\Sigma)$ to $S$

$T_{\Sigma}(D)\ =\ \\{R(\bar{t})\mid R(\bar{t})\text{ is an immediate}\\\
\text{consequence of }D\text{ and }\Sigma\\}.$

We then define

$T_{\Sigma}^{0}(D)\ =\ D,$

and for each $i>0$,

$T_{\Sigma}^{i}(D)\ =\ T_{\Sigma}(T_{\Sigma}^{i-1}(D)).$

Finally, we define

$T_{\Sigma}^{\infty}(D)\ =\ \bigcup_{i\geq 0}T_{\Sigma}^{i}(D).$

It is not difficult to see that

$T_{\Sigma}^{\infty}(D)\ =\ T_{\Sigma}^{|\mathsf{base}(D,\Sigma)|}(D),$

which in turn implies that $T_{\Sigma}(D)$ can be computed in polynomial time
in the size of $D$; see, e.g., (?). Hence, for each $i\geq 0$,
$T_{\Sigma}^{i}(D)$ can be computed in polynomial time in the size of $D$.
Note that $T_{\Sigma}^{\infty}(D)=\Sigma(D)$ (?).

The above discussion, together with the following auxiliary lemmas, will prove
our claim. For a fact $\alpha\in T_{\Sigma}^{\infty}(D)$, we write
$\mathsf{rank}_{D,\Sigma}(\alpha)$ for the integer $\min\\{i\mid\alpha\in
T_{\Sigma}^{i}(D)\\}$.

######  Lemma 29.

For every fact $\alpha\in T_{\Sigma}^{\infty}(D)$,
$\mathsf{rank}_{D,\Sigma}(\alpha)=\mathsf{min\text{-}dag\text{-}depth}(\alpha,D,\Sigma)$.

###### Proof.

Consider an arbitrary fact $\alpha\in T_{\Sigma}^{\infty}(D)$ and let
$n=\mathsf{min\text{-}dag\text{-}depth}(\alpha,D,\Sigma)$. We proceed by
induction on $n$.

Base Case. For $n=0$, the claim follows immediately by the definition of proof
DAG and of $T_{\Sigma}$.

Inductive Step. There is a proof DAG $G=(V,E,\lambda)$ of $\alpha$ w.r.t. $D$
and $\Sigma$ with $0pt{G}=n$. Let $u_{1},\ldots,u_{k}$ be the out-neighbours
of the root node $v$, and let $\lambda(u_{i})=R_{i}(\bar{u}_{i})$, for each
$i\in[k]$. Since $0pt{G}=n$, for each $i\in[k]$,
$\mathsf{min\text{-}dag\text{-}depth}(R_{i}(\bar{u}_{i}),D,\Sigma)\leq
0pt{G_{i}}<n$, with $G_{i}$ being the subDAG of $G$ rooted at $u_{i}$. By
inductive hypothesis,
$\mathsf{rank}_{D,\Sigma}(R_{i}(\bar{u}_{i}))\leq\mathsf{min\text{-}dag\text{-}depth}(R_{i}(\bar{u}_{i}),D,\Sigma)$,
for each $i\in[k]$, and thus,
$\\{R_{1}(\bar{u}_{1}),\ldots,R_{k}(\bar{u}_{k})\\}\subseteq
T_{\Sigma}^{n-1}(D)$. Moreover, by the definition of proof DAG, there exist a
rule
$R_{0}(\bar{x}_{0})\text{:--}R_{1}(\bar{x}_{1}),\ldots,R_{k}(\bar{x}_{k})$ in
$\Sigma$ and a function $h:\bigcup_{i\in[n]}\bar{x}_{i}\rightarrow\mathbf{C}$
such that $\alpha=R_{0}(h(\bar{x}_{0}))$ and $h(\bar{x}_{i})=\bar{u}_{i}$ for
each $i\in[k]$. Consequently,
$\mathsf{rank}_{D,\Sigma}(\alpha)\leq\max_{i\in[k]}\\{\mathsf{rank}_{D,\Sigma}(R_{i}(\bar{u}_{i}))\\}+1\leq
n$. We further observe that $\alpha\not\in T_{\Sigma}^{n-1}(D)$ since,
otherwise, by induction hypothesis we can conclude that
$\mathsf{min\text{-}dag\text{-}depth}(\alpha,D,\Sigma)<n$, which is a
contradiction. Hence, $\mathsf{rank}_{D,\Sigma}(\alpha)=n$.

The claim follows by Lemma 29.

The central notion of minimal-depth proof DAG follows:

######  Definition 30 (Minimal-Depth Proof DAG).

Consider a Datalog program $\Sigma$, a database $D$ over
$\mathsf{edb}(\Sigma)$, and a fact $\alpha$ over $\mathsf{sch}(\Sigma)$. A
minimal-depth proof DAG of $\alpha$ w.r.t. $D$ and $\Sigma$ is a proof DAG $G$
of $\alpha$ w.r.t. $D$ and $\Sigma$ such that $0pt{G}$ coincides with
$\mathsf{min\text{-}dag\text{-}depth}(\alpha,D,\Sigma)$.

The analogous result to Proposition 21 follows:

######  Proposition 31.

For a Datalog program $\Sigma$, there is a polynomial $f$ such that, for every
database $D$ over $\mathsf{edb}(\Sigma)$, fact $\alpha$ over
$\mathsf{sch}(\Sigma)$, and $D^{\prime}\subseteq D$, the following are
equivalent:

  1. 1.

There is a minimal-depth proof tree $T$ of $\alpha$ w.r.t. $D$ and $\Sigma$
such that $\mathsf{support}(T)=D^{\prime}$.

  2. 2.

There is a minimal-depth proof DAG $G=(V,E,\lambda)$ of $\alpha$ w.r.t. $D$
and $\Sigma$ with $\mathsf{support}(G)=D^{\prime}$ and $|V|\leq f(|D|)$.

The direction (2) implies (1) is shown by “unravelling” the minimal-depth
proof DAG $G$ into a minimal-depth proof tree $T$ such that
$\mathsf{support}(G)=\mathsf{support}(T)$. We use the same “unravelling”
construction as in the proof of direction (2) implies (1) of Proposition 5,
which preserves the minimality of the depth. We now proceed with the direction
(1) implies (2). The underlying construction proceeds in two main steps
captured by Lemmas 32 and 33 given below.

$\bullet$ The first step is to show that a minimal-depth proof tree $T$ of
$\alpha$ w.r.t. $D$ and $\Sigma$ with $\mathsf{support}(T)=D^{\prime}$ can be
converted into a minimal-depth proof tree $T^{\prime}$ of $\alpha$ w.r.t. $D$
and $\Sigma$ with $\mathsf{support}(T^{\prime})=D^{\prime}$ that has “small”
subtree count.

######  Lemma 32.

For each Datalog program $\Sigma$, there is a polynomial $f$ such that, for
every database $D$ over $\mathsf{edb}(\Sigma)$, fact $\alpha$ over
$\mathsf{sch}(\Sigma)$, and $D^{\prime}\subseteq D$, if there is a minimal-
depth proof tree $T$ of $\alpha$ w.r.t. $D$ and $\Sigma$ with
$\mathsf{support}(T)=D^{\prime}$, then there is also such a proof tree
$T^{\prime}$ with $\mathsf{scount}(T^{\prime})\leq f(|D|)$.

###### Proof.

We first argue that the proof tree $T$ has “small” depth. In particular, by
Lemma 6, there exists a polynomial $f$ and a proof tree $T^{\prime}$ of
$\alpha$ w.r.t. $D$ and $\Sigma$ with $0pt{T^{\prime}}\leq f(|D|)$. Since, by
hypothesis, $T$ is of minimal-depth, we conclude that $0pt{T}\leq f(|D|)$. The
other crucial observation is that the construction underlying Lemma 7, which
converts a proof tree of “small” depth into a proof tree of “small“ subtree
count with the same support preserves the minimality of the depth. It can be
verified that the proof tree $T^{\prime}$ obtained by applying on $T$ the
construction underlying Lemma 7 is such that $0pt{T^{\prime}}\leq 0pt{T}$.
Hence, since $T$ is a minimal-depth proof tree, then so is $T^{\prime}$.
Consequently, we can apply the construction of Lemma 7 to the minimal-depth
proof tree $T$ and get a minimal-depth proof tree $T^{\prime}$ with
$\mathsf{support}(T)=\mathsf{support}(T^{\prime})$ such that
$\mathsf{scount}(T^{\prime})\leq f(|D|)$, where $f$ is the polynomial provided
by Lemma 7.

$\bullet$ The second step shows that a minimal-depth proof tree $T$ of
$\alpha$ w.r.t. $D$ and $\Sigma$ with $\mathsf{support}(T)=D^{\prime}$ of
“small” subtree count can be converted into a compact minimal-depth proof DAG
$G$ of $\alpha$ w.r.t. $D$ and $\Sigma$ with $\mathsf{support}(G)=D^{\prime}$.

######  Lemma 33.

For each Datalog program $\Sigma$ and a polynomial $f$, there is a polynomial
$g$ such that, for every database $D$ over $\mathsf{edb}(\Sigma)$, fact
$\alpha$, and $D^{\prime}\subseteq D$, if there is a minimal-depth proof tree
$T$ of $\alpha$ w.r.t. $D$ and $\Sigma$ with $\mathsf{support}(T)=D^{\prime}$
and $\mathsf{scount}(T)\leq f(|D|)$, then there is a minimal-depth proof DAG
$G=(V,E,\lambda)$ of $\alpha$ w.r.t. $D$ and $\Sigma$ with
$\mathsf{support}(G)=D^{\prime}$ and $|V|\leq g(|D|)$.

###### Proof.

We employ the construction underlying Lemma 8, which converts a proof tree of
“small” subtree count into a non-recursive proof DAG of polynomial size with
the same support, since it preserves the minimality of the depth.

It is now clear that the direction (1) implies (2) of Proposition 31 is an
immediate consequence of Lemmas 32 and 33.

Finalize the Proof. We can now finalize the proof of the claim that
$\mathsf{Why\text{-}Provenance_{MD}[\mathsf{Dat}]}$ is in NP in data
complexity. Fix a Datalog query $Q=(\Sigma,R)$. Given a database $D$ over
$\mathsf{edb}(\Sigma)$, a tuple $\bar{t}\in\mathsf{dom}(D)^{\mathsf{ar}(R)}$,
and a subset $D^{\prime}$ of $D$, to decide whether
$D^{\prime}\in\mathsf{why}_{\mathsf{MD}}(\bar{t},D,Q)$ we simply need to check
for the existence of a minimal-depth proof tree $T$ of $R(\bar{t})$ w.r.t. $D$
and $\Sigma$ such that $\mathsf{support}(T)=D^{\prime}$. By Proposition 31,
this is tantamount to the existence of a polynomially-sized minimal-depth
proof DAG $G$ of $R(\bar{t})$ w.r.t. $D$ and $\Sigma$ with
$\mathsf{support}(G)=D^{\prime}$. The existence of such a non-recursive proof
DAG can be checked via a non-deterministic algorithm that runs in polynomial
time in the size of the database as it was done for proving that
$\mathsf{Why\text{-}Provenance[\mathsf{Dat}]}$ is in NP in data complexity
(Theorem 3). The only difference is that now we need to additionally check
that the guessed DAG $G$ is of minimal-depth, i.e., that $0pt{G}$ coincides
with $\mathsf{min\text{-}dag\text{-}depth}(R(\bar{t}),D,\Sigma)$. It remains
to argue that the latter can be done in polynomial time. The fact that
$\mathsf{min\text{-}dag\text{-}depth}(R(\bar{t}),D,\Sigma)$ can be computed in
polynomial time follows from Proposition 28. Now, $0pt{G}$ can be computed by
converting $G$ into an edge-weighted graph $G^{\prime}$ by assigning weight
$-1$ to each edge, and then running Dijkstra’s polynomial-time algorithm for
finding the smallest weight of a path between two nodes.111We recall that
Dijkstra’s algorithm is correct on graphs with _arbitrary_ integer edge
labels, only when the input graph is a DAG. Indeed, for general graphs,
computing the length of the longest path between two nodes is NP-hard.
Consequently, $\mathsf{Why\text{-}Provenance_{MD}}[Q]$ is in NP, and thus,
$\mathsf{Why\text{-}Provenance_{MD}[\mathsf{Dat}]}$ is in NP in data
complexity.

Lower Bound

We proceed to establish that
$\mathsf{Why\text{-}Provenance_{MD}[\mathsf{LDat}]}$ is NP-hard in data
complexity. To this ends, we need to show that there exists a linear Datalog
query $Q$ such that the problem $\mathsf{Why\text{-}Provenance_{MD}}[Q]$ is
NP-hard. The proof is via a reduction from $\mathsf{3SAT}$, which takes as
input a Boolean formula $\varphi=C_{1}\wedge\ldots\wedge C_{m}$ in 3CNF, where
each clause has exactly 3 literals (a Boolean variable $v$ or its negation
$\neg v$), and asks whether $\varphi$ is satisfiable.

The Linear Datalog Query. We start by defining the linear Datalog query
$Q=(\Sigma,R)$. We actually adapt the query $Q$ used in the proof of the fact
that $\mathsf{Why\text{-}Provenance[\mathsf{LDat}]}$ is NP-hard in data
complexity (see Theorem 3) in such a way that every proof tree has the same
depth. As usual, we use $\\_$ if the name of a variable is not important, and
semicolons in a tuple expression in order to separate terms with a different
semantic meaning. The program $\Sigma$ follows:

$\displaystyle\sigma_{1}$ $\displaystyle:$ $\displaystyle
R(x)\,\,\text{:--}\,\,{\rm Var}(x;y,\\_;z),{\rm Assign}(x,y,z),$
$\displaystyle\sigma_{2}$ $\displaystyle:$ $\displaystyle
R(x)\,\,\text{:--}\,\,{\rm Var}(x;\\_,y;z),{\rm Assign}(x,y,z),$
$\displaystyle\sigma_{3}$ $\displaystyle:$ $\displaystyle{\rm
Assign}(x,y,z)\,\,\text{:--}\,\,{\rm NextC}(x;z,w;k,\ell),$
$\displaystyle\hskip 28.45274ptC(x,y;\\_,\\_;\\_,\\_;z,w;k,\ell),{\rm
Assign}(x,y,w),$ $\displaystyle\sigma_{4}$ $\displaystyle:$ $\displaystyle{\rm
Assign}(x,y,z)\,\,\text{:--}\,\,{\rm NextC}(x;z,w;k,\ell),$
$\displaystyle\hskip 28.45274ptC(\\_,\\_;x,y;\\_,\\_;z,w;k,\ell),{\rm
Assign}(x,y,w),$ $\displaystyle\sigma_{5}$ $\displaystyle:$ $\displaystyle{\rm
Assign}(x,y,z)\,\,\text{:--}\,\,{\rm NextC}(x;z,w;k,\ell),$
$\displaystyle\hskip 28.45274ptC(\\_,\\_;\\_,\\_;x,y;z,w;k,\ell),{\rm
Assign}(x,y,w),$ $\displaystyle\sigma^{\prime}$ $\displaystyle:$
$\displaystyle{\rm Assign}(x,y,z)\,\,\text{:--}\,\,{\rm NextC}(x;z,w;y,\\_),$
$\displaystyle\hskip 128.0374pt{\rm Assign}(x,y,w),$
$\displaystyle\sigma^{\prime\prime}$ $\displaystyle:$ $\displaystyle{\rm
Assign}(x,y,z)\,\,\text{:--}\,\,{\rm NextC}(x;z,w;\\_,y),$
$\displaystyle\hskip 128.0374pt{\rm Assign}(x,y,w),$ $\displaystyle\sigma_{6}$
$\displaystyle:$ $\displaystyle{\rm Assign}(x,z,w)\,\,\text{:--}\,\,{\rm
Next}(x,y;z,\\_;w),R(y),$ $\displaystyle\sigma_{7}$ $\displaystyle:$
$\displaystyle{\rm Assign}(x,z,w)\,\,\text{:--}\,\,{\rm
Next}(x,y;\\_,z;w),P(y),$ $\displaystyle\sigma_{8}$ $\displaystyle:$
$\displaystyle R(x)\,\,\text{:--}\,\,{\rm Last}(x).$

The key difference compared to the Datalog program used in the proof of
Theorem 3 is that now, roughly speaking, the rules $\sigma_{1},\sigma_{2}$
also attach the id of the first clause to the variable assignment; the last
position of the relation ${\rm Var}$ stores the id of the first clause. The
rules
$\sigma_{3},\sigma_{4},\sigma_{5},\sigma^{\prime},\sigma^{\prime\prime}$,
where $\sigma_{3}$, $\sigma_{4}$ and $\sigma_{5}$ are adapted from the
previous proof, whereas $\sigma^{\prime}$, $\sigma^{\prime\prime}$ are new,
force a subtree to always to perform $m$ “steps”, when going through those
rules; NextC provides an ordering of the clauses of the formula. It is easy to
verify that $\Sigma$ is indeed a linear Datalog program.

From $\mathsf{3SAT}$ to $\mathsf{Why\text{-}Provenance_{MD}}[Q]$. We now
establish that $\mathsf{Why\text{-}Provenance_{MD}}[Q]$ is NP-hard by reducing
from $\mathsf{3SAT}$. Consider a 3CNF Boolean formula
$\varphi=C_{1}\wedge\cdots\wedge C_{m}$ with $n$ Boolean variables
$v_{1},\ldots,v_{n}$. For a literal $\ell$, we write $\mathsf{v}(\ell)$ for
the variable occurring in $\ell$, and $\mathsf{b}(\ell)$ for the number $1$
(resp., $0$) if $\ell$ is a variable (resp., the negation of a variable). We
define $D_{\varphi}$ as the database over $\mathsf{edb}(\Sigma)$

$\displaystyle\\{{\rm Var}(v_{i};0,1;1)\mid i\in[n]\\}$ $\displaystyle\cup$
$\displaystyle\\{{\rm Next}(v_{i},v_{i+1};0,1;m+1)\mid i\in[n-1]\\}$
$\displaystyle\cup$ $\displaystyle\\{{\rm Next}(v_{n},\bullet;0,1;m+1),{\rm
Last}(\bullet)\\}$ $\displaystyle\cup$
$\displaystyle\\{C(\mathsf{v}(\ell_{1}),\mathsf{b}(\ell_{1});\mathsf{v}(\ell_{2}),\mathsf{b}(\ell_{2});\mathsf{v}(\ell_{3}),\mathsf{b}(\ell_{3});i,i+1;0,1)\mid$
$\displaystyle\hskip 56.9055pti\in[m]\text{ with
}C_{i}=(\ell_{1}\vee\ell_{2}\vee\ell_{3})\\}$ $\displaystyle\cup$
$\displaystyle\\{{\rm NextC}(v_{i};j,j+1;0,1)\mid i\in[n]\ \text{ and
}j\in[m]\\}.$

We can show the next lemma, which essentially states that the above
construction leads to a correct polynomial-time reduction from $\mathsf{3SAT}$
to $\mathsf{Why\text{-}Provenance}[Q]$:

######  Lemma 34.

The following hold:

  1. 1.

$D_{\varphi}$ can be constructed in polynomial time in $\varphi$.

  2. 2.

$\varphi$ is satisfiable iff
$D_{\varphi}\in\mathsf{why}((v_{1}),D_{\varphi},Q)$.

###### Proof.

It is straightforward to see that $D_{\varphi}$ can be constructed in
polynomial time in the size of $\varphi$. We proceed to establish item (2).
But let us first state and prove an auxiliary technical lemma, which
essentially states that all proof trees of $R(v_{1})$ w.r.t. $D_{\varphi}$ and
$\Sigma$ have the same depth.

######  Lemma 35.

For every proof tree $T$ of $R(v_{1})$ w.r.t. $D_{\varphi}$ and $\Sigma$,
$0pt{T}=n\cdot(m+2)+1$.

###### Proof.

A proof tree of $R(v_{1})$ w.r.t. $D_{\varphi}$ and $\Sigma$ has a root node
$v$ labeled with $R(v_{1})$, and thus, its children are necessarily labeled
with facts obtained by means of either rule $\sigma_{1}$ or $\sigma_{2}$. From
these children, only one, say $u$, is labeled with an intensional fact, which
is of the form ${\rm Assign}(v_{1},\cdot,1)$ (the constant $1$ is due to the
variable $z$ in the body of rules $\sigma_{1},\sigma_{2}$). Then, the children
of $u$ are necessarily labeled with facts obtained via one of
$\sigma_{3},\sigma_{4},\sigma_{5},\sigma^{\prime},\sigma^{\prime\prime}$ (this
is because of the constant $1$ in the fact labeling $u$). Moreover, due to the
presence of the atom ${\rm NextC}(x;z,w;k,\ell)$ in the body of each such
rule, only one child of $u$, say $u^{\prime}$, is labeled with an intensional
fact of the form ${\rm Assign}(v_{1},\cdot,2)$. Applying the same reasoning,
from this node with label ${\rm Assign}(v_{1},\cdot,2)$, one of the rules
$\sigma_{3},\sigma_{4},\sigma_{5},\sigma^{\prime},\sigma^{\prime\prime}$ will
be used, and the id on the third position will be increased again, until it
will coincide with $m+1$. Up to this point, the longest path in the tree from
the root is of length $m$+1. It is not difficult to see now that the only rule
that can be applied is either $\sigma_{6}$ or $\sigma_{7}$ due to the variable
$w$ appearing in the atom ${\rm Next}(x,y;z,\\_;w)$. After one of such rules
is applied the only node labeled with an intensional fact has as label the
fact $R(v_{2})$, if $n>1$, and $R(\bullet)$ otherwise, and the total depth is
$m+1+1=m+2$. Thus, either $\sigma_{1}$ will then be used again, or
$\sigma_{8}$. By applying the above reasoning for all the variables of
$\varphi$, the total depth of a proof tree of $R(v_{1})$ w.r.t. $D_{\varphi}$
and $\Sigma$ is precisely $n\cdot(m+2)+1$, as needed.

With Lemma 35 in place, to prove our claim it suffices to show that $\varphi$
is satisfiable iff there is a proof tree $T$ (regardless of its depth) of
$R(v_{1})$ w.r.t. $D_{\varphi}$ and $\Sigma$ such that
$\mathsf{support}(T)=D_{\varphi}$. To prove this last claim, it is not
difficult to see how one can adapt the proof given for Theorem 3. The main
difference is that we additionally need to argue that when a proof tree of
$R(v_{1})$ uses the rules
$\sigma_{3},\sigma_{4},\sigma_{5},\sigma^{\prime},\sigma^{\prime\prime}$, and
thus, we have a node in the proof tree labeled with a fact of the form ${\rm
Assign}(v_{i},\mathsf{val},j)$, if the truth value $\mathsf{val}$ chosen for
$v_{i}$ does not make the clause $C_{j}$ true, then the proof tree will follow
$\sigma^{\prime}$ or $\sigma^{\prime\prime}$, depending on the value of
$\mathsf{val}$. Hence, in any case, through rules
$\sigma_{3},\sigma_{4},\sigma_{5},\sigma^{\prime},\sigma^{\prime\prime}$, any
proof tree will be able to touch all facts with predicate ${\rm NextC}$ in the
database. Since these are the only new facts w.r.t. the ones used in the proof
of Theorem 3 (all other facts have been only slightly modified), if $\varphi$
is satisfiable, then we have a proof tree $T$ of $R(v_{1})$ w.r.t.
$D_{\varphi}$ and $\Sigma$ with the property that
$\mathsf{support}(T)=D_{\varphi}$, and vice versa.

By Lemma 34, $\mathsf{Why\text{-}Provenance_{MD}}[Q]$ is NP-hard. Thus,
$\mathsf{Why\text{-}Provenance_{MD}[\mathsf{LDat}]}$ is NP-hard in data
complexity.

###  C.2 Non-Recursive Queries

We now focus on non-recursive Datalog queries, and show the following about
the data complexity of why-provenance relative to minimal-depth proof trees:

######  Theorem 36.

$\mathsf{Why\text{-}Provenance_{MD}[\mathsf{NRDat}]}$ is in $\rm AC_{0}$ in
data complexity.

This is shown via FO rewritability as done for Theorem 9. Let us stress,
however, that the target FO query cannot be obtained by simply refining the
space of proof trees underlying the definition of $\mathsf{cq}(Q)$, for a
Datalog query $Q$, as done in the case of non-recursive proof trees (see
Theorem 25). The key reason is that the notion of minimal-depth is not over
all proof trees, but over the proof trees of a certain fact. This dependency
on the fact (and indirectly, on the database) does not allow us to simply
consider a refined family of proof trees as we did for non-recursive proof-
trees, and a slightly more involved construction is needed. Actually, we are
going to adapt the FO query underlying Theorem 9.

First-Order Rewriting. Consider a non-recursive Datalog query $Q=(\Sigma,R)$.
Recall that in the proof of Theorem 9, for a CQ
$\varphi(\bar{y})\in\mathsf{cq}^{\approx}(Q)$, we defined an FO query
$Q_{\varphi(\bar{y})}=\psi_{\varphi(\bar{y})}(x_{1},\ldots,x_{\mathsf{ar}(R)})$,
where $x_{1},\ldots,x_{\mathsf{ar}(R)}$ are distinct variables that do not
occur in any of the CQs of $\mathsf{cq}^{\approx}(Q)$, with the following
property: for every database $D$ and tuple
$\bar{t}\in\mathsf{dom}(D)^{\mathsf{ar}(R)}$, $\bar{t}\in
Q_{\varphi(\bar{y})}(D)$ iff $\bar{t}$ is an answer to $\varphi(\bar{y})$ over
$D$, and, in addition, all the atoms of $D$ are used in order to entail the
sentence $\varphi[\bar{y}/\bar{t}]$, i.e., there are no other facts in $D$
besides the ones that have been used as witnesses for the atoms occurring in
$\varphi[\bar{y}/\bar{t}]$. We are going to extend $Q_{\varphi(\bar{y})}$ into
$Q^{+}_{\varphi(\bar{y})}=\psi^{+}_{\varphi(\bar{y})}(x_{1},\ldots,x_{\mathsf{ar}(R)})$
that, in addition, performs the minimal depth check. Recall that, with
$\varphi$ being of the form
$\exists\bar{z}\,(R_{1}(\bar{w}_{1})\wedge\cdots\wedge R_{n}(\bar{w}_{n}))$,
the formula $\psi_{\varphi(\bar{y})}$, with free variables
$\bar{x}=(x_{1},\ldots,x_{\mathsf{ar}(R)})$, is of the form

$\exists\bar{y}\exists\bar{z}\left(\varphi_{1}\ \wedge\ \varphi_{2}\ \wedge\
\varphi_{3}\right),$

where $\varphi_{1}$ is defined as

$\bigwedge\limits_{i\in[n]}\,R_{i}(\bar{w}_{i})\ \wedge\ (\bar{x}=\bar{y})\
\wedge\ \bigwedge\limits_{\begin{subarray}{c}u,v\in\mathsf{var}(\varphi),\\\
u\neq v\end{subarray}}\neg(u=v)$

$\varphi_{2}$ is defined as

$\bigwedge\limits_{P\in\\{R_{1},\ldots,R_{n}\\}}\neg\left(\exists\bar{u}_{P}\left(P(\bar{u}_{P})\
\wedge\ \bigwedge\limits_{\begin{subarray}{c}i\in[n],\\\
R_{i}=P\end{subarray}}\,\neg(\bar{w}_{i}=\bar{u}_{P})\right)\right)$

and $\varphi_{3}$ is defined as

$\bigwedge\limits_{P\in\mathsf{edb}(\Sigma)\setminus\\{R_{1},\ldots,R_{n}\\}}\neg\left(\exists\bar{u}_{P}\,P(\bar{u}_{P})\right).$

Now, the formula $\psi^{+}_{\varphi(\bar{y})}$ is

$\exists\bar{y}\exists\bar{z}\left(\varphi_{1}\ \wedge\ \varphi_{2}\ \wedge\
\varphi_{3}\ \wedge\ \varphi_{4}\right),$

where the additional conjunct $\varphi_{4}$ is defined as follows. For a CQ
$\chi(\bar{s})\in\mathsf{cq}^{\approx}(Q)$, we write $0pt{\chi(\bar{s}),Q}$
for the integer

$\min\\{0pt{T}\mid T\text{ is a }Q\text{-tree with
}\chi(\bar{s})\approx\mathsf{cq}(T)\\}$

that is, the smallest depth among all $Q$-trees whose induced CQ is isomorphic
to $\chi(\bar{s})$. Now, the formula $\varphi_{4}$ is

$\bigwedge\limits_{\begin{subarray}{c}\xi(\bar{s})\in\mathsf{cq}^{\approx}(Q)\\\
\text{with
}\xi=\exists\bar{u}(P_{1}(\bar{v}_{1}),\ldots,P_{m}(\bar{v}_{m})),\\\
0pt{\xi(\bar{s}),Q}<0pt{\varphi(\bar{y}),Q}\end{subarray}}\neg\exists\bar{s}\exists\bar{u}\bigg{(}\bigwedge\limits_{i\in[m]}\,P_{i}(\bar{v}_{i})\
\wedge\\\ (\bar{x}=\bar{s})\ \wedge\
\bigwedge\limits_{\begin{subarray}{c}u,v\in\mathsf{var}(\varphi),\\\ u\neq
v\end{subarray}}\neg(u=v)\bigg{)}$

which states that there is no other CQ
$\xi(\bar{s})\in\mathsf{cq}^{\approx}(Q)$ whose depth $d$ is smaller than the
one of $\varphi(\bar{y})$, and it witnesses the existence of a proof tree of
depth $d$ of a fact $R(\bar{t})$ w.r.t. $D$ and $\Sigma$, where $\bar{t}$ is
the tuple witnessed by $(x_{1},\ldots,x_{\mathsf{ar}(R)})$.

With the FO query $Q^{+}_{\varphi(\bar{y})}$ for each CQ
$\varphi(\bar{y})\in\mathsf{cq}^{\approx}(Q)$ in place, it should be clear
that the desired FO query $Q^{+}_{\mathit{FO}}$ is defined as
$\Phi^{+}(x_{1}\ldots,x_{\mathsf{ar}(R)})$, where

$\Phi^{+}\ =\
\bigvee_{\varphi(\bar{y})\in\mathsf{cq}^{\approx}(Q)}\psi^{+}_{\varphi(\bar{y})}.$

We proceed to show the correctness of the construction.

######  Lemma 37.

Given a non-recursive Datalog query $Q=(\Sigma,R)$, a database $D$ over
$\mathsf{edb}(\Sigma)$, $\bar{t}\in\mathsf{dom}(D)^{\mathsf{ar}(R)}$, and
$D^{\prime}\subseteq D$,
$D^{\prime}\in\mathsf{why}_{\mathsf{MD}}(\bar{t},D,Q)$ iff $\bar{t}\in
Q^{+}_{\mathit{FO}}(D^{\prime})$.

###### Proof.

We start with the $(\Rightarrow)$ direction. By hypothesis, there is a
minimal-depth proof tree $T$ of $R(\bar{t})$ w.r.t. $D$ and $\Sigma$ such that
$\mathsf{support}(T)=D^{\prime}$. By Lemma 12, we get that the CQ
$\varphi(\bar{y})\in\mathsf{cq}^{\approx}(Q)$ induced by $T$ is such that
$\bar{t}\in Q_{\varphi(\bar{y})}(D^{\prime})$. Thus, to prove that $\bar{t}\in
Q^{+}_{\varphi(\bar{y})}(D^{\prime})$, it suffices to show that $\bar{t}\in
Q^{\prime}(D^{\prime})$, where
$Q^{\prime}=\varphi_{4}(x_{1},\ldots,x_{\mathsf{ar}(R)})$ with $\varphi_{4}$
being

$\bigwedge\limits_{\begin{subarray}{c}\xi(\bar{s})\in\mathsf{cq}^{\approx}(Q)\\\
\text{with
}\xi=\exists\bar{u}(P_{1}(\bar{v}_{1}),\ldots,P_{m}(\bar{v}_{m})),\\\
0pt{\xi(\bar{s}),Q}<0pt{\varphi(\bar{y}),Q}\end{subarray}}\neg\exists\bar{s}\exists\bar{u}\bigg{(}\bigwedge\limits_{i\in[m]}\,P_{i}(\bar{v}_{i})\
\wedge\\\ (\bar{x}=\bar{s})\ \wedge\
\bigwedge\limits_{\begin{subarray}{c}u,v\in\mathsf{var}(\varphi),\\\ u\neq
v\end{subarray}}\neg(u=v)\bigg{)}.$

Towards a contradiction, assume that $\bar{t}\not\in Q^{\prime}(D^{\prime})$.
This in turn implies that there exists a CQ
$\xi(\bar{s})\in\mathsf{cq}^{\approx}(Q)$ of the form
$\exists\bar{u}(P_{1}(\bar{v}_{1}),\ldots,P_{m}(\bar{v}_{m}))$ with
$0pt{\xi(\bar{s}),Q}<0pt{\varphi(\bar{y}),Q}$ such that the sentence

$\exists\bar{s}\exists\bar{u}\bigg{(}\bigwedge\limits_{i\in[m]}\,P_{i}(\bar{v}_{i})\
\wedge\\\ (\bar{t}=\bar{s})\ \wedge\
\bigwedge\limits_{\begin{subarray}{c}u,v\in\mathsf{var}(\varphi),\\\ u\neq
v\end{subarray}}\neg(u=v)\bigg{)}$

is satisfied by $D^{\prime}$. This implies that there is an assignment $h$ to
the variables in $\xi$ with $h(\bar{s})=\bar{t}$, $h(u)\neq h(v)$, for each
$u,v\in\mathsf{var}(\xi)$ with $u\neq v$, and, for each $i\in[m]$,
$P_{i}(h(\bar{v}_{i}))\in D^{\prime}$. Since $\xi(\bar{s})$ is induced by a
$Q$-tree $T^{\prime}$ with depth $d=0pt{\xi(\bar{s}),Q}$, $T^{\prime}$ is a
proof tree of $R(\bar{t})$ w.r.t. $D$ and $\Sigma$ of depth $d$ such that

$\mathsf{support}(T^{\prime})=\\{P_{1}(h(\bar{v}_{1})),\ldots,P_{m}(h(\bar{v}_{m}))\\}\
\subseteq\ D^{\prime}.$

However, since

$0pt{T^{\prime}}\ =\ 0pt{\xi(\bar{s}),Q}\ <\ 0pt{\varphi(\bar{y}),Q}$

and

$0pt{\varphi(\bar{y}),Q}\ \leq\ 0pt{T},$

we conclude that $0pt{T^{\prime}}<0pt{T}$, which contradicts the fact that $T$
is a minimal-depth proof tree.

We now proceed with direction $(\Leftarrow)$. By hypothesis, $\bar{t}\in
Q^{+}_{\mathit{FO}}(D^{\prime})$. Therefore, there exists a CQ
$\varphi(\bar{y})\in\mathsf{cq}^{\approx}(Q)$ such that $\bar{t}\in
Q^{+}_{\varphi(\bar{y})}(D^{\prime})$. It is clear that $\bar{t}\in
Q_{\mathit{FO}}(D^{\prime})$, and form the proof of Lemma 12 we get that
$\varphi(\bar{y})$ is induced by a $Q$-tree $T$ that is also a proof tree of
$R(\bar{t})$ w.r.t. $D$ and $\Sigma$ with $\mathsf{support}(T)=D^{\prime}$. We
assume w.l.o.g. that $0pt{T}=0pt{\varphi(\bar{y}),Q}$, i.e., $T$ is the proof
tree of the smallest depth among those that induce $\varphi(\bar{y})$. It
remains to show that $T$ is a minimal-depth proof tree. Towards a
contradiction, assume that $T$ is not a minimal-depth proof tree. Thus, there
exists another proof tree $T^{\prime}$ for $R(\bar{t})$ w.r.t. $D$ and
$\Sigma$ with $0pt{T^{\prime}}<0pt{T}$. Let
$\xi(\bar{s})\in\mathsf{cq}^{\approx}(Q)$ be the CQ induced by $T^{\prime}$.
It is clear that

$0pt{\xi(\bar{s}),Q}\ \leq\ 0pt{T^{\prime}}\ <\ 0pt{\varphi(\bar{y}),Q}.$

This allows us to conclude that $\bar{t}\not\in
Q^{+}_{\varphi(\bar{y})}(D^{\prime})$, which is a contradiction. Consequently,
$T$ is a minimal-depth proof tree of $R(\bar{t})$ w.r.t. $D$ and $\Sigma$.
Since $\mathsf{support}(T)=D^{\prime}$, we get that
$D^{\prime}\in\mathsf{why}_{\mathsf{MD}}(R(\bar{t}),D,Q)$, as needed.

##  Appendix D Unambiguous Proof Trees

In this section, we provide proofs for all claims of Section 5, and provide
further details on our experimental evaluation.

###  D.1 Proof of Theorem 14

We start by proving Theorem 14, which we recall here for convenience:

######  Theorem 14.

The following hold:

  1. 1.

$\mathsf{Why\text{-}Provenance_{UN}[C]}$ is NP-complete in data complexity,
for each class $\mathsf{C}\in\\{\mathsf{Dat},\mathsf{LDat}\\}$.

  2. 2.

$\mathsf{Why\text{-}Provenance_{UN}[\mathsf{NRDat}]}$ is in $\rm AC_{0}$ in
data compl.

We prove item (1) and item (2) of Theorem 14 separately. We start by focusing
on item (1).

Proof of Item (1)

Our main task is to show that
$\mathsf{Why\text{-}Provenance_{UN}[\mathsf{Dat}]}$ is in NP. The NP-hardness
of $\mathsf{Why\text{-}Provenance_{UN}[\mathsf{LDat}]}$ follows from the NP-
hardness of $\mathsf{Why\text{-}Provenance_{NR}[\mathsf{LDat}]}$, which we
have already shown in Section B. The latter follows from the observation that,
in the case of linear Datalog programs, non-recursive proof trees and
unambiguous proof trees coincide. We now show the NP upper bound.

This result relies on a characterization of the existence of an unambiguous
proof tree of a fact $\alpha$ w.r.t. a database $D$ and a Datalog program
$\Sigma$ with $\mathsf{support}(T)=D^{\prime}\subseteq D$ via the existence of
a so-called unambiguous proof DAG $G$ of $\alpha$ w.r.t. $D$ and $\Sigma$ with
$\mathsf{support}(G)=D^{\prime}$ of polynomial size. This in turn allows us to
devise a guess-and-check algorithm that runs in polynomial time We proceed to
formalize the above high-level description.

For a rooted DAG $G=(V,E,\lambda)$ and a node $v\in V$, we use $G[v]$ to
denote the subDAG of $G$ rooted at $v$. Moreover, two rooted DAGs
$G=(V,E,\lambda)$ and $G^{\prime}=(V^{\prime},E^{\prime},\lambda^{\prime})$
are _isomorphic_ , denoted $G\approx G^{\prime}$, if there is a bijection
$h:V\rightarrow V^{\prime}$ such that , for each node $v\in V$,
$\lambda(v)=\lambda(h(v))$, and for each two nodes $u,v\in V$, $(u,v)\in E$
iff $(h(u),h(v))\in E^{\prime}$. With the above definitions in place, we can
now introduce the key notion of unambiguous proof DAG.

######  Definition 38 (Unambiguous Proof DAG).

Consider a Datalog program $\Sigma$, a database $D$ over
$\mathsf{edb}(\Sigma)$, and a fact $\alpha$ over $\mathsf{sch}(\Sigma)$. An
_unambiguous proof DAG of $\alpha$ w.r.t. $D$ and $\Sigma$_ is a proof DAG
$G=(V,E,\lambda)$ of $\alpha$ w.r.t. $D$ and $\Sigma$ such that, for all
$v,u\in V$, $\lambda(u)=\lambda(v)$ implies $G[u]\approx G[v]$.

We are now ready to present our characterization.

######  Proposition 39.

For a Datalog program $\Sigma$, there is a polynomial $f$ such that, for every
database $D$ over $\mathsf{edb}(\Sigma)$, fact $\alpha$ over
$\mathsf{sch}(\Sigma)$, and $D^{\prime}\subseteq D$, the following are
equivalent:

  1. 1.

There exists an unambiguous proof tree $T$ of $\alpha$ w.r.t. $D$ and $\Sigma$
such that $\mathsf{support}(T)=D^{\prime}$.

  2. 2.

There is an unambiguous proof DAG $G=(V,E,\lambda)$ of $\alpha$ w.r.t. $D$ and
$\Sigma$ with $\mathsf{support}(G)=D^{\prime}$ and $|V|\leq f(|D|)$.

###### Proof.

We first prove (1) implies (2). Let $T$ be an unambiguous proof tree of
$\alpha$ w.r.t. $D$ and $\Sigma$ with $\mathsf{support}(T)=D^{\prime}$. By
definition, the subtree count of $T$ is “small”; in fact, for every label
$\alpha$ of $T$, $|T[\alpha]_{/\approx}|=1$. We then employ the construction
underlying Lemma 8, which converts a proof tree of “small” subtree count into
proof DAG of polynomial size with the same support, since it preserves
unambiguity.

For (2) implies (1), we employ the “unravelling” construction used to prove
that (2) implies (1) in Proposition 5 since it also preserves unambiguity.

Finalize the Proof. With Proposition 39 in place, proving item (1) of Theorem
14 is straightforward. Indeed, we can employ a guess-and-check algorithm
similar in spirit to the one employed to prove the NP upper bound of Theorem
3. The key difference is that here we also need to verify that the guessed DAG
$G$ is unambiguous. This can be easily done by guessing, together with the
graph $G$, for every pair $u,v$ of nodes of $G$ with the same label, a
bijection $h_{(u,v)}$ from the nodes of $G[u]$ to the nodes of $G[v]$. The
number of nodes of $G$ is polynomial w.r.t. $|D|$, by Proposition 39, and thus
the number of bijections to guess is polynomial w.r.t. $|D|$. With the above
bijections in place, it is enough to verify that each bijection $h_{(u,v)}$
witnesses that $G[u]\approx G[v]$. The latter check can be easily performed in
polynomial time.

Proof of Item (2)

This is shown via first-order rewritability as done for Theorem 9. In fact,
the construction of the target FO query is exactly the same as in the proof of
Theorem 9 with the key difference that, for a Datalog query $Q$, the set of
CQs $\mathsf{cq}(Q)$ is defined by considering only unambiguous proof trees,
i.e., is the set $\\{\mathsf{cq}(T)\mid T\text{ is a {\em unambiguous}
$Q$-tree}\\}$.

###  D.2 Proof of Proposition 15

The goal is to prove Propostion 15. But first we need to introduce some
auxiliary notions and results, which will then allow us to formally define the
Boolean formula $\phi_{(\bar{t},D,Q)}$. We will then proceed with the proof of
Propostion 15

A More Refined Characterization. The Boolean formula in question relines on a
more refined characterization than the one provided by Proposition 39. For
this, we need to define a new kind of graph that witnesses the existence of an
unambiguous proof tree.

######  Definition 40 (Compressed DAG).

Consider a Datalog program $\Sigma$, a database $D$ over
$\mathsf{edb}(\Sigma)$, and a fact $\alpha$ over $\mathsf{sch}(\Sigma)$. A
_compressed DAG_ of $\alpha$ w.r.t. $D$ and $\Sigma$ is a rooted DAG
$G=(V,E)$, with $V\subseteq\mathsf{base}(D,\Sigma)$, such that:

  1. 1.

The root of $G$ is $\alpha$.

  2. 2.

If $\beta\in V$ is a leaf node, then $\beta\in D$.

  3. 3.

If $\beta\in V$ has $n\geq 1$ outgoing edges
$(\beta,\gamma_{1}),\ldots,(\beta,\gamma_{n})$, then there is a rule
$R_{0}(\bar{x}_{0})\ \text{:--}\
R_{1}(\bar{x}_{1}),\ldots,R_{m}(\bar{x}_{m})\in\Sigma$ and a function
$h:\bigcup_{i\in[m]}\bar{x}_{i}\rightarrow\mathbf{C}$ such that
$\beta=R_{0}(h(\bar{x}_{0}))$, and
$\\{\gamma_{i}\\}_{i\in[n]}=\\{R_{i}(h(\bar{x}_{i}))\mid i\in[m]\\}$.

A compressed DAG can be seen as a proof DAG-like structure where no more than
one node is labeled with the same fact. The above definition allows us to
refine the characterization given in Proposition 39 as follows; for a non-
labeled DAG $G=(V,E)$, with a slight abuse of notation, we denote
$\mathsf{support}(G)=\\{v\in V\mid v\text{ is a leaf of }G\\}$.

######  Proposition 41.

For a Datalog program $\Sigma$, database $D$ over $\mathsf{edb}(\Sigma)$, fact
$\alpha$ over $\mathsf{sch}(\Sigma)$, and database $D^{\prime}\subseteq D$,
the following are equivalent:

  1. 1.

There exists an unambiguous proof tree $T$ of $\alpha$ w.r.t. $D$ and $\Sigma$
such that $\mathsf{support}(T)=D^{\prime}$.

  2. 2.

There exists a compressed DAG $G$ of $\alpha$ w.r.t. $D$ and $\Sigma$, such
that $\mathsf{support}(G)=D^{\prime}$.

###### Proof.

We first prove that (1) implies (2). Due to Proposition 39, it suffices to
show that if there exists an unambiguous proof DAG
$G^{\prime}=(V^{\prime},E^{\prime},\lambda^{\prime})$ of $\alpha$ w.r.t. $D$
and $\Sigma$ such that $\mathsf{support}(G^{\prime})=D^{\prime}$, then there
exists a compressed DAG $G=(V,E)$ of $\alpha$ w.r.t. $D$ and $\Sigma$ with
$\mathsf{support}(G)=D^{\prime}$. Assume that
$G^{\prime}=(V^{\prime},E^{\prime},\lambda^{\prime})$ is an unambiguous proof
DAG of $\alpha$ w.r.t. $D$ and $\Sigma$ such that
$\mathsf{support}(G^{\prime})=D^{\prime}$. Since $G^{\prime}$ is unambiguous,
for every two non-leaf nodes $u,v\in V^{\prime}$ with
$\beta=\lambda^{\prime}(u)=\lambda^{\prime}(v)$, we must have that
$S=\\{\lambda^{\prime}(u_{1}),\ldots,\lambda^{\prime}(u_{n})\\}=\\{\lambda^{\prime}(v_{1}),\ldots,\lambda^{\prime}(v_{m})\\}$,
where $u_{1},\ldots,u_{n}$ and $v_{1},\ldots,v_{m}$ are the children of $u$
and $v$ in $G^{\prime}$, respectively. So, for each fact $\beta$ labeling a
non-leaf node in $G^{\prime}$, let us call the above (unique) set $S$ the
_justification of $\beta$ in $G^{\prime}$_. Hence, constructing a compressed
DAG $G=(V,E)$ for $\alpha$ w.r.t. $D$ and $\Sigma$, with
$\mathsf{support}(G)=D^{\prime}$ is straightforward. That is, the root of $G$
is $\alpha$, and if a node $\beta\in V$, letting
$S=\\{\gamma_{1},\ldots,\gamma_{n}\\}$ be its justification in $G^{\prime}$,
$G$ has nodes $\gamma_{1},\ldots,\gamma_{n}$, and edges
$(\beta,\gamma_{1}),\ldots,(\beta,\gamma_{n})$.

For proving (2) implies (1), we use an “unravelling” construction, similar to
the one employed in the proof of Proposition 5 to convert a proof DAG to a
proof tree. In particular, consider a compressed DAG $G=(V,E)$ of $\alpha$
w.r.t. $D$ and $\Sigma$ with $\mathsf{support}(G)=D^{\prime}$. By definition
of $G$, for each non-leaf node $\beta$ of $G$, its children
$\gamma_{1},\ldots,\gamma_{n}$ in $G$ are such that there exists a rule
$R_{0}(\bar{x}_{0})\ \text{:--}\
R_{1}(\bar{x}_{1}),\ldots,R_{m}(\bar{x}_{m})\in\Sigma$ and a function
$h:\bigcup_{i\in[m]}\bar{x}_{i}\rightarrow\mathbf{C}$ such that
$\beta=R_{0}(h(\bar{x}_{0}))$, and
$\\{\gamma_{i}\\}_{i\in[n]}=\\{R_{i}(h(\bar{x}_{i}))\mid i\in[m]\\}$; we call
$(\sigma,h)$ the _trigger of $\beta$ in $G$_, for some arbitrarily chosen pair
$(\sigma,h)$ as described above. We unravel $G$ into an unambiguous proof tree
$T=(V^{\prime},E^{\prime},\lambda^{\prime})$ of $\alpha$ w.r.t. $D$ and
$\Sigma$ as follows. We add a node $v$ to $T$ with label
$\lambda^{\prime}(v)=\alpha$. Then, if $v$ is a node of $T$ with some label
$\lambda^{\prime}(v)=\beta$, letting $(\sigma,h)$ be the trigger of $\beta$ in
$G$, where $\sigma=R_{0}(\bar{x}_{0})\ \text{:--}\
R_{1}(\bar{x}_{1}),\ldots,R_{m}(\bar{x}_{m})$, we add $m$ fresh new nodes
$u_{1},\ldots,u_{m}$ to $T$, where $u_{i}$ has label
$\lambda^{\prime}(u_{i})=R_{i}(h(\bar{x}_{i}))$, for $i\in[m]$, and we add
edges $(v,u_{1}),\ldots,(v,u_{m})$ to $T$. The fact that $T$ is a proof tree
of $\alpha$ w.r.t. $D$ and $\Sigma$ follows by construction. To see that $T$
is unambiguous, observe that by the definition of compressed DAG, and by the
construction of $T$, for every two non-leaf nodes $u,v$ of $T$ with the same
label $\beta$, $u$ and $v$ have the same number of children
$u_{1},\ldots,u_{n}$, and $v_{1},\ldots,v_{n}$, with
$\lambda^{\prime}(u_{i})=\lambda^{\prime}(v_{i})$, for $i\in[n]$. Clearly,
$\mathsf{support}(T)=D^{\prime}$.

With the above characterization in place, we are now ready to discuss how we
construct our Boolean formula.

Graph of Rule Instances and Downward Closure. For our purposes, a _(directed)
hypergraph_ $\mathcal{H}$ is a pair $(V,E)$, where $V$ is the set of _nodes_
of $\mathcal{H}$, and $E$ is the set of its _hyperedges_ , i.e., pairs of the
form $(\alpha,T)$, where $\alpha\in V$, and $\emptyset\subsetneq T\subseteq
V$. For two nodes $u,v$ of $\mathcal{H}$, we say that _$u$ reaches $v$ in
$\mathcal{H}$_, if either $u=v$, or there exists a sequence of hyperedges of
the form $(u_{1},T_{1}),\ldots,(u_{n},T_{n})$, with $u_{1}=u$, $v\in T_{n}$,
and $u_{i}\in T_{i-1}$ for $1<i\leq n$. For $u\in V$, we write
$\mathcal{H}_{\downarrow u}$ for the hypergraph $(V^{\prime},E^{\prime})$
obtained from $\mathcal{H}$, where $V^{\prime}$ contains $u$ and all nodes
reachable from $u$, and the hyperedges are all the hyperedges of $\mathcal{H}$
mentioning a node of $V^{\prime}$. We can now introduce the notion of graph of
rule instances.

######  Definition 42 (Graph of Rule Instances).

Consider a Datalog program $\Sigma$, and a database $D$ over
$\mathsf{edb}(\Sigma)$. The _graph of rule instances (GRI) of $D$ and
$\Sigma$_ is the hypergraph $\mathsf{gri}(D,\Sigma)=(V,E)$, with
$V\subseteq\mathsf{base}(D,\Sigma)$, such that

  1. 1.

For each $\alpha\in D$, $\alpha\in V$.

  2. 2.

If there exists a rule $R_{0}(\bar{x}_{0})\ \text{:--}\
R_{1}(\bar{x}_{1}),\ldots,R_{n}(\bar{x}_{n})$ in $\Sigma$ and a function
$h:\bigcup_{i\in[n]}\bar{x}_{i}\rightarrow\mathbf{C}$ such that
$\alpha_{i}=R_{i}(h(\bar{x}_{i}))\in V$, for $i\in[n]$, then
$\alpha_{0}=R_{0}(h(\bar{x}_{0}))\in V$, and
$(\alpha_{0},\\{\alpha_{1},\ldots,\alpha_{n}\\})\in E$.

Roughly, $\mathsf{gri}(D,\Sigma)$ is a structure that “contains” all possible
compressed DAGs of $\alpha$ w.r.t. $D$ and $\Sigma$. Since we are interested
in finding only compressed DAGs of a specific fact $\alpha$, we do not need to
consider $\mathsf{gri}(D,\Sigma)$ in its entirety, but we only need the sub-
hypergraph of $\mathsf{gri}(D,\Sigma)$ containing $\alpha$, and all nodes
reachable from it. Formally, for a Datalog program $\Sigma$, a database $D$
over $\mathsf{edb}(\Sigma)$, and a node (i.e., a fact) $\alpha$ of
$\mathsf{gri}(D,\Sigma)$, the _downward closure_ of $\alpha$ w.r.t. $D$ and
$\Sigma$ is the hypergraph
$\mathsf{down}(D,\Sigma,\alpha)=\mathsf{gri}(D,\Sigma)_{\downarrow\alpha}$. In
other words, the downward closure keeps from $\mathsf{gri}(D,\Sigma)$ only the
part that is relevant to derive the fact $\alpha$. It is easy to verify that
$\mathsf{down}(D,\Sigma,\alpha)$ “contains” all compressed DAGs of $\alpha$
w.r.t. $D$ and $\Sigma$, and the next technical result follows:

######  Lemma 43.

Consider a Datalog program $\Sigma$, a database $D$ over
$\mathsf{edb}(\Sigma)$, a fact $\alpha$ over $\mathsf{sch}(\Sigma)$, and a
compressed DAG $G=(V,E)$ of $\alpha$ w.r.t. $D$ and $\Sigma$. Then, for every
node $\beta\in V$ with outgoing edges
$(\beta,\gamma_{1}),\ldots,(\beta,\gamma_{n})$ in $G$, we have that
$(\beta,\\{\gamma_{1},\ldots,\gamma_{n}\\})$ is a hyperedge of
$\mathsf{down}(D,\Sigma,\alpha)$.

The Boolean Formula. We are now ready to introduce the desired Boolean
formula. For a Datalog query $Q=(\Sigma,R)$, a database $D$ over
$\mathsf{edb}(\Sigma)$, and a tuple
$\bar{t}\in\mathsf{dom}(D)^{\mathsf{ar}(R)}$, we construct in polynomial time
in $|D|$ the formula $\phi_{(\bar{t},D,Q)}$ such that the why-provenance of
$\bar{t}$ w.r.t. $D$ and $Q$ relative to unambiguous proof trees can be
computed from the truth assignments that make $\phi_{(\bar{t},D,Q)}$ true.

Let $\mathsf{down}(D,Q,R(\bar{t}))=(V,E)$. The set of Boolean variables of
$\phi_{(\bar{t},D,Q)}$ is composed of four disjoint sets $V_{N}$, $V_{H}$,
$V_{E}$, and $V_{C}$ of variables. Each variable in $V_{N}$ corresponds to a
node of $\mathsf{down}(D,Q,R(\bar{t}))$, i.e.,
$V_{N}=\\{x_{\alpha}\mid\alpha\in V\\}$, each variable in $V_{H}$ corresponds
to a hyperedge of $\mathsf{down}(D,Q,R(\bar{t}))$, i.e., $V_{H}=\\{y_{e}\mid
e\in E\\}$, and each variable in $V_{E}$ corresponds to a ”standard edge” that
can be extracted from a hyperedge of $\mathsf{down}(D,Q,R(\bar{t}))$, i.e.,
$V_{E}=\\{z_{(\alpha,\beta)}\mid(\alpha,T)\in E\text{ with }\beta\in T\\}$.
The set $V_{C}$ will be discussed later. Roughly, the variables in $V_{N}$ and
$V_{E}$ that will be true via a satisfying assignment of
$\phi_{(\bar{t},D,Q)}$ will induce the nodes and the edges of a compressed DAG
$G$ for $R(\bar{t})$ w.r.t. $D$ and $Q$, which, by Proposition 41, will imply
that $\mathsf{support}(G)\in\mathsf{why}_{\mathsf{UN}}(\bar{t},D,Q)$.

The formula $\phi_{(\bar{t},D,Q)}$ is of the form

$\phi_{\mathit{graph}}\wedge\phi_{\mathit{root}}\wedge\phi_{\mathit{proof}}\wedge\phi_{\mathit{acyclic}}.$

We proceed to discuss each of the above formulas. In the following, we use
$A\Rightarrow B$ as a shorthand for $\neg A\vee B$. The first formula
$\phi_{\mathit{graph}}$ is in charge of guaranteeing consistency between the
truth assignments of the variables in $V_{N}$ and the variables in $V_{E}$,
i.e., if an edge between two nodes is stated to be part of $G$, then the two
nodes must belong to G as well:

$\phi_{\mathit{graph}}=\bigwedge\limits_{z_{(\alpha,\beta)}\in
V_{E}}(z_{(\alpha,\beta)}\Rightarrow
x_{\alpha})\wedge(z_{(\alpha,\beta)}\Rightarrow x_{\beta}).$

The second formula $\phi_{\mathit{root}}$ guarantees that the atom
$R(\bar{t})$ is indeed a node of $G$, it is the root of $G$, and no other atom
that is a node of $G$ can be the root (i.e., it must always have at least one
incoming edge):

$\phi_{\mathit{root}}=x_{R(\bar{t})}\wedge\left(\bigwedge\limits_{z_{(\alpha,R(\bar{t}))}\in
V_{E}}\neg z_{(\alpha,R(\bar{t}))}\right)\wedge\\\
\bigwedge\limits_{\begin{subarray}{c}x_{\alpha}\in V_{N}\\\ \text{ with
}\alpha\neq
R(\bar{t})\end{subarray}}\left(x_{\alpha}\Rightarrow\bigvee\limits_{z_{(\beta,\alpha)}\in
V_{E}}z_{(\beta,\alpha)}\right).$

We now move to the next formula $\phi_{\mathit{proof}}$. Roughly, this formula
is in charge of ensuring that, whenever an intensional atom $\alpha$ is a node
of $G$, then it must have the correct children in $G$. That is, its children
are the ones coming from some hyperedge of $\mathsf{down}(D,Q,R(\bar{t}))$,
and no other nodes are its children (this is needed to guarantee that $G$ is a
_compressed_ DAG). This is achieved with two sub-formulas. The first part is
in charge of choosing some hyperedge $(\alpha,T)$ of
$\mathsf{down}(D,Q,R(\bar{t}))$, for each intensional atom $\alpha$, while the
second guarantees that for each selected hyperedge $(\alpha,T)$ (one per
intensional atom $\alpha$), _all and only_ the nodes in $T$ are children of
$\alpha$ in $G$:

$\phi_{\mathit{proof}}=\bigwedge\limits_{\begin{subarray}{c}x_{\alpha}\in
V_{N}\text{ with }\\\ \alpha\text{ intensional
}\end{subarray}}\left(x_{\alpha}\Rightarrow\bigvee\limits_{y_{(\alpha,T)}\in
V_{H}}y_{(\alpha,T)}\right)\wedge\\\
\bigwedge\limits_{\begin{subarray}{c}y_{e}\in V_{H}\\\ \text{with
}e=(\alpha,T)\end{subarray}}\left(\bigwedge\limits_{z_{(\alpha,\beta)}\in
V_{E}}y_{e}\Rightarrow\ell_{e,\beta}\right),$

where, for a hyperedge $e=(\alpha,T)$, $\ell_{e,\beta}$ denotes
$z_{(\alpha,\beta)}$ if $\beta\in T$, and $\neg z_{(\alpha,\beta)}$ otherwise.

Remark. Although we are interested in choosing _exactly one_ hyperedge
$(\alpha,T)$ for each intensional atom $\alpha$, the above formula uses a
simple disjunction rather an exclusive or. This is fine as any truth
assignment that makes two variables $y_{(\alpha,T_{1})}$ and
$y_{(\alpha,T_{2})}$ true cannot be a satisfying assignment, since the second
subformula in $\phi_{\mathit{proof}}$, e.g., requires that the variables
$z_{(\alpha,\beta)}$ with $\beta\in T_{1}$ are true, while all others must be
false. Hence, since $T_{1}\neq T_{2}$, when considering the hyperedge
$(\alpha,T_{2})$, this subformula will not be satisfied.

The remaining formula to discuss is $\phi_{\mathit{acyclic}}$. This last
formula is in charge of checking that $G$, i.e., the graph whose edges
correspond to the true variables in $V_{E}$, is acyclic. Checking acyclicity
of a graph encoded via Boolean variables in a Boolean formula is a well-
studied problem in the SAT literature, and thus different encodings exist. For
the sake of our construction, it is enough to use the simplest (yet, not very
efficient in practice) encoding, which just encodes the transitive closure of
the graph. However, for our experimental evaluation, we will implement this
formula using a more efficient encoding based on so-called vertex elimination,
which reduces by orders of magnitude the size of the formula
$\phi_{\mathit{acyclic}}$ (?).

To encode the transitive closure, we now need to employ the set of Boolean
variables $V_{C}$, having a variable of the form $t_{(\alpha,\beta)}$, for
every two nodes $\alpha,\beta$ of $\mathsf{down}(D,Q,R(\bar{t}))$.
Intuitively, $t_{(\alpha,\beta)}$ denotes whether a path exists from $\alpha$
to $\beta$ in $G$. With these variables in place, writing
$\phi_{\mathit{acyclic}}$ is straightforward: it just encodes the transitive
closure of the underlying graph, and then checks whether no cycle exists:

$\phi_{\mathit{acyclic}}=\left(\bigwedge\limits_{z_{(\alpha,\beta)}\in
V_{E}}z_{(\alpha,\beta)}\Rightarrow t_{(\alpha,\beta)}\right)\wedge\\\
\left(\bigwedge\limits_{\begin{subarray}{c}z_{(\alpha,\beta)}\in
V_{E},t_{(\beta,\gamma)}\in V_{C}\end{subarray}}z_{(\alpha,\beta)}\wedge
t_{(\beta,\gamma)}\Rightarrow t_{(\alpha,\gamma)}\right)\wedge\\\
\left(\bigwedge\limits_{t_{(\alpha,\alpha)}\in V_{C}}\neg
t_{(\alpha,\alpha)}\right).$

This completes the construction of our Boolean formula. One can easily verify
that the formula is in CNF, and that can be constructed in polynomial time. We
proceed to show its correctness, i.e., Proposition 15. For a truth assignment
$\tau$ from the variables of $\phi_{(\bar{t},D,Q)}$ to $\\{0,1\\}$, we write
$\mathsf{db}(\tau)$ for the database $\\{\alpha\in D\mid x_{\alpha}\in
V_{N}\text{ and }\tau(x_{\alpha})=1\\}$, i.e., the database collecting all
facts having a corresponding variable in $\phi_{(\bar{t},D,Q)}$ that is true
w.r.t. $\tau$. Finally, we let ${[\\![\phi_{(\bar{t},D,Q)}]\\!]}$ as

$\left\\{\mathsf{db}(\tau)\mid\tau\text{ is a satisfying assignment of
}\phi_{(\bar{t},D,Q)}\right\\}.$

We are now ready to prove Proposition 15, which we report here for
convenience:

######  Proposition 15.

Consider a Datalog query $Q=(\Sigma,R)$, a database $D$ over
$\mathsf{edb}(\Sigma)$, and a tuple
$\bar{t}\in\mathsf{dom}(D)^{\mathsf{ar}(R)}$. It holds that
$\mathsf{why}_{\mathsf{UN}}(\bar{t},D,Q)={[\\![\phi_{(\bar{t},D,Q)}]\\!]}$.

###### Proof.

Due to Proposition 41, it suffices to show that:

######  Lemma 44.

For every database $S\subseteq D$, the following are equivalent:

  1. 1.

There exists a compressed DAG $G$ of $R(\bar{t})$ w.r.t. $D$ and $\Sigma$ with
$\mathsf{support}(G)=S$.

  2. 2.

There exists a satisfying truth assignment $\tau$ of $\phi_{(\bar{t},D,Q)}$
such that $\mathsf{db}(\tau)=S$.

###### Proof.

We start with the implication $(1)\Rightarrow(2)$. Assume that $G=(V,E)$ is a
compressed DAG for $R(\bar{t})$ w.r.t. $D$ and $\Sigma$ with
$\mathsf{support}(G)=S$. We construct the following truth assignment $\tau$ of
$\phi_{(\bar{t},D,Q)}$:

  * •

For each $x_{\alpha}\in V_{N}$, $\tau(x_{\alpha})=1$ if $\alpha$ is a node of
$G$, otherwise $\tau(x_{\alpha})=0$.

  * •

For each $z_{(\alpha,\beta)}\in V_{E}$, $\tau(z_{(\alpha,\beta)})=1$ if there
is an edge $(\alpha,\beta)$ in $G$, otherwise $\tau(z_{(\alpha,\beta)})=0$.

  * •

For each $y_{(\alpha,T)}\in V_{H}$, $\tau(y_{(\alpha,T)})=1$ if $\alpha$ is a
node in $G$ with outgoing edges $(\alpha,\beta_{1}),\ldots,(\alpha,\beta_{n})$
such that $T=\\{\beta_{1},\ldots,\beta_{n}\\}$, otherwise
$\tau(y_{(\alpha,T)})=0$.

  * •

For each $t_{(\alpha,\beta)}\in V_{C}$, $\tau(t_{(\alpha,\beta)})=1$ if there
is a path from $\alpha$ to $\beta$ in $G$, otherwise
$\tau(t_{(\alpha,\beta)})=0$.

We now claim that $\tau$ makes $\phi_{(\bar{t},D,Q)}$ true and
$\mathsf{db}(\tau)=S$.

Observation 1. By Lemma 43, every node $\alpha$ of $G$ has a variable
$x_{\alpha}$ in $\phi_{(\bar{t},D,Q)}$. Similarly, if a node $\alpha$ has
outgoing edges $(\alpha,\beta_{1}),\ldots,(\alpha,\beta_{n})$ in $G$, then
$z_{(\alpha,\beta_{i})}$ for $i\in[n]$, and $y_{(\alpha,T)}$, with
$T=\\{\beta_{1},\ldots,\beta_{n}\\}$, are all variables of
$\phi_{(\bar{t},D,Q)}$.

From Observation 1, each fact $\alpha\in\mathsf{support}(G)=S$ has a
corresponding variable $x_{\alpha}$ in $\phi_{(\bar{t},D,Q)}$. Moreover, by
construction of $\tau$, $\tau(x_{\alpha})=1$ for each $\alpha\in S$.
Furthermore, for all facts $\beta$ of $D$ not in $S$ it means there is no node
in $G$ labeled with $\beta$, and thus $\tau(x_{\beta})=0$. Hence
$\mathsf{db}(\tau)=S$.

We now show that $\tau$ makes $\phi_{(\bar{t},D,Q)}$ true. We proceed by
considering its subformulas separately.

$\phi_{\mathit{graph}}$.

It is clear that $\tau$ makes this formula true since when
$\tau(z_{(\alpha,\beta)})=1$, it means that $\alpha$ and $\beta$ are nodes of
$G$, and thus, by construction of $\tau$,
$\tau(x_{\alpha})=\tau(x_{\beta})=1$.

$\phi_{\mathit{root}}$.

Since $R(\bar{t})$ is the root of $G$, by Observation 1 and by construction of
$\tau$, $\tau(x_{R(\bar{t})})=1$. To see why the formula

$\left(\bigwedge\limits_{z_{(\alpha,R(\bar{t}))}\in V_{E}}\neg
z_{(\alpha,R(\bar{t}))}\right)$

is true, since $R(\bar{t})$ is the root, it does not have any incoming edges,
and thus, by construction of $\tau$, $\tau(z_{(\alpha,R(\bar{t}))})=0$, for
each $z_{(\alpha,R(\bar{t}))}\in V_{E}$. Finally, regarding the formula

$\bigwedge\limits_{\begin{subarray}{c}x_{\alpha}\in V_{N}\\\ \text{ with
}\alpha\neq
R(\bar{t})\end{subarray}}\left(x_{\alpha}\Rightarrow\bigvee\limits_{z_{(\beta,\alpha)}\in
V_{E}}z_{(\beta,\alpha)}\right),$

if $\tau(x_{\alpha})=1$, for some $\alpha\neq R(\bar{t})$, by construction of
$\tau$, $\alpha$ is a node of $G$. By Observation 1, for every edge
$(\beta,\alpha)$ in $G$, we have that $z_{(\beta,\alpha)}$ is a variable of
$\phi_{(\bar{t},D,Q)}$, and $\tau(z_{(\beta,\alpha)})=1$, hence the
disjunction is true.

$\phi_{\mathit{proof}}$.

We start by considering the formula

$\bigwedge\limits_{\begin{subarray}{c}x_{\alpha}\in V_{N}\text{ with }\\\
\alpha\text{ intensional
}\end{subarray}}\left(x_{\alpha}\Rightarrow\bigvee\limits_{y_{(\alpha,T)}\in
V_{H}}y_{(\alpha,T)}\right).$

If $\tau(x_{\alpha})=1$, for some intensional fact $\alpha$, it means that
$\alpha$ is a node of $G$. Let $(\alpha,\beta_{1}),\ldots,(\alpha,\beta_{n})$
be the outgoind edges of $\alpha$ in $G$. By Observation 1, $y_{(\alpha,T)}$,
with $T=\\{\beta_{1},\ldots,\beta_{n}\\}$, is a variable of
$\phi_{(\bar{t},D,Q)}$, and by construction of $\tau$,
$\tau(y_{(\alpha,T)})=1$, hence the disjunction is true. We now consider the
formula

$\bigwedge\limits_{\begin{subarray}{c}y_{e}\in V_{H}\\\ \text{with
}e=(\alpha,T)\end{subarray}}\left(\bigwedge\limits_{z_{(\alpha,\beta)}\in
V_{E}}y_{e}\Rightarrow\ell_{e,\beta}\right).$

If $\tau(y_{e})=1$, for $e=(\alpha,T)$, then $\alpha$ is a node of $G$ with
outgoing edges $(\alpha,\beta_{1}),\ldots,(\alpha,\beta_{n})$, where
$T=\\{\beta_{1},\ldots,\beta_{n}\\}$. By Observation 1,
$z_{(\alpha,\beta_{i})}\in V_{E}$, for $i\in[n]$, and by construction of
$\tau$, $\tau(z_{(\alpha,\beta_{i})})=1$, for $i\in[n]$. Hence, all
implications of the form $y_{e}\Rightarrow\ell_{e,\beta}$, where
$\beta\in\\{\beta_{1},\ldots,\beta_{n}\\}$ are true. Regarding the other
implications, i.e., when $\beta\not\in\\{\beta_{1},\ldots,\beta_{n}\\}$, since
$\alpha$ has no other outgoing edges in $G$, by construction of $\tau$,
$\tau(z_{(\alpha,\beta)})=0$, for all other facts
$\beta\not\in\\{\beta_{1},\ldots,\beta_{n}\\}$. Hence, the whole formula is
satisfied.

$\phi_{\mathit{acyclic}}$.

The fact that the formula is true follows from the acyclicity of $G$,
Observation 1, and the construction of $\tau$.

We now proceed with $(2)\Rightarrow(1)$. By hypothesis, there is a truth
assignment $\tau$ that makes $\phi_{(\bar{t},D,Q)}$ true and
$\mathsf{db}(\tau)=S$. We define the auxiliary sets

$\displaystyle\mathsf{nodes}(\tau)$ $\displaystyle=$
$\displaystyle\\{\alpha\mid x_{\alpha}\in V_{N}\text{ and
}\tau(x_{\alpha})=1\\}$ $\displaystyle\mathsf{edges}(\tau)$ $\displaystyle=$
$\displaystyle\\{(\alpha,\beta)\mid z_{(\alpha,\beta)}\in V_{E}\text{ and
}\tau(z_{(\alpha,\beta)})=1\\}.$

Since $\tau$ makes $\phi_{\mathit{graph}}$ true, every fact occurring in
$\mathsf{edges}(\tau)$ also occurrs in $\mathsf{nodes}(\tau)$; hence,
$G=(\mathsf{nodes}(\tau),\mathsf{edges}(\tau))$ is a well-defined directed
graph. Moreover, since $\mathsf{db}(\tau)=S$, all the nodes without outgoing
edges in $G$ are precisely the ones in $S$. Finally, since $\tau$ makes
$\phi_{\mathit{acyclic}}$ true, $G$ is acyclic, and since $\tau$ satisfies
$\phi_{\mathit{root}}$, $R(\bar{t})$ is the only node of $G$ without incoming
edges. Thus, $G$ is a DAG, its root is $R(\bar{t})$, and its leaves is exactly
the set $S$. It remains to argue that $G$ is a compressed DAG of $R(\bar{t})$
w.r.t. $D$ and $\Sigma$.

Consider a node $\alpha$ of $G$ which is an intensional fact. It is clear that
$\tau(x_{\alpha})=1$, and thus, the dijunction in $\phi_{\mathit{proof}}$ must
be true. Hence, $\tau(y_{(\alpha,T)})=1$, for some hyperedge $(\alpha,T)$ of
$\mathsf{down}(D,Q,R(\bar{t}))$. In particular, since $\tau$ makes

$\bigwedge\limits_{\begin{subarray}{c}y_{e}\in V_{H}\\\ \text{with
}e=(\alpha,T)\end{subarray}}\left(\bigwedge\limits_{z_{(\alpha,\beta)}\in
V_{E}}y_{e}\Rightarrow\ell_{e,\beta}\right)$

true in $\phi_{\mathit{proof}}$, and $\tau(y_{(\alpha,T)})=1$, we must have
that $\tau$ assigns $1$ to all variables of the form $z_{(\alpha,\beta)}$ with
$\beta\in T$, and $0$ to all other variables of the form $z_{(\alpha,\beta)}$
with $\beta\not\in T$. This means that there is no other variable of the form
$y_{(\alpha,T^{\prime})}$ with $T^{\prime}=T$ that is assigned $1$ by $\tau$.
Hence, for each node $\alpha$ of $G$ which is intensional, $\alpha$ has
outgoing edges $(\alpha,\beta_{1}),\ldots,(\alpha,\beta_{n})$, and these are
such that there exists a hyperedge of $\mathsf{down}(D,Q,R(\bar{t}))$ of the
form $(\alpha,T)$, with $T=\\{\beta_{1},\ldots,\beta_{n}\\}$. The latter, by
definition of downward closure, implies that for each node $\alpha$ of $G$
which is intensional, $\alpha$ has outgoing edges
$(\alpha,\beta_{1}),\ldots,(\alpha,\beta_{n})$, and these are such that there
exists a rule $\sigma\in\Sigma$ of the form $R_{0}(\bar{x}_{0})\ \text{:--}\
R_{1}(\bar{x}_{1}),\ldots,R_{m}(\bar{x}_{m})$, with $m\geq n$, and a function
$h:\bigcup_{i\in[n]}\bar{x}_{i}\rightarrow\mathbf{C}$, such that
$R_{0}(h(\bar{x}_{0}))=\alpha$ and
$\\{R_{1}(h(\bar{x}_{1})),\ldots,R_{m}(h(\bar{x}_{m}))\\}=\\{\beta_{1},\ldots,\beta_{n}\\}$.
Hence, $G$ is a compressed DAG of $R(\bar{t})$ w.r.t. $D$ and $\Sigma$, as
needed.

Proposition 15 immediately follows from Lemma 44.

###  D.3 Implementation Details

In this section, we expand on the discussion of our implementation presented
in the main body of the paper. In what follows, fix a Datalog query
$Q=(\Sigma,R)$, a database $D$ over $\mathsf{edb}(\Sigma)$, and a tuple
$\bar{t}\in\mathsf{dom}(D)^{\mathsf{ar}(R)}$.

Constructing the Downward Closure. Recall that the construction of
$\phi_{(\bar{t},D,Q)}$ relies on the downward closure of $R(\bar{t})$ w.r.t.
$D$ and $\Sigma$. It turns out that the hyperedges of the downward closure can
be computed by executing a slightly modified Datalog query $Q_{\downarrow}$
over a slightly modified database $D_{\downarrow}$. In other words, the
answers to $Q_{\downarrow}$ over $D_{\downarrow}$ coincide with the hyperedges
of the downward closure. For this, we are going to adopt a slight modification
of an existing approach presented in (?). In that paper, the authors were
studying the problem of computing the why-provenance of Datalog queries w.r.t.
_standard_ proof trees. However, except for the construction of
$\mathsf{down}(D,Q,R(\bar{t}))$, their approach to compute the supports for
general trees is fundamentally different from ours, since they employ
existential rule-based engines rather than SAT solvers; it is not clear how
their approach could be adapted for our purposes, as we require checking
whether the underlying trees are unambiguous. Moreover, the approach of (?)
computes the _whole set_ of supports all at once, while our approach based on
SAT solvers allows to _enumerate_ supports, and thus allows the incremental
construction of the why-provenance. Nonetheless, the construction of
$\mathsf{down}(D,Q,R(\bar{t}))$ is common to both approaches, and thus we
borrow the techniques of (?) for this task, which we briefly recall in the
following.

The main idea is to employ an existing Datalog engine to compute the answers
of a query $Q_{\downarrow}$ obtained from $Q$ over a slight modification
$D_{\downarrow}$ of $D$; the answers in $Q_{\downarrow}(D_{\downarrow})$ will
coincide with all the hyperedges of $\mathsf{down}(D,Q,R(\bar{t}))$. To this
end, the rules of $Q_{\downarrow}$ contain all the rules in $\Sigma$, which
will be in charge of deriving all nodes of $\mathsf{gri}(D,\Sigma)$, plus an
additional set of rules that will be in charge of using such nodes to
construct all the hyperedges of $\mathsf{down}(D,Q,R(\bar{t}))$. Formally, let
$\omega$ be the maximum arity of predicates in $\Sigma$, and $b$ the maximum
number of atoms in the body of a rule of $\Sigma$. We define two new
predicates:

  * •

$\mathsf{CurNode}$ of arity $\omega+1$ that stores the current node of
$\mathsf{down}(D,Q,R(\bar{t}))$ being processed during the evaluation of
$Q_{\downarrow}$.

  * •

$\mathsf{HEdge}$ of arity $(\omega+1)+b\times(\omega+1)$, which stores the
hyperedges being constructed during the evaluation of $Q_{\downarrow}$.

Furthermore, for an atom $\alpha=P(\bar{u})$, we denote $\langle\alpha\rangle$
as the tuple of length $\omega+1$ of the form
$c_{P},\bar{u},\star,\ldots,\star$, where $c_{P}$ and $\star$ are constants
not in $D$. Intuitively, $\langle\alpha\rangle$ encodes the atom $\alpha$ as a
tuple of fixed length. Finally, for an atom $\alpha$ and a sequence of atoms
$\beta_{1},\ldots,\beta_{n}$, with $n\leq b$, we use
$\langle\alpha,\beta_{1},\ldots,\beta_{n}\rangle$ to denote the tuple of
length $(\omega+1)+b\times(\omega+1)$ of the form
$\langle\alpha\rangle,\langle\beta_{1}\rangle,\ldots,\langle\beta_{n}\rangle,\star,\ldots,\star$.

We define the Datalog query $Q_{\downarrow}=(\Sigma^{\prime},\mathsf{HEdge})$,
where $\Sigma^{\prime}=\Sigma\cup\Sigma^{\prime\prime}$, where, for each rule
$\sigma\in\Sigma$ of the form $R_{0}(\bar{x}_{0})\ \text{:--}\
R_{1}(\bar{x}_{1}),\ldots,R_{n}(\bar{x}_{n})$, $\Sigma^{\prime\prime}$
contains the rules

$\sigma_{1}\ =\ \mathsf{HEdge}(\langle
R_{0}(\bar{x}_{0}),R_{1}(\bar{x}_{1}),\ldots,R_{n}(\bar{x}_{n})\rangle)\
\text{:--}\ \\\ \mathsf{CurNode}(\langle
R_{0}(\bar{x}_{0})\rangle),R_{1}(\bar{x}_{1}),\ldots,R_{n}(\bar{x}_{n})$

and, for each $i\in[n]$,

$\sigma^{(i)}_{2}\ =\ \mathsf{CurNode}(\langle R_{i}(\bar{x}_{i})\rangle)\
\text{:--}\ \\\ \mathsf{CurNode}(\langle
R_{0}(\bar{x}_{0})\rangle),R_{1}(\bar{x}_{1}),\ldots,R_{n}(\bar{x}_{n}).$

Essentially, the rule $\sigma_{1}$ will construct a hyperedge $(\alpha,T)$ of
$\mathsf{down}(D,Q,R(\bar{t}))$ whenever it is known that $\alpha$ is a node
of $\mathsf{down}(D,Q,R(\bar{t}))$, and all the atoms in $T$ are used in
$\mathsf{gri}(D,\Sigma)$ to generate $\alpha$. The rules of the form
$\sigma^{(i)}_{2}$ are marking the new nodes as being part of
$\mathsf{down}(D,Q,\bar{t})$. Note that the rules of $\Sigma^{\prime\prime}$
contain constants, whereas, according to our definition, rules are constant-
free. Nevertheless, all existing Datalog engines support rules with constants,
and for the sake of keeping the discussion simple, we slightly abuse our
definition of rules in this section. It is easy to adapt the above set of
rules to a set of rules without constants, by adding some auxiliary facts to
the database.

The database $D_{\downarrow}$ is $D\cup\\{\mathsf{CurNode}(\langle
R(\bar{t})\rangle)\\}$, which simply states that $R(\bar{t})$ must be a node
of $\mathsf{down}(D,Q,R(\bar{t}))$. One can easily see that each tuple in
$Q_{\downarrow}(D_{\downarrow})$ encodes a hyperedge of
$\mathsf{down}(D,Q,R(\bar{t}))$, and thus, we can construct
$\mathsf{down}(D,Q,R(\bar{t}))$ by simply asking $Q_{\downarrow}$ over
$D_{\downarrow}$.

Let us note that the main differences between our definition of
$Q_{\downarrow}$ and $D_{\downarrow}$ w.r.t. the ones of (?) is that we encode
nodes and hyperedges of $\mathsf{down}(D,Q,R(\bar{t}))$ as tuples, which
allows us to employ the same Datalog engine that is used to answer the
original query $Q$, rather than using external engines supporting more
expressive languages such as existential rules.

Constructing the Formula. Regarding the construction of the formula
$\phi_{(\bar{t},D,Q)}$, as already discussed before, for efficiency reasons,
we consider a different encoding of the subformula $\phi_{\mathit{acyclic}}$.
Rather than using the transitive closure, we employ the technique of vertex
elimination (?). The advantage of this approach is that it requires a number
of Boolean variables for the encoding of $\phi_{\mathit{acyclic}}$ which is of
the order of $O(n\times\delta)$, where $n$ is the number of nodes of the
underlying graph, and $\delta$ is the so-called _elimination width_ of the
graph, which, roughly, is related to how connected the underlying graph is.
Hence, we can avoid the costly construction of quadratically many variables
whenever the elimination width is low.

Incrementally Constructing the Why-Provenance. Recall that we are interested
in the incremental computation of the why-provenance, which is more useful in
practice than computing the whole set at once. To this end, we need a way to
enumerate all the members of the why-provenance without repetitions. This is
achieved by adapting a standard technique from the SAT literature for
enumerating the satisfying assignments of a Boolean formula, called blocking
clause. We initially collect in a set $S$ all the facts of $D$ occurring in
the downward closure of $R(\bar{t})$ w.r.t. $D$ and $\Sigma$. Then, after
asking the SAT solver for an arbitrary satisfying assignment $\tau$ of
$\phi_{(\bar{t},D,Q)}$, we output the database $\mathsf{db}(\tau)$, and then
construct the “blocking” clause $\vee_{\alpha\in S}\ell_{\alpha},$ where
$\ell_{\alpha}=\neg x_{\alpha}$ if $\alpha\in\mathsf{db}(\tau)$, and
$\ell_{\alpha}=x_{\alpha}$ otherwise. We then add this clause to the formula,
which expresses that no other satisfying assignment $\tau^{\prime}$ 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.

---
(a) $\mathsf{Doctors}$
|
(b) $\mathsf{TransClosure}$ | (c) $\mathsf{Galen}$
|
(d) $\mathsf{Andersen}$ | (e) $\mathsf{CSDA}$
Figure 3: Building the downward closure and the Boolean formula (all
scenarios).

###  D.4 Experimental Evaluation

In this section, we provide further details on the performance of our SAT-
based approach, by presenting the results of the experimental evaluation over
all the scenarios we considered in the paper; we report again the
$\mathsf{Andersen}$ scenario for the sake of completeness. Recall that in our
experimental analysis we consider two main tasks separately: (1) construct the
downward closure and the Boolean formula, and (2) incrementally compute the
why-provenance using the SAT solver.

Concerning task 1, we report in Figure 3 one plot for each scenario we
consider, where in each plot we report the total running time for each
database of that scenario. Furthermore, for each plot, and each database
considered therein, we have five bars, that correspond to the five randomly
chosen tuples. Each such bar shows the time for building the downward closure
plus the time for constructing the Boolean formula. To ease the presentation,
we grouped the $\mathsf{Doctors}$-based scenarios in one plot (recall that all
such scenarios share a single database).

We can see that in most of the scenarios, the running time is in the order of
some seconds. This is especially true for the $\mathsf{TransClosure}$ and
$\mathsf{Doctors}$-based scenarios, having the simplest queries, while for the
$\mathsf{Galen}$ scenario, where the query is more complex, as it involves
non-linear recursion, the time is slightly higher for the largest database
$D_{4}$. The $\mathsf{Andersen}$ and $\mathsf{CSDA}$ scenarios are the most
challenging, since they both contain very large databases. Moreover, although
the databases in $\mathsf{Andersen}$ are smaller than those of
$\mathsf{CSDA}$, the complexity of its query, which involves non-linear
recursion, makes the running time of $\mathsf{Andersen}$ over its largest
database (6.8M facts) comparable to $\mathsf{CSDA}$ with the larger database
$D_{\mathsf{httpd}}$ (10M facts). Of course, for the much larger databases
$D_{\mathsf{postgresql}}$ and $D_{\mathsf{linux}}$, the running time is much
higher, going up to 6-7 minutes for some tuples. Considering the size of the
databases at hand, we believe the running times for these last scenarios are
quite reasonable. As already discussed in the main body of the paper, we
observed that most of the time is spent in building the downward closure.

Concerning task 2, that is, the incremental computation of the why-provenance,
we present in Figure 4 one plot for each scenario we consider, where in each
plot of scenario $s$ we report, for each database of $s$, the times required
to build an explanation, that is, the time between the current member of the
why-provenance and the next one (this time is also known as the delay). Each
plot collects the delays of constructing the members of the why-provenance (up
to a limit of 10K members or 5 minutes timeout) for each of the five randomly
chosen tuples. We use box plots, where the bottom and the top borders of the
box represent the first and third quartile, i.e., the delay under which 25%
and 75% of all delays occur, respectively, and the orange line represents the
median delay. Moreover, the bottom and the top whisker represent the minimum
and maximum delay, respectively. All times are expressed in milliseconds and
we use logarithmic scale. As we did for task 1, we grouped the
$\mathsf{Doctors}$-based scenarios in one plot.

---
(a) $\mathsf{Doctors}$
|
(b) $\mathsf{TransClosure}$ | (c) $\mathsf{Galen}$
|
(d) $\mathsf{Andersen}$ | (e) $\mathsf{CSDA}$
Figure 4: Incremental computation of the why-provenance (all scenarios).

As observed in the main body of the paper, most of the delays are even lower
than 1 millisecond, with the median in the order of microseconds. Therefore,
once we have the Boolean formula in place, incrementally computing the members
of the why-provenance is extremely fast. The worst case occurs in the
$\mathsf{TransClosure}$ scenario, when considering the Facebook database,
where we also have the only two cases where the construction of the supports
exceeds the 5 minutes mark before being able to construct 10K supports, i.e.,
for the third and fifth tuple. Overall, in the $\mathsf{TransClosure}$
scenario w.r.t. the Facebook database, the average delay is higher, and some
supports require up to 10 seconds to be constructed. We believe that this has
to do with the fact that the database $D_{\text{facebook}}$ encodes a graph
which is highly connected, and thus the CNF formula, and in particular the
formula $\phi_{\mathit{acyclic}}$ encoding the acyclicity check, becomes quite
large, and thus is much more demanding for the SAT solver. This was somehow
expected since the vertex-elimination technique for checking acyclicity
performs better the less connected the underlying graph is. We have confirmed
this by running some other experiments with databases taken from (?), which
contain highly connected, synthetic graphs. In this case, although
constructing the downward closure is very efficient (in the order of seconds),
the construction of the formula $\phi_{\mathit{acyclic}}$ goes out of memory.
Hence, we expect that in applications where highly connected input graphs are
common, a different approach for checking acyclicity in a CNF formula would be
required. Nonetheless, we can safely conclude that in most cases, computing
the members of the why-provenance can be done very efficiently.

###  D.5 Comparative Evaluation

As mentioned in Section 6, we have performed a preliminary comparison with
(?). We conclude this section by discussing the details of this comparative
evaluation. Let us first clarify that our implementation deals with a
different problem. For a Datalog query $Q=(\Sigma,R)$, a database $D$ over
$\mathsf{edb}(\Sigma)$, and a tuple
$\bar{t}\in\mathsf{dom}(D)^{\mathsf{ar}(R)}$, the approach from (?) has been
designed and evaluated for building the whole set $\mathsf{why}(\bar{t},D,Q)$,
whereas our approach has been designed and evaluated for incrementally
computing $\mathsf{why}_{\mathsf{UN}}(\bar{t},D,Q)$. However, there is a
setting where a reasonable comparison can be performed, which will provide
some insights for the two approaches. This is when the Datalog query $Q$ is
both linear and non-recursive in which case the sets
$\mathsf{why}(\bar{t},D,Q)$ and $\mathsf{why}_{\mathsf{UN}}(\bar{t},D,Q)$
coincide since a proof tree of $R(\bar{t})$ w.r.t. $D$ and $\Sigma$ is
trivially unambiguous. Therefore, towards a fair comparison, we are going to
consider the scenarios $\mathsf{Doctors}\text{-}i$, for $i\in[7]$, which
consist of a Datalog query that is linear and non-recursive, and consider the
end-to-end runtime of our approach (not the delays) without, of course,
setting a limit on the number of members of why-provenance to build, or on the
total runtime.

The comparison is shown in Figure 5. For each scenario, we present the runtime
for all five randomly chosen tuples for our approach (in blue) and the
approach of (?) (in red); if a bar is missing for a certain tuple, then the
execution ran out of memory. We observe that for the simple scenarios the two
approaches are comparable in the order of a second. Now, concerning the
demanding scenarios, i.e., $\mathsf{Doctors}\text{-}i$ for $i\in\\{1,5,7\\}$,
we observe that our approach is, in general, faster. Observe also that for
some of the most demanding cases, the approach of (?) runs out of memory. We
believe that the latter is due to the use of the rule engine VLog, which is
intended for materialization-based reasoning with existential rules, whereas
our approach relies on a Datalog engine (in particular, DLV), and thus,
exploiting all the optimizations that are typically employed for evaluating a
Datalog query. For example, the technique of magic-set rewriting, implemented
by DLV, can greatly reduce the memory usage by building much fewer facts
during the evaluation of the rules; see, e.g., (?).

Figure 5: Comparison of the end-to-end computation of the why-provenance.