accepted arguments, or on some other property of the extensions. Specifically,
grounded extensions [
Circumscription [
This paper presents the argumentation reasoner pyglaf, which materializes
the above intuition. The reasoner is implemented in Python, and its interface is
fully compliant with the specification1 given for the Second International
Competition on Computational Models of Argumentation (ICCMA’17). pyglaf
implements linear reductions from many computational problems of abstract
argumentation framework to circumscription. The circumscribed theories are encoded
in the input format of circumscriptino [
An additional use case is given by the Dung’s Triathlon, a special track of
ICCMA’17 where the argumentation reasoners are asked to compute the grounded,
stable and preferred extensions of the input graph, in a single run of computation.
pyglaf addresses the triathlon by taking advantage of the following
observations [
The implemented prototype is tested empirically on the instances of the
First International Competition on Computational Models of Argumentation
(ICCMA’15). For the enumeration of complete, stable, grounded, and preferred
extensions, the performance of pyglaf is almost aligned with the most efficient
argumentation reasoners of ICCMA’15. Semi-stable, stage, and ideal extensions
were not part of ICCMA’15, but they are supported by the reasoner ConArg2
[
This section introduces the required background on abstract argumentation
frameworks [
Abstract argumentation framework An abstract argumentation framework (AF) is a directed graph G whose nodes are arguments, and whose arcs represent an attack relation. Let arg (G) and att (G) denote respectively the set of nodes and arcs in G. The size of G, denoted |G|, is defined as the number of its nodes and arcs, that is, |G| := |arg (G)| + |att (G)|. An extension E is a set of arguments. The range of E in G is EG+ := E ∪ {x | ∃yx ∈ att (G) with y ∈ E}. (When G is clear from the context, the range of E in G is simply denoted E+.) Example 1. Let G be the graph reported in Figure 1. Hence, arg (G) = {a, b, c, d, e, f }, att (G) = {aa, ab, ba, cd, dc, ce, de, ef }, and |G| = 6 + 8 = 14. The following are some extensions of G that will be used later in the paper: E1 = ∅, E2 = {d, f }, E3 = {b, d, f }, E4 = {b}, E5 = {b, c, f }, and E6 = {c, f }. The associated ranges are the following: E1+ = ∅, E2+ = {c, d, e, f }, E3+ = {a, b, c, d, e, f }, E4+ = {a, b}, E5+ = {a, b, c, d, e, f }, and E6+ = {c, d, e, f }.
Let G be an AF, and E ⊆ arg (G). The following semantics are of interest for this paper: – E is conflict-free if there are no x, y ∈ E with xy ∈ att (G). Let CF(G) denote the set of conflict-free extensions of G. – E is admissible if E ∈ CF(G), and for all yx ∈ att (G) such that x ∈ E, there is zy ∈ att (G) such that z ∈ E. Let ADM(G) denote the set of admissible extensions of G. – E is complete if E ∈ ADM(G), and satisfies the following property: if x ∈ arg (G) is such that for all yx ∈ att (G) there is zy ∈ att (G) with z ∈ E, then x ∈ E. Let CO(G) denote the set of complete extensions of G. – E is stable if E ∈ CO(G), and EG+ = arg (G). Let ST(G) denote the set of stable extensions of G. – E is grounded if E ∈ CO(G), and there is no E ∈ CO(G) such that E ⊂ E.
Let GR(G) denote the set of grounded extensions of G. – E is preferred if E ∈ CO(G), and there is no E ∈ CO(G) such that E ⊃ E.
Let PR(G) denote the set of preferred extensions of G. – E is semi-stable if E ∈ CO(G), and there is no E ∈ CO(G) such that
E +G ⊃ EG+. Let SST(G) denote the set of semi-stable extensions of G. – E is stage if E ∈ CF(G), and there is no E ∈ CF(G) such that E +G ⊃ EG+.
Let STG(G) denote the set of stage extensions of G. – E is ideal if E ∈ ADM(G), E ⊆ PR(G), and there is no E ∈ ADM(G) such that E ⊆ PR(G) and E ⊃ E. Let ID(G) denote the set of ideal extensions of G.
In particular, the last seven semantics above are those considered in the Second International Competition on Computational Models of Argumentation (ICCMA’17).
Example 2 (Continuing Example 1). The set of complete extensions of G is EC3+O(=GE)5=+ ={Ea1r,g.(. G.,)E.T6}h.eEse3 aarnedalEso5 tahree palrseofetrhreeds,tsaebmlei-esxtatebnles,ioannsdosftGagebeecxatuensesions of G. E1 is evidently the grounded extension. Finally, the ideal extension is {b}.
For an argument x ∈ arg (G), and a set S of extensions, x is credulously accepted in S, denoted S |=c x, if there is E ∈ S such that x ∈ E. Argument x is skeptically accepted in S, denoted S |=s x, if x ∈ E for all E ∈ S. Example 3 (Continuing Example 2). S |=s b and S |=s f holds for S being ST(G), PR(G), SST(G), STG(G). For the same S, S |=c d and S |=c c, but S |=s d and S |=s c. 2.2
Circumscription Let A be a fixed, countable set of atoms including ⊥. A literal is an atom possibly preceded by the connective ¬. For a literal , let denote its complementary literal, that is, p = ¬p and ¬p = p for all p ∈ A; for a set L of literals, let L be { | ∈ L}. Moreover, for a set L of literals and a set A of atoms, the restriction of L to symbols in A is L|A := L ∩ (A ∪ A).
Formulas are defined as usual by combining atoms and the connectives ¬, ∧, ∨, →, ↔. A theory is a set T of formulas including ¬⊥; the set of atoms occurring in T is denoted by atoms(T ). The size of formulas and theories is defined as the number of occurring literals; formally: for p ∈ A, |p| := 1; for φ and ψ formulas, and ◦ ∈ {∧, ∨, →, ↔}, |¬φ| := |φ|, and |φ ◦ ψ| := |φ| + |ψ|; for a theory T , |T | := φ∈T |φ|.
An assignment is a set A of literals such that A ∩ A = ∅. An interpretation for a theory T is an assignment I such that (I ∪ I) ∩ A = atoms(T ). Relation |= is defined as usual: for p ∈ A, I |= p if p ∈ I; for φ and ψ formulas, I |= ¬φ if I |= φ, I |= φ ∧ ψ if I |= φ and I |= ψ, I |= φ ∨ ψ if I |= φ or I |= ψ, and I |= φ → ψ if I |= ψ whenever I |= φ; I |= φ ↔ ψ if I |= ψ whenever I |= φ, and vice versa; for a theory T , I |= T if I |= φ for all φ ∈ T . I is a model of a theory T if I |= T . Let models(T ) denote the set of models of T . (Models will be also represented by the set of their atoms, as their negative literals are implicit.) Example 4. Let T1 be the theory {¬⊥, a ∨ b, c ∨ d → ¬a ∧ b}. The size of T1 is |T1| = 1 + 2 + 4 = 7. The models of T1 are the following: {a}, {b}, {a, b}, {b, c}, {b, d}, and {b, c, d}.
Circumscription applies to a theory T , a set P of literals, and a set Z of atoms; literals in P are subject to minimization, while atoms in Z are irrelevant. Formally, relation ≤P Z is defined as follows: for I, J interpretations of T , I ≤P Z J if both I|A\(P ∪P ∪Z) = J |A\(P ∪P ∪Z) and I ∩ P ⊆ J ∩ P . I ∈ models(T ) is a preferred model of T with respect to ≤P Z if there is no J ∈ models(T ) such that I ≤P Z J and J ≤P Z I. Let CIRC (T, P, Z) denote the set of preferred models of T with respect to ≤P Z .
Example 5 (Continuing Example 4). CIRC (T1, {a, b, c, d}, ∅) contains the minimal models of T1: {a}, and { }
b . Minimization can be restricted to few atoms: CIRC (T1, {b}, {a, c, d}) contains only { } a . Atoms not in P nor in Z are used to group interpretations: CIRC (T1, {b}, {c, d}) contains {a}, but also { } b , {b, c}, {b, d}, and {b, c, d}. Finally, CIRC (T1, {¬a, ¬b}, {d}) contains the following models: {a, b}, {b, c}, and {b, c, d}. 3
The constructions presented in this section associate arguments of the input AF G with atoms of a theory T , so to have a trivial one-to-one mapping between extensions of G and models of T . In particular, a set S of extensions of G and a set S of models of T are said equivalent with respect to G, denoted S ≡G S , if S = {I ∩ arg (G) | I ∈ S }.
In order to maintain the theory compact, additional atoms are possibly introduced. Specifically, for each argument x, an atom ax is possibly introduced to represent that x is attacked by some argument that belongs to the computed extension: ax ↔ yx∈att(G) y x ∈ arg (G) Note that if there is no yx ∈ att (G), then yx∈att(G) y is essentially ⊥, that is, atom ax is constrained to be false. Other atoms possibly introduced by our constructions are of the form rx, to enforce that argument x belongs to the range EG+ of the computed extension E:
attacked (G ) :=
range(G ) := (1) (2) (3) (4) (5) (6) rx → x ∨ yx∈att(G) y x ∈ arg (G) Example 6 (Continuing Example 2). For the graph G in Figure 1, the following formulas are possibly introduced: S1 := {aa ↔ a ∨ b, ab ↔ a, ac ↔ d, ad ↔ c, ae ↔ c ∨ d, af ↔ e}; S2 := {ra → a ∨ b, rb → b ∨ a, rc → c ∨ d, rd → d ∨ c, re → e ∨ c ∨ d, rf → f ∨ e}. In fact, note that S1 is attacked (G), and S2 is range(G).
The notion of conflict-free, admissible, complete, and stable extensions are encoded by the following sets of formulas: conflict -free(G) := {¬⊥} ∪ {¬x ∨ ¬y | xy ∈ att (G)} admissible(G) := conflict -free(G) ∪ attacked (G) ∪ {x → ay | yx ∈ att (G)} complete(G) := admissible(G) ∪ ay → x
x ∈ arg (G)
yx∈att(G) stable(G) := complete(G) ∪ range(G) ∪ {rx | x ∈ arg (G)} In particular, note that in (4) truth of an argument x implies that all arguments attacking x are actually attacked by some true argument. In (5), instead, whenever all attackers of an argument x are attacked by some true argument, argument x is forced to be true. Finally, in (6) all atoms of the form rx are forced to be true, so that the range of the computed extension has to cover all arguments.
Example 7 (Continuing Example 6). Consider the following sets of formulas: S3 := {¬⊥, ¬a, ¬a ∨ ¬b, ¬c ∨ ¬d, ¬c ∨ ¬e, ¬d ∨ ¬e, ¬e ∨ ¬f }; S4 := {a → aa, a → ab, b → aa, c → ad, e → ac, d → ac, e → ad, f → ae}; S5 := {aa ∧ ab → a, aa → b, ad → c, ac → d, ac ∧ ad → e, ae → f }.
Note that S3 is conflict -free(G), S3 ∪ S1 ∪ S4 is admissible(G), S3 ∪ S1 ∪ S4 ∪ S5 is complete(G), and S3 ∪ S1 ∪ S4 ∪ S5 ∪ S2 ∪ {ra, rb, rc, rd, re, rf } is stable(G).
The following circumscribed theories capture the complete, stable, grounded, preferred, semi-stable, and stage semantics of G: co(G) := CIRC (complete(G), ∅, Z) st (G) := CIRC (stable(G), ∅, Z) gr (G) := CIRC (complete(G), arg (G), {ax | x ∈ arg (G)}) pr (G) := CIRC (complete(G), arg (G), {ax | x ∈ arg (G)}) sst (G) := CIRC (complete(G) ∪ range(G), {¬rx | x ∈ arg (G)}, Z) stg (G) := CIRC (conflict -free(G) ∪ range(G), {¬rx | x ∈ arg (G)}, Z) (7) (8) (9) (10) (11) (12) where Z is arg (G) ∪ {ax | x ∈ arg (G)}. Note that the notion of complete and stable extensions does not really involve any preference relation, and therefore the set of literals to be minimized is empty in (7) and (8). Grounded and preferred extensions are instead obtained by imposing complementary objective literals: true arguments are minimized in (9) to capture grounded extensions, and false arguments are minimized in (10) to capture preferred extensions. Finally, in (11) and (12) false atoms in the range of the computed extensions are minimized, where computed extensions are respectively complete extensions and conflictfree extensions.
Example 8 (Continuing Example 7). Let Z be {a, b, c, d, e, f, aa, ab, ac, ad, ae, af }. It can be checked that CIRC (S3 ∪ S1 ∪ S4 ∪ S5, ∅, Z) contains, for i ∈ [1..6], the model Ei ∪ {ax | x ∈ Ei+}, and only these models. Similar for the other circumscribed theories resulting by applying (8)–(12) to graph G in Figure 1.
The ideal semantics cannot be captured by reductions similar to those above.
However, every AF G is associated with a unique ideal extension, which can be
equivalently defined as follows (Proposition 3.6 by Caminada [
Example 9 (Continuing Example 7). The union of all admissible extensions of graph G in Figure 1 is U = {b, c, d, f }. Hence, Y = {b, f }, and id (G, U ) is CIRC (S3 ∪ S1 ∪ S4 ∪ {¬a, ¬c, ¬d, ¬e}, {¬b, ¬f }, ∅) = {{b}}. 3.1
Properties Correctness of the reductions presented in this section is a direct consequence of the fact that equations (3)–(6) encode the definitions of conflict-free, admissible, complete, and stable extensions in propositional logic.
Theorem 1 (Correctness). Let G be an AF. The following equivalences hold: CO(G) ≡G co(G), ST(G) ≡G st (G), GR(G) ≡G gr (G), PR(G) ≡G pr (G), SST(G) ≡G sst (G), STG(G) ≡G stg (G), and ID(G) ≡G id (G, E∈ADM(G) E).
Compactness of the reductions follows from the fact that equations (3)–(6) have linear size with respect to the size of G.
Theorem 2 (Compactness). Let G be an AF. The size of the theories in (7)–(13) is linear in |G|.
Credulous acceptance can be also reduced to circumscription for complete, stable, and preferred extensions.
Theorem 3 (Credulous). Let G be an AF, and x be an argument. The following properties hold: – CO(G) |=c x iff CIRC (complete(G)∪{x}, ∅, arg (G)∪{ay | y ∈ arg (G)}) = ∅; – ST(G) |=c x iff CIRC (stable(G) ∪ {x}, ∅, arg (G) ∪ {ay | y ∈ arg (G)}) = ∅; – PR(G) |=c x iff CIRC (complete(G) ∪ {x}, arg (G), {ax | x ∈ arg (G)}) = ∅.
Similarly, skeptical acceptance can be reduced to circumscription for complete, and stable extensions.
Theorem 4 (Skeptical). Let G be an AF, and x be an argument. The following properties hold: – CO(G) |=s x iff CIRC (complete(G)∪{¬x}, ∅, arg (G)∪{ay | y ∈ arg (G)}) = ∅; – ST(G) |=s x iff CIRC (stable(G) ∪ {¬x}, ∅, arg (G) ∪ {ay | y ∈ arg (G)}) = ∅. 4
The reductions presented in the previous section have been implemented in the reasoner pyglaf (http://alviano.com/software/pyglaf/). The underlying programming language is Python, and the external circumscription solver is circumscriptino. The communication between pyglaf and circumscriptino is handled in the simplest possible way, that is, via stream processing. This design choice is principally motivated by the fact that the communication is often minimal, limited to a single invocation of the circumscription solver.
The interface of pyglaf is fully compliant with the specification given for the Second International Competition on Computational Models of Argumentation (ICCMA’17). Abstract argumentation frameworks can be encoded in trivial graph format (tgf) as well as in aspartix format (apx). The following data
Algorithm 1: Compute the union of admissible extensions of an AF G 1 T := admissible(G); // fix the underlying theory 2 Z := arg(G) ∪ {ax | x ∈ arg(G)}; // fix the set of irrelevant atoms 3 U := ∅; // initialize the union of all admissible extensions 4 repeat 5 Compute I ∈ CIRC (T, arg(G) \ U, Z); // prefer arguments not in U 6 I := I ∩ arg(G); // restrict to arguments of G 7 U := U ∪ I; // possibly extend the union 8 until I ⊆ U; // terminate when no argument is added to U structures are populated during the parsing of the input graph G: a list arg of the arguments in arg (G); a dictionary argToIdx, mapping each argument x to its position in arg; a dictionary att, mapping each argument x to the set {y | xy ∈ att (G)}; a dictionary attR, mapping each argument x to the set {y | yx ∈ att (G)}. The first element of the list arg, in position 0, is not used to simplify the alignment between arguments of G and variables of the produced circumscribed theory. Within these data structures, the theories in (7)–(13) can be constructed in amortized linear time. Actually, their CNF representation is easily built without introducing any additional atom, as all formulas in the previous section are either implications of the form A → B, or equivalences of the form p ↔ A, where p is an atom and A, B are sets of literals. Ideal extension. The linear reduction for the computation of the ideal extension requires the union of all admissible extensions as an input parameter. Such a set U is computed by means of Algorithm 1. Initially, U is empty, and circumscriptino is asked to compute a first admissible extension that maximize the accepted arguments. The accepted arguments are then added to U , another admissible extension is computed by circumscriptino. However, this time the maximization only involves the arguments that do not belong to U , so to expand U as much as possible. This process is repeated until the admissible extension returned by circumscriptino is covered by set U , as such extension witnesses that all admissible extensions are a subset of U .
Credulous and skeptical acceptance. Credulous acceptance is addressed according to Theorem 3 for complete, stable, and preferred extensions. Similarly, skeptical acceptance is addressed according to Theorem 4 for complete, and stable extensions. Grounded and ideal extensions are unique, and therefore credulous (and skeptical) acceptance are addressed by checking the presence of the query argument in the computed extension. Actually, for the ideal extension, a negative answer is possibly produced already if the query argument is not part of the union of all admissible extensions. The remaining acceptance problems are addressed naively by extension enumeration.
Dung’s Triathlon. The triathlon is addressed by Algorithm 2 based on the
following observations: the grounded extension is contained in every preferred
extension (Theorem 25 by Dung [
Algorithm 2: Grounded, stable and preferred extensions of G
1 Compute Igr ∈ co(G); // first of all, compute the grounded extension
2 stable := ∅; // initialize the set of stable extensions
3 preferred := ∅; // initialize the set of preferred extensions
// simplification: Igr is contained in all preferred extensions
4 T := complete(G) ∪ {x ∈ arg(G) | x ∈ Igr}; P := arg(G); Z := {ax | x ∈ arg(G)};
5 for I ∈ CIRC (T, P, Z) do // enumerate preferred extensions
6 preferred := preferred ∪ {I}; // found new preferred extension
7 if for all x ∈ arg(G) \ I there is yx ∈ att(G) such that y ∈ I then
8 stable := stable ∪ {I}; // the preferred extension is also stable
9 return (Igr, stable, preferred);
extension (Lemma 15 by Dung [
In order to assess empirically the implemented reasoner, instances from the
First International Competition on Computational Models of Argumentation
(ICCMA’15) were tested on the enumeration of all extensions for several
semantics. The performance of pyglaf is compared with the following reasoners that
participated in the competition: ArgSemSAT (version 1.0rc3; [
Complete and stable extensions. For these two semantics the set of objective literals is empty. Aggregated results are reported on Table 1. The performance of pyglaf is essentially aligned to the performance of ArgSemSAT and LabSATSolver: they run out of time on the same instance of 4 st small. All instances are solved by aspartix-d, while ConArg2 collected several timeouts. Similar results are obtained for the enumeration of stable extensions, which was completed for all instances by all tested reasoners but ConArg2. Grounded and preferred extensions. For the computation of grounded and preferred extensions the underlying propositional theory has models representing complete extensions of the input graph. Complementary objective literals are used: accepted arguments are minimized to obtain the grounded extension, while nonaccepted arguments are minimized to obtain preferred extensions. Aggregated results are reported on Table 2. The grounded extension is unique, and computed very efficiently by pyglaf, ArgSemSAT, and LabSATSolver. Several timeouts are instead collected by aspartix-d and ConArg2. As for preferred extensions, a very good performance is exhibited by pyglaf, ArgSemSAT, and LabSATSolver, running out of time only on one instance (the same instance for which they cannot enumerate all complete extensions). Preferred extensions can be also enumerated by the reasoners prefMaxSAT and prefASP. The first reasoner collected several timeouts, while prefASP resulted very efficient and solved all testcases.
Other extensions and Dung’s Triathlon. The enumeration of semi-stable, stage and ideal extensions is supported by ConArg2, but not by the other reasoners (at least in the versions found on the web). Hence, for these two semantics the comparison is restricted to pyglaf and ConArg2. Aggregated results are reported on Table 3. The performance of pyglaf is in general better than that of ConArg2, especially on the enumeration of semi-stable and ideal extensions. Several timeouts are collected by pyglaf on the enumeration of stage extensions due to their large number. It is interesting to observe that for the stage semantics pyglaf requires around one order of magnitude less memory than ConArg2. Concerning the triathlon, the improvement on the naive approach of executing the three computational tasks sequentially is minimal: the gain is limited to one solved instance, and few seconds of computation on average. 6
There are many argumentation reasoners; the closest to the present work are
ArgSemSAT [
The definition of circumscription given in this paper is slightly different from
the one originally introduced by Mc Carthy [
Many semantics of abstract argumentation frameworks are naturally encoded in the language of circumscription. Based on the comparison with some of the best performant reasoners of ICCMA’15, the linear encodings implemented in pyglaf appear to be a reasonable solution to the enumeration problems of abstract argumentation frameworks. Clearly, this is subject to the availability of an efficient solver for circumscription. Currently, circumscriptino is used, but pyglaf can easily accommodate different solvers. Some of the acceptance problems are currently handled naively. This condition can be significantly improved by extending circumscriptino with native support for query answering, which we plan to address in the near future. core analysis. TPLP 17, 1–18 (2017) average execution time (seconds) on solved instances, and memory consumption (MB). semi-stable
stage pyglaf