On Symbolically Encoding the
Behavior of Random Forests

We will now formalize some notions on multi-valued variables and then use them to formally define PI-explanations in a multi-valued setting [19, 14]. We use three multi-valued variables for our running examples: Variable $A$ with values $1,2,3$, variable $B$ with values $r,b,g$ and variable $C$ with values $l,m,h$.

A literal is a non-trivial propositional expression that mentions a single variable. The following are literals: ${B\!\!=\!r}\vee{B\!\!=\!b}$, ${A\!\!=\!2}$ and ${C\!\!\not=\!h}$. The following are not literals as they are trivial: ${B\!\!=\!r}\vee{B\!\!=\!b}\vee{B\!\!=\!g}$ and ${C\!\!=\!h}\wedge{C\!\!\not=\!h}$. Intuitively, for a variable with $n$ values, a literal specifies a set of values $S$ where the cardinality of set $S$ is in $\{1,\ldots,n-1\}$. A literal is simple if it specifies a single value (cardinality of set $S$ is $1$). When multi-valued variables correspond to the discretization of continuous variables, our treatment allows a literal to specify non-contiguous intervals of a continuous variable.

Consider two literals ${\ell}_{i}$ and ${\ell}_{j}$ for the same variable. We say ${\ell}_{i}$ is stronger than ${\ell}_{j}$ iff ${\ell}_{i}\models{\ell}_{j}$ and ${\ell}_{i}\not\equiv{\ell}_{j}$. In this case, ${\ell}_{j}$ is weaker than ${\ell}_{i}$. For example, ${B\!\!=\!r}$ is stronger than ${B\!\!=\!r}\vee{B\!\!=\!b}$. It is possible to have two literals where neither is stronger or weaker than the other (e.g., ${B\!\!=\!r}\vee{B\!\!=\!b}$ and ${B\!\!=\!g}$).

A term is a conjunction of literals over distinct variables. The following is a term: ${A\!\!=\!2}\wedge({B\!\!=\!r}\vee{B\!\!=\!b})\wedge{C\!\!\not=\!h}$. A term is simple if all of its literals are simple. The following term is simple: ${A\!\!=\!2}\wedge{B\!\!=\!r}\wedge{C\!\!=\!h}$. The following terms are not simple: ${A\!\!\not=\!2}\wedge{B\!\!=\!r}\wedge{C\!\!=\!h}$ and ${A\!\!=\!2}\wedge({B\!\!=\!r}\vee{B\!\!=\!b})\wedge{C\!\!=\!h}$. A simple term that mentions every variable is called an instance.

Term ${\tau}_{i}$ subsumes term ${\tau}_{j}$ iff ${\tau}_{j}\models{\tau}_{i}$. If we also have ${\tau}_{i}\not\equiv{\tau}_{j}$, then ${\tau}_{i}$ strictly subsumes ${\tau}_{j}$. For example, the term ${A\!\!=\!2}\wedge({B\!\!=\!r}\vee{B\!\!=\!b})\wedge{C\!\!\not=\!h}$ is strictly subsumed by the terms ${A\!\!\not=\!1}\wedge({B\!\!=\!r}\vee{B\!\!=\!b})\wedge{C\!\!\not=\!h}$ and ${A\!\!=\!2}\wedge{C\!\!\not=\!h}$.

We stress two points now. First, if term ${\tau}_{i}$ strictly subsumes term ${\tau}_{j}$ that does not necessarily mean that ${\tau}_{i}$ mentions a fewer number of variables than ${\tau}_{j}$. In fact, it is possible that the literals of ${\tau}_{i}$ and ${\tau}_{j}$ are over the same set of variables. Second, a term does not necessarily fix the values of its variables (unless it is a simple term), which is a departure from how terms are defined in Boolean logic.

