If $n=1$, the claim is trivial, so we assume $n>1$. Trivially,
$\mathrm{op}(\mathcal{M}_{1},\mathcal{M}_{2})\to r=1$, so the claim is also
trivial for $j=r$. We now examine the general case of $j\neq r$, for which we
will use the inductive hypothesis of $n-1$. Based on Equation 7, we have that

$\mathrm{op}(\mathcal{M}_{1},\mathcal{M}_{2})\to
j=(\mathrm{op}(\mathcal{M}_{1}^{0},\mathcal{M}_{2}^{0})\to
j)+(\mathrm{op}(\mathcal{M}_{1}^{1},\mathcal{M}_{2}^{1})\to j)$

Note that $\mathrm{op}(\mathcal{M}_{1}^{0},\mathcal{M}_{2}^{0})$ and
$\mathrm{op}(\mathcal{M}_{1}^{1},\mathcal{M}_{2}^{1})$ are COBDDs of dimension
$n-1$, as they do not include label $r$. Then, by inductive hypothesis, we
have that

$(\mathrm{op}(\mathcal{M}_{1}^{0},\mathcal{M}_{2}^{0})\to
j)+(\mathrm{op}(\mathcal{M}_{1}^{1},\mathcal{M}_{2}^{1})\to
j)\leq(\mathcal{M}_{1}^{0}\to j)+(\mathcal{M}_{2}^{0}\to
j)+(\mathcal{M}_{1}^{1}\to j)+(\mathcal{M}_{2}^{1}\to j)$

But by definition,

$\mathcal{M}_{i}\to j=(\mathcal{M}_{i}^{0}\to j)+(\mathcal{M}_{i}^{1}\to
j)\qquad(i\in\\{1,2\\}).$

By combining the three previous equations, we get the desired result:

$\mathrm{op}(\mathcal{M}_{1},\mathcal{M}_{2})\to j\leq(\mathcal{M}_{1}\to
j)+(\mathcal{M}_{2}\to j).$

∎

We are now ready to finish the proof of the lemma. As for a model
$\mathcal{M}$ of dimension $n$ we have that
$\mathrm{width}(\mathcal{M})=\max_{1\leq j\leq n}(\mathcal{M}\to j)$, it
follows from Claim 7 that

$\mathrm{width}\left(\mathrm{op}(\mathcal{M}_{1},\mathcal{M}_{2})\right)\leq\max_{1\leq
j\leq n}(\mathcal{M}_{1}\to j)+(\mathcal{M}_{2}\to
j)\leq\mathrm{width}(\mathcal{M}_{1})+\mathrm{width}(\mathcal{M}_{2})$

which concludes the proof. ∎

We now state a lemma of Capelli and Mengel [8, 9] that will be used in our
proof, but before let us introduce appropriate notation. Given a COBDD
$\mathcal{M}$ of dimension $n$, and a set $S\subseteq\\{1,\ldots,n\\}$ we
define $\exists_{S}\mathcal{M}$ as a COBDD of dimension $n-|S|$, such that for
every instance $\mathbf{e}$ of dimension $n-|S|$, we have that
$\exists_{S}\mathcal{M}(\mathbf{e})=1$ iff there is an instance
$\mathbf{e}^{\prime}$ of dimension $n$ that holds both:

  * •

$\mathcal{M}(\mathbf{e}^{\prime})=1$

  * •

Let the list $t_{1},\ldots,t_{n-|S|}$ correspond to $\\{1,\ldots,n\\}\setminus
S$ in increasing order. Then $e^{\prime}[t_{i}]=e[i]$, for every
$i\in\\{1,\ldots,n-|S|\\}$.

For example, if $\mathcal{M}$ is a model of dimension $3$ equivalent to
$(x_{1}\land x_{2})\lor(x_{2}\land\neg x_{3})$, then if we take $S=\\{1,3\\}$,
$\exists_{S}\mathcal{M}$ is equivalent to $x_{2}$, as if $x_{2}$ is true, then
there exists values of $x_{1}$ and $x_{3}$ that satisfy $\mathcal{M}$ (namely
$1$ and $0$) respectively, whereas if $x_{2}$ is false, then no values of
$x_{1}$ and $x_{3}$ will help satisfy $\mathcal{M}$.

######  Lemma 3 (Lemma 1, [8]).

Fix an integer $k>0$. Given a COBDD $\mathcal{M}$ of dimension $n$ and width
$k$, and a set $S\subseteq\\{1,\ldots,n\\}$, one can compute a COBDD
$\exists_{S}\mathcal{M}$ of width at most $2^{k}$ in polynomial time.

We can define $\forall_{S}\mathcal{M}$ as $\neg\exists_{S}\neg\mathcal{M}$,
and thus the previous lemma applies as well to $\forall_{S}\mathcal{M}$.

In our case, however, partial instances can have three possible values: $0,1,$
and $\bot$. Therefore, we define _Complete Ordered Ternary Decision Diagrams_
(COTDDs) analogously to COBDDs but with nodes having three outgoing edges
labeled with $0,1,\bot$. Note that, given a COBDD $\mathcal{M}$ of dimension
$n$, we can build in polynomial time a COTDD $\mathcal{M}^{3}$ of dimension
$n$ such that for every partial instance $\mathbf{e}$ of dimension $n$,
$\mathcal{M}^{3}(\mathbf{e})=1$ iff $\mathbf{e}$ is a full instance and
$\mathcal{M}(\mathbf{e})=1$. This can be done by first creating a path $P$ of
nodes according to the underlying order of $\mathcal{M}$, starting from the
second label in the ordering, such that each node is connected to the next one
by its three outgoing edges, and the last one is connected to a leaf labeled
$\mathbf{false}$. Then, start by $M^{3}\coloneqq M$, and to each node labeled
$u$ in $M^{3}$, connect it with its outgoing $\bot$ edge to the node labeled
with the successor of $u$ in $P$.

