section[0em]2.9em1pc subsection[0.75em]3.3em1pc 11institutetext: IRIT, CNRS,
Toulouse, France
11email<EMAIL_ADDRESS>
# Logic-Based Explainability in Machine Learning

Joao Marques-Silva  0000-0002-6632-3086

###### Abstract

The last decade witnessed an ever-increasing stream of successes in Machine
Learning (ML). These successes offer clear evidence that ML is bound to become
pervasive in a wide range of practical uses, including many that directly
affect humans. Unfortunately, the operation of the most successful ML models
is incomprehensible for human decision makers. As a result, the use of ML
models, especially in high-risk and safety-critical settings is not without
concern. In recent years, there have been efforts on devising approaches for
explaining ML models. Most of these efforts have focused on so-called model-
agnostic approaches. However, all model-agnostic and related approaches offer
no guarantees of rigor, hence being referred to as non-formal. For example,
such non-formal explanations can be consistent with different predictions,
which renders them useless in practice. This paper overviews the ongoing
research efforts on computing rigorous model-based explanations of ML models;
these being referred to as formal explanations. These efforts encompass a
variety of topics, that include the actual definitions of explanations, the
characterization of the complexity of computing explanations, the currently
best logical encodings for reasoning about different ML models, and also how
to make explanations interpretable for human decision makers, among others.

###### Keywords:

Explainable AI Formal explanations Automated reasoning

###### Table of Contents

  1. 1 Introduction
  2. 2 Preliminaries
    1. 2.1 Logic Foundations
      1. 2.1.1 Propositional Logic & Boolean Satisfiability.
      2. 2.1.2 First Order Logic.
      3. 2.1.3 Encodings & Interfacing Reasoners.
    2. 2.2 Classification Problems
      1. 2.2.1 Examples of Classifiers.
      2. 2.2.2 Running Examples.
    3. 2.3 Non-Formal Explanations
  3. 3 Formal Explainability
    1. 3.1 Abductive Explanations
    2. 3.2 Contrastive Explanations
    3. 3.3 Global Abductive Explanations & Counterexamples
    4. 3.4 Duality Results
    5. 3.5 Additional Notes
    6. 3.6 A Timeline for Formal Explainability
  4. 4 Computing Explanations
    1. 4.1 Progress in Computing Explanations
    2. 4.2 General Oracle-Based Approach
    3. 4.3 Explaining Decision Lists
    4. 4.4 From DLs to DTs & DSs
    5. 4.5 Explaining Neural Networks
    6. 4.6 Other Families of Classifiers
    7. 4.7 An Alternative – Compilation-Based Approaches
  5. 5 Tractable Explanations
    1. 5.1 Decision Trees
    2. 5.2 Monotonic Classifiers
    3. 5.3 Other Families of Classifiers
  6. 6 Explainability Queries
    1. 6.1 Enumeration of Explanations
    2. 6.2 Explanation Membership
    3. 6.3 Additional Explainability Queries
  7. 7 Probabilistic Explanations
    1. 7.1 Problem Formulation
    2. 7.2 Probabilistic Explanations for Decision Trees
    3. 7.3 Additional Results
  8. 8 Input Constraints & Distributions
  9. 9 Formal Explanations with Surrogate Models
  10. 10 Additional Topics & Extensions
  11. 11 Future Research & Conclusions
    1. 11.1 Research Directions
    2. 11.2 Concluding Remarks
      1. Acknowledgements.

##  1 Introduction

Recent years witnessed remarkable advancements in artificial intelligence
(AI), concretely in machine learning (ML) [222, 217, 143, 49]. These
advancements have triggered an ever-increasing range of practical applications
[142]. Some of these applications often impact humans, with credit worthiness
representing one such application, among many others [116]. Unfortunately, the
most promising ML models are inscrutable in their operation, with the term
_black-box_ being often ascribed to such ML models. Black-box ML models cause
distrust, especially when their operation is difficult to understand or it is
even incorrect, not to mention situations where the operation of ML models is
the likely cause for events with disastrous consequences [104, 82, 183], but
also the case of unfairness and bias [292, 334]. (The issues caused by AI
systems are illustrated by an ever-increasing list of incidents [6, 252].)
Moreover, recent work argues [53] that Perrow’s framework of normal accidents
[284] (which has been used to explain the occurrence of catastrophic accidents
in the past) also applies to AI systems, thereby conjecturing that such
(catastrophic) accident(s) in AI systems should be expected in the near
future. Motivated by this state of affairs, but also by recent regulations and
recommendations [115, 156, 277], and by existing proposals of regulation of
AI/ML systems [116, 338, 7], there is a pressing need for building trust into
the operation of ML models. The demand for clarifying the operation of black-
box decision making has motivated the rapid growth of research in the general
theme of _explainable AI_ (XAI). XAI can be viewed as the process of aiding
human decision makers to understand the decisions made by AI/ML systems, with
the purpose of delivering trustworthy AI. The importance of both trustworthy
AI and XAI is illustrated by recent guidelines, recommendations and
regulations put forward by the European Union (EU), the United States
government, the Australian government, the OECD and UNESCO [115, 93, 156, 157,
7, 117, 116, 273, 31, 30, 277, 338], among others. Motivated by the above,
there have been calls for the use of formal methods in the verification of
systems of AI and ML [315], with explainability representing a key component
[242]. There have also been efforts towards developing an understanding of
past incidents in AI systems [251, 252, 361, 360, 285, 253].

Well-known explainability approaches include so-called model-agnostic methods
[301, 235, 302] and, for neural networks, approaches based on variants of
saliency maps [322, 263, 309]. Unfortunately, the most popular XAI approaches
proposed in recent years are marred by lack of rigor, and provide explanations
that are often logically unsound [180, 272, 170]. (One illustrative example is
that of an explanation consistent both with a declined bank loan application
and with an approved bank loan application [242].) The drawbacks of these
(non-formal) XAI approaches raise important concerns in settings that impact
humans. Example settings include those referred to as _high-risk_ and _safety-
critical_ 111The definition of _high-risk_ in this proposal is aligned with
recent EU documentation [116]. Concrete examples include the management and
operation of critical infrastructure, credit worthiness, law enforcement,
among many others [116]. Some authors refer to _high-stakes_ when addressing
related topics [304]. By safety-critical, we take the meaning that is common
in formal methods [211], namely settings where errors are unacceptable, e.g.
where human lives are at risk. There is growing interest in deploying ML-
enabled systems in safety-critical applications (e.g. [91]). . The use of
unsound explainability methods in either high-risk or safety-critical could
evidently have catastrophic consequences. (And there are unfortunately too
many examples of bugs having massive economic cost, or that resulted in the
loss of lives [254, 133, 39, 3, 223, 311].)

A more recent alternative XAI approach offers formal guarantees of rigor, it
is logic-based, and it is in most cases based on efficient automated reasoning
tools. This document offers an overview of the advancements made in the
general field of _formal explainability_ in AI (FXAI).

##### A brief history of FXAI.

The recent work on formal explainability in machine learning finds its roots
in the independent efforts of two research teams [320, 178]222It should be
noted that efforts towards explaining the operation of systems of artificial
intelligence (AI) can be traced back to at least the late 70s [331], with
follow up work since then [332, 317, 313, 128, 111, 118, 283, 14, 16, 15, 119,
308, 175]. Nevertheless, the interest in formalizing explanations is
documented in much earlier work [153]. A distinctive aspect of recent work is
not only the focus on ML models, namely classifiers, but also the research on
novel topics, e.g. contrastive and probabilistic explanations, which we will
define later.. The initial goals of this earlier work seemed clear at the
outset: to propose a formal alternative to the mostly informal approaches to
explainability that were being investigated at the time. Nevertheless, the
experimental results in these initial works also raised concerns about the
practical applicability of formal explanations. However, it soon became clear
that there was much more promise to formal explainability than what the
original works anticipated. Indeed, we claim that it is now apparent that
formal explainability represents an emerging field of research, and one of
crucial importance. A stream of results in recent years amply support this
claim [320, 178, 321, 179, 180, 272, 362, 96, 170, 97, 171, 177, 29, 319, 298,
64, 186, 239, 38, 186, 240, 191, 237, 174, 24, 84, 65, 166, 25, 19, 61, 232,
11, 164, 297, 355, 101, 189, 242, 165, 172, 145, 99, 28, 59, 60, 13, 26, 122,
233, 219, 21, 187, 27, 98, 354, 190, 367, 168, 192, 22, 185, 85, 167, 368,
163, 40, 12]. Among these, several results are significant. It has been shown
that computing one explanation is tractable for a number of classifiers [239,
186, 240, 166, 84, 165, 99, 187]. Different duality results have been obtained
[179, 177], which relate different kinds of explanations. Practically
efficient logic encodings have been devised for computing explanations for a
number of families of classifiers [180, 170, 191, 174, 172, 28]. Compilation
approaches for explainability have been studied in a number of recent works
[320, 321, 96, 97, 101, 99]. A number of computational complexity results,
that cover the computation of one explanation but also other queries, have
been proved [191, 174, 240, 166, 25]. Different explainability queries have
been studied [29, 166, 25]. The size of formal explanations have been
addressed by considering probabilistic explanations [355, 189, 354, 190, 22].
The effect of input constraints on explainability, that restrict the points in
feature space to consider, has been studied in recent works [145, 367]. The
use of surrogate models for computing formal explanations of complex models
has been proposed [65]. Formal explanations have been applied in different
application domains [237]. Furthermore, initial links between explainability
and fairness, robustness and model learning have been uncovered [179, 171].
Given the above, the purpose of this document is to offer an account of what
we feel have been the most important results in this novel field of research,
up until the time of writing.

##### Main goals.

The paper aims to offer a high-level comprehensive overview of the emerging
field of formal explainability. The paper starts by covering existing formal
definitions of explanations. One class of explanations answers a Why?
question; these are referred to as abductive explanations. Another class of
explanations answers a Why not? question; these are referred to as contrastive
explanations. Then, the paper builds on the rigorous definitions of
explanations to study how formal explanations can be computed in practice,
highlighting some of the algorithms used. The paper uses running examples to
illustrate how such explanations are computed in practice. Moreover, the paper
also overviews families of classifiers for which computing one explanation is
tractable. These include decision trees and naive bayes classifiers, among
several others. Furthermore, the paper summarizes recent progress along a
number of lines of research, which aim at making formal explainability a
practical option of choice. Concrete examples of lines of research include: i)
answering a growing number of explainability queries, e.g. enumeration of
explanations; ii) computing probabilistic explanations, which trade-off
explanation size for rigor; iii) taking into account input constraints and
distributions, since not all inputs may be possible for an ML model; and also
iv) approximating complex ML models with simpler models, which are easier to
explain. The paper also overviews a number of additional topics of research in
the general area of formal explainability. Since the paper aims at offering a
broad overview of the field, some more technical aspects are omitted, and left
to the existing references.

##### Additional goals.

This document also takes the opportunity to deconstruct a number of
misconceptions that pervade Machine Learning research. One unfortunately
common misconception is that logic is inadequate for reasoning about ML
models. This paper, but also a growing list of references (see above), offer
ample evidence that this is certainly not the case. For example, formal
explanations for random forests [191] were shown to be more efficient to
compute than those obtained with heuristic methods. Another common
misconception is that computationally hard (e.g. NP-hard,
$\operatorname*{\textnormal{D}^{\textnormal{p}}}$-hard, etc.) problems are
_intractable_ , and so large-scale problems cannot be solved in practice. By
now, there are more than two decades of comprehensive experimental evidence
that attests to the contrary [55, 131]. In many practical settings, automated
reasoners are often (and sometimes most often) remarkably efficient at solving
computationally hard problems of very large scale [342, 343, 131]. Boolean
satisfiability (SAT) solvers (but also mixed integer linear programming (MILP)
solvers) are prime examples of the progress that has been observed in
improving, sometimes dramatically, the practical efficiency of automated
reasoners [55, 81, 57, 58, 212]333It should be clarified that SAT, MILP and
SMT automated reasoners and their variants solve their target problems
_exactly_ , provided such reasoners are given enough time [55, 81, 57, 58,
212]. Nevertheless, these automated reasoners should not be confused with the
burgeoning field of exact exponential and parameterized algorithms [125, 90].
The former, i.e. automated reasoners, are without exception extensively
validated and evaluated in practical settings, being applied to large-scale
problem-solving [55, 81]; regarding the latter, decades of research have
resulted in significant theoretical advances, but these have not been matched
by practical impact.. The bottom line is that some of these computational
problems may be intractable in theory, but in practice that is hardly ever the
case [343, 131]. Another quite common misconception is the existence of so-
called interpretable models, e.g. decision trees, lists and sets, but even
linear classification models. For example, some of the best known model
agnostic (and so non-formal) explainability approaches [301, 235] learn a
simple _interpretable_ model as the explanation for a more complex model. Some
other authors propose the use of interpretable models as the explanation
itself [304, 262, 305], specially in high-risk and safety-critical settings.
There is by now comprehensive evidence [239, 186, 166, 174, 187] that even
these so-called interpretable models can provide explanations that are
_arbitrarily_ redundant. Therefore, even so-called interpretable models ought
to be explained with the methods described in this paper444More importantly,
the growing evidence on the need to explain “interpretable” models [239, 187,
166, 174, 187] justifies wondering, in hindsight, about the practical
relevancy of learning (quasi-)optimal interpretable models [275, 52, 276, 356,
220, 51, 17, 358, 18, 348, 306, 78, 271, 181, 238, 138, 349, 162, 32, 33, 346,
4, 228, 196, 161, 347, 5, 136, 365, 366, 173, 106, 312, 280, 352, 318, 10,
105, 137, 353, 255, 314, 43]..

##### Organization.

The paper is organized in two main parts. The first part introduces a number
of well-established topics. Section 2 introduces the definitions and notation
used throughout the paper. Section 3 introduces the formal definitions of
explanations that have been studied in recent years. Based on the proposed
definitions of explanations, Section 4 studies algorithms for the computation
of explanations. In addition, as shown in Section 5, for some families of
classifiers, there are polynomial-time algorithms for computing one
explanation. The rest of the document covers the second part of the paper, and
targets topics related with ongoing research. Thus, this second part is
presented with less detail. Section 6 goes beyond computing one explanation,
and delves into explainability queries, that include enumeration of
explanations and deciding feature inclusion in explanations. Section 7
addresses the size of explanations, and proposes _probabilistic explanations_
as a mechanism to reduce explanation size. Section 8 overviews approaches for
accounting for input constraints and distributions. Section 9 overviews work
on approximating complex ML models with surrogate (or distilled) simpler
models, which are easier to explain. Section 10 summarizes a number of
additional topics of research. Finally, Section 11 identifies some directions
of research, and concludes the paper.

##  2 Preliminaries

##### Computational Complexity

The paper addresses a number of well-known classes of decision and function
(or search) problems. For decision problems, these include P, NP,
$\operatorname*{\textnormal{D}^{\textnormal{p}}}$,
$\operatorname*{\Sigma_{2}^{\textnormal{p}}}$, among others. For function
problems, we will also consider standard classes, including FP, FNP, among
others. (The interested reader is referred to a standard reference on
computational complexity [23].)

###  2.1 Logic Foundations

Throughout this section, we adopt notation and definitions from standard
references [281, 66, 87, 45, 81, 55].

####  2.1.1 Propositional Logic & Boolean Satisfiability.

This section studies the decision problem for propositional logic, also
referred to as the Boolean Satisfiability (SAT) problem [55]. (The
presentation follows standard references, e.g. [210, 87, 55].) SAT is well-
known to be an NP-complete [83] decision problem, with algorithm
implementations that can be traced to the early 1960s [103, 102].

##### Syntax – well-formed propositional formulas.

We consider a set of propositional atoms $X=\\{x_{1},\ldots,x_{n}\\}$ (these
are also most often referred to as boolean variables), and associate an index
with each atom, i.e. $i$ with $x_{i}$, $i=1,\ldots,n$, represented as the set
$\mathfrak{X}$. A (well-formed) propositional formula, or simply a formula, is
defined inductively as follows:

  1. 1.

An atom $x_{i}$ is a formula.

  2. 2.

If $\varphi$ is a formula, then $\neg\varphi$ is a formula. (The logic
operator $\neg$ is referred to as negation.)

  3. 3.

If $\varphi_{1}$ and $\varphi_{2}$ are formulas, then
$\varphi_{1}\lor\varphi_{2}$ is a formula. (The logic operator $\lor$ is
referred to as disjunction.)

  4. 4.

If $\varphi$ is a formula, then $(\varphi)$ is a formula.

A literal is an atom $x_{i}$ or its negation $\neg{x_{i}}$. We can use
additional logic operators, defined in terms of the basic operators above.
Well-known examples include:

  1. 1.

$\varphi_{1}\land\varphi_{2}$ represents the formula
$\neg(\neg\varphi_{1}\lor\neg\varphi_{2})$. (The logic operator $\land$ is
referred to as conjunction.)

  2. 2.

$\varphi_{1}\operatorname*{\rightarrow}\varphi_{2}$ represents the formula
$\neg\varphi_{1}\lor\varphi_{2}$. (The logic operator
$\operatorname*{\rightarrow}$ is referred to as implication.)

  3. 3.

$\varphi_{1}\operatorname*{\leftrightarrow}\varphi_{2}$ represents the formula
$(\varphi_{1}\operatorname*{\rightarrow}\varphi_{2})\land(\varphi_{2}\operatorname*{\rightarrow}\varphi_{1})$.
(The logic operator $\operatorname*{\leftrightarrow}$ is referred to as
equivalence. Also, we use $\operatorname*{\rightarrow}$ in the definition for
simplicity, and could just use the initial logic operators.)

Parentheses are used to enforce precedence between operators. Otherwise, the
precedence between operators is:
$\neg,\land,\lor,\operatorname*{\rightarrow},\operatorname*{\leftrightarrow}$.
A clause is a disjunction of literals. A term is a conjunction of literals.
For both clauses and terms, we will disallow having either clauses or terms
defined using an atom and its negation, or repetition of literals. This is
formalized as follows. Given $A,B\subseteq\mathfrak{X}$, with
$A\cap{B}=\emptyset$, a clause is defined by,