In Boolean logic, the only way to get a term that strictly subsumes term ${\tau}$ is by dropping some literals from ${\tau}$. In multi-valued logic, we can also do this by weakening some literals in term ${\tau}$ (i.e., without dropping any of its variables). This notion of weakening a literal generalizes the notion of dropping a literal in the Boolean setting. In particular, dropping a Boolean literal ${\ell}$ from a Boolean term can be viewed as weakening it into ${\ell}\vee\neg{\ell}$.

Term ${\tau}$ is an implicant of expression $\Delta$ iff ${\tau}\models\Delta$. Term ${\tau}$ is a prime implicant of $\Delta$ iff it is an implicant of $\Delta$ that is not strictly subsumed by another implicant of $\Delta$. It is possible to have two terms over the same set of variables such that (a) the terms are compatible in that they admit some common instance, (b) both are implicants of some expression $\Delta$, yet (c) only one of them is a prime implicant of $\Delta$. We stress this possibility as it does not arise in a Boolean setting. We define the notions of simple implicant and simple prime implicant in the expected way.

Consider now a classifier specified using a multi-valued expression $\Delta$. The variables of $\Delta$ will be called features so an instance $\alpha$ is a simple term that mentions all features. That is, an instance fixes a value for each feature of the classifier. A decision on instance $\alpha$ is positive iff the expression $\Delta$ evaluates to $1$ on instance $\alpha$, written $\Delta(\alpha)=1$. Otherwise, the decision is negative (when $\Delta(\alpha)=0$).

The notation $\Delta_{\alpha}$ is crucial for defining explanations: $\Delta_{\alpha}$ is defined as $\Delta$ if decision $\Delta(\alpha)$ is positive and $\Delta_{\alpha}$ is defined as $\neg\Delta$ if decision $\Delta(\alpha)$ is negative. A PI-explanation for decision $\Delta(\alpha)$ is a prime implicant of $\Delta_{\alpha}$ that is consistent with instance $\alpha$. This basically generalizes the notion of PI-explanation introduced in [25] to a multi-valued setting.

The term explanation is somewhat too encompassing so any definition of this general notion is likely to draw criticism as being too narrow. The PI-explanation is indeed narrow as it is based on a syntactic restriction: it must be a conjunction of literals (i.e., a term) [25]. In the Boolean setting, a PI-explanation is a minimal subset of instance characteristics that is sufficient to trigger the same decision made on the instance. In the multi-valued setting, it can be more generally described as an abstraction of the instance that triggers the same decision made on the instance (still in the syntactic form of a term).

As an example, consider the following truth table representing the decision function of a classifier over two ternary variables $X$ and $Y$:

Consider instance ${X\!\!=\!x_{3}}\wedge{Y\!\!=\!y_{1}}$ leading to a positive decision. The sub-term ${X\!\!=\!x_{3}}$ is a PI-explanation for this decision: setting input $X$ to $x_{3}$ suffices to trigger a positive decision. Similarly, the sub-term ${Y\!\!=\!y_{1}}$ is a second PI-explanation for this decision. Consider now instance ${X\!\!=\!x_{1}}\wedge{Y\!\!=\!y_{2}}$ leading to a negative decision. This decision has a single PI-explanation: ${X\!\!\not=\!x_{3}}\wedge{Y\!\!\not=\!y_{1}}$. Any instance consistent with this explanation will be decided negatively.

Consider a multi-valued variable $X$ with values $x_{1},\ldots,x_{n}$. This encoding uses Boolean variables $x_{2},\ldots,x_{n}$ to encode the values of variable $X$. Literal ${X\!\!=\!x_{i}}$ is encoded by setting the first $i-1$ Boolean variables to $1$ and the rest to $0$. For example, if $n=3$, the values of $X$ are encoded as $\bar{x}_{2}\bar{x}_{3}$, $x_{2}\bar{x}_{3}$ and $x_{2}x_{3}$. Some instantiations of these Boolean variables will not correspond to any value of variable $X$ and are ruled out by enforcing the following constraint: all Boolean variables set to $1$ must occur before all Boolean variables set to $0$. We denote this constraint by $\Psi_{X}$: $\bigwedge_{i\in\{3,\ldots,n\}}(x_{i}\Rightarrow x_{i-1})$.

