An XAI View on Explainable ASP: Methods, Systems, and Perspectives

1 Introduction

Understanding the decision-making of AI systems is crucial for accepting them as tools in industry and society to ease our everyday life. This need especially occurs for AI systems based on machine learning, as they usually provide little-to-no insights on their underlying models built from observed data. The field of Explainable AI (XAI) tackles the challenge of AI systems providing explanations on their decisions and their models, to help in the understanding of their mechanism [Calegari et al., 2020; Schwalbe and Finzel, 2024]. Symbolic AI, which is based on describing the knowledge of the world and a problem at hand through logical or related formal languages, is in a strong position for XAI as symbolic and especially rule-based representations are more understandable to humans than what subsymbolic AI systems (largely neural networks) provide, and thus allow for transparency.

One of the core logic-based formalisms in symbolic AI is Answer Set Programming (ASP) [Brewka et al., 2011; Lifschitz, 2019], which is based on logic programs under stable model semantics. In ASP, a problem is represented by a set of rules of the form H ← B in a first-order language (called "program"), where intuitively, H must hold whenever B is true. The models of such programs (called answer sets [Gelfond and Lifschitz, 1991]) then correspond to the solutions of the problem. The representation often follows a "guess-and-check" methodology, where solution candidates are generated (usually via choice rules) and invalid candidates ruled out through constraints. A notable feature of ASP is nonmonotonicity, i.e., adding rules to a program may cause new answer sets and that inferences from all answer sets no longer hold. It embraces the closed world assumption and can be fruitfully exploited to model exceptions and defaults, e.g., inertia rules in planning.

Thanks to its declarative and expressive language, the rich support for features such as aggregates, optimisation, and preference handling, and by the availability of efficient solvers, ASP is highly popular and widely used beyond AI in Computer Science and other fields. It has been used to solve a variety of problems such as combinatorial optimisation, logical reasoning, planning, bioinformatics, and data integration to name a few [Schaub and Woltran, 2018], with growing use in industry [Rajaratnam et al., 2023]. Moreover, recent work shows the potential of ASP for neuro-symbolic AI [Rader and Russo, 2025; Shakarian et al., 2023] and aiding Large Language Models in reasoning [Kareem et al., 2024; Rajasekharan et al., 2023].

Given that an ASP program is a declarative specification without explicit control flow, users might have issues following the underlying reasoning mechanisms, i.e., why a certain result was returned by the solver. Several tools and theories for explainability in ASP exist and continue to be investigated. Those explanation concepts not only differ in what kind of answer they provide, but also in what kind of setting they operate in. A previous landmark survey on explanations in ASP [Fandinno and Schulz, 2019] focuses on the questions of why a certain atom is (not) in a given answer set and why no answer set can be computed. However, from an XAI perspective scenarios, where an ASP user finds themselves with a question about the behaviour of the ASP system, are more diverse than these plain settings.

In this survey, we provide an overview of the types of explanations that may arise in ASP and show how they are covered by existing ASP explanation approaches. Specifically:

• By taking an XAI perspective, we structure our survey along Local vs. Global explanations, distinguishing explanations for computed answer sets and explanations over the general behaviour of the given program.
• We identify a comprehensive list of typical user questions. While some of them can be natively addressed by existing

methods, some cannot. Thus, we show how they can be reduced to other questions where explanations are possible.

• Naturally, we cover approaches and tools that were not available for Fandinno and Schulz's survey.
• The user-centric view also allows us to highlight explanatory settings where current concepts and tools are lacking, even though those scenarios may be encountered by ASP users. We thus propose directions for future research to fill these gaps, as well as to address recent developments in AI.

This survey is intended to serve both researchers, and ASP users who are not experts, but are looking for explanation tools and methods which fit their situation and purpose.

2 Answer Set Programming

Syntax. A (disjunctive) logic program is a finite set of rules:

where each αi is an atom of form p(t1, . . . , tn), where p is a predicate, and each ti is either a constant or a variable. A literal is either a formula α (positive literal) or not α (negative literal), where α is an atom. Intuitively, not α is true if α cannot be derived using rules, and false otherwise; not is called default negation. For a rule r of form H(r) ← B(r), we refer to H(r) as the head of r, and to B(r) as the body of r. The positive body atoms of r are denoted by B+(r) = {αk+1, . . . , αm}, and the negative body atoms by B-(r) = {αm+1, . . . , αn}. A rule r is normal if k = 1 and a constraint if k = 0; Furthermore, r is positive if n = m and a fact if k = n = 1 and it is variable-free. A rule is ground if all its literals are variable-free. A program P is normal, positive or ground if its rules are.Lastly, we use not S = {not s | s ∈ S} for any set of atoms S as a shorthand.

