{'fraction_non_alphanumeric': 0.04225320790802144, 'fraction_numerical': 0.00989614606266818, 'mean_word_length': 4.153334861333945, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 1, 'https://': 0, 'lorem ipsum': 0, 'www.': 4, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 6, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
On the Explanatory Power of Decision Trees

Decision trees have long been recognized as models of choice in sensitive applications where interpretability is of paramount importance. In this paper, we examine the computational ability of Boolean decision trees in deriving, minimizing, and counting sufficient reasons and contrastive explanations. We prove that the set of all sufficient reasons of minimal size for an instance given a decision tree can be exponentially larger than the size of the input (the instance and the decision tree). Therefore, generating the full set of sufficient reasons can be out of reach. In addition, computing a single sufficient reason does not prove enough in general; indeed, two sufficient reasons for the same instance may differ on many features. To deal with this issue and generate synthetic views of the set of all sufficient reasons, we introduce the notions of relevant features and of necessary features that characterize the (possibly negated) features appearing in at least one or in every sufficient reason, and we show that they can be computed in polynomial time. We also introduce the notion of explanatory importance, that indicates how frequent each (possibly negated) feature is in the set of all sufficient reasons. We show how the explanatory importance of a feature and the number of sufficient reasons can be obtained via a model counting operation, which turns out to be practical in many cases. We also explain how to enumerate sufficient reasons of minimal size. We finally show that, unlike sufficient reasons, the set of all contrastive explanations for an instance given a decision tree can be derived, minimized and counted in polynomial time.


Introduction
In essence, explaining a decision to a person is to give the details or reasons that help a person (the explainee) understand why the decision has been made. This is a significant issue especially when decisions are made by Machine Learning (ML) models, such as random forests, Markov networks, support vector machines, and deep neural networks. Actually, with the growing number of applications that rely on ML techniques, researches on eXplainable AI (XAI) have become increasingly important, by providing efficient methods for interpreting ML models, and explaining their decisions (see for instance [12,13,14,16,19,22,26,28,29,33,35]).
When dealing with Boolean classifiers, which is what we do in this paper, two decisions are possible, only: 1 for the instances classified as positive instances, and 0 for the remaining ones (the negative instances). Whatever the way x has been classified, an explainee may seek for explanations from two distinct types [28]. On the one hand, "abductive" explanations for x are intended to explain why x has been classified in the way it has been classified by the ML model (thus, addressing the "Why?" question). On the other hand, the purpose of "contrastive" (also known as "counterfactual") explanations for x is to explain why x has not been classified by the ML model as the explainee expected it (thus, addressing the "Why not?" question). In both cases, explanations that are as simple as possible are preferred (where simplicity is modeled as irredundancy, or even as size minimality). 1 .
Although there is no formal notion of interpretability [25], for classification problems, decision trees [5,31] are arguably among the most interpretable ML models. Because of their interpretability, decision trees are often considered as target models for distilling a black-box model into a comprehensible one [6,12]. Furthermore, decision trees are often the components of choice for building (less interpretable, but potentially more accurate) ensemble classifiers, such as random forests [4] and gradient boosted decision trees [7].
The interpretability of decision trees is endowed with two key characteristics. On the one hand, decision trees are transparent: each node in a decision tree has some meaning, and the principles used for generating all nodes can be explained. On the other hand, decision trees are locally explainable: by construction of a decision tree T , any input instance x is mapped to a unique root-to-leaf path that yields to a decision label. The subset of (positive and negative) features t T x occurring in the path used to find the right label 1 or 0 for x in the decision tree T can be viewed as a "direct reason" for classifying x as a positive instance or as a negative instance. t T x is an abductive explanation for x given T , which explains why x has been classified by T as it has been classified. Indeed, every instance x that coincides with x on t T x is classified by T in the same way as x. However, such "direct reasons" can contain arbitrarily many redundant features [20]. This motivates to take account for other types of abductive explanations in the case of decision trees, namely, sufficient reasons [9] (also known as prime implicant explanations [34]), that are irredundant abductive explanations, and minimal sufficient reasons (i.e., those sufficient reasons of minimal size).
In this paper, we examine the computational ability of Boolean decision trees in deriving, minimizing and counting sufficient reasons and contrastive explanations. We prove that the set of all sufficient reasons of minimal size for an instance given a decision tree can be exponentially larger than the size of the input. When this is the case, generating the full set of sufficient reasons (i.e., the complete reason for the instance [9]) is typically out of reach. In addition, computing a single sufficient reason does not prove enough in general; indeed; two sufficient reasons for the same instance may differ on many features. To deal with this issue and generate synthetic views of the set of all sufficient reasons, we introduce the notions of relevant features and of necessary features that characterize the (possibly negated) features appearing in at least one or in every sufficient reason, and we show that they can be computed in polynomial time. We also introduce the notion of explanatory importance, that indicates how frequent each (possibly negated) feature is in the set of all sufficient reasons. Though deriving the explanatory importance of a feature in the set of sufficient reasons and determining the cardinality of this set are two computationally demanding tasks, we show how they can be achieved thanks to model counting operation, which turns out to be practical in many cases. We also explain how to enumerate sufficient reasons of minimal size, which is a way to count them when they are not too numerous. We finally show that, from a computational standpoint, contrastive explanations highly depart from sufficient reasons. Indeed, the set of all contrastive explanations for an instance given a decision tree can be computed in polynomial time. As a consequence, such explanations can also be minimized and counted in polynomial time. The rest of the paper is organized as follows. Preliminaries about decision trees, abductive reasons, and contrastive explanations are given in Section 2. The computation of all sufficient reasons is considered in Section 3. Necessary and relevant features are presented in this section, as well as the approach for assessing the explanatory importance of a feature and for counting the number of sufficient reasons. We also explain there how minimal sufficient reasons can be enumerated. An algorithm for computing all the contrastive explanations for the instance given the decision tree is presented in Section 4. Experimental results are reported in Section 5. Finally, Section 6 concludes the paper. Proofs are reported in a final appendix. Additional empirical results are available on the web page of the EXPEKCTATION project: http: //www.cril.univ-artois.fr/expekctation/.

Decision Trees, Abductive and Contrastive Explanations
For an integer n, let [n] be the set {1, · · · , n}. By F n we denote the class of all Boolean functions from {0, 1} n to {0, 1}, and we use X n = {x 1 , · · · , x n } to denote the set of input Boolean variables, corresponding to the features under consideration. Any assignment x ∈ {0, 1} n is called an instance. If f (x) = 1 for some f ∈ F n , then x is called a model of f . x is a positive instance when f (x) = 1 and a negative instance when f (x) = 0.
We refer to f as a propositional formula when it is described using the Boolean connectives ∧ (conjunction), ∨ (disjunction) and ¬ (negation), together with the Boolean constants 1 (true) and 0 (false). As usual, a literal is a variable x i (a positive literal) or its negation ¬x i , also denoted x i (a negative literal). A positive literal x i is associated with a positive feature (i.e., x i is set to 1), while a negative literal x i is associated with a negative feature (i.e., x i is set to 0). A term (or monomial ) t is a conjunction of literals, and a clause c is a disjunction of literals. A DNF formula is a disjunction of terms and a CNF formula is a conjunction of clauses. The set of variables occurring in a formula f is denoted Var (f ). A formula f is consistent if and only if it has a model. A CNF formula is monotone whenever every occurrence of a literal in the formula has the same polarity (i.e., if a literal occurs positively (resp. negatively) in the formula, then it does not have any negative (resp. positive) occurrence in the formula). A formula f 1 implies a formula f 2 , noted f 1 |= f 2 , if and only if every model of f 1 is a model of f 2 . Two formulae f 1 and f 2 are equivalent, noted f 1 ≡ f 2 whenever they have the same models. The conditioning of a formula f by a literal , denoted f | , is the formula obtained from f by replacing each occurrence of x i with 1 (resp. 0) and each occurrence of In what follows, we shall often treat assignments as terms, and terms and clauses as sets of literals. Given an assignment z ∈ {0, 1} n , the corresponding term is defined as A term t covers an assignment z if t ⊆ t z . An implicant of a Boolean function f is a term that implies f . A prime implicant of f is an implicant t of f such that no proper subset of t is an implicant of f . Dually, an implicate of a Boolean function f is a clause that is implied by f , and a prime implicate of f is an implicate c of f such that no proper subset of c is an implicate of f . With these basic notions in hand, we shall focus on the following representation class of Boolean functions: Definition 1 (Decision Tree). A (Boolean) decision tree is a binary tree T , each of whose internal nodes is labeled with one of n input Boolean variables, and whose leaves are labeled 0 or 1. Every variable is assumed (without loss of generality) to appear at most once on any root-to-leaf path (read-once property). The value T (x) ∈ {0, 1} of T on an input instance x is given by the label of the leaf reached from the root as follows: at each node, go to the left or right child depending on whether the input value of the corresponding variable is 0 or 1, respectively. The size of T , denoted |T |, is given by the number of its nodes.
The class of decision trees over X n is denoted DT n . It is well-known that any decision tree T ∈ DT n can be transformed in linear time into an equivalent disjunction of terms, denoted DNF(T ), where each term corresponds to a path x 4 x 4 x 4 x 4 0 1 0 1 0 1 0 1 Figure 1: A decision tree T for recognizing Cattleya orchids. The left (resp. right) child of any decision node labelled by xi corresponds to the assignment of xi to 0 (resp. 1).
from the root to a leaf labeled with 1. Dually, T can be transformed in linear time into a conjunction of clauses, denoted CNF(T ), where each clause is the negation of the term describing a path from the root to a leaf labeled with 0. For illustration, the following toy example will be used throughout the paper as a running example: Example 1. The decision tree in Figure 1 separates Cattleya orchids from other orchids using the following features: x 1 : "has fragrant flowers", x 2 : "has one or two leaves", x 3 : "has large flowers", and x 4 : "is sympodial".
As a salient characteristic, decision trees convey a single explicit abductive explanation for classifying any input instance: Definition 2 (Direct Reason). Let T ∈ DT n and x ∈ {0, 1} n . The direct reason for x given T is the term, denoted t T x , corresponding to the unique root-to-leaf path of T that is compatible with x.
Another important notion of abductive explanations is the following concept of sufficient reason [9], that, unlike the notion of direct reason, is not specific to decision trees: Definition 3 (Sufficient Reason). Let f ∈ F n and x ∈ {0, 1} n such that f (x) = 1 (resp. f (x) = 0). A sufficient reason for x given f is a prime implicant t of f (resp. ¬f ) that covers x. sr (x, f ) denotes the set of sufficient reasons for x given f .
Thus, a sufficient reason [9] (also known as prime implicant explanation [34]) for an instance x given a class described by a Boolean function f is a subset t of the characteristics of x that is minimal w.r.t. set inclusion such that any instance x sharing this set t of characteristics is classified by f as x is. Thus, when f (x) = 1, t is a sufficient reason for x given f if and only if t is a prime implicant of f such that x implies t, and when f (x) = 0, t is a sufficient reason for x given f if and only if t is a prime implicant of ¬f such that t covers x. Accordingly, sufficient reasons are suited to explain why the instance at hand x has been classified by f as it has been classified. Unlike direct reasons [20], sufficient reasons do not contain any redundant feature.
When considering the sufficient reasons of the input instance, one may be interested in focusing on the shortest ones, alias the minimal sufficient reasons. Those reasons are valuable since conciseness is often a desirable property of explanations (Occam's razor). Formally: Definition 4 (Minimal Sufficient Reason). Let f ∈ F n and x ∈ {0, 1} n . A minimal sufficient reason for x given f is a sufficient reason for x given f that contains a minimal number of literals.
Finally, unlike direct and (possibly minimal) sufficient reasons that aim to explain the classification of the instance x under consideration as achieved by the classifier f , contrastive explanations are valuable when x has not been classified by f as expected by the explainee. In this case, one looks for minimal subsets of the features that when switched in x are enough to get instances that are classified positively (resp. negatively) by f if x is classified negatively (resp. positively) by f . Formally, a contrastive explanation for x given f [18] is a subset t of the characteristics of x that is minimal w.r.t. set inclusion among those such that at least one instance x that coincides with x except on the characteristics from t is not classified by f as x is.
Definition 5 (Contrastive Explanation). Let f ∈ F n and x ∈ {0, 1} n such that f (x) = 1 (resp. f (x) = 0). A contrastive explanation for x given f is a term t over X n such that t ⊆ t x , t x \ t is not an implicant of f (resp. ¬f ), and for every ∈ t, t \ { } does not satisfy this last condition.
Example 2. Based on our running example, we can observe that T (x) = 1 for the instance x = (1, 1, 1, 1). The direct reason for x given T is the term are the sufficient reasons for x given T . x 1 ∧ x 4 is the unique minimal sufficient reason for x given T . x 4 , x 1 ∧ x 2 , and x 1 ∧ x 3 are the contrastive explanations for x given T . Thus, the instance (1, 1, 1, 0) that differs with x only on x 4 is not classified by T as x is ((1, 1, 1, 0) is classified as a negative instance).
We mention in passing that when dealing with decision trees T , we could have focused only on explanations for the positive instances x given T . This comes from the fact that DT n is closed under negation, in the sense that for any T ∈ DT n , ¬T can be obtained by just replacing from T the label of each leaf with its complement. So, for any instance x ∈ {0, 1} n , a direct reason (resp. sufficient reason, minimal sufficient reason, contrastive explanation) explaining why T (x) = 0 is precisely the same as a direct reason (resp. sufficient reason, minimal sufficient reason, contrastive explanation) explaining why (¬T )(x) = 1. Considering T or its negation ¬T has no computational impact since ¬T can be computed in time linear in the size of T .

Computing All Sufficient Reasons
Sufficient reasons can be exponentially numerous. When switching from the direct reason for an instance (that is unique but not always redundancy-free) to its sufficient reasons, a main obstacle to be dealt with lies in the number of reasons to be considered. Indeed, even for the restricted class of decision trees with logarithmic depth, an input instance can have exponentially many sufficient reasons: There is a decision tree T ∈ DT n of depth log 2 (n + 1) such that for any x ∈ {0, 1} n , the number of sufficient reasons for x given T is at least By definition, the minimal sufficient reasons for x given T cannot be more numerous than its sufficient reasons. However, focusing on minimal sufficient reasons does not solve the problem since an instance can also have exponentially many minimal sufficient reasons: Proposition 2. For every n ∈ N such that n is odd, there is a decision tree T ∈ DT n of depth n+1 2 such that T contains 2n + 1 nodes and there is an instance x ∈ {0, 1} n such that the number of minimal sufficient reasons for x given T is equal to 2 √ n−1 .
In many practical cases, the number of sufficient reasons for an instance given a decision tree can be very large. Figure 2 (top) shows an mnist instance (the leftmost subfigure) that has 482 185 073 664 sufficient reasons. Among them there are very dissimilar sufficient reasons. As an illustration, the two rightmost subfigures present two sufficient reasons for this instance, and they differ on many features (blue (resp. red) dots correspond to pixels on (resp. off)).
For such datasets, computing the set of all the sufficient reasons for a given instance is not always feasible. Furthermore, if the computation succeeds but the number of sufficient reasons is huge, their (disjunctively interpreted) set, alias the complete reason for the instance [9], can hardly be considered as intelligible by the explainee. Finally, due to the number of sufficient reasons and their diversity, deriving one of them is not informative enough. Thus, one needs to design approaches to synthesizing their set while avoiding the two pitfalls (the computational one and the informational one).
Synthesizing the set of sufficient reasons. In this objective, the following notions of necessary / (ir)relevant features appear useful. These notions of necessity and relevance echo the ones that have been considered in [11] for logic-based abduction.
Definition 6 (Explanatory Features). Let f ∈ F n , and x ∈ {0, 1} n be an instance. Let e be an explanation type. The necessary (resp. irrelevant) features for the family s of sufficient reasons for x given f are the most (resp. less) important features for explaining the classification of x by f , since they belong to every (resp. no) sufficient reason for x given f . Clearly enough, the notions of relevant/irrelevant feature considered here must not be confused with the ones defined in [1]. Indeed, in the latter paper, the (ir)relevance of a feature is defined for a class, not for an explanations (thus, an explanatory feature can be relevant for a given positive instance x and irrelevant for another positive instance x ).
When a single sufficient reason t for x given f has been computed, the cardinality of t deprived from the features of Nec s (x, f ) is small, and the cardinality of the symmetric difference between t and Rel s (x, f ) is small as well, t can be viewed as a good representative of the complete reason for x given f in the sense that a sufficient reason t for x given f that differs a lot from t cannot exist.
In the case when f is a decision tree T , though the set of all sufficient reasons for x given T cannot be generated when it is too large, Nec s (x, f ), Rel s (x, f ), and Irr s (x, f ) can be derived efficiently: Going a step further consists in evaluating the explanatory importance of every (positive or negative) feature: Definition 7 (Explanatory Importance). Let f ∈ F n , and x ∈ {0, 1} n be an instance. Let e be an explanation type, and E e (x, f ) the set of all explanations for x given f that are of type e. The explanatory importance of a literal over X n for x given f w.r.t. e is given by Example 3. On the running example, we have Nec The notion of explanatory importance must not be confused with the notions of feature importance (which can be defined and assessed in many different ways): the former is local (i.e., relative to an instance) and not global, it concerns literals and not variables (polarity matters), and it is about the explanation task, not the prediction one.
In order to compute the explanatory importance of a literal, a straightforward approach consists in enumerating the explanations of E e (x, f ). This is feasible when this set is not too large, which is not always the case for sufficient reasons even when f is a decision tree T . Thus, for dealing with the remaining case, an alternative approach must be looked for.
We designed such an approach for computing Imp s ( , x, T ). We know that sr (x, T ) is by construction the set of prime implicants of g = {c∩t x : c ∈ CNF(T )}. Thus, we exploited the translation presented in [21] showing how to associate in polynomial time with a given CNF formula (here, g) another formula (over a distinct set of variables), let us say h, such that the models of h are in one-to-one correspondence with the prime implicants of g. In our case, the translation can be simplified because g is a monotone CNF formula. Since h is not primarily a CNF formula, leveraging Tseitin transformation [36], we turned h in linear time into a query-equivalent CNF formula i. Note that every auxiliary variable that is introduced in i is defined from the other variables (those occurring in h), so that the number of models of i is the same as the number of models of h. Finally, we took advantage of the compilation-based model counter D4 [23] to compile i into a d-DNNF circuit [8], and this enabled us to compute in time polynomial in the size of i both the number of sufficient reasons and the explanatory importance of every literal (indeed, the d-DNNF language supports in polytime the model counting query and the conditioning transformation [10]). We show in Section 5 that, despite a high complexity in the worst case (the size of i can be exponential in |T |), this approach based on knowledge compilation proves quite efficient in practice.
Clearly enough, when Imp e ( , x, T ) has been computed for every , one can easily generate explanatory heat maps. Figure 2 (bottom) shows an mnist instance (the leftmost subfigure) that has 19 115 685 sufficient reasons, 6 necessary literals, and 94 relevant literals. The central subfigure is the corresponding heat map. Blue (resp. red) pixels correspond to positive (resp. negative) literals in the instance, and the intensity of the color aims to reflect the explanatory importance of the corresponding literal. The rightmost subfigure gives the explanatory features (dark pixels are associated with necessary literals, and light pixels to relevant literals).
Enumerating the minimal sufficient reasons. An approach to synthesizing the set of sufficient reasons consists in focusing on the minimal ones. Indeed, though the set of minimal sufficient reasons for an instance given a decision tree can be exponentially large, the number of minimal sufficient reasons cannot exceed the number of sufficient reasons, and it can be significantly lower in practice.
However, unlike sufficient reasons that can be generated in polynomial time using a greedy algorithm (see e.g., [20]), computing minimal reasons is not an easy task, as shown in [2]: 3 Proposition 4. Let T ∈ DT n and x ∈ {0, 1} n . Computing a minimal sufficient reason for x given T is NP-hard.
Despite this intractability result, minimal sufficient reasons can be generated in many practical cases. A common approach for handling NP-optimization problems is to rely on modern constraint solvers. One follows this direction here and casts the task of finding minimal sufficient reasons as a Boolean constraint optimization problem. We first need to recall that a Partial MaxSAT problem consists of a pair (C soft , C hard ) where C soft and C hard are (finite) set of clauses. The goal is to find a Boolean assignment that maximizes the number of clauses c in C soft that are satisfied, while satisfying all clauses in C hard .
Proposition 5. Let T be a decision tree in DT n and x ∈ {0, 1} n be an instance such that T (x) = 1. Let (C soft , C hard ) be an instance of the Partial MaxSAT problem such that: The intersection of t x with t x * where x * is an optimal solution of (C hard , C soft ), is a minimal sufficient reason for x given T .
Clearly enough, if x is such that T (x) = 0, then it is enough to consider the same instance of Partial MaxSAT as above, except that C hard = {c ∩ t x : c ∈ CNF(¬T )}.
Finally, one can take advantage of this Partial MaxSAT characterization for generating a preset number of minimal sufficient reasons (basically, one generates a first reason t, then one adds to C hard the negation of t as a clause as well as a CNF encoding of a cardinality constraint for ensuring that the next reasons to be generated have the same size as the one of t, and we resume until the bound is reached or no solution exists).
Interestingly, it has been shown that sufficient reasons and contrastive explanations are connected by a minimal hitting set duality [18]. This duality can be leveraged to derive one of the two sets of explanations from the other one using algorithms for computing minimal hitting sets [32,37].
However, in the case of decision trees, a more direct and much more efficient approach to derive all the contrastive explanations for x ∈ {0, 1} n given T ∈ DT n can be designed.
x 4 for x given T (viewing clauses and terms as sets of literals).
As straightforward consequences of Proposition 6, computing necessary / relevant features and computing the explanatory importance of features w.r.t. contrastive explanations can be achieved in time polynomial in n + |T |. Similarly, statistics about the size of contrastive explanations can be easily established, and contrastive explanations can be easily minimized and counted.

Experiments
Empirical setting. We have considered 90 datasets, which are standard benchmarks from the well-known repositories Kaggle (www.kaggle.com), OpenML (www.openml.org), and UCI (archive.ics.uci.edu/ml/). mnist38 and mnist49 are subsets of the mnist dataset, restricted to the instances of 3 and 8 (resp. 4 and 9) digits. Because some datasets are suited to the multi-label classification task, we used the standard "one versus all" policy to deal with them: all the classes but the target one are considered as the complementary class of the target. Categorical features have been treated as arbitrary numbers (the scale is nominal). As to numeric features, no data preprocessing has taken place: these features have been binarized on-the-fly by the decision tree learning algorithm that has been used.
For every benchmark b, a 10-fold cross validation process has been achieved. Namely, a set of 10 decision trees T b have been computed and evaluated from the labelled instances of b, partitioned into 10 parts. One part was used as the test set and the remaining 9 parts as the training set for generating a decision tree. This tree is thus in 1-to-1 correspondence with the test set chosen within the whole dataset b. The classification performance for b was measured as the mean accuracy obtained over the 10 decision trees generated from b. The CART algorithm, and more specifically its implementation provided by the Scikit-Learn library [30] has been used to learn decision trees. All hyper-parameters of the learning algorithm have been set to their default value. Notably, decision trees have been learned using the Gini criterion, and without any maximal depth or any other manual limitation. For each benchmark b, each decision tree T b , and a subset of at most 100 instances x picked up at random in the test set following a uniform distribution, we computed a sufficient reason for x given T b (using the standard greedy algorithm run on the direct reason t T b x ), and a minimal sufficient reason for x given T b using the Partial MaxSAT encoding presented in Proposition 5. This enabled us to draw some statistics (median, maximum) about the sizes of the reasons that have been generated. Using the algorithm presented in the proof of Proposition 3, we also derived the necessary and relevant explanatory features for each x, and again drew some statistics about them. Exploiting the model counter D4, we computed the number of sufficient reasons for x given T b , as well as the explanatory importance of every feature. Taking advantage of the algorithm given in Proposition 4, we computed the number of contrastive explanations for x given T b , and drew some statistics about those numbers and about the sizes of the contrastive explanations. Finally, using the approach described in Section 3, we enumerated all the minimal sufficient reasons for x given T b up to a limit of 10 000, and again drew some statistics about the numbers of minimal sufficient reasons. Of course, for each computation, we measured the corresponding runtimes since this is fundamental to determine the extent to which the algorithms are practical (details are provided at http://www.cril.univ-artois.fr/expekctation/).
All the experiments have been conducted on a computer equipped with Intel(R) XEON E5-2637 CPU @ 3.5 GHz and 128 GiB of memory. D4 [23] was run with its default parameters. For computing minimal reasons, we used the Pysat library [17], which provides the implementation of the RC2 Partial MaxSAT solver. This solver was run using the parameters corresponding to the "Glucose" setting. A time-out of 100s per instance was set for D4.
Results. Table 1 (top and bottom) reports an excerpt of our results, focusing on 12 benchmarks out of 90 (the selected datasets are among those containing many instances and/or many features). The leftmost column gives the name of the dataset b. Columns %A, %N , and #B give, respectively, the mean accuracy over the 10 decision trees, the average number of nodes in those trees, and the average number of binary features they are based on. The next columns give statistics (median, maximum) about, respectively, the size of the sufficient reasons (|Sufficient|) and of the minimal sufficient reasons (|Minimal|) that have been computed, as well as about the number of necessary (#Nec. Features) and relevant (#Rel. Features) features that appear in the full set of sufficient reasons for the instance. Table 1 (bottom) give statistics (median, maximum) about, respectively, the number of sufficient reasons (#Sufficient), the number of contrastive explanations (#Contrastive) and their sizes (|Contrastive|), and finally the number of minimal sufficient reasons (#Minimal).
As to the computation times, it turns out that all the algorithms described in the previous sections proved as efficient in practice. This is not surprising for those algorithms having a polytime worst-case complexity (the greedy algorithm for computing a sufficient reason, the one for deriving explanatory features, and the one for computing all the contrastive explanations). It was less obvious at first sight for the algorithms used for counting the number of sufficient reasons and for computing the explanatory importance of features. However, all the computations that have been run have terminated in due time, except for 3 datasets out of 90, namely adult, bank_marketing, and bank. For these datasets, the time limit of 100s has been reached for, respectively, 203, 150, and 336 instances out of 1000 (in this case, the median number of sufficient reasons has not been reported). Notably, for all the 90 datasets but those 3, the median time required for counting the number of sufficient reasons and computing the explanatory importance of features never exceeded 1s. Computing a minimal sufficient reason, and more generally all such reasons looked challenging as well, due to both the intrinsic complexity of computing a minimal sufficient reason and to their number. Nevertheless, our enumeration algorithm succeeded in deriving all the minimal sufficient reasons for every dataset except 3 out of 90, namely farm-ads, mnist49, and gisette. For these datasets, the limit of 10 000 reasons has been reached for, respectively, 5, 16, and 3 instances out of 1000.
Interestingly, the median time needed to derive all the minimal sufficient reasons for the instances for which the computation has been successful exceeded 1s only for 2 datasets (adult and bank_marketing).
Beyond providing evidence that the number of reasons can be huge, our experiments have highlighted that the greedy algorithm for deriving a sufficient reason computes in practice a minimal sufficient reason in many cases. They have also shown that the number of explanatory relevant features for an instance is typically much lower than the number of binary features used to describe it, and that the number of explanatory necessary features is also significantly lower than the number of explanatory relevant features. The gap between the two explains the possibly enormous number of sufficient reasons. When considering the full set of reasons, a considerable difference between the number of sufficient reasons and the number of minimal sufficient reasons can also be observed. Finally, like minimal sufficient reasons, the number of contrastive explanations appears in many cases not very large, which is a good point from an intelligibility perspective.

Conclusion
In light of our results, it turns out that the explanatory power of decision trees goes far beyond its ability to generate direct reasons. From a decision tree, the explanatory importance of features and the minimal sufficient reasons for an instance can be computed efficiently most of the time. For decision trees, fully addressing the "Why not?" question also appears as easier than fully addressing the "Why?" question: computing the full set of sufficient reasons for the instance at hand is typically out of reach, while computing its full set of contrastive explanations is tractable.
Accordingly, the language of decision trees appears not only as appealing for the learning purpose, but also as a good target when one needs to reason on the various forms of explanations (abductive and contrastive ones) associated with the predictions made. This coheres with (and completes) the results reported in [1], showing that many other explanation and verification tasks are tractable for decision tree classifiers.

Proof of Proposition 1
Proof. Let T be the complete binary tree of depth k, formed by n = 2 k − 1 internal nodes and 2 k leaves. We assume a breadth-first ordering of internal nodes, such that the root is labeled by x 1 , the nodes of depth 1 are labeled by x 2 and x 3 , and so on. Each internal node at depth k − 1 from the root of T has two children, one of it is a 0-leaf and the other one is a 1-leaf. For an arbitrary instance x ∈ {0, 1} n and any complete subtree T of T of depth d, let s(x, T ) denote the set of sufficient reasons of x given T , and let σ(x, d) = |s(x, T )| denote the number of those sufficient reasons. We show by induction on d that: For the base case (1), any complete subtree T of T of depth d = 1 has a single internal node, say x i , with two leaves labeled by 0 and 1, respectively. Therefore, the unique sufficient reason for x given T is either x i or x i , and hence, σ(x, 1) = 1. Now, consider any complete subtree T of T of depth d + 1 rooted at a node x i . Let T l (x i ) and T r (x i ) denote the subtrees of depth d, respectively rooted at the left child of x i and the right child of x i . Suppose without loss of generality that the unique path leading to T (x) = 1 includes the left child of x i (i.e. T l (x) = 1). By construction, Finally, since the doubly exponential sequence 5 given by a(1) = 1 and a(d Using 2 k−1 = (n + 1)/2, we get the desired result.

Proof of Proposition 2
Proof. One first need the following lemma that gives a recursive characterization of the set of sufficient reasons for an instance given a Boolean classifier: For any Boolean function f ∈ F n and any instance x ∈ {0, 1} n , the following inductive characterization of sr (x, f ) holds: Proof. Let us recall first the following inductive characterization of pi (f ), the set of prime implicants of f ∈ F n , based on the Shannon decomposition of f over any of its variables x (see e.g., [3]): and pi For the base cases sr (x, 1) = {1} and sr (x, 0) = {}, the result is obvious. For the general case, taking x ∈ Var ( ), we have: sr , t x |= t }, and t x |= t} Now, since x is an instance, whatever , it cannot be the case that t x |= and t x |= . Suppose that = x (the case = x is similar). In this situation, , t x |= t}, and t x |= t} can belong to sr (x, f ). As a consequence, we get that: sr If t = ∧ t is such that t x |= t holds, then we have t x |= t . Hence, we have: Consider now the condition ∃t ∈ pi ((f | ) ∧ (f | )), t |= t and suppose that it is satisfied. Since pi ((f | ) ∧ (f | )) = max ({t ∧ t : t ∈ pi (f | ), t ∈ pi (f | )}, |=), there exist t ∈ pi (f | ) and t ∈ pi (f | ) such that t = t ∧ t . Thus, we have t |= t ∧ t , and in particular t |= t holds. But since t and t are prime implicants of f | , this implies that t ≡ t holds. Furthermore, from t |= t ∧ t we get that t |= t . In addition, a prime implicant t of f | such that t |= t exists if and only if t |= f | . Altogether, the condition ∃t ∈ pi ((f | ) ∧ (f | )), t |= t is equivalent to t |= f | . Thus, we get that: sr From the inductive characterization of sr (x, f ) given by the previous proposition, we can easily derive a bottom-up algorithm allowing to derive sr (x, f ) when f is represented by a decision tree.
Consider now a decision tree T of depth k ≥ 1 having the form of the one reported in Figure 3. T has 2k − 1 decision nodes and 2k leaves. Suppose that the variables associated with the decision nodes are in one-to-one correspondence with the decision nodes (i.e., they are all distinct). The number of variables occurring in T is thus n = 2k − 1, therefore T has 2n + 1 nodes. Consider now the instance x ∈ {0, 1} n such that x i = 1 for every i ∈ [n]. We are going to prove by induction on the depth k of such a tree T that x has 2 k−1 minimal reasons given T , each of them containing k literals.  The proof takes advantage of the recursive characterization of the set of all sufficient reasons for an instance given a decision tree, as made precise by Lemma 1.
• Base case k = 1. We have n = 1. T consists of a decision node labelled by the single variable of X n , say x, a left child that is a 0-leaf and a right child that is a 1-leaf. T is equivalent to x and x is implied by t x . Hence, x is the unique sufficient reason for x given T , so it is also the unique minimal reason for x given T . As expected, the number of minimal reasons for x given T is equal to 2 k−1 . The size of the unique minimal reason is k = 1.
• Inductive step k > 1. Let x be the variable of X n labelling the root node of T . By construction, the left child T l of T is equivalent to a single variable, say x l , that is the unique minimal reason for x given T l . The right child T r of T has the same form as T , but with depth k − 1. By induction hypothesis, we know that x has 2 k−2 minimal reasons given T r , each of them containing k − 1 literals. As shown by Lemma 1, provided that the variables labelling the decision nodes are pairwise distinct, the minimal reasons for x given T are obtained by extending every minimal reason for x given T r with x l and by extending every minimal reason for x given T r with x. Accordingly, x has 2 × (2 k−2 ) = 2 k−1 minimal reasons given T and each of them contains k − 1 + 1 = k literals.
Finally, since n = 2k − 1, we have k = n+1 2 and the number of minimal reasons for x given T is equal to 2 k−1 = 2 √ n−1 .