We now state the equivalent lemmas for COTDDs.

######  Lemma 4.

The following operations can be performed in polynomial time:

  * •

(Negation) Given a COTDD $\mathcal{M}$ of dimension $n$ and width $k$, compute
a COTDD $\neg\mathcal{M}$ of width $k$ and the same ordering of variables,
such that $\neg\mathcal{M}(\mathbf{e})=1-\mathcal{M}(\mathbf{e})$ for every
instance $\mathbf{e}$ of dimension $n$.

  * •

(Disjunction) Given COTDDs $\mathcal{M}_{1}$ and $\mathcal{M}_{2}$ of width at
most $k$, of dimension $n$, with a common linear ordering ${<}$ on the set
$\\{1,\ldots,n\\}$ compute a COTDD
$\mathcal{M}\coloneqq\mathcal{M}_{1}\lor\mathcal{M}_{2}$ over the same linear
ordering ${<}$, and width at most $3k$, such that
$\mathcal{M}(\mathbf{e})=\max(\mathcal{M}_{1}(\mathbf{e}),\mathcal{M}_{2}(\mathbf{e}))$
for every instance $\mathbf{e}$ of dimension $n$.

  * •

(Conjunction) Given COTDDs $\mathcal{M}_{1}$ and $\mathcal{M}_{2}$ of width at
most $k$, of dimension $n$, with a common linear ordering ${<}$ on the set
$\\{1,\ldots,n\\}$ compute a COTDD
$\mathcal{M}\coloneqq\mathcal{M}_{1}\land\mathcal{M}_{2}$ over the same linear
ordering ${<}$, and width at most $3k$, such that
$\mathcal{M}(\mathbf{e})=\min(\mathcal{M}_{1}(\mathbf{e}),\mathcal{M}_{2}(\mathbf{e}))$
for every instance $\mathbf{e}$ of dimension $n$.

###### Proof.

The case of negation is exactly as before. For disjunction and conjunction the
proof works in the same way but by considering that if
$\mathcal{M}_{1}=(r,\mathcal{M}^{0}_{1},\mathcal{M}^{1}_{1},\mathcal{M}^{\bot}_{1})$
and
$\mathcal{M}_{2}=(r,\mathcal{M}^{0}_{2},\mathcal{M}^{1}_{2},\mathcal{M}^{\bot}_{2})$,
then the following equations hold:

$\mathrm{op}(\mathcal{M}_{1},\mathcal{M}_{2})=\left(r,\mathrm{op}(\mathcal{M}_{1}^{0},\mathcal{M}_{2}^{0}),\mathrm{op}(\mathcal{M}_{1}^{1},\mathcal{M}_{2}^{1}),\mathrm{op}(\mathcal{M}_{1}^{\bot},\mathcal{M}_{2}^{\bot})\right)$
(8) $\mathcal{M}_{i}\to j=(\mathcal{M}_{i}^{0}\to j)+(\mathcal{M}_{i}^{1}\to
j)+(\mathcal{M}_{i}^{\bot}\to j)\qquad(i\in\\{1,2\\},\forall j\neq r,1\leq
j\leq\dim(\mathcal{M}))$ (9)

∎

######  Lemma 5 ( Lemma 1, [8]).

Fix an integer $k>0$. Given a COTDD $\mathcal{M}$ of dimension $n$ and width
$k$, and a set $S\subseteq\\{1,\ldots,n\\}$, one can compute a COBDD
$\exists_{S}\mathcal{M}$ of width at most $2^{k}$ in polynomial time.

###### Proof.

Direct from the proof in [8], as the same construction can be done in the
ternary case. ∎

We are finally ready to restate our theorem and prove it.

######  Theorem 3.

Let $k\geq 1$ and query $\varphi$ in FOIL. Then
$\textsc{Eval}(\varphi,k\text{-}\mathsf{COBDD})$ can be solved in polynomial
time.

###### Proof.

We assume that $\varphi$ alternates quantifiers and starts with an existential
one without loss of generality as one can trivially enforce this by adding
_dummy_ variables. Thus, let $\varphi(x_{1},\ldots,x_{\ell})=\exists
x_{\ell+1}\forall x_{\ell+2}\cdots\forall x_{\ell+m-1}\exists
x_{\ell+m}\psi(x_{1},\ldots,x_{\ell+m})$, where $\psi$ is quantifier-free, and
let $\mathcal{M},\mathbf{e}_{1},\ldots,\mathbf{e}_{\ell}$ be an input of the
$\textsc{Eval}(\varphi,k\text{-}\mathsf{COBDD})$ problem. Let
$n=\dim(\mathcal{M})$.

Let us introduce a final piece of notation: from a list of partial instances
$\mathbf{e}_{1},\ldots,\mathbf{e}_{p}$ of dimension $n$ each, we can define a
unique instance $\mathbf{e}_{[1,p]}$ of dimension $pn$ that is simply the
concatenation of instances $\mathbf{e}_{1},\ldots,\mathbf{e}_{p}$. More in
general, we will use notation $[i,j]$ for $i\leq j$ to denote the set
$\\{i,\ldots,j\\}$. We use as well $\mathbf{e}[i:j]$ with $i<j$ referring to
the partial instance $(\mathbf{e}[i],\ldots,\mathbf{e}[j])$ of dimension
$j-i+1$, where $\mathbf{e}$ is a a partial instance of dimension at least $j$.