Example 1. Suppose the manager of the Bremen Town Musicians 1 relies on the following program P1 about donkeys:

The program has three non-ground rules and two facts; intuitively, a donkey which is classified as old will be sold unless it is a musician, and a donkey is a musician unless it is sold. All rules are normal and P1 is thus a normal program. However, one could also consider P2 resulting from P1 by replacing the first two rules with:

Here (6) is a disjunctive rule and (7) a constraint. The choice of becoming a musician is now expressed via disjunction.

1 Inspired by the Grimms' Fairy Tale

Semantics. The answer set semantics is defined via ground programs that are obtained by grounding as follows.

The Herbrand universe of a program P , denoted by HUP , is the set of all constant symbols appearing in P, and the Herbrand base of P , denoted by HBP , is the set of all ground atoms constructable with predicates from P and terms from HUP . The ground instances of a rule r ∈ P, denoted by grd(r, P), is the set of rules obtained by replacing all variables in r with constant symbols in HUP in all possible ways. The grounding of P is then grd(P) = ⋃r∈P grd(r, P).

An interpretation I of a ground program P is a subset of HBP . Such I (i) satisfies a literal ℓ, denoted by I |= ℓ, whenever α ∈ I if ℓ = α, and α ̸∈ I if ℓ = not α, (ii) satisfies a rule r ∈ P (denoted by I |= r) if H(r) ∩ I ̸= ∅ whenever B+(r) ⊆ I and B-(r) ∩ I = ∅, and satisfies (is a model of) P (denoted by I |= P), if I |= r for all r ∈ P. Amodel I of P is minimal if there is no J |= P such that J ⊂ I.

The Gelfond-Lifschitz (GL-)reduct P I of a program P relative to an interpretation I is the program obtained from grd(P ) when each rule H(r) ← B+(r), not B-(r) (i) with B-(r) ∩ I ̸= ∅ is deleted, and (ii) is replaced by H(r) ← B+(r), otherwise. Informally, the first step removes the rules where I contradicts some default negated literal, while the second step removes the negative body from all others.

An interpretation I is an answer set of a program P, if it is the minimal model of the GL-reduct P I . By AS(P) we denote the set of answer sets of a program P . A program P is unsatisfiable (or inconsistent) if AS(P) = ∅.

