# Foundations of Symbolic Languages
for Model Interpretability

Marcelo Arenas1,4, Daniel Baez3, Pablo Barceló2,4, Jorge Pérez3,4, Bernardo
Subercaseaux4,5
1 Department of Computer Science, PUC-Chile
2 Institute for Mathematical and Computational Engineering, PUC-Chile
3 Department of Computer Science, Universidad de Chile
4 Millennium Institute for Foundational Research on Data, Chile
5 Carnegie Mellon University, USA
[marenas<EMAIL_ADDRESS><EMAIL_ADDRESS><EMAIL_ADDRESS>
###### Abstract

Several queries and scores have been proposed to explain individual
predictions made by ML models. Examples include queries based on “anchors”,
which are parts of an instance that are sufficient to justify its
classification, and “feature-perturbation” scores such as SHAP. Given the need
for flexible, reliable, and easy-to-apply interpretability methods for ML
models, we foresee the need for developing declarative languages to naturally
specify different explainability queries. We do this in a principled way by
rooting such a language in a logic called FOIL, that allows for expressing
many simple but important explainability queries, and might serve as a core
for more expressive interpretability languages. We study the computational
complexity of FOIL queries over classes of ML models often deemed to be easily
interpretable: decision trees and more general decision diagrams. Since the
number of possible inputs for an ML model is exponential in its dimension,
tractability of the FOIL evaluation problem is delicate, but can be achieved
by either restricting the structure of the models, or the fragment of FOIL
being evaluated. We also present a prototype implementation of FOIL wrapped in
a high-level declarative language, and perform experiments showing that such a
language can be used in practice.

##  1 Introduction

inline]hola

Context. The degree of interpretability of a machine learning (ML) model seems
to be intimately related with the ability to “answer questions” about it.
Those questions can either be global (behavior of the model as a whole) or
local (behavior regarding certain instances/features). Concrete examples of
such questions can be found in the recent literature, including, e.g., queries
based on “anchors”, which are parts of an instance that are sufficient to
justify its classification [32, 13, 16, 4], and numerical scores that measure
the impact of the different features of an instance on its result [36, 31,
24].

It is by now clear that ML interpretability admits no silver-bullet [18], and
that in many cases a combination of different queries may be the most
effective way to understand a model’s behavior. Also, model interpretability
takes different flavors depending on the application domain one deals with.
This naturally brings to the picture the need for general-purpose
specification languages that can provide flexibility and expressiveness to
practitioners specifying interpretability queries. An even more advanced
requirement for these languages is to be relatively easy to use in practice.
This tackles the growing need for bringing interpretability methods closer to
users with different levels of expertise.

One way in which these requirements can be approached in a principled way is
by developing a declarative interpretability language, i.e., one in which
users directly express the queries they want to apply in the interpretability
process (and not how these queries will be evaluated). This is of course
reminiscent of the path many other areas in computer science have followed, in
particular by using languages rooted in formal logic; so has been the case,
e.g., in data management [1], knowledge representation [3], and model checking
[15]. One of the advantages of this approach is that logics have a well-
defined syntax and clear semantics. On the one hand, this ensures that the
obtained explanations are provably sound and faithful to the model, which
avoids a significant drawback of several techniques for explaining models in
which the explanations can be inaccurate, or require themselves to be further
explained [33]. On the other hand, a logical root facilitates the theoretical
study of the computational cost of evaluation and optimization for the queries
in the language.

Our proposal. Our first contribution is the proposal of a logical language,
called FOIL, in which many simple yet relevant interpretability queries can be
expressed. We believe that FOIL can further serve as a basis over which more
expressive interpretability languages can be built, and we propose concrete
directions of research towards its expansion. In a nutshell, given a decision
model $\mathcal{M}$ that performs classification over instances $\mathbf{e}$
of dimension $n$, FOIL can express properties over the set of all partial and
full instances of dimension $n$. A partial instance $\mathbf{e}$ is a vector
of dimension $n$ in which some features are undefined. Such undefined features
take a distinguished value $\bot$. An instance is full if none of its features
is undefined. The logic FOIL is simply first-order logic with access to two
predicates on the set of all instances (partial or full) of dimension $n$: A
unary predicate $\textsc{Pos}(\mathbf{e})$, stating that $\mathbf{e}$ is a
full instance that $\mathcal{M}$ classifies as positive, and a binary
predicate $\mathbf{e}\subseteq\mathbf{e}^{\prime}$, stating that instance
$\mathbf{e}^{\prime}$ potentially fills some of the undefined features of
instance $\mathbf{e}$; e.g., $(1,\,0,\,\bot)\subseteq(1,\,0,\,1)$, but
$(1,\,0,\,\bot)\not\subseteq(1,\,1,\,1)$.

As an overview of our proposal, consider the case of a bank using a binary
model to judge applications for loans. Figure 1(a) illustrates the problem
with concrete features, and Figure 1(b) presents an example of a concrete
interactive syntax. In Figure 1(b), after loading and exploring the model, the
interaction asks whether the model could give a loan to a person who is
married and does not have kids. Assuming that the “Accepted” class is the
positive one, this interaction can easily be formalized in FOIL by means of
the query $\exists
x\,\big{(}\textsc{Pos}(x)\land(\bot,\bot,\bot,\bot,0,1,\bot)\subseteq
x\big{)}.$

$\begin{matrix}\text{Stable job}\\\ >\text{ 40yo}\\\ \text{Previous loans}\\\
\text{Owns a house}\\\ \text{Has kids}\\\ \text{Married}\\\ \text{Criminal
Record}\end{matrix}$$\begin{pmatrix}0\\\ 1\\\ 1\\\ 0\\\ 0\\\ 1\\\
1\end{pmatrix}$ Black Box Model Application Rejected

(a) Diagram of a particular loan decision.

⬇

> load("mlp.np") as MyModel;

> show features;

(stableJob, >40yo, prevLoan, ownsHouse,

hasKids, isMarried, crimRecord): Boolean

> show classes;

Rejected (0), Accepted (1)

\par> exists person,

person.isMarried

and not person.hasKids

and MyModel(person) = Accepted;

YES

(b) Example of a possible concrete syntax for a language tailored for
interpretability queries.

Figure 1: Example of a bank that uses a model to decide whether to accept loan
applications considering binary features like “does the requester have a
stable job” and “are they older than 40”?

Theoretical contributions. The evaluation problem for a fixed FOIL query
$\varphi$ is as follows. Given a decision model $\mathcal{M}$, is it true that
$\varphi$ is satisfied under the interpretation of predicates $\subseteq$ and
Pos defined above? An important caveat about this problem is that, in order to
evaluate $\varphi$, we need to potentially look for an exponential number of
instances, even if the features are Boolean, thus rendering the complexity of
the problem infeasible in some cases. Think, for instance, of the query
$\exists x\,\textsc{Pos}(x)$, which asks if $\mathcal{M}$ has at least one
positive instance. Then this query is intractable for every class of models
for which this problem is intractable; e.g., for the class of propositional
formulas in CNF (notice that this is nothing but the satisfiability problem
for the class at hand).

The main theoretical contribution of our paper is an in-depth study of the
computational cost of FOIL on two classes of Boolean models that are often
deemed to be “easy to interpret”: decision trees and ordered binary decision
diagrams (OBDDs) [10, 33, 19, 28, 14]. An immediate advantage of these models
over, say, CNF formulas, is that the satisfiability problem for them can be
solved in polynomial time; i.e., the problem of evaluating the query $\exists
x\textsc{Pos}(x)$ is tractable. Our study aims to (a) “measure” the degree of
interpretability of said models in terms of the formal yardstick defined by
the language FOIL; and (b) shed light on when and how some simple
interpretability queries can be evaluated efficiently on these decision
models.

We start by showing that, in spite of the aforementioned claims on the good
level of interpretability for the models considered, there is a simple query
in FOIL that is intractable over them. In fact, such an intractable query has
a natural “interpretability” flavor, and thus we believe this proof to be of
independent interest.

However, these intractability results should not immediately rule out the use
of FOIL in practice. In fact, it is well known that a logic can be intractable
in general, but become tractable in practically relevant cases. Such cases can
be obtained by either restricting the syntactic fragment of the logic
considered, or the structure of the models in which the logic is evaluated. We
obtain positive results in both directions for the models we mentioned above.
We explain them next.

Syntactic fragments. We show that queries in $\exists\text{\rm FOIL}$, the
existential fragment of FOIL, admit tractable evaluation over the models we
study. However, this language lacks expressive power for capturing some
interpretability queries of practical interest. We then introduce
$\exists\text{\rm FOIL}^{+}$, an extension of $\exists\text{\rm FOIL}$ with a
finite set of unary universal queries from FOIL that is enough for expressing
some relevant interpretability queries. We provide a characterization theorem
for the tractability of $\exists\text{\rm FOIL}^{+}$ over any class of Boolean
decision models that reduces the tractability of this fragment to the
tractability of two fixed and specific FOIL queries. Then we prove that said
queries are tractable over perceptrons, which implies the tractability of
$\exists\text{\rm FOIL}^{+}$ for this model. Unfortunately, the evaluation of
said queries is NP-hard for decision trees and OBDDs. Both the proof of
tractability for perceptrons and intractability for decision trees and OBDDs
are relatively simple, thus showing that the characterization theorem provides
a useful technique for understanding which models are tractable for the
evaluation of $\exists\text{\rm FOIL}^{+}$.

Structural restrictions. We restrict the models allowed in order to obtain
tractability of evaluation for arbitrary FOIL queries. In particular, we show
that evaluation of $\varphi$, for $\varphi$ a fixed FOIL query, can be solved
in polynomial time over the class of OBDDs as long as they are complete, i.e.,
any path from the root to a leaf of the OBDD tests every feature from the
input, and have bounded width, i.e., there is a constant bound on the number
of nodes of the OBDD in which a feature can appear.

Practical implementation. We designed FOIL with a minimal set of logical
constructs and tailored for models with binary input features. These decisions
are reasonable for a detailed theoretical analysis but may hamper FOIL usage
in more general scenarios, in particular when models have (many) categorical
or numerical input features, and queries are manually written by non-expert
users. To tackle this we introduce a more user-friendly language with a high-
level syntax (_à la_ SQL in the spirit of the query in Figure 1(b)) that can
be compiled into FOIL queries. Moreover, we present a prototype implementation
that can be used to query decision trees trained in standard ML libraries by
binarizing them into models (a subclass of binary decision diagrams) over
which FOIL queries can be efficiently evaluated. We also test the performance
of our implementation over synthetic and real data giving evidence of the
usability of FOIL as a base for practical interpretabilty languages.

##  2 A Logic for Interpretability Queries

Background. An instance of dimension $n$, with $n\geq 1$, is a tuple
$\mathbf{e}\in\\{0,1\\}^{n}$. We use notation $\mathbf{e}[i]$ to refer to the
$i$-th component of this tuple, or equivalently, its $i$-th feature. Moreover,
we consider an abstract notion of a model of dimension $n$, and we define it
as a Boolean function $\mathcal{M}:\\{0,1\\}^{n}\to\\{0,1\\}$. That is,
$\mathcal{M}$ assigns a Boolean value to each instance of dimension $n$, so
that we focus on binary classifiers with Boolean input features. Restricting
inputs and outputs to be Boolean makes our setting cleaner while still
covering several relevant practical scenarios. We use notation $\text{\rm
dim}(\mathcal{M})$ for the dimension of a model $\mathcal{M}$.

A partial instance of dimension $n$ is a tuple
$\mathbf{e}\in\\{0,1,\bot\\}^{n}$. Intuitively, if $\mathbf{e}[i]=\bot$, then
the value of the $i$-th feature is undefined. Notice that an instance is a
particular case of a partial instance where all features are assigned value
either $0$ or $1$. Given two partial instances $\mathbf{e}_{1}$,
$\mathbf{e}_{2}$ of dimension $n$, we say that $\mathbf{e}_{1}$ is subsumed by
$\mathbf{e}_{2}$ if for every $i\in\\{1,\ldots,n\\}$ such that
$\mathbf{e}_{1}[i]\neq\bot$, it holds that
$\mathbf{e}_{1}[i]=\mathbf{e}_{2}[i]$. That is, $\mathbf{e}_{1}$ is subsumed
by $\mathbf{e}_{2}$ if it is possible to obtain $\mathbf{e}_{2}$ from
$\mathbf{e}_{1}$ by replacing some unknown values. Notice that a partial
instance $\mathbf{e}$ can be thought of as a compact representation of the set
of instances $\mathbf{e}^{\prime}$ such that $\mathbf{e}$ is subsumed by
$\mathbf{e}^{\prime}$, where such instances $\mathbf{e}^{\prime}$ are called
the completions of $\mathbf{e}$.

Models. A _binary decision diagram_ (BDD [38]) over instances of dimension $n$
is a rooted directed acyclic graph $\mathcal{M}$ with labels on edges and
nodes such that: (i) each leaf is labeled with $\mathbf{true}$ or
$\mathbf{false}$; (ii) each internal node (a node that is not a leaf) is
labeled with a feature $i\in\\{1,\dots,n\\}$; and (iii) each internal node has
two outgoing edges, one labeled $1$ and the another one labeled $0$. Every
instance $\mathbf{e}\in\\{0,1\\}^{n}$ defines a unique path
$\pi_{\mathbf{e}}=u_{1}\cdots u_{k}$ from the root $u_{1}$ to a leaf $u_{k}$
of $\mathcal{M}$ such that: if the label of $u_{i}$ is $j\in\\{1,\dots,n\\}$,
where $i\in\\{1,\ldots,k-1\\}$, then the edge from $u_{i}$ to $u_{i+1}$ is
labeled with $\mathbf{e}[j]$. Moreover, the instance $\mathbf{e}$ is positive,
denoted by $\mathcal{M}(\mathbf{e})=1$, if the label of $u_{k}$ is
$\mathbf{true}$; otherwise the instance $\mathbf{e}$ is negative, which is
denoted by $\mathcal{M}(\mathbf{e})=0$. A binary decision diagram
$\mathcal{M}$ is _free_ (FBDD) if for every path from the root to a leaf, no
two nodes on that path have the same label. Besides, $\mathcal{M}$ is ordered
(OBDD) if there exists a linear order $<$ on the set $\\{1,\dots,n\\}$ of
features such that, if a node $u$ appears before a node $v$ in some path in
$\mathcal{M}$ from the root to a leaf, then $u$ is labeled with $i$ and $v$ is
labeled with $j$ for features $i,j$ such that $i<j$. A _decision tree_ is
simply an FBDD whose underlying DAG is a tree. Finally, a perceptron
$\mathcal{M}$ of dimension $n$ is a pair $(w,t)$ where
${\bm{w}}\in\mathbb{R}^{n}$ and $t\in\mathbb{R}$, and the classification of an
instance $\mathbf{e}\in\\{0,1\\}^{n}$ is defined as
$\mathcal{M}(\mathbf{e})=1$ if and only if ${\bm{w}}\cdot\mathbf{e}\geq t$.

In this paper, we focus on the following classes of models: $\mathsf{OBDD}$,
the class of ordered BDDs, $\mathsf{DTree}$, the class of decision trees, and
$\mathsf{Ptron}$, the class of perceptrons. None of these classes directly
subsume the other: decision trees are not necessarily ordered, while the
underlying DAG of an OBDD is not necessarily a tree. In fact, it is known that
neither OBDDs can be compiled into polynomial-size decision trees nor decision
trees into polynomial-size OBDDs [17, 6]. Perceptrons on the other hand can
only model linear decision boundaries and thus are inherently less expressive
than decision trees or OBDDs. It is also known that perceptrons cannot be
compiled in polynomial time to decision trees or OBDDs unless
$\mathrm{P}=\text{\rm NP}$ [4].

The logic FOIL. We consider first-order logic over a vocabulary consisting of
a unary predicate Pos and a binary predicate $\subseteq$. This logic is called
first-order interpretability logic (FOIL), and it is our reference language
for defining conditions on models that we would like to reason about. In
particular, predicate Pos is used to indicate the value of an instance in a
model, while predicate $\subseteq$ is used to represent the subsumption
relation among partial instances. In what follows, we show that many natural
properties can be expressed in a simple way in FOIL, demonstrating the
suitability of this language for the purpose of expressing explainability
queries.

We assume familiarity with the syntax and semantics of first-order logic (see
the appendix for a review of these concepts). In particular, given a
vocabulary $\sigma$ consisting of relations $R_{1}$, $\ldots$, $R_{\ell}$,
recall that a structure $\mathfrak{A}$ over $\sigma$ consists of a domain,
where quantifiers are instantiated, and an interpretation for each relation
$R_{i}$. Moreover, given a first-order formula $\varphi$ defined over the
vocabulary $\sigma$, we write $\varphi(x_{1},\ldots,x_{k})$ to indicate that
$\\{x_{1},\ldots,x_{k}\\}$ is the set of free variables of $\varphi$. Finally,
given a structure $\mathfrak{A}$ over the vocabulary $\sigma$ and elements
$a_{1}$, $\ldots$, $a_{k}$ in the domain of $\mathfrak{A}$, we use
$\mathfrak{A}\models\varphi(a_{1},\ldots,a_{k})$ to indicate that formula
$\varphi$ is satisfied by $\mathfrak{A}$ when each variable $x_{i}$ is
replaced by element $a_{i}$ ($1\leq i\leq k$).

Our goal when introducing FOIL is to have a logic that allows to specify
natural properties of models in a simple way. In this sense, we still need to
define when a model $\mathcal{M}$ satisfies a formula in FOIL, as
$\mathcal{M}$ is not a structure over the vocabulary $\\{\textsc{Pos}$,
$\subseteq\\}$ (so we cannot directly use the notion of satisfaction of a
formula by a structure). More precisely, assuming that $\text{\rm
dim}(\mathcal{M})=n$, the structure $\mathfrak{A}_{\mathcal{M}}$ associated to
$\mathcal{M}$ is defined as follows. The domain of
$\mathfrak{A}_{\mathcal{M}}$ is the set $\\{0,1,\bot\\}^{n}$ of all partial
instances of dimension $n$. An instance $\mathbf{e}\in\\{0,1\\}^{n}$ is in the
interpretation of predicate Pos in $\mathfrak{A}_{\mathcal{M}}$ if and only if
$\mathcal{M}(\mathbf{e})=1$. Finally, a pair $(\mathbf{e}_{1},\mathbf{e}_{2})$
is in the interpretation of predicate $\subseteq$ in
$\mathfrak{A}_{\mathcal{M}}$ if and only if $\mathbf{e}_{1}$ is subsumed by
$\mathbf{e}_{2}$. Then, given a formula $\varphi(x_{1},\ldots,x_{k})$ in FOIL
and partial instances $\mathbf{e}_{1}$, $\ldots$, $\mathbf{e}_{k}$ of
dimension $n$, model $\mathcal{M}$ is said to satisfy
$\varphi(\mathbf{e}_{1},\ldots,\mathbf{e}_{k})$, denoted by
$\mathcal{M}\models\varphi(\mathbf{e}_{1},\ldots,\mathbf{e}_{k})$, if and only
if
$\mathfrak{A}_{\mathcal{M}}\models\varphi(\mathbf{e}_{1},\ldots,\mathbf{e}_{k})$.