$\omega_{A,B}\triangleq\left(\lor_{i\in{A}}x_{i}\lor\lor_{i\in{B}}\neg{x_{i}}\right)$

and a term is defined by,

$\tau_{A,B}\triangleq\left(\land_{i\in{A}}x_{i}\land\land_{i\in{B}}\neg{x_{i}}\right)$

when clear from the context, we will drop the subscript from $\omega_{A,B}$
and $\tau_{A,B}$. $\mathbb{W}$ denotes the set of all possible clauses defined
on the set of atoms $X$. Similarly, $\mathbb{T}$ denotes the set of all
possible terms defined on the set of atoms $X$. A conjunctive normal form
(CNF) formula is a conjunction of clauses. A disjunctive normal form (DNF)
formula is a disjunction of terms.

To simplify some of the subsequent definitions in this section, clauses and
terms will also be viewed as sets of literals, each CNF formula as a set of
clauses, and each DNF formula as a set of terms.

##### Semantics – assignments & valuations.

An assignment is any point in $\mathbf{u}\in\\{0,1\\}^{n}$. (Throughout, we
associate 0 with both false and $\bot$, and 1 with both true and $\top$.) The
actual value ascribed to a propositional formula is derived from the
assignment of propositional values to the formula’s atoms. Each such complete
assignment is referred to as an _interpretation_. Given a formula $\varphi$,
and an assignment $\mathbf{u}\in\\{0,1\\}^{n}$, the valuation of $\varphi$
given $\mathbf{u}$ is represented by $\varphi^{\mathbf{u}}$, and it is defined
inductively as follows:

  1. 1.

$\varphi^{\mathbf{u}}=1$ if $\varphi=x_{i}$ and $u_{i}=1$ or
$\varphi=\neg{x_{i}}$ and $u_{i}=0$.

  2. 2.

$\varphi^{\mathbf{u}}=0$ if $\varphi=x_{i}$ and $u_{i}=0$ or
$\varphi=\neg{x_{i}}$ and $u_{i}=1$.

  3. 3.

$\varphi^{\mathbf{u}}=\neg(\psi^{\mathbf{u}})$, if $\varphi=\neg\psi$.

  4. 4.

$\varphi^{\mathbf{u}}=\psi_{1}^{\mathbf{u}}\lor\psi_{2}^{\mathbf{u}}$, if
$\varphi=\psi_{1}\lor\psi_{2}$.

  5. 5.

$\varphi^{\mathbf{u}}=(\psi^{\mathbf{u}})$, if $\varphi=(\psi)$.

Clearly, for any $\mathbf{u}\in\\{0,1\\}^{n}$,
$\varphi^{\mathbf{u}}\in\\{0,1\\}$. Also, it is plain to extend the semantics
to the other logic operators:
$\land,\operatorname*{\rightarrow},\operatorname*{\leftrightarrow}$. A
propositional formula $\varphi$ can also be viewed as representing a boolean
function that maps $\\{0,1\\}^{n}$ to $\\{0,1\\}$. The same symbol will be
used to refer to both formula and function, i.e.
$\varphi:\,\,\\{0,1\\}^{n}\to\\{0,1\\}$. Given some assignment
$\mathbf{u}\in\\{0,1\\}^{n}$, it is the case that
$\varphi(\mathbf{u})=\varphi^{\mathbf{u}}$.

Given a formula $\varphi$, $\mathbf{u}\in\\{0,1\\}$ is a _model_ of $\varphi$
if it makes $\varphi$ true, i.e. $\varphi^{\mathbf{u}}=1$. A formula $\varphi$
is _satisfiable_ or _consistent_ (represented by
$\varphi\operatorname*{\,\nvDash}\perp$) if it admits a model; otherwise, it
is _unsatisfiable_ or _inconsistent_ (represented by
$\varphi\operatorname*{\,\vDash}\perp$).

Practical reasoners for the SAT problem represent a success story of Computer
Science [342, 131]. Modern conflict-driven clause learning (CDCL) SAT
reasoners routinely decide formulas with millions of variables and tens of
millions of clauses [55, Chapter 4]. (This success hinges on the paradigm of
learning clauses from search conflicts [247, 248].) Furthermore, SAT reasoners
are the underlying engine used to achieve significant performance gains in
different areas of automated reasoning, including different boolean
optimization problems [55, Chapters 23, 24, 28], answer-set programming [134],
constraint programming [278], quantified boolean formulas [55, Chapters 30,
31], but also for reasoners for fragments of first order logic [55, Chapter
33] and theorem proving [132, 213, 214, 351]. SAT reasoners are often publicly
available and their performance improvements are regularly
assessed555http://www.satcompetition.org/.. There exist publicly available
toolkits that streamline prototyping with SAT reasoners. At the time of
writing, the reference example is PySAT [176].

It should be noted that the high performance reasoners mentioned above most
often require logic formulas represented in CNF (or in clausal form). There
are well-known, efficient, procedures for converting arbitrary (non-clausal)
logic formulas into clausal form [336, 286]. Given a propositional formula
$\varphi$, defined on a set of propositional atoms $X$,
$\psi=\left\llbracket{\varphi}\right\rrbracket$ is the _clausification_ of
$\varphi$, such that $\psi$ is defined on a set of atoms $X\cup{A}$, where $A$
denotes additional auxiliary atoms. One important result is that $\varphi$ and
$\psi$ are _equisatisfiable_ , i.e. $\varphi$ is satisfiable iff $\psi$ is
satisfiable. Encodings are detailed further in Section 2.1.3.

##### Entailment and equivalence.

Given two formulas $\varphi$ and $\tau$, we say that $\tau$ _entails_
$\varphi$, denoted by $\tau\operatorname*{\,\vDash}\varphi$, if,

$\forall(\mathbf{u}\in\\{0,1\\}^{n}).\left[\tau^{\mathbf{u}}\operatorname*{\rightarrow}\varphi^{\mathbf{u}}\right]$

which serves to indicate that any model of $\tau$ is also a model of
$\varphi$. We say that $\varphi_{1}\equiv\varphi_{2}$ iff
$\varphi_{1}\operatorname*{\,\vDash}\varphi_{2}$ and
$\varphi_{2}\operatorname*{\,\vDash}\varphi_{1}$.

Let $\tau_{A,B}$ and $\tau_{C,D}$ be terms, with both $A,B$ and $C,D$
representing disjoint pairs of subsets of $\mathfrak{X}$. Then, we have that,

######  Proposition 1.

$\tau_{A,B}\equiv\tau_{C,D}$ iff $A=C$ and $B=D$.

######  Proposition 2.

If $\tau_{A,B}\operatorname*{\,\vDash}\tau_{C,D}$ and
$\tau_{A,B}\not\equiv\tau_{C,D}$, then $C\subseteq{A}$, $D\subseteq{B}$, and
$C\subsetneq{A}$ or $D\subsetneq{B}$.

Clearly, similar results can be stated for clauses.

######  Example 1.

The terms $x_{1}\land\neg{x_{2}}\land{x_{3}}$ and $x_{1}\land\neg{x_{2}}$ are
represented, respectively, by $\tau_{A,B}$ and $\tau_{C,D}$, with
$A=\\{1,3\\}$, $B=\\{2\\}$, $C=\\{1\\}$ and $D=\\{2\\}$. It is the case that
$x_{1}\land\neg{x_{2}}\land{x_{3}}\operatorname*{\,\vDash}{x_{1}}\land\neg{x_{2}}$.
As can be concluded, $C\subsetneq{A}$ and $D\subseteq{B}$.
$\hfill\triangleleft$

##### Prime implicants and implicates.

Let $\varphi$ represent a propositional formula, and let $\tau_{A,B}$
represent a term. $\tau_{A,B}$ is a _prime implicant_ of $\varphi$ if,

  1. 1.

$\tau_{A,B}\operatorname*{\,\vDash}\varphi$.

  2. 2.

For any other term $\tau_{C,D}$, such that
$\tau_{A,B}\operatorname*{\,\vDash}\tau_{C,D}$ and
$\tau_{A,B}\not\equiv\tau_{C,D}$, then
$\tau_{C,D}\operatorname*{\,\nvDash}\varphi$.

Whenever the first condition holds (i.e.
$\tau_{A,B}\operatorname*{\,\vDash}\varphi$), then we say that $\tau_{A,B}$ is
an _implicant_ of $\varphi$.

######  Example 2.

Consider the terms $\tau_{A,B}=x_{1}\land{x_{2}}$ and $\tau_{C,D}=x_{1}$.
(Note that $A=\\{1,2\\},B=\emptyset,C=\\{1\\},D=\emptyset$.) Let
$\varphi=(x_{1}\land{x_{2}}\land{x_{3}})\lor({x_{1}}\land{x_{2}}\land\neg{x_{3}})$.
Clearly, for any assignment $\mathbf{u}\in\\{0,1\\}^{3}$ to
$x_{1},x_{2},x_{3}$, if $x_{1}=x_{2}=1$, then $\tau_{A,B}=1$ and also
$\varphi=1$, independently of the value of $x_{3}$. Hence,
$\tau_{A,B}\operatorname*{\,\vDash}\varphi$. However,
$\tau_{C,D}\operatorname*{\,\nvDash}\varphi$, in that there are assignments
$\mathbf{u}$ to $x_{1},x_{2},x_{3}$ such that $\tau_{C,D}^{\mathbf{u}}=1$ but
$\varphi^{\mathbf{u}}=0$. For example, whenever $x_{2}=0$, then $\varphi$
takes value 0, and that is not necessarily the case with $\tau_{C,D}$. Proving
that $\tau_{A,B}$ is a prime implicant of $\varphi$ would apparently require
proving that any term with literals that are a proper subset of $\tau_{A,B}$
are not implicants of $\varphi$. As discussed below, in practice one can
devise more efficient algorithms. $\hfill\triangleleft$

For completeness, we also mention prime implicates. Let $\varphi$ be a
propositional formula, and let $\omega_{A,B}$ be a clause. $\omega_{A,B}$ is a
_prime implicate_ of $\varphi$ if,

  1. 1.

$\varphi\operatorname*{\,\vDash}\omega_{A,B}$.

  2. 2.

For any other clause $\omega_{C,D}$, such that
$\omega_{C,D}\operatorname*{\,\vDash}\omega_{A,B}$ and
$\omega_{A,B}\not\equiv\omega_{C,D}$, then
$\varphi\operatorname*{\,\nvDash}\tau_{C,D}$.

Whenever the first condition holds (i.e.
$\varphi\operatorname*{\,\vDash}\omega_{A,B}$), then we say that
$\omega_{A,B}$ is an _implicate_ of $\varphi$.

A well-known result (which can be traced to [307]) is that, for a
propositional formula $\varphi$, prime implicants are minimal hitting sets
(MHSes) of the prime implicates and vice-versa666Recall that a set
${\mathcal{H}}$ is a _hitting set_ of a set of sets
${\mathcal{S}}=\\{S_{1},\ldots,S_{k}\\}$ if
${\mathcal{H}}\cap{S_{i}}\not=\emptyset$ for $i=1,\ldots,k$. ${\mathcal{H}}$
is a minimal hitting set of ${\mathcal{S}}$, if ${\mathcal{H}}$ is a hitting
set of ${\mathcal{S}}$, and there is no proper subset of ${\mathcal{H}}$ that
is also a hitting set of ${\mathcal{S}}$.. This result is at the core of
recent algorithms for enumerating prime implicants and implicates of a
propositional formula $\varphi$ [288].

Given a propositional formula $\varphi$ and a term $\tau$, with
$\tau\operatorname*{\,\vDash}\varphi$, a prime implicant $\pi$, with
$\tau\operatorname*{\,\vDash}\pi$, can be computed with at most a linear
number of calls to an NP oracle [337, 67, 288]. (The same observations apply
to the case of prime implicates.) In Section 4, we will revisit some of these
results when computing formal explanations.

##### Reasoning about inconsistency.

In many situations, there is the need to reason about inconsistent formulas
[246]. For example, we may be interested in explaining the reasons of
inconsistency, but we may also be interested in identifying which clauses to
ignore (or equivalently to remove from the formula) so as to restore
consistency777This paragraph aims at brevity. However, there are recent up-to-
date treatments of these topics [246].. The general setting is to consider a
set of clauses ${\mathcal{B}}$. ${\mathcal{B}}$ represents some background
knowledge base, and so it is assumed to be consistent. We say that
${\mathcal{B}}$ contains the _hard_ clauses (or in general the hard
constraints). A clause is hard when it cannot be removed (from the set of
clauses) to recover consistency. Furthermore, we also consider a set clauses
${\mathcal{S}}$, such that
$\varphi_{{\mathcal{B}},{\mathcal{S}}}={\mathcal{B}}\cup{\mathcal{S}}\operatorname*{\,\vDash}\perp$,
and $\varphi_{{\mathcal{B}},{\mathcal{S}}}$ is the formula (or set of
constraints) we want to reason about. The clauses in ${\mathcal{S}}$ represent
the _soft_ clauses (or constraints), and these can be removed to restore
consistency. (In the rest of this document, we will just refer to $\varphi$,
being implicit that $\varphi$ is characterized by the background knowledge
${\mathcal{B}}$ and by the soft clauses ${\mathcal{S}}$.)

######  Definition 1 (MUS).

Let $\varphi={\mathcal{B}}\cup{\mathcal{S}}$ be an inconsistent set of clauses
(or constraints), i.e. $\varphi\operatorname*{\,\vDash}\bot$.
${\mathcal{M}}\subseteq{\mathcal{S}}$ is a Minimal Unsatisfiable Subset (MUS)
if ${\mathcal{B}}\cup{\mathcal{M}}\operatorname*{\,\vDash}\bot$ and
$\forall_{{\mathcal{M}}^{\prime}\subsetneq{\mathcal{M}}},\,{\mathcal{B}}\cup{\mathcal{M}}^{\prime}\operatorname*{\,\nvDash}\bot$.

Informally, an MUS provides some irreducible information that suffices to be
added to the background knowledge ${\mathcal{B}}$ to attain an inconsistent
formula; thus, an MUS represents an explanation for the causes of
inconsistency. Alternatively, one might be interested in correcting the
formula, removing some clauses to achieve consistency.

######  Definition 2 (MCS).

Let $\varphi={\mathcal{B}}\cup{\mathcal{S}}$ be an inconsistent set of clauses
($\varphi\operatorname*{\,\vDash}\bot$). ${\mathcal{C}}\subseteq{\mathcal{S}}$
is a Minimal Correction Subset (MCS) if
${\mathcal{B}}\cup{\mathcal{S}}\setminus{\mathcal{C}}\operatorname*{\,\nvDash}\bot$
and $\forall_{{\mathcal{C}}^{\prime}\subsetneq{\mathcal{C}}}$,
${\mathcal{B}}\cup{\mathcal{S}}\setminus{\mathcal{C}}^{\prime}\operatorname*{\,\vDash}\bot$.

With each MCS ${\mathcal{C}}$, one associates a Maximal Satisfiable Subset
(MSS), given by ${\mathcal{S}}\setminus{\mathcal{C}}$.

######  Example 3.

Let $c_{1}=(x_{1})$, $c_{2}=(x_{2})$, $c_{3}=(x_{3})$,
$c_{4}=(\neg{x_{1}}\lor\neg{x_{2}})$, and
$c_{5}=(\neg{x_{1}}\lor\neg{x_{3}})$. Moreover, let
$\varphi={\mathcal{B}}\cup{\mathcal{S}}$, with
${\mathcal{B}}=\\{c_{4},c_{5}\\}$ and ${\mathcal{S}}=\\{c_{1},c_{2},c_{3}\\}$.
Hence, it is simple to conclude that an example of an MUS is
$\\{c_{1},c_{2}\\}$, an example of an MCS is $\\{c_{1}\\}$, and an example of
an MSS is $\\{c_{2},c_{3}\\}$. $\hfill\triangleleft$

Let $\mathsf{MUS}$, be a predicate,
$\mathsf{MUS}:2^{{\mathcal{S}}}\to\\{0,1\\}$, such that
$\mathsf{MUS}({\mathcal{M}})=1$ iff ${\mathcal{M}}\subseteq{\mathcal{S}}$ is
an MUS of $\varphi={\mathcal{B}}\cup{\mathcal{S}}$. Moreover, let
$\mathsf{MCS}$, be a predicate, $\mathsf{MCS}:2^{{\mathcal{S}}}\to\\{0,1\\}$,
such that $\mathsf{MCS}({\mathcal{C}})=1$ iff
${\mathcal{C}}\subseteq{\mathcal{S}}$ is an MCS of
$\varphi={\mathcal{B}}\cup{\mathcal{S}}$. Furthermore, we define,

$\displaystyle\mathbb{MU}(\varphi)$
$\displaystyle=\\{{\mathcal{M}}\subseteq{\mathcal{S}}\,|\,\mathsf{MUS}({\mathcal{M}})\\}$
(1) $\displaystyle\mathbb{MC}(\varphi)$
$\displaystyle=\\{{\mathcal{C}}\subseteq{\mathcal{S}}\,|\,\mathsf{MCS}({\mathcal{M}})\\}$
(2)

Moreover, there exists a well-known (subset-)minimal hitting set relationship
between MUSes and MCSes:

######  Proposition 3.

Given $\varphi={\mathcal{B}}\cup{\mathcal{S}}$, and
${\mathcal{M}}\subseteq{\mathcal{S}}$, ${\mathcal{C}}\subseteq{\mathcal{S}}$,
then

  1. 1.

${\mathcal{M}}$ is an MUS iff it is a minimal hitting set of the MCSes in
$\mathbb{MC}$;

  2. 2.

${\mathcal{C}}$ is an MCS iff it is a minimal hitting set of the MUSes in
$\mathbb{MU}$.