The fundamental problem with this encoding is that a multi-valued literal that represents non-contiguous values cannot be represented by a Boolean term. Hence, this encoding cannot generate prime implicants that include such literals. Consider the multi-valued expression $\Delta=({X\!\!=\!x_{1}}\vee{X\!\!=\!x_{3}})$, where $X$ has values $x_{1},\ldots,x_{4}$, and its Boolean encoding $\Delta_{b}=\bar{x}_{2}\bar{x}_{3}\bar{x}_{4}+x_{2}x_{3}\bar{x}_{4}$. There is only one prime implicant of $\Delta$, which is ${X\!\!=\!x_{1}}\vee{X\!\!=\!x_{3}}$, but this prime implicant cannot be represented by a Boolean term (that implies $\Delta_{b}$) so it will never be generated.

Consider a multi-valued variable $X$ with values $x_{1},x_{2},\ldots,x_{n}$. This encoding uses Boolean variables $x_{2},x_{3},\ldots,x_{n}$ to encode the values of variable $X$. Every instantiation of these Boolean variables will map to a value of variable $X$ in the following way. If all Boolean variables are $0$, then we map the instantiation to value $x_{1}$. Otherwise we map an instantiation to the maximum index whose variable is $1$. The following table provides an example for $n=4$.

We can alternatively view this encoding as representing literal ${X\!\!=\!x_{1}}$ using the Boolean term $\bar{x}_{2}\ldots\bar{x}_{n}$ and literal ${X\!\!=\!x_{i}}$, $i\geq 2$, using the term $x_{i}\bar{x}_{i+1}\ldots\bar{x}_{n}$. Literals over multiple values can also be represented with this encoding. For example, we can represent the literal ${X\!\!=\!x_{1}}\vee{X\!\!=\!x_{2}}$ using the term $\bar{x}_{3}\bar{x}_{4}.$

This encoding also turned out to be unsuitable for computing prime implicants. Consider the multi-valued expression $\Delta=({X\!\!=\!x_{1}}\vee{X\!\!=\!x_{3}})$, which has one prime implicant $\Delta$. The Boolean encoding $\Delta_{b}$ is $\bar{x}_{2}\bar{x}_{3}\bar{x}_{4}+x_{3}\bar{x}_{4}$ and has two prime implicants $\bar{x}_{2}\bar{x}_{4}$ and $x_{3}\bar{x}_{4}$. The term $x_{3}\bar{x}_{4}$ corresponds to the multi-valued implicant ${X\!\!=\!x_{3}}$, which is not prime. The term $\bar{x}_{2}\bar{x}_{4}$ does not even correspond to a multi-valued term. So in this encoding too, prime implicants of the original multi-valued expression $\Delta$ cannot be computed by locally and independently processing prime implicants of the encoded Boolean expression $\Delta_{b}$.

The prefix and highest-bit encodings provide some insights into requirements that enable one to locally and independently map Boolean prime implicants into multi-valued ones. The requirements are: (1) every multi-valued literal should be representable using a Boolean term, and (2) equivalence and subsumption relations over multi-valued literals should be preserved over their Boolean encodings. The next encoding satisfies these requirements. It is based on [11] but deviates from it in some significant ways that we explain later.

Suppose $X$ is a multi-valued variable with values $x_{1},\ldots,x_{n}$. This encoding uses a Boolean variable $x_{i}$ for each value $x_{i}$ of variable $X$. Suppose now that ${\ell}$ is a literal that specifies a subset $S$ of these values. The literal will be encoded using the negative Boolean term $\bigwedge_{x_{i}\not\in S}\bar{x}_{i}$. For example, if variable $X$ has three values, then literal ${X\!\!=\!x_{2}}$ will be encoded using the negative Boolean term $\bar{x}_{1}\bar{x}_{3}$ and literal ${X\!\!=\!x_{1}}\vee{X\!\!=\!x_{2}}$ will be encoded using the negative Boolean term $\bar{x}_{3}$. This encoding requires the employment of an exactly-one constraint for each variable $X$, which we denote by $\Psi_{X}$: $(\bigvee_{i}x_{i})\wedge\bigwedge_{i\neq j}\neg(x_{i}\wedge x_{j})$. We also use $\Psi$ to denote the conjunction of all exactly-one constraints.