Evaluation problem. FOIL is our main tool in trying to understand how
interpretable is a class of models. In particular, the following is the main
problem studied in this paper, given a class $\mathcal{C}$ of models and a
formula $\varphi(x_{1},\ldots,x_{k})$ in FOIL.

Problem: Eval$(\varphi,\mathcal{C})$ Input: A model
$\mathcal{M}\in\mathcal{C}$ of dimension $n$, and partial instances
$\mathbf{e}_{1},\ldots,\mathbf{e}_{k}$ of dimension $n$ Output: Yes, if
$\mathcal{M}\models\varphi(\mathbf{e}_{1},\ldots,\mathbf{e}_{k})$, and No
otherwise

For example, assume that $\mathsf{CNF}$, $\mathsf{DNF}$ are the classes of
models given as propositional formulae in CNF and DNF, respectively. If
$\varphi=\exists x\,\textsc{Pos}(x)$, then
$\textsc{Eval}(\varphi,\mathsf{CNF})$ is NP-complete and
$\textsc{Eval}(\varphi,\mathsf{DNF})$ can be solved in polynomial time, as
such problems correspond to the satisfiability problems for the propositional
formulae in CNF and DNF, respectively.

Given a model $\mathcal{M}$, it is important to notice that the size of the
structure $\mathfrak{A}_{\mathcal{M}}$ can be exponential in the size of
$\mathcal{M}$. Hence, $\mathfrak{A}_{\mathcal{M}}$ is a theoretical
construction needed to formally define the semantics of FOIL, but that should
not be built when verifying in practice if a formula $\varphi$ is satisfied by
$\mathcal{M}$. In fact, if we are aiming at finding tractable algorithms for
FOIL-evaluation, then we need to design an algorithm that uses directly the
encoding of $\mathcal{M}$ as a model (for example, as a binary decision tree)
rather than as a logical structure. In other words, in order to evaluate a
query $\varphi=\exists x\,\textsc{Pos}(x)$ over a model $\mathcal{M}$ of
dimension $n$, one could certainly iterate over all $2^{n}$ instances
$\mathbf{e}\in\\{0,1\\}^{n}$ and evaluate $\mathcal{M}(\mathbf{e})$. This of
course impractical for even small-dimensional data. Therefore, evaluating
formulas without iterating over the entire space of (partial) instances is the
main technical challenge behind the results presented in this paper.

##  3 Expressing Properties in the Logic

Basic queries. We provide some formulas in FOIL to gain more insight into this
logic. Fix a model $\mathcal{M}$ of dimension $n$. We can ask whether
$\mathcal{M}$ assigns value 1 to some instance by using FOIL-formula $\exists
x\,\textsc{Pos}(x)$. Similarly, formula $\exists
y\,(\textsc{Full}(y)\wedge\neg\textsc{Pos}(y))$ can be used to check whether
$\mathcal{M}$ assigns value 0 to some instance, where

$\displaystyle\textsc{Full}(x)$ $\displaystyle=$ $\displaystyle\forall
y\,(x\subseteq y\to x=y)$ (1)

is used to verify whether all values in $x$ are known (that is,
$\mathcal{M}\models\textsc{Full}(\mathbf{e})$ if and only if $\mathbf{e}$ is
an instance). Notice that formula $\textsc{Full}(y)$ has to be included in
$\exists y\,(\textsc{Full}(y)\wedge\neg\textsc{Pos}(y))$ since
$\mathcal{M}\models\neg\textsc{Pos}(\mathbf{e})$ for each partial instance
$\mathbf{e}$ with unknown values.

Given an instance $\mathbf{e}$ such that $\mathcal{M}(\mathbf{e})=1$, we can
ask if the values assigned to the first two features are necessary to obtain a
positive classification. Formally, define $\mathbf{e}_{\\{1,2\\}}$ as a
partial instance such that
$\mathbf{e}_{\\{1,2\\}}[1]=\mathbf{e}_{\\{1,2\\}}[2]=\bot$ and
$\mathbf{e}_{\\{1,2\\}}[i]=\mathbf{e}[i]$ for every $i\in\\{3,\ldots,n\\}$,
and assume that

$\displaystyle\varphi(x)$ $\displaystyle=$ $\displaystyle\forall
y\,((x\subseteq y\wedge\textsc{Full}(y))\to\textsc{Pos}(y)).$

If $\mathcal{M}\models\varphi(\mathbf{e}_{\\{1,2\\}})$, then the values
assigned in $\mathbf{e}$ to the first two features are not necessary to obtain
a positive classification. Notice that the use of unknown values in
$\mathbf{e}_{\\{1,2\\}}$ is fundamental to reason about all possible
assignments for the first two features, while keeping the remaining values of
features unchanged. Besides, observe that a similar question can be expressed
in FOIL for any set of features.

As before, we can ask if there is a completion of a partial instance
$\mathbf{e}$ that is assigned value 1, by using FOIL-formula $\psi(x)=\exists
y\,(x\subseteq y\wedge\textsc{Full}(y)\wedge\textsc{Pos}(y))$; that is,
$\mathcal{M}\models\psi(\mathbf{e})$ if and only if there is an assignment for
the unknown values of $\mathbf{e}$ that results in an instance classified
positively.

Minimal sufficient reasons. Given an instance $\mathbf{e}$ and a partial
instance $\mathbf{e}^{\prime}$ that is subsumed by $\mathbf{e}$, consider the
problem of verifying whether $\mathbf{e}^{\prime}$ is a sufficient reason for
$\mathbf{e}$ in the sense that every completion of $\mathbf{e}^{\prime}$ is
classified in the same way as $\mathbf{e}$ [34, 4, 21]. The following query
expresses this:

$\displaystyle\textsc{SR}(x,y)$ $\displaystyle=$
$\displaystyle\textsc{Full}(x)\wedge y\subseteq x\wedge\forall z\,[(y\subseteq
z\wedge\textsc{Full}(z))\to(\textsc{Pos}(x)\leftrightarrow\textsc{Pos}(z))],$
(2)

given that $\mathcal{M}\models(\mathbf{e},\mathbf{e}^{\prime})$ if and only if
$\mathbf{e}^{\prime}$ is a sufficient reason for $\mathbf{e}$. Finally, it can
also be expressed in FOIL the condition that $y$ is a minimal sufficient
reason for $x$:

$\displaystyle\textsc{mSR}(x,y)$ $\displaystyle=$
$\displaystyle\textsc{SR}(x,y)\wedge\forall z\,((z\subseteq
y\wedge\textsc{SR}(x,z))\to z=y).$

That is, $\mathcal{M}\models(\mathbf{e},\mathbf{e}^{\prime})$ if and only if
$\mathbf{e}^{\prime}$ is a sufficient reason for $\mathbf{e}$, and there is no
partial instance $\mathbf{e}^{\prime\prime}$ such that
$\mathbf{e}^{\prime\prime}$ is a sufficient reason for $\mathbf{e}$ and
$\mathbf{e}^{\prime\prime}$ is properly subsumed by $\mathbf{e}^{\prime}$.
Minimal sufficient reasons have also been called PI-explanations or abductive
explanations in the literature [35, 26, 21, 20].

Bias detection queries. Let us consider an elementary approach to fairness
based on _protected_ features, i.e., features from a set $P$ that should not
be used for decision taking (e.g., gender, age, marital status, etc). We use a
formalization of this notion proposed in [16], while noting it does not
capture many other forms of biases and unfairness [27], and is thus to be
taken only as an example. Given a model $\mathcal{M}$ of dimension $n$, and a
set of protected features $P\subseteq\\{1,\ldots,n\\}$, an instance
$\mathbf{e}$ is said to be a biased decision of $\mathcal{M}$ if there exists
an instance $\mathbf{e}^{\prime}$ such that $\mathbf{e}$ and
$\mathbf{e}^{\prime}$ differ only on features from $P$ and
$\mathcal{M}(\mathbf{e})\neq\mathcal{M}(\mathbf{e}^{\prime})$. A model
$\mathcal{M}$ is biased if and only if there is an instance $\mathbf{e}$ that
is a biased decision of $\mathcal{M}$. In what follows, we show how to encode
queries relating to biased decisions in FOIL.

Let $S=\\{1,\ldots,n\\}$, and assume that ${\bm{0}}_{S}$ is an instance of
dimension $n$ such that ${\bm{0}}_{S}[i]=0$ for every $i\in S$, and
${\bm{0}}_{S}[j]=\bot$ for every $j\in\\{1,\ldots,n\\}\setminus S$. Moreover,
define ${\bm{1}}_{S}$ in the same way but considering value 1 instead of 0,
and define

$\displaystyle\textsc{Match}(x,y,u,v)$ $\displaystyle=$ $\displaystyle\forall
z\,[(z\subseteq u\vee z\subseteq v)\to(z\subseteq x\leftrightarrow z\subseteq
y)].$

When this formula is evaluated replacing $u$ by ${\bm{0}}_{S}$ and $v$ by
${\bm{1}}_{S}$, it verifies whether $x$ and $y$ have the same value in each
feature in $S$. More precisely, given a model $\mathcal{M}$ and instances
$\mathbf{e}_{1}$, $\mathbf{e}_{2}$ of dimension $n$, we have that
$\mathcal{M}\models\textsc{Match}(\mathbf{e}_{1},\mathbf{e}_{2},{\bm{0}}_{S},{\bm{1}}_{S})$
if and only if $\mathbf{e}_{1}[i]=\mathbf{e}_{2}[i]$ for every $i\in S$.
Notice that the use of free variables $u$ and $v$ as parameters allows us to
represent the matching of two instances in the set of features $S$, as, in
fact, such matching is encoded by the formula
$\textsc{Match}(x,y,{\bm{0}}_{S},{\bm{1}}_{S})$. The use of free variables as
parameters is thus a useful feature of FOIL.

With the previous terminology, we can define a query

$\textsc{BiasedDecision}(x,u,v)\ =\ \textsc{Full}(x)\ \wedge\\\ \exists
y\,[\textsc{Full}(y)\wedge\textsc{Match}(x,y,u,v)\wedge(\textsc{Pos}(x)\leftrightarrow\neg\textsc{Pos}(y))].$

To understand the meaning of this formula, assume that
$N=\\{1,\ldots,n\\}\setminus P$ is the set of non-protected features. When
$\textsc{BiasedDecision}(x,u,v)$ is evaluated replacing $u$ by ${\bm{0}}_{N}$
and $v$ by ${\bm{1}}_{N}$, it verifies whether there exists an instance $y$
such that $x$ and $y$ have the same values in the non-protected features but
opposite classification, so that $x$ is a biased decision. Hence, the formula

$\displaystyle\textsc{BiasedModel}(u,v)$ $\displaystyle=$
$\displaystyle\exists x\,\textsc{BiasedDecision}(x,u,v)$

can be used to check whether a model $\mathcal{M}$ is biased with respect to
the set $P$ of protected features, as $\mathcal{M}$ satisfies this property if
and only if
$\mathcal{M}\models\textsc{BiasedModel}({\bm{0}}_{N},{\bm{1}}_{N})$.

A query of the form $\exists
x\,\big{(}\textsc{Pos}(x)\land(\bot,\bot,\bot,\bot,0,1,\bot)\subseteq
x\big{)}$ was included as an initial example in Section 1. According to the
formal definition of FOIL, such a query corresponds to $\varphi(u)=\exists
x\,\big{(}\textsc{Pos}(x)\land u\subseteq x\big{)}$, and the desired answer is
obtained when verifying whether $\varphi(\mathbf{e})$ is satisfied by a model,
where $\mathbf{e}[1]=\mathbf{e}[2]=\mathbf{e}[3]=\mathbf{e}[4]=\bot$,
$\mathbf{e}[5]=0$, $\mathbf{e}[6]=1$ and $\mathbf{e}[7]=\bot$. Again, notice
that the use of free variables as parameters is an important feature of FOIL.

##  4 Limits to Efficient Evaluation

Several important interpretability tasks have been shown to be tractable for
the decision models we study in the paper [4], which has justified the
informal claim that they are “interpretable”. But this does not mean that all
interpretability tasks are in fact tractable for these models. We try to
formalize this idea by studying the complexity of evaluation for queries in
FOIL over them. We show next that the evaluation problem over the models
studied in the paper can become intractable, even for some simple queries in
the logic with a natural interpretability flavor. This intractability result
is of importance, in our view, as it sheds light on the limits of efficiency
for interpretability tasks over the models studied, and hence on the
robustness of the folklore claims about them being “interpretable”.

######  Theorem 1.

There exists a formula $\psi(x)$ in FOIL for which
Eval$(\psi(x),\mathsf{DTree})$ and Eval$(\psi(x),\mathsf{OBDD})$ are NP-hard.

This result tell us that there exists a concrete property expressible in FOIL
that cannot be solved in polynomial time for decision trees and OBDDs (unless
$\text{P}=\text{\rm NP}$). In what follows, we describe this property, and how
it is represented as a formula $\psi(x)$ in FOIL (the complete proof of
Theorem 1 is provided in the appendix).

Assume that $x\subset y$ is the formula $x\subseteq y\wedge x\neq y$ that
verifies whether $x$ is properly subsumed by $y$. We first define the
following auxiliary predicates:

$\displaystyle\textsc{Adj}(x,y)$ $\displaystyle=$ $\displaystyle x\subset
y\wedge\neg\exists z\,(x\subset z\wedge z\subset y),$
$\displaystyle\textsc{Diff}(x,y)$ $\displaystyle=$
$\displaystyle\textsc{Full}(x)\wedge\textsc{Full}(y)\wedge x\neq
y\wedge\exists z\,(\textsc{Adj}(z,x)\wedge\textsc{Adj}(z,y)).$

More precisely, $\textsc{Adj}(x,y)$ is used to check whether a partial
instance $x$ is adjacent to a partial instance $y$, in the sense that $x$ is
properly subsumed by $y$ and there is no partial instance $z$ such that $x$ is
properly subsumed by $z$ and $z$ is properly subsumed by $y$. Moreover,
$\textsc{Diff}(x,y)$ is used to verify whether two instances $x$ and $y$
differ exactly in the value of one feature. By using these predicates, we
define the following notion of stability for an instance:

$\displaystyle\textsc{Stable}(x)$ $\displaystyle=$ $\displaystyle\forall
y\,[\textsc{Diff}(x,y)\to(\textsc{Pos}(x)\leftrightarrow\textsc{Pos}(y))].$

That is, an instance $x$ is said to be stable if and only if any change in
exactly one feature of $x$ leads to the same classification. Then the formula
$\psi(x)$ in Theorem 1 is defined as follows:

$\displaystyle\psi(x)$ $\displaystyle=$ $\displaystyle\exists y\,(x\subseteq
y\wedge\textsc{Pos}(y)\wedge\textsc{Stable}(y)).$

Hence, given a partial instance $x$, formula $\psi(x)$ is used to check if
there is a completion of $x$ that is stable and positive. Theorem 1 states
that checking this for decision trees and OBDDs is an intractable problem.
Observe that the notion of stability used in $\psi(x)$ has a natural
interpretability flavor: it identifies positive instances whose classification
is not affected by the perturbation of a single feature. Note as well that the
supposed interpretability of decision trees has already been questioned and
nuanced in the literature [23, 4], to which this result contributes.

##  5 Tractable Restrictions

Theorem 1 tells us that evaluation of FOIL queries can be an intractable
problem, but of course this does not completely rule out the applicability of
the logic. In fact, as we show in this section one can obtain tractability by
either restricting the analysis to a useful syntactic fragment of FOIL, or by
considering a structural restriction on the class of models over which FOIL
queries are evaluated.

###  5.1 A tractable fragment of FOIL

We present a fragment of FOIL that is simple enough to yield tractability, but
which is at the same time expressive enough to encode natural interpretability
problems. This is not a trivial challenge, though, as the proof of Theorem 1
shows intractability of queries in a syntactically simple fragment of FOIL (in
fact, only two quantifier alternations suffice for the result to hold).

Our starting point in this search is $\exists\text{\rm FOIL}$, which is the
fragment of FOIL consisting of all formulas where no universal quantifier
occurs and no existential quantifier appears under a negation (each such a
formula can be rewritten into a formula of the form $\exists
x_{1}\cdots\exists x_{k}\,\alpha$, where $\alpha$ does not mention any
quantifiers). Moreover, we consider the fragment $\forall\text{\rm FOIL}$ of
FOIL, which is defined in the same way as $\exists\text{\rm FOIL}$ but
exchanging the roles of universal and existential quantifiers. Then we show
the following:

######  Proposition 1.

Let $\varphi$ be a query in $\exists\text{\rm FOIL}$ or $\forall\text{\rm
FOIL}$. Then $\textsc{Eval}(\varphi,\mathsf{DTree})$ and
$\textsc{Eval}(\varphi,\mathsf{OBDD})$ can be solved in polynomial time.

However, the fragment $\exists\text{\rm FOIL}$ has a limited expressive power
since, for example, the predicate $\textsc{Full}(x)$ defined in (1) cannot be
expressed in it (see Appendix B for a formal proof of this claim). To remedy
this, we extend $\exists\text{\rm FOIL}$ by including predicate
$\textsc{Full}(x)$ and two other unary predicates that are common in
interpretability queries. More precisely, let $\textsc{AllPos}(x)$ and
$\textsc{AllNeg}(x)$ be unary predicates defined as follows:

$\displaystyle\textsc{AllPos}(x)$ $\displaystyle=$ $\displaystyle\forall
y\,\big{(}(x\subseteq y\wedge\textsc{Full}(y)\big{)}\to\textsc{Pos}(y)),$
$\displaystyle\textsc{AllNeg}(x)$ $\displaystyle=$ $\displaystyle\forall
y\,\big{(}x\subseteq y\to\neg\textsc{Pos}(y)\big{)}.$