The MHS relationship between MUSes and MCSes was first demonstrated in the
context of model-based diagnosis [300] and later investigated for
propositional formulas in clausal form [56]. As immediate from the original
work [300], the MHS relationship applies in general to systems of constraints,
where each is represented as a first-order logic statement.

######  Example 4.

For the formula from Example 3, it is immediate to conclude that,

$\begin{array}[]{l}\mathbb{MU}(\varphi)=\\{\\{c_{1},c_{2}\\},\\{c_{1},c_{3}\\}\\}\\\
\mathbb{MC}(\varphi)=\\{\\{c_{1}\\},\\{c_{2},c_{3}\\}\\}\\\ \end{array}$

Moreover, one can observe that each MUS is an MHS of the MCSes, and that each
MCS is an MHS of the MUSes. $\hfill\triangleleft$

Complexity-wise, deciding whether a set of clauses is an MUS is known to be
$\operatorname*{\textnormal{D}^{\textnormal{p}}}$-complete [282, 281]. It is
also well-known that an MUS can be computed with at most a number of calls to
an NP-oracle that grows linearly with the number of clauses in the worst-case
[79]. MUSes and MCSes are tightly related with optimization problems [246].
For example, if each soft constraint is assigned a unit cost, then solving the
maximum satisfiability problem (MaxSAT) corresponds to finding a maximum cost
MSS [264, 55]. Under the assumption of a unit cost assigned to each clause,
then an MCS can be computed with a logarithmic number of calls to an NP-
oracle, e.g. by solving (unweighted) MaxSAT. (If non-unit costs are assumed,
then a worst-case linear number of calls to an NP-oracle is required.)
However, in practice there are more efficient algorithms that may require in
the worst-case a number of calls to an NP-oracle larger than logarithmic [241,
257, 256]. There have been very significant improvements in the practical
performance of MaxSAT solvers in recent years [55, Chapters 23, 24, 28]. A
number of solvers for MaxSAT and related problems are publicly
available888https://maxsat-evaluations.github.io/ and http://www.cril.univ-
artois.fr/PB16/ http://www.satcompetition.org/2011/ (MUS track)..

##### Quantification problems.

It is often of interest to quantify some of the variables in a propositional
formula (by default it is assumed that all variables are existentially
quantified). This is achieved by using two more logic operators, namely
$\forall$ for universal quantification and $\exists$ for existential
quantification. QBF (Quantified Boolean Formulas) is the problem of deciding
whether a quantified propositional formula is true or false. The problem of
deciding QBF is PSPACE-complete [23]. In this paper, we will briefly study
quantified problems with two levels of quantifier alternation, concretely
$\exists\forall$, which is a well-known
$\operatorname*{\Sigma_{2}^{\textnormal{p}}}$-complete decision problem. There
have been very significant improvements in the practical performance of QBF
solvers in recent years [55, Chapters 30, 31]. A number of solvers for QBF are
publicly available999http://www.qbflib.org/..

##### Logic-based abduction.

Abductive reasoning can be traced to the work of C. Peirce [152], with its
first uses in artificial intelligence in the early 1970s [266, 287]. Logic-
based abduction can be viewed as the problem of finding a (minimimum or
minimal) subset of hypotheses, which is consistent with some background
theory, and such that those hypotheses are sufficient for some manifestation.
A propositional abduction problem (PAP) is represented by a 5-tuple
$P=(X,{\mathcal{H}},{\mathcal{M}},{\mathcal{T}},\varsigma)$ [308, 175]. $X$ is
a finite set of atoms. ${\mathcal{H}}$, ${\mathcal{M}}$ and ${\mathcal{T}}$
denote propositional formulas representing, respectively, the set of
hypotheses, the set of manifestations, and the background theory.
(${\mathcal{H}}$ is further constrained to be a set of clauses.) $\varsigma$
is a function that associates a cost with each clause of ${\mathcal{H}}$,
$\varsigma\>:\>{\mathcal{H}}\to\mathbb{R}^{+}_{0}$. Given the background
theory ${\mathcal{T}}$, a set ${\mathcal{E}}\subseteq{\mathcal{H}}$ of
hypotheses is an explanation (for the manifestations) if: (i) ${\mathcal{E}}$
entails the manifestations ${\mathcal{M}}$ (given ${\mathcal{T}}$), i.e.
${\mathcal{T}}\land{\mathcal{E}}\operatorname*{\,\vDash}{\mathcal{M}}$; and
(ii) ${\mathcal{E}}$ is consistent (given ${\mathcal{T}}$), i.e.
${\mathcal{T}}\land{\mathcal{E}}\operatorname*{\,\nvDash}\bot$. The
propositional abduction problem is usually defined as computing a minimum cost
(or cardinality minimal) explanation for the manifestations subject to the
background theory. Moreover, one can consider explanations of (subset-)minimal
cost. The complexity of logic-based abduction has been studied in the past
[73, 111]. There are also recent practical algorithms for propositional
abduction [308, 175].

The computation of a prime implicant of some propositional formula $\varphi$,
defined on atoms $X$, can be formulated as a problem of abduction. Let
$\mathbf{u}$ be an assignment to the atoms of $\varphi$, such that
$\varphi^{\mathbf{u}}=1$. Given $\mathbf{u}$, construct the set
${\mathcal{H}}$ of hypotheses as follows: if $u_{i}=1$, then add $x_{i}$ to
${\mathcal{H}}$, otherwise add $\neg{x_{i}}$ to ${\mathcal{H}}$. We let
${\mathcal{T}}=\emptyset$ and ${\mathcal{M}}=\varphi$. Given the definition of
${\mathcal{H}}$, then a (subset-)minimal set
${\mathcal{E}}\subseteq{\mathcal{H}}$ is a prime implicant if, (i)
${\mathcal{E}}\operatorname*{\,\vDash}\varphi$; and (ii)
${\mathcal{E}}\operatorname*{\,\nvDash}\bot$. Observe that, by hypothesis,
condition (ii) is trivially satisfied. Hence, a prime implicant of $\varphi$
(given ${\mathcal{H}}$) is a subset-minimal set of literals
${\mathcal{E}}\subseteq{\mathcal{H}}$ such that
${\mathcal{E}}\operatorname*{\,\vDash}\varphi$.

In practice, when $\varphi$ is non-clausal, deciding entailment is somewhat
more complicated. In these cases, and as mentioned earlier, most often one
needs to clausify $\varphi$, so that it can be reasoned about. A difficulty
with efficient clausification procedures is that these introduce auxiliary
variables. As a result, we need to follow a different approach for computing a
prime implicant.

Let $\psi=\left\llbracket{\varphi}\right\rrbracket_{{\mathcal{V}}}$ be the
propositional clausal representation of $\varphi$, given some logic theory
${\mathcal{V}}$, which uses additional auxiliary atoms represented as set
${A}$. (Section 2.1.3 details further the use of logic encodings.) We
distinguish an auxiliary propositional atom $t\in{A}$, such that $t=1$ for the
assignments to $X$ and $A$ which satisfy $\psi$ (and so $\varphi$). In this
new setting, we let ${\mathcal{T}}=\psi$ and ${\mathcal{M}}=(t)$. Given a
(consistent) set of literals ${\mathcal{H}}$, representing a satisfying
assignment to the atoms of $\varphi$, then a (subset-)minimal set
${\mathcal{E}}\subseteq{\mathcal{H}}$ is a prime implicant if, (i)
$\psi\land{\mathcal{E}}\operatorname*{\,\vDash}{t}$; and (ii)
${\mathcal{E}}\operatorname*{\,\nvDash}\bot$. As before, condition (ii) is
trivially satisfied. Hence, a prime implicant of $\varphi$ (given
${\mathcal{H}}$) is a subset-minimal set of literals
${\mathcal{E}}\subseteq{\mathcal{H}}$ such that
$\psi\land{\mathcal{E}}\operatorname*{\,\vDash}{t}$.

##### Propositional Languages.

A propositional language represents a subset of the set of propositional
formulas, and several such subsets have been extensively studied [94, 95,
100]101010For brevity, we will not delve into defining propositional languages
and queries/transformations of interest. The interested reader is referred to
the bibliography [100].. One well-known example is negation normal form (NNF),
representing a directed-acyclic graph of $\land$ and $\lor$ operators, where
the leaves are atomic propositions or their negation. Other well-known
examples are DNF and CNF formulas. By imposing additional constraints on the
$\lor$ and $\land$ nodes of NNF formulas, one can devise classes of
propositional languages that exhibit important tractability properties. A
detailed analysis of propositional languages is available in [100]. Some
results on formal explainability have been derived for propositional languages
in recent years [320, 97, 29, 25, 165].

####  2.1.2 First Order Logic.

This section briefly mentions one well-known extension of propositional logic,
namely first order logic (FOL). FOL extends propositional logic with
predicates, functions, constants and quantifiers, and such that variables are
allowed to take values from arbitrary domains. In contrast with propositional
logic, where an interpretation is an assignment of values to the formula’s
atoms, in the case of FOL, an interpretation must ascribe a meaning to
predicates, functions and constants. Whereas validity in FOL is undecidable
[45], one can reason in concrete theories, with a well-known example being
satisfiability modulo theories.

##### Satisfiability modulo theories (SMT).

