Explaining Answer-Set Programs with Abstract Constraint Atoms

1 Introduction

The growing pervasiveness of artificial intelligence (AI) in everyday life has led to concerns about the transparency of AI systems, and regulations against using "black-box" systems for sensitive tasks are under development.

Answer-Set Programming (ASP) is a symbolic, rule-based reasoning formalism that has been employed for various AI applications in numerous domains [Erdem et al., 2016; Falkner et al., 2018], among them life sciences [Erdem and Oztok, 2015], health insurance [Beierle et al., 2005], or psychology [Inclezan, 2015], to mention a few.

ASP allows for a declarative encoding of problems in a succinct manner. Solutions for them are obtained from answersets, which result from the evaluation of the encoding using an ASP solver. While ASP is a declarative AI approach, there is still need for providing concise and interpretable explanations as to why certain facts are, or are not, in a computed answerset. For this reason, a number of explanation approaches for ASP have been developed; we refer to [Fandinno and Schulz, 2019] for a comprehensive survey and to the Related Work section for more discussion. However, most of the approaches in the literature do not support language extensions like aggregates [Faber et al., 2004] or choice rules [Gebser et al., 2012]. As both features are frequently used in practice, the applicability of explanation approaches is limited and ASP can not live up to its full potential of a transparent AI tool.

We tackle this shortcoming by introducing several formal notions of justification based on programs with Abstract Constraint atoms (c-atoms) [Marek and Truszczynski, 2004]. The choice of the latter is motivated by the fact that such programs embrace many of the common ASP language extensions. Our main contributions are briefly summarized as follows.

• We introduce formal notions aiming to give reasons as to why an atom is true, respectively, false in a given answerset. To this end, we present both model-based and rule-based notions of justification to answer these questions, guided by the basic principles of sufficiency, coherence, and conciseness.
• Specifically, the model-based notion (m-justification) resorts to minimal partial model semantics, and aims to reveal what parts of the answer-set are responsible for the (non)satisfaction of possibly negated c-atoms and, in further generalisation, to the firing or non-firing of single rules.
• The rule-based notion (r-justification) takes the whole program into account and shows in a more operational view how an atom is derived or excluded from the answer-set in terms of an r-justification chain, which is a suitable sequence of r-justifications. Different from some other proposals in the literature, such chains proceed top-down and expand on false atoms, revealing that their derivation is blocked by missing support in a non-constructive manner (cf. Section 7).
• We analyse the computational complexity of problems related to recognising and computing the novel notions of justifications on an abstract basis for representing c-atoms. The complexity ranges for the recognition problems from NP/coNP to Σp2 , while computing justifications is feasible in polynomial time with an NP oracle.

Our notions of justifications provide succinct reasons for the presence or absence of an atom in an answer-set. They can serve as building blocks for more comprehensive justifications, and may be used in tandem to obtain more insight on answersets and make them better understandable. In particular, we imagine that our notions can be utilised in an interactive fashion where the user has control over which rules get expanded and explained. This top-down approach is also more akin to query answering than the common bottom-up approach and thus more aligns with the user perspective. This is especially the case when one considers interactive justification finding, where the user starts with the atom that should be justified and proceeds by finding supporting rules (r-justifications) and looking at what is needed to fire those rules (m-justifications).

Proofs of the results will be included in an extended version.

2 Preliminaries

We consider propositional Answer-Set Programming (ASP), assuming a denumberable set A of propositional atoms.

In particular, we consider programs consisting of Abstract Constraint Atoms (c-atoms) [Marek and Truszczynski, 2004], which are defined as follows. A c-atom is a tuple A = ⟨D, C⟩, where D ⊆ A is the domain and C ⊆ 2D are the satisfiers of the c-atom. Note that we require that C is smooth, i.e., for every S ∈ C there is some S′ ⊆ S such that S′ is ⊆-minimal in C. For a c-atom A, we will use DA to denote its domain and C A to denote its satisfiers. A c-literal is either a c-atom A (positive c-literal) or its (default) negation not A (negative c-literal). Similar to [Shen et al., 2009], we use ⊥ to denote ⟨D, ∅⟩ for any domain D and ⊤ for ⟨∅, {∅}⟩.

The notion of c-atoms effectively generalises propositional atoms: any propositional atom a can be expressed by the c-atom ⟨{a}, {{a}}⟩. We call the latter elementary and whenever convenient, we will identify it with a.

We define the complement of a c-atom A = ⟨D,C⟩ as A = ⟨D, C⟩ where C = 2D \ C are the non-satisfiers of A. Clearly, A = A holds.

Furthermore, A = ⟨D,C⟩ is called (a) monotone if for every S ∈ C it holds that S′ ∈ C for every S′ such that S ⊆ S′ ⊆ D, (b) convex if for every S ∈ C it holds that for every S′ and S′′ such that S ⊆ S′ ⊆ S′′ ⊆ D, S′′ ∈ C implies S′ ∈ C, and (c) bi-smooth if C is also smooth. A c-literal not A is called monotone (respectively convex or bismooth) if A is. This is naturally extended to sets of c-literals. Clearly, monotonicity implies convexity and any c-atom over a finite domain is bi-smooth.

Following [Oetsch et al., 2018], we define (disjunctive) logic programs over c-atoms, which consist of a finite number of rules of the form