Then $\exists\text{\rm FOIL}^{+}$ is defined as the fragment of FOIL
consisting of all formulae where no universal quantifier occurs and no
existential quantifier appears under a negation, and which are defined over
the extended vocabulary $\\{\textsc{Pos}$, $\subseteq$, Full, AllPos,
$\textsc{AllNeg}\\}$. In the same way, we define $\forall\text{\rm FOIL}^{+}$
by exchanging the roles of universal and existential quantifiers. Notice that
the formula defining the notion of sufficient reason in (2) is in
$\forall\text{\rm FOIL}^{+}$. Similarly, the notion of minimal sufficient
reason introduced in Section 3 can be expressed in $\forall\text{\rm
FOIL}^{+}$:

$\textsc{mSR}(x,y)\ =\ \textsc{SR}(x,y)\wedge\forall u\,[(u\subseteq y\wedge
u\neq y\wedge\textsc{Pos}(x))\to\neg\textsc{AllPos}(u)]\ \wedge\\\ \forall
v\,[(v\subseteq y\wedge v\neq
y\wedge\neg\textsc{Pos}(x))\to\neg\textsc{AllNeg}(v)].$

In what follows, we investigate the tractability of the fragments
$\exists\text{\rm FOIL}^{+}$ and $\forall\text{\rm FOIL}^{+}$. In particular,
in the case of $\exists\text{\rm FOIL}^{+}$, we show that the tractability for
a class of models $\mathcal{C}$ can be characterized in terms of the
tractability in $\mathcal{C}$ of two specific queries in $\exists\text{\rm
FOIL}^{+}$:

$\textsc{PartialAllPos}(x,y,z)\ =\ \exists u\,[x\subseteq
u\wedge\textsc{AllPos}(u)\ \wedge\\\ \exists v\,(y\subseteq v\wedge u\subseteq
v)\wedge\exists w\,(z\subseteq w\wedge u\subseteq w)],$

and $\textsc{PartialAllNeg}(x,y,z)$ that is defined exactly as
$\textsc{PartialAllPos}(x,y,z)$ but replacing $\textsc{AllPos}(u)$ by
$\textsc{AllNeg}(u)$. More precisely, we have the following:

######  Theorem 2.

For every class $\mathcal{C}$ of models, the following conditions are
equivalent: (a) $\textsc{Eval}(\varphi,\mathcal{C})$ can be solved in
polynomial time for each query $\varphi$ in $\exists\text{\rm FOIL}^{+}$; (b)
$\textsc{Eval}(\textsc{PartialAllPos},\mathcal{C})$ and
$\textsc{Eval}(\textsc{PartialAllNeg},\mathcal{C})$ can be solved in
polynomial time.

This theorem gives us a concrete way to study the tractability of
$\exists\text{\rm FOIL}^{+}$ over a class of models. Besides, as the negation
of a query in $\forall\text{\rm FOIL}^{+}$ is a query in $\exists\text{\rm
FOIL}^{+}$, Theorem 2 also provides us with a tool to study the tractability
of $\forall\text{\rm FOIL}^{+}$. In fact, it is possible to prove the
following for the class $\mathsf{Ptron}$ of perceptrons.

######  Proposition 2.

The problems $\textsc{Eval}(\textsc{PartialAllPos},\mathsf{Ptron})$ and
$\textsc{Eval}(\textsc{PartialAllNeg},\mathsf{Ptron})$ can be solved in
polynomial time.

From this proposition and Theorem 2, it is possible to establish the following
tractability results for $\exists\text{\rm FOIL}^{+}$ and $\forall\text{\rm
FOIL}^{+}$.

######  Corollary 1.

Let $\varphi$ be a query in $\exists\text{\rm FOIL}^{+}$ or $\forall\text{\rm
FOIL}^{+}$. Then $\textsc{Eval}(\varphi,\mathsf{Ptron})$ can be solved in
polynomial time.

In fact, a more general corollary holds:
$\textsc{Eval}(\varphi,\mathsf{Ptron})$ is tractable as long as $\varphi$ is a
Boolean combination of queries in $\exists\text{\rm FOIL}^{+}$ (which covers
the case of $\forall\text{\rm FOIL}^{+}$). Unfortunately, these queries turn
out to be intractable over decision trees and OBDDs.

######  Proposition 3.

Let $\mathcal{C}$ be $\mathsf{OBDD}$ or $\mathsf{DTree}$. The problems
$\textsc{Eval}(\textsc{PartialAllPos},\mathcal{C})$ and
$\textsc{Eval}(\textsc{PartialAllNeg},\mathcal{C})$ are NP-hard.

###  5.2 A structural restriction ensuring tractability

We now look into the other direction suggested before, and identify a
structural restriction on OBDDs that ensures tractability of evaluation for
each query in FOIL. This restriction is based on the usual notion of width of
an OBDD [5, 9]. An OBDD $\mathcal{M}$ over a set $\\{1,\dots,n\\}$ of features
is complete if each path from the root of $\mathcal{M}$ to one of its leaves
includes every feature in $\\{1,\dots,n\\}$. The width of $\mathcal{M}$,
denoted by $0pt(\mathcal{M})$, is defined as the maximum value $n_{i}$ for
$i\in\\{1,\ldots,n\\}$, where $n_{i}$ is the number of nodes of $\mathcal{M}$
labeled by feature $i$. Then, given $k\geq 1$, $k\text{-}\mathsf{COBDD}$ is
defined as the class of complete OBDDs $\mathcal{M}$ such that
$0pt(\mathcal{M})\leq k$. By building on techniques from [9], we prove that:

######  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.

##  6 Practical Implementation

The FOIL language has at least two downsides from a usability point of view.
First, in FOIL every query is constructed using a minimal set of basic logical
constructs. Moreover, the variables in queries are instantiated by feature
vectors that may have hundreds of components. This implies that some simple
queries may need fairly long and complicated FOIL expressions. Second, FOIL is
designed to only work over models with binary input features. These downsides
are a consequence of our design decisions that were reasonable for a detailed
theoretical analysis but may hamper FOIL usage in more general scenarios, in
particular when models have (many) categorical or numerical input features.

In this section, we describe a simple high-level syntax and implementation of
a more user-friendly language (_à la_ SQL) to query general decision trees,
and we show how to compile it into FOIL queries to be evaluated over a
suitable binarization of the queried model. As a whole, the pipeline requires
several pieces that we explain in this section: (i) a working and efficient
query-evaluation implementation of a fragment of FOIL over a suitable sub-
class of Binary Decision Diagrams (BDDs), (ii) a transformation from the high-
level syntax to FOIL queries, and (iii) a transformation from a general
decision tree to a BDD over which the FOIL query can be efficiently evaluated.
We only present here the main ideas and intuitions of the implemented methods.
A detailed exposition along with our implementation and a set of real examples
can be found in the supplementary material.

###  6.1 Implementing and testing core FOIL

We implemented a version of the algorithm derived from Section 5.1 for
evaluating existential and universal FOIL queries that is proven to work over
a suitable sub-class of BDDs. The method receives a query as a plain text file
and a BDD in JSON format. We tested the efficiency of our implementation
varying three different parameters: the number of input features, the number
of leaves of the decision tree, and the size of the input queries. We created
a set of trees trained with random input data with input feature dimensions in
the range $[10,350]$, and of $100$, $500$ and $1000$ leaves ($24$ different
decision trees). We note that the best performing decision trees over standard
datasets [37] rarely contain more than $1000$ total nodes [25], thus the trees
that we tested can be considered of standard size. We created a set of random
queries with $1$ to $4$ quantified variables, and a varying number of
operators ($60$ different queries). We run every query $5$ times over each
tree, and averaged the execution time to obtain the running time of one case.
From all our tests no case required more than $2.5$ seconds for its complete
evaluation with a total average execution time of $0.213$ seconds and standard
deviation of $0.169$ in the whole dataset. Figure 2(a) shows the average time
(average over different queries) for all settings. We observed that some
queries where specially more time consuming than others. Figure 2(b) shows the
maximum execution time over all queries for each setting. The most important
factor when evaluating queries is the number of input features, which is
consistent with a theoretical worst case analysis. All experiments where run
on a personal computer with a 2.48GHz Intel N3060 processor and 2GB RAM. The
exact details of the machine are presented in the supplementary material.

(a) Average time for 60 random FOIL queries over Decision Trees trained with
random data.

(b) Maximum time for 60 random FOIL queries over Decision Trees trained with
random data.

⬇

\par> exists student,

student.age <= 18 and

(student.internetAtHome or

student.male) and

goodGrades(student)

(c) Example of a query in our system executed over a model trained in the
dataset in [29].

Figure 2: Execution time for FOIL queries and a high-level practical syntax.

###  6.2 Interpretability symbolic queries in practice

High-level features. We designed and implemented a prototype system for user-
friendly interpretability queries. Figure 2(c) shows a real example query that
can be posed in our system for a model trained over the _Student Performance
Data Set_ [29]. Notice that our syntax allow named features, names for the
target class (goodGrades in the example) and the comparison with numerical
thresholds which goes beyond the FOIL formalization. Our current
implementation allows for numerical and logical comparisons, as well as handy
logical shortcuts such as implies and iff. Moreover we implemented a wrapper
to directly import Decision Trees trained in the Scikit-learn [30] library.

Binarizing models and queries. One of the main issues when compiling these new
queries into FOIL is how to binarize numerical features. Choi et al. [12]
describe in extensive detail an approach to encode general decision trees into
binary ones. The key observation is that one can separate numerical values
into equivalence classes depending on the thresholds used by a decision tree.
For example, assume a tree with an _age_ feature that learns nodes with
thresholds $\text{age}\leq 16$ and $\text{age}\leq 24$. It is clear that such
a tree cannot distinguish an $\text{age}=17$ from an $\text{age}=19$. In
general, every tree induces a finite number of equivalence classes for each
numerical feature and one can take advantage of that to produce a binary
version of the tree [12]. In our case, we also need to take the query into
account. For instance, when evaluating a query with a condition student.age <=
18, ages $17$ and $19$ become distinguishable. Considering all these
thresholds we have intervals $(-\infty,16]$, $(16,18]$, $(18,24]$,
$(24,\infty)$ and we can use four binary features to encode in which interval
an age value lies. It is worth noting that this process creates extra
artificial features, and thus, the decision tree that learned real thresholds
needs to be binarized in the new feature space accordingly. One can show that
a naive implementation would imply an exponential blow up in the size of the
new tree. To avoid this our binarization process transforms the real-valued
decision tree into a binary FBDD, over which we prove that our polynomial
algorithms from Section 5.1 are still applicable.

Performance tests. We tested a set of $20$ handcrafted queries over decision
trees with up to 400 leaves trained for the Student Performance Data Set [29],
which combines Boolean and numerical features. Our results show that natural
queries can be evaluated over decision trees of standard size [25] in less
than a second on a standard personal machine, thus validating the practical
usability of our prototype.

##  7 Final Remarks and Future Work

In several aspects the logic FOIL is limited in expressive power for
interpretability purposes. This was a design decision for this paper, in order
to start with a “minimal” logic that would allow highlighting the benefits of
having a declarative language for interpretability tasks, and at the same time
allowing to carry out a clean theoretical analysis of its evaluation
complexity. However, a genuinely practical declarative language should include
other functionalities that allow more sophisticated queries to be expressed.
As an example, consider the notion of SHAP-score [24] that has a predominant
place in the literature on interpretability issues today. In a nutshell, for a
decision model $\mathcal{M}$ with $\dim(\mathcal{M})=n$ and instance
$\mathbf{e}\in\\{0,1\\}^{n}$, this score corresponds to a weighted sum of
expressions of the form $\\#\textsc{Pos}_{S}(\mathbf{e})$, for
$S\subseteq\\{1,\dots,n\\}$, where $\\#\textsc{Pos}_{S}(\mathbf{e})$ is the
number of instances $\mathbf{e}^{\prime}$ for which
$\mathcal{M}(\mathbf{e}^{\prime})=1$ and $\mathbf{e}^{\prime}$ coincides with
$\mathbf{e}$ over all features in $S$. Expressing this query, hence, requires
extending FOIL with a recursive mechanism that permits to iterate over the
subsets $S$ of $\\{1,\dots,n\\}$, and a feature for counting the number of
positive completions of a partial instance; e.g., in the form of a “numerical”
query $\phi(x):=\\#y.(x\subseteq y\wedge\textsc{Pos}(y))$. Logics of this kind
abound in computer science logic (c.f., [22, 2]), and one could use all this
knowledge in order to build a suitable extension of FOIL for dealing with this
kind of interpretability tasks. One can also envision a language facilitating
the comparison of different models by providing separate Pos predicates for
each of them. Then, for example, one can ask whether two models are
equivalent, or if they differ for a particular kind of instances. Such an
extension can affect the complexity of evaluation in nontrivial ways.

Arguably, interpretability measures the degree in which _humans_ can
understand decisions made by _machines_. One of our main calls in this paper
is to build more _symbolic_ interpretability tools, and thus, make them closer
to how humans reason about facts and situations. Having a symbolic high-level
interpretability language to inspect ML models and their decisions is thus a
natural and challenging way of pursuing this goal. We took a step further in
this paper presenting theoretical and practical results, but several problems
remain open. A particularly interesting one is whether a logical language can
effectively interact with intrinsically non-symbolic models, and if so, what
mechanisms could allow for practical tractability without sacrificing provable
correctness.

## Acknowledgments and Disclosure of Funding

This work was partially funded by ANID \- Millennium Science Initiative
Program - Code ICN17_002. Arenas is funded by Fondecyt grant 1191337, while
Barceló and Pérez are funded by Fondecyt grant 1200967.

## References

  * [1] S. Abiteboul, R. Hull, and V. Vianu.  Foundations of Databases.  Addison-Wesley, 1995.
  * [2] M. Arenas, M. Muñoz, and C. Riveros.  Descriptive complexity for counting complexity classes.  Logical Methods in Computer Science ; Volume 16, pages Issue 1 ; 1860–5974, 2020.
  * [3] F. Baader, D. Calvanese, D. L. McGuinness, D. Nardi, and P. F. Patel-Schneider, editors.  The Description Logic Handbook: Theory, Implementation, and Applications.  Cambridge University Press, 2003.
  * [4] P. Barceló, M. Monet, J. Pérez, and B. Subercaseaux.  Model interpretability through the lens of computational complexity.  In NeurIPS, 2020.
  * [5] B. Bollig.  On the width of ordered binary decision diagrams.  In COCOA, pages 444–458, 2014.
  * [6] Y. Breitbart, H. Hunt, and D. Rosenkrantz.  On the size of binary decision diagrams representing boolean functions.  Theoretical Computer Science, 145(1-2):45–69, July 1995.
  * [7] R. E. Bryant.  Graph-based algorithms for boolean function manipulation.  IEEE Trans. Comput., 35(8):677–691, Aug. 1986.
  * [8] F. Capelli and S. Mengel.  Knowledge compilation, width and quantification.  CoRR, abs/1807.04263, 2018.
  * [9] F. Capelli and S. Mengel.  Tractable QBF by Knowledge Compilation.  In STACS, pages 18:1–18:16, 2019.
  * [10] H. Chan and A. Darwiche.  Reasoning about bayesian network classifiers.  In UAI, pages 107–115, 2003.
  * [11] C. C. Chang and H. J. Keisler.  Model theory.  Elsevier, 1990.
  * [12] A. Choi, A. Shih, A. Goyanka, and A. Darwiche.  On symbolically encoding the behavior of random forests.  CoRR, abs/2007.01493, 2020.
  * [13] A. Choi, R. Wang, and A. Darwiche.  On the relative expressiveness of bayesian and neural networks.  Int. J. Approx. Reason., 113:303–323, 2019.
  * [14] K. Chubarian and G. Turán.  Interpretability of bayesian network classifiers: OBDD approximation and polynomial threshold functions.  In ISAIM, 2020.
  * [15] E. M. Clarke, O. Grumberg, and D. A. Peled.  Model checking.  MIT Press, 2001.
  * [16] A. Darwiche and A. Hirth.  On the reasons behind decisions.  In ECAI, pages 712–720, 2020.
  * [17] A. Darwiche and P. Marquis.  A knowledge compilation map.  Journal of Artificial Intelligence Research, 17:229–264, Sept. 2002\.
  * [18] F. Doshi-Velez and B. Kim.  Towards a rigorous science of interpretable machine learning, 2017.
  * [19] L. H. Gilpin, D. Bau, B. Z. Yuan, A. Bajwa, M. Specter, and L. Kagal.  Explaining explanations: An overview of interpretability of machine learning.  In DSAA, pages 80–89, 2018.
  * [20] A. Ignatiev, N. Narodytska, and J. Marques-Silva.  Abduction-based explanations for machine learning models.  CoRR, abs/1811.10656, 2018.
  * [21] Y. Izza, A. Ignatiev, and J. Marques-Silva.  On explaining decision trees.  CoRR, abs/2010.11034, 2020.
  * [22] L. Libkin.  Elements of Finite Model Theory.  Texts in Theoretical Computer Science. An EATCS Series. Springer, 2004\.
  * [23] Z. C. Lipton.  The mythos of model interpretability: In machine learning, the concept of interpretability is both important and slippery.  Queue, 16(3):31–57, June 2018.
  * [24] S. M. Lundberg and S. Lee.  A unified approach to interpreting model predictions.  In NIPS, pages 4765–4774, 2017.
  * [25] R. G. Mantovani, T. Horváth, R. Cerri, S. B. Junior, J. Vanschoren, and A. C. P. de Leon Ferreira de Carvalho.  An empirical study on hyperparameter tuning of decision trees.  CoRR, abs/1812.02207, 2018.
  * [26] J. Marques-Silva, T. Gerspacher, M. C. Cooper, A. Ignatiev, and N. Narodytska.  Explaining naive bayes and other linear classifiers with polynomial time and delay.  In H. Larochelle, M. Ranzato, R. Hadsell, M. Balcan, and H. Lin, editors, Advances in Neural Information Processing Systems 33: Annual Conference on Neural Information Processing Systems 2020, NeurIPS 2020, December 6-12, 2020, virtual, 2020.
  * [27] N. Mehrabi, F. Morstatter, N. Saxena, K. Lerman, and A. Galstyan.  A survey on bias and fairness in machine learning.  ACM Comput. Surv., 54(6), July 2021.
  * [28] C. Molnar.  Interpretable Machine Learning.  2019\.  https://christophm.github.io/interpretable-ml-book/.
  * [29] F. Pagnotta and H. M. Amran.  Using data mining to predict secondary school student alcohol consumption, 2016.
  * [30] F. Pedregosa, G. Varoquaux, A. Gramfort, V. Michel, B. Thirion, O. Grisel, M. Blondel, P. Prettenhofer, R. Weiss, V. Dubourg, J. Vanderplas, A. Passos, D. Cournapeau, M. Brucher, M. Perrot, and E. Duchesnay.  Scikit-learn: Machine learning in Python.  Journal of Machine Learning Research, 12:2825–2830, 2011.
  * [31] M. T. Ribeiro, S. Singh, and C. Guestrin.  "why should I trust you?": Explaining the predictions of any classifier.  In SIGKDD, pages 1135–1144, 2016.
  * [32] M. T. Ribeiro, S. Singh, and C. Guestrin.  Anchors: High-precision model-agnostic explanations.  In AAAI, pages 1527–1535, 2018.
  * [33] C. Rudin.  Please stop explaining black box models for high stakes decisions.  CoRR, abs/1811.10154, 2018.
  * [34] A. Shih, A. Choi, and A. Darwiche.  A symbolic approach to explaining bayesian network classifiers.  In J. Lang, editor, Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, IJCAI 2018, July 13-19, 2018, Stockholm, Sweden, pages 5103–5111, 2018.
  * [35] A. Shih, A. Choi, and A. Darwiche.  A symbolic approach to explaining bayesian network classifiers, 2018.
  * [36] E. Strumbelj and I. Kononenko.  An efficient explanation of individual classifications using game theory.  J. Mach. Learn. Res., 11:1–18, 2010.
  * [37] J. Vanschoren, J. N. Van Rijn, B. Bischl, and L. Torgo.  Openml: networked science in machine learning.  ACM SIGKDD Explorations Newsletter, 15(2):49–60, 2014.
  * [38] I. Wegener.  Bdds: design, analysis, complexity, and applications.  Discrete Applied Mathematics, 138(1-2):229–251, 2004.