Now, the proof consists of two parts. First, we will show that based on
$\mathcal{M}$ one can build a COTDD $\mathcal{M}^{\prime}$ of width at most
$f(k)$ for a suitable function $f$, such that

$\mathcal{M}\models\psi(\mathbf{e}_{1},\ldots,\mathbf{e}_{\ell+m})\iff\mathcal{M}^{\prime}(\mathbf{e}_{[1,\ell+m]})=1$

We will do this by induction over $|\psi|$ in the next claim, but first let us
define a linear ordering ${\prec}$ of $[1,n(\ell+m)]$ as follows. If
$\pi(1),\ldots,\pi(n)$ is the ordering of $\mathcal{M}$, then

$\pi(1)\prec\pi(1)+n\prec\pi(1)+2n\prec\ldots\prec\pi(1)+(\ell+m-1)n\prec$

continued by

$\pi(2)\prec\pi(2)+n\prec\pi(2)+2n\prec\ldots\prec\pi(2)+(\ell+m-1)n\prec$

and so on, all the way up to

$\pi(n)\prec\pi(n)+n\prec\pi(n)+2n\prec\ldots\prec\pi(n)+(\ell+m-1)n$

We now formalize the desired claim.

######  Claim 8.

Let $\phi$ be any formula in FOIL mentioning a set of variables
$\\{x_{i},\ldots,x_{j}\\}~{}\subseteq~{}\\{x_{1},\ldots,x_{\ell+m}\\}$, that
has at most $c$ logical connectives (i.e., $\land,\lor,\neg$). Then, we can
build in polynomial time a COTDD $\mathcal{M}_{\phi}$ over the ordering
${\prec}$, of dimension $n(\ell+m)$ and width at most $f(c,k)$ for a suitable
function $f$, such that for any partial instance $\mathbf{e}$ of dimension
$n(\ell+m)$

$\mathcal{M}_{\phi}(\mathbf{e})=1\iff\mathcal{M}\models\phi(\mathbf{e}[i:i+n-1],\ldots,\mathbf{e}[j:j+n-1])$

###### Proof.

The proof is by induction on $c$. The base cases $(c=0)$ are constructive and
relatively involved, so let us start by the inductive cases, where $c>0$.

  * •

If $\phi=\phi_{1}\lor\phi_{2}$, simply use the inductive hypothesis to build
models $\mathcal{M}_{\phi_{1}}$ and $\mathcal{M}_{\phi_{2}}$ and then use
Lemma 4 to build
$\mathcal{M}_{\phi}\coloneqq\mathcal{M}_{\phi_{1}}\lor\mathcal{M}_{\phi_{2}}$
of width is at most
$3\max(0pt(\mathcal{M}_{\phi_{1}},0pt(\mathcal{M}_{\phi_{2}})))$. It is not
hard to see that the resulting model satisfies the desired conditions.

  * •

If $\phi=\phi_{1}\land\phi_{2}$, simply use the inductive hypothesis to build
models $\mathcal{M}_{\phi_{1}}$ and $\mathcal{M}_{\phi_{2}}$ and then use
Lemma 4 to build
$\mathcal{M}_{\phi}\coloneqq\mathcal{M}_{\phi_{1}}\land\mathcal{M}_{\phi_{2}}$
of width is at most
$3\max(0pt(\mathcal{M}_{\phi_{1}},0pt(\mathcal{M}_{\phi_{2}})))$. It is not
hard to see that the resulting model satisfies the desired conditions.

  * •

If $\phi=\neg\phi_{1}$, simply use the inductive hypothesis to build model
$\mathcal{M}_{\phi_{1}}$ and then use Lemma 4 to build
$\mathcal{M}_{\phi}\coloneqq\neg\mathcal{M}_{\phi_{1}}$ of width is at most
$0pt(\mathcal{M}_{\phi_{1}})$. It is not hard to see that the resulting model
satisfies the desired conditions.

For the base cases let us introduce some notation to facilitate our
construction. We will use $P[u,v]$, for $u\prec v$, to mean a path of nodes
labeled from $u$ up to $v$ following the ordering ${\prec}$ and where each
node is connected to the next one by its three outgoing edges. Also, if $a$
and $b$ are nodes, $a\xrightarrow{x}b$ with $x\in\\{0,1,\bot\\}$ means that
$a$’s outgoing edge labeled with $x$ goes to $b$. If $P$ is a path of nodes,
then $P\xrightarrow{x}\alpha$ means that the outgoing edge labeled with $x$ of
the last node in $P$ goes to $\alpha$. Similarly, $\alpha\xrightarrow{x}P$
means means the outgoing edge labeled with $x$ of $\alpha$ (which could be the
last node of a path if $\alpha$ is one) goes to the first node in $P$. We can
now prove that the base cases, when $c=0$, are also satisfied.

  * •