Using the encoding in [11], one typically represents literal ${X\!\!=\!x_{i}}$ by the Boolean term $x_{i}$ which asserts value $x_{i}$. Our encoding, however, represents this literal by eliminating all other values of $X$. The following result reveals why we made this choice (proofs of results can be found in the appendix).

Exactly-one constraints are normally added to an encoding as done in [11]. We next show that this leads to unintended results when computing prime implicants, requiring another deviation from [11]. Consider two ternary variables $X$ and $Y$, the expression $\Delta:{X\!\!=\!x_{1}}\vee{Y\!\!=\!y_{1}}$ and its Boolean encoding $\Delta_{b}:\bar{x}_{2}\bar{x}_{3}+\bar{y}_{2}\bar{y}_{3}$. If $\Psi$ is the conjunction of all exactly-one constraints ($\Psi=\Psi_{X}\wedge\Psi_{Y}$), then $\Delta$ and $\Delta_{b}\wedge\Psi$ will each have five models:

The term ${X\!\!=\!x_{1}}$ is an implicant of $\Delta$. However, its corresponding Boolean encoding $\bar{x}_{2}\bar{x}_{3}$ is not an implicant of $\Delta_{b}\wedge\Psi$ (neither is $x_{1}\bar{x}_{2}\bar{x}_{3}$). For example, $x_{1}\bar{x}_{2}\bar{x}_{3}y_{1}y_{2}\bar{y}_{3}$ does not imply $\Delta_{b}\wedge\Psi$ since $y_{1}y_{2}\bar{y}_{3}$ does not satisfy the exactly-one constraint $\Psi_{Y}$. This motivates Definition 1 below and further results on handling exactly-one constraints, which we introduce after some notational conventions.

In what follows, we use $\Delta$/${\tau}$ to denote multi-valued expressions/terms, and $\Gamma$/${\rho}$ to denote Boolean expressions/terms. We also use $\Delta_{b}$ and ${\tau}_{b}$ to denote the Boolean encodings of $\Delta$ and ${\tau}$. A completion of a term is a complete variable instantiation that is consistent with the term. We use $\alpha$ to denote completions. Finally, we use $\Psi$ to denote the conjunction of all exactly-one constraints.

Note that ${\rho}\models\Gamma$ implies ${\rho}\models_{\Psi}\Gamma$ but the converse is not true.

We now show how one-hot encodings can be used for computing prime implicants, particularly, how exactly-one constraints should be integrated.

The proof is based on two lemmas that hold by construction and that use the notion of full encoding of an instance. Consider ternary variables $X$ and $Y$. For instance ${\tau}:{X\!\!=\!x_{1}}\wedge{Y\!\!=\!y_{1}}$ the full encoding is ${\rho}:x_{1}\bar{x}_{2}\bar{x}_{3}y_{1}\bar{y}_{2}\bar{y}_{3}$ ($x_{1}$ and $y_{1}$ are included). Note that ${\rho}\wedge\Psi={\rho}$ since ${\rho}$ is guaranteed to satisfy constraints $\Psi$.

