  Random Forest (RFs) are among the most widely used Machine Learning (ML)
classifiers. Even though RFs are not interpretable, there are no dedicated
non-heuristic approaches for computing explanations of RFs. Moreover, there is
recent work on polynomial algorithms for explaining ML models, including naive
Bayes classifiers. Hence, one question is whether finding explanations of RFs
can be solved in polynomial time. This paper answers this question negatively,
by proving that computing one PI-explanation of an RF is D^P-complete.
Furthermore, the paper proposes a propositional encoding for computing
explanations of RFs, thus enabling finding PI-explanations with a SAT solver.
This contrasts with earlier work on explaining boosted trees (BTs) and neural
networks (NNs), which requires encodings based on SMT/MILP. Experimental
results, obtained on a wide range of publicly available datasets, demontrate
that the proposed SAT-based approach scales to RFs of sizes common in practical
applications. Perhaps more importantly, the experimental results demonstrate
that, for the vast majority of examples considered, the SAT-based approach
proposed in this paper significantly outperforms existing heuristic approaches.