If $\phi=\textsc{Pos}(x_{i})$ for $i\in[1,\ell+m]$, then we build
$\mathcal{M}_{\phi}$ recursively as follows. Assume
$\mathcal{M}=(r,\mathcal{M}^{0},\mathcal{M}^{1})$, and create a path
$P_{r}=P[r,r+(i-1)n]$. Then create three identical paths $P_{r\to 0}=P_{r\to
1}=P_{r\to f}\coloneqq P[r+in,\pi(n)+(\ell+m-1)n]$. Then, add connections
$P_{r}\xrightarrow{\bot}P_{r\to f}\xrightarrow{0,1,\bot}\mathbf{false}$, as
positive instances have no occurrences of $\bot$. Connect
$P_{r}\xrightarrow{0}P_{r\to 0}$ and $P_{r}\xrightarrow{1}P_{r\to 1}$.
Finally, if we let $R(\mathcal{M}^{0}),R(\mathcal{M}^{1})$ be the results of
the recursive procedure applied to $\mathcal{M}^{0}$ and $\mathcal{M}^{1}$,
respectively, then we connect $P_{r\to
0}\xrightarrow{0,1,\bot}R(\mathcal{M}^{0})$ and $P_{r\to
1}\xrightarrow{0,1,\bot}R(\mathcal{M}^{1})$. The recursive procedure applied
to a leaf will just keep it as such. It is easy to see that this can be done
in polynomial time, and it is not hard to see that the desired equation for
$\mathcal{M}_{\phi}$ is satisfied. Moreover, note that for each node $r$ in
$\mathcal{M}$, we introduce three nodes with the same label (namely, when
creating the paths $P_{r\to 0}$, $P_{r\to 1}$ and $P_{r\to f}$, noting that
nodes in $P_{r\to f}$ can be shared for every $q$ such that $r\prec q$) which
implies the width of $\mathcal{M}_{\phi}$ is no more than $3k$.

  * •

If $\phi=x_{i}\subseteq x_{j}$, we build $\mathcal{M}_{\phi}$ as follows. We
first build a path $P_{f}=[1,\pi(n)+(\ell+m-1)n]\to\mathbf{false}$. For each
$1\leq t\leq n$ we will build a gadget that checks that
$\mathbf{e}_{i}[t]=\bot\lor\mathbf{e}_{i}[t]=\mathbf{e}_{i}[t]$. The gadget
for $\pi(1)$ will be connected to that of $\pi(2)$ and so on, so the ordering
${\prec}$ is respected. The exact form of each gadget depends on whether $i<j$
or the opposite, as in the first case $t+(i-1)n\prec t+(j-1)n$, for each
$1\leq t\leq n$, and vice-versa if $j<i$. Consider first the case where $i<j$.
Then, for the gadget for $t\in\\{1,\ldots,n\\}$ we build a path
$P^{1}\coloneqq P[\pi(t),\pi(t)+(i-1)n]$, two identical paths
$P^{2}=P^{3}\coloneqq P[\pi(t)+in,\pi(t)+(j-1)n]$. and $P^{4}\coloneqq
P[\pi(t)+jn,\pi(t)+(\ell+m-1)n]$. We then connect
$P^{1}\xrightarrow{0}P^{2}\xrightarrow{0}P^{4}$ and
$P^{1}\xrightarrow{1}P^{3}\xrightarrow{1}P^{4}$, Also, for a label $u$, let us
denote $s(u)$ to its successor according to $\prec$, and let $f(s(u))$ be the
node in $P_{f}$ with label $s(u)$. Next, connect
$P^{1}\xrightarrow{1}P^{3}\xrightarrow{0}f(s(\pi(t)+(j-1)n))$ and
$P^{1}\xrightarrow{0}P^{3}\xrightarrow{1}f(s(\pi(t)+(j-1)n))$. If $t=n$, we
connect $P^{4}\xrightarrow{0,1,\bot}\mathbf{true}$ and otherwise, if $t<n$ and
$G_{t+1}$ is the gadget for $t+1$, we connect
$P^{4}\xrightarrow{0,1,\bot}G_{t+1}$. The case when $j<i$ is similar, but
every gadget for $1\leq t\leq n$ checks first the value of the $t$-th feature
in the $j$-th variable, and then checks that the $t$-th variable is either
$\bot$ or matches the previously mentioned value. We omit the details as they
are a trivial modification of the previous construction.

It is clear that this procedure takes polynomial time, and it is not hard to
see that this procedure satisfies the desired condition. Moreover the
resulting COTDD has width $3$, as $P^{2}$ and $P^{3}$ make for two occurrences
of the labels appearing in them, and a final one comes from $P_{f}$.

As each recursive step reduces $c$ by one, and can at most increase the width
by a factor of $3$, it follows that the width of the resulting model is at
most $k3^{c}$, and thus $f(c,k)=k3^{c}$ is a suitable function. This concludes
the proof of the claim. ∎

Now, for the second part of the proof, assume we have already built
$\mathcal{M}^{\prime}$ by using the previous claim noting that as $\psi$ is a
fixed formula, $c$ is a fixed constant which implies that the function $f$ of
the previous claim depends thus solely on $k$. Let us now state a simpler
claim.

######  Claim 9.

For appropriate sets $S_{1},\ldots,S_{m}$ subsets of $[1,n(\ell+m)]$, that can
be determined in polynomial time, the following holds:

$\mathcal{M}\models\varphi(\mathbf{e}_{1},\ldots,\mathbf{e}_{\ell})\iff\exists_{S_{1}}\forall_{S_{2}}\cdots\forall_{S_{m-1}}\exists_{S_{m}}\mathcal{M}^{\prime}(\mathbf{e}_{[1,\ell]})=1$

###### Proof.

Trivial by the definition of $\exists_{S}$ and $\forall_{S}$ when defining
each $S_{i}$ as $[n(\ell+i-1)+1,n(\ell+i)]$. ∎

In order to finish the proof, we use the previous claim and simply compute
$\mathcal{M}^{\star}\coloneqq\exists_{S_{1}}\forall_{S_{2}}\cdots\forall_{S_{m-1}}\exists_{S_{m}}\mathcal{M}^{\prime}$
by $m$ repeated applications of Lemma 5, and computing two negations for each
$\forall_{S_{i}}$ according to Lemma 4. This results in $\mathcal{M}^{\star}$
having width at most $f(k)=2^{2^{2^{\cdots^{2^{3^{|\varphi|k}}}}}}$, where the
tower has $m$ times the number $2$. Then we build the partial instance
$\mathbf{e}_{[1,\ell]}$ and finally evaluate
$\mathcal{M}^{\star}(\mathbf{e}_{[1,\ell]})$, which thanks to the previous
claim is enough to solve the whole problem. As every part of the algorithm is
proven to be correct, and the running time of each component is polynomial, we
conclude the whole proof.