where A1, . . . , An are c-atoms, l ≥ 1 and m, n ≥ 2. We call a rule normal if l = 1; a fact if l = 1, m = n = 2 and Am = ⊤, a constraint if l = 1 and Al = ⊥; positive if n = m; definite if it is normal and |AC1 | = 1; basic if it is normal and A1 is elementary; and convex if every Ai, for l < i ≤ n, is convex. We call a program normal, (positive, definite, basic, convex) if all of its rules are. Note that, different to most of the literature, we do not allow empty rule heads or bodies, because we can express constraints with ⊥ and facts using ⊤.

For a rule r of the form (1), H(r) := {A0, . . . ,Al} is the head of the rule, whereas B+(r) := {Al+1, . . . ,Am} and B-(r) := {Am+1, . . . , An} are the positive and, respectively, negative body. Furthermore, B(r) := B+(r) ∪ not B-(r), where not S := {not A | A ∈ S} for any set of c-atoms S. The set of all propositional atoms appearing in program P is denoted by AP .

Sometimes we will also prefix rules with labels, i.e., write l : r where l is the label and r is a rule as defined above, to give proper names to rules and ease readability.

The semantics of logic programs is based on interpretations. Here, we also introduce them as potentially partial. A partial interpretation is a tuple I = ⟨I +, I -⟩, where I +, I - ⊆ A and I + ∩ I - = ∅. A partial interpretation I = ⟨I +, I -⟩ is total on set S if I + ∪ I - ⊇ S. Intuitively, this indicates that no atoms in the set S are undefined by I. When it is clear from context, we drop the set S and by default, we assume interpretations are total and identify them by the single set I +. Furthermore, we say that I is finite if I + is.

Satisfaction of c-atoms is defined as follows. This definition, which is mostly based on [Son and Pontelli, 2007], is semantically equivalent to the one of [Wang et al., 2012]. However, unlike them, we do not require prefixed powersets and thus needless auxiliary definitions.

A c-atom A = ⟨D, C⟩ is satisfied by a partial interpretation I = ⟨I +, I -⟩, denoted I |= A, if S ∈ C, where S = I + ∩D and for each U ∈ C s.t. S ⊂ U, it holds that U ∩ I - ̸= ∅.

The partial interpretation I satisfies not A (I |= not A) if for each S ∈ C, either (a) S∩I - ̸= ∅ or (b) (U \S)∩I + ̸= ∅ for U = ⋃{X ∈ C | S ⊆ X}.

Intuitively, a c-atom is satisfied by an interpretation I if one of its satisfiers, which cannot be extended to an unsatisfier, is known to be true. In contrast, a c-atom is falsified by I, i.e., I |= not A, if for each of its satisfiers at least one of (a) or (b) hold. Intuitively, (a) L implies that the satisfier is known to be false, whereas (b) ensures that something is already known to be true which, in addition with the satisfier, makes I + ∩ D a non-satisfier. In other words, (b) states that even if the satisfier would be true, the resulting extension of the interpretation would not satisfy the c-atom.

For a set of c-literals L, we say a (partial) interpretation I satisfies L, denoted I |= L , if I |= L for every L ∈ L; satisfies a rule r, denoted I |= r, if I |= L for some L ∈ H(r) whenever I |= B(r). A (partial) interpretation is a model of L if I |= L and a countermodel otherwise.

Example 1. Consider the c-atom A = ⟨D, C⟩, where D = {a, b} and C = {{a}}, and the partial interpretation J1 = ⟨{a}, ∅⟩. Now, even though a ∈ J + 1 is known to be true, we have J1 ̸|= A, since {a, b} ∈ C and b ̸∈ J - 1 . Furthermore, J1 ̸|= not A because neither condition (a) nor (b) of the definition above holds. The latter does not hold, since for the only satisfier S = {a}, U = {a, b} and thus (U \S)∩J + = ∅.

Now, consider the partial interpretation J2 = ⟨{a}, {b}⟩. Clearly, now J2 |= A as well as J2 ̸|= not A hold, the latter for the same reason as above.

A seminal concept in ASP is the notion of reduct. The original GL reduct [Gelfond and Lifschitz, 1988] is the most known, but it is only defined over propositional programs without c-atoms. Several reducts have been introduced to handle them. Here, we use the following, which is a slight variation of the so called FLP reduct [Faber et al., 2004].

Let P be a program and I be a total interpretation. Then

where HR(M, I) := {⟨DA, {I ∩ DA}⟩ | A ∈ M, I |= A} if I |= H(r) and HR(M, I) := ⊥ otherwise, is the extended FLP reduct of P with respect to I.

A finite total interpretation I is then an answer-set of P if I |= P I and there is no total interpretation I ′ ⊂ I such that I ′ |= P I . The set of all answer-sets of P is denoted by AS(P). Note that Oetsch et al. 2012 gave a similar definition using a different version of the FLP reduct. However, their notion of answer-set seems to coincide with our. The introduced semantics neatly generalise aggregates and choice atoms as implemented in the ASP solver DLV [Leone et al., 2006] and, with restrictions, in the solver clingo [Gebser et al., 2014].

3 Basic Properties of c-Literals

Our definitions allow us to derive some useful properties of (sets of) c-literals.

Proposition 1. Given a c-atomA, then for every partial interpretation J we have J |= not A iff J |= A.

This proposition, which was used implicitly in [Son and Pontelli, 2007], allows us to use complements of c-atoms and their negation interchangeably. Furthermore, it turns out that a set of c-atoms, and thus c-literals by the above proposition, can be merged into a single c-atom.