Appendix

#### Organization

The supplementary material is organized as follows: Section A presents a brief
review of the concepts concerning first-order logic that are used in our work.
Section C presents a proof of Theorem 1, our negative result concerning
decision trees and OBDDs, while Section D is devoted to our positive result.
Section B proves that $\exists\text{\rm FOIL}^{+}$ is strictly more expressive
than $\exists\text{\rm FOIL}$, justifying its independent study. Then, Section
E is devoted to the tractability of $\exists\text{\rm FOIL}$ and
$\exists\text{\rm FOIL}^{+}$; it includes proofs both for Theorem 2 and
Proposition 2, which together imply the tractability of $\exists\text{\rm
FOIL}^{+}$ for perceptrons. Next, Section F presents a proof of Theorem 3,
implying the full tractability of FOIL for a restricted class of OBDDs.
Section G discusses details of the practical implementation, while Section H
explains the the methodology of our experiments. Then, Section I discusses
details of the high-level version we implemented, and also presents several
examples of queries for the _Student Performance Data Set_ which serve to show
the usability of our implementation in practice. Finally Section J explains
the binarization process for real-valued decision trees and high-level
queries. A repository with code with our implementation for FOIL and the high-
level syntax as well as examples and scripts to replicate our experiments can
be found at

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

##  Appendix A Syntax and semantics of first-order logic

We review the definition of first-order logic (FO) over vocabularies
consisting only of relations.

#### Syntax of FO.

A vocabulary $\sigma$ is a finite set $\\{R_{1},\dots,R_{m}\\}$, where each
$R_{i}$ is a relation symbol with associated arity $n_{i}>0$, for
$i\in\\{1,\ldots,m\\}$. We assume the existence of a countably infinite set of
variables $\\{x,y,z,\dots\\}$, possibly with subscripts. The set of FO-
formulas over $\sigma$ is inductively defined as follows.

  1. 1.

If $x,y$ are variables, then $x=y$ is an FO-formula over $\sigma$.

  2. 2.

If relation symbol $R\in\sigma$ has arity $n>0$ and $x_{1},\dots,x_{n}$ are
variables, then $R(x_{1},\dots,x_{n})$ is an FO-formula over $\sigma$.

  3. 3.

If $\varphi,\psi$ are FO-formulas over $\sigma$, then $(\neg\varphi)$,
$(\varphi\vee\psi)$, and $(\varphi\wedge\psi)$ are FO-formulas over $\sigma$.

  4. 4.

If $x$ is a variable and $\varphi$ is an FO-formula over $\sigma$, then
$(\exists x\,\varphi)$ and $(\forall x\,\varphi)$ are FO-formulas over
$\sigma$.

FO-formulas of type (1) and (2) are called atomic. A variable $x$ in FO-
formula $\varphi$ appears free, if there is an occurrence of $x$ in $\varphi$
that is not in the scope of a quantifier $\exists x$ or $\forall x$. An FO-
sentence is an FO-formula without free variables. We often write
$\varphi(x_{1},\ldots,x_{k})$ to denote that $\\{x_{1},\ldots,x_{k}\\}$ is the
set of free variables of $\varphi$.

#### Semantics of FO.

FO-formulae over a vocabulary $\sigma$ are interpreted over
$\sigma$-structures. Formally, a $\sigma$-structure is a tuple

$\displaystyle\mathfrak{A}$ $\displaystyle=$ $\displaystyle\langle
A,\,R_{1}^{\mathfrak{A}},\cdots,R_{m}^{\mathfrak{A}}\rangle,$

where $A$ is the domain of $\mathfrak{A}$, and for each relation symbol
$R\in\sigma$ of arity $n$, we have that $R^{\mathfrak{A}}$ is an $n$-ary
relation over $A$. We call $R_{i}^{\mathfrak{A}}$ the interpretation of
$R_{i}$ in $\mathfrak{A}$.

Let $\varphi$ be an FO-formula over a vocabulary $\sigma$, and $\mathfrak{A}$
a $\sigma$-structure. Consider a mapping $\nu$ that associates an element in
$A$ to each variable. We formally define the satisfaction of FO-formula
$\varphi$ over the pair $(\mathfrak{A},\nu)$, denoted by
$(\mathfrak{A},\nu)\models\varphi$, as follows.

  1. 1.

If $\varphi$ is an atomic formula of the form $x=y$, then
$(\mathfrak{A},\nu)\models\varphi\,\Leftrightarrow\,\nu(t_{1})=\nu(t_{2})$.

  2. 2.

If $\varphi$ is an atomic formula of the form $R(x_{1},\ldots,x_{n})$ for some
$R\in\sigma$, then
$(\mathfrak{A},\nu)\models\varphi\,\Leftrightarrow\,(\nu(x_{1}),\dots,\nu(x_{n}))\in
R^{\mathfrak{A}}$.

  3. 3.

If $\varphi$ is of the form $(\neg\psi)$, then
$(\mathfrak{A},\nu)\models\varphi\,\Leftrightarrow\,(\mathfrak{A},\nu)\not\models\psi$.

  4. 4.

If $\varphi$ is of the form $(\psi\vee\psi^{\prime})$, then
$(\mathfrak{A},\nu)\models\varphi$ iff $(\mathfrak{A},\nu)\models\psi$ or
$(\mathfrak{A},\nu)\models\psi^{\prime}$.

  5. 5.

If $\varphi$ is of the form $(\psi\wedge\psi^{\prime})$, then
$(\mathfrak{A},\nu)\models\varphi$ iff $(\mathfrak{A},\nu)\models\psi$ and
$(\mathfrak{A},\nu)\models\psi^{\prime}$.

  6. 6.

If $\varphi$ is of the form $(\exists x\,\psi)$, then
$(\mathfrak{A},\nu)\models\varphi$ iff there exists $a\in A$ for which
$(\mathfrak{A},\nu[x/a])\models\psi$. Here, $\nu[x/a]$ is a mapping that takes
the same value as $\nu$ on every variable $y\neq x$, and takes value $a$ on
$x$.

  7. 7.

If $\varphi$ is of the form $(\forall x\,\psi)$, then
$(\mathfrak{A},\nu)\models\varphi$ iff for every $a\in A$ we have that
$(\mathfrak{A},\nu[x/a])\models\psi$.

For an FO-formula $\varphi(x_{1},\dots,x_{k})$ and assignment $\nu$ such that
$\nu(x_{i})=a_{i}$, for each $i\in\\{1,\ldots,k\\}$, we write
$\mathfrak{A}\models\varphi(a_{1},\ldots,a_{k})$ to denote that
$(\mathfrak{A},\nu)\models\varphi$. If $\varphi$ is a sentence, we write
simply $\mathfrak{A}\models\varphi$, as for any pair of mappings $\nu_{1}$,
$\nu_{2}$ for the variables, it holds that
$(\mathfrak{A},\nu_{1})\models\varphi$ iff
$(\mathfrak{A},\nu_{2})\models\varphi$.

##  Appendix B Proof that the FULL predicate cannot be expressed in the
existential fragment of FOIL

This proof requires some background in model theory. Namely, it uses the
following ideas:

  * •

Given a structure $\mathfrak{A}$ with domain $A$, a set $S\subseteq A$ induces
a _sub-structure_ $\mathfrak{A}^{\prime}$ such that the domain of
$\mathfrak{A}^{\prime}$ is $A^{\prime}$ and
$R^{\mathfrak{A}^{\prime}}=R^{\mathfrak{A}}\cap S^{n}$ for every relation
$R\in\sigma$ of arity $n$.

  * •

Let $\mathfrak{A}$, $\mathfrak{B}$ be two structures over a vocabulary
$\sigma$ with domains $A$ and $B$, respectively. An _isomorphism_ $f:A\to B$
between $\mathfrak{A}$ and $\mathfrak{B}$ satisfies the following property for
every FO-formula $\varphi$ over $\sigma$, and every mapping $\nu$:

$(\mathfrak{A},\nu)\models\varphi\ \iff\
(\mathfrak{B},f\circ\nu)\models\varphi$

where $(f\circ\nu)$ is a mapping that associates $f(\nu(x))$ to each variable
$x$.

  * •

If $\varphi(x_{1},\ldots,x_{k})$ is an existential FO-formula over a
vocabulary $\sigma$, $\mathfrak{A}$ is a $\sigma$-structure with domain $A$,
$\mathfrak{A}^{\prime}$ is an induced sub-structure of $\mathfrak{A}$ with
domain $A^{\prime}$, and $a_{1},\ldots,a_{k}\in A^{\prime}$:

$\mathfrak{A}^{\prime}\models\varphi(a_{1},\ldots,a_{k})\ \implies\
\mathfrak{A}\models\varphi(a_{1},\ldots,a_{k})$

All these ideas are standard, and can be found for example in the reference
book of Chang and Keisler [11].

We now proceed with the actual proof. For the sake of contradiction, assume
that $\textsc{Full}(x)$ can be expressed in $\exists\text{\rm FOIL}$. More
precisely, assume that $\varphi(x)$ is a formula in $\exists\text{\rm FOIL}$
such that for every $n\geq 1$, every model $\mathcal{M}$ of dimension $n$, and
every partial instance $\mathbf{e}$ of dimension $n$:

$\displaystyle\mathfrak{A}_{\mathcal{M}}\models\varphi(\mathbf{e})$ if and
only if $\displaystyle\mathbf{e}\text{ is an instance}.$ (3)

Let $\mathcal{M}_{1}$ be a model of dimension 1 such that
$\mathcal{M}_{1}(\mathbf{e})=0$ for every instance $\mathbf{e}$. Then we have
that:

$\displaystyle\mathfrak{A}_{\mathcal{M}_{1}}$ $\displaystyle=$
$\displaystyle\langle\\{\bot,0,1\\},\textsc{Pos}^{\mathfrak{A}_{\mathcal{M}_{1}}},\subseteq^{\mathfrak{A}_{\mathcal{M}_{1}}}\rangle,$

where $\textsc{Pos}^{\mathfrak{A}_{\mathcal{M}_{1}}}=\emptyset$. Moreover,
given condition 3, we also know that
$\mathfrak{A}_{\mathcal{M}_{1}}\models\varphi((0))$. Let $\mathcal{M}_{2}$ be
a model of dimension 2 such that $\mathcal{M}_{2}(\mathbf{e})=0$ for every
instance $\mathbf{e}$. Then we have that:

$\displaystyle\mathfrak{A}_{\mathcal{M}_{2}}$ $\displaystyle=$
$\displaystyle\langle\\{\bot,0,1\\}^{2},\textsc{Pos}^{\mathfrak{A}_{\mathcal{M}_{2}}},\subseteq^{\mathfrak{A}_{\mathcal{M}_{2}}}\rangle,$

where $\textsc{Pos}^{\mathfrak{A}_{\mathcal{M}_{2}}}=\emptyset$. Moreover, let
$\mathfrak{A}^{\prime}$ be the sub-structure of
$\mathfrak{A}_{\mathcal{M}_{2}}$ induced by the set of instances
$\\{(\bot,\bot),(0,\bot),(1,\bot)\\}$. Then we have that function
$f:\\{(\bot),(0),(1)\\}\to\\{(\bot,\bot),(0,\bot),(1,\bot)\\}$ defined as
$f((x))=(x,\bot)$ is an isomorphism from $\mathfrak{A}_{\mathcal{M}_{1}}$ to
$\mathfrak{A}^{\prime}$ such that $f((0))=(0,\bot)$. Hence, given that
$\varphi(x)$ is a formula in first-order logic and
$\mathfrak{A}_{\mathcal{M}_{1}}\models\varphi((0))$, we conclude that
$\mathfrak{A}^{\prime}\models\varphi((0,\bot))$. Moreover, given that
$\mathfrak{A}^{\prime}$ is an induced sub-structure of
$\mathfrak{A}_{\mathcal{M}_{2}}$ and $\varphi(x)$ is an existential formula in
first-order logic, we have that
$\mathfrak{A}_{\mathcal{M}_{2}}\models\varphi((0,\bot))$. Notice that this
contradicts condition 3, as $(0,\bot)$ is not an instance.

##  Appendix C Proof of Theorem 1

Let us restate the theorem for the reader’s convenience.

######  Theorem 1.

There exists a formula $\psi(x)$ in FOIL for which
Eval$(\psi(x),\mathsf{DTree})$ and Eval$(\psi(x),\mathsf{OBDD})$ are NP-hard.

###### Proof.

We show that the problem is NP-hard by reducing from the satisfiability
problem for propositional formulas in 3-CNF. We will in fact show that
hardness holds already for the class $\mathsf{DTree}\cap\mathsf{OBDD}$, which
proves both cases a once. Let $\varphi=C_{1}\wedge\cdots\wedge C_{n}$ be a
propositional formula, where each $C_{i}$ is a disjunction of three literal
and does not contain repeated or complementary literals. Moreover, assume that
$\\{x_{1},\ldots,x_{m}\\}$ is the set of variables occurring in $\varphi$, and
the proof will use partial instances of dimension $n+m$. Notice that the last
$m$ features of such a partial instance $\mathbf{e}$ naturally define a truth
assignment for the propositional formula $\varphi$. More precisely, for every
$i\in\\{1,\ldots,n\\}$, we use notation $\mathbf{e}(C_{i})=1$ to indicate that
there is a disjunct $\ell$ of $C_{i}$ such that $\ell=x_{j}$ and
$\mathbf{e}[n+j]=1$, or $\ell=\neg x_{j}$ and $\mathbf{e}[n+j]=0$, for some
$j\in\\{1,\ldots,m\\}$. Furthermore, we say $\mathbf{e}(\varphi)=1$ if
$\mathbf{e}(C_{i})=1$ for every $i\in\\{1,\ldots,n\\}$.

We will build an _ordered decision tree_ (thus belonging to
$\mathsf{DTree}\cap\mathsf{OBDD})$, over the natural ordering
$1<2<\cdots<n+m-1<n+m$. Let us denote this ordering with ${\prec}$ in order to
avoid confusion. For each clause $C_{i}$ ($i\in\\{1,\ldots,n\\}$), let
$\mathcal{T}_{C_{i}}$ be a decision tree of dimension $n+m$ (but that will
only use features $n+1,\ldots,n+m$) such that for every entity $\mathbf{e}$:
$\mathcal{T}_{C_{i}}(\mathbf{e})=1$ if and only $\mathbf{e}(C_{i})=1$.
Moreover, we require each $\mathcal{T}_{C_{i}}$ to be ordered with respect to
${\prec}$, Notice that $\mathcal{T}_{C_{i}}$ can be constructed in constant
time as it only needs to contain at most eight paths of depth 3. For example,
assuming that $C=(x_{1}\vee x_{2}\vee x_{3})$, a possible decision tree
$\mathcal{T}_{C}$ is depicted in the following figure:

$n+1$$n+2$$n+2$$n+3$$n+3$$n+3$$n+3$$\mathbf{false}$$\mathbf{true}$$\mathbf{true}$$\mathbf{true}$$\mathbf{true}$$\mathbf{true}$$\mathbf{true}$$\mathbf{true}$$0$$1$$0$$1$$0$$1$$0$$1$$0$$1$$0$$1$$0$$1$

Moreover, define $\mathcal{T}_{\varphi}$ as the following decision tree,
clearly ordered with respect to ${\prec}$:

$1$$\mathcal{T}_{C_{1}}$$2$$\mathcal{T}_{C_{2}}$$3$$\mathcal{T}_{C_{3}}$$\cdots$$n$$\mathcal{T}_{C_{n}}$$\mathbf{true}$$0$$1$$0$$1$$0$$1$$1$$0$$1$

Finally, define $\mathbf{e}$ as a partial instance of dimension $n+m$ such
that $\mathbf{e}[i]=1$ for every $i\in\\{1,\ldots,n\\}$, and
$\mathbf{e}[n+j]=\bot$ for every $j\in\\{1,\ldots,m\\}$, and define $\psi(x)$
as the following formula in FOIL (equivalent to the formula presented in the
body of the paper):

$\psi(x)\ =\ \exists y\,(x\subseteq y\wedge\textsc{Full}(y)\wedge\forall
z\,((z\subseteq y\wedge\neg y\subseteq z)\ \rightarrow\\\ \exists
u\,(z\subseteq u\wedge\neg u\subseteq z\wedge\neg\textsc{Full}(u))\vee\forall
v\,((z\subseteq v\wedge\neg v\subseteq z)\rightarrow\textsc{Pos}(v)))).$ (4)