∎

##  Appendix G Details of the FOIL implementation and the experimental setting

All our code and instructions to run experiments can be found at the following
URL

https://github.com/AngrySeal/FOIL-Prototype

For the implementation of the algorithms we used C++ to assure efficiency. For
parsing queries we used the ANTLR (v4.9.1) parser generator. Queries can be
specified in a straightforward way in plain text by using tokens Exists and
ForAll for quantification, tokens `~`, ^, V, for logical connectives $\neg$,
$\wedge$ and $\vee$. respectively, and tokens of the form x1, x2, x3, u, v, z,
etc. for variables, plus parentheses for stating precedence. Instances
mentioned in the queries are written as (0,1,?,0) where ? represents the
$\bot$ value (for defining partial instances). Besides that, we used P( ) for
the unary operator $\textsc{Pos}(\cdot)$ and <= for the containment
$\subseteq$. The following is an example query.

    Exists x, Exists y, (P(x) V P(y)) ^ (~( x <= y ) ^ ~(y <= (?,?,?,0,1,?,?)))

For debugging purposes we implemented a naive evaluation method (126 lines of
code) that considers models as black boxes for evaluating Pos, and that
evaluates a query by testing all possible combinations for the mentioned
variables. For the obvious reasons, this implementation is not practical but
it is straightforward to prove its correctness. Thus we use it to check the
correctness of the evaluation process of the more efficient algorithms.

We implemented versions for the query evaluator for perceptrons (not described
in the paper), decision trees and a modification of FBDDs (see Section J for
details). For these last two cases, the implementation had 660 lines of code.
Trees and BDDs are passed to the implementation in a straightforward JSON
format. We checked the correctness by generating a set of random queries over
random models and comparing the output of each algorithm against our naive
implementation.

##  Appendix H Details of the experimental setting

We used Python for the query and models generation process. We generated
random queries with the following recursive process. We initially fix the
dimension of the queried model, the number of quantified variables allowed to
be used in the complete query, and whether they are going to be universally or
existentially quantified. We then construct the quantified-free part as
follows. When asking for an expression of size $n$, the query generator method
chooses a random size $k$ from $1$ to $n-1$, then generates two expressions of
size $k$ and $n-k$ and joined them choosing either ^ or V randomly. The base
case is when asking for an expression of size $1$ in which case we choose
randomly between P($x$), $C$ <= $x$, $x$ <= $C$ and $x$ <= $y$, where $C$
represents a random partial instance constructed according to the dimension of
the queried model as a tuple using values 0, 1 and ?, and $x$ and $y$
represents randomly chosen variables from all of the variables allowed to be
used in the query. Every random choice was done with numpy’s default_rng.
Before returning from every recursive call, the method choose randomly whether
a negation (`~`) is added in fron of the expression.

For generating the decision-tree models to be queried, we used the Scikit-
learn library. We first select an input dimension, and then we generated a
random dataset of that dimension. All input data that we generate are random
binary tuples and the target value (classification) is a random bit. Then we
select the size $N$ for the tree and trained a decision-tree model with $N$
leaves. Finally, we transformed the obtained decision-tree into a binary one
in the JSON format that our implementation can consume.

For the experiments shown in Figure 2(a) and 2(b) and using the methods
described above, we generanted $60$ random queries and trained $24$ random
decision trees of different sizes (see Section 6.1). The performance tests
were done in a small personal computer: 64-bits, 2.48GHz, Dual Core Intel
Celeron N3060 with 2GB of RAM and Linux Mint 20.1 Ulyssa. Even in this modest
machine, the evaluation time for random queries and models was extremely short
(see Section 6.1). This gives evidence that our methods can be run even for
trees and queries of considerable size in a personal machine without the need
of a big computer infrastructure.

##  Appendix I A high-level language for FOIL

As we described in the body of the paper, we designed a high-level user-
friendly syntax tailored for general models with numerical and categorical
features. As FOIL does not allow the use of features beyond binary ones, we
need to develop a way for binarizing queries and models. We describe the
binarization in the next section, and we only describe here the main features
of our user-friendly language.

Figure 3 shows examples of queries written for the Student Performance Data
Set [29]222Download dataset at:
https://archive.ics.uci.edu/ml/datasets/Student+Performance. In the high-level
syntax we use the expressions exists and for every that represents the logical
quantification, and tokens and, or, not and implies for typical logical
connectives. Variables can be any string that is not a reserved keyword. In
the examples in Figure 3 we use student, st1 and st2 as variables.

Our implementation allows for loading a trained model before evaluating
queries (see details on model loading below). Whenever a model is loaded the
meta information about features and types as well as the classification is
also loaded to be interpreted in the queries. A main difference with basic
FOIL is that in our high-level syntax we allow for the use of named features.
For example in the first query in Figure 3 we use student.male to refer to the
binary feature male of a student instance. Moreover we can refer to different
classes (the output of the model) with names. For our example, we trained a
binary classifier in which the positive class name is goodFinalGrades. Thus,
the expression goodFinalGrades(student) is equivalent to the P( ) expression
in the basic FOIL implementation. With all this we can intuitively interpret
the first query in Figure 3 as asking if having a male gender is enough for
the model to make a decision about the final grades.

