Notably, the results reported in the last two propositions differ significantly from those presented in a number of previous papers
where an equivalence-preserving polynomial-time translation (alias an encoding) from a given family \(\mathcal {L}\)  of Boolean classifiers
to CNF formulae is looked for (see e.g., [1]}, [2]}, [3]}).
Determining such translations permits to take advantage of automated reasoning techniques
for addressing XAI queries, given that existing solvers for Boolean representations are most of the time based on the CNF format.
Here, we have looked for polynomial-time translations from the language of CNF formulae to the languages \(\mathcal {L}\)  of the classifiers we focus on,
in order to prove that the XAI queries are computationally hard whenever the input classifier is in \(\mathcal {L}\) . This is quite a different, yet complementary perspective.
Indeed, when such translations exist, leveraging CNF encodings to address XAI queries
makes sense from a computational standpoint, i.e., it is not using a sledgehammer to crack a nut. However,
those translations are not guaranteed to exist for every family \(\mathcal {L}\)  of classifiers, so that it can be the case that an XAI query is tractable for the
\(\mathcal {L}\)  while being computationally hard for CNF classifiers.
Accordingly, our study shows that this is precisely what happens with decision trees. For this family of classifiers,
it is meaningful to develop algorithms for addressing XAI queries that are directly based on the representations at hand (decision trees), instead of
designing CNF encodings.
