Source-linked AI summary
Solving Hard XAI Queries Based on a Compiled Dual-Rail Encoding
Arthur Ledaguenel, Florent Capelli, Jean-Marie Lagniez
TL;DR
The paper addresses the hardness of computing abductive explanations for boolean classifiers, including cases that remain hard on OBDDs. It uses compiled dual-rail encodings to recover efficient computation for several explanation queries, while identifying representation-dependent limitations and assumptions.
Problem
Computing boolean-classifier explanations is generally hard, and several abductive-explanation classes remain hard even when the classifier is represented as an OBDD.
Method
The paper represents the classifier's dual-rail encoding in tractable compiled languages and uses conditioning and related operations to answer explanation queries.
Results
A d-DNNF representation of the dual-rail supports polynomial-time algebraic counting queries on abductive explanations, while a dec-DNNF representation supports incremental-polynomial-delay enumeration of sufficient reasons.
Takeaways & Limitations
Dual-rail compilation extends tractable compiled-representation support to hard explanation classes, including preferred explanations and abductive Shapley-value computation.
Takeaways & Limitations
The paper does not provide a formal proof of #P-hardness for the specific abductive Shapley value, and some results rely on structured representations supporting conditioning and consistency checks.
Abstract
from arXiv · showhide
The widespread adoption of artificial intelligence (AI) within real-world applications has raised a lot of concerns regarding their trustworthiness, especially in critical applications. The field of eXplainable AI (XAI) has emerged with the objective of providing explanations to the users about the decisions made by AI systems. Several explanations for boolean classifiers have been introduced in the literature, including abductive and contrastive explanations, each giving a different insight on the decision of the classifier. However, computing an explanation for a decision of a boolean classifier is a hard problem in general. One way to deal with this complexity is to rely on a compiled representation of the classifier for which each explanation can be computed efficiently. Unfortunately, we prove in this paper that several classes of abductive explanations, remain hard to compute even for Ordered Binary Decision Diagrams, one of the most tractable subsets of the knowledge compilation map. Included in such classes are shorter abductive explanations or abductive explanations that include the explainee's preferences. To recover the benefits of working with compiled representations, we show that a proper representation of the dual-rail encoding of the classifier can be used to compute efficiently these classes of explanations.
1 Introduction
XAI seeks to explain decisions of boolean classifiers, but explanation computation is generally hard. The paper studies how compiled representations and dual-rail encodings address this difficulty.
- Computing explanations for boolean-classifier decisions is generally hard, motivating tractability analyses for particular classifier representations.
- Knowledge compilation provides representations that can support efficient queries, including subset-minimal abductive explanations for d-DNNF classifiers.
- The paper proves that several abductive-explanation classes remain hard even for OBDDs, including shortest and preference-aware explanations.
- A proper dual-rail representation supports efficient computation of shortest, preferred, and coverage-based explanations, while its CNF form works with existing compilers.
- The paper experimentally measures the complexity gap between compiling the original classifier function and its dual-rail encoding.
2 Related works
Prior work studies explanation complexity on compiled classifiers and preference-aware explanations. Earlier dual-rail applications mainly used SAT or integer programming, whereas this paper compiles dual-rail encodings to support broader XAI queries.
- Earlier research analyzed abductive-explanation complexity across classifier representations and studied preference-based explanations using quantitative or qualitative preferences.
- Dual-rail encodings previously generated or enumerated selected prime implicants, typically through SAT or integer linear programming solvers.
- This paper extends dual-rail use by compiling the encoding into tractable representations and applying it to a broader range of XAI queries.
3 Preliminaries
The preliminaries define terms, boolean functions, knowledge-compilation representations, abductive explanations, preference criteria, and algebraic model-counting queries used throughout the paper.
- Boolean functions and terms: A term is a consistent set of literals, an instance assigns one literal to every variable, and an implicant is a term whose extensions are models of a function.
- Knowledge compilation: Knowledge compilation represents boolean functions in languages such as circuits and decision diagrams to support tractable reasoning and transformations.
- XAI queries: An abductive explanation is an implicant of the selected decision function that is consistent with the observed instance.
- XAI queries: Sufficient reasons are subset-minimal explanations, while shortest reasons minimize explanation size and are necessarily sufficient reasons.
- Preferences: Quantitative preferences use additive dis-utility over variables, whereas qualitative preferences use a stratification whose lexicographic size defines shorter explanations.
- Algebraic model counting: Algebraic model counting expresses counting and optimization queries as sum-of-products computations over models using semiring operations.
4 Dual-rail encoding
The dual-rail encoding represents implicants as pure assignments over positive and negative literal variables. Selector-based conditioning filters these implicants to explanations consistent with an instance, and prime implicants correspond to sufficient reasons.
- Dual-rail representation: The dual-rail encoding introduces positive and negative literal variables and constrains assignments to be pure.
- Dual-rail representation: Pure dual-rail terms and instances correspond bijectively to terms and implicants over the original variables.
- Instance conditioning: For a model x, selector variables define f_x so that a selector assignment satisfies f_x exactly when the corresponding selected literals form an implicant of f.
- Instance conditioning: The function f_x is monotone, because adding selected variables preserves satisfaction.
- Sufficient reasons: Prime implicants of f_x correspond exactly to sufficient reasons for the decision on x.
- Sufficient reasons: In the running example, ϕ_x has three models and two prime implicants corresponding to three abductive explanations and two sufficient reasons.
- Compilation: If f˘ supports polynomial-time conditioning in a representation language, f_x can be obtained in polynomial time in the size of f˘.
5 Solving hard queries using f ˘
The section establishes that many implicant and abductive-explanation optimization queries remain hard on OBDDs, while suitable dual-rail representations restore polynomial-time or incremental-polynomial-delay procedures for several queries.
- Hardness on OBDDs: Reasoning about implicants is generally hard, and most optimization queries remain NP-hard even when formulas are represented as OBDDs.The section cites NP-hardness for deciding restricted implicants and for shortest implicants on OBDDs.
- Dual-rail tractability: Algebraic counting queries over implicants and abductive explanations become polynomial-time computable from d-DNNF representations of the dual-rail encoding.The correspondence between dual-rail models and implicants or abductive explanations supports both counting and preferred-selection queries.
- Hardness on OBDDs: A shortest abductive explanation for a model of an OBDD is NP-hard to compute, and reductions transfer this hardness to related abductive queries.The shortest-explanation result follows from the corresponding implicant hardness and the reduction structure among XAI queries.
- Dual-rail tractability: Adequate dual-rail representations enable incremental-polynomial-delay enumeration of sufficient reasons, including for models whose prime-implicant explanations are hard to enumerate on OBDDs.The paper contrasts the OBDD enumeration difficulty with the dec-DNNF dual-rail result.
- Further queries: The dual-rail approach also supports polynomial-time computation of abductive Shapley values and testing whether a weak abductive explanation is a CPI-Xp under structured representations.The CPI-Xp test uses structured d-DNNF representations of the constrained classifier and constraints sharing a common base.
- Complexity boundary: The paper notes that counting abductive explanations for an OBDD is #P-hard, limiting direct access to methods requiring that count even though the specific Shapley-value hardness is not formally established.This is presented as an obstacle to extending the proof method to OBDD representations.
6 Compiling f ˘
The paper shows how to compile the dual-rail encoding into tractable representations for hard XAI queries while preserving useful structural properties of the original CNF.
- Compiling the dual-rail encoding: The dual-rail encoding of a CNF can itself be represented as a CNF, allowing existing knowledge compilers to be used unchanged.The resulting CNF representation is computed in linear time and has linear size.
- Correctness: The dual-rail construction enforces pure models and links models of the encoding to implicants of the original formula.The proof establishes that every model of the constructed CNF is pure and corresponds to an implicant of the input CNF.
- Preserving structure: A CNF representation of the dual-rail encoding preserves most of the original CNF’s structural width properties.The construction replaces each original variable with a pair of variables in the corresponding decomposition.
- Query tractability: Compiled dual-rail representations provide polynomial support for XAI queries that are hard to answer from ordinary classifier compilations.This support yields fixed-parameter tractable algorithms for CNF inputs under standard width parameters.
7 Experiments
Experiments compare compiling the original CNF with compiling its dual-rail encoding, finding that the latter incurs greater resource costs while enabling richer polynomial-time query support.
- Solved instances and resource use: 1355 instances were solved by d4 versus 1237 by d4˘, with d4˘ also producing 171 memory-outs versus 59 for d4.The dual-rail compilation had 37 timeouts, compared with 31 for d4.
- Compilation time: About one order of magnitude of additional compilation time is typically required by d4˘.The overhead is paid once offline and supports queries that are NP-hard without the dual-rail encoding.
- Compiled representation size: The dual-rail encoding generally increases d-DNNF size, measured by the number of edges, but the growth remains manageable.The resulting structure supports polynomial-time query answering that is not generally available from plain CNF compilation.
8 Conclusion
The paper establishes hardness for several XAI queries on OBDDs and uses compiled dual-rail encodings to recover efficient support for counting, preference-based, enumeration, and coverage-based explanations.
- Hardness results: Several XAI queries remain hard even for OBDD representations, including shortest and preference-aware abductive explanations.OBDDs are identified as one of the most tractable languages in the knowledge compilation map.
- Counting and preferences: A d-DNNF representation of the dual-rail encoding supports algebraic counting over implicants and abductive explanations for positive decisions.Special cases include preferred explanations under quantified or stratified preferences and a Shapley value based on abduction.
- Enumeration and coverage: A dec-DNNF dual-rail representation enumerates sufficient reasons for positive decisions with incremental polynomial delay.Sharing structure with domain constraints also supports coverage-based explanations.
- Future directions: Future work includes broader runtime experiments, comparisons with solver-based methods, analysis of enumeration delays, and compilation beyond clausal formulas.The paper specifically identifies explanation-enumeration delays and non-clausal inputs as promising directions.