Interestingly, $\psi(x)$ can be rewritten by using only two variables, which
proves that an even more restricted fragment of FOIL is hard to evaluate. The
following two-variable formula is equivalent to $\psi(x)$:

$\exists y\,(x\subseteq y\wedge\textsc{Full}(y)\wedge\forall x\,((x\subseteq
y\wedge\neg y\subseteq x)\ \rightarrow\\\ \exists y\,(x\subseteq y\wedge\neg
y\subseteq x\wedge\neg\textsc{Full}(y))\vee\forall y\,((x\subseteq y\wedge\neg
y\subseteq x)\rightarrow\textsc{Pos}(y)))).$

In what follows, we prove that $\varphi$ is satisfiable if and only if
$\mathfrak{A}_{\mathcal{T}_{\varphi}}\models\psi(\mathbf{e})$, from which we
conclude that the theorem holds.

  * $(\Leftarrow)$

Assume that $\mathfrak{A}_{\mathcal{T}_{\varphi}}\models\psi(\mathbf{e})$, and
assume that $\mathbf{e}_{1}$ is a witness for the variable $y$, that is,

$\mathfrak{A}_{\mathcal{T}_{\varphi}}\ \models\
\mathbf{e}\subseteq\mathbf{e}_{1}\wedge\textsc{Full}(\mathbf{e}_{1})\wedge\forall
z\,((z\subseteq\mathbf{e}_{1}\wedge\neg\mathbf{e}_{1}\subseteq z)\
\rightarrow\\\ \exists u\,(z\subseteq u\wedge\neg u\subseteq
z\wedge\neg\textsc{Full}(u))\vee\forall v\,((z\subseteq v\wedge\neg v\subseteq
z)\rightarrow\textsc{Pos}(v))).$

In what follows, we show that $\mathbf{e}_{1}(\varphi)=1$, from which we
conclude that $\varphi$ is satisfiable. Fix an arbitrary
$i\in\\{1,\ldots,n\\}$. Then, let $\mathbf{e}_{2}$ be a partial instance of
dimension $n+m$ such that (i) $\mathbf{e}_{2}[i]=\bot$; (ii)
$\mathbf{e}_{2}[j]=1$ for each $j\in\\{1,\ldots,n\\}$ with $j\neq i$, and
(iii) $\mathbf{e}_{2}[n+k]=\mathbf{e}_{1}[n+k]$ for each
$k\in\\{1,\ldots,m\\}$. Then given that
$(\mathbf{e}_{2}\subseteq\mathbf{e}_{1}\wedge\neg\mathbf{e}_{1}\subseteq\mathbf{e}_{2})$,
we have that:

$\mathfrak{A}_{\mathcal{T}_{\varphi}}\ \models\ \exists
u\,(\mathbf{e}_{2}\subseteq u\wedge\neg
u\subseteq\mathbf{e}_{2}\wedge\neg\textsc{Full}(u))\ \vee\\\ \forall
v\,((\mathbf{e}_{2}\subseteq v\wedge\neg
v\subseteq\mathbf{e}_{2})\rightarrow\textsc{Pos}(v)).$

Therefore, given that $\mathbf{e}_{2}$ assigns value $\bot$ to exactly one
feature, we conclude that:

$\displaystyle\mathfrak{A}_{\mathcal{T}_{\varphi}}$ $\displaystyle\models$
$\displaystyle\forall v\,((\mathbf{e}_{2}\subseteq v\wedge\neg
v\subseteq\mathbf{e}_{2})\rightarrow\textsc{Pos}(v)).$ (5)

Define $\mathbf{e}_{3}$ as an instance of dimension $n+m$ such that
$\mathbf{e}_{3}[i]=0$, $\mathbf{e}_{3}[j]=1$ for each $j\in\\{1,\ldots,n\\}$
with $j\neq i$, and $\mathbf{e}_{3}[n+k]=\mathbf{e}_{2}[n+k]$ for each
$k\in\\{1,\ldots,m\\}$. Then, by considering that
$(\mathbf{e}_{2}\subseteq\mathbf{e}_{3}\wedge\neg\mathbf{e}_{3}\subseteq\mathbf{e}_{2})$
holds, we conclude from 5 that $\textsc{Pos}(\mathbf{e}_{3})$ holds.
Therefore, given that $\mathbf{e}_{3}[i]=0$ and $\mathbf{e}_{3}[j]=1$ for each
$j\in\\{1,\ldots,n\\}$ with $j<i$, we have that
$\mathcal{T}_{C_{i}}(\mathbf{e}_{3})=1$, from which we deduce that
$\mathcal{T}_{C_{i}}(\mathbf{e}_{1})=1$, since
$\mathbf{e}_{1}[n+j]=\mathbf{e}_{2}[n+j]=\mathbf{e}_{3}[n+j]$ for every
$j\in\\{1,\ldots,m\\}$. As $i$ is an arbitrary element in the set
$\\{1,\ldots,n\\}$, we conclude that $\mathbf{e}_{1}(C_{i})=1$ for every
$i\in\\{1,\ldots,n\\}$ and, thus, $\mathbf{e}_{1}(\varphi)=1$, which was to be
shown.

  * $(\Rightarrow)$

Assume that $\varphi$ is satisfiable, and let $\sigma$ be a truth assignment
such that $\sigma(\varphi)=1$. Moreover, define an instance $\mathbf{e}_{1}$
of dimension $n+m$ such that $\mathbf{e}_{1}[i]=1$ for each
$i\in\\{1,\ldots,n\\}$ and $\mathbf{e}_{1}[n+j]=\sigma(x_{j})$ for each
$j\in\\{1,\ldots,m\\}$. Then we have that $\mathbf{e}_{1}(\varphi)=1$,
$\mathbf{e}\subseteq\mathbf{e}_{1}$ and $\textsc{Full}(\mathbf{e}_{1})$ hold.
Next we show that:

$\mathfrak{A}_{\mathcal{T}_{\varphi}}\ \models\ \forall
z\,((z\subseteq\mathbf{e}_{1}\wedge\neg\mathbf{e}_{1}\subseteq z)\
\rightarrow\\\ \exists u\,(z\subseteq u\wedge\neg u\subseteq
z\wedge\neg\textsc{Full}(u))\vee\forall v\,((z\subseteq v\wedge\neg v\subseteq
z)\rightarrow\textsc{Pos}(v))),$

from which we conclude that
$\mathfrak{A}_{\mathcal{T}_{\varphi}}\models\psi(\mathbf{e})$. Let
$\mathbf{e}_{2}$ be a partial instance of dimension $n+m$ such that
$(\mathbf{e}_{2}\subseteq\mathbf{e}_{1}\wedge\neg\mathbf{e}_{1}\subseteq\mathbf{e}_{2})$
holds. We need to prove that:

$\mathfrak{A}_{\mathcal{T}_{\varphi}}\ \models\ \exists
u\,(\mathbf{e}_{2}\subseteq u\wedge\neg
u\subseteq\mathbf{e}_{2}\wedge\neg\textsc{Full}(u))\ \vee\\\ \forall
v\,((\mathbf{e}_{2}\subseteq v\wedge\neg
v\subseteq\mathbf{e}_{2})\rightarrow\textsc{Pos}(v)).$

Notice that $\mathbf{e}_{2}$ assigns value $\bot$ to at least one feature in
$X$, since
$(\mathbf{e}_{2}\subseteq\mathbf{e}_{1}\wedge\neg\mathbf{e}_{1}\subseteq\mathbf{e}_{2})$
holds. If $\mathbf{e}_{2}$ assigns value $\bot$ to at least two features, then
clearly $\mathfrak{A}_{\mathcal{T}_{\varphi}}\models\exists
u\,(\mathbf{e}_{2}\subseteq u\wedge\neg
u\subseteq\mathbf{e}_{2}\wedge\neg\textsc{Full}(u))$. Hence, assume that
$\mathbf{e}_{2}$ assigns value $\bot$ to exactly one feature, and consider the
following cases.

    * –

If $\mathbf{e}_{2}[n+j]=\bot$ for some $j\in\\{1,\ldots,m\\}$. Then for every
partial instance $\mathbf{e}_{3}$ of dimension $n+m$ such that
$(\mathbf{e}_{2}\subseteq\mathbf{e}_{3}\wedge\neg\mathbf{e}_{3}\subseteq\mathbf{e}_{2})$
holds, we have that $\mathbf{e}_{3}[i]=1$ for every $i\in\\{1,\ldots,n\\}$.
Therefore, from the definition of $\mathcal{T}_{\varphi}$, we conclude that
$\textsc{Pos}(\mathbf{e}_{3})$ holds. Thus, we have that
$\mathfrak{A}_{\mathcal{T}_{\varphi}}\models\forall
v\,((\mathbf{e}_{2}\subseteq v\wedge\neg
v\subseteq\mathbf{e}_{2})\rightarrow\textsc{Pos}(v))$.

    * –

If $\mathbf{e}_{2}[i]=\bot$ for some $i\in\\{1,\ldots,n\\}$. Then assume that
$\mathbf{e}_{3}$ is a partial instance of dimension $n+m$ such that
$(\mathbf{e}_{2}\subseteq\mathbf{e}_{3}\wedge\neg\mathbf{e}_{3}\subseteq\mathbf{e}_{2})$
holds. If $\mathbf{e}_{3}[i]=1$, then we have that $\mathbf{e}_{3}[j]=1$ for
every $j\in\\{1,\ldots,n\\}$, and we conclude by definition of
$\mathcal{T}_{\varphi}$ that $\textsc{Pos}(\mathbf{e}_{3})$ holds. If
$\mathbf{e}_{3}[i]=0$, then we conclude that
$\mathcal{T}_{\varphi}(\mathbf{e}_{3})=\mathcal{T}_{C_{i}}(\mathbf{e}_{3})$,
since $\mathbf{e}_{3}[j]=1$ for every $j\in\\{1,\ldots,n\\}$ such that $j<i$.
Given that $\mathbf{e}_{1}$, $\mathbf{e}_{2}$ and $\mathbf{e}_{3}$ only differ
in the value of $f_{i}$, we have that
$\mathbf{e}_{3}[n+k]=\mathbf{e}_{2}[n+k]=\mathbf{e}_{1}[n+k]$ for every
$k\in\\{1,\ldots,m\\}$, so that
$\mathcal{T}_{C_{i}}(\mathbf{e}_{3})=\mathcal{T}_{C_{i}}(\mathbf{e}_{1})$. But
then given that $\mathbf{e}_{1}(\varphi)=1$, we know that
$\mathcal{T}_{C_{i}}(\mathbf{e}_{1})=1$, which implies that
$\mathcal{T}_{\varphi}(\mathbf{e}_{3})=\mathcal{T}_{C_{i}}(\mathbf{e}_{3})=\mathcal{T}_{C_{i}}(\mathbf{e}_{1})=1$.
We conclude again that $\textsc{Pos}(\mathbf{e}_{3})$ holds, from which we
deduce that $\mathfrak{A}_{\mathcal{T}_{\varphi}}\models\forall
v\,((\mathbf{e}_{2}\subseteq v\wedge\neg
v\subseteq\mathbf{e}_{2})\rightarrow\textsc{Pos}(v))$.

This concludes the proof of the theorem.

∎

##  Appendix D Proof of Proposition 1

Let us restate and prove the corresponding proposition.

######  Proposition 1.

Let $\varphi$ be a query in $\exists\text{\rm FOIL}$ or $\forall\text{\rm
FOIL}$. Then $\textsc{Eval}(\varphi,\mathsf{DTree})$ and
$\textsc{Eval}(\varphi,\mathsf{OBDD})$ can be solved in polynomial time.

###### Proof.

We will prove this for the more general class of $\mathsf{FBDD}$, that
contains both $\mathsf{DTree}$ and $\mathsf{OBDD}$. Assume that the input
formula is of the form $\varphi=\exists x_{1},\cdots,\exists
x_{k}\psi(x_{1},\ldots,x_{k})$, with $\psi$ quantifier-free, and let
$\mathcal{M}$ be the input model with $\dim(\mathcal{M})=n$. Our algorithm
will try to construct a valuation $\mathbf{e}_{1},\ldots,\mathbf{e}_{k}$ of
the variables of $\varphi$ such that
$\mathcal{M}\models\psi(\mathbf{e}_{1},\ldots,\mathbf{e}_{k})$, and if this
fails, it will be certain that no satisfying valuation exists.

We assume as well the input formula has constants but no free-variables as if
the input instance has free variable we can simply replace them by the partial
instances $\mathbf{e}_{i}$ supplied in the input. Let
$V=\\{{\bm{x}}_{1},\ldots,{\bm{x}}_{k}\\}$ be the variables mentioned in
$\varphi$, of which there is only a constant number as $\varphi$ is fixed. Let
$E=\\{\mathbf{e}_{1},\ldots,\mathbf{e}_{k}\\}$ be their corresponding
undetermined instances.

For each element in the domain of $\mathfrak{A}_{\mathcal{M}}$, that is, for
each tuple in $\\{0,1,\bot\\}^{n}$, we define its _type_ as the set of unary
predicates of $\exists\text{\rm FOIL}$ that it satisfies when interpreted over
$\mathfrak{A}_{\mathcal{M}}$. In the case of $\exists\text{\rm FOIL}$, this
set corresponds either to $\\{\textsc{Pos}\\}$ or to $\\{\neg\textsc{Pos}\\}$,
but we present the general strategy as it can be used for bigger fragments of
FOIL, as shown later in the proof of Theorem 2.

Let $\mathcal{T}$ be the set of types which is of course a fixed set
independent of $\mathcal{M}$. We will guess the type of each instance
$\mathbf{e}\in E$. More formally, we can iterate over all type assignments
$\tau:E\to\mathcal{T}$ as there is only fixed number of them. Similarly, we
can define a _containment assignment_ $\gamma$ as an assignment of all the
ordered pairs $(\mathbf{e}_{i},\mathbf{e}_{j})$ to $\\{0,1\\}$, with the
meaning that $\mathbf{e}_{i}\subseteq\mathbf{e}_{j}$ iff
$\gamma(\mathbf{e}_{i},\mathbf{e}_{j})=1$. Such an assignment is said to be
_possible_ only if it holds the properties of a partial order. Given a
possible containment assignment $\gamma$, we can interpret it as a pair of
sets

$P=\\{(\mathbf{e}_{i},\mathbf{e}_{j})\mid\gamma(\mathbf{e}_{i},\mathbf{e}_{j})=1\\}\quad;\quad
N=\\{(\mathbf{e}_{i},\mathbf{e}_{j})\mid\gamma(\mathbf{e}_{i},\mathbf{e}_{j})=0\\}$

Note as well that there is a constant number of possibilities for the pair
$P,N$. Because the formula $\varphi$ is existential, if there is an
determinization of $E$ that models $\varphi$, then there is a pair
$(\tau,\gamma=(P,N))$ where $\tau$ is a possible type assignment and
$\gamma=(P,N)$ is a possible containment assignment, such that $E$ is
_consistent_ with both $\tau$ and $\gamma$. More precisely, $E$ is consistent
with $\tau$ and $\gamma$ iff:

  * •

For every $\mathbf{e}\in E$ and every unary predicate $\rho$,

$\rho\in\tau(\mathbf{e})\iff\mathbf{e}\in\rho^{\mathfrak{A}_{\mathcal{M}}}$

  * •

For every pair $\mathbf{e}_{i},\mathbf{e}_{j}\in E$,

$\gamma(\mathbf{e}_{i},\mathbf{e}_{j})=1\iff(\mathbf{e}_{i},\mathbf{e}_{j})\in\subseteq^{\mathfrak{A}_{\mathcal{M}}}$

We can afford to iterate over the constantly many pairs $(\tau,\gamma)$, and
for each pair $(\tau,\gamma)$ it is trivial to decide whether $\varphi$ gets
satisfied under said assignments (simply by replacing every atomic term in
$\varphi$ by the value assigned to it by $\tau$ or $\gamma$). Therefore, in
order to prove the whole theorem, it is enough to design a polynomial time
algorithm that decides whether there determinization of $E$ that is a
consistent with a given pair $(\tau,\gamma)$. More precisely, proving the next
claim will be enough to conclude our proof.

######  Claim 1.

Given a pair $(\tau,\gamma=(P,N))$, one can check in polynomial time whether
there is a determinization of $E$ that is consistent with $(\tau,\gamma)$.

###### Proof of Claim 1.

First, as the desired determinization $E$ must be consistent with $N$, it must
hold that for every fact $(\mathbf{e}_{i},\mathbf{e}_{j})\in N$, there is an
index $1\leq k\leq n$ such that $\mathbf{e}_{i}[k]\neq\bot$ and
$\mathbf{e}_{i}[k]\neq\mathbf{e}_{j}[k]$. We can afford to guess, for each of
the constantly many facts $(\mathbf{e}_{i},\mathbf{e}_{j})\in N$, an index $k$
and the values of $\mathbf{e}_{i}[k],\mathbf{e}_{j}[k]$, that certify the
fact. After said guesses have been made, we can assume a set $F$ of guessed
facts of the form $\mathbf{e}[k]=\alpha$, with $\alpha\in\\{0,1,\bot\\}$.
Then, for every fact in $F$ of the form $\mathbf{e}[k]=\beta$, with
$\beta\in\\{0,1\\}$, we include in $F$ all facts of the form
$\mathbf{e}^{\prime}[k]=\beta$ for every $\mathbf{e}^{\prime}$ such that
$(\mathbf{e},\mathbf{e}^{\prime})\in P$. Also, for every fact in $F$ of the
form $\mathbf{e}[k]=\bot$, we include $\mathbf{e}^{\prime}[k]=\bot$ for every
$\mathbf{e}^{\prime}$ such that $(\mathbf{e}^{\prime},\mathbf{e})\in P$. As
any determinization of $E$ respecting $F$ will at least be consistent with
$N$, it remains only to check whether there is an interpretation $E$
respecting to $F$ that is consistent with $\tau$ and $P$.