Proof of Proposition 3
Proof. The algorithms to compute Nec s (x, T ), Rel s (x, T ), and Irr s (x, T ) are as follows: first compute CNF(T ) and then remove from this set of clauses every literal that does not belong to t x . This can be done in O(n|T |) time. By construction, the resulting CNF formula f is monotone: every literal in it occurs with the same polarity as the one it has in t x . Furthermore, the size of f cannot exceed the size of CNF(T ), thus the size of T .
Since f is a monotone CNF formula, its prime implicates can be computed by removing from f every clause that is a strict superset of another clause of f .This can be achieved in quadratic time in the size of f , thus in the size of T . Let g be the resulting formula in prime implicates form and equivalent to f . g is equivalent to the complete reason for x given T . Since it is in prime implicates form, g is Lit-dependent on every literal occurring in it (i.e., g is Lit-simplified, see Proposition 8 in [24] for details), hence so is the complete reason for x given T .
This means that for every literal occurring in g, there exists a sufficient reason for x given T that contains , so that Rel s (x, T ) is the set of literals occurring in g and Irr s (x, T ) is the complement of Rel s (x, T ) in the set of all literals over X n . Finally, since by definition the literals of Nec s (x, T ) must belong to every sufficient reason for x given T , they are given by the unit clauses that belong to g.