By providing first order logic with concrete theories, e.g. integer
arithmetic, real arithmetic or mixed integer-real arithmetic, among many other
possibilities, one obtains decidable fragments, for which practically
efficient reasoners have been developed over the last two decades. (There
exist undecidable theories in SMT [218], but that is beyond the goals of this
document. SMT solvers generalize SAT to reason with fragments of first order
logic [218, 81, 55]. Throughout this paper, we will use SMT reasoners solely
as an alternative for mixed-integer linear programming reasoners (see below),
even though SMT reasoners allow for significantly more general fragments of
FOL. Similar to the case of SAT, we can solve optimization problems over SMT
formulas (MaxSMT), and we can also reason about inconsistency. Previous
definitions (see Section 2.1.1) also apply in this setting.

##### Mixed integer linear programming (MILP).

MILP can be formulated as a first-order logic theory (e.g. [66], where
variables can take values from boolean, integer and real domains, and where
the allowed binary functions are $+$ and $-$, with their usual meanings, and
the allowed binary predicates are $=$ and $\leq$, also with their usual
meanings. We will also allow a countable number of unary constant functions
$b\cdot$, with $b\in\mathbb{R}$ (thus accounting for the other possible cases
of $\mathbb{B}$ and $\mathbb{Z}$), and where each $b\cdot$ represents a
coefficient. Starting from a set $V$ of (variable) numbers, i.e.
$V=\\{1,\ldots,m\\}$, we consider a partition of $V$ into $B$, $I$ and $R$.
The general MILP formulation is thus:

$\begin{array}[t]{lcl}\textnormal{min}&&\sum_{j=1}^{n}c_{j}x_{j}\\\\[5.0pt]
\textnormal{s.t.}&&\begin{array}[t]{l}\sum_{j=1}^{n}a_{ij}x_{j}\leq{b_{i}},i=1,\ldots,r\\\\[1.5pt]
x_{j}\in\\{0,1\\},j\in{B}\\\ x_{j}\in\mathbb{Z},j\in{I}\\\
x_{j}\in\mathbb{R},j\in{R}\\\ a_{ij},b_{i}\in\mathbb{R}\end{array}\end{array}$

Several proprietary and publicly available MILP solvers are available111111For
example, https://www.ibm.com/ae-en/analytics/cplex-optimizer,
https://www.gurobi.com/, https://sourceforge.net/projects/lpsolve/., with
significant performance gains reported over the years [57, 58, 212].

##### Additional definitions.

The definitions introduced in the propositional logic case can be generalized
to the case of FOL, SMT, MILP, etc. These generalizations include entailment,
prime implicants and implicates, but also the definitions associated with
reasoning about inconsistency. A discussion of some of these concepts beyond
propositional logic is available for example in [246].

####  2.1.3 Encodings & Interfacing Reasoners.

Throughout the document, we will extensively refer to SAT, SMT and MILP
reasoners. Consistency checking with a reasoner for theory ${\mathcal{T}}$ on
a ${\mathcal{T}}$-theory formula $\varphi_{{\mathcal{T}}}$ is represented by
$\operatorname*{\textnormal{{{CO}}}}(\varphi_{{\mathcal{T}}};{\mathcal{T}})$,
and denotes whether $\varphi_{{\mathcal{T}}}$ has at least one model (given
${\mathcal{T}}$), i.e. an interpretation that satisfies
$\varphi_{{\mathcal{T}}}$. For simplicity, the parameterization on
${\mathcal{T}}$ is omitted, and so we use
$\operatorname*{\textnormal{{{CO}}}}(\varphi_{{\mathcal{T}}})$ instead. These
theory reasoners operate on formulas of a suitable logic language. Given some
logic formula $\varphi$, $\llbracket\varphi\rrbracket_{{\mathcal{T}}}$ denotes
the encoding of $\varphi$ in a representation suitable for reasoning by a
decision oracle for theory ${\mathcal{T}}$. (For simplicity, we just use
$\llbracket\varphi\rrbracket$.) As shown below, the computation of formal
explanations assumes the existence of a reasoner that decides the
satisfiability (or consistency) of a statement expressed in theory
${\mathcal{T}}$.

For the case of propositional theories, SAT reasoners most often work with
clausal representations. As noted earlier, there exist procedures for
converting arbitrary (non-clausal) logic formulas into clausal form [336,
286], which require the use of additional propositional atoms. There are also
well-known encodings of constraints into clausal form [55, Chapters 02, 28].
Examples include cardinality constraints, e.g. AtMost$K$ (i.e.
$\sum_{i}x_{i}\leq{K}$, with boolean $x_{i}$) or AtLeast$K$ (i.e.
$\sum_{i}\geq{k}$, with boolean $x_{i}$) constraints, and pseudo-boolean
constraints ($\sum{i}a_{i}x_{i}\leq{b}$, also with boolean $x_{i}$), among
many others.

###  2.2 Classification Problems

Classification problems in ML are defined on a set of features (or attributes)
${\mathcal{F}}=\\{1,\ldots,m\\}$ and a set of classes
${\mathcal{K}}=\\{c_{1},c_{2},\ldots,c_{K}\\}$. Each feature
$i\in{\mathcal{F}}$ takes values from a domain ${\mathcal{D}}_{i}$. In
general, domains can be categorical or ordinal, with values that can be
boolean or integer. (Although real-valued could be considered for some of the
classifiers studied in the paper, we opt not to specifically address real-
valued features.) The set of domains is represented by
$\mathbb{D}=({\mathcal{D}}_{1},\ldots,{\mathcal{D}}_{m})$. Feature space is
defined as
$\mathbb{F}={\mathcal{D}}_{1}\times{{\mathcal{D}}_{2}}\times\ldots\times{{\mathcal{D}}_{m}}$;
$|\mathbb{F}|$ represents the total number of points in $\mathbb{F}$. For
boolean domains, ${\mathcal{D}}_{i}=\\{0,1\\}={\mathcal{B}}$, $i=1,\ldots,m$,
and $\mathbb{F}={\mathcal{B}}^{m}$. The notation
$\mathbf{x}=(x_{1},\ldots,x_{m})$ denotes an arbitrary point in feature space,
where each $x_{i}$ is a variable taking values from ${\mathcal{D}}_{i}$. The
set of variables associated with features is $X=\\{x_{1},\ldots,x_{m}\\}$.
Moreover, the notation $\mathbf{v}=(v_{1},\ldots,v_{m})$ represents a specific
point in feature space, where each $v_{i}$ is a constant representing one
concrete value from ${\mathcal{D}}_{i}$. With respect to the set of classes
${\mathcal{K}}$, the size of ${\mathcal{K}}$ is assumed to be finite; no
additional restrictions are imposed on ${\mathcal{K}}$. Nevertheless, with the
goal of simplicity, the paper considers examples where $|{\mathcal{K}}|=2$,
concretely ${\mathcal{K}}=\\{0,1\\}$, or alternatively
${\mathcal{K}}=\\{\ominus,\oplus\\}$. An ML classifier ${\mathcal{M}}$ is
characterized by a (non-constant) _classification function_ $\kappa$ that maps
feature space $\mathbb{F}$ into the set of classes ${\mathcal{K}}$, i.e.
$\kappa:\mathbb{F}\to{\mathcal{K}}$. Each classifier ${\mathcal{M}}$ is
represented unambiguously by the tuple
$({\mathcal{F}},\mathbb{D},\mathbb{F},{\mathcal{K}},\kappa)$. (With a mild
abuse of notation, we also write
${\mathcal{M}}=({\mathcal{F}},\mathbb{D},\mathbb{F},{\mathcal{K}},\kappa)$.)
An _instance_ (or observation) denotes a pair $(\mathbf{v},c)$, where
$\mathbf{v}\in\mathbb{F}$ and $c\in{\mathcal{K}}$, with
$c=\kappa(\mathbf{v})$.

The _classifier decision problem_ (CDP) is to decide whether the logic
statement $\exists(\mathbf{x}\in\mathbb{F}).(\kappa(\mathbf{x})=c)$, for
$c\in{\mathcal{K}}$, is true. Given some target class $c\in{\mathcal{K}}$, the
goal of CDP is to decide whether there exists some point $\mathbf{x}$ in
feature space for which the prediction is $c$. For example, for a neural
network or a random forest, it is easy to prove that CDP is NP-complete. In
contrast, for univariate decision trees, CDP is in P. This is further
discussed in the next section.

####  2.2.1 Examples of Classifiers.

This paper studies decision trees (DTs), decision sets (DSs) and decision
lists (DLs) in greater detail. Nevertheless, formal explainability has been
studied in the context of several other well-known families of classifiers,
including naive bayes classifiers (NBCs) [239], decision diagrams and graphs
[166], tree ensembles [180, 170, 191, 172], monotonic classifiers [240, 84],
neural networks [178], and bayesian network classifiers [320, 321]. Additional
information can be found in the cited references.

##### Decision trees (DTs).

DTs are among the still most widely used family of classifiers, with
applications in both ML and data mining (DM) [70, 293, 294, 363, 124]. A
decision tree is a directed acyclic graph, with one root node that has no
incoming edges, and the remaining nodes having exactly one incoming edge.
Terminal nodes have no outgoing edges, and non-terminal nodes have two or more
outgoing edges. Each terminal node is associated with a class, i.e. the
predicted class for the node. Each non-terminal node is associated with
exactly one feature121212Thus, this paper only considers _univariate_ DTs, for
which where each non-terminal node test a single feature. In contrast, for
multivariable DTs [71], we assume that each non-terminal node can test
arbitrary functions of the features. For ordinal features, multivariate DTs
are also referred to as _oblique_ [267].. Each outgoing edge is associated
with a literal defined using the values of the feature, and such that any
value of the feature domain is consistent with exactly one of the literals of
the outgoing edges. A tree path ${\mathcal{P}}$ connects the root node with
one of the tree’s terminal nodes. Common (implicit) assumptions of DTs are
that: (i) all paths in a DT are consistent; and (ii) for each point
$\mathbf{v}$ in feature space, there exists exactly one path ${\mathcal{P}}$
that is consistent with $\mathbf{v}$. (Observe that (ii) requires that the
branches at each node capture all values in the domain of the tested feature
and that the branches’ conditions be mutually disjoint.) Given these
assumptions of DTs, it is easy to see that CDP is in P. One simply picks the
target class and a terminal node predicting the class, and reconstructs the
path to the root; a procedure that runs in linear time on the size of the
tree. An example of a DT is shown in Figure 2(a). (This example will be
analyzed in greater detail below.)

##### Decision lists (DLs) and sets (DSs).

DLs and DSs also find a wide range of applications [80, 124, 220, 18, 17]. DLs
and DSs represent, respectively, ordered and unordered rule sets. There exist
in-depth studies of DLs [303], but in contrast DSs are less well-understood.
Each rule is of the form:

$\begin{array}[]{ccccccccc}\textnormal{R${}_{j}$:}&&\textnormal{IF~{}}&&(\tau_{j})&&\textnormal{~{}THEN~{}}&&d_{j}\\\
\end{array}$

where $\tau_{j}$ represents a boolean expression defined on the features and
their domains, and $d_{j}\in{\mathcal{K}}$. We say that the rule _fires_ if
its literal ($\tau_{j}$) is consistent (or holds true). For DLs, and with the
exception of the first rule, all other rules are of the form:

$\begin{array}[]{ccccccccc}\textnormal{R${}_{l}$:}&&\textnormal{ELSE~{}IF~{}}&&(\tau_{l})&&\textnormal{~{}THEN~{}}&&d_{l}\\\
\end{array}$

For the last (default) rule, it is required that $\tau_{l}$ is a tautology,
i.e. the rule always fires if all others do not. (This basically corresponds
to solely having ELSE as the rule’s condition.) The default rule is marked as
$\textnormal{R}_{\textnormal{\sc{def}}}$. An example of a DL is shown in
Figure 1(a). An example of a DS would be the same DL, but without the ELSE’s,
i.e. there would be no order among the listed rules. (The DL example will be
analyzed in greater detail below.) In contrast with DLs, the lack of order of
rules in DSs raises a number of issues [181]. One issue is _overlap_ , i.e.
two or more rules predicting different classes may fire on the same point of
feature space. A second issue is _coverage_ , i.e. without a default rule, it
may happen that no rule fires on some points of feature space. It is
conjectured that is is $\operatorname*{\Sigma_{2}^{\textnormal{p}}}$-hard to
learn DSs that ensure both no overlap and ensuring coverage of all points in
feature space [181].

##### Neural networks (NNs).

We consider a simple architecture for an NN, concretely feed-forward NNs,
which we refer to as NNs. (A comprehensive treatment of NNs can be found
elsewhere [142].) An NN is composed of a number of layers of neurons. The
output values of the neurons in a given layer $\mathbf{x}^{l}$ are computed
given the output values of the neurons in the previous layer
$\mathbf{x}^{l-1}$, up to a number $L$ of layers, and such that the inputs
represent layer 0. Furthermore, each neuron computes an intermediate value
given the output values of the neurons in the previous layer, and the weights
of the connections between layers. For each layer, the intermediate computed
values are represented by $\mathbf{y}^{l}$. The output value of each neuron is
the result of applying a non-linear activation function on the values of
$\mathbf{y}^{l}$, thus obtaining $\mathbf{x}^{l}$. Assuming a ReLU [269]
activation function, one obtained the following:

$\begin{array}[]{l}\mathbf{y}^{l}=\mathbf{A}^{l}\cdot(\mathbf{x}^{l-1})^{\textnormal{T}}\\\\[2.5pt]
\mathbf{x}^{l}=\max(\mathbf{y}^{l},\mathbf{0})\\\ \end{array}$ (3)

where $\mathbf{x}^{0}$ denote the input values, $\mathbf{x}^{L}$ denotes the
output values, and $\mathbf{A}^{l}$ denotes the weights matrix (that also
accounts for a possible bias vector, by including a variable $x_{0}^{l-1}=1$).
For classification problems, there are different mechanisms to predict the
actual class associated with the computed output values. One option is to have
each output represent a class. Another option is to pick the class depending
on the range of values taken by the output variable. This alternative is
illustrated with the running example presented later in this section.

A recent alternative to NNs, namely binarized neural networks (BNNs) [169] has
also been investigated from the perspective of explainability [272].

##### Monotonic classifiers.

Monotonic classifiers find a number of important applications, and have been
studied extensively in recent years [120, 364, 231, 324]. Let $\preccurlyeq$
denote a partial order on the set of classes ${\mathcal{K}}$. For example, we
assume $c_{1}\preccurlyeq{c_{2}}\preccurlyeq\ldots{c_{K}}$. Furthermore, we
assume that each domain $D_{i}$ is ordered such that the value taken by
feature $i$ is between a lower bound $\lambda(i)$ and an upper bound $\mu(i)$.
Given $\mathbf{v}_{1}=(v_{11},\ldots,v_{1i},\ldots,v_{1m})$ and
$\mathbf{v}_{2}=(v_{21},\ldots,v_{2i},\ldots,v_{2m})$, we say that
$\mathbf{v}_{1}\leq\mathbf{v}_{2}$ if,
$\forall(i\in{\mathcal{F}}).v_{1i}\leq{v_{2i}}$. Finally, a classifier is
monotonic if whenever $\mathbf{v}_{1}\leq\mathbf{v}_{2}$, then
$\kappa(\mathbf{v}_{1})\preccurlyeq\kappa(\mathbf{v}_{2})$.

##### Additional families of classifiers.

Formal explainability has been studied in the context of other families of
classifiers, including random forests (RFs) [191, 65], boosted trees (BTs)
[180, 170, 172], tree ensembles (TEs, which include both RFs and BTs) [172],
decision graphs (DGs)& diagrams [166], naive bayes classifiers (NBCs) [239],
monotonic classifiers [240], propositional language classifiers [165], and
bayesian network classifiers [320, 321]. Most of these classifiers are covered
in standard references on ML [124, 316, 142].

A random forest is represented by a set of decision trees, each tree trained
from a random sample of the original dataset. In the originally proposed
formulation of RFs [68], the selected class is picked by majority voting among
all trees. As an example, we show that CDP for RFs is NP-complete.

######  Proposition 4.

For RFs, CDP is NP-complete.

Proof.  The decision problem is clearly in NP. Simply pick a point in feature
space, and then compute in polynomial time the prediction of the RF, the
decision problem answers true if the prediction is $c$, and it answers false
if the prediction is other than $c$.
To prove NP-hardness, we reduce the decision problem for propositional
formulas represented in CNF, a problem well-known to be complete for NP. Let
$\psi$ be a CNF formula with $m$ propositional variables and $n$ clauses,
$\varsigma_{1},\ldots,\varsigma_{n}$:

  * •

Create $n$ decision trees, one for each clause $\varsigma_{j}$, and such that
DT $j$ predicts 1 if at least one literal of $\varsigma_{j}$ is satisfied, and
0 if all literals of $\varsigma_{j}$ are falsified.

  * •

Also, create $n-1$ decision trees, each with a single terminal node with
prediction 0.

Clearly, the reduction runs in polynomial time. Moreover, it is immediate that
the RF picks class 1 if and only if the formula is satisfied. Let the
assignment to $\psi$ be such that $\psi(x_{1},\ldots,x_{m})$ is satisfied. In
this case, each DT associated with a clause will predict 1 and the other $n-1$
DTs will predict 0; hence the prediction will be 1. Furthermore, for the
prediction to be 1, it must be the case that the $n$ DTs associated with the
clauses must predict 1, since one must offset the $n-1$ trees that
guaranteedly predict 0. $\Box$

A simpler argument could be used to prove that CDP for multivariate decision
trees is also NP-complete. As an example, the CNF formula could be tested on a
single tree node.

####  2.2.2 Running Examples.

Throughout the paper, the following running examples will be used to
illustrate some of the main results.

######  Example 5 (DL).

The first running example is a simple DL, that is adapted from [124, Section
6.1]. (The original classification problem is to decide whether some animal is
a dolphin. The features have been numbered, respectively 1 is Gills, 2 is
Teeth, 3 is Beak, and 4 is Length. Moreover, the feature values have been
replaced by numbers. These changes are meant to facilitate the logical
analysis of the classifier, and do not affect in any way the computed
explanations.) As a result, ${\mathcal{F}}_{1}=\\{1,2,3,4\\}$,
${\mathcal{D}}_{1i}=\\{0,1\\},i=1,2,3$, ${\mathcal{D}}_{14}=\\{0,1,2\\}$,
${\mathcal{K}}_{1}=\\{0,1\\}$, and $\kappa_{1}$ is defined by Figure 1(a).
Clearly,
$\mathbb{F}=\\{0,1\\}\times\\{0,1\\}\times\\{0,1\\}\times\\{0,1,2\\}$.
Moreover, the target instance is $(\mathbf{v},c)=((0,0,1,2),1)$. Each of the
rules $\textnormal{R}_{1}$, $\textnormal{R}_{2}$, and $\textnormal{R}_{3}$
tests a single literal, and a final default rule
$\textnormal{R}_{\textnormal{\sc{def}}}$ fires on the points in feature space
inconsistent with the other rules. Finally, Table 1 lists the class predicted
by the DL for every point in feature space. $\hfill\triangleleft$

$\begin{array}[]{lllcl}\textnormal{R${}_{1}$:}&\textnormal{IF~{}}&(x_{1}=1)&\textnormal{~{}THEN~{}}&0\\\
\textnormal{R${}_{2}$:}&\textnormal{ELSE
IF~{}}&(x_{2}=1)&\textnormal{~{}THEN~{}}&1\\\
\textnormal{R${}_{3}$:}&\textnormal{ELSE
IF~{}}&(x_{4}=1)&\textnormal{~{}THEN~{}}&0\\\
\textnormal{R${}_{\textnormal{\sc{def}}}$:}&\textnormal{ELSE~{}}&&\textnormal{~{}THEN~{}}&1\end{array}$
(a) Decision list

$\begin{array}[]{c|c}\textnormal{Item}&\textnormal{Definition}\\\
\hline\cr{\mathcal{F}}_{1}&\\{1,2,3,4\\}\\\
\hline\cr{\mathcal{D}}_{1i},i=1,2,3&\\{0,1\\}\\\
\hline\cr{\mathcal{D}}_{14}&\\{0,1,2\\}\\\
\hline\cr{\mathcal{K}}_{1}&\\{0,1\\}\end{array}$ (b) Classification problem

$\begin{array}[]{c|c|c}\textnormal{Feature \\#}&\textnormal{Feature
Name}&\textnormal{Original \& Mapped Domain}\\\ \hline\cr
1&\textnormal{Gills}&\\{\textnormal{No}{\to}0,\textnormal{Yes}{\to}1\\}\\\
\hline\cr
2&\textnormal{Teeth}&\\{\textnormal{Few}{\to}0,\textnormal{Many}{\to}1\\}\\\
\hline\cr
3&\textnormal{Beak}&\\{\textnormal{No}{\to}0,\textnormal{Yes}{\to}1\\}\\\
\hline\cr
4&\textnormal{Length}&\\{\textnormal{3}{\to}0,\textnormal{4}{\to}1,\textnormal{5}{\to}2\\}\\\
\hline\cr\lx@intercol\hfil\textnormal{Classes}\hfil\lx@intercol\vrule\lx@intercol&\\{\textnormal{No}{\to}0,\textnormal{Yes}{\to}{1}\\}\end{array}$
(c) Mapping of features

Figure 1: Decision list, adapted from [124] Entry |  $x_{1}$ |  $x_{2}$ |  $x_{3}$ |  $x_{4}$ |  Rule |  $\kappa_{1}(x_{1},x_{2},x_{3},x_{4})$
---|---|---|---|---|---|---
00 |  0 |  0 |  0 |  0 |  $\textnormal{R}_{\textnormal{\sc{def}}}$ |  1
01 |  0 |  0 |  0 |  1 |  $\textnormal{R}_{3}$ |  0
02 |  0 |  0 |  0 |  2 |  $\textnormal{R}_{\textnormal{\sc{def}}}$ |  1
03 |  0 |  0 |  1 |  0 |  $\textnormal{R}_{\textnormal{\sc{def}}}$ |  1
04 |  0 |  0 |  1 |  1 |  $\textnormal{R}_{3}$ |  0
05 |  0 |  0 |  1 |  2 |  $\textnormal{R}_{\textnormal{\sc{def}}}$ |  1
06 |  0 |  1 |  0 |  0 |  $\textnormal{R}_{2}$ |  1
07 |  0 |  1 |  0 |  1 |  $\textnormal{R}_{2}$ |  1
08 |  0 |  1 |  0 |  2 |  $\textnormal{R}_{2}$ |  1
09 |  0 |  1 |  1 |  0 |  $\textnormal{R}_{2}$ |  1
10 |  0 |  1 |  1 |  1 |  $\textnormal{R}_{2}$ |  1
11 |  0 |  1 |  1 |  2 |  $\textnormal{R}_{2}$ |  1
12 |  1 |  0 |  0 |  0 |  $\textnormal{R}_{1}$ |  0
13 |  1 |  0 |  0 |  1 |  $\textnormal{R}_{1}$ |  0
14 |  1 |  0 |  0 |  2 |  $\textnormal{R}_{1}$ |  0
15 |  1 |  0 |  1 |  0 |  $\textnormal{R}_{1}$ |  0
16 |  1 |  0 |  1 |  1 |  $\textnormal{R}_{1}$ |  0
17 |  1 |  0 |  1 |  2 |  $\textnormal{R}_{1}$ |  0
18 |  1 |  1 |  0 |  0 |  $\textnormal{R}_{1}$ |  0
19 |  1 |  1 |  0 |  1 |  $\textnormal{R}_{1}$ |  0
20 |  1 |  1 |  0 |  2 |  $\textnormal{R}_{1}$ |  0
21 |  1 |  1 |  1 |  0 |  $\textnormal{R}_{1}$ |  0
22 |  1 |  1 |  1 |  1 |  $\textnormal{R}_{1}$ |  0
23 |  1 |  1 |  1 |  2 |  $\textnormal{R}_{1}$ |  0
Table 1: Truth table for Example 5, where the target instance
$(\mathbf{v},c)=((0,0,1,2),1)$ corresponds to entry 05.

######  Example 6 (DT).

The second running example is the decision tree shown in Figure 2. (This DT is
adapted from [162] by replacing the names of the features and renaming the
binary domains to boolean. The original DT was produced with the tool OSDT
(optimal sparse decision trees) [162].) For this DT classifier (see Figure
2(b)), ${\mathcal{F}}_{2}=\\{1,2,3,4,5\\}$,
${\mathcal{D}}_{2i}=\\{0,1\\},i=1,\ldots,5$, ${\mathcal{K}}_{2}=\\{0,1\\}$,
and $\kappa_{2}$ is captured by the DT shown in the Figure 2(a). As can be
observed, the DT has 15 nodes, with the non-terminal nodes being
$N=\\{1,2,4,5,7,8,10\\}$ and the terminal nodes being
$T=\\{3,6,9,11,12,13,14,15\\}$. Each non-terminal node is associated with a
feature from ${\mathcal{F}}$ (we assume univariate DTs), and each outgoing
edge tests one or more values from the feature’s domain. For example, the edge
$(2,4)$ is associated with the literal $x_{2}=0$, being consistent with points
in feature space where $x_{2}$ takes value 0. Each terminal node is associated
with a prediction from ${\mathcal{K}}$. The set of paths is ${\mathcal{R}}$.
Throughout the paper, ${\mathcal{R}}$ is partitioned into two sets, namely
${\mathcal{P}}$ associated with prediction 1, and ${\mathcal{Q}}$ associated
with prediction 0. (The split of ${\mathcal{R}}$ serves to aggregate paths
according to their prediction, but the naming is arbitrary, and we could
consider other splits, e.g. ${\mathcal{P}}$ for prediction 0, and
${\mathcal{Q}}$ for prediction 1.) Moreover,
${\mathcal{P}}=\\{P_{1},P_{2},P_{3},P_{4},P_{5}\\}$, with $P_{1}=\langle
1,2,4,7,10,15\rangle$, $P_{2}=\langle 1,2,4,7,11\rangle$, $P_{3}=\langle
1,2,5,8,13\rangle$, $P_{4}=\langle 1,2,5,9\rangle$, and $P_{5}=\langle
1,3\rangle$. Similarly, ${\mathcal{Q}}=\\{Q_{1},Q_{2},Q_{3}\\}$, with
$Q_{1}=\langle 1,2,4,6\rangle$, $Q_{2}=\langle 1,2,4,7,10,14\rangle$, and
$Q_{3}=\langle 1,2,5,8,12\rangle$. Furthermore, the target instance we will
study is $(\mathbf{v},c)=((0,0,1,0,1),1)$, being consistent with path $P_{1}$
and so with prediction 1. Finally, Table 2 shows parts of the truth table of
the example DT, that will be used later when analyzing the instance
$(\mathbf{v},c)=((0,0,1,0,1),1)$. $\hfill\triangleleft$

BDT/.style= for tree= l=1.5cm,s sep=1.15cm, if n children=0circle,
draw=black,text=black,edge= my edge , if n=1 edge+=0 my edge, , edge=thick, ,
BDT [$x_{1}$, label=[yshift=-6.875ex]1 [$x_{2}$, label=[yshift=-6.875ex]2,
edge label=node[midway,left,xshift=-0.5pt] $=0$ [$x_{3}$,
label=[yshift=-6.875ex]4, edge label=node[midway,left,xshift=-2.5pt] $=0$ [0,
label=[yshift=-5.0ex]6, edge label=node[midway,left,xshift=-0.5pt] $=0$,
rectangle, fill=tred3!20 ] [$x_{4}$, label=[yshift=-6.875ex]7, edge
label=node[midway,right,xshift=0.5pt] $=1$ [$x_{5}$,
label=[yshift=-6.875ex]10, edge label=node[midway,left,xshift=-1.5pt] $=0$ [0,
label=[yshift=-5.0ex]14, edge label=node[midway,left,xshift=-1.5pt] $=0$,
rectangle, fill=tred3!20 ] [1, label=[yshift=-5.0ex]15, edge
label=node[midway,right,xshift=0.5pt] $=1$, rectangle, fill=tgreen3!25 ] ] [1,
label=[yshift=-5.0ex]11, edge label=node[midway,right,xshift=0.5pt] $=1$,
rectangle, fill=tgreen3!25 ] ] ] [$x_{4}$, label=[yshift=-6.875ex]5, edge
label=node[midway,right,xshift=1.5pt] $=1$ [$x_{5}$, label=[yshift=-6.875ex]8,
edge label=node[midway,left,xshift=-0.5pt] $=0$ [0, label=[yshift=-5.0ex]12,
edge label=node[midway,left,xshift=-0.5pt] $=0$, rectangle, fill=tred3!20 ]
[1, label=[yshift=-5.0ex]13, edge label=node[midway,right,xshift=0.5pt] $=1$,
rectangle, fill=tgreen3!25 ] ] [1, label=[yshift=-5.0ex]9, edge
label=node[midway,right,xshift=0.5pt] $=1$, rectangle, fill=tgreen3!25 ] ] ]
[1, label=[yshift=-5.0ex]3, edge label=node[midway,right,xshift=0.5pt] $=1$,
rectangle, fill=tgreen3!25 ] ]

(a) Decision tree

Feature in [162] |  Boolean feature
---|---
middle-middle=x |  $x_{1}$
top-left=x |  $x_{2}$
bottom-right=x |  $x_{3}$
bottom-left=x |  $x_{4}$
top-right=x |  $x_{5}$

Definitions
---
${\mathcal{F}}_{2}$ | $\\{1,2,3,4,5\\}$
${\mathcal{D}}_{21},\ldots,{\mathcal{D}}_{25}$ | $\\{0,1\\}$
${\mathcal{K}}_{2}$ | $\\{0,1\\}$

(b) Mapping of features

Figure 2: Decision tree, adapted from [162, Figure 5b], for the tic-tac-toe
dataset, and also studied in [187]

$x_{3}$ |  $x_{5}$ |  $x_{1}$ |  $x_{2}$ |  $x_{4}$ |  $\kappa_{2}(\mathbf{x})$
---|---|---|---|---|---
1 |  1 |  0 |  0 |  0 |  1
1 |  1 |  0 |  0 |  1 |  1
1 |  1 |  0 |  1 |  0 |  1
1 |  1 |  0 |  1 |  1 |  1
1 |  1 |  1 |  0 |  0 |  1
1 |  1 |  1 |  0 |  1 |  1
1 |  1 |  1 |  1 |  0 |  1
1 |  1 |  1 |  1 |  1 |  1
(a) With $x_{3}=x_{5}=1$, it is that case that
$\kappa_{2}(x_{1},x_{2},x_{3},x_{4},x_{5})=1$, independently of the values of
the other features

$x_{3}$ |  $x_{5}$ |  $x_{1}$ |  $x_{2}$ |  $x_{4}$ |  $\kappa_{2}(\mathbf{x})$
---|---|---|---|---|---
0 |  0 |  0 |  0 |  0 |  0
0 |  1 |  0 |  0 |  0 |  0
1 |  0 |  0 |  0 |  0 |  0
1 |  1 |  0 |  0 |  0 |  1
(b) With $x_{1}=x_{2}=x_{4}=0$, it is that case that
$\kappa_{2}(x_{1},x_{2},x_{3},x_{4},x_{5})$ can take a value other than 1,
depending on the values assigned to $x_{3}$ and $x_{5}$

Table 2: Partial truth tables of $\kappa_{2}$. These serve to analyze the
values taken by $\kappa_{2}(x_{1},x_{2},x_{3},x_{4},x_{5})$ for different
combinations of feature values, starting from $\mathbf{x}=(0,0,1,0,1)$.

######  Example 7 (NN).

The third running example is an NN, as shown in Figure 3. For this example,
${\mathcal{F}}_{3}=\\{1,2\\}$,
$\mathbb{D}=\\{{\mathcal{D}}_{31},{\mathcal{D}}_{32}\\}$, with
${\mathcal{D}}_{31}={\mathcal{D}}_{32}=\\{0,1\\}$, and so
$\mathbb{F}_{3}=\\{0,1\\}^{2}$, ${\mathcal{K}}=\\{0,1\\}$, and
$\kappa_{3}(x_{1},x_{2})=(\max(x_{1}+x_{2}-0.5,0)>0)$. We also have, from (3):

$\begin{array}[]{l}\mathbf{A}^{1}=\left[\begin{matrix}-0.5&{+}1&{+}1\end{matrix}\right]\\\\[4.0pt]
\mathbf{x}^{0}=\left[\begin{matrix}1&x^{0}_{1}&x^{0}_{2}\end{matrix}\right]\\\\[4.5pt]
\mathbf{y}^{1}=\left[\begin{matrix}y^{1}_{1}\end{matrix}\right]=\mathbf{A}^{1}\cdot(\mathbf{x}^{0})^{\textnormal{T}}\\\
\end{array}$

It is easy to conclude that the classifier corresponds to the Boolean function
$f(x_{1},x_{2})=x_{1}\lor{x_{2}}$. This is confirmed by the truth table shown
in Figure 3(b). For this example, the instance considered is
$(\mathbf{v},c)=((1,0),1)$. $\hfill\triangleleft$

$x_{0}=1$$x_{1}$$x_{2}$ $\sum$
Sum$y_{1}=\sum_{i=0}^{n}w_{i}x_{i}$-0.5+1+1InputsReLU$t_{1}=\max(y_{1},0)$$y_{1}$$t_{1}$$\begin{array}[]{l}t_{1}=\max(x_{1}+x_{2}-0.5,0)\\\
o_{1}=\textnormal{ITE}(t_{1}>0,1,0)\\\ \end{array}$
---
(a) NN computing $\kappa(x_{1},x_{2})=x_{1}\lor{x_{2}}$

$x_{1}$ | $x_{2}$ | $y_{1}$ | $t_{1}$ | $o_{1}$
---|---|---|---|---
0 | 0 | -0.5 | 0 | 0
1 | 0 | 0.5 | 0.5 | 1
0 | 1 | 0.5 | 0.5 | 1
1 | 1 | 1.5 | 1.5 | 1

(b) Truth table

Figure 3: Simple neural network

######  Example 8 (Monotonic classifier).

The fourth and final running example is a monotonic classifier, adapted from
[240]. The goal is to predict a student’s grade given the grades on the
different components of assessment. The different grading components have
domain $\\{0,\ldots,10\\}$. It is also the case that
${F}\preccurlyeq{E}\preccurlyeq{D}\preccurlyeq{C}\preccurlyeq{B}\preccurlyeq{A}$,
where the operator $\preccurlyeq$ is used to represent the order between
different grades. The details of the classifier are summarized in Figure 4.
The classifier “predicts” a student’s grade given the grades in different
grading components, using the following formulas:

$\begin{array}[]{rcl}M&=&\textnormal{ite}(S\geq 9,A,\textnormal{ite}(S\geq
7,B,\textnormal{ite}(S\geq 5,C,\textnormal{ite}(S\geq
4,D,\textnormal{ite}(S\geq 2,E,F)))))\\\\[3.0pt]
S&=&\max\left[0.3\times{Q}+0.6\times{X}+0.1\times{H},R\right]\end{array}$

Also, it is clearly the case that,
$\kappa_{4}(\mathbf{x_{1}})\preccurlyeq\kappa_{4}(\mathbf{x}_{2})\textnormal{~{}if~{}$\mathbf{x}_{1}\leq\mathbf{x}_{2}$}$,
and so the classifier is monotonic. $\hfill\triangleleft$

Feature id |  Feature variable |  Feature name |  Domain
---|---|---|---
1 |  $Q$ |  Quiz |  $\\{0,\ldots,10\\}$
2 |  $X$ |  Exam |  $\\{0,\ldots,10\\}$
3 |  $H$ |  Homework |  $\\{0,\ldots,10\\}$
4 |  $R$ |  Project |  $\\{0,\ldots,10\\}$
(a) Features and domains

Variable | Meaning | Range
---|---|---
$S$ | Final score | $\in\\{0,\ldots,10\\}$
$\kappa(\cdot)\triangleq{M}$ | Student grade | $\in\\{A,B,C,D,E,F\\}$
(b) Definition of $\kappa_{4}$

Figure 4: Example of a monotonic classifier [240]

###  2.3 Non-Formal Explanations

As observed in Section 1, most of past work on XAI has studied non-formal
explainability approaches. We will briefly summarize the main ideas. The
interested reader is referred to the many surveys on the topic [1, 263, 310,
149, 309, 335, 299, 159, 160]. There is a burgeoning and fast growing body of
work on non-formal approaches for computing explanations. The best known
approaches offer no guarantees of rigor, and include model-agnostic approaches
or solutions based on saliency maps for neural networks.

##### Model-agnostic methods.

The most visible approaches for explaining ML models are model-agnostic
methods [301, 235, 302]. These can be organized into methods that learn a
simpler interpretable model, e.g. a linear model or a decision tree. This is
the case with LIME [301] and SHAP [235]. The difference between LIME and SHAP
is the approach used to learn the model, with LIME being based on iterative
sampling, and SHAP based on the _approximate_ computation of Shapley values.
(It should be underscored that the Shapley values in SHAP are not computed
exactly, but only approximated. Indeed, the complexity of exactly computing
Shapley values is unwieldy [72, 20], with one exception being a fairly
restricted form of boolean circuits [20], referred to as deterministic,
decomposable boolean circuits [100], and which capture binary decision
trees131313Earlier work [234] also investigated the exact computation of
Shapley values for decision trees. However, issues about the proposed
algorithm have been raised by more recent work [20, 72].. These model agnostic
methods can also be viewed as associating a measure of relative importance to
each features, being often referred to as _feature attribution_ methods. One
alternative model-agnostic approach is to identify which features are the most
relevant for the prediction. We refer to such approaches as _feature
selection_ methods. One concrete example is Anchor [302]. Similar to other
model agnostic approaches, Anchor is based on sampling. It should be noted
that model-agnostic approaches exhibit a number of important drawbacks, the
most critical of which is unsoundness [180, 272, 170]. Despite critical
limitations, including the risk of unsound explanations, the impact of these
tools can only be viewed as impressive141414See for example
https://bit.ly/3eXIiNU, https://bit.ly/3BJL4z7, and https://bit.ly/3djA1Do..

##### Neural networks & saliency maps.

In the concrete case of neural networks, past work proposed the use of
variants of saliency maps [322, 310, 263, 309], that give a graphical
interpretation of a prediction. One popular approach is based on so-called
layerwise relevancy propagation [36]. However, recent work has revealed
important drawbacks of these approaches [2, 209, 350, 325].

##### Intrinsic interpretability.

Some authors have advocated the use of so-called _interpretable_ ML models,
for which the explanation is the model itself [304, 262, 305, 230, 314, 77,
43, 357]. For example, it is widely accepted that decision trees are
interpretable. Claims about the interpretability of decision trees go back at
least until the early 2000s [69, Sec. 9, Page 206]. Motivated by their
interpretability, decision trees have been applied to a wide range of domains,
including the medical domain [333, 340, 224]. Unfortunately, recent results
[187] demonstrate that decision trees can hardly be deemed interpretable, at
least as long as interpretability correlates with the succinctness of
explanations. Interpretability of decision lists and sets is at least as
problematic as it is for decision trees. If that were not the case, then one
would be able to just represent DTs as DLs or DSs [303]. The bottom line is
that even interpretable ML models should be explained, as the comprehensive
results in earlier work [187] demonstrate.

##### Assessment.

A number of additional limitations of non-formal explanations have been
reported in recent years [75, 326, 221, 108, 189, 135, 216]. Furthermore, a
number of authors have raised concerns about the current uses of XAI and its
technology [268, 274, 199], with examples of misuse also reported [184].

##  3 Formal Explainability

Formal explanation approaches have been studied in a growing body of research
in recent years [320, 178, 321, 179, 180, 272, 362, 96, 170, 97, 171, 177, 29,
319, 298, 64, 186, 239, 38, 186, 240, 191, 237, 174, 24, 84, 65, 166, 25, 19,
61, 232, 11, 164, 297, 355, 101, 189, 242, 165, 172, 145, 99, 28, 59, 60, 13,
26, 122, 233, 219, 21, 187, 27, 98, 354, 190, 367, 168, 192, 22, 185, 85, 167,
368, 163, 40, 12]. This section introduces formal explanations and describes
some of their properties.

##### Explanation problems.

Given a classifier
${\mathcal{M}}=({\mathcal{F}},\mathbb{D},\mathbb{F},{\mathcal{K}},\kappa)$, we
consider two explanation problems. First, we mostly study a given _local_
explanation problem ${\mathcal{E}}_{L}=({\mathcal{M}},\mathbf{v},c)$, with
$\mathbf{v}\in\mathbb{F}$, $c\in{\mathcal{K}}$ and $c=\kappa(\mathbf{v})$,
which respects a concrete point in feature space, i.e. a concrete prediction.
Second, we will also consider a _global_ explanation problem
${\mathcal{E}}_{G}=({\mathcal{M}},c)$, with $c\in{\mathcal{K}}$, which
respects solely a concrete prediction $c$, that can be predicted in many
points of feature space.

As a result, a tuple $({\mathcal{M}},(\mathbf{v},c))$ will allow us to
unambiguously represent the classification problem ${\mathcal{M}}$ for which
we want to compute the local AXp’s and CXp’s given the instance
$(\mathbf{v},c)$. Similarly, $({\mathcal{M}},c)$ also unambiguously represents
the classification problem for which we want to compute the global AXp’s given
the prediction $c$.

###  3.1 Abductive Explanations

This paper uses the definition of _abductive explanation_ [178] (AXp), which
corresponds to a PI-explanation [320] in the case of boolean classifiers.
AXp’s represent prime implicants of the discrete-valued classifier function
(which computes the predicted class)151515There exist also standard references
with detailed overviews of the uses of prime implicants in the context of
boolean functions [151, 87]. Generalizations of prime implicants beyond
boolean domains have been considered before [249]. Prime implicants have also
been referred to as minimum satisfying assignments in first-order logic (FOL)
[107], and have been studied in modal and description logics [54]. . AXp’s can
also be viewed as an instantiation of logic-based abduction [128, 313, 73,
111]. Throughout this paper we will opt to use the acronym AXp to refer to
abductive explanations.

Let us consider a given classifier, computing a classification function
$\kappa$ on feature space $\mathbb{F}$, a point $\mathbf{v}\in\mathbb{F}$,
with prediction $c=\kappa(\mathbf{v})$, and let ${\mathcal{X}}$ denote a
subset of the set of features ${\mathcal{F}}$,
${\mathcal{X}}\subseteq{\mathcal{F}}$. ${\mathcal{X}}$ is a weak AXp for the
instance $(\mathbf{v},c)$ if,

$\begin{array}[]{rcl}\mathsf{WeakAXp}({\mathcal{X}})&~{}:={}{}&\forall(\mathbf{x}\in\mathbb{F}).\left[\bigwedge_{i\in{\mathcal{X}}}(x_{i}=v_{i})\right]\operatorname*{\rightarrow}(\kappa(\mathbf{x})=c)\\\
\end{array}$ (4)

(We could highlight that $\mathsf{WeakAXp}$ is parameterized on $\kappa$,
$\mathbf{v}$ and $c$, but opt not to clutter the notation, and so these
dependencies will be left implicit.) Thus, given an instance $(\mathbf{v},c)$,
a (weak) AXp is a subset of features which, if fixed to the values dictated by
$\mathbf{v}$, then the prediction is guaranteed to be $c$, independently of
the values assigned to the other features.

######  Example 9.

With respect to the DL of Figure 1, it is apparent that
${\mathcal{X}}=\\{1,4\\}$ is a (weak) abductive explanation for the instance
$(\mathbf{v},c)=((0,0,1,2),1)$. Indeed, if $(x_{1}=0)\land(x_{4}=2)$, then the
prediction will be 1, independently of the values taken by the other features.
This can easily be concluded from Table 1; if $x_{1}$ and $x_{4}$ are fixed,
then the possible entries are 02, 05, 08 and 11, all with prediction 1. Hence,
we can write that,

$\forall(\mathbf{x}\in\mathbb{F}_{1}).\left[(x_{1}=0)\land(x_{4}=2)\right]\operatorname*{\rightarrow}(\kappa_{1}(\mathbf{x})=1)$

Observe that any set ${\mathcal{Z}}$, with
${\mathcal{X}}\subseteq{\mathcal{Z}}\subseteq{\mathcal{F}}$, is also a weak
AXp. $\hfill\triangleleft$

Moreover, ${\mathcal{X}}\subseteq{\mathcal{F}}$ is an AXp if, besides being a
weak AXp, it is also subset-minimal, i.e.

$\begin{array}[]{rcl}\mathsf{AXp}({\mathcal{X}})&~{}:={}{}&\mathsf{WeakAXp}({\mathcal{X}})\land\forall({\mathcal{X}}^{\prime}\subsetneq{\mathcal{X}}).\neg\mathsf{WeakAXp}({\mathcal{X}}^{\prime})\\\
\end{array}$ (5)

######  Example 10.

From Table 1, and given the weak AXp $\\{1,4\\}$ (see Example 9) it is also
possible to conclude that if either $x_{1}$ or $x_{4}$ are allowed to change
their value, then the prediction can be changed. Hence,
${\mathcal{X}}=\\{1,4\\}$ is effectively an AXp. $\hfill\triangleleft$

Observe that an AXp can be viewed as a possible irreducible answer to a “Why?”
question, i.e. why is the classifier’s prediction $c$? It should be plain in
this work, but also in earlier work, that the representation of AXp’s using
subsets of features aims at simplicity. The sufficient condition for the
prediction is evidently the conjunction of literals associated with the
features contained in the AXp.

The following example demonstrates the importance of explaining decision
trees, even if these are most often deemed interpretable.

######  Example 11.

We consider the DT from Figure 2, and the instance $((0,0,1,0,1),1)$.
Intrinsic interpretability [304, 262] would argue that the explanation for
this instance is the path consistent with the instance. Hence, we would claim
that,

$\begin{array}[]{cccc}\textnormal{IF~{}}&[(x_{1}=0)\land(x_{2}=0)\land(x_{3}=1)\land(x_{4}=0)\land(x_{5}=1)]&\textnormal{~{}THEN~{}}&1\\\
\end{array}$

However, Table 2 clarifies that, as long as features 3 and 5 are assigned the
same value, then the prediction remains unchanged. Hence, a far more
_intuitive_ explanation would be,

$\begin{array}[]{cccc}\textnormal{IF~{}}&[(x_{3}=1)\land(x_{5}=1)]&\textnormal{~{}THEN~{}}&1\\\
\end{array}$

Clearly, the (only) AXp for the given instance is exactly that one, i.e.
${\mathcal{X}}=\\{3,5\\}$, and we can state,

$\forall(\mathbf{x}\in\mathbb{F}_{2}).\left[(x_{3}=1)\land(x_{5}=1)\right]\operatorname*{\rightarrow}(\kappa_{2}(\mathbf{x})=1)$

$\hfill\triangleleft$

Example 11 illustrates important limitations of DTs in terms of
interpretability, and justifies recent work on explaining DTs [186, 188, 187].
More importantly, it has been shown that the redundancy in tree paths (i.e.
features unnecessary for the prediction) can be arbitrarily large on the
number of features [187]. Given the recent efforts on learning optimal (and
quasi-optimal) “interpretable” models [275, 52, 276, 356, 220, 51, 17, 358,
18, 348, 306, 78, 271, 181, 238, 138, 349, 162, 32, 33, 346, 4, 228, 196, 161,
347, 5, 136, 365, 366, 173, 106, 312, 280, 352, 318, 10, 105, 137, 353, 255],
that include learning optimal decision trees and sets, recent results
demonstrate [174, 187] that even such optimal and interpretable models should
be explained.

###  3.2 Contrastive Explanations

Similarly to the case of AXp’s, one can define (weak) contrastive explanations
(CXp’s) [261, 177]. ${\mathcal{Y}}\subseteq{\mathcal{F}}$ is a weak CXp for
the instance $(\mathbf{v},c)$ if,

$\begin{array}[]{rcl}\mathsf{WeakCXp}({\mathcal{Y}})&~{}:={}{}&\exists(\mathbf{x}\in\mathbb{F}).\left[\bigwedge_{i\not\in{\mathcal{Y}}}(x_{i}=v_{i})\right]\land(\kappa(\mathbf{x})\not=c)\\\
\end{array}$ (6)

(As before, for simplicity we keep the parameterization of $\mathsf{WeakCXp}$
on $\kappa$, $\mathbf{v}$ and $c$ implicit.) Thus, given an instance
$(\mathbf{v},c)$, a (weak) CXp is a subset of features which, if allowed to
take any value from their domain, then there is an assignment to the features
that changes the prediction to a class other than $c$, this while the features
not in the explanation are kept to their values (_ceteris paribus_).

######  Example 12.

For the DT of Figure 2, and the instance $(\mathbf{v},c)=((0,0,1,0,1),1)$, it
is the case that ${\mathcal{Y}}=\\{3\\}$ is a (weak) contrastive explanation.
Indeed, if we allow the value of feature 3 to change, then there exists some
point in feature space, e.g. $(0,0,0,0,1)$, for which the remaining features
take the values in $\mathbf{v}$, and such that the prediction changes to 0.
Hence, we can write,

$\exists(\mathbf{x}\in\mathbb{F}_{2}).\left[(x_{1}=0)\land(x_{2}=0)\land(x_{4}=0)\land(x_{5}=1)\right]\land(\kappa_{2}(\mathbf{x})\not=1)$

Intuitively, we are saying that it suffices to change the value of feature 3
to get a different prediction. $\hfill\triangleleft$

Furthermore, a set ${\mathcal{Y}}\subseteq{\mathcal{F}}$ is a CXp if, besides
being a weak CXp, it is also subset-minimal, i.e.

$\begin{array}[]{rcl}\mathsf{CXp}({\mathcal{Y}})&~{}:={}{}&\mathsf{WeakCXp}({\mathcal{Y}})\land\forall({\mathcal{Y}}^{\prime}\subsetneq{\mathcal{Y}}).\neg\mathsf{WeakCXp}({\mathcal{Y}}^{\prime})\\\
\end{array}$ (7)

######  Example 13.

For the DL of Figure 1, it is plain that if $x_{1}$ is allowed to change value
(i.e. entry 14 of Table 1) or if $x_{4}$ is allowed to change value (i.e.
entry 01 of Table 1), then the prediction will change. Hence, either $\\{1\\}$
or $\\{4\\}$ are weak contrastive explanations for the given instance.
Furthermore, both weak CXp’s are irreducible, and so both are effectively
CXp’s. $\hfill\triangleleft$

A CXp can be viewed as a possible irreducible answer to a “Why Not?” question,
i.e. why isn’t the classifier’s prediction a class other than $c$? A different
perspective for a contrastive explanation is as the answer to a _How?_
question, i.e. how to change the features so as to change the prediction. In
recent literature this alternative view has been investigated under the name
_actionable recourse_ [339, 345, 201, 200]. It should be underlined that
whereas AXp’s correspond to prime implicants of the boolean function
$(\kappa(\mathbf{x})=c)$ that are consistent with some point
$\mathbf{v}\in\mathbb{F}$, CXp’s are _not_ prime implicates of function
$(\kappa(\mathbf{x})=c)$. Nevertheless, the concept of _counterexample_
studied in formal explainability [178] corresponds to prime implicates of the
function $(\kappa(\mathbf{x})=c)$ (which are not restricted to be consistent
with some specific point $\mathbf{v}\in\mathbb{F}$).

One important observation is that, independently of what $\kappa$ represents,
the $\mathsf{WeakAXp}$ and $\mathsf{WeakCXp}$ predicates (respectively defined
using (4) and (6)) are _monotone_ 161616Clearly, from the definition of
$\mathsf{WeakAXp}$ (resp. $\mathsf{WeakCXp}$), if
$\mathsf{WeakAXp}({\mathcal{Z}})$ (resp. $\mathsf{WeakCXp}({\mathcal{Z}})$)
holds, then $\mathsf{WeakAXp}({\mathcal{Z}}^{\prime})$ (resp.
$\mathsf{WeakCXp}({\mathcal{Z}}^{\prime})$) also holds for any superset
${\mathcal{Z}}^{\prime}$ of ${\mathcal{Z}}$. If
$\mathsf{WeakAXp}({\mathcal{Z}})$ (resp. $\mathsf{WeakCXp}({\mathcal{Z}})$)
does not hold, then $\mathsf{WeakAXp}({\mathcal{Z}}^{\prime})$ (resp.
$\mathsf{WeakCXp}({\mathcal{Z}}^{\prime})$) also does not hold for any subset
${\mathcal{Z}}^{\prime}$ of ${\mathcal{Z}}$.. This means that the tests for
minimality (i.e., respectively (5) and (7)) can be simplified to:

$\begin{array}[]{rcl}\mathsf{AXp}({\mathcal{X}})&~{}:={}{}&\mathsf{WeakAXp}({\mathcal{X}})\land\forall(t\in{\mathcal{X}}).\neg\mathsf{WeakAXp}({\mathcal{X}}\setminus\\{t\\})\\\
\end{array}$ (8)

and,

$\begin{array}[]{rcl}\mathsf{CXp}({\mathcal{Y}})&~{}:={}{}&\mathsf{WeakCXp}({\mathcal{Y}})\land\forall(t\in{\mathcal{Y}}).\neg\mathsf{WeakCXp}({\mathcal{Y}}\setminus\\{t\\})\\\
\end{array}$ (9)

Observe that, instead of considering all possible subsets of ${\mathcal{X}}$
(resp. ${\mathcal{Y}}$), it suffices to consider the subsets obtained by
removing a single element from ${\mathcal{X}}$ (resp. ${\mathcal{Y}}$). This
observation is at the core of the algorithms proposed in recent years for
computing AXp’s and CXp’s of a growing range of families of classifiers [178,
179, 272, 239, 186, 240, 191, 237, 166, 174, 164]. As will be clarified in
Section 4, the computation of AXp’s can be related with MUS extraction, and
the computation of CXp’s can be related with MCS extraction.

Given a local explanation problem ${\mathcal{E}}$, the sets of AXp’s and CXp’s
are defined as follows,

$\displaystyle\mathbb{A}({\mathcal{E}})$
$\displaystyle=\\{{\mathcal{X}}\subseteq{\mathcal{F}}\,|\,\mathsf{AXp}(X)\\}$
(10) $\displaystyle\mathbb{C}({\mathcal{E}})$
$\displaystyle=\\{{\mathcal{Y}}\subseteq{\mathcal{F}}\,|\,\mathsf{CXp}(X)\\}$
(11)

###  3.3 Global Abductive Explanations & Counterexamples

The definition of AXp’s considered until now is _localized_ , in that it takes
a concrete point $\mathbf{v}$ into account. However, abductive explanations
can be defined only with respect to the class, and ignore concrete points in
feature space; these are referred to as global AXp’s. Following [179], let
$\pi:\mathbb{F}\to\\{0,1\\}$, represent a term that is a prime implicant of
the predicate $[\kappa(\mathbf{x})=c]$, i.e.,

$\forall(\mathbf{x}\in\mathbb{F}).\pi(\mathbf{x})\operatorname*{\rightarrow}\left(\kappa(\mathbf{x})=c\right)$

(Each literal will be of the form $x_{i}=u_{i}$, where $u_{i}$ is taken from
${\mathcal{D}}_{i}$.) The set of literals of $\pi$ is a global abductive
explanation of the prediction $c$.

We are also interested in the prime implicates of the predicate
$[\kappa(\mathbf{x})=c]$, which will be convenient to represent by $\neg\eta$,
where $\eta$ is a term $\eta:\mathbb{F}\to\\{0,1\\}$,

$\forall(\mathbf{x}\in\mathbb{F}).\left(\kappa(\mathbf{v})=c\right)\operatorname*{\rightarrow}\left[\neg\eta(\mathbf{x})\right]$

This statement can be rewritten as follows,

$\forall(\mathbf{x}\in\mathbb{F}).\eta(\mathbf{x})\operatorname*{\rightarrow}\left(\kappa(\mathbf{v})\not=c\right)$

The set of literals in $\eta$ is referred to as a _counterexample_ (CEx) for
the prediction $c$, and represents the negation of a prime implicate for the
predicate $[\kappa(\mathbf{x})=c]$. Clearly, both global AXp’s and CEx’s are
irreducible (and so subset-minimal).

######  Example 14.

For the DL of Figure 1(a), let $c=0$, i.e. the predicted class is 0. It is
plain that the predicted class is 0 whenever $x_{1}=1$. Thus,
$\\{(x_{1}=1)\\}$ is a global abductive explanation for class $c=0$.
Similarly, if $x_{2}=0$ and $x_{4}=1$, then the predicted class is again
guaranteed to be 0. Thus, the other global abductive explanation is
$\\{(x_{2}=0),(x_{4}=1)\\}$. We could use minimal hitting set duality between
prime implicants and implicates [307] to list the counterexamples. However, we
can also directly reason in terms of the DL to uncover the CEx’s, as shown in
Table 3. $\hfill\triangleleft$

Global AXp’s |  $\\{\\{x_{1}=1\\},\\{x_{2}=0,x_{4}=1\\}\\}$
---|---
Counterexamples |  $\\{x_{1}=0,x_{2}=1\\},\\{x_{1}=0,x_{4}=0\\}$
Table 3: Global abductive explanations and counterexamples for the DL of
Figure 1(a).

(Local) AXp’s, CXp’s and global AXp’s and CEx’s reveal important relationships
between prime implicants and implicates, as discussed later in Section 3.5.

###  3.4 Duality Results

This section overviews duality results in formal explainability, which have
been established in recent years [177, 179].

##### Duality between AXp’s and CXp’s.

Given the definition of sets of AXp’s and CXp’s (see (10) and (11)), and by
building on Reiter’s seminal work [300], recent work [177] proved the
following duality between minimal hitting sets:

######  Proposition 5 (Minimal hitting-set duality between AXp’s and CXp’s).

Given a local explanation problem ${\mathcal{E}}$, we have that,

  1. 1.

${\mathcal{X}}\subseteq{\mathcal{F}}$ is an AXp (and so
${\mathcal{X}}\in\mathbb{A}({\mathcal{E}})$) iff ${\mathcal{X}}$ is an MHS of
the CXp’s in $\mathbb{C}({\mathcal{E}})$.

  2. 2.

${\mathcal{Y}}\subseteq{\mathcal{F}}$ is a CXp (and so
${\mathcal{X}}\in\mathbb{C}({\mathcal{E}})$) iff ${\mathcal{Y}}$ is an MHS of
the AXp’s in $\mathbb{A}({\mathcal{E}})$.

We refer to Proposition 5 as MHS duality between AXp’s and CXp’s. The previous
result has been used in more recent papers for enabling the enumeration of
explanations [240, 174, 166].

######  Example 15.

For the DL of Example 5, and the instance $(\mathbf{v},c)=((0,0,1,2),1)$, we
have argued (see Examples 9, 10 and 13) that an AXp is $\\{1,4\\}$ and that
$\\{1\\}$ and $\\{4\\}$ are CXp’s. Clearly, the AXp is a MHS of the CXp’s and
vice-versa. Hence, we have listed all the AXp’s and CXp’s for this instance.
$\hfill\triangleleft$

Furthermore, a consequence of Proposition 5 is the following result:

######  Proposition 6.

Given a classifier function $\kappa:\mathbb{F}\to{\mathcal{K}}$, defined on a
set of features ${\mathcal{F}}$, a feature $i\in{\mathcal{F}}$ is included in
some AXp iff $i$ is included in some CXp.

##### Duality between global AXp’s and counterexamples [179].

Another minimal hitting-set duality result, different from Proposition 5, was
investigated in earlier work [179], and relates _global_ AXp’s (i.e. not
restricted to be consistent with a specific point $\mathbf{v}\in\mathbb{F}$)
and counterexamples (see also Example 13). Given the definition of (global)
AXp’s and CEx’s (see Section 3.3), we say that two sets of literals _break_
each other if these have inconsistent literals. Furthermore, [179] proves the
following result,

######  Proposition 7.

For a global explanation problem, every CEx breaks every global AXp and vice-
versa.

######  Example 16.

From Example 14, it is plain to conclude (see Table 3) that each global
abductive explanation breaks each counterexample and vice-versa.
$\hfill\triangleleft$

###  3.5 Additional Notes

##### Relationship with non-formal explainability.

Past work has shown how formal explanations can serve to assess the quality or
rigor of non-formal explanations [180, 272, 170]. For example, a non-formal
explanation can be _corrected_ and made subset-minimal, using the non-formal
explanation as a starting point for the computation of some other, formal,
explanations [180, 170]. Moreover, some authors have recently noticed what is
referred to as the _disagreement problem in XAI_ [216]. From the perspective
of formal explainability, differences in explanations just represent different
AXp’s, which can exist. More important, as discussed in Section 6, it is
conceptually feasible, and often practically efficient, to navigate the space
of explanations.

##### Literals based on the equality operator.

As can be observed, both running examples use literals of the form
$(x_{i}=u_{i})$. The same applies to the definitions of (weak) AXp’s and
CXp’s. This need not be the case, as discussed elsewhere [187]. In the case of
DTs, more general literals have been associated with explanations [187], e.g.
by describing literals using set membership. Nevertheless, and for simplicity,
in this document we will use literals that use solely the equality operator.

##### Prime implicants & implicates vs. MUSes & MCSes.

For global abductive explanations, the duality result established in earlier
work [179] essentially relates prime implicants and implicates of some boolean
function $\varsigma:\mathbb{F}\to\\{0,1\\}$, with
$\varsigma(\mathbf{x})=(\kappa(\mathbf{x})=c)$. In contrast, the duality
results established in more recent work [177] relate localized AXp’s and
CXp’s, and can instead be viewed as relating MUSes and MCSes of some
inconsistent formula (see Section 4 for additional detail). These results
reveal a more fine-grained relationship between prime implicants and prime
implicates, than what is proposed in earlier work [307, 288].

##### Formal explainability and model-based diagnosis.

Although we approach formal explainability as a problem of abduction, there
are other possible ways to represent the problem of explainability. One well-
known example is model-based diagnosis (MBD) [300]. We consider a system
description $\mathsf{SD}$ consisting of a set of first-order logic statements,
and a set of constants $\mathsf{Comp}$, representing the system’s components.
Each component may or may not be operating correctly, and we use a predicate
$\mathsf{Ab}$ to indicate whether the component $C_{j}$ is operating
incorrectly (i.e. $\mathsf{Ab}(C_{j})$ holds, denoting abnormal behavior), or
correctly (i.e. $\neg\mathsf{Ab}(C_{j})$ holds, denoting normal behavior).
Furthermore, we also assume some observation $\mathsf{Obs}$ about the system’s
expected behavior. In a diagnosis scenario, where $\mathsf{Obs}$ disagrees
with expected result, it is the case that,

$\mathsf{SD}\cup\\{\neg\mathsf{Ab}(C_{1}),\neg\mathsf{Ab}(C_{2}),\ldots,\neg\mathsf{Ab}(C_{n})\\}\cup\mathsf{Obs}\operatorname*{\,\vDash}\bot$
(12)

A conflict set is a (subset)-minimal set $\mathsf{CS}$ of $\mathsf{Comp}$ such
that,

$\mathsf{SD}\cup\\{\neg\mathsf{Ab}(C_{i})\,|\,C_{i}\in\mathsf{CS}\\}\cup\mathsf{Obs}\operatorname*{\,\vDash}\bot$
(13)

A diagnosis is a subset-minimal set $\Delta$ of $\mathsf{Comp}$ such that,

$\mathsf{SD}\cup\\{\neg\mathsf{Ab}(C_{i})\,|\,C_{i}\in\mathsf{Comp}\setminus\Delta\\}\cup\mathsf{Obs}\operatorname*{\,\nvDash}\bot$
(14)

A simple reduction of the problem of finding abductive explanations to model
based diagnosis, can be organized as follows:

  1. 1.

$\mathsf{SD}$ is given by,
$\llbracket\land_{i\in{\mathcal{F}}}[(x_{i}=v_{i})\lor\mathsf{Ab}(i)]\rrbracket$,
where $\llbracket\cdot\rrbracket$ denotes a logic encoding in a suitable logic
theory.

  2. 2.

$\mathsf{Obs}$ is given by $\llbracket\kappa(\mathbf{x})\not=c\rrbracket$.

Clearly, if all components operate correctly, then the system description is
inconsistent with the stated observation, as expected. (And in this case the
stated observation is _not_ observing $c$.) Furthermore, it is easy to see
that a minimal conflict is an abductive explanation, and a minimal diagnosis
is a contrastive explanation. It should be underlined that the proposed
reduction aims at simplicity, but it can also be perceived as somewhat
artificial. Clearly, the computation of $\kappa$ could be deemed part of the
system description, such that its operation was forced to be correct. Other
variations could be envisioned. Given the progress observed in MBD in recent
years [258, 244], it would be interesting to assess the scalability of MBD
tools in the context of explainability.

###  3.6 A Timeline for Formal Explainability

Figure 5 depicts the evolution in time of the main areas of research in formal
explainability.

Week 020192020202120222023XP definitionsAXp, CXp, dualityTractabilityDTs,
NBCs, etc.Efficient solutionsRFs, DLs, BTs, etc.QueriesMember., Enum.,
etc.Input distrib.Inp. constr.Prob. XPsDTs, NBCs, etc.New topicsDistil., etc.

Figure 5: A timeline of research on formal explainability

The initial focus (in 2019-2020) was on the definition of explanations,
duality results, but also approaches for the computation of explanations. The
next major effort (in 2020-2021) was on classifiers exhibiting tractable
computation of one explanation. This was soon followed by efforts on the
efficient computation of explanations even when the computation of
explanations was computationally hard (in 2021-2022). More recently, there has
been research on addressing different explainability queries (in 2021-2022),
tackling input distributions (started in 2022), and computing probabilistic
explanations in practice (also started in 2022). There are additional topics
of research, which are also discussed in this document. Although there is
ongoing research in most areas of research shown in Figure 5, it is also the
case that the most recent topics exhibit more open research questions. The
rest of this paper, overviews the areas of research in formal explainability
shown in Figure 5.

##  4 Computing Explanations

This section covers the computation of explanations, both abductive and
contrastive. The focus are on families of classifiers for which computing one
explanation is computationally hard. The next section covers families of
classifiers for which there exist polynomial-time algorithms for computing one
abductive/contrastive explanation.

###  4.1 Progress in Computing Explanations

Since 2019, there has been steady progress in the practical efficiency of
computing formal explanations. Figure 6 summarizes the observed progress.

NBCs [239]DTs [186, 188]XpGs [166]GDFs [166]Monotonic [240, 84]d-DNNF [165]DLs
[174]RFs [191]BTs [170, 172]NNs [178]BNs [320]Practical scalability
(effectiveness)EffectiveIneffectiveComputational complexityComputationally
hardPoly-timeComputing one XP

Figure 6: Progress in formal explainability

For some families of classifiers, including decision trees, graphs and
diagrams, naive bayes classifiers, monotonic classifiers, restricted
propositional language classifiers and others, it has been shown that
computing one AXp is tractable [239, 186, 240, 166, 84, 165, 188]. For some
other families of classifiers, e.g. decision lists and sets, random forests
and tree ensembles, it has been established the computational hardness of
computing one AXp [191, 174]. However, and also for these families of
classifiers, existing logical encodings enable the efficient computation of
one AXp [180, 170, 191, 174, 172] in practice. Finally, for a few other
families of classifiers [320, 178], computing one AXp is not only
computationally hard, but existing algorithms are not efficient in practice,
at least for large scale ML models. The next sections analyze some of these
results in more detail.

###  4.2 General Oracle-Based Approach

The main approach for computing explanations is based on exploiting automated
reasoners (e.g. SAT, SMT, MILP, etc.) as oracles. We start by analyzing how to
decide whether a subset ${\mathcal{X}}$ of features is a weak AXp. From (4),
negating twice, we get:

$\neg\exists(\mathbf{x}\in\mathbb{F}).\left[\bigwedge\nolimits_{i\in{\mathcal{X}}}(x_{i}=v_{i})\right]\land(\kappa(\mathbf{x})\not=c)\\\
$

This corresponds to deciding the consistency of a logic formula, as follows:

$\neg\operatorname*{\textnormal{{{CO}}}\\!}\left(\left\llbracket{\left[\bigwedge\nolimits_{i\in{\mathcal{X}}}(x_{i}=v_{i})\right]\land(\kappa(\mathbf{x})\not=c)}\right\rrbracket_{{\mathcal{T}}}\right)$

The computation of a single AXp or a single CXp can be achieved by adapting
existing algorithms provided a few requirements are met. First, reasoning in
theory ${\mathcal{T}}$ is required to be monotone, i.e.  _in_ consistency is
preserved if constraints are added to a set of constraints, and consistency is
preserved if constraints are removed from a set of constraints. Second, for
computing one AXp, the predicate to consider is:

$\mathbb{P}_{\textnormal{axp}}({\mathcal{S}};{\mathcal{T}},{\mathcal{F}},\kappa,\mathbf{v})\triangleq\neg\operatorname*{\textnormal{{{CO}}}\\!}\left(\left\llbracket\left(\bigwedge\nolimits_{i\in{\mathcal{S}}}(x_{i}=v_{i})\right)\land(\kappa(\mathbf{x})\not=c)\right\rrbracket\right)$
(15)

and for computing one CXp, the predicate to consider is:

$\mathbb{P}_{\textnormal{cxp}}({\mathcal{S}};{\mathcal{T}},{\mathcal{F}},\kappa,\mathbf{v})\triangleq\operatorname*{\textnormal{{{CO}}}\\!}\left(\left\llbracket\left(\bigwedge\nolimits_{i\in{\mathcal{F}}\setminus{\mathcal{S}}}(x_{i}=v_{i})\right)\land(\kappa(\mathbf{x})\not=c)\right\rrbracket\right)$
(16)

where, the starting set ${\mathcal{S}}$ can be any set that respects the
invariant of the predicate for which it serves as an argument. For example,
for computing a AXp, ${\mathcal{S}}$ can represent any weak AXp, and for
computing a CXp, ${\mathcal{S}}$ can represent any weak CXp. (Similar to the
case of $\operatorname*{\textnormal{{{CO}}}}$, $\mathbb{P}_{\textnormal{axp}}$
and $\mathbb{P}_{\textnormal{cxp}}$ are parameterized by ${\mathcal{T}}$,
${\mathcal{F}}$, $\kappa$, $\mathbf{v}$, and also $c=\kappa(\mathbf{v})$. For
simplicity, this parameterization will be left implicit when convenient. Also,
the parameterization on $c=\kappa(\mathbf{v})$, given the ones on $\kappa$ and
$\mathbf{v}$.) Observe that, since (4) and (6) are monotone, then
$\mathbb{P}_{\textnormal{axp}}$ and $\mathbb{P}_{\textnormal{cxp}}$ are also
monotone with respect to set ${\mathcal{S}}$.

Input: Seed ${\mathcal{S}}\subseteq{\mathcal{F}}$, parameters $\mathbb{P}$,
${\mathcal{T}}$, ${\mathcal{F}}$, $\kappa$, $\mathbf{v}$

Output: One XP ${\mathcal{W}}$

1:procedure
$\mathsf{oneXP}$(${\mathcal{S}};\mathbb{P},{\mathcal{T}},{\mathcal{F}},\kappa,\mathbf{v}$)

2: ${\mathcal{W}}\leftarrow{\mathcal{S}}$ $\triangleright$ Initialization:
$\mathbb{P}({\mathcal{W}})$ holds

3: for $i\in{\mathcal{S}}$ do $\triangleright$ Loop invariant:
$\mathbb{P}({\mathcal{W}})$ holds

4: if
$\mathbb{P}({\mathcal{W}}\setminus\\{i\\};{\mathcal{T}},{\mathcal{F}},\kappa,\mathbf{v})$
then

5: ${\mathcal{W}}\leftarrow{\mathcal{W}}\setminus\\{i\\}$ $\triangleright$
Update ${\mathcal{W}}$ only if $\mathbb{P}({\mathcal{W}}\setminus\\{i\\})$
holds

6: return ${\mathcal{W}}$ $\triangleright$ Returned set ${\mathcal{W}}$:
$\mathbb{P}({\mathcal{W}})$ holds

Algorithm 1 Finding one AXp/CXp

Moreover, the monotonicity of $\mathbb{P}_{\textnormal{axp}}$ and
$\mathbb{P}_{\textnormal{cxp}}$ enables adapting standard algorithms for
computing one explanation. Algorithm 1 illustrates one possible
approach171717This algorithm is referred to as the _deletion-based_ algorithm
[79], but it can be traced back to the work of Valiant [341] (and some authors
[197] argue that it is implicit in works from the $\text{19}^{\text{th}}$
century [259]). Although variants of Algorithm 1 are most often used in
practical settings, there are several alternative algorithms that can also be
used, including QuickXplain [198], Progression [243], or even insertion-based
[323], among others [44, 34]. As illustrated by Algorithm 1, it is now known
that most of these algorithms can be formalized in an abstract way, thus
allowing them to be used to solve subset-minimal problems when these problems
can be represented by monotonic predicates [245]. As argued earlier,
predicates $\mathbb{P}_{\textnormal{axp}}$ (see Equation 15) and
$\mathbb{P}_{\textnormal{cxp}}$ (see Equation 16) are both monotonic.. For
computing one AXp or one CXp, the initial seed set ${\mathcal{S}}$ of
Algorithm 1 is set to ${\mathcal{F}}$. However, as long as the precondition
$\mathbb{P}({\mathcal{S}})$ holds, then any set
${\mathcal{S}}\subseteq{\mathcal{F}}$ can be considered.

######  Example 17.

We consider the DT of Figure 2, and both the computation of one AXp and one
CXp when ${\mathcal{S}}=\\{3,4,5\\}$. For the AXp, it is plain that if
features $\\{3,4,5\\}$ are fixed, then the prediction does not change (as
shown in Table 2(a)). Table 4 summarizes the execution of Algorithm 1 when
computing one AXp and one CXp, starting from a set of literals (i.e. the seed)
${\mathcal{S}}=\\{3,4,5\\}$. (Without additional information, we would start
from ${\mathcal{S}}={\mathcal{F}}$, and so the table would include a few more
lines.) The difference between the two executions is the result of the
predicate used. $\hfill\triangleleft$

${\mathcal{W}}$ |  $i$ |  $\mathbb{P}_{\textnormal{axp}}$ |  Decision
---|---|---|---
$\\{3,4,5\\}$ |  3 |  0 |  Keep 3
$\\{3,4,5\\}$ |  4 |  1 |  Drop 4
$\\{3,5\\}$ |  5 |  0 |  Keep 5
(a) Finding 1 AXp

${\mathcal{W}}$ |  $i$ |  $\mathbb{P}_{\textnormal{cxp}}$ |  Decision
---|---|---|---
$\\{3,4,5\\}$ |  3 |  1 |  Drop 3
$\\{4,5\\}$ |  4 |  1 |  Drop 4
$\\{5\\}$ |  5 |  0 |  Keep 5
(b) Finding 1 CXp

Table 4: Computation of 1 AXp and 1 CXp starting from seed
${\mathcal{S}}=\\{3,4,5\\}$. The partial truth tables in Tables 2(a) and 2(b)
can be used for computing both $\mathbb{P}_{\textnormal{axp}}$ and
$\mathbb{P}_{\textnormal{cxp}}$. Table 2(a) serves to validate whether the
prediction remains unchanged. Table 2(b) serves to assess whether there are
points in feature space for which the prediction changes.

In some settings, it may be relevant to compute one smallest AXp or one
smallest CXp. Computing one CXp can be achieved by computing a smallest(-cost)
MCS. Hence, a MaxSAT/MaxSMT reasoner can be used in this case. For AXp’s, and
given their relationship with MUSes, a different approach needs to be devised.
For a given theory ${\mathcal{T}}$, let

$\begin{array}[]{lcr}\mathsf{Decide}({\mathcal{X}})&\quad~{}{:={}}&\operatorname*{\textnormal{{{CO}}}\\!}\left(\left\llbracket{\left[\bigwedge\nolimits_{i\in{\mathcal{X}}}(x_{i}=v_{i})\right]\land(\kappa(\mathbf{x})\not=c)}\right\rrbracket_{{\mathcal{T}}}\right)\\\
\end{array}$ (17)

Furthermore, we assume that $\mathsf{Decide}({\mathcal{X}})$ returns a pair
$(\textnormal{{{outc}}},\mu)$, indicating whether the formula is indeed
consistent and, if it is, the computed assignment. Algorithm 2 illustrates the
use of dualization for computing one smallest AXp, and builds on earlier work
on computing smallest MUSes [182].

Input: Algorithm parameterized by ${\mathcal{T}}$, ${\mathcal{F}}$, $\kappa$,
$\mathbf{v}$

Output: Smallest AXp ${\mathcal{M}}$

1:procedure $\mathsf{minXP}$

2: ${\mathcal{H}}\leftarrow\emptyset$

3: while true do

4: ${\mathcal{M}}\leftarrow\mathsf{MinimumHS}({\mathcal{H}})$

5:
$(\textnormal{{{outc}}},\mu)\leftarrow\mathsf{Decide}({\mathcal{M}};{\mathcal{T}},{\mathcal{F}},\kappa,\mathbf{v})$

6: if $\mathbf{not~{}}\textnormal{{{outc}}}$ then

7: return ${\mathcal{M}}$

8: else

9:
${\mathcal{L}}\leftarrow\mathsf{PickFalseLits}({\mathcal{F}}\setminus{\mathcal{M}},\mu)$

10: ${\mathcal{H}}\leftarrow{\mathcal{H}}\cup{\mathcal{L}}$

Algorithm 2 Finding one smallest AXp

Any minimum-size hitting set such that the picked (fixed) features represent a
weak AXp must be a smallest AXp.

##### Relationship with MUSes & MCSes.

We can relate the computation of AXp’s and CXp’s respectively with the
extraction of MUSes and MCSes. We construct a formula
$\varphi={\mathcal{B}}\cup{\mathcal{S}}$ in some theory ${\mathcal{T}}$ where
the background knowledge ${\mathcal{B}}$ corresponds to,

$\displaystyle{\mathcal{B}}\triangleq\left\llbracket{\kappa(\mathbf{x})\not=c}\right\rrbracket_{{\mathcal{T}}}$
(18)

and the soft constraints ${\mathcal{S}}$ correspond to,

$\displaystyle{\mathcal{S}}\triangleq\left\\{\left\llbracket{x_{i}=v_{i}}\right\rrbracket_{{\mathcal{T}}}\,|\,i\in{\mathcal{F}}\right\\}$
(19)

Clearly, $\varphi={\mathcal{B}}\cup{\mathcal{S}}$ is inconsistent, i.e. if all
features are fixed, then the prediction must be $c$. As a result, an MUS
${\mathcal{U}}$ of ${\mathcal{B}}\cup{\mathcal{S}}$ (i.e. a subset of
${\mathcal{U}}$ of ${\mathcal{S}}$) is such that
${\mathcal{U}}\cup{\mathcal{S}}$ is inconsistent. Thus, ${\mathcal{U}}$
represents a subset-minimal set of features which, if fixed, ensure
inconsistency (and so the prediction must be $c$); hence, ${\mathcal{U}}$ is
an AXp. Similarly, an MCS ${\mathcal{C}}$ of ${\mathcal{B}}\cup{\mathcal{S}}$
(i.e. a subset of ${\mathcal{C}}$ of ${\mathcal{S}}$) is such that
${\mathcal{B}}\cup({\mathcal{S}}\setminus{\mathcal{C}})$ is consistent. Thus,
${\mathcal{C}}$ represents a subset-minimal set of features which, if allowed
to change their, ensure consistency (and so the prediction can be different
from $c$); hence, ${\mathcal{C}}$ is a CXp.

###  4.3 Explaining Decision Lists

This section details the computation of AXp’s/CXp’s in the case of DLs.
Furthermore, it is briefly mentioned the relationship with computing
explanations for DSs and DTs.

##### Explaining DLs.

The computation of AXp’s has been shown to be computationally hard, both for
DLs and DSs [174]. As a result, the solution approach is to follow the general
approach detailed in Section 4.2. However, we will devise a propositional
encoding and use SAT solvers as NP oracles.

To illustrate the computation of explanations (both AXp’s and CXp’s), we
consider a DL with the following structure:

$\begin{array}[]{lllcl}\textnormal{R${}_{1}$:}&\textnormal{IF~{}}&(\tau_{1})&\textnormal{~{}THEN~{}}&d_{1}\\\
\textnormal{R${}_{2}$:}&\textnormal{ELSE
IF~{}}&(\tau_{2})&\textnormal{~{}THEN~{}}&d_{2}\\\
\lx@intercol\hfil\cdots\hfil\lx@intercol\\\
\textnormal{R${}_{j}$:}&\textnormal{ELSE
IF~{}}&(\tau_{j})&\textnormal{~{}THEN~{}}&d_{j}\\\
\lx@intercol\hfil\cdots\hfil\lx@intercol\\\
\textnormal{R${}_{n}$:}&\textnormal{ELSE
IF~{}}&(\tau_{n})&\textnormal{~{}THEN~{}}&d_{n}\\\
\textnormal{R${}_{\textnormal{\sc{def}}}$:}&\textnormal{ELSE~{}}&&\textnormal{~{}THEN~{}}&d_{n+1}\end{array}$

where $d_{r}\in{\mathcal{K}},r=1,\ldots,n+1$, and $\tau_{j}$ is a conjunction
of literals, or in general some logic formula.

Let $\left\llbracket{\phi}\right\rrbracket_{{\mathcal{T}}}$ denote the
propositional CNF encoding of $\phi$. This encoding can introduce not only a
number of additional clauses, but also fresh propositional variables. The
resulting formula will be represented by $\mathfrak{E}_{\phi}(z_{1},\ldots)$,
where $z_{1}$ is a propositional variable taking value 1 iff $\phi$ takes
value 1. To develop a propositional CNF encoding, we let
$\mathfrak{E}_{\tau_{j}}(t_{j},\ldots)$ represent the clauses associated with
$\left\llbracket{\tau_{j}}\right\rrbracket_{{\mathcal{T}}}$, i.e. the
propositional CNF encoding of $\tau_{j},j=1,\ldots,n$, and where $t_{j}$
represents a new propositional variable that takes value 1 only in points of
feature space where $\tau_{j}$ is true. (Additional propositional variables
may be used, and these are represented by $\ldots$ at this stage.) Let the
target class be $c$ and define the propositional constant $e_{j}$ to be 1 iff
$d_{j}$ matches $c$.

Moreover, since literals may require propositional encodings, let
$\mathfrak{E}_{x_{i}=v_{i}}(l_{i},\ldots)$ represent the clauses associated
$\left\llbracket{x_{i}=v_{i}}\right\rrbracket_{{\mathcal{T}}},i=1,\ldots,m$,
and where $l_{i}$ represents a new propositional variable that takes value 1
only in points of feature space where $x_{i}=v_{i}$. (Additional propositional
variables may be used, and these are represented by $\ldots$ at this stage.
Also, we can envision re-using and sharing common encodings; this will be
discussed in Example 18 below.)

Clearly, for some point $\mathbf{x}$ in feature space, the prediction changes
if it is the case that,

  1. 1.

For $\tau_{j}$, with $e_{j}=0$ and $1\leq{j}\leq{n}$, it is the case that
$\tau_{j}$ is true, and for any $1\leq{k}<j$, with $e_{k}=1$, $\tau_{k}$ is
false:

$\left[f_{j}\leftrightarrow\left(t_{j}\land\bigwedge\nolimits_{1\leq{k}<j,e_{k}=1}\neg{t_{k}}\right)\right]$

where $f_{j}$ is a new propositional variable, denoting that rule $j$ with a
different prediction would fire (and so it would _flip_ its previous status).
(Clearly, if some other rule $\textnormal{R}_{r}$, $\tau_{r}$ with $r<j$ and
$e_{r}=0$, fires then the prediction will also change as intended, and this is
covered by some other constraint. Hence, there is no need to account for such
rules.)

  2. 2.

Moreover, we require that at least one $f_{j}$, with $e_{j}=0$ and
$1\leq{j}\leq{n}$, to be true:

$\left(\bigvee\nolimits_{1\leq{j}\leq{n},e_{j}=0}{f_{j}}\right)$

Given the above, we now organize the propositional encoding in two components,
one composed of soft clauses and the other composed of hard clauses:

  * •

The set of soft clauses is given by:

${\mathcal{S}}\triangleq\\{(l_{i}),i=1,\ldots,m\\}$ (20)

  * •

The set of hard clauses is given by:

$\displaystyle{\mathcal{B}}\triangleq$
$\displaystyle\bigwedge\nolimits_{1\leq{i}\leq{m}}\mathfrak{E}_{x_{i}=v_{i}}(l_{i},\ldots)\land\bigwedge\nolimits_{1\leq{j}\leq{n}}\mathfrak{E}_{\tau_{j}}(t_{j},\ldots)\land$
$\displaystyle\bigwedge\nolimits_{1\leq{j}\leq{n},e_{j}=0}\left(f_{j}\leftrightarrow\left(t_{j}\land\bigwedge\nolimits_{1\leq{k}<j,e_{k}=1}\neg{t_{k}}\right)\right)\land$
$\displaystyle\left(\bigvee\nolimits_{1\leq{j}\leq{n},e_{j}=0}{f_{j}}\right)$
(21)

It is plain that ${\mathcal{B}}\cup{\mathcal{S}}$ represents an inconsistent
propositional formula. Any MUS of ${\mathcal{B}}\cup{\mathcal{S}}$ is a subset
of ${\mathcal{S}}$, and represents one AXp. Moreover, any MCS is also a subset
of ${\mathcal{S}}$, and represents one CXp. As argued earlier, AXp’s are MHSes
of CXp’s and vice-versa [300, 56, 177]. This observation also means that we
can use _any_ algorithm for MUS/MCS extraction/enumeration for computing
explanations of DLs [246].

Finally, the propositional encoding proposed above differs slightly from the
one proposed in earlier work [174], offering a more streamlined encoding.

######  Example 18.

Let us investigate how we can encode the computation of one AXp for the DL
running example (see Figure 1). The soft clauses are given by,

${\mathcal{S}}=\\{l_{1},l_{2},l_{3},l_{4}\\}$

where $l_{i}$ is associated with
$\left\llbracket{x_{i}=v_{i}}\right\rrbracket_{{\mathcal{T}}}$, i.e. it is one
of the variables used in $\mathfrak{E}_{x_{i}=v_{i}}$. For simplicity, there
is no need to encode $x_{i}=v_{i}$ for $i=1,2,3$, with $\mathbf{v}=(0,0,1,2)$,
and so we let $l_{1}\operatorname*{\leftrightarrow}\neg{x_{1}}$,
$l_{2}\operatorname*{\leftrightarrow}\neg{x_{2}}$, and
$l_{3}\operatorname*{\leftrightarrow}{x_{3}}$. However, for $x_{4}=2$, a
dedicated propositional encoding is required. Hence, we use three
propositional variables, $\\{x_{41},x_{42},x_{43}\\}$, and pick a one hot
encoding to get
$\mathfrak{E}_{\tau_{3}}(l_{4},\ldots)\triangleq{l_{4}}\operatorname*{\leftrightarrow}{x_{43}}\land\textnormal{EqualsOne}(x_{41},x_{42},x_{43})$,
where $x_{43}=1$ iff $x_{4}=1$. There are many propositional encodings for
$\textnormal{EqualsOne}(x_{41},x_{42},x_{43})$ [55] constraints. One simple
solution is,

$(\neg{x_{41}}\lor\neg{x_{42}})\land(\neg{x_{41}}\lor\neg{x_{43}})\land(\neg{x_{42}}\lor\neg{x_{43}})\land(x_{41}\lor{x_{42}}\lor{x_{43}})$

For each rule we need to encode $\tau_{j}$. It is immediate to get
$t_{1}\operatorname*{\leftrightarrow}{x_{1}}$ for $\tau_{1}$, and
$t_{2}\operatorname*{\leftrightarrow}{x_{2}}$ for $\tau_{2}$. With respect to
$\tau_{3}$, we can use the same encoding as above (for $x_{4}$), and so we get
$t_{3}\operatorname*{\leftrightarrow}{x_{42}}$. (It is clear that the
constraints for encoding the possible values of $x_{4}$ would be the same as
before, and so there is no need to replicate them.)

Furthermore, we must encode the change of prediction. Since the prediction for
$(0,0,1,2)$ is 1, then we are interested in rules $\textnormal{R}_{1}$ and
$\textnormal{R}_{3}$, since these are the only options to change the
prediction. As a result, we get,

$\begin{array}[]{l}f_{1}\operatorname*{\leftrightarrow}{t_{1}}\\\
f_{3}\operatorname*{\leftrightarrow}\left({t_{3}}\land\neg{t_{2}}\right)\\\
\end{array}$

indicating that the prediction changes if either $t_{1}$ is true (i.e. rule
$\textnormal{R}_{1}$ fires), or $t_{3}$ is true _and_ $t_{2}$ is false (i.e.
rule $\textnormal{R}_{3}$ fires and rule $\textnormal{R}_{2}$ does not fire,
and earlier rules are already covered by other constraints). Finally, we need
the constraint $(f_{1}\lor{f_{3}})$, to enforce that a change of prediction
will take place.

Given the above, we get that,

$\displaystyle{\mathcal{B}}=$
$\displaystyle(l_{1}\operatorname*{\leftrightarrow}\neg{x_{1}})\land(l_{2}\operatorname*{\leftrightarrow}\neg{x_{2}})\land(l_{3}\operatorname*{\leftrightarrow}{x_{3}})\land(l_{4}\operatorname*{\leftrightarrow}{x_{43}})\land$
$\displaystyle\textnormal{EqualsOne}(x_{41},x_{42},x_{43})\land$
$\displaystyle(t_{1}\operatorname*{\leftrightarrow}{x_{1}})\land(t_{2}\operatorname*{\leftrightarrow}{x_{2}})\land(t_{3}\operatorname*{\leftrightarrow}{x_{42}})\land$
$\displaystyle(f_{1}\operatorname*{\leftrightarrow}{t_{1}})\land(f_{3}\operatorname*{\leftrightarrow}(t_{3}\land\neg{t_{2}}))\land(f_{1}\lor{f_{3}})$

Moreover, and by inspection, the tuple $({\mathcal{S}},{\mathcal{B}})$ can be
simplified to,

${\mathcal{S}}=\\{\neg{x_{1}},\neg{x_{2}},x_{3},x_{43}\\}$

and,

${\mathcal{B}}=\textnormal{EqualsOne}(x_{41},x_{42},x_{43})\land(f_{1}\operatorname*{\leftrightarrow}{x_{1}})\land(f_{3}\operatorname*{\leftrightarrow}(x_{42}\land\neg{x_{2}}))\land(f_{1}\lor{f_{3}})$

It is apparent that ${\mathcal{B}}\cup{\mathcal{S}}$ is inconsistent. Finally,
we can also observe that for tuple $({\mathcal{S}}^{\prime},{\mathcal{B}})$
with,

$\begin{array}[]{lcl}{\mathcal{S}}^{\prime}&=&\\{\neg{x_{1}},x_{43}\\}\\\\[2.0pt]
{\mathcal{B}}&=&\textnormal{EqualsOne}(x_{41},x_{42},x_{43})\land(f_{1}\operatorname*{\leftrightarrow}{x_{1}})\land(f_{3}\operatorname*{\leftrightarrow}(x_{42}\land\neg{x_{2}}))\land(f_{1}\lor{f_{3}})\end{array}$

${\mathcal{B}}\cup{\mathcal{S}}^{\prime}$ is still inconsistent. Thus,
${\mathcal{S}}^{\prime}=\\{\neg{x_{1}},x_{43}\\}$ is an unsatisfiable subset
(which we can prove to be irreducible), and so ${\mathcal{X}}=\\{1,4\\}$ is a
weak AXp (which we can prove to be an AXp). $\hfill\triangleleft$

Existing results indicate that the computation of explanations for DLs is very
efficient in practice [174].

###  4.4 From DLs to DTs & DSs

##### Explaining DTs as DLs.

A conceptually straightforward approach for explaining DTs is to represent a
DT as a DL. Hence, the propositional encoding proposed above for explaining
DLs can also be used for explaining DTs. Nevertheless, as argued in Section
5.1, in the case of DTs there are polynomial time algorithms for computing one
abductive explanation, and there are polynomial time algorithms for
enumerating all the contrastive explanations.

##### The case of DSs.

The fact that DSs are unordered raises a number of technical difficulties,
including the fact that, if there can be rules that predict different classes
and fire on the same input, then the classifier does not compute a function.
This is referred to as _overlap_ [181]. If the rules predicting each class are
represented as a DNF, then one call to an NP oracle suffices to decide whether
overlap exists.

Let a DS be represented by a set of DNF formulas, one for each class in
${\mathcal{K}}$. Moreover, let $z_{r}$ represent the value computed for DNF
$r$, which predicts class $c_{r}\in{\mathcal{K}}$. There exists _no_ overlap
is the following condition does _not_ hold:

$\sum\nolimits_{r=1}^{K}z_{r}>1$

If we also want to ensure that there is a prediction for any point in feature
space, then we can instead require that the following constraint is
inconsistent:

$\sum\nolimits_{r=1}^{K}z_{r}\not=1$ (22)

i.e. we want the sum to be equal to 1 on each point of feature space.
(Clearly, the constraint above must be inconsistent given the logic encoding
of the classifier. The actual encoding of each $z_{r}$ will depend on how the
DNFs are represented, and there is no restriction of considering purely
boolean classifiers.)

Under the standard assumption that (22) is inconsistent, then the encoding
proposed for DLs can be adapted to the case of DSs. We will have to encode
each term (i.e. each unordered rule), and then encode the disjunction of terms
for each DNF. We will briefly outline a propositional encoding for computing
abductive (and contrastive) explanations. The approach differs from the DL
case since we do not have order in the rules. Hence, each class is analyzed as
a DNF. As usual, we consider an instance $(\mathbf{v},c_{s})$, where
$c_{s}\in{\mathcal{K}}$ is the predicted class. The constraints for the
encodings are organized as follows:

  1. 1.

The DNF $r$ of class $c_{r}\in{\mathcal{K}}$, it is a disjunction of $n_{r}$
terms $\tau_{rj},r=1,\ldots,n_{r}$.

  2. 2.

Each term $\tau_{rj}$ is encoded into
$\mathfrak{E}_{\tau_{rj}}(t_{rj},\ldots)$, such that $t_{j}=1$ iff the term
$\tau_{rj}$ takes value 1.

  3. 3.

The literals of the form $(x_{i}=v_{i})$ will be encoded into the clauses
$\mathfrak{E}_{x_{i}=v_{i}}(l_{i},\ldots)$.
(As mentioned earlier in this section in the case of DLs, the encoding from
the original feature variables to propositional variables is assumed in all
these encodings.)

  4. 4.

The soft clauses will be $(l_{i})$, $i=1,\ldots,m$.

  5. 5.

A class $c_{r}$ is picked iff $p_{r}=1$, where $p_{i}$ is a fresh
propositional variable. Hence, we define $p_{r}$, for class $c_{r}$ as
follows:
$p_{r}\operatorname*{\leftrightarrow}\left(\lor_{j=1}^{n_{r}}{t_{rj}}\right)$

  6. 6.

The prediction changes if $p_{s}=0$.
(Observe that we could instead introduce another propositional variable $s$,
defined as follows
$s\operatorname*{\leftrightarrow}\lor_{c_{r}\in{\mathcal{K}}\setminus\\{c_{s}\\}}p_{r}$,
such that $s=1$ would mean that the prediction changes. However, this is
unnecessary.)

Given the above, we can write down a propositional encoding for a DS
classifier which respects (22). The set of soft clauses is given by:

${\mathcal{S}}\triangleq\\{(l_{i}),i=1,\ldots,m\\}$ (23)

The set of hard clauses is given by:

$\displaystyle{\mathcal{B}}\triangleq$
$\displaystyle\bigwedge\nolimits_{1\leq{i}\leq{m}}\mathfrak{E}_{x_{i}=v_{i}}(l_{i},\ldots)\land\bigwedge_{1\leq{r}\leq{K}}\bigwedge\nolimits_{1\leq{j}\leq{n_{r}}}\mathfrak{E}_{\tau_{rj}}(t_{rj},\ldots)\land$
$\displaystyle\bigwedge\nolimits_{1\leq{j}\leq{K}}p_{r}\operatorname*{\leftrightarrow}\left(\lor_{j=1}^{n_{r}}{t_{rj}}\right)$
(24)

###  4.5 Explaining Neural Networks

To illustrate the modeling flexibility of the approach proposed in the
previous section, let us develop an MILP/SMT encoding for the problem of
computing one AXp for a neural network. The encoding to be used is based on
the MILP representation of NNs proposed in earlier work [123] and is
illustrated with the NN running example of Figure 3. The MILP encoding is
shown in Figure 7(a).

To decide whether a set ${\mathcal{X}}\subseteq{\mathcal{F}}$ is a weak AXp,
we would have to decide the _in_ consistency of (adapted from Figure 7(a)):

$\displaystyle\bigwedge\nolimits_{i\in{\mathcal{X}}}(x_{i}=v_{i})\land$
$\displaystyle[(x_{1}+x_{2}-0.5=t_{1}-s_{1})\land(z_{1}=1\operatorname*{\rightarrow}{t_{1}}\leq
0)\land(z_{1}=0\operatorname*{\rightarrow}{s_{1}}\leq 0)\land$
$\displaystyle(o_{1}=(t_{1}>0))\land(t_{1}\geq 0)\land(s_{1}\geq
0)]\land\left[(o_{1}\not=1)\right]$ (25)

where