If $F$ fully determines some predicates that a certain instance $\mathbf{e}\in
E$ must satisfy, for example because $F$ contains facts
$\mathbf{e}[k]=\beta\in\\{0,1\\}$ for all $1\leq k\leq n$ and thus we know
that $\mathbf{e}$ must be a full instance, we can check whether
$\textsc{Pos}(\mathbf{e})$ and if that holds reject immediately if
$\textsc{Pos}(\mathbf{e})\not\in\tau(\mathbf{e})$. Therefore, we can safely
assume this is not the case, and that $\tau$ is not directly contradicted by
$F$. We thus modify the undetermined instances
$\mathbf{e}_{1},\ldots,\mathbf{e}_{k}$ according to $F$. Let us now interpret
$P$ as a directed acyclic graph $G$ obtained in the following way: (i) create
a node for every instance $\mathbf{e}\in E$, (ii) create an edge
$\mathbf{e}\to\mathbf{e}^{\prime}$ iff $(\mathbf{e},\mathbf{e}^{\prime})\in
P$, (iii) collapse strongly connected components to a single node. Note that,
as strongly connected components before the last step correspond to instances
that must be equal, we can think of them as a single instance, because
forcefully $\tau$ must assign the same to each of them. We can now view our
problem as that of determinizing every node in a DAG $G$, in such a way that
the containment dictated by the graph is satisfied, and so is $\tau$.

If $G$ has multiple connected components (it will only have a constant number
of them), it is easy to see that we can simply make the check for each of them
separately, and return that the instance is positive if every connected
component holds the check. This is because different connected components do
not share instances $\mathbf{e}$, and thus a determinization of a connected
component is always compatible with the determinization of another connected
component. As a consequence, our problem is now even smaller; we need to show
that it is possible to determine in polynomial time if the undetermined
components in each node of a given connected DAG $G$ can be assigned values
that are consistent with given assignments $\tau$ and $P$, assuming the
guessed facts $F$.

We now show a direct simple algorithm for this problem:

  1. 1.

Choose an arbitrary topological ordering $\phi$ of $G$.

  2. 2.

Iterate over the nodes according to $\phi$, and for each node $\mathbf{e}$ do
the next step.

  3. 3.

If $\textsc{Pos}\in\tau(\mathbf{e})$, go to step 4., otherwise go to 5.

  4. 4.

We determinize $\mathbf{e}$ in an arbitrary way that is accepted by
$\mathcal{M}$. This is easily done in polynomial time for FBDDs; it is enough
to prune the edges of the FBDD that contradict a defined feature in
$\mathbf{e}$, and then find any positive leaf of the resulting model. Take
$\mathbf{e}$ to be the next node according to $\phi$ and go back to 3. If
there is no next node, go to 6.

  5. 5.

Assign every undetermined component of $\mathbf{e}$ to $\bot$, as that does
not restrict any future choices while ensuring that
$\textsc{Pos}\not\in\tau(\mathbf{e})$. Take $\mathbf{e}$ to be the next node
according to $\phi$ and go back to 3. If there is no next node, go to 6.

  6. 6.

Now that nodes have no undetermined components, check that every fact dictated
by $\tau$ is true for the values that have been determined. If all the facts
are correctly satisfied, return Yes, otherwise return No.

It is clear that, if the preceding algorithm returns Yes, then it is correct,
as it has a concrete determinization consistent with $\tau$, and it must be
consistent with $P$ as every undetermined component that is assigned $0$ or
$1$ its propagated to the successors in the graph. It only remains to justify
that it is correct when it returns No. Assume, looking for a contradiction,
that the algorithm returns No but there actually exists a determinization $B$
of $E$ that is consistent with $\tau$ and $P$, assuming the guessed facts $F$.
Let $A$ be the determinization that the algorithm tested in step 6, and let
$i$ be the first node according to $\phi$, the choice of the algorithm in step
1, such that $A(\phi_{i})\neq B(\phi_{i})$. Such an index must exists because
$A$ must differ from $B$. Among all determinizations that are consistent with
$\tau$ and $P$, let $B^{\prime}$ be the one that maximizes the index $i$ of
its first difference with $A$. Then, let $\mathbf{e}$ be $i$-th node according
to $\phi$, and thus the first node where $A$ and $B^{\prime}$ differ. If
$\textsc{Pos}\in\tau(\mathbf{e})$, the algorithm determinized $\mathbf{e}$ in
an arbitrary way that makes $\mathbf{e}$ a positive instance. But then, as
$\mathbf{e}$ is positive (and therefore a full instance), it cannot have any
successors in $G$, and thus if we let $B^{\prime\prime}\coloneqq B^{\prime}$
except for $B^{\prime\prime}(\mathbf{e})\coloneqq A(\mathbf{e})$, then
$B^{\prime\prime}$ must also be consistent with $\tau$, which contradicts the
maximality of $i$. If $\textsc{Pos}\not\in\tau(\mathbf{e})$ we have two cases,
either $B^{\prime}(\mathbf{e})$ is a full instance or not. If it is, then
again it has no successors in $G$, so it must be that the inconsistency is
that the algorithm determinized $\mathbf{e}$ in a way that makes it a positive
instance. This is clearly not possible, as the only step in the algorithm that
introduces values different from $\bot$, and thus that makes feasible for
$\mathbf{e}$ to be a positive instance, is step 4, which occurs exactly when
$\textsc{Pos}\in\tau(\mathbf{e})$. It remains to see the case where
$B^{\prime}(\mathbf{e})$ is not a full instance. Assume $j$ is the first
component for which $A(\mathbf{e})[j]\neq B^{\prime}(\mathbf{e})[j]$. If
$A(\mathbf{e})[j]=\bot$, then note that every successor of
$B^{\prime}(\mathbf{e})$ is also a successor of $A(\mathbf{e})$ and thus if
$B^{\prime}(\mathbf{e})$ is consistent with $\tau$, then so is
$A(\mathbf{e})$. This implies the inconsistency in $\tau$ must appear later in
$\phi$, and thus we can again take $B^{\prime\prime}$ equal to $B^{\prime}$
except for $B^{\prime\prime}(\mathbf{e})\coloneqq A(\mathbf{e})$ which will
contradict the maximality of $i$. If $A(\mathbf{e})[j]\neq\bot$, then said
value need to come from $F$, as the algorithm only introduces the value $\bot$
for instances where $\textsc{Pos}\not\in\tau(\mathbf{e})$, which means that
$B^{\prime}(\mathbf{e})[j]=A(\mathbf{e})[j]$, as $B^{\prime}$ must also
respect $F$, which contradicts the minimality of $j$.

∎

As the preceding claim has been proved, and there are constantly many pairs
$(\tau,\gamma)$ to consider, there is a polynomial time algorithm for the
whole problem. ∎

##  Appendix E Proof of Theorem 2, Proposition 2 and Proposition 3

Before the proofs, let us gain a better understanding on the PartialAllPos and
PartialAllNeg formulas. Recall that

$\textsc{PartialAllPos}(x,y,z)\ =\ \exists u\,[x\subseteq
u\wedge\textsc{AllPos}(u)\ \wedge\\\ \exists v\,(y\subseteq v\wedge u\subseteq
v)\wedge\exists w\,(z\subseteq w\wedge u\subseteq w)]$ (6)

We will prove that this query captures an important computational problem. Let
us introduce a fourth kind of value: $\diamondsuit$, so we now define
_undetermined instances_ as tuples in $\\{0,1,\bot,\diamondsuit\\}^{n}$ for
some $n\geq 1$. A component with value $\diamondsuit$ is said to be
_undetermined_. Given an undetermined instance $\mathbf{e}$ of dimension $n$,
we say that a partial instance $\mathbf{e}^{\prime}$ of dimension $n$ is a
_determinization_ of $\mathbf{e}$ if for $\mathbf{e}$ matches
$\mathbf{e}^{\prime}$ in every component that is not undetermined. Note that
$\mathbf{e}$ cannot have undetermined components as it is a partial instance
(i.e., a tuple in $\\{0,1,\bot\\}^{n}$).

Consider now the following computational problem:

Problem: DeterminizationAllPos$(\mathcal{C})$ Input: A model
$\mathcal{M}\in\mathcal{C}$ of dimension $n$, and an undetermined instance
$\mathbf{e}$ of dimension $n$ Output: Yes, if there is a determinization
$\mathbf{e}^{\prime}$ of $\mathbf{e}$ such that all completions of
$\mathbf{e}^{\prime}$ are positive, and No otherwise

It turns out that DeterminizationAllPos is intimately related to
PartialAllPos:

######  Lemma 1.

Let $\mathcal{C}$ be any class of models. Then
$\textsc{Eval}(\textsc{PartialAllPos},\mathcal{C})$ can be solved in
polynomial time if and only if $\textsc{DeterminizationAllPos}(\mathcal{C})$
can also be solved in polynomial time.

###### Proof.

We prove both directions as separate claims for an arbitrary class of models
$\mathcal{C}$.

######  Claim 2.

If $\textsc{Eval}(\textsc{PartialAllPos},\mathcal{C})$ can be solved in
polynomial time then $\textsc{DeterminizationAllPos}(\mathcal{C})$ can also be
solved in polynomial time.

###### Proof.

Assume that $\textsc{Eval}(\textsc{PartialAllPos},\mathcal{C})$ can be solved
in polynomial time for $\mathcal{C}$. Then, consider an instance
$(\mathcal{M},\mathbf{e})$ of DeterminizationAllPos, and let $n$ be the
dimension of said instance. From $\mathbf{e}$, we build three partial
instances $\mathbf{e}_{x},\mathbf{e}_{y},\mathbf{e}_{z}$ in the following way:

  * •

$\mathbf{e}_{x}$ is a determinization of $\mathbf{e}$ such that every
undetermined component of $\mathbf{e}$ is replaced by $\bot$ in
$\mathbf{e}_{x}$.

  * •

$\mathbf{e}_{y}$ is a partial instance that has a $1$ in every component where
$\mathbf{e}$ has $\bot$, and $\bot$ in every other component.

  * •

$\mathbf{e}_{z}$ is a partial instance that has a $0$ in every component where
$\mathbf{e}$ has $\bot$, and $\bot$ in every other component.

We now claim that
$\mathcal{M}\models\textsc{PartialAllPos}(\mathbf{e}_{x},\mathbf{e}_{y},\mathbf{e}_{z})$
if and only if $(\mathcal{M},\mathbf{e})$ is a positive instance of
DeterminizationAllPos.

Indeed, assume first that
$\mathcal{M}\models\textsc{PartialAllPos}(\mathbf{e}_{x},\mathbf{e}_{y},\mathbf{e}_{z})$,
and let be $\mathbf{e}_{u},\mathbf{e}_{v},\mathbf{e}_{w}$ be their witnesses.
Trivially, $\mathbf{e}_{u}$ is a partial instance for which every completion
is positive. Note that because
$\mathcal{M}\models\mathbf{e}_{x}\subseteq\mathbf{e}_{u}$ and the definition
of $\mathbf{e}_{x}$, we have that the defined components of $\mathbf{e}_{u}$
and $\mathbf{e}$ match. It only remains to see that if $\mathbf{e}[i]=\bot$
for some $1\leq i\leq n$, then $\mathbf{e}_{u}[i]=\bot$ as well. Assume to the
contrary that for some $i$ it happens that $\mathbf{e}[i]=\bot$ but
$\mathbf{e}_{u}[i]\neq\bot$. If $\mathbf{e}_{u}[i]=0$, then
$\mathbf{e}_{v}[i]=0$, as
$\mathcal{M}\models\mathbf{e}_{u}\subseteq\mathbf{e}_{v}$. But
$\mathbf{e}_{v}[i]=0$ contradicts the fact that $\mathbf{e}_{y}[i]=1$ (by
construction) as $\mathcal{M}\models\mathbf{e}_{y}\subseteq\mathbf{e}_{v}$.
Similarly, if $\mathbf{e}_{u}[i]=1$, then $\mathbf{e}_{w}[i]=1$, as
$\mathcal{M}\models\mathbf{e}_{u}\subseteq\mathbf{e}_{w}$. But
$\mathbf{e}_{w}[i]=1$ contradicts the fact that $\mathbf{e}_{z}[i]=0$ (by
construction) as $\mathcal{M}\models\mathbf{e}_{z}\subseteq\mathbf{e}_{w}$.

For the other direction, assume $(\mathcal{M},\mathbf{e})$ is a positive
instance of DeterminizationAllPos, and let $\mathbf{e}^{\prime}$ be the
determinization of $\mathbf{e}$ that serves as a witness. We claim that
$\mathbf{e}_{u}\coloneqq\mathbf{e}^{\prime}$ is a witness for
$\mathcal{M}\models\textsc{PartialAllPos}(\mathbf{e}_{x},\mathbf{e}_{y},\mathbf{e}_{z})$.
Indeed, it is trivial that
$\mathcal{M}\models\mathbf{e}_{x}\subseteq\mathbf{e}_{u}$ as both
$\mathbf{e}_{x}$ and $\mathbf{e}_{u}$ are determinization of $\mathbf{e}$, but
$\mathbf{e}_{x}$ replaced undetermined components by $\bot$. It is also clear
that $\mathcal{M}\models\textsc{AllPos}(\mathbf{e}_{u})$, as all completions
of $\mathbf{e}^{\prime}$ are positive by definition. Then, let
$\mathbf{e}_{v}$ be the completion of $\mathbf{e}_{u}$ that replaces every
$\bot$ component of $\mathbf{e}_{u}$ with $1$. Let $\mathbf{e}_{w}$ be defined
analogously but replacing $\bot$ with $0$. It is then easy to check that

$\mathcal{M}\models(\mathbf{e}_{y}\subseteq\mathbf{e}_{v}\wedge\mathbf{e}_{u}\subseteq\mathbf{e}_{v})\wedge(\mathbf{e}_{z}\subseteq\mathbf{e}_{w}\wedge\mathbf{e}_{u}\subseteq\mathbf{e}_{w})$

and thus
$\mathcal{M}\models\textsc{PartialAllPos}(\mathbf{e}_{x},\mathbf{e}_{y},\mathbf{e}_{z})$,
which is enough to conclude the proof. ∎

######  Claim 3.

If $\textsc{DeterminizationAllPos}(\mathcal{C})$ can be solved in polynomial
time then $\textsc{Eval}(\textsc{PartialAllPos},\mathcal{C})$ can also be
solved in polynomial time.

###### Proof.

Assume that $\textsc{DeterminizationAllPos}(\mathcal{C})$ can be solved in
polynomial time. Then, let
$(\mathcal{M},\mathbf{e}_{x},\mathbf{e}_{y},\mathbf{e}_{z})$ be an input of
$\textsc{Eval}(\textsc{PartialAllPos},\mathcal{C})$, and let
$n=\dim(\mathcal{M})$.

First, we claim that if for some $1\leq i\leq n$ it happens that
$\mathbf{e}_{y}[i]\neq\bot\neq\mathbf{e}_{x}[i]$ or
$\mathbf{e}_{z}[i]\neq\bot\neq\mathbf{e}_{x}[i]$, then we can trivially deduce
that $(\mathcal{M},\mathbf{e}_{x},\mathbf{e}_{y},\mathbf{e}_{z})$ is a
negative instance of $\textsc{Eval}(\textsc{PartialAllPos},\mathcal{C})$.
Indeed, if $\mathbf{e}_{y}[i]\neq\bot$, and
$(\mathcal{M},\mathbf{e}_{x},\mathbf{e}_{y},\mathbf{e}_{z})$ were to be a
positive instance, then there would exists witnesses
$\mathbf{e}_{u},\mathbf{e}_{v},\mathbf{e}_{w}$, which would hold the following
properties:

  1. 1.

$\mathbf{e}_{u}[i]=\mathbf{e}_{x}[i]$, as
$\mathcal{M}\models\mathbf{e}_{x}\subseteq\mathbf{e}_{u}$ and
$\mathbf{e}_{x}[i]$ is assumed to not be $\bot$.

  2. 2.

$\mathbf{e}_{v}[i]=\mathbf{e}_{y}[i]$, as
$\mathcal{M}\models\mathbf{e}_{y}\subseteq\mathbf{e}_{v}$ if
$\mathbf{e}_{y}[i]\neq\bot$.

  3. 3.

$\mathbf{e}_{w}[i]=\mathbf{e}_{z}[i]$, as
$\mathcal{M}\models\mathbf{e}_{z}\subseteq\mathbf{e}_{w}$ if
$\mathbf{e}_{z}[i]\neq\bot$.

  4. 4.

$\mathbf{e}_{v}[i]=\mathbf{e}_{u}[i]$, as
$\mathcal{M}\models\mathbf{e}_{u}\subseteq\mathbf{e}_{v}$ and
$\mathbf{e}_{u}[i]=\mathbf{e}_{x}[i]$ is assumed to not be $\bot$.

  5. 5.

$\mathbf{e}_{w}[i]=\mathbf{e}_{u}[i]$, as
$\mathcal{M}\models\mathbf{e}_{u}\subseteq\mathbf{e}_{w}$ and
$\mathbf{e}_{u}[i]=\mathbf{e}_{x}[i]$ is assumed to not be $\bot$.

Transitively, it would follow if $\mathbf{e}_{y}[i]\neq\bot$, then
$\mathbf{e}_{x}[i]=\mathbf{e}_{y}[i]$, and if $\mathbf{e}_{z}[i]\neq\bot$,
then $\mathbf{e}_{x}[i]=\mathbf{e}_{z}[i]$, which contradicts the assumption.

Therefore, we can safely assume from now on that, if
$\mathbf{e}_{x}[i]\neq\bot$, then either $\mathbf{e}_{y}[i]=\bot$ or
$\mathbf{e}_{y}[i]=\mathbf{e}_{x}[i]$, and the same holds for
$\mathbf{e}_{z}[i]$. We now define $\mathbf{e}$ as an undetermined instance
that is equal to $\mathbf{e}_{x}$ except that it has $\diamondsuit$ in every
component where $\mathbf{e}_{x}$ has $\bot$. We now claim that
$(\mathcal{M},\mathbf{e}_{x},\mathbf{e}_{y},\mathbf{e}_{z})$ is a positive
instance of $\textsc{Eval}(\textsc{PartialAllPos},\mathcal{C})$ if and only if
$(\mathcal{M},\mathbf{e})$ is a positive instance of DeterminizationAllPos.

