Solving Hard XAI Queries Based on a Compiled Dual-Rail Encoding

Summary

This paper studies the complexity of computing abductive explanations for boolean classifiers given as compiled representations. The authors first prove hardness results: computing shortest implicants (Theorem 5), shortest abductive explanations (Corollary 8), and counting abductive explanations (Theorem 12) are NP-hard or #P-hard even for OBDDs, one of the most tractable knowledge compilation languages, via reductions from QSAT2 and minimum vertex cover. As a remedy, they propose reasoning over the dual-rail encoding f± of the classifier: a d-DNNF representation of f± supports polynomial-time algebraic model counting on implicants and abductive explanations (Theorems 6, 9), yielding efficient computation of shortest, weight-optimal, and stratified-preferred explanations and of abductive Shapley values (Theorem 11), while a dec-DNNF enables incremental-polynomial-delay enumeration of sufficient reasons (Theorem 10). Coverage-based explanations under domain constraints become decidable in polynomial time when structured representations share a vtree base (Theorem 16). Since the dual-rail of a CNF is itself a CNF computable in linear time (Lemma 17) with width at most doubled (Theorem 18), existing compilers apply as-is. Experiments with a modified d4 compiler on public benchmarks show dual-rail compilation solves fewer instances (1237 vs 1355) with nearly triple the memory-outs (171 vs 59) and roughly an order-of-magnitude slowdown. Main limitations: no query runtimes are measured, no SAT-solver baselines are compared, and #P-hardness of the abductive Shapley value remains unproven.