Besides naming features, our syntax also allows the comparison of with
numerical thresholds. In this case we use the typical <= and > with their
natural meaning. For instance, in our example using the Student Performance
Data Set, the feature alcoholWeek states the level of alcohol consumption
during week days, with value $1$ begin low, and value $5$ being high. Thus,
the second query in Figure 3 asks if it is possible that the trained model
classify a student with a high alcohol consumption during week days
(student.alcoholWeek > 3) as having good final grades. The comparison with
numerical thresholds departs significantly from the base FOIL formalization,
and thus it is not trivial how to compile this type of queries into FOIL. We
describe the process in the next section.

Finally, in order to have meaningful answers for existential queries of the
form $\exists x(\neg\textsc{Pos}(x))$, that is, asking for the existence of
instances that are classified as negative for the model, we implemented the
operator full( ) that essentially requires an instance to be not partial, that
is, not using $\bot$ (the formal definition of this property is in Equation
1). The reason for this is that only total instances can be positive in models
and since queries are evaluated over the set of all partial instances, the
query $\exists x(\neg\textsc{Pos}(x))$ is trivially true. Having full( ) as
part of the language allows us to more easily deal with this case. For
example, the third query in Figure 3 uses full( ) to ask if there is a student
with low alcohol consumption during the week and that is classified as not
getting good grades.

All our queries have as possible answer either YES or NO. It is not difficult
to extend our implementation such that, whenever the answer for an existential
query is a YES then we can provide an instance as witness for that answer. One
can similarly provide a witness when the answer for a universal query is a NO.
This is part of our ongoing work.

Finally, we handcrafted over 20 queries similar to the ones in Figure 3 and
tested them over a decision tree with no more than 400 leaves. You can find
the complete set of queries that we tested in our companion code.

    for every student,
        student.male = true
        implies goodFinalGrade(student)

    exists student,
        student.alcoholWeek > 3
        and goodFinalGrade(student)

    exists student,
        student.alcoholWeek < 2
        and full(student) and not goodFinalGrade(student)

    for every student,
        student.alcoholWeekend > 3 and student.alcoholWeek > 3
        implies not goodFinalGrade(student)

    exists student,
        (student.alcoholWeekend > 3 or student.alcoholWeek > 3)
        and student.gradePartial2 <= 6 and student.male = false
        and goodFinalGrade(student)

    exists st1, exists st2,
        st1.studyTime > 2 and st2.studyTime <= 3
        and goodFinalGrade(st1) and
        full(st2) and not goodFinalGrade(st2)

Figure 3: Example queries in high-level syntax

##  Appendix J Binarization of queries and models

The definition of FOIL considers only binary instances (i.e., tuples in
$\\{0,1\\}^{n}$ for some $n\geq 1$), and consequently, binary classifiers
$\mathcal{M}:\\{0,1\\}^{n}\to\\{0,1\\}$ for some $n\geq 1$. As many real life
classification problems involve a combination of categorical and numerical
features, this could present a limitation to our approach. However, in this
section we show that it is possible to overcome this apparent drawback by
binarizing queries and models. A recent article by Choi et al. [12], studies
binary encodings for decision trees as well. Our approach is slightly
different, as we are concerned as well with the issue of binarizing queries.

Let us define HL-FOIL as a _high-level_ equivalent of FOIL. First, we define a
_schema_ for HL-FOIL as a mapping from _feature names_ to _feature types_ ,
which can be either $\mathbb{R}$ or $\mathbb{B}=\\{0,1\\}$, intuitively
meaning that said feature is numerical or Boolean, respectively. We use
notation $S(f)$ to obtain the type of a feature by its name. Moreover, if a
schema $S$ defines the type of a feature $f$, we say $f\in S$.

For example, consider the following possible schema for the Student
Performance Data Set:

$S=\\{(\text{age},\mathbb{R}),(\text{alcoholWeek},\mathbb{R}),(\text{parentsTogether},\mathbb{B}),\ldots\\}.$

We say a real-valued decision tree $\mathcal{T}$ is compatible with a schema
$S$ if each internal node $u\in\mathcal{T}$ holds one of the following
conditions:

  * •

(Numerical) Node $u$ has label $(f,\tau)$ for some $f\in S,\tau\in\mathbb{R}$,
and $S(f)=\mathbb{R}$.

  * •

(Boolean) Node $u$ has label $f$ with $f\in S$, and $S(f)=\mathbb{B}$.

Given a schema $S$, the following are atomic $\text{\rm HL-FOIL}_{S}$
formulas:

  * •

$\textsc{Pos}(x)$, where $x$ is a variable.

  * •

$\textsc{Full}(x)$, where $x$ is a variable.

  * •

$(\leq,x,f,\tau)$, where $x$ is a variable, $S(f)=\mathbb{R}$, and
$\tau\in\mathbb{R}$.

  * •

$(=,x,f,b)$, where $x$ is a variable, $S(f)=\mathbb{B}$, and $b\in\mathbb{B}$.

Naturally, the domain of $\text{\rm HL-FOIL}_{S}$ consists of functions from
feature names $f\in S$ to values in $S(f)\cup\\{\bot\\}$, which we call
instances of $\text{\rm HL-FOIL}_{S}$. Continuing with our running example,
the function $\mathbf{e}$ such that
$\mathbf{e}(\text{age})=19.4,\mathbf{e}(\text{parentsTogether})=0,\ldots.$ is
an instance of $\text{\rm HL-FOIL}_{S}$. The semantics for the atomic formulas
$\textsc{Full}(x)$, $(\leq,x,f,\tau)$, and $(=,x,f,b)$ is naturally defined as
one would expect, by checking whether $\mathbf{e}_{x}(f)\leq\tau$, and
$\mathbf{e}_{x}(f)=b$, respectively. In order to clarify the semantics of Pos,
we detail how instances of $\text{\rm HL-FOIL}_{S}$ are evaluated by a
decision tree.