Indeed, assume that
$(\mathcal{M},\mathbf{e}_{x},\mathbf{e}_{y},\mathbf{e}_{z})$ is a positive
instance of $\textsc{Eval}(\textsc{PartialAllPos},\mathcal{C})$. Then, it is
trivial that its witness $\mathbf{e}_{u}$ is a determinization of $\mathbf{e}$
with only positive completions. For the other direction, if
$(\mathcal{M},\mathbf{e})$ is a positive instance of DeterminizationAllPos
with witness $\mathbf{e}^{\prime}$, then it is easy to see that taking
$\mathbf{e}_{u}\coloneqq\mathbf{e}_{v}\coloneqq\mathbf{e}_{w}\coloneqq\mathbf{e}^{\prime}$
proves that $(\mathcal{M},\mathbf{e}_{x},\mathbf{e}_{y},\mathbf{e}_{z})$ is a
positive instance of $\textsc{Eval}(\textsc{PartialAllPos},\mathcal{C})$, as
clearly
$\mathcal{M}\models\mathbf{e}_{x}\subseteq\mathbf{e}_{u}\land\textsc{AllPos}(\mathbf{e}_{u})$
and also trivially
$\mathcal{M}\models\mathbf{e}_{u}\subseteq\mathbf{e}_{v}\land\mathbf{e}_{u}\subseteq\mathbf{e}_{w}$,
thus leaving only
$\mathcal{M}\models\mathbf{e}_{y}\subseteq\mathbf{e}_{v}\land\mathbf{e}_{z}\subseteq\mathbf{e}_{w}$
to justify, which we do simply by using the previous fact that if
$\mathbf{e}_{y}[i]\neq\bot$ for some $i$,
$\mathbf{e}_{x}[i]=\mathbf{e}_{y}[i]$, from which we know that
$\mathbf{e}_{v}[i]=\mathbf{e}_{y}[i]$,as
$\mathcal{M}\models\mathbf{e}_{x}\subseteq\mathbf{e}_{u}\subseteq\mathbf{e}_{v}$.
The same reasoning justifies that
$\mathcal{M}\models\mathbf{e}_{z}\subseteq\mathbf{e}_{w}$

∎

The lemma follows directly from the combination of both claims. ∎

It is easy to see that the same proof applies to PartialAllNeg and
DeterminizationAllNeg. We now restate the main theorem of this section and
proceed to prove it.

######  Theorem 2.

For every class $\mathcal{C}$ of models, the following conditions are
equivalent: (a) $\textsc{Eval}(\varphi,\mathcal{C})$ can be solved in
polynomial time for each query $\varphi$ in $\exists\text{\rm FOIL}^{+}$; (b)
$\textsc{Eval}(\textsc{PartialAllPos},\mathcal{C})$ and
$\textsc{Eval}(\textsc{PartialAllNeg},\mathcal{C})$ can be solved in
polynomial time.

###### Proof.

The fact that $(a)$ implies $(b)$ is trivial as PartialAllPos and
PartialAllNeg can be written in $\exists\text{\rm FOIL}^{+}$ as shown in the
body of the paper. It remains to prove that $(b)$ implies $(a)$. The proof is
an extension of the proof of Proposition 1. As it is again constructive and
technical, let us first present a sketch. We assume unary predicates
$\textsc{ExistsNeg},\textsc{ExistsPos}$, that trivially allow for expressing
AllPos and AllNeg.

#### Sketch of proof

Assume that the input formula is of the form $\varphi=\exists
x_{1},\cdots,\exists x_{k}\psi(x_{1},\ldots,x_{k})$, with $\psi$ quantifier-
free, and let $\mathcal{M}$ be the input model with $\dim(\mathcal{M})=n$. Our
algorithm will try to construct a valuation
$\mathbf{e}_{1},\ldots,\mathbf{e}_{k}$ of the variables of $\varphi$ such that
$\mathcal{M}\models\psi(\mathbf{e}_{1},\ldots,\mathbf{e}_{k})$, and if this
fails, it will be certain that no satisfying valuation exists. In order to do
so, the algorithm starts taking $\mathbf{e}_{1},\ldots,\mathbf{e}_{k}$ as
undetermined instances, and in particular it starts setting
$\mathbf{e}_{1}=\mathbf{e}_{2}=\cdots=\mathbf{e}_{k}=\diamondsuit^{n}$. Then,
as $k$ is a fixed constant, the algorithm can afford to guess which unary
predicates of $\exists\text{\rm FOIL}^{+}$ will be satisfied by each
$\mathbf{e}_{i}$, and also all the containments
$\mathbf{e}_{i}\subseteq\mathbf{e}_{j}$ that hold. Note that some of such
guesses might be inconsistent, as for example, they could fail to respect the
transitive property of ${\subseteq}$, or guess that an $\mathbf{e}_{i}$ will
hold both Pos and ExistsNeg, which is not possible either. Inconsistent
guesses are simply discarded. As only constantly many guesses exists, the
complicated part of the algorithm is: given a consistent guess, check if it is
possible to determinize all instances $\mathbf{e}_{1}$ through
$\mathbf{e}_{k}$ while respecting the guess. One can show that the complicated
cases are captured by the DeterminizationAllPos and DeterminizationAllNeg
problems, which because of Lemma 1 are solvable in polynomial time given
condition $(b)$.

We assume as well the input formula has no free-variables, as it complicates
the exposition without adding combinatorial insight. Let
$V=\\{{\bm{x}}_{1},\ldots,{\bm{x}}_{k}\\}$ be the variables mentioned in
$\varphi$, of which there is only a constant number as $\varphi$ is fixed. Let
$E=\\{\mathbf{e}_{1},\ldots,\mathbf{e}_{k}\\}$ be their corresponding
undetermined instances, as the proof sketch suggests. Also, let $\mathcal{M}$
be the input model, and let $n=\dim(\mathcal{M})$. For each element in the
domain of $\mathfrak{A}_{\mathcal{M}}$, that is, for each tuple in
$\\{0,1,\bot\\}^{n}$, we define its _type_ as the set of unary predicates of
$\exists\text{\rm FOIL}^{+}$ that it satisfies when interpreted over
$\mathfrak{A}_{\mathcal{M}}$. Note that not all sets of unary predicates are
possible types, as for example no tuple can satisfy the set
$\\{\textsc{Pos},\textsc{ExistsNeg}\\}$. Let $\mathcal{T}$ be the set of types
that are possible, which is of course a fixed set independent of
$\mathcal{M}$. We will guess the type of each instance $\mathbf{e}\in E$. More
formally, we can iterate over all type assignments $\tau:E\to\mathcal{T}$ as
there is only fixed number of them. Similarly, we can define a _containment
assignment_ $\gamma$ as an assignment of all the ordered pairs
$(\mathbf{e}_{i},\mathbf{e}_{j})$ to $\\{0,1\\}$, with the meaning that
$\mathbf{e}_{i}\subseteq\mathbf{e}_{j}$ iff
$\gamma(\mathbf{e}_{i},\mathbf{e}_{j})=1$. Such an assignment is said to be
_possible_ only if it holds the properties of a partial order. Given a
possible containment assignment $\gamma$, we can interpret it as a pair of
sets

$P=\\{(\mathbf{e}_{i},\mathbf{e}_{j})\mid\gamma(\mathbf{e}_{i},\mathbf{e}_{j})=1\\}\quad;\quad
N=\\{(\mathbf{e}_{i},\mathbf{e}_{j})\mid\gamma(\mathbf{e}_{i},\mathbf{e}_{j})=0\\}$

Note as well that there is a constant number of possibilities for the pair
$P,N$. Because the formula $\varphi$ is existential, if there is an
determinization of $E$ that models $\varphi$, then there is a pair
$(\tau,\gamma=(P,N))$ where $\tau$ is a possible type assignment and
$\gamma=(P,N)$ is a possible containment assignment, such that $E$ is
_consistent_ with both $\tau$ and $\gamma$. More precisely, $E$ is consistent
with $\tau$ and $\gamma$ iff:

  * •

For every $\mathbf{e}\in E$ and every unary predicate $\rho$,

$\rho\in\tau(\mathbf{e})\iff\mathbf{e}\in\rho^{\mathfrak{A}_{\mathcal{M}}}$

  * •

For every pair $\mathbf{e}_{i},\mathbf{e}_{j}\in E$,

$\gamma(\mathbf{e}_{i},\mathbf{e}_{j})=1\iff(\mathbf{e}_{i},\mathbf{e}_{j})\in\subseteq^{\mathfrak{A}_{\mathcal{M}}}$

We can afford to iterate over the constantly many pairs $(\tau,\gamma)$, and
for each pair $(\tau,\gamma)$ it is trivial to decide whether $\varphi$ gets
satisfied under said assignments (simply by replacing every atomic term in
$\varphi$ by the value assigned to it by $\tau$ or $\gamma$). Therefore, in
order to prove the whole theorem, it is enough to design a polynomial time
algorithm that decides whether there determinization of $E$ that is a
consistent with a given pair $(\tau,\gamma)$. More precisely, proving the next
claim will be enough to conclude our proof.

######  Claim 4.

Given a pair $(\tau,\gamma=(P,N))$, one can check in polynomial time whether
there is a determinization of $E$ that is consistent with $(\tau,\gamma)$.

###### Proof.

First, as the desired determinization $E$ must be consistent with $N$, it must
hold that for every fact $(\mathbf{e}_{i},\mathbf{e}_{j})\in N$, there is an
index $1\leq k\leq n$ such that $\mathbf{e}_{i}[k]\neq\bot$ and
$\mathbf{e}_{i}[k]\neq\mathbf{e}_{j}[k]$. We can afford to guess, for each of
the constantly many facts $(\mathbf{e}_{i},\mathbf{e}_{j})\in N$, an index $k$
and the values of $\mathbf{e}_{i}[k],\mathbf{e}_{j}[k]$, that certify the
fact. Also, for every $\textsc{Full}\not\in\tau(\mathbf{e})$, we can guess a
component $\mathbf{e}[k]=\bot$. After said guesses have been made, we can
assume a set $F$ of guessed facts of the form $\mathbf{e}[k]=\alpha$, with
$\alpha\in\\{0,1,\bot\\}$. Then, for every fact in $F$ of the form
$\mathbf{e}[k]=\beta$, with $\beta\in\\{0,1\\}$, we include in $F$ all facts
of the form $\mathbf{e}^{\prime}[k]=\beta$ for every $\mathbf{e}^{\prime}$
such that $(\mathbf{e},\mathbf{e}^{\prime})\in P$. Also, for every fact in $F$
of the form $\mathbf{e}[k]=\bot$, we include $\mathbf{e}^{\prime}[k]=\bot$ for
every $\mathbf{e}^{\prime}$ such that $(\mathbf{e}^{\prime},\mathbf{e})\in P$.
As any determinization of $E$ respecting $F$ will at least be consistent with
$N$, it remains only to check whether there is an interpretation $E$
respecting to $F$ that is consistent with $\tau$ and $P$.

If $F$ fully determines some predicates that a certain instance $\mathbf{e}\in
E$ must satisfy, for example because $F$ contains facts
$\mathbf{e}[k]=\beta\in\\{0,1\\}$ for all $1\leq k\leq n$ and thus we know
that $\mathbf{e}$ must be a full instance, we can reject immediately if
$\textsc{Full}\not\in\tau(\mathbf{e})$. Therefore, we can safely assume this
is not the case, and that $\tau$ is not directly contradicted by $F$. Let us
now interpret $P$ as a directed acyclic graph $G$ obtained in the following
way: (i) create a node for every instance $\mathbf{e}\in E$, (ii) create an
edge $\mathbf{e}\to\mathbf{e}^{\prime}$ iff
$(\mathbf{e},\mathbf{e}^{\prime})\in P$, (iii) collapse strongly connected
components to a single node. Note that, as strongly connected components
before the last step correspond to instances that must be equal, we can think
of them as a single instance, because forcefully $\tau$ must assign the same
to each of them. We can now view our problem as that of determinizing every
node in a DAG $G$, in such a way that the containment dictated by the graph is
satisfied, and so is $\tau$.

If $G$ has multiple connected components (it will only have a constant number
of them), it is easy to see that we can simply make the check for each of them
separately, and return that the instance is positive if every connected
component holds the check. This is because different connected components do
not share instances $\mathbf{e}$, and thus a determinization of a connected
component is always compatible with the determinization of another connected
component. As a consequence, our problem is now even smaller; we need to show
that it is possible to determine in polynomial time if the undetermined
components in each node of a given connected DAG $G$ can be assigned values
that are consistent with given assignments $\tau$ and $P$.

We now show a direct simple algorithm for this problem:

  1. 1.

Choose an arbitrary topological ordering $\phi$ of $G$.

  2. 2.

Iterate over the nodes according to $\phi$, and for each node $\mathbf{e}$ do
the next step.

  3. 3.

If $\textsc{Full}\in\tau(\mathbf{e})$, go to step 4., otherwise go to 5.

  4. 4.

We either have $\textsc{Pos}\in\tau(\mathbf{e})$ or
$\textsc{ExistsNeg}\in\tau(\mathbf{e})$, but not both. On the first case,
solve the DeterminizationAllPos problem with input $(\mathcal{M},\mathbf{e})$
and determinize $\mathbf{e}$ accordingly. On the second case, solve the
DeterminizationAllNeg problem. Take $\mathbf{e}$ to be the next node according
to $\phi$ and go back to 3. If there is no next node, go to 6.

  5. 5.

We either have $\textsc{ExistsPos}\in\tau(\mathbf{e})$ or
$\textsc{ExistsNeg}\in\tau(\mathbf{e})$, or both. If both, assign every
undetermined component of $\mathbf{e}$ to $\bot$, as that only gives more room
for completions of $\mathbf{e}$ to be both positive and negative. If only
$\textsc{ExistsPos}\in\tau(\mathbf{e})$, solve the DeterminizationAllPos
problem with input $(\mathcal{M},\mathbf{e})$. If only
$\textsc{ExistsNeg}\in\tau(\mathbf{e})$, solve the DeterminizationAllNeg
problem. Then, propagate each value 0 or 1 that was assigned to an
undetermined component of $\mathbf{e}$ to its successors in $G$. Take
$\mathbf{e}$ to be the next node according to $\phi$ and go back to 3. If
there is no next node, go to 6.

  6. 6.

Now that nodes have no undetermined components, check that every fact dictated
by $\tau$ is true for the values that have been determined. If all the facts
are correctly satisfied, return Yes, otherwise return No.

It is clear that, if the preceding algorithm returns Yes, then it is correct,
as it has a concrete determinization consistent with $\tau$, and it must be
consistent with $P$ as every undetermined component that is assigned $0$ or
$1$ its propagated to the successors in the graph. It only remains to justify
that it is correct when it returns No. Assume, looking for a contradiction,
that the algorithm returns No but there actually exists a determinization $B$
of $E$ that is consistent with $\tau$ and $P$. Let $A$ be the determinization
that the algorithm tested in step 6, and let $i$ be the first node according
to $\phi$, the choice of the algorithm in step 1, such that $A(\phi_{i})\neq
B(\phi_{i})$. Such an index must exists because $A$ must differ from $B$.
Among all determinizations that are consistent with $\tau$ and $P$, let
$B^{\prime}$ be the one that maximizes the index $i$ of its first difference
with $A$. Then, let $\mathbf{e}$ be $i$-th node according to $\phi$, and thus
the first node where $A$ and $B^{\prime}$ differ. If
$\textsc{Full}\in\tau(\mathbf{e})$, then the algorithm determinized
$\mathbf{e}$ according to step 4. If $\textsc{Pos}\in\tau(\mathbf{e})$, the
algorithm determinized $\mathbf{e}$ according to the algorithm for
DeterminizationAllPos, and thus if $B(\mathbf{e})$ is effectively positive,
then $A(\mathbf{e})$ must also be, by Lemma 1 and the theorem hypothesis.
Therefore, the inconsistency between $A$ and $\tau$ is not created by
$A(\mathbf{e})$. But then, as $\mathbf{e}$ is full, it cannot have any
successors in $G$, and thus if we let $B^{\prime\prime}\coloneqq B^{\prime}$
except for $B^{\prime\prime}(\mathbf{e})\coloneqq A(\mathbf{e})$, then
$B^{\prime\prime}$ must also be consistent with $\tau$, which contradicts the
maximality of $i$. The case in which $\textsc{ExistsNeg}\in\tau(\mathbf{e})$
is analogous.

It remains to see the case where $\textsc{Full}\not\in\tau(\mathbf{e})$.
Assume $j$ is the first component for which $A(\mathbf{e})[j]\neq
B^{\prime}(\mathbf{e})[j]$. If $A(\mathbf{e})[j]=\bot$, then it must be the
case that both $\textsc{ExistsPos}\in\tau(\mathbf{e})$ and
$\textsc{ExistsNeg}\in\tau(\mathbf{e})$. Note that every completion of
$B^{\prime}(\mathbf{e})$ is also a completion of $A(\mathbf{e})$ and thus if
$B^{\prime}(\mathbf{e})$ is consistent with $\tau$, then so is
$A(\mathbf{e})$. This implies the inconsistency in $\tau$ must appear later in
$\phi$, and thus we can again take $B^{\prime\prime}$ equal to $B^{\prime}$
except for $B^{\prime\prime}(\mathbf{e})\coloneqq A(\mathbf{e})$ which will
contradict the maximality of $i$.

If $A(\mathbf{e})[j]=1$ or $A(\mathbf{e})[j]=0$, it must be the case that
$\textsc{ExistsPos}\in\tau(\mathbf{e})$ but
$\textsc{ExistsNeg}\not\in\tau(\mathbf{e})$, or vice-versa. This means that
determinizations of $\mathbf{e}$ must have either all positive completions or
all negative completions. Again because of Lemma 1 and the theorem hypothesis,
$A(\mathbf{e})$ must hold AllPos or AllNeg if it was possible to determinize
$\mathbf{e}$ in that way, which is the case because $B(\mathbf{e})$ does so.
Then note that by taking $B^{\prime\prime}$ which is equal to $B^{\prime}$
except that it $B^{\prime\prime}(\mathbf{e}^{\prime})[j]=A(\mathbf{e})[j]$ for
every successor $\mathbf{e}^{\prime}$ of $\mathbf{e}$ (itself included), we
get an assignment that must also be consistent with $\tau$, as
$\textsc{ExistsNeg}\not\in\tau(\mathbf{e})$ implies that ExistsNeg does not
hold for any of the successors of $\mathbf{e}$ either. Moreover, no fact of
the form Full can be broken either, as for every non-full variable we already
included in $F$ a guess of an undefined component for it. Thus
$B^{\prime\prime}$ is consistent with $\tau$, and it either contradicts the
maximality of $i$ or the minimality of $j$. Having explored all possible cases
of failure, we can conclude that the algorithm is correct, and as it is
clearly polynomial, we finish the proof of this claim.

∎

As the preceding claim has been proved, and there are constantly many pairs
$(\tau,\gamma)$ to consider, there is a polynomial time algorithm for the
whole problem.

