Model Explanation via Support Graphs
Pedro Cabalar, Brais Muñiz
TL;DR
The paper addresses the problem of explaining why atoms are true in answer sets by introducing support graphs as acyclic, labelled witnesses. It formalizes justified and stable models and proves that every stable model is justified, but not conversely for disjunctive programs, providing a rigorous groundwork for explainability in ASP. A central contribution is a meta-programming ASP encoding, x(P), which, given a program $P$ and a stable model $I$, constructs $x(P,I)$ whose answer sets correspond one-to-one with explanations of $I$; this encoding is proven sound and complete and underpins the xclingo tool. The work enables on-demand, graph-based explanations for ASP results and lays the foundation for future comparisons, extensions to unsatisfiable cases, and preference-based explanation ordering, with practical implications for debugging and interpretability in symbolic AI systems.
Abstract
In this note, we introduce the notion of support graph to define explanations for any model of a logic program. An explanation is an acyclic support graph that, for each true atom in the model, induces a proof in terms of program rules represented by labels. A classical model may have zero, one or several explanations: when it has at least one, it is called a justified model. We prove that all stable models are justified whereas, in general, the opposite does not hold, at least for disjunctive programs. We also provide a meta-programming encoding in Answer Set Programming that generates the explanations for a given stable model of some program. We prove that the encoding is sound and complete, that is, there is a one-to-one correspondence between each answer set of the encoding and each explanation for the original stable model.