Term ${\tau}:{X\!\!=\!x_{1}}\vee{X\!\!=\!x_{2}}$ has six completions: ${X\!\!=\!x_{1}}\wedge{Y\!\!=\!y_{1}}$, ${X\!\!=\!x_{2}}\wedge{Y\!\!=\!y_{1}}$, …, ${X\!\!=\!x_{2}}\wedge{Y\!\!=\!y_{3}}$. Its Boolean encoding ${\tau}_{b}:\bar{x}_{3}$ also has six completions that are consistent with $\Psi$: $x_{1}\bar{x}_{2}\bar{x}_{3}y_{1}\bar{y}_{2}\bar{y_{3}}$, $\bar{x}_{1}x_{2}\bar{x}_{3}y_{1}\bar{y}_{2}\bar{y_{3}}$, …, $\bar{x}_{1}x_{2}\bar{x}_{3}\bar{y}_{1}\bar{y}_{2}y_{3}$. Each of these completions $\alpha$ is guaranteed to satisfy constraints $\Psi$ leading to $\alpha\wedge\Psi=\alpha$. Next, we relate the prime implicants of multi-valued expressions and their encodings.

This proposition suggests the following procedure for computing multi-valued prime implicants from Boolean prime implicants. Given a multi-valued expression $\Delta$, we encode each literal in $\Delta$ using its negative Boolean term, leading to the Boolean expression $\Delta_{b}$. We then construct the exactly-one constraints $\Psi$ and compute prime implicants of $\Psi\Rightarrow\Delta_{b}$, keeping those that are negative and consistent with constraints $\Psi$.³³3It is straightforward to augment the algorithm of [25] so that it only enumerates such prime implicants, by blocking the appropriate branches. Those Boolean prime implicants correspond precisely to the multi-valued prime implicants of $\Delta$.⁴⁴4Note that when computing PI-explanations, we are interested only in prime implicants that are consistent with a given instance. Any negative prime implicant which is consistent with an instance must also be consistent with constraints $\Psi$. The only way a negative Boolean term ${\rho}$ can violate constraints $\Psi$ is by setting all Boolean variables of some multi-valued variable to false. However, every instance $\alpha$ will set one of these Boolean variables to true so ${\rho}$ cannot be consistent with $\alpha$.

The only system we are aware of that computes prime implicants of decision tree encodings (and forests) is Xplainer [9]. This system bypasses the encoding complications we alluded to earlier as it computes prime implicants in a specific manner [6, 7]. In particular, it encodes a multi-valued expression into a Boolean expression using the classical one-hot encoding. But rather than computing prime implicants of the Boolean encoding directly (which would lead to incorrect results), it reduces the problem of computing prime implicants of a multi-valued expression into one that requires only consistency testing of the Boolean encoding, which can be done using repeated calls to a SAT solver. The classical one-hot encoding is sound and complete for this purpose. Our treatment, however, is meant to be independent of the specific algorithm used to compute prime implicants. It would be needed, for example, when compiling the encoding into a tractable circuit and then computing prime implicants as done in [25, 5].

Consider a decision tree, such as the one depicted in Figure 1. Each internal node in the tree represents a decision, which is either true or false. Each leaf is annotated with the predicted label. We can thus view a decision tree as a function whose inputs are all of the unique decisions that can be made in the tree, and whose output is the resulting label. Each leaf of the decision tree represents a simple term over the decisions made on the path to reach it, found by conjoining the appropriate literals. The Boolean function representing a particular class can then be found by simply disjoining the paths for all leaves of that class. That is, this Boolean function outputs true for all inputs that result in the corresponding class label, and false otherwise. We can also obtain this function for an ensemble of decision trees, such as a random forest. We first obtain the Boolean functions of each individual decision tree, and then aggregate them appropriately. For a random forest, we can use a simple majority gate whose inputs are the outputs of each decision tree; see also [1]. Finally, once we have the Boolean function of a classifier, we could apply a SAT or SMT solver to analyze it as proposed by [10, 16, 7]. We could also compile it into a tractable representation, such as an Ordered Binary Decision Diagram (OBDD), and then analyze it as proposed by [25, 24, 26, 23]. In the latter case, a representation such as an OBDD allows us to perform certain queries and transformation on a Boolean function efficiently, which facilitates the explanation and formal verification of the underlying machine learning classifier, as also shown more generally in [1].