Theorem 1. For every set L = {L1, . . . ,Ln} of c-literals there is a c-atomAL such that for every partial interpretation J, we have J |= L iff J |= AL. Furthermore, if L is a set of convex c-literals, then AL is convex as well.

The intuition here is as follows. The domains of the c-atoms can simply be merged and the satisfiers are then all subsets of the resulting domain that are satisfiers of all c-atoms in the original when intersected with the respective domain.

We define the following order over partial interpretations.

Definition 1. Let J1 and J2 be partial interpretations. Then J1 ≤ J2 if J + 1 ⊆ J + 2 and J - 1 ⊆ J - 2 . Furthermore, J1 < J2 if J1 ≤ J2 and J1 ̸= J2.

We have an intuitive result on the monotonicity of partial interpretations.

Proposition 2. Let J1 and J2 be partial interpretations s.t. J1 ≤ J2. Then, for every c-literal L, J1 |= L implies J2 |= L.

4 Model-based Justifications

Inspired by the philosophical study of explanation and justification, c.f. [Miller, 2019], we argue that a justification for the inclusion, or non-inclusion, of an atom in an answer-set should obey the following properties, which are intuitively described as:

Sufficiency: The justification should give sufficient reason to why the atom is or is not contained in the answer-set.

Coherence: The justification should be coherent, i.e., the justification contains nothing which is in contradiction with the answer-set.

Conciseness: The justification should be concise, meaning that it contains no superfluous information.

Note that the last property is not the same as the following, which we do not require.

Necessity: The justification is necessary, i.e., the inclusion, or non-inclusion, of the atom follows from the knowledge given in the justification. If the content of the latter were false, then the atom would not, or would respectively, be contained in the answer-set.

The reason why we do not demand necessity will become clear later on. In this section, we will introduce formal notions of justification for (non)satisfaction of c-atoms w.r.t. a given answer-set without taking the respective program into account.

4.1 Justifications for c-literals

We now come to our notion of what justifies the satisfaction of a c-atom.

Definition 2. Let L be a c-literal and I be a total model of L. Then, a partial interpretation J is called a (positive) mjustification of I |= L if (i) J ≤ I, (ii) J |= L and (iii) there is no J ′ < J such that J ′ |= L. The set of all m-justifications of L w.r.t. I is denoted by J (L, I).

The intuition here is that an m-justification should highlight the parts of the model that are responsible for the satisfaction of the c-literal. The condition (i) enforces coherence, (ii) ensures that the m-justification is sufficient and (iii) describes conciseness. Furthermore, we have the following property.

Definition 3. Let L be a c-literal and J be an m-justification of I |= L. Then we call J definite if J(L, I) = {J}.

Generally, c-atoms will not have a definite m-justification, which is why we do not require this property in Definition 2.

In the case of a definite m-justification, we also have an important theorem, which shows that definite m-justifications satisfy our informal notion of "necessity".

Theorem 2. Suppose J = ⟨J +, J -⟩ is a definite mjustification of I |= L. Then, for every X ̸= ∅, (i) I \ X ̸|= L if X ⊆ J +, and (i) I ∪ X ̸|= L if X ⊆ J -.

Definition 2 can be readily extended to non-satisfaction.

Definition 4. Let L be a c-literal and I be a total countermodel of L. Then J is a (negative) m-justification of I ̸|= L if J is an m-justification of I |= L.

As stated, m-justifications are not unique, but there is always at least one as we are going to show now. First, we establish the following result.

Proposition 3. Let I be a total interpretation. Then for every c-atomA, either I |= A or I |= not A.

Intuitively, the proposition states that for a total interpretation, the truth value of a c-literal cannot be undefined.

Proposition 4. Let L be a bi-smooth c-literal and I be a total interpretation. Then there exists some J ≤ I such that J is an m-justification either for I |= L or for I ̸|= L.

Example 2. Consider the c-atom A1 = ⟨D1, C1⟩ where D1 = {a, b, c} and C1 = {{a}, {b, c}, {a, b}, {a, c}, {a, b, c}}, which represents the aggregate #sum{2 : a, 1 : b, 1 : c} > 1. Suppose we have I1 = {a, b, c} and S1 = I ∩ D1. Clearly, S1 ∈ C1 and thus I1 |= A1. Furthermore, ⟨{a}, ∅⟩ and ⟨{b, c}, ∅⟩ are valid m-justifications. The former can be read as follows: the c-atom A1 is satisfied by I because a is true. Consider I2 = {b}. Since I2 ̸|= A1, we may look for mjustifications of A = ⟨D1, {∅, {b}, {c}}⟩. The partial interpretation ⟨∅, {a, c}⟩ is the only m-justification. The intuition here is that I2 ̸|= A1 holds because neither a nor c are satisfied by I2, which, since b cannot be false in I2, would be a requirement for A to be satisfied.

Example 3. Consider the aggregate atom #max{1 : a, 1 : b, 2 : c} < 2 and let A2 = ⟨D2, C2⟩ be the corresponding c-atom, i.e., D2 = {a, b, c} and C2 = {∅, {a}, {b}, {a, b}}. Suppose we have model I3 = {a, b}. Then, ⟨∅, {c}⟩ is a definite m-justification.

Example 4. Consider the aggregate atom #sum{1 : a, 1 : b, 1 : c} = 1 and let A3 = ⟨D3, C3⟩ be the corresponding c-atom, i.e., D3 = {a, b, c} and C3 = {{a}, {b}, {c}}. Suppose we have a model I4 = {a}. The only valid m-justification is ⟨{a}, {b, c}⟩, which intuitively says that I4 |= A3 holds, i.e., the sum is exactly 1, because a is true and b and c are false.