∎

In order to finish this section, we restate and prove Proposition 2.

######  Proposition 2.

The problems $\textsc{Eval}(\textsc{PartialAllPos},\mathsf{Ptron})$ and
$\textsc{Eval}(\textsc{PartialAllNeg},\mathsf{Ptron})$ can be solved in
polynomial time.

###### Proof.

Based on Lemma 1, it is enough to show that the problems
$\textsc{DeterminizationAllPos}(\mathsf{Ptron})$ and
$\textsc{DeterminizationAllNeg}(\mathsf{Ptron})$ can be solved in polynomial
time. Let us focus on the case of DeterminizationAllPos, as the other case is
analogous. Thus, an input instance consists of a perceptron
$\mathcal{M}=(w,t)$ of dimension $n$, and an undetermined instance
$\mathbf{e}$ of dimension $n$. A polynomial time algorithm follows directly
from the next claim.

######  Claim 5.

$(\mathcal{M},\mathbf{e})$ a Yes instance of
$\textsc{DeterminizationAllPos}(\mathsf{Ptron})$ if and only if the following
equation holds

$\left(\sum_{i,\mathbf{e}[i]\in\\{0,1\\}}w_{i}\mathbf{e}[i]\right)+\left(\sum_{i,\mathbf{e}[i]=\bot}\min(0,w_{i})\right)+\left(\sum_{i,\mathbf{e}[i]=\diamondsuit}\max(0,w_{i})\right)\geq
t$

###### Proof of Claim 4..

For the forward direction, assume $(\mathcal{M},\mathbf{e})$ a Yes instance,
and let $\mathbf{e}^{\prime}$ the determinization of $\mathbf{e}$ such that
all its completions are positive under $\mathcal{M}$. In particular, consider
the completion $\mathbf{e}^{*}$ such that if $\mathbf{e}^{\prime}[i]=\bot$,
then $\mathbf{e}^{*}[i]=\min(0,w_{i})$, and
$\mathbf{e}^{*}[i]=\mathbf{e}^{\prime}[i]$ otherwise. The fact that this
completion is positive means that

$\left(\sum_{i,\mathbf{e}^{\prime}[i]\in\\{0,1\\}}w_{i}\mathbf{e}^{\prime}[i]\right)+\left(\sum_{i,\mathbf{e}^{\prime}[i]=\bot}\min(0,w_{i})\right)\geq
t$

Now, the components in $\mathbf{e}^{\prime}$ can be separated according to
whether they were determined or not in $\mathbf{e}$ already:

$\left(\sum_{i,\mathbf{e}[i]\in\\{0,1\\}}w_{i}\mathbf{e}[i]\right)+\left(\sum_{i,\mathbf{e}[i]=\bot}\min(0,w_{i})\right)\
+\\\
\left(\sum_{i,\mathbf{e}[i]=\diamondsuit,\mathbf{e}^{\prime}[i]\in\\{0,1\\}}w_{i}\mathbf{e}^{\prime}[i]\right)+\left(\sum_{i,\mathbf{e}[i]=\diamondsuit,\mathbf{e}^{\prime}[i]=\bot}\min(0,w_{i})\right)\geq
t$

By noting that $\max(0,w_{i})\geq w_{i}\mathbf{e}^{\prime}[i]$ and
$\max(0,w_{i})\geq\min(0,w_{i})$ we have that

$\left(\sum_{i,\mathbf{e}[i]=\diamondsuit}\max(0,w_{i})\right)\geq\left(\sum_{i,\mathbf{e}[i]=\diamondsuit,\mathbf{e}^{\prime}[i]\in\\{0,1\\}}w_{i}\mathbf{e}^{\prime}[i]\right)+\left(\sum_{i,\mathbf{e}[i]=\diamondsuit,\mathbf{e}^{\prime}[i]=\bot}\min(0,w_{i})\right)$

and thus we conclude simply by combining the three previous equations. For the
backward direction, assume the equation holds, and let define the
determinization $\mathbf{e}^{\star}$ such that

$\mathbf{e}^{\star}[i]\begin{cases}\mathbf{e}[i]&\text{if
}\mathbf{e}[i]\neq\diamondsuit\\\ 1&\text{if }\mathbf{e}[i]=\diamondsuit\text{
and }w_{i}\geq 0\\\ 0&\text{otherwise.}\end{cases}$

Note that this implies that if $e[i]=\diamondsuit$ then
$\mathbf{e}^{\star}[i]w_{i}=\max(0,w_{i})$. Now let $\mathbf{e}^{\prime}$ be
any completion of $\mathbf{e}^{\star}$, and we aim to prove that

$\sum_{i}w_{i}\mathbf{e}^{\prime}[i]\geq t$

By construction, we have that

$\sum_{i}w_{i}\mathbf{e}^{\prime}[i]=\left(\sum_{i,\mathbf{e}[i]\in\\{0,1\\}}w_{i}\mathbf{e}[i]\right)+\left(\sum_{i,\mathbf{e}[i]=\diamondsuit}\max(0,w_{i})\right)+\left(\sum_{i,\mathbf{e}[i]=\bot}w_{i}\mathbf{e}^{\prime}[i]\right)$

But

$\left(\sum_{i,\mathbf{e}[i]=\bot}w_{i}\mathbf{e}^{\prime}[i]\right)\geq\left(\sum_{i,\mathbf{e}[i]=\bot}\min(0,w_{i})\right)$

and thus

$\sum_{i}w_{i}\mathbf{e}^{\prime}[i]\geq\left(\sum_{i,\mathbf{e}[i]\in\\{0,1\\}}w_{i}\mathbf{e}[i]\right)+\left(\sum_{i,\mathbf{e}[i]=\bot}\min(0,w_{i})\right)+\left(\sum_{i,\mathbf{e}[i]=\diamondsuit}\max(0,w_{i})\right)$

which is at least $t$ by hypothesis. Therefore, any completion $e^{\prime}$ is
positive, which concludes the proof. ∎

∎

In order to make the previous result more meaningful, we show explicitly that
the class of perceptrons is not tractable for unrestricted FOIL.

######  Proposition 4.

The problem of deciding whether a model is biased [16], expressible in FOIL
through the formula BiasedModel, is NP-hard for the class of perceptrons.

###### Proof.

In order to show hardness we will reduce from the subset sum problem, which is
well known to be NP-hard. Recall that the subset sum problem consists on,
given natural numbers $s_{1},\ldots,s_{n},k\in\mathbb{N}$, to decide whether
there is a subset $S\subseteq\\{1,\ldots,n\\}$ such that $\sum_{i\in
S}s_{i}=k$. Let us proceed with the reduction. Based on a subset sum instance
$s_{1},\ldots,s_{n},k$, we create a perceptron with $n$ unprotected features
(that we assume to have indices $1$ through $n$) with associated weights
$s_{1},\ldots,s_{n}$ and a single protected feature, with index $n+1$ and
weight $1$. Given the described weights, let $\mathcal{M}$ be the resulting
perceptron that has those weights and bias111Recall that the bias of a
perceptron has nothing to do with the notion of bias that relates to fairness.
$-k-1$. The following claim is enough to establish the reduction.

######  Claim 6.

The perceptron $\mathcal{M}$ is biased if and only if $s_{1},\ldots,s_{n},k$
is a positive instance of the subset sum problem.

For the forward direction, consider $\mathcal{M}$ to be biased. That means
there are instances $\mathbf{e}_{1}$ and $\mathbf{e}_{2}$ such that
$\mathcal{M}(\mathbf{e}_{1})\neq\mathcal{M}(\mathbf{e}_{2})$, that differ only
on the $n+1$-th feature, as it is the only protected one. Assume wlog that
$\mathcal{M}(\mathbf{e}_{1})=1$ and $\mathcal{M}(\mathbf{e}_{2})=0$, by
swapping the variables if it is not already the case. This implies
${\bm{w}}\cdot\mathbf{e}_{1}\geq k+1$ and ${\bm{w}}\cdot\mathbf{e}_{2}<k+1$.
As ${\bm{w}}\cdot\mathbf{e}_{1}\geq{\bm{w}}\cdot\mathbf{e}_{2}$, and
$\mathbf{e}_{1}$ differs from $\mathbf{e}_{2}$ only on the $n+1$-th feature,
it must hold that $\mathbf{e}_{1}[{n+1}]=1$ and $\mathbf{e}_{2}[{n+1}]=0$, as
$w_{n+1}=1$. Let $P$ be the set of unprotected features of $\mathbf{e}_{1}$
(and thus $\mathbf{e}_{2}$) that are set to $1$. Then we can write
${\bm{w}}\cdot\mathbf{e}_{1}=\big{(}\sum_{i\in P}s_{i}\big{)}+1$, as each
weight $w_{i}$ was chosen to be equal to $s_{i}$. Then when considering
$\mathbf{e}_{1}$ we have that $\big{(}\sum_{i\in P}s_{i}\big{)}+1\geq k+1$
and, by considering $\mathbf{e}_{2}$, that $\big{(}\sum_{i\in
P}s_{i}\big{)}<k+1$, from which we deduce that $\sum_{i\in P}s_{i}=k$. We have
found a subset of $\\{s_{1},\ldots,s_{n}\\}$ that adds up to $k$, which is
enough to conclude the forward direction of the proof. For the backward
direction, consider an arbitrary set $P\subseteq\\{1,\ldots,n\\}$ such that
$\sum_{i\in P}s_{i}=k$. It is then easy to verify that the instance
$\mathbf{e}_{1}$ that has a $1$ in every feature whose index belongs to $P$, a
$1$ in the $n+1$-th feature, and $0$ on the rest, is a positive instance of
$\mathcal{M}$. Furthermore, $\mathbf{e}_{2}$ that differs from
$\mathbf{e}_{1}$ only in the $n+1$-th feature can be checked to be a negative
instance. As we have found a pair of instances that differ only on protected
features, and yet have opposite classifications, the model $\mathcal{M}$ must
be biased. ∎

We now restate and prove Proposition 3.

######  Proposition 3.

Let $\mathcal{C}$ be $\mathsf{OBDD}$ or $\mathsf{DTree}$. The problems
$\textsc{Eval}(\textsc{PartialAllPos},\mathcal{C})$ and
$\textsc{Eval}(\textsc{PartialAllNeg},\mathcal{C})$ are NP-hard.

###### Proof.

. It is enough to prove that hardness holds already for the class of ordered
decision trees (i.e., $\mathsf{DTree}\cap\mathsf{OBDD}$). Moreover, based on
Lemma 1, it is enough to show that the problems DeterminizationAllPos and
DeterminizationAllNeg are NP-hard for ordered decision trees. We focus on the
case of DeterminizationAllPos, as the other one is analogous.

We do this by reducing from 3-SAT. Indeed, let $\varphi$ be a formula in 3CNF,
with $m$ clauses and $n$ variables. Let us assume that $m=2^{k}$ for some
integer $k$, as otherwise one can simply add $2^{\lceil\log_{2}m\rceil}-m\in
O(m)$ clauses consisting of new fresh variables. Then, create an ordered
decision tree $\mathcal{T}$ of dimension $k+n$ in the following way:

  * •

The first $k$ features are labeled $a_{1},\ldots,a_{k}$, and then $n$ features
corresponding to the variables of $\varphi$ are labeled $x_{1},\ldots,x_{n}$.
The features in $\mathcal{T}$ are ordered

$a_{1}\preceq a_{2}\preceq\cdots\preceq a_{k}\preceq x_{1}\preceq
x_{2}\preceq\cdots\preceq x_{n}.$

  * •

Start creating $\mathcal{T}$ by building a complete binary ordered tree over
the features $a_{1},\ldots,a_{k}$, where the root has label $a_{1}$, and all
nodes at distance $i$ from the root have label $a_{i+1}$. The last layer of
said tree consists exactly of $2^{k-1}$ nodes labeled $a_{k}$.

  * •

For each clause $C_{i}\quad(1\leq i\leq 2^{k})$ create an ordered (according
to the ordering described above) decision tree $\mathcal{T}_{i}$ equivalent to
said clause. Note that as each clause mentions exactly 3 variables, each of
the $\mathcal{T}_{i}$ can be built in constant time from clause $C_{i}$.

  * •

Let $L$ be the set of $2^{k-1}$ nodes labeled with $a_{k}$ in $\mathcal{T}$.
Let $\ell_{1},\cdots,\ell_{2^{k-1}}$ be any ordering of $L$, and to node
$\ell_{i}$ connect $\mathcal{T}_{2i-1}$ with an edge labeled $0$ and
$\mathcal{T}_{2i}$ with an edge labeled $0$.

Note that this construction can trivially be performed in polynomial time. Now
build an undetermined instance $\mathbf{e}$ of dimension $k+n$, where
$\mathbf{e}[i]=\bot$ for $1\leq i\leq k$ and $\mathbf{e}[i]=\diamondsuit$
otherwise. We claim that there exists a determinization $\mathbf{e}^{\prime}$
of $\mathbf{e}$ such that all its completions are positive, if and only if,
$\varphi$ is satisfiable. Indeed, assume first that such a determinization
$\mathbf{e}^{\prime}$ exists. Then, define $\mathbf{e}^{\prime\prime}$ in the
following way:

$\mathbf{e}^{\prime\prime}[i]=\begin{cases}\mathbf{e}[i]&\text{if
}\mathbf{e}[i]\neq\diamondsuit\\\ \mathbf{e}^{\prime}[i]&\text{if
}\mathbf{e}[i]=\diamondsuit\text{ and }\mathbf{e}^{\prime}[i]\in\\{0,1\\}\\\
0&\text{otherwise.}\end{cases}$

As by construction $\mathbf{e}^{\prime}\subseteq\mathbf{e}^{\prime\prime}$ it
must also hold that all completions of $\mathbf{e}^{\prime\prime}$ are
positive. Moreover, note that $\mathbf{e}^{\prime\prime}[i]=\bot$ for all
$1\leq i\leq k$ and $\mathbf{e}^{\prime\prime}[i]\in\\{0,1\\}$ for all
$k+1\leq i\leq k+n$. We build an $\sigma$ of variables of $\varphi$ based on
$\mathbf{e}^{\prime\prime}$ by setting variable $x_{i}$ to
$\mathbf{e}^{\prime\prime}[k+i]$, for $1\leq i\leq n$. Now, we claim that
$\sigma$ is a satisfying assignment. Indeed, to see that $\sigma$ satisfies
clause $C_{i}$, consider the completion $\mathbf{e}^{*}$ of
$\mathbf{e}^{\prime\prime}$ that sets the features $a_{1},\ldots,a_{k}$ in
such a way that the path of $\mathbf{e}^{*}$ over $\mathcal{T}$ arrives to
$\mathcal{T}_{i}$. As $\mathbf{e}^{*}$ is a positive instance of
$\mathcal{T}$, it must be a positive instance of $\mathcal{T}_{i}$, and thus
by construction $\sigma$ satisfies $C_{i}$.

For the other direction, let $\sigma$ be a satisfying assignment to $\varphi$,
and build the determinization $\mathbf{e}^{\star}$ such that
$\mathbf{e}^{\star}[k+i]=\sigma(x_{i})$ for $1\leq i\leq n$. As $\sigma$
satisfies every clause, $\mathbf{e}^{\star}$ is a positive instance of every
$\mathcal{T}_{i}$, and thus any completion of $\mathbf{e}^{\star}$ is a
positive instance of $\mathcal{T}$. ∎

##  Appendix F Proof of Theorem 3

In order to make the proof more readable, let us first prove a lemma about
simple operations over $k\text{-}\mathsf{COBDD}$s.

######  Lemma 2.

The following operations can be performed in polynomial time:

  * •

(Negation) Given a $k\text{-}\mathsf{COBDD}$ $\mathcal{M}$ of dimension $n$,
compute a $k\text{-}\mathsf{COBDD}$ $\neg\mathcal{M}$ over 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 $k\text{-}\mathsf{COBDD}$s $\mathcal{M}_{1}$ and
$\mathcal{M}_{2}$, of dimension $n$, with a common linear ordering ${<}$ on
the set $\\{1,\ldots,n\\}$ compute a COBDD
$\mathcal{M}\coloneqq\mathcal{M}_{1}\lor\mathcal{M}_{2}$ over the same linear
ordering ${<}$, and width at most $2k$, 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 $k\text{-}\mathsf{COBDD}$s $\mathcal{M}_{1}$ and
$\mathcal{M}_{2}$, of dimension $n$, with a common linear ordering ${<}$ on
the set $\\{1,\ldots,n\\}$ compute a COBDD
$\mathcal{M}\coloneqq\mathcal{M}_{1}\land\mathcal{M}_{2}$ over the same linear
ordering ${<}$, and width at most $2k$, 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.

Negation is trivial, it suffices to interchange the labels $\mathbf{true}$ and
$\mathbf{false}$ in every leaf of $\mathcal{M}$. Disjunction and Conjunction
follow the classical algorithm for OBDDs by Bryant [7], and in what follows we
argue that width is no more than doubled. Let us introduce some notation; the
inductive structure of OBDDs allows us to say that $\mathcal{M}_{1}$ has a
root node labeled with $r\in\\{1,\ldots,n\\}$ connected to OBDDs
$\mathcal{M}_{1}^{0}$ and $\mathcal{M}_{1}^{1}$ by edges labeled with $0$ and
$1$ respectively, which we denote as
$\mathcal{M}_{1}=(r,\mathcal{M}_{1}^{0},\mathcal{M}_{2}^{0})$. Analogously,
let $\mathcal{M}_{2}=(r,\mathcal{M}_{2}^{0},\mathcal{M}_{2}^{1})$, as
$\mathcal{M}_{1}$ and $\mathcal{M}_{2}$ share the ordering ${<}$ and are
complete, their root must have the same label. Then, for
$\mathrm{op}\in\\{\text{Conjunction},\text{Disjunction}\\}$, Bryant’s
algorithm inductively computes operations according to the following equation

$\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})\right).$
(7)

Let us use notation $\mathcal{M}\to j$ for the number of nodes in
$\mathcal{M}$ labeled with $j$. We are now ready to prove a stronger claim by
induction on $n$, the dimension of the models, from which the lemma trivially
follows.

######  Claim 7.

Let $\mathcal{M}_{1}$ and $\mathcal{M}_{2}$ be COBDDs of dimension $n$ with a
common ordering ${<}$, and let $j$ be any label in $\\{1,\ldots,n\\}$. Then
Bryant’s algorithm guarantees that

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

###### Proof of Claim 7.