Example 2 (Ex. 1 cont'd). The Herbrand universe of P1 is HUP = {d, 25}. For the interpretation I1 = {donkey(d), age(d, 25), old(d), sold(d)}, we have (among others) the following rules in the reduct P I1 1 : 2

I1 is a minimal model of P I1 1 and thus I1 ∈ AS(P1).

Language extensions. The ASP-Core-2 Input Language Format [Calimeri et al., 2020] defines several language extensions; most are syntactic sugar but convenient in practice. We give here an informal account of some major constructs.

Aggregates are atoms of the form #aggr E ≺ u where #aggr is the aggregate type (#count, #sum, #min or #max), E is an aggregate set, ≺ is a comparison operator, and u is a term; they can appear only in rule bodies.

Example 3 (Ex. 1 cont'd). Let us add the facts donkey(e), age(e, 11) to P1, yielding P3. To express that at most one donkey can be a musician, we can add the constraint

The aggregate is true if the predicate musician holds for more than one constant; then the constraint "fires" and prevents that the interpretation is an answer set.

2 Rules which are trivially satisfied are not shown.

Choice rules are of the form l ≤ {e1; . . . ; en} ≤ u ← B and select between l and u atoms from e1, . . . , en; if l = u, we may write "= u".

Example 4 (Ex. 1 cont'd). The selection between sold(D) and musician(D) in (6) can be expressed with a choice rule:

The rule enforces that for each donkey D exactly one of sold(D) and musician(D) has to be true.

Weak constraints are of the form :∼ B. [w, t1, . . . , tm], where B is a set of literals, the ti are constants or variables, and w is the weight. They incur a penalty w if B is satisfied, i.e., the constraint instance is violated. An answer set is then assigned the sum of all such penalties; it is optimal, if it has minimal penalty. More elaborated versions have priority levels, which allow to conveniently express model preference.

Example 5 (Ex. 3 cont'd). Instead of enforcing that only one of the two donkeys in P3 can be a musician by the constraint (12), we can use also a weak constraint:

Each ground instance of (14) violated in an answer set incurs penalty 1. Hence, any optimal answer set will neither contain musician(d) nor musician(e) as both can be sold.

Further language extensions such as strong negation, conditional literals etc. ease problem encoding.

3 Forms of Explanations in ASP

Explainable AI (XAI) strives for making the behaviour of AI models, in particular of neural models such as classifiers, understandable to the user. While explainability and interpretability are often used interchangeably [Adadi and Berrada, 2018] and confused, the subject is usually either the output for a specific input, or insight into the model as a whole. This leads to (local) explanations (concerning a single data point) and global explanations (all data points), respectively, which in a logic-based setting can be defined using abduction principles [Marques-Silva, 2022], linking the notions to minimal satisfying assumptions and prime implicates.

We can align explainability of ASP with this distinction as follows. ASP programs are AI models, and answer sets of ASP programs are data points. Then local explanations refer to the case where the user has an answer set that they ask questions about. In contrast, global explanations address user questions about answer sets without having one at hand; here, the general program behaviour is of concern.

In the following, we will also speak of justification, which is sometimes used synonymously with the term explanation, and for our purposes we consider a justification a type of explanation.

3.1 Local Explanations

Local explanations in terms of ASP amount to explaining the reasoning behind an obtained answer set. In particular, given an answer set I of a program P, a user might ask questions about the presence or absence of certain atoms in I.

Q1 : Given I ∈ AS(P), why I |= ℓ for some literal ℓ? These forms of questions are the most common explanation problems with several approaches addressing such questions. Here we will briefly summarize the concepts, categorizing each distinct approach as a specific method, denoted by (M1), (M2), etc. We start with those which were already covered by the previous survey of Fandinno and Schulz [2019]. For more details we refer to that work.

Justifications. Offline justifications (M1) [Pontelli et al., 2009] are labelled directed graphs which, intuitively, can be seen as a step-by-step derivation of the truth value of the respective atom using the rules of the program, originally defined for ground, i.e., variable free, normal logic programs.

ABA-based justifications (M2) [Schulz and Toni, 2016] have their roots in abstract argumentation [Dung, 1995]. More specifically, they use arguments to describe the semantics of logic programs and the justifications are derived from trees of conflicting arguments (attack trees). A labeled assumptionbased argumentation (ABA)-based answer set (LABAS) justification is a graph structure where the vertices are literals and edges are either attacks (representing conflicts between arguments) or supports (representing derivation relationships).

Causal justifications (M3) [Cabalar and Fandinno, 2017] provide explanations for literals in a given answer set based on a causal semantics for logic programs. The basis for causal justifications are algebraic terms representing joint causation through multiplication and alternative causes through addition. These causal terms can be presented as directed graphs showing the causal dependencies between literals.

Justifications in rule-based ASP computation (M4) [B´eatrix et al., 2016] stem from the way the ASP solver ASPeRiX computes answer sets. Unlike to most solvers, it operates on the non-ground program and non-deterministically chooses rules rather than atoms. During this computation, the truth value of atoms is iteratively established and the reason for it being in the answer set is a set of ground rules which intuitively can be used to derive the atom in question.

Now we come to more recent methods or extensions.

Extended Justifications. The notion of offline justification has been recently extended to handle choice rules and constraints [Trieu et al., 2021] and implemented in the xASP2 system, also supporting aggregates [Alviano et al., 2024b].

One of the main changes in xASP2 is that it computes the well-founded model of the given program P first. 3 The explanation identifies which atoms are false in the well-founded model and determines a minimal set of additional atoms that must be assumed false. Together with the program facts, these allow deriving the atoms in I through rule application. The overall explanation is constructed in two phases: first, program rewriting and ASP meta encodings compute the minimal assumption set; second, these assumptions are used to generate a tree-like justification graph. The tree-like graph represents the rule application sequence yielding the target literal ℓ, where internal nodes correspond to rule applications and leaves are either facts, atoms false in the well-founded model, or assumptions.

3 Briefly, the well-founded model WFM(P ) is a 3-valued approximation of AS(P) where atoms true (resp. false) in WFM(P) are true (resp. false) in each I ∈ AS(P) [Van Gelder et al., 1991].

Example 6 (Ex. 1 cont'd). When we use xASP2 to explain why sold(d) is in I, its browser displays the graph in Fig. 1a. 4 The (green) root node sold(d) is connected via rule (1) to its positive body literals donkey(d) and old(d), which are also true in I and displayed in green. The negative body literal musician(d) is false in I; this is represented as a purple assumption node, indicating it must be assumed false for the derivation to hold. The atom old(d) (middle node) is further linked to its supporting facts age(d, 25) and donkey(d) dark green leaf nodes) via rule (3). This tree-like structure shows how sold(d) is derived from the program facts together with the assumption that musician(d) is false.

Another novel approach is explanations via unit-provable unsatisfiable subsets (1-PUS) (M5), which are the basis of the UCOREXPLAIN system [Alviano et al., 2024a]. The concept of a 1-PUS is similar to the notion of minimal unsatisfiable sets [Alviano et al., 2023] which is defined relative to a given set O of objective atoms, and is a minimal subset U ⊆ O such that P∪{{o} ≥ 0 ←| o ∈ O}∪{← not u | u ∈ U} has no answer sets. A 1-PUS differs by not checking the unsatisfiability of the amended program; instead, a simple set of (incomplete) derivation rules is used to check whether we can derive a contradiction. Furthermore, subset minimality is replaced with a user specified lexicographic order. In UCOREXPLAIN, the objective atoms O are auxiliary atoms that are injected into the rule bodies in the input program P. Intuitively, o∈O controls whether a particular rule is enabled. Furthermore, the system adds a special rule to the program which makes it inconsistent whenever the literal ℓ we seek to explain is true. Hence, a 1-PUS in this setting represents a preferred set of rules which, in conjunction with simple derivation rules, can be used to derive ℓ.

4 For space reasons, Fig. 1a shows a recreation.

The justifications provided by UCOREXPLAIN can then be displayed in a graph similar to xASP2. An important difference being that in xASP2, an atom a can only be justified by a rule r if a ∈ H(r), which is not so in UCOREXPLAIN.

Explanation trees are obtained from a class of a vertexlabeled tree of a program, with variations such as shortest and k different explanations [Erdem and Oztok, 2015].

Support Graphs. Support graphs (M6) are defined over labelled programs, where each rule r is given a label Lb(r) [Cabalar and Mu˜niz, 2024]. Furthermore, LB(P) = {Lb(r) | r ∈ P} is the set of all labels in program P . For each atom p in an answer set I, they then define the notion of support which is defined as SUP(P, I, p) = {r ∈ P | p ∈ H(r), I |= B(r)}, i.e., the set of rules of P which have p in their head and have a true body w.r.t. I. Now, a support graph is a labelled directed graph G = (I,E, λ) whose nodes are the atoms of the answer set I, edges e ⊆ I × I connect atoms, and λ : I → Lb(P) is an injective function assigning a label to each atom. Furthermore, it is required that for every p ∈ I, the rule r for which λ(p) = Lb(r) satisfies r ∈ SUP(P, I, p) and B+(r) = {q | (q, p) ∈ E}. Intuitively, p is connected to all positive body atoms of r. If a support graph G is acyclic, it is called an explanation. The system xclingo uses support graphs to provide explanations [Cabalar and Mu˜niz, 2024]. It can handle choice rules, but due to the nature of support graphs, it can only give explanations for atom which are in the given answer set.

Example 7 (Ex. 1 cont'd). Figure 1b shows the output of xclingo to explain sold(d) ∈ I. The atom sold(d) is connected to donkey(d) and old(d) to derive it using rule (1).

Furthermore, xclingo allows the ASP programmer to attach natural language messages to rules via annotations (e.g., %# message "..."). These messages replace technical rule references in explanations, enabling domain-specific explanations for end-users without ASP expertise.

Witnesses. Similarly, witnesses (M7) [Wang et al., 2022] are solver-independent but aim only at explaining positive literals. The notion aims at explaining why a set S of such literals is in a given answer set I of P by stepwise logical derivation, where in each step a set of rules in a reduct of P w.r.t. I augmented with already derived atoms is considered; for S = I, this amounts to explaining why I is an answer of P. For each step, a proof method, in particular resolution, may be chosen. In this way, an explanation of why I = {a, b} is an answer set of P = {a ∨ b, a ← b, b ← a}, can be given without resorting to guessing: for S = {a, b}, derive in step 1 a from a ∨ b. and a ← b by resolution, and in step 2 b from a and b ← a. Recently, witnesses have been extended to programs with constraint atoms [Wang et al., 2025].

Transform question into unsatisfiability. Interestingly, Q1 can be transformed into the question of why a program has no answer set. For example, explaining why a ∈ I reduces to explaining why P ∪ {← b | b ̸∈ I} ∪ {← ¬b | b ∈ I, b ̸= a} ∪ {← a} has no answer sets. The intuition is that we add the literals true/false in I as assumptions except for a which is forced to be false. This idea was implicitly applied by Alviano et al. [2024a]. It should be noted that for programs with choice rules the amended program may still be satisfiable. However, in such a case the literal is justified by the choice and there is no better explanation. Hence, explaining why a program is inconsistent, which is already of great interest by itself, could be a stepping stone to a more universal explanation approach.

Miller [2019] argues that why-questions of form Q1 are unequipped for providing proper explanations and instead questions should be seen as contrastive in the sense of "Why X and not Y ?". In our setting this translates to asking Q2. Although such a question can be transformed into unsatisfiability similar to above, which was considered for (weaker) questions of form "Why not Y ?" [Bogatarkan and Erdem, 2020], dedicated explanation techniques exist in ASP.

Contrastive Explanations for ASP. Eiter et al. [2023] give a formal framework for contrastive explanation (M8) in ASP. In detail, their approach assumes that the user wants to know why for a set of atoms E ⊆ I is included in the answer set instead of another set of atoms F ∩ I = ∅. In order to provide an answer to this question, a counterfactual account is generated which consists of a program P ′ with answer set I ′ such that E ∩ I ′ = ∅ and F ⊆ I ′ and P ′ is "similar" to P. The latter means that P ′ retains as many rules as possible from P and the rules r ∈ P ′ \ P are facts from a given set of assumables.

A counterfactual explanation is then a triple (Q1,Q2,Q∆), where Q1 and Q2 are essentially minimal sets of ground rules that derive E w.r.t. P and I, and F w.r.t. P ′ and I ′ , respec-

tively, and Q∆ = P \ P ′ is the set of rules that were removed.

The contrastive explanation results from the counterfactual explanation by taking the symmetric difference of Q1 and Q2 and removing the (optional) fixed rules, which must be in P ′ .

Example 8 (Ex. 1 cont'd). Consider again P1 and assume we add the following constraint yielding P4:

Now, the grounding of the program P4 includes the following rules:

It holds that AS(P4)={I1}. Suppose a user asks why sold(d)∈I1 rather than musician(d)∈I1, and the facts are fixed. The only contrastive explanation is then ({(16), (18)}, {(17)}, {19) intuitively meaning that (16) and (18) explain why sold(d) ∈ I1, but if (19) were removed, we could get musician(d) ∈ I1 via (17).

Q3 : Why is answer set I of P reported as optimal?

For programs with weak constraints, explanations for optimality would be of great interest. Although currently no method is specifically tailored to this question, it is possible to reduce it to checking why there is no answer set that is better. This can be done by introducing a constraint enforcing strictly less penalty than I. Explanation methods for the non-existence of answer sets, which we discuss later, can then be employed. While we classified this question as local, it could also be seen as global as the only thing we take from I is its cost.

3.2 Global Explanations

Global explanations aim to explain the model and its logic as a whole [Adadi and Berrada, 2018]. In terms of ASP, this concerns the following questions.

Q4 : Why is a (not) in some answer set of P?

Explaining why a appears, or does not appear, in some answer set of P can be seen as local where the I is left implicit. Hence, a local explanation, of a computed witness I, can be given. However, obtaining global explanations without needing a specific answer set at hand is also possible.

Why-not Provenance. This question has been tackled by why-not provenance (M9) [Dam´asio et al., 2013] which provides justifications for the truth values of atoms w.r.t. answer set semantics for normal logic programs. This notion has formal similarities with causal justifications, but rather than causal reasons it gives possible modifications of the program that are needed to ensure a certain truth value.

Top-down Computation (M10) The Constraint Answer Set Solving system s(CASP) [Arias et al., 2018] can provide justification trees for atoms contained in some answer set due to its implementation in Prolog. The system finds stable models by goal-directed search and top-down evaluation operating on the non-ground program. This means that the user essentially queries for a certain - potentially negated - predicate and is given an answer set where a particular ground instance of the predicate is contained. The process is top-down in the sense that it starts from the queried predicate and looks whether a ground instance can be justified in an answer set. This has the side effect of producing a justification tree which can be displayed to the user. Furthermore, this explanation also operates on the non-ground program, thus potentially yielding more compact explanations.

Example 9 (Ex. 1 cont'd). If we run s(CASP) for the ground query sold(d) on P1 and ask for a justification, it outputs

'sold' holds (for d), because 'donkey' holds (for d), and 'old' holds (for d), because 'donkey' holds (for d), justified above, and 'age' holds (for d, and 25). there is no evidence that 'musician' holds (for d), because 'donkey' holds (for d), justified above, and it is assumed that 'sold' holds (for d)

In a similar fashion, the Satoh-Iwayama procedure [Satoh and Iwayama, 1992; Dauphin and Satoh, 2019], which is also goal-directed, can be used to answer Q4. It also produces a derivation tree that can be given as a justification, but different from s(CASP), the procedure operates on ground programs.

Q5 : Why is a in no or in every answer set of P?

Dedicated explanation concepts related to questions of this form are proof systems (M11) for ASP. For example, Bonatti [2001] introduced a resolution calculus for sceptical entailment, which is when a appears in every answer set, and a tableaux calculus was introduced by Gebser and Schaub [2013]. Recently, Eiter and Geibinger [2025] presented a sequent calculus for sceptical entailment in equilibrium logic, which is a logical underpinning of ASP.

Similar to the questions in the previous section, answering why an atom a is in no (respectively, every) answer set of P can be reduced to explaining why P ∪ {← ¬a} (respectively, P ∪ {← a}) has no answer set.

Q6 : Why does P have no answer sets?

Generally, the works studying this question concern debugging, i.e., they aim not at a user seeking general explanations but rather to provide technical feedback to the ASP engineer who was expecting a different result, or proof logging, where solvers provide verifiable certificates for their results.

Debugging. One avenue of research into debugging is given by meta-encoding techniques (M12) which, intuitively, provide reasons why each interpretation is not an answer set. Systems that implement this approach are spock [Brain et al., 2007; Gebser et al., 2008] and Ouroboros [Oetsch et al., 2010]; for the latter no a-priori knowledge of inconsistency is needed when the user provides an interpretation whereas spock needs no such information. Another approach is to remove the inconsistency by utilizing minimal unsatisfiable sets (MUS) (M13), as done e.g. in DWASP [Dodaro et al., 2019]. A minimal unsatisfiable set contains (non-ground) rules of the program which cannot jointly hold, but if one of them were removed, then the program would be consistent. This concept has roots in model-based diagnosis and constraint satisfaction and has been generalized to nonmonotonic logics including ASP [Eiter et al., 2014; Brewka et al., 2019] taking the nonmonotonicity of the stable model semantics into account. Stepping (M14) [Oetsch et al., 2018] is an interactive debugging approach that lets the user build an intended answer set step by step, illustrating where the process fails. For more details on debugging techniques we refer to the survey of Fandinno and Schulz [2019].

Proof Systems. For Q5, we mentioned proof systems for ASP, which can also serve as a basis to answer question Q6, as it is essentially asking why ⊥ is derivable.

Furthermore, for certifying the result whenever a solver reports "unsat", specialised proof logging systems for SAT were adapted to ASP [Alviano et al., 2019; Chew et al., 2024]. Those systems output resolution proofs for the SAT clauses generated by the solver to derive ⊥.

Abstraction. In contrast to debugging and proof approaches, abstraction (M15) notions in ASP highlight the reason for unsolvability through omitting or clustering irrelevant details [Saribatur and Eiter, 2021; Saribatur et al., 2021]. Here, abstraction is considered as an over-approximation, where a program P ′ over A′ is called an abstraction of a program P over A, if there exists a mapping m : A → A′ ∪ {⊤} such that for each answer set I of P, I ′ = {m(l) | l ∈ I} is an answer set of P ′ , i.e., m(AS(P)) ⊆ AS(P ′ ). Omission-based abstraction [Saribatur and Eiter, 2021] relies on a mapping mA : A→A∪ {⊤} for a set A of atoms to be omitted, such that mA(α) = ⊤ if α ∈ A and mA(α) = α if α ∈ A \ A.

Thus mA(AS(P)) amounts to projecting away the omitted atoms, denoted as AS (P )|A. An abstract program omit (P, A) is constructed by a syntactic operator that removes rules with heads in A and add choice rules to the head of rules with body atoms occurring in A. This ensures over-approximation of the (projected) answer sets. An (answer set) blocker set refers to a set R of atoms that are kept in the vocabulary, while the rest is omitted from a ground program P to obtain the program omit(P, A\R), such that omit(P, A\R) is also unsatisfiable; the atoms in R are thus blocking occurrence of answer sets.

Example 10 (Ex. 8 cont'd). Assume we add the following rules to P4, yielding P5 that is unsatisfiable:

A blocker set for the grounding of the program P5 would be R = {donkey(d),musician(d), age(d, 25), canSing(d)}, with resulting abstraction omit(grd(P5),A \ R) as below that is still unsatisfiable.

In fact R would be the minimal blocker set, as omitting further atoms would no longer preserve unsatisfiability.

A CEGAR-style [Clarke et al., 2003] abstraction and refinement methodology enables automated computation of these atom sets. This is lifted to the non-ground case for clustering of domain elements [Saribatur et al., 2021] to find abstractions that "zoom-in" on the unsatisfiable part of the program.

3.3 Summary

Table 1 presents an overview of the explanation techniques we addressed in this section; the symbol ∗ means one can reduce the question to another one and use the latter's method, like how we can explain why an atom is in some answer set (Q4) by providing a witness and using it for the explanation (Q1). We show which questions these techniques can explain, which program type they support, whether they support explaining positive or negative atoms (or both), if they are solver-dependent, and their explanation output. We can observe that all of the questions can be explained natively or via transforming to another question. While Q3 is the only question with no native explanation, Q2 and Q5 have one dedicated technique, and the rest of the questions have multiple supporting techniques. Observe that many of the questions can be reduced to explaining unsatisfiability. Most of the methods can explain both truth values, and there is a balanced view of solver-dependency. We see quite a diversity in the explanation outputs.

Other Related Explanation Methods

The system fasp [Fichte et al., 2022] allows for navigation toward desired partial solutions (called facets) in ASP, which recently was extended to navigate the solution space of ASPencoded planning tasks [Gnad et al., 2025]. Facets are atoms that occur in some but not all answer sets. Interactively enforcing or forbidding such facets to see which properties hold allows the user to better understand the solution space. A further recent answer set explorer is viasp [Glaser et al., 2025].

Model reconciliation is a form of contrastive explanation by reconciling the system's and the user's model (i.e., programs) to agree on a property of the made decision, which was also considered in ASP with a focus on planning [Son et al., 2021; Nguyen et al., 2020].

4 Outlook for Explainable ASP

Having reviewed the existing ASP explanation approaches, we spot gaps and present issues for future research.

4.1 Practical Aspects

Notably, there are more explanation concepts than actual software tools implementing them. Issues with the tools include the following ones.

Language Features. As shown in Section 2, disjunction and language extensions can help with representing challenging real-world problems. Table 2 summarizes the language support of available explanation tools. Although, with recent advances, there are more tools supporting language extensions, there are still some gaps. Disjunction is often not supported by the tools, because the underlying explanation method cannot generally handle it. The reason for that being the increase in expressiveness when one adds disjunctive rules with headcycles. Support for aggregates and choice rules has increased, but most tools still do not support them or have some syntactic restriction on them. Weak constraints are still generally not supported. Here DWASP is the exception, though this is a debugging tool - supporting weak constraints is independent from a diagnosis on how to restore consistency.

System Divide. The methods implemented in current systems either focus on providing local explanations or global ones. This puts the burden of deciding on which system(s) to employ on the user, depending on the questions they have and may cause undesired overhead.

Scalability/Non-ground ASP. Since most of these approaches can be considered as post-hoc, meaning that they are for explaining an encountered outcome, e.g., an answer set or none, the techniques need to reconstruct the reasoning that achieves the result in order to explain it. This of course causes issues especially if the problem at hand is large or difficult to solve. Given that providing explanations has high computational complexity in general [Eiter et al., 2023; Wang et al., 2022], it is important to find ways to tackle scalability, e.g., by incorporating explanation techniques into the ASP solvers. Also most explanation approaches operate on ground programs where all variables have been instantiated, except for s(CASP), which also justifies the instantiation of the variables. While ASP solvers also often only operate on ground programs, in the scope of explanation, preserving the relationship between ground atoms that were obtained from instantiating the same predicate may be beneficial.

Complex User Questions. Currently, in case of questions that arise over a collection of answer sets, the only way to address them is to get explanations for each answer set. However, when a user asks Q7: Why is a (not) in answer sets I1, . . . , In?, they expect a global explanation on the behaviour of the program that obtains a in those particular answer sets, which currently cannot be obtained. Explanations with respect to the quantity of answer sets, which may be needed for industrial settings with configuration problems etc., also cannot be addressed through any of the approaches. These questions can be of form Q8 : Why does P have so many/few answer sets? and likely need dedicated solutions. Facets [Fichte et al., 2022] could be a worthwhile technique when constructing such explanations. Observe that these questions can also be seen as contrastive, as the user has encountered a number of answer sets against their expectation. Thus explanations on under-/over-restrictions would be of use. Furthermore, as symmetry is another cause for many answers, explanations that also show the detected symmetries might be helpful.

4.2 Cognitive Aspects

Here, we consider cognitive aspects of explanations in ASP.

Conciseness. One challenge is reducing information complexity of explanations for large programs, as they may contain many rules to trace. Providing more concise explanations from a possibly higher-level view remains open. Abstraction can be helpful to achieve this, as considered in other domains, e.g., planning [Sreedharan et al., 2021] and mathematical reasoning [Poesia Reis e Silva and Goodman, 2022]. Recent work reports a dual effect of applying abstraction in ASP explanations: abstraction by clustering helps in understanding, while omission reduces cognitive effort [Saribatur et al., 2026]. These results support the need for further investigations on obtaining concise explanations.

Interpretability. An important aspect when providing explanations is whether the provided explanation is indeed understandable to the user, especially if they are not experts. While justifications or similar techniques aim to provide the reasoning behind the made decision, contrastive explanations have insight into the epistemic state of the explainee and can focus on the actual core of the misunderstanding [Miller, 2019].

Regarding explaining inconsistency, due its difficult nature, finding a satisfying answer is challenging. Concepts from debugging, like minimal unsatisfiable subsets or proof logging may be used, but it is unclear how respective rule sets should be presented to a non-expert. Notably, the idea was successfully applied for ASP-based product configuration [Herud et al., 2022], which is a domain where minimal unsatisfiable subsets can easily be translated into an explanation. Step-wise explanation notions [Bogaerts et al., 2020; Oetsch et al., 2018] could be beneficial for understanding how unsatisfiability in ASP is brought about.

Taking into account the aim of conciseness, one idea for explaining inconsistency is by some hidden "lemma". For example, a graph colouring instance may be inconsistent due to some clique in the graph. Revealing this clique would be an adequate explanation for users with sufficient domain knowledge. However, how such explanation could be derived is unknown. Abstraction could be useful but also investigating interpolation, which could produce the lemma, might be worthwhile [Gabbay et al., 2010].

Interaction and Communication. Another issue with the available explanation techniques is the lack of user-friendly tools that allow one to obtain explanations without much technical expertise. In order to communicate the highly technical explanation to the end-user, Large Language Models (LLMs)

might be of help. This has been explored in preliminary work on explanations for guess-and-check programs where questions are parsed by an LLM and the resulting MUS is translated by the LLM into natural language [Geibinger et al., 2024].

Recently LLMs and symbolic solvers were bridged through the Model Context Protocol (MCP) [Szeider, 2025]. It enables LLMs to access formal reasoning capabilities including ASP, showing potential in achieving a user-friendly interaction for ASP explanations. Furthermore, it remains to be explored whether LLMs can be used to find explanations for ASP.

5 Conclusion

We have provided an overview of explanations in ASP from an XAI perspective, structured along explanation types and on what questions the ASP user might find themselves with. We profiled a number of existing explanation methods and existing systems that can be used off-the-shelf to address the user questions. Overall, there is a rich landscape of methods and systems available with diversity in explanation types, question support, and explanation formats, but none fits all needs.

We further presented issues from practical and cognitive perspectives to address, some of which concern limitation in language support, complex user questions, and, importantly, interpretability and communication. Notably, most of the user questions can be transformed into unsatisfiability; thus advanced explanations for program inconsistency could provide a stepping stone to more universal explanation approaches. That and connecting to latest AI research poses a challenge.

Acknowledgments

This research was funded in whole or in part by the Austrian Science Fund (FWF) grants 10.55776/COE12 and 10.55776/T1315, the Vienna Science and Technology Fund (WWTF) grant 10.47379/ICT25044, and benefited from the European Union's Horizon 2020 research and innovation programme under grant agreement No 101034440 (LogiCS@TUWien).

Tobias Geibinger is a recipient of a DOC Fellowship of the Austrian Academy of Sciences.