For a decision tree $\mathcal{T}$ compatible with $S$ and an instance
$\mathbf{e}$ of $\text{\rm HL-FOIL}_{S}$, we define $\mathcal{T}(\mathbf{e})$
inductively:

  * •

If $\mathcal{T}$ is a leaf labeled with $\mathbf{true}$, then
$\mathcal{T}(\mathbf{e})=1$, and $\mathcal{T}(\mathbf{e})=0$ if the label is
$\mathbf{false}$.

  * •

If $\mathcal{T}$ has a root labeled with $(f,\tau)$, left sub-tree
$\mathcal{T}_{0}$, and right sub-tree $\mathcal{T}_{1}$, then
$\mathcal{T}(\mathbf{e})$ is defined as follows. If $\mathbf{e}(f)\leq\tau$,
then $\mathcal{T}(\mathbf{e})=\mathcal{T}_{1}(\mathbf{e})$, and otherwise
$\mathcal{T}(\mathbf{e})=\mathcal{T}_{0}(\mathbf{e})$.

  * •

If $\mathcal{T}$ has a root labeled with $f$, left sub-tree $\mathcal{T}_{0}$,
and right sub-tree $\mathcal{T}_{1}$, then $\mathcal{T}(\mathbf{e})$ is
defined as $\mathcal{T}_{f(\mathbf{e})}(\mathbf{e})$.

It is important to stress that Boolean decision trees, in order to prevent
inconsistencies, cannot repeat node labels in any path from the root a leaf.
For real-valued decision trees we need a stronger requirement to avoid
inconsistencies: if $\mathcal{T}$ has a root labeled with $(f,\tau)$, left
sub-tree $\mathcal{T}_{0}$, and right sub-tree $\mathcal{T}_{1}$, then all
nodes labeled with $(f,\tau_{0})$ in $\mathcal{T}_{0}$ must hold
$\tau_{0}>\tau$, and similarly all nodes labeled with $(f,\tau_{1})$ in
$\mathcal{T}_{1}$ must hold $\tau_{1}<\tau$.

We are now ready to define a binarization procedure.

######  Definition 1.

A binarization procedure $\mathcal{B}$ is an algorithm that takes: (i) a
schema $S$; (ii) an existential formula $\varphi$ in $\text{\rm HL-FOIL}_{S}$
; (iii) a decision tree $\mathcal{T}$ compatible with $S$, and returns a
formula $\psi\in(\exists\text{\rm FOIL}\cup\textsc{Full})$ together with a
binary model $\mathcal{M}$, such that

$\mathcal{T}\models\varphi\iff\mathcal{M}\models\psi.$

The rest of this section is dedicated to show an efficient binarization
procedure $\mathcal{B}$. First, let us show the intuition behind the procedure
with a simple example. Figure 4 depicts a real-valued decision tree
$\mathcal{T}$ over the schema $S$ of our running example. Note that, although
an instance $\mathbf{e}$ can have any real value as $\mathbf{e}(\text{age})$,
$\mathcal{T}$ only distinguishes 4 intervals:

$(-\infty,16],\;(16,21],\;(21,25],\;(25,\infty)$

$\text{age}\leq 21$$\text{age}\leq 25$$\text{age}\leq
16$$\mathbf{true}$$\mathbf{false}$$\mathbf{true}$$\mathbf{false}$$0$$1$$1$$0$$0$$1$
Figure 4: Example of real-valued decision tree. For the sake of clarity,
labels are written as $f\leq\tau$ instead of $(f,\tau)$.

Now consider the $\text{\rm HL-FOIL}_{S}$ query:

$\varphi=\exists x\,\textsc{Pos}(x)\land(\leq,x,\text{age},27)$

Consider now instances $\mathbf{e}_{1},\mathbf{e}_{2}$ such that
$\mathbf{e}_{1}(\text{age})=26$ and $\mathbf{e}_{2}(\text{age})=28$. While
$\mathcal{T}$ accepts both $\mathbf{e}_{1}$ and $\mathbf{e}_{2}$ by traversing
the same path, only $\mathbf{e}_{1}$ is a witness for $\varphi$. This implies
that we require a finer partition of the real line into intervals. Namely,

$\mathcal{I}_{\text{age}}=(-\infty,16],\;(16,21],\;(21,25],\;(25,27],\;(27,\infty)$

is a _correct partition_ for the tuple $(\mathcal{T},\varphi,\text{age})$.
Based on this, as $|\mathcal{I}_{\text{age}}|=5$, we will use $5-1=4$ binary
features to encode the age of instances. In particular, the leftmost $1$ among
those $4$ binary features will indicate the interval to which the age of an
instance belongs, interpreting that if there is no $1$ among the $4$ binary
features, it belongs to the last interval. This will then allow to do the
following compilation from $\text{\rm HL-FOIL}_{S}$ to FOIL:

$(\leq,x,\text{age},27)\rightsquigarrow\neg\left(x\subseteq\begin{pmatrix}0,\,0,\,0,\,0,\,\bot,\,\bot,\,\ldots\end{pmatrix}\right)$

As a FOIL instance $\mathbf{e}$ not having $0$ in the first four Boolean
features that encode age must have at least a $1$ in one of those Boolean
features, and thus, it corresponds to a $\text{\rm HL-FOIL}_{S}$ instance
whose age lies in one of the first four intervals of
$\mathcal{I}_{\text{age}}$, and therefore have $\text{age}\leq 27$.

