The widespread deployment of artificial intelligence in real‑world systems has raised serious concerns about trustworthiness, especially in safety‑critical domains. Explainable AI (XAI) seeks to provide users with understandable reasons behind model decisions. For Boolean classifiers, the literature distinguishes abductive explanations, which identify a minimal set of features that guarantee the observed output, and contrastive explanations, which highlight changes needed to obtain a different output. Computing such explanations is generally intractable.
A common strategy is to compile the classifier into a tractable representation, such as an Ordered Binary Decision Diagram (OBDD), enabling efficient query answering. Nevertheless, we prove that several important classes of abductive explanations remain hard even on OBDDs, including the shortest abductive explanations and those that respect a user’s preference ordering.
To overcome this limitation, we introduce a proper compiled form based on the dual‑rail encoding of the classifier. This representation allows polynomial‑time computation of the hard abductive explanation classes on many instances, thus regaining the efficiency benefits of knowledge compilation.
Review