4.2 Justifications for Sets of c-literals

We extend our notion of justifications from c-literals to sets of c-literals in the following way.

Definition 5. Let L = {L1, . . . , Ln} be a set of c-literals and I be a total model of L. Then, a partial model J of L is called

• (i) a locally concise (positive) m-justification if there is a sequence of m-justifications J1, . . . , Jn such that Ji ∈ J (Li, I) and J = ⟨⋃1≤i≤n J + i , ⋃1≤i≤n J - i ⟩, and
• (ii) a globally concise (positive) m-justification if there is no partial interpretation J ′ < J such that J ′ |= L.

Clearly, every m-justification for a set is sufficient and coherent. Notably, according to our definition, an m-justification for a set of c-literals is only the ≤-minimal partial model if it is globally concise. The basic idea is that global conciseness might be too strong in some cases, since it prefers m-justifications that are concise and sufficient for multiple c-literals. In contrast, local conciseness only requires the mjustification to be the union of m-justifications for all c-literals.

Example 5. Consider the set of c-literals L1 = {A4,A5}, where A4 represents the #sum{2 : a, 1 : b, 1 : c} > 1 and A5 represents #max{2 : a, 1 : b} > 1. Furthermore, let I5 = {a, b, c} an interpretation. We know from previous examples that J(A4, I5) = {⟨{a}, ∅⟩, ⟨{b, c}, ∅⟩} and we clearly have J(A5, I5) = {⟨{a}, ∅⟩}. We have one globally concise m-justification for L1, ⟨{a}, ∅⟩, while there are two locally concise m-justifications, namely, ⟨{a}, ∅⟩ and ⟨{a, b, c}, ∅⟩. Global conciseness would ignore one of the two m-justifications for A4. Of course, it can be argued that ⟨{a}, ∅⟩ is in fact a stronger m-justification for L1 than ⟨{a, b, c}, ∅⟩ as it is non-redundant. However, depending on the context, the additional m-justifications obtained through local conciseness provide broader, more inclusive explanations and more diversity.

We can again easily adopt our notions to non-satisfaction.

Definition 6. Let L be a set of c-literals and I be a total countermodel of L. Then, a partial interpretation J is a locally concise (negative) m-justification of I ̸|= L if J is an m-justification of L for some L ∈ L. Furthermore, J is globally concise if there is no partial interpretation J ′ < J such that J ′ is an m-justification of I |= L for some L ∈ L.

For convenience, given a total interpretation I, a set L of c-literals and a partial interpretation J, we say that J is an m-justification for L if it is an m-justification for I |= L or I ̸|= L. Similarly, for single c-literals.

5 Rule-based Justifications

We now come to giving rule-based justifications, i.e., we aim to explain why atoms are in a given answer-set, but in addition to the previous section, we take the program into account as well. First, we give the following definitions.

Definition 7 (Presumptuous Entailment). Let P be a program, J be a partial interpretation and A be a c-atom. Then we define P |=J A if for every total model I of P s.t. I ≥ J, it holds that I |= A.

The idea behind Presumptuous entailment is that we want to define inferences under certain preconditions; viz., when we have some information about what is, or is not, true.

The next definition is based the known concept of support in answer-set semantics [Lifschitz, 2010].

Definition 8. Let r be a rule and I be a total model of r. Then, r is a failed support for atom a w.r.t. I if I ̸|= B(r) and for every I ′ , I ′ |= a if I ′ |= r and I ′ |= B(r).

The intuition behind failed supports is that they are rules whose body is not satisfied, but if they would be active, then the respective atom would also have to be true.

We now come to the main notions of this section.

Definition 9. Let P be a program, I ∈ AS(P) be an answerset and a be an atom. Then, a triple (a◦ ,Q, J), where ◦ ∈ {+,-}, Q ⊆ P is a set of rules, and J ≤ I is a partial interpretation, is an r-justification for a w.r.t. P and I if the following conditions hold:

• (a) If a ∈ I, then ◦ = +, QI |=J a and there is no R ⊂ Q such that RI |=J a.
• (b) If a ̸∈ I, then ◦ = -, Q = {r ∈ P | r is a failed support of a w.r.t. I}, and for every r ∈ Q, J |= A for some A ∈ B(r).

We say that the r-justification is concise if J is ≤-minimal.

An r-justification is essentially composed of three things: (1) An annoted atom indicating what is justified, (2) the set of rules needed to do so, and (3) a partial interpretation explaining why the rules do, or respectively do not, yield the atom. Recalling our informal notions of what properties a justification should have, we see that "sufficiency" and "coherence" are defined by reflection. Furthermore, both conditions (a) and (b) ensure that the set of rules Q is minimal and thus contains no redundant rules.

Example 6. Consider the program P1 = {r1 : d ← ⟨{a, b, c}, {∅, {a}, {b}, {a, b}}⟩, r2 : a ← not c, r3 : c ←

not a } and one of its answer-sets {a, d}. Intuitively, the body of rule r1 is true whenever c is false and the other encode a choice between a and c. The concise r-justifications for a, b, c and d are then (a+, {r2}, ⟨∅, {c}⟩), (b-, ∅, ⟨∅, ∅⟩), (c-, {r3}, ⟨{a}, ∅⟩) and (d+, {r1}, ⟨∅, {c}⟩).

The next theorem shows that r-justifications always exist.

Theorem 3. Let P be a program and I ∈ AS(P) be an answer-set of P. Then for every atom a, there is an rjustification (a◦ , Q, J) w.r.t. P and I.

We want to utilise this notion to justify atoms step by step. We do this by chaining r-justifications providing something akin to rule derivation, but with negative atoms mixed in.

Definition 10. We call a sequence of r-justifications w.r.t. P and I, J = (a◦1 , Q1, J1), . . . , (a◦n , Qn, Jn) an r-justification chain for a1 if for every (a◦i ,Qi, Ji) ∈ J , it holds that

• (a) for each a ∈ J + i some (a+j ,Qj, Jj) exists such that aj = a and either j > i or aj = a1 and there is no subsequence (a+k1 , Qk1 , Jk1 ), . . . , (a+kℓ , Qkℓ , Jkℓ ) of J where k1 = 1, kℓ = i, and akh+1 ∈ J + kh , for all 1 < h < ℓ;
• (b) for each a ∈ J - i some (a-j ,Qj, Jj) exists s.t. aj = a;
• (c) if i > 1, then there is some (a◦j ,Qj, Jj) such that ai ∈ J ◦ j and j < i; and
• (d) ai = aj for 1 ≤ j ≤ n implies i = j.

The intuition here is that positive information must be justified recursively, which eventually bottoms out, while negative information can be cyclic. Condition (a) ensures that each positive premise of a positive r-justification has some positive r-justification that comes later, with an exception for the case when the premise in question is the starting atom a1 to be positively justified: if there is no chain as described, the r-justification (a+i ,Qi, Ji) is definitely not needed to derive the atom a1, but only to "block" the derivation of some other atom. Example 9 shows such a case. Condition (b) enforces that negative premises are justified somewhere in the chain, but not necessarily after their usage. Condition (c) merely ensures that the chain does not contain unnecessary r-justifications, whereas (d) enforces that each atom appears at most once.

Example 7. Consider P2 = {r4 : ⟨{a, b}, {{a}, {b}}⟩ ← a}. Clearly, the only answer-set of P2 is ∅ and the r-justifications for a and b not being true are (a-, {r4}, ⟨∅, {a}⟩) and (b-, ∅, ⟨∅, {a}⟩). In fact the former is also an r-justification chain, since a not being true is justified by itself and the nonfiring of rule r4.

Note that for negative r-justifications, we do not require that the assumptions are justified by further r-justification to the right, but rather that they appear somewhere in the chain.

Example 8. Let us consider P3 = {r5 : a ← ⟨{b}, ∅⟩, r6 : b ← ⟨{a}, ∅⟩}. Now, P3 has two answer-sets {a} and {b}. The justification chain for a w.r.t {a} is then (a+, {r5}, ⟨∅, {b}⟩), (b-, {r6}, ⟨{a}, ∅⟩).

The intuition here is that negative atoms have no constructive role in the answer-set and thus do not have to be built "bottom-up". There can be situations where a positive rjustification requires a positive atom that has already been justified.

Example 9. Consider the program P4 = {r7 : a ← not b, r8 : b ← not c, r9 : c ← a}. Now, P4 has answer-set {a, c} and an r-justification chain for a is (a+, {r7}, ⟨∅, {b}⟩), (b-, {r8}, ⟨{c}, ∅⟩), (c+, {r9}, ⟨{a}, ∅⟩).

In the last element of the chain c depends on a being true which has already been justified in the beginning.

For an answer-set, r-justification chains can always be found for every atom.

Theorem 4. Let P be a program and I ∈ AS(P) be an answer-set of P. Then for every atom a, there is an rjustification chain J for a w.r.t. P and I.

However, not all r-justification chains will offer the most insight.

Example 10. For the program P5 = {r10 : a ← b, r11 : b ← not c, r12 : ⊥← c}, the set {a, b} is the unique answerset and J = (a+, {r10, r11}, ⟨∅, {c}⟩), (c-, ∅, ⟨∅, ∅⟩) is an r-justification chain for a.

In the above example, the derivation of b through r11 is hidden in the first element of the chain. Ideally we want to decompose such an r-justification and put an r-justification for b before the one for a. This idea motivates the next definition.

Definition 11. Given an r-justification (a+, Q, J) we call rjustifications (a+1 ,Q1, J1), (a+2 ,Q2, J2) an elaboration of it if a = a1, Q1,Q2 ⊂ Q, J + 1 = J + ∪ {a2}, J + 2 = J + and J - 1 , J - 2 ⊆ J -. We call an r-justification elaborated if there is no elaboration for it, and an r-justification chain elaborated if all its elements are elaborated.

Example 11. Reconsider program P5 from Example 10. Then J in the example can be elaborated through the first element yielding (a+, {r10}, ⟨{b}, ∅⟩), (b+, {r11}, ⟨∅, {c}⟩), (c-, ∅, ⟨∅, ∅⟩) as a (concise) chain.

Example 12. We have the program P6 = {r13 : a ∨ b ← ⊤, r14 : c ← a, r15 : c ← b, r16 : ⟨{a, b}, {{a, b}}⟩ ← c}.

Now, an r-justification for a is (a+, P6, ⟨∅, ∅⟩) which is not elaborated. It might be tempting to try to elaborate it using b, but (a+, {r15, r16}, ⟨{b}, ∅⟩), (b+, P6, ⟨∅, ∅⟩) is not a valid elaboration since P6 ̸⊂ P6 and b can only be derived using the whole program. However, (a+, {r15, r16}, ⟨{c}, ∅⟩), (c+, {r13, r14, r15}, ⟨∅, ∅⟩) is in fact an elaboration for a. This can be motivated by highlighting that while both b and c can be used to derive a, the latter atom requires less rules to do so.

It is of course interesting to consider how m-justification from the previous section and r-justification relate. For a subclass of programs, namely normal and convex programs, we have the following result showing a strong correspondence.

Theorem 5. Let P be a normal, convex program and I ∈ AS(P). For each elaborated, concise r-justification (a+, Q, J), it holds that Q = {r} is a singleton set and J is a globally concise m-justification for I |= B(r) w.r.t. P and I.

The reason for this result is that for such programs we can define an immediate consequence operator for definite programs. Now, the restriction to normal programs is necessary because otherwise the reduct defined in Section 2 would not yield a definite program. In contrast convexity is required to ensure that the fixpoint of the consequence operator is indeed an answer-set. The next examples also show that we do not have such elaborate r-justifications in general.

Example 13. Suppose we have the program Q = {r17 : p ← q, r18 : q ← p} which we use to define P7 = Q ∪ {r19 : p∨q ←⊤} and P8 = Q∪{r20 : p ← ⟨{p, q}, {∅, {p, q}}⟩}. The former is clearly convex but disjunctive, whereas the latter is normal but not convex. Now, {p, q} is the sole answerset for both programs but the elaborated r-justification for p w.r.t. P7 is (p+, {r17, r19}, ⟨∅, ∅⟩}) and the one w.r.t. P8 is (p+, {r17, r20}, ⟨∅, {q}⟩}). In both cases it is not possible to use a single rule to derive p.

In the final part of this section, we will show how mjustification and r-justification can be jointly used.

Example 14. Consider the program

where {b; c} represents a choice between some subset of b and c. Given the answer-set {a, b, d}, a possible r-justification chain for a is (a+, {r21}, ⟨{b, d}, {c}⟩}), (d+, {r22}, ⟨{b}, ∅⟩}), (b+, {r23}, ⟨∅, {c}⟩}), (c-, ∅, ⟨∅, ∅⟩). Looking at the first element of the chain, we see that rule r21 derives a based on ⟨{b, d}, {c}⟩. If we now look at the m-justifications for the body atoms of r21, i.e., #sum{1 : b, 2 : d} > 2 and #sum{3 : d, 2 : c} < 5, we obtain ⟨{b, d}, ∅⟩ and ⟨∅, {c}⟩. In other words, the truth of b and d satisfies the first aggregate, whereas the second aggregate is true because c is false in the answer-set.

The interplay between m-justifications and r-justifications is can especially be beneficial in an interactive setting as the next example shows.

Example 15. Assume we have the following in the common ASP-Core-2 syntax [Calimeri et al., 2020]:

Intuitively, the program contains facts about an employee and their sales for the last three months. Rule r24 states that employee 1 is a top earner if she sold more than 10 units in at least one month and the total units she sold is at least 20. The single answer-set of P10 contains the atom top(1) indicating that employee 1 is a top earner. Suppose now the user has access to an interactive explanation system and asks why employee 1 is a top earner. The system can start the explanation process by giving an r-justification for top(1), for instance (top(1), {r24, r25, r26, r27}, ⟨∅, ∅⟩). Elaboration of this r-justification would not really yield additional insight, but the user can instead opt to view an mjustification for the body of r24. The unique m-justification is ⟨{emp(1), sold(1, 1, 12), sold(1, 2, 8)}, ∅⟩ indicating that employee 1 was designated as a top earner because she sold 12 units in the first month and 8 in the second. The process can even be further fine-grained - if the user wishes - by giving the m-justifications of the individual body literals. For example, the first aggregate has the m-justification ⟨{sold(1, 1, 12)}, ∅⟩, which tells the user that the sales in the first month were necessary to satisfy this part of the body of the rule.

6 Complexity

We now consider complexity and assume basic familiarity with complexity theory, cf. [Papadimitriou, 1994].

6.1 Computational Basis

Before we present our study of the complexity of the problems emerging from what we have discussed so far, we first have to give some assumptions on the underlying representation and evaluation of c-atoms. We do not commit to a specific formalism, but rather request that any representation R(A) = (D, R(C)) of a c-atom A satisfies the following property.

Definition 12. Let A = ⟨D, C⟩ be a c-atom and J be a partial interpretation. Then AJ = ⟨D, CJ) where CJ = {S ∈ C | S ⊇ J +, S ∩ J - = ∅}⟩ is the fixing of J in A; it is total, if J is total on D.

Assertion 1. Given a c-atom A = ⟨D, C⟩ (i.e., R(A)) and a total fixing I of A, deciding whether CI ̸= ∅ is in P.

In other words, checking whether a set S is a satisfier (seen as a total fixing) of a c-atom A can be done in polynomial time. For example, using for the representation R(A) of A simply C as an explicit collection, a Boolean formula, some (perhaps restricted) CNF/DNF, a BDD etc. would fulfill this elementary property. We then easily obtain

Lemma 1. Given a set L of c-literals and a partial interpretation J, deciding J |= L is coNP-complete resp. J ̸|= L is NP-complete. Both tests are in P, if J is a total fixing of each c-literal in L (in particular, if J is a total interpretation).

Both deciding I |= L and I |= L are in P, if R(·) fulfills stronger properties; e.g., if deciding C ̸= ∅ (satisfiability) from R(A) is in P and R(·) is polynomially closed under fixing, i.e., some representation R(AI) in the formalism is computable in polynomial time from R(A) and I. E.g., DNFs, Horn CNFs, and many other representations have this property.

Furthermore, if R(·) is polynomially closed under conjunctions, i.e., from R(Li) of c-literals Li (remember that negative c-literals can be replaced by complemented c-atoms), i = 1, . . . , n, some R(A) in the formalism is computable in polynomial time for A = AL as in Theorem 1, we can merge all c-literals into a single c-atom without an exponential blowup. This extends to merging of c-literals if R(·) is also polynomially closed under negation, i.e., R(A) is computable in polynomial time from R(A). Clearly, Boolean formulas have these properties.

6.2 Complexity Results

We now come to our complexity results for m-justification as introduced in Section 4. We start with the problem dealing with the recognition of m-justifications.

Theorem 6. Given a c-literal L, a total interpretation I, and a partial interpretation J ≤ I, deciding whether J is an m-justification is DP-complete.

The class DP informally contains the problems amounting to the "conjunction" of a problem in NP and a problem in coNP; the canonical DP-complete problem is SAT-UNSAT, i.e., to decide, given Boolean formulas F, G whether F is satisfiable and G is unsatisfiable. In Theorem 6, the coNP-check is required by condition (i) of Definition 2 as partial model checking is coNP-complete. The NP-check stems from condition (ii) which requires minimality of the partial interpretation.

Now, by the computational assumptions in the previous subsection (yielding Lemma 1), we can readily obtain:

Corollary 1. Given a set L of c-literals, a total interpretation I, and a partial interpretation J ≤ I, deciding whether J is a globally concise m-justification for L is DP-complete.

However, under local conciseness, the complexity of recognizing positive and negative m-justifications diverges.

Theorem 7. Given a set L of c-literals, a total interpretation I of L, and a partial interpretation J ≤ I, deciding whether J is a locally concise m-justification for L is (a) ΣP2 -complete if I |= L and (b) ΘP2 -complete otherwise.

The case (a) can be solved by guessing a sequence of potential m-justifications whose union is J and then checking whether each candidate is in fact an m-justification for the corresponding c-literal in L. As this check is in DP, we obtain that the problem is in P NP = ΣP2 . In case (b), deciding negative m-justification amounts to checking whether the given partial interpretation J is a model of the complement of some c-literal in L. This can be done with parallel DP-checks thus NP checks, which puts the problem into P NP || = ΘP2 ;matching hardness is by a reduction from evaluating a disjunction of DP instances. This means lower complexity than ΣP2 but higher than DP (under common complexity hypotheses).

If we restrict ourselves to convex c-literals, most of the problems we have discussed so far become tractable.

Theorem 8. Given a set L of convex c-literals, a total interpretation I of L and a partial interpretation J ≤ I, deciding whether (a) J is a locally concise m-justification for L is NPcomplete if I |= L and (b) J is a globally, respectively locally, concise m-justification is in P otherwise.

This result is due to Theorem 1, which allows us to merge a set of convex c-literals semantically into a single convex c-atom. Recognising locally concise positive m-justifications is still intractable, as the guess as in Theorem 8.(a) is needed. In fact, the NP-hardness holds even for monotone c-literals.

Now we turn to the complexity of computing justifications.

Theorem 9. Given a set L of c-literals and a total interpretation I, computing an m-justification for L is in FP NP and FP NP || -hard even if L is a singleton set.

Indeed, with an NP oracle, we can just minimize I atom by atom. This result is not very surprising, as m-justifications resemble prime implicants sharing this complexity (cf. Sec. 7).

Our final complexity results for m-justifications concern definite m-justifications.

Theorem 10. Given a c-literal L and a total interpretation I, deciding whether a definite m-justification for L exists is coNP-complete, and computing the latter FP NP [1]-complete.

Note that FP NP [1] is the class of function problems computable in polynomial time having access to exactly one NPoracle call. Here, coNP membership holds as we only need to check for each atom in, respectively not in, the interpretation, whether it is required for the truth of L. This can be done in polynomial time and yields a partial interpretation J. If J is an m-justification, which can be verified in coNP, then it is also definite. Otherwise, there is no definite m-justification.

We now turn to r-justifications as introduced in Section 5.

Theorem 11. Given a program P and an answer-set I ∈ AS(P). Then deciding whether a triple (a◦ ,Q, J) is an rjustification w.r.t. P and I is (a) DP-complete if ◦ = +, and (b) coNP-complete if ◦ = -. Deciding whether the triple is a concise r-justification is DP-complete.

Essentially, the complexity in (a) stems from checking presumptuous entailment, which is coNP-complete, and minimality of the rules, which requires an NP-complete check. In case (b), the complexity is slightly lower. The underlying reason is that we simply have to check whether the set Q contains exactly the failed support w.r.t. P and I. This amounts to checking for each rule in Q whether it is a failed support. As all checks are in coNP, so is their conjunction. Conciseness requires an additional NP-check.

Finally, we consider problems for r-justification chains.

Theorem 12. Given a program P , an answer-set I ∈ AS(P) and an r-justification chain J , deciding whether J is elaborated is NP-complete.

Informally, we can check for an atom b in coNP whether it can be used for some elaboration. By combining the checks for all b into a single coNP-check, deciding whether some elaboration exists is in coNP, and thus the negation is in NP.

Theorem 13. Given a program P , I ∈ AS(P), and an atom a, computing an elaborated r-justification chain for a is in FP NP and FP NP || -hard even if P is normal and convex. If P is normal and all c-atoms are elementary, the problem is in P.

Informally, we can set up an r-justification chain with positive and negative justifications of the form (b+, Qb, ⟨∅, I -⟩) and (b-,Qb, ⟨I + b , I -⟩), resp., and repeatedly replace nonelaborated r-justifications with some elaboration. The number of repetitions is polynomial, hence this is feasible in FP NP . The FP NP || -hardness is by a reduction from computing some m-justification (cf. Theorem 9).

The complexity results given in this section are of course for the worst case. Since we already have an answer-set, related work [Wang et al., 2022] suggests that finding r-justification chains should be practically feasible. However, such investigations are subject to future work.

7 RelatedWork

Our m-justifications naturally link to prime implicants, cf. [Umans et al., 2006], which are smallest formulas (in the context of propositional logic, a non-redundant conjunction of literals) that imply a given formula. and they were used to offer explanations for machine learning classifiers [Shih et al., 2018; Ignatiev et al., 2019]. Our m-justifications J of c-atoms A = ⟨D, C⟩ amount to prime implicants of a Boolean formula F(A) associated with A, while negative and locally concise m-justifications of (sets of) c-literals have no immediate counterpart. Nonetheless, the link may be fruitfully exploited for efficient computation of m-justifications [Jackson, 1992].

While there are many works on explainability in ASP [Fandinno and Schulz, 2019], few address programs with c-atoms. Notable ones are stepping [Oetsch et al., 2018], which is a debugging approach, and computations [Liu et al., 2010], which is a definition of answer-set semantics through constructive computation. However, the goals of these works differ from ours. Namely, stepping aims for debugging at discrepancies between the actual and an expected answer-set, considering counterfactual situations; Liu et al.'s computations aim to generalise answer-set semantics to programs with c-atoms. Both works essentially pursue a bottom-up construction of answer-sets, while our r-justification chains proceed top-down and are thus more goal oriented and leaner. Furthermore, Liu et al.'s computations give no justifications for atoms not in an answer-set, do not support disjunction, and they have slightly different semantics. E.g., program P8 in Example 13 (which is not convex) would have the unique answer-set ∅, which differs from ASP solvers like DLV [Leone et al., 2006] and clingo [Gebser et al., 2014] that also yield {p, q} as the only answer-set.

The notions for programs most similar to our r-justification chains are β-witnesses [Wang et al., 2022] and offline justification graphs [Pontelli et al., 2009], which recently were extended to programs with choice rules and constraints [Trieu et al., 2021], respectively with variables [Trieu et al., 2022]. The main difference between our approach and theirs on choice is that offline justification graphs can designate an atom to be true by the choice rule and the other atoms in the choice do not appear in the justification at all. In an r-justification, those atoms always appear as negative prerequisites. This has the benefit that in an r-justification chain, such atoms can also be constructively falsified. Furthermore, justification graphs currently neither handle disjunction nor aggregates. In contrast to justification graphs and r-justification chains, β-witnesses only encompass positive information about what is in an answer-set. The main similarity between our r-justification chains and βwitnesses is that they also use sets of rules to iteratively justify atoms, but bottom-up. Offline justification graphs do incorporate information about the atoms absent from an answer-set. Intuitively, they aim at a constructive proof of an atom using the well-founded model of the program. Atoms not contained in that model can be assumed to be false, and thus cycles in the graph prevented. This is in stark contrast to our r-justification chains, which do not require such constructive proofs for false atoms, but confine to blocked support. Furthermore, while well-founded semantics for disjunctive programs is available, cf. [Wang et al., 2012], generalising justification graphs from normal propositional to disjunctive programs with c-atoms is non-trivial.

Another related notion is the formal theory of justification [Denecker et al., 2015; Marynissen et al., 2022], which aims to characterise different semantics of logic programs in terms of "justifications". Intuitively, different semantics can be formalised by which justifications are accepted. In contrast to our work, the justifications of the formal theory are potentially infinite and describe dependencies between atoms containing no direct information about rules. Furthermore, disjunction and c-atoms in the rule heads are not supported.

8 Conclusion &FutureWork

We introduced and studied complementary notions of justification for ASP programs built over Abstract Constraint atoms, which encompass various ASP language extensions, among them aggregates and choice rules. Our m-justifications use a semantic approach based on minimal partial models, while rjustification chains are a more syntactically minded, rule-based notion. We have provided several examples and showed how the notions can be jointly used. Besides some basic properties of justifications, we provided complexity results for emerging computational tasks. While they are often intractable in general, we identified relevant tractable cases.

Our ongoing and future work aims to extend this theoretical study of justification, and to utilise it in a fully-fledged and interactive explanatory system. Specifically, a user may opt in a session for the model- or the rule-based approach at the current stage to obtain more insight, control which rules get expanded, and drive possible elaboration of justifications. Investigating how our justifications can be used or extended to offer contrastive justifications, which inform about changes to flip the membership of atoms in an answer-set, is another worthwhile endeavour.

Acknowledgments

Tobias Geibinger is a recipient of a DOC Fellowship of the Austrian Academy of Sciences at the Institute of Logic and Computation at the TU Wien. Furthermore, this work has benefited from Humane AI Net ICT-48-2020-RIA / 952026.