More formally, assume a real-valued decision tree $\mathcal{T}$ and a
$\text{\rm HL-FOIL}_{S}$ query $\varphi$. Then, for every feature name $f\in
S$ such that $S(f)=\mathbb{R}$, we define its _partition set_ as follows:

$P_{f}=\\{\tau\mid(f,\tau)\text{ labels a node in }\mathcal{T},\text{ or
}(\leq,x,f,\tau)\text{ appears in }\varphi\text{ for some variable }x\\}$

Feature $f$ will be encoded using $|P_{f}|$ Boolean features. The resulting
dimension of instances of $\text{\rm HL-FOIL}_{S}$ compiled into FOIL
instances will therefore be $n=\sum_{f\in S}|P_{f}|$, taking the convention
that if $S(f)=\mathbb{B}$ then $|P_{f}|=1$.

As $S$ is unordered, but instances of FOIL have an ordering of their features,
we choose an arbitrary ordering of features names $f_{1},\ldots,f_{k}$, and we
associate to them ranges of Boolean features as follows. To $f_{1}$ we
associate the components in the range $[1,|P_{f_{1}}|]$, and then for
$f_{i},i>1$, we associate $[\ell,\ell+|P_{f_{i}}|-1]$, where $\ell$ is end of
the range associated to $f_{i-1}$ plus $1$.

Therefore comparison of the form $(\leq,x,f,\tau)$, for some variable $x$,
will thus be compiled as:

$(\leq,x,f,\tau)\rightsquigarrow\neg\left(x\subseteq\mathbf{e}_{\tau}\right)$

where, if $\tau$ is the $i$-th smallest element in $P_{f}$, then
$\mathbf{e}_{\tau}$ is an instance having $0$ in the first $i$ Boolean
features associated to $f$, and $\bot$ in the rest.

We now need to binarize the decision tree $\mathcal{T}$ accordingly. We do so
by transforming $\mathcal{T}$ into a BDD $\mathcal{B}(\mathcal{T},\varphi)$
(not necessarily free) that is _almost_ -free, in a precise sense that we will
detail. If $\mathcal{T}$ was using a single node $u$ to test whether the age
of an instance was at most $27$, we now require several nodes to test for the
different Boolean features encoding the age of said instance. In particular,
if age is encoded with Boolean features of indices $[i,\ldots,j]$, and $27$ is
the $k$-th smallest value in $P_{\text{age}}$, then
$\mathcal{B}(\mathcal{T},\varphi)$ needs to test that there is a $1$ in among
the features of indices $[i,\ldots,i+k-1]$. Thus, we create in
$\mathcal{B}(\mathcal{T})$ a _gadget_ for node $u$ of $\mathcal{T}$ that tests
whether

$\mathbf{e}[i]\lor\mathbf{e}[i+1]\lor\cdots\lor\mathbf{e}[i+k-1].$

Correctness is clear from the construction of the binarization procedure.
Figure 5 illustrates $\mathcal{B}(\mathcal{T},\varphi)$ continuing with the
previous example.

$1$$2$$3$$3$$4$$\mathbf{true}$$\mathbf{false}$$1$$1$$1$$1$$1$$0$$0$$0$$0$$0$
Figure 5: Illustration of $\mathcal{B}(\mathcal{T},\varphi)$, assuming age is
the only feature, and considering a query $\varphi=\exists x\textsc{Pos}(x)$
that does not mention any threshold $\tau$.

While $\mathcal{B}(\mathcal{T},\varphi)$ is not necessarily an FBDD, we claim
that it is close enough to one in what concerns the evaluation of
$\exists\text{\rm FOIL}$ formulas. As the proof of Proposition 1 implies, the
only characteristic of models we require for efficient evaluation in the
existential fragment is that one can find in polynomial time a determinization
of an undetermined instance that is positive for said models. This is clearly
not possible for general BDDs, as even checking if there is one positive
instance for a BDD is NP-hard [38]. Surprisingly, the same algorithm for FBDDs
presented in the proof of Proposition 1 turns out to work for
$\mathcal{B}(\mathcal{T},\varphi)$.

In order to see illustrate why this is true, we consider a more sophisticated
example of a real-valued decision tree $\mathcal{T}$, presented in Figure 6.
Note that both the gadgets for nodes labeled $(\text{age},21)$ and
$(\text{age},25)$ will use the Boolean features associated to age, and thus
the _freeness_ property will be broken. The reason the presented algorithm
does not work in general BDDs is that a positive leaf could only be reachable
through inconsistent paths, i.e., paths that contain both edges representing
that a feature has value $0$ and $1$. In the case of
$\mathcal{B}(\mathcal{T},\varphi)$, features may appear multiple times in a
path from root to leaf, but always as part of different gadgets associated to
different nodes in $\mathcal{T}$. This implies that, even if an inconsistent
choice is made for a particular Boolean feature of
$\mathcal{B}(\mathcal{T},\varphi)$, an inconsistent path in
$\mathcal{B}(\mathcal{T},\varphi)$ still corresponds as a consistent path in
$\mathcal{T}$, because paths in $\mathcal{B}(\mathcal{T},\varphi)$ translate
back to paths in $\mathcal{T}$ by considering if gadgets where exited by
failing or succeeding the disjunction they represent.

$\text{age}\leq 21$male$\text{age}\leq 25$$\text{age}\leq
16$$\mathbf{true}$$\mathbf{false}$$\mathbf{true}$$\mathbf{false}$$\mathbf{false}$$0$$1$$1$$0$$0$$1$$0$$1$
Figure 6: Example of real-valued decision tree. For the sake of clarity,
labels are written as $f\leq\tau$ instead of $(f,\tau)$.