We present an enhancement of exp(ASP), a system that generates explanation graphs for a literal ℓan atom or its default negation ∼ -given an answer set of a normal logic program , which explain why ℓ is true (or false) given and . The new system, exp(ASP), difers from exp(ASP) in that it supports choice rules and utilizes constraint rules to provide explanation graphs that include information about choices and constraints.
Answer Set Programming (ASP) [1, 2] is a popular paradigm for decision making and problem solving in Knowledge Representation and Reasoning. It has been successfully applied in a variety of applications such as robotics, planning, diagnosis, etc. ASP is an attractive programming paradigm as it is a declarative language, where programmers focus on the representation of a specific problem as a set of rules in a logical format, and then leave computational solutions of that problem to an answer set solver. However, this mechanism typically gives little insight into why something Figure 1: Explanation of (1, ) is a solution and why some proposed set of literals is not a solution. This type of reasoning falls within the scope of explainable Artificial Intelligence and is useful to enhance the understanding of the resulting solutions as well as for debugging programs. There have been a number of approaches proposed [3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13], but to the best of our knowledge, no system deals directly with ASP programs with choice atoms.
In this paper, we present an improvement over our previous system, exp(ASP) [14], called exp(ASP). Given an ASP program , an answer set , and an atom , exp(ASP) is aimed at answering the question “why is true/false in ?” by producing explanation graphs for atom . The current system, exp(ASP), does not consider programs with choice atoms and other constructs that extend the modeling capabilities of ASP. For instance, Fig. 1 shows an explanation graph for the atom (1, ) given the typical encoding of the graph coloring problem that does not use choice rules. This explanation graph does provide the reason for the color assigned to node 1 by indicating that the node is red because it is not blue and not green. It is not obvious that this information represents the requirement that each node is colored with exactly one color. The improvement described here extends our approach with the ability to handle ASP programs containing choice rules and include constraint information in the explanation graphs.
The rest of the paper is organised as follows. Section 2 briefly introduces our previous system, exp(ASP). Section 3 describes the components of an explanation graph. Section 4 describes how our enhanced system, exp(ASP), computes explanation graphs for an atom , with an illustrative example. Finally, Section 5 concludes our paper. 2. Background: The exp(ASP) System exp(ASP) deals with normal logic programs which are collection of rules of the form ℎ() ← () where ℎ() is an atom and () = +, − with + and − are collections of atoms in a propositional language and − denotes the set { | ∈ − } and not is the default negation.
exp(ASP) generates explanation graphs under the answer set semantics [15]. It implemented the algorithms proposed in [12] to generate explanation graphs of a literal ℓ ( or ∼ for some atom in the Herbrand base of ), given an answer set of a program . Specifically, the system produces labeled directed graphs, called explanation graphs, for ℓ, whose nodes belong to ∪ {∼ | ∈ } ∪ {⊤, ⊥, assume} and whose links are labeled with +, − or ∘ (in Fig. 1, solid/dash/dot edges represent +/− /∘ edges). Intuitively, for each node , ̸∈ {⊤, ⊥, assume} in an explanation graph (, ), the set of neighbors of represents a support for being true given (see below).
The main components of exp(ASP) are: 1. Preprocessing: This component produces an aspif representation [16] of that will be used in the reconstruction of ground rules of . It also computes supported sets for atoms (or its negations) in the Herbrand base of and stored in an associative array . 2. Computing minimal assumption set: This calculates a minimal assumption set given the answer set and according to the definition in [12]. 3. Computing explanation graphs: This component uses the supported sets in and constructs e-graphs for atoms in (or their negations) under the assumption that each element ∈ is assumed to be false.
We note that exp(ASP) does not deal with choice atoms [17]. The goal of this paper is to extend exp(ASP) to deal with choice atoms and utilize constraint information.
exp(ASP) employs the notion of a supported set of a literal in a program in its construction. Given a program , an answer set of , and an atom , if ∈ and is a rule such that (i) ℎ() = , (ii) + ⊆ , and (iii) − ∩ = ∅, (, ) = + ∪ {∼ | ∈ − }; and refer to this set as a supported set of for rule . If ∈/ , for every rule such that ℎ() = , then (∼ , ) ∈ {{} | ∈ ∩ − } ∪ {{∼ } | ∈ + ∖ }.
To account for choice atoms1 in , the notion of supported set needs to be extended. For simplicity of the presentation, we assume that any choice atom is of the form {1 : 1, . . . , : } where2 ’s and ’s are atoms. Let and denote and , respectively. Furthermore, we write ∈ to refer to an element in {1, . . . , }. For ∈ , ∼= indicates that : belongs to {1 : 1, . . . , : }.
In the presence of choice atoms, an atom can be true because belongs to a choice atom that is a head of a rule and () is true in . In that case, we say that is chosen to be true and extend (, ) with a special atom +ℎ to indicate that is chosen to be true. Likewise, can be false even if it belongs to a choice atom that is a head of a rule and () is true in . In that case, we say that is chosen to be false and extend (∼ , ) with a special atom − ℎ to indicate that is chosen to be false. Also, ∼= will belong to the support set of (, ) and (∼ , ).
The above extension only considers the case belongs to the head of a rule. (, ) also needs to be extended with atoms corresponding to choice atoms in the body of . Assume that is a choice atom in +. By definition, if () is true in then ≤ | | ≤ where = {(, ) | ∈ , ∼= , |= ∧ }. For this reason, we extend (, ) with . Because is not a standard atom, we indicate the support of given by defining (, ) = {}. Furthermore, for each ∈ , (, ) = {* }. When = ∅, we write (, ) = {* }. Similar elements will be added to (, ) or (∼ , ) in other cases (e.g., the choice atom belongs to − ) or has diferent form (e.g., when = 0 or = ∞). We omit the precise definitions of the elements that need to be added to (, ) for brevity.
The introduction of diferent elements in supported sets of literals in a program necessitates the extension of the notion of explanation graph. Due to the space limitation, we introduce its key components and provide the intuition behind each component. The precise definition of an explanation graph is rather involved and is included in the appendix for review. First, we introduce additional types of nodes. Besides +choice, − choice, * True, and * Empty, we consider the following types of nodes: ∙ Tuples are of the form (1, . . . , , 1, . . . , ) to represent elements belonging to choice atoms (e.g., ((1, ), ()) representing an element in 1{((, ) : ()}1). denotes all tuple nodes in program . ∙ Choices are of the form ≤ ≤ or ∼ ( ≤ ≤ ) where ⊆ . Intuitively, when ≤ ≤ (resp. ∼ ( ≤ ≤ )) occurs in an explanation graph, it indicates that ≤ ≤ is satisfied (resp. not satisfied) in the given answer set . denotes all choices. ∙ Constraints are of the form _() or _ (∼ ). The former (resp. latter) indicates that is (resp. is not) true in and satisfies all 1We use choice atoms synonymous with weight constraints. 2As we employ the aspif representation, this is a reasonable assumption. the constraints such that ∈ + (resp. ∈ − ). The set of all constraints is denoted with .
Having defined the nodes of the graph, we next introduce the new types of links in explanation graphs as follows: − ∙ is used to connect literals and ∼ to +choice and − choice, respectively, where ∈ and is a choice atom in the head of a rule. − ◇ is used to connect literals and ∼ to _() and _(∼ ), respectively. − ⊕ is used to connect a tuple ∈ to * True. − ⊘ is used to connect a choice ∈ to * Empty.
We present here an updated definition of explanation graph by adding the necessary nodes and links, which is defined as follows: Definition 1. [Explanation Graph] Let us consider a program , an answer set , a set of assumptions with respect to , Herbrand base and a set of choice head atoms = { | ∈ , ℎ ℎ , ∈ }. Let = {(1, . . . , , 1, . . . , ) | , ∈ }, = { ≤ { 1, . . . , } ≤ | ∈ , ∈ N, ∈ N ∪ ∅}, = {_() | ∈ } ∪ {_(∼ ) | ̸∈ }, = { | ∈ } ∪ {∼ | ̸∈ }, = ∪ ∪ {∼ () | ∈ } ∪ ∪ ∪ {⊤, ⊥, assume, +choice, − choice, * True, * Empty} where ⊤ and ⊥ represent true and false, respectively. An explanation graph of an atom occurring in is a finite labeled and directed graph = (, ) with ⊆ and ⊆ × × { +, − , ∘ , ∙ , ◇ , ⊕ , ⊘} , where (, , ) ∈ represents a link from to with the label , and satisfies the first five conditions in Definition 2.1 [14] and the following additional conditions: • if (, +ℎ, ∙ ) ∈ then ∈ ∩ ; • if (∼ , − ℎ, ∙ ) ∈ then ∈/ and ∈ ; • if (, , ◇ ) ∈ then ∈ and is of the form _(); • if (, * , ⊕ ) ∈ then ∈ ; • if (, * , ⊘ ) ∈ then ∈ ∪ {∼ () | ∈ }; • if (, , +) ∈ such that ∈ and ∈ then ∈ {1, . . . , }; • if (, , − ) ∈ such that ∈ {∼ () | ∈ } and ∈ then ∈ {1, . . . , }; • if (_(), , +) ∈ and (_(), ∼ , − ) ∈ then for all triggered constraints containing ∈ + in satisfied by . • if (_(∼ ), , +) ∈ and (_(∼ ), ∼ , − ) ∈ then for all triggered constraints containing ∈ − in satisfied by . • there exists no , such that (⊤, , ) ∈ , (⊥, , ) ∈ , (assume, , ) ∈ (+choice, , ) ∈ , (− choice, , ) ∈ , (* True, , ) or (* Empty, , ) ∈ . • for every ∈ ∩ and is not a fact in , or ∈ = {∼ | ∈/ ∧ ∈ } – there exists no ∈ ∩ such that (, , − ) or (, , ∘ ) belong to ; – there exists no ∼ ∈ ∩ {∼ | ̸∈ } such that (, ∼ , +) or (, ∼ , ∘ ) belong to ; – If we have ∗ + = { | (, , +) ∈ , ∈ } then + ⊆ , ∗ − = { | (, ∼ , − ) ∈ , ∈ } then − ∩ = ∅, ∗ 1 = (, , +) ∈ where = ≤ { 1, . . . , } ≤ ∈ and a set of atoms 1 ⊆ { 1, . . . , } such that ∀ = (1 , . . . , , 1 , . . . , ) ∈ 1, |= 1 ∧ . . . ∧ ∧ 1 ∧ . . . ∧ and ≤ | 1| ≤ , ∗ 2 = (, ∼ (), − ) ∈ where = ≤ { 1, . . . , } ≤ ∈ and a set of atoms 2 ⊆ { 1, . . . , } such that ∀ = (1 , . . . , , 1 , . . . , ) ∈ 2, |= 1 ∧ . . . ∧ ∧ 1 ∧ . . . ∧ and |2| < or |2| > , ∗ 3 = (, , +) ∈ where = ≤ { 1, . . . , } ∈ and a set of atoms 3 ⊆ { 1, . . . , } such that ∀ = (1 , . . . , , 1 , . . . , ) ∈ 3, |= 1 ∧ . . . ∧ ∧ 1 ∧ . . . ∧ and |3| ≥ , ∗ 4 = (, ∼ (), − ) ∈ where = ≤ { 1, . . . , } ∈ and a set of atoms 4 ⊆ { 1, . . . , } such that ∀ = (1 , . . . , , 1 , . . . , ) ∈ 4, |= 1 ∧ . . . ∧ ∧ 1 ∧ . . . ∧ and |4| < , ∗ there is a rule ∈ whose head is or ∈ where = {1 : 1, . . . , : } such that + = + ∖ {ℎ }, − = − ∖ {ℎ }, and whose body contains choice atoms · 1 = {1 : 1, . . . , : } ∈ + if we have 1; · 2 = {1 : 1, . . . , : } ∈ − if we have 2; · 3 = {1 : 1, . . . , : } ∈ + or ′3 = {1 : 1, . . . , : } − 1 ∈
− if we have 3. Note that in ′3, the upper bound ′3 = − 1; · 4 = {1 : 1, . . . , : } ∈ − or ′4 = {1 : 1, . . . , : } − 1 ∈ + if we have 4. Note that in ′4, the upper bound ′4 = − 1.
– contains no cycle containing . • for every ∼ ∈ ∩ {∼ | ̸∈ } and ̸∈ , – there exists no ∈ ∩ such that (∼ , , +) or (∼ , , ∘ ) belong to ; – there exists no ∼ ∈ ∩ {∼ | ̸∈ } such that (∼ , ∼ , − ) or (∼ , ∼ , ∘ ) belong to ; – if we have ∗ + = { | (∼ , , − ) ∈ , ∈ } then + ⊆ ∗ − = { | (∼ , ∼ , +) ∈ , ∈ } then − ∩ = ∅ ∗ 1 = (∼ , ∼ (), − ) ∈ where = ≤ { 1, . . . , } ≤ ∈ and a set of atoms 1 ⊆ { 1, . . . , } such that ∀ = (1 , . . . , , 1 , . . . , ) ∈ 1, |= 1 ∧ . . . ∧ ∧ 1 ∧ . . . ∧ and |1| < or |1| > , ∗ 2 = (∼ , , +) ∈ where = ≤ { 1, . . . , } ≤ ∈ and a set of atoms 2 ⊆ { 1, . . . , } such that ∀ = (1 , . . . , , 1 , . . . , ) ∈ 1, |= 1 ∧ . . . ∧ ∧ 1 ∧ . . . ∧ and ≤ | 2| ≤ , ∗ 3 = (∼ , ∼ (), +) ∈ where = ≤ { 1, . . . , } ∈ and a set of atoms 3 ⊆ { 1, . . . , } such that ∀ = (1 , . . . , , 1 , . . . , ) ∈ 3, |= 1 ∧ . . . ∧ ∧ 1 ∧ . . . ∧ and || < ∗ 4 = (∼ , , − ) ∈ where = ≤ { 1, . . . , } ∈ and a set of atoms 4 ⊆ { 1, . . . , } such that ∀ = (1 , . . . , , 1 , . . . , ) ∈ 4, |= 1 ∧ . . . ∧ ∧ 1 ∧ . . . ∧ and |4| ≥ , and ∗ for every rule ∈ whose head is we have that + ∩ − ̸= ∅ or − ∩ + ̸= ∅ or () contains choice atoms · 1 = {1 : 1, . . . , : } ∈ + if we have 1; · 2 = {1 : 1, . . . , : } ∈ − if we have 2; · 3 = {1 : 1, . . . , : } ∈ + or ′3 = {1 : 1, . . . , : } − 1 ∈
− if we have 3. Note that in ′3, the upper bound ′3 = − 1; · 4 = {1 : 1, . . . , : } ∈ − or ′4 = {1 : 1, . . . , : } − 1 ∈ + if we have 4. Note that in ′4, the upper bound ′4 = − 1.
– any cycle containing ∼ in contains only nodes in ∩ {∼ | ̸∈ }. 4. The exp(ASP)ystem In this section, we will focus on describing how the three main tasks in Sec. 2 are implemented. exp(ASP) uses a data structure, associative array, whose keys can be choices, tuples, constraints, or literals. For an associative array , we use .() to denote the set of keys in and ↦→ [] to denote that is associated to []. To illustrate the diferent concepts, we will use the program 1 that contains a choice atom and a constraint rule as follows: (1) a (3) c (5) 1 {m(X) : n(X)} 1 :− :− :− 4.1. Preprocessing b, c. a. c.
(2) b (4) (6) n(1..2).
:−
:−
c, a.
b, m(
Similar to exp(ASP), a program is preprocessed to maintain facts and as many ground rules as possible by using the –text and –keep-facts options and replacing facts with the external statements. The aspif representation [16] of the program is then obtained and processed, together with the given answer set, for generating explanation graphs. The aspif statements of 1 is given in Listing 1. Let us briefly discuss the aspif representation before continuing with the description of other components.
Listing 1: aspif Representation of 1
1 asp 1 0 0
2 5 1 2
3 5 2 2
4 1 0 1 3 0 1 -4
5 1 0 1 4 0 2 -5 -3
6 1 0 1 5 0 2 4 3
7 1 0 1 6 0 1 3
8 1 0 0 0 2 7 5
9 1 1 1 7 0 2 6 1
10 1 1 1 8 0 2 6 2
11 1 0 1 9 0 2 1 7
12 1 0 1 10 0 2 2 8
13 1 0 1 11 1 1 2 9 1 10 1
14 1 0 1 12 1 2 2 9 1 10 1
15 1 0 1 13 0 2 11 -12
16 1 0 0 0 2 6 -13
17 4 4 n(
Each line encodes a statement in aspif. Lines starting with 4, 5, and 1 are output, external,
and rule statements, respectively. Atoms are associated with integers and encoded in output
statements (e.g., Line 17: 1 is the identifier of (
Given the aspif representation ′ of a program , an associative array is created where = {(, ℎ) ↦→ | ∈ {0, 1}, ℎ ∈ , = {() | ∈ ′, ℎ() = ℎ}}. Here, for an element (, ℎ) ↦→ in , is the type of head ℎ, either disjunction ( = 0) or choice ( = 1). Furthermore, for an answer set of , ( ) = { ↦→ | ∈ { | ∈ } ∪ {∼ | ∈/ }, = {(, ) | ∈ }} [14].
Algorithm 1 shows how constraints are processed given the program and its answer set . The outcome of this algorithm is an associative array . First, —the set of constraints (the bodies of constraints)—is computed. Afterwards, for each body of a constraint in , and are computed. Each element in requires some trigger constraint to falsify the body , which are those in . Each ℎ_ encodes a support for a choice Algorithm 1: _(, )
Input: - associative array of rules (this is ), - an answer set 1 = { | [(0, ℎ)] = ∧ ℎ = ∅} 2 ← {∅ ↦→ ∅} // Initialize an empty associative array : .() = ∅ 3 for ∈ do 4 ← { | ∈ + ∧ ∈ } ∪ {∼ | ∈ − ∧ ∈/ } 5 ← {∼ | ∈ + ∧ ∈/ } ∪ { | ∈ − ∧ ∈ } 6 if choice atom in and = {(, ) | ∈ , ∼= , |= ∧ } then 7 = {(, ) | ∈ , ∼= } 8 if = {1 : 1, . . . , : } ∈ + and || < or || > then 9 ℎ_ ← { “ ∼ ( <= <= )”} 10 11 12 13 14 15 if = {1 : 1, . . . , : } ∈ − and ≤ | | ≤ then
ℎ_ ← { “ <= <= ”} if = {1 : 1, . . . , : } ∈ + or = {1 : 1, . . . , : } − 1 ∈ − and || < then
ℎ_ ← { “ ∼ ( <= )”} if = {1 : 1, . . . , : } ∈ − or = {1 : 1, . . . , : } − 1 ∈ + and || ≥ then
ℎ_ ← { “ <= ”} ← ∪ ℎ_ if ̸= ∅ then [ℎ_] ← [] [] ← [{“ * ”}] ℎ ℎ ∈ else
[ℎ_] ← [{“ * ”}] for ∈ do
Append {_()} to a list [] [_()] ← [ ∪ {} | ∈ , ∈
[_()]] 25 return atom. _(), where ∈ , is assigned to support the explanation of (Line 23), and is used for the explanation of _() to justify the satisfaction of constraints containing (Line 24). For {1 : 1, . . . , : } in a choice atom , we write = {(, ) | ∈ , ∼= } (e.g., Line 7).
During the preprocessing, the set of all negation atoms in , ( ) = { | ∈
− ∧ ∈ } [12, 14], is computed. For 1 and the answer set = {(
Example 1. For program 1 and its answer set = {(
(1) shows that atom in 4 makes the constraint satisfied while (
The pseudocode of computing minimal assumption sets is shown in Algorithm 2. A tentative assumption set [12, 14] is computed (Line 1), which is a superset of minimal assumption sets. The atoms in are false in and do not belong to the set of cautious consequences, denoted by ( ), of the program . The minimal assumption set is computed in Line 6, which is the union of outputs from functions and . Note that several minimal assumption sets w.r.t an answer set of may exist.
Function , ( ) in Sec. 4.1 is utilized to compute all derivation paths of ∈ (Line 12). Then, the derivation paths in are examined to see whether the cycle condition in the definition of the explanation graph is satisfied (Lines 13-16). During this process, other tentative assumption atoms, that are derived from , are stored in a set , which is appended to [] ( is an associative array). If is derivable from other atoms in , then the relation of will be checked in function and is stored in a set ′. A set = ∖ ′ contains atoms that must be assumed to be false (Lines 17-19).
We calculate sets of minimal atoms that break all cycles among tentative assumption atoms via . This is done by the function .
Example 2. Let us reconsider the program 1 and Example 1.
• For the program 1, we have: = {, } • From (1) in Example 1, atom is not derivable from other atoms in while atom is derivable from an atom in {}. Thus, we have ′ = {}, = {} and = : [{}]. Also, there is no cycle between and , so () = ∅. As a result, the minimal assumption set is = {}. Algorithm 2: _ (( ), ( ), )
Input: ( ) - A cautious consequence of a program , ( ) - A set of negative atoms in , - A associative array computed in Sec. 4.1 1 = { | ∈ ( ) ∧ ∈/ ∧ ∈/ ( )} 2 ← {∅ ↦→ ∅} 3 (, ) = ( , ) 4 = () 5 for ∈ do 6 ← ∪ 7 ← ∪ { } 8 return 9 10 function ( , ) 11 for ∈ do 12 Find all derivation paths of from 13 for ∈ do 14 Find = { | ∈ ∧ ̸= } such that is derived from 15 if there is no negative cycles in derivation path then 16 Append to a list [] 28 () ← { | ∀ ∈ , ̸= =⇒ ⃒⃒ ⃒⃒ ≤ ⃒⃒ ⃒⃒ } 29 return ()
In this section, we describe how the explanation graph is generated by utilizing , from Sec. 4.1 and the minimal assumption set from Sec. 4.2. In order to leverage the algorithm from the previous work, and are combined into a dictionary as follows: = { ↦→ | ∈ .() ∪ .(), = [ ∪ ] ℎ ℎ ∈ [] ∈ []}. Note that = ∅ if ∄ ∈ .() and = ∅ if ∄ ∈ .(). Given , the algorithm from [14] will find the explanation graph of literal in , taking into consideration the additional types of nodes and links.
Example 3. For program 1, the explanation graph of (
As can be seen from Fig. 2, a justification for (
We illustrate the application of our updated system, exp(ASP), to the graph coloring problem. We use a solution of the problem where each node is assigned a unique color by the choice rule: 1{(, ) : ()}1 ← ().
Fig. 3 shows the explanation graph of (1, ). Unlike Fig. 1, Fig. 3 shows that a
choice head (1, ) is chosen to be true while two choice heads, (3, ) and
(2, ), are chosen to be false, which are represented via orange dotted links (link
∙ ). Fig. 3 displays the constraint that (
In this paper, we proposed an extension of our explanation generation system for ASP programs, exp(ASP), which supports choice rules and includes constraint information. Our future goal is to extend exp(ASP) so that it can deal with other clingo constructs like the aggregates #, #, #, etc.
The second author would like to acknowledge the partial support of the NSF 1812628 grant. Portions of this publication and research efort are made possible through the help and support of NIST via cooperative agreement 70NANB19H102.