Proof of Proposition 5
Proof. Let x * be any solution of (C soft , C hard ). Observe that the set of all hard clauses c ∩ t x (where c is a clause of CNF(T )) corresponds to a monotone CNF formula. Therefore, in order to satisfy such a clause c ∩ t x , x * must set a literal of t x to 1. Thus, x * satisfies all the hard clauses of C hard if and only if the term consisting of the literals that are shared by t x = n i=1 i and t x * is an implicant of T and is implied by x.
The soft clauses of C soft are used to select among the assignments that satisfy all the hard clauses, the ones that correspond to minimal sufficient reasons. Soft clauses are given by literals i , which are precisely the complementary literals to those occurring in t x . Having a soft clause i violated by x * means that the literal of t x is necessary to get an implicant of T given the assignment of the other variables in x * . Whenever a soft clause i is violated by x * a penalty of 1 incurs. This ensures that the term consisting of the literals that are shared by t x = n i=1 i and t x * is a minimal sufficient reason for x given T .

Proof of Proposition 6
Proof. By definition, the sufficient reasons t for x given f are the prime implicants of f that covers x. Thus, they are precisely the prime implicants of the (conjunctively-interpreted) set of clauses {c ∩ t x : c ∈ CNF(f )} where CNF(f ) is any CNF formula equivalent to f . Furthermore, the complete reason for x given f (equivalent to the disjunction of all the sufficient reasons for x given f [9]) is a monotone Boolean function because every sufficient reason covers x which assigns in a unique way every variable from X n . The prime implicates of such a monotone function are precisely the minimal hitting sets of the prime implicants of the function. Because of the minimal hitting set duality between sufficient reasons and contrastive explanations for x given f [18], the contrastive explanations for x given f are thus the sets of literals corresponding to the prime implicates of {c ∩ t x : c ∈ CNF(f )}. Now, since the (conjunctively-interpreted) set of clauses {c ∩ t x : c ∈ CNF(f )} is equivalent to the complete reason for x given f , it is a monotone function, and as a consequence, its prime implicates are its minimal elements w.r.t. ⊆. This comes from the correctness of any resolution-based algorithm for generating prime implicates (see e.g., [27]). Finally, when f is a decision tree T , {c ∩ t x : c ∈ CNF(T )} can be computed in time polynomial in n + |T | because CNF(T ) can be computed in time linear in |T |. Using an extra quadratic time in the size of this set {c ∩ t x : c ∈ CNF(T )}, its minimal elements w.r.t. ⊆ can be selected. The resulting set is by construction the set of all the contrastive explanations for x given T , and this set has been computed in time polynomial in n + |T |.