1 Introduction

This paper describes a new algorithm for the computation of the semantics of argumentation frameworks based on the idea of forward propagation of \(\mathbf {in}\) labels of accepted argument. The basic mechanism is very simple: the construction of complete extensions is done by attempting to re-label \(\mathbf {in}\) all undecided (\(\mathbf {und}\)) arguments that could potentially be labelled \(\mathbf {in}\) by a labelling function and checking whether the resulting function can be made “legal”.

The algorithm works on the strongly connected components (SCCs) of an argumentation framework which are arranged into layers following the direction of attacks. Because of the dependencies between the valid assignments of labels of attacking and attacked arguments, a solution for one layer may impose constraints on the possible solutions for SCCs of subsequent layers. In such cases, we say that the solution of one layer conditions the possible legal label assignments of the attacked SCC. So we take this idea further by looking at the consequences of legally labelling an argument \(\mathbf {in}\) in an SCC: we search for labelling assignments of the SCC satisfying an increasing set of constraints. All solutions thus found are combined in the way described in [11].

We start with the undecided arguments of an SCC that could potentially be labelled \(\mathbf {in}\) in some solution. By labelling one of these arguments \(\mathbf {in}\), we are forced to label all of its attackers \(\mathbf {out}\) (i.e., reject them). If all attackers of an argument are re-labelled \(\mathbf {out}\), then the argument must be re-labelled \(\mathbf {in}\), imposing new constraints on the labels of the arguments that it attacks, and so forth. Forcing the attacker of an argument to be labelled \(\mathbf {out}\) is done analogously by requiring that at least one of the attacker’s attacker is labelled \(\mathbf {in}\), so the whole process can be done through a series of recursive forward propagation operations of \(\mathbf {in}\) labels each of smaller complexity than the original one.

Searching for extensions in this way has several advantages. The constraints can prune the search space considerably by ruling out assignments that violate the admissibility conditions. Thus, the algorithm is designed to incrementally “fill in” the gaps of an admissible but partially uncommitted labelling function by successively swapping labels from \(\mathbf {und}\) to \(\mathbf {in}\) or \(\mathbf {out}\), and as a result generating all complete extensions along the way. As a by-product, we can pick an argument of interest and attempt to construct a legal labelling assignment that labels the argument in a particular way (e.g., \(\mathbf {in}\)), without necessarily having to look at all solutions of the SCC or the argumentation framework as a whole.

The rest of the paper is structured as follows. In Sect. 2, we provide some background material for the paper. This is followed by the presentation of the algorithm itself in Sect. 3.Footnote 1 In Sect. 4, we compare our algorithm with others in the literature. Section 5 provides some empirical evaluation of the algorithm and we conclude in Sect. 6 with a discussion and some future work.

2 Background

An abstract argumentation framework is a system for reasoning about arguments proposed by Dung [9] and defined in terms of a directed graph \(\langle \mathcal A,\mathcal R \rangle \), where \(\mathcal A\) is a finite non-empty set of arguments and \(\mathcal R\) is a binary relation on \(\mathcal A\), called the attack relation. If \((X,Y) \in \mathcal R\), we say that X attacks Y and denote it in the graph with an edge from X to Y. In what follows, \(X^{-}=\{Y \in \mathcal A| \text {(Y,X)} \in \mathcal R\}\); and \(X^{+}=\{Y \in \mathcal A| \text {(X,Y)} \in \mathcal R\}\). For sets \(E\subseteq \mathcal A\), \(E^-\) and \(E^+\) are defined in an obvious way via set union. We write \(E\! \rightarrow \! X\) as a shorthand for \(X \in E^+\). The path-equivalence relation \(\sim _\mathcal{R}\subseteq \mathcal A^2\) is defined as \(X \sim _\mathcal{R}Y\) iff \(X=Y\) or there is a path from X to Y and a path from Y to X in \(\mathcal R\). A strongly connected component (SCC) is an equivalence class of arguments under \(\sim _\mathcal{R}\).

One of the main purposes of an argumentation framework is to provide a way of reasoning about the status of its arguments, i.e., whether an argument is accepted or is defeated by other arguments. Arguments that have no attacks are always accepted. However, an attack from X to Y may not be sufficient to defeat Y, because X may itself be defeated, and thus the statuses of arguments need to be determined systematically. In Dung’s original formulation, this is usually done through acceptability conditions for the arguments. A semantics can then be defined in terms of extensions—subsets of \(\mathcal A\) with special properties. A set \(E \subseteq \mathcal A\) is said to be conflict-free if for all elements \(X,Y \in E\), we have that \((X,Y) \not \in \mathcal R\). Although a conflict-free set only contains elements that do not attack each other, this does not necessarily mean that all arguments in the set are properly supported. Well-supported sets satisfy special admissibility criteria. An argument \(X\in \mathcal A\) is acceptable with respect to E, if for all \(Y \in X^{-}\), \(E\cap Y^{-}\ne \varnothing \). A set E is admissible if it is conflict-free and all of its elements are acceptable with respect to itself. An admissible set E is a complete extension iff E contains all arguments which are acceptable with respect to itself; E is called a preferred extension iff E is a \(\subseteq \)-maximal complete extension; and E is stable if E is preferred and \(E \cup E^{+}=\mathcal A\).

Dung’s semantics can also be presented in terms of a Caminada labelling function of the form \(\lambda :\mathcal A\longrightarrow \) {\(\mathbf {in}\),\(\mathbf {out}\),\(\mathbf {und}\)} satisfying certain conditions [4, 5, 15]. Let dom denote the domain of a function and \(\lambda \) a labelling function, we define \(in(\lambda ) = \{X \in \mathrm {dom}~\lambda | \lambda (X) = \mathbf {in}\}\); \(und(\lambda ) = \{X \in \mathrm {dom}~\lambda | \lambda (X) = \mathbf {und}\}\); and \(out(\lambda ) = \{X \in \mathrm {dom}~\lambda | \lambda (X) =\) \(\mathbf {out}\)}. The notion of extension is recovered from the set \(in(\lambda )\) for some labelling function \(\lambda \). Furthermore, we say that an argument X is illegally labelled \(\mathbf {in}\) by \(\lambda \), if \(X^{-} \not \subseteq out(\lambda )\); X is illegally labelled \(\mathbf {out}\) by \(\lambda \), if \(X^{-} \cap in(\lambda ) =\varnothing \); and X is illegally labelled \(\mathbf {und}\) by \(\lambda \), if either \(X^{-}\subseteq out(\lambda )\) or \(X^{-}\cap in(\lambda )\ne \varnothing \). Finally, X is super-illegally labelled \(\mathbf {in}\) if it is attacked by an argument that is legally labelled \(\mathbf {in}\) or labelled \(\mathbf {und}\) [12]. A labelling function is legal it does not illegally label any arguments.

2.1 Computing Extensions via Decomposition into SCCs

Baroni et al. proposed a general recursive schema for argumentation semantics in [1]. The schema employs the decomposition of an argumentation framework into SCCs and can be used to obtain Dung’s admissibility-based semantics. Based on that, many researchers showed how to compute the extensions of argumentation frameworks under several semantics. Baumann adapted the Modgil-Caminada’s algorithms [12] to compute extensions under the grounded, preferred and stable semantics in what he called “split” frameworks [2]. Preliminary experimental results of the advantages of these techniques were then shown in [3]. Liao described the use of the decomposition idea for computation of argumentation semantics in a more general way [11].

The overall process can be summarised as follows. Firstly, the SCCs of an argumentation framework are arranged into layers following the direction of attack. Then the solutions for each layer are computed using an appropriate algorithm for the semantics at hand and the solutions of the previous layers. Finally, the solutions of subsequent layers are combined in a systematic way. To illustrate this idea, consider the argumentation framework \(\mathcal{{N}}\) in Fig. 1 with SCCs \(S_1=\{X\}\), \(S_2=\{W,Y\}\) and \(S_3=\{A,B,C,D,E\}\). Following the attack relation, these SCCs can be arranged into two layers, the first containing \(S_1\) and \(S_2\) and the second containing \(S_3\). The solutions of the SCCs in a given layer are all independent from each other, but the attacks between arguments of different layers create dependencies of the solutions of an SCC on the solutions of the SCCs attacking it. For example, the computation of the solutions of \(S_3\) depends on the labels assigned to X and W, and thus on the solutions of \(S_1\) and \(S_2\). As \(S_1\) and \(S_2\) have no external attackers, their solutions can be computed completely independently of the rest of the framework. \(S_2\) has three legal assignments: one in which both W and Y are labelled \(\mathbf {und}\) and the other two in which one of them is labelled \(\mathbf {in}\) and the other is labelled \(\mathbf {out}\). \(X=\mathbf {in}\) is the only solution to \(S_1\), so each of the partial solutions to \(S_2\) must be augmented with the assignment \(X = \mathbf {in}\), giving all partial solutions to layer 0: \(f_1\!:\,X = Y = \mathbf {in}, W = \mathbf {out}\), \(f_2\!: X = W = \mathbf {in}, Y = \mathbf {out}\), and \(f_3\!:\,X = \mathbf {in}, W = Y = \mathbf {und}\).Footnote 2 [11].

Now consider the computation of the solutions for \(S_3\). We say that \(S_3\)’s solutions are conditioned by the labels of the external attackers X and W in the partial solutions \(f_1\), \(f_2\) and \(f_3\). In any such solution, \(X=\mathbf {in}\), but the label of W could be either \(\mathbf {out}\), \(\mathbf {in}\) or \(\mathbf {und}\). In order to generate all complete extensions for \(\mathcal{{N}}\), each partial solution \(f_1\), \(f_2\) and \(f_3\) needs to be expanded with the solutions for \(S_3\) under the constraints that they impose.

Definition 1

(Initial Conditioned Solution for an SCC). Let f be a conditioning solution for an SCC S. The initial solution for S conditioned by f \({\lambda ^{f}_{S}}: S\longmapsto \) {\(\mathbf {out}\),\(\mathbf {und}\),\(\mathbf {in}\)} is a legal labelling function whose set \(in(\lambda ^{f}_{S})\) is \(\subseteq \)-minimal with respect to all legal labelling functions conditioned by f.

\(\lambda ^{f}_{S}\) is the “minimal” (grounded) solution for S under f. It is a special case of forward propagation from external attackers starting with the all undecided labelling (all-\(\mathbf {und}\)). The Discrete Gabbay-Rodrigues Iteration Schema [10] is an example of a method that can perform this propagation very efficiently.

Since \(f_1(X)\!=\!\mathbf {in}\) and \(f_1(W)\!=\!\mathbf {out}\), the search for the solutions for \(S_3\) conditioned by \(f_1\) consists of the search for all solutions to \(S_3\) with the constraint \(A\!=\!\mathbf {out}\) or the search of all possible ways to “expand” \(\lambda _S^{f_1}\) by swapping labels from \(\mathbf {und}\) to \(\mathbf {in}\) or \(\mathbf {out}\). Similarly, since the \(f_2(X)\!=\!f_2(W)\!=\!\mathbf {in}\), under \(f_2\) we need to satisfy the constraint \(A\!=\!B\!=\!\mathbf {out}\). A similar reasoning applies to solution \(f_3\) in which we have the “implicit” constraint \(\lambda _S^{f_3}(B)\ne \mathbf {in}\) (since \(\lambda _S^{f_3}(W)\!=\!\mathbf {und}\)). More generally speaking, the whole process can be thought of as follows: given a SCC S, a conditioning solution f, and a partial labelling function \(\lambda _S^f\), compute the set \(\varLambda \) of all expansions of \(\lambda _S^f\) satisfying some constraints.

Fig. 1.
figure 1

A complex argumentation framework and its decomposition into layers.

Decomposition breaks the argumentation problem into smaller sub-problems, but an algorithm is still needed to find the solutions for each SCC. Modgil-Caminada’s algorithm for preferred extensions is one algorithm that can be adapted for this [12].

2.2 Modgil-Caminada’s Algorithm for Preferred Extensions

For space limitations we cannot present Modgil-Caminada’s algorithm in full, but we will describe it in general terms. This should suffice for our discussion.

Since preferred extensions are associated with maximal sets of arguments that are labelled \(\mathbf {in}\), Modgil-Caminada’s algorithm starts with the labelling function that labels all arguments \(\mathbf {in}\) (all-\(\mathbf {in}\)) and then successively “corrects” illegally labelled arguments via a so-called transition step. Eventually, all illegal labels get corrected, and the set of arguments labelled \(\mathbf {in}\) will correspond to an extension – those that are maximal will correspond to the preferred extensions.Footnote 3 A transition step consists of the following. If the argument X is illegally labelled \(\mathbf {in}\), then it is re-labelled \(\mathbf {out}\), if it can be legally re-labelled so. Otherwise it is re-labelled \(\mathbf {und}\). Afterwards, the labels of all arguments in \(X^{+}\) that become illegally labelled \(\mathbf {out}\) by the fact that X has been re-labelled from \(\mathbf {in}\) to \(\mathbf {out}\) or \(\mathbf {und}\), are then also changed to \(\mathbf {und}\). The algorithm applies transition steps as follows. If there is any argument X in \(\lambda \) that is super illegally labelled \(\mathbf {in}\), then the algorithm performs a single transition step on X generating a new labelling function \(\lambda ^{\prime }\) and then calls itself recursively from \(\lambda ^{\prime }\). If there is no such argument, the algorithm will instead iterate through all arguments that are illegally labelled \(\mathbf {in}\); apply a transition step on each; and call itself recursively from the new labelling functions thus generated. Eventually, all labels will become legal and the algorithm will simply return the labelling functions with maximal sets of arguments labelled \(\mathbf {in}\).

In Sects. 4 and 5, we will see that the strategy used by Modgil-Caminada’s algorithm may result in a very high number of operations.

3 A New Algorithm for Enumeration and Decision Problems of Argumentation Semantics

Our algorithm’s strategy takes advantage of the constraints that a legal labelling function must satisfy. These constraints come from two sources: (i) the labels of the external attacking arguments in the conditioning solutions (which already partially determine the SCC’s solution); and (ii) the internal constraints arising from re-labelling the seed argument \(\mathbf {in}\). The constraints help to reduce the search space. The successful implementation of this strategy relies on an efficient propagation mechanism (see Sect. 6) and a bottom-up method for constructing all extensions.

This way of looking into the problem has two major implications. By generating all complete extensions, the method can be used in problems involving the grounded, complete, stable and preferred semantics. For the grounded semantics, all we need to do is to propagate the (unique) conditioning solution; for the preferred semantics, we generate alternative solutions but only keep those that maximise the set of nodes labelled \(\mathbf {in}\); and for the stable semantics we exclude preferred solutions with undecided nodes. Secondly, because we only work on an individual argument at a time, we can define decision procedures for argument acceptability that do not need to necessarily generate all extensions.

In order to lighten the notation, we will drop the subscript and superscript in \({\lambda ^{f}_{S}}\) when the context makes the SCC S and the conditioning solution \(\text {f}\) clear. Given a partial solution \(\lambda \) conditioned by a solution f, an argument X of an SCC S can potentially be re-labelled from \(\mathbf {und}\) to \(\mathbf {in}\) if it satisfies the following conditions: (I1) \(\lambda (X)\!=\!\mathbf {und}\); (I2) \(X \not \in X^{-}\) (it does not attack itself); and (I3) \(\{Y \in X^- | f(Y)\!=\!\mathbf {und}\}\!=\!\varnothing .\) Footnote 4 The set \(possIns_S \subseteq S\) is the set of nodes satisfying conditions (I1)–(I3). Thus the starting point for Algorithm 1 is an SCC S; the set \(possIns_S\); a conditioning solution f for previous layers; and a partial solution \(\lambda \) for S conditioned by f. The algorithm will compute the set \(\varLambda \) of all complete (or preferred)Footnote 5 labelling functions that “expand” \(\lambda \) by successively searching for complete/preferred labelling functions that label an element of \(possIns_S\) \(\mathbf {in}\). Each search is done via Algorithm 4, which we now explain.

figure a

In Sect. 2, we saw that an argument X is legally labelled \(\mathbf {in}\) in a solution \(\lambda \) if all arguments that it attacks are labelled \(\mathbf {out}\) and that if all arguments that attack X are labelled \(\mathbf {out}\) then X must be labelled \(\mathbf {in}\) in \(\lambda \). Thus, to re-label X \(\mathbf {in}\) we must re-label \(\mathbf {out}\) all arguments that it attacks. By re-labelling some arguments \(\mathbf {out}\), we may also be forced to re-label \(\mathbf {in}\) some other arguments, and so forth. We call this process the forward propagation of the \(\mathbf {in}\) label. All attackers of X must also be labelled \(\mathbf {out}\) for X to be legally labelled \(\mathbf {in}\) in \(\lambda \). Thus, all external attackers of X must be labelled \(\mathbf {out}\) (by f) and all internal attackers that are still labelled \(\mathbf {und}\) must be re-labelled \(\mathbf {out}\). This can be done by ensuring that every internal attacker Y that is labelled \(\mathbf {und}\), gets an attacker Z to be legally re-labelled \(\mathbf {in}\). We call the process of ensuring that all attackers of X are legally labelled \(\mathbf {out}\) the backward propagation of the \(\mathbf {in}\) label. Backward propagations can be done in terms of one or more forward propagations and this is the motivation for the title of the algorithm.

Although we start with “good enough” candidates, i.e., arguments satisfying (I1)–(I3), both types of propagations may fail, since we have no control over the assignments of conditioning solutions and the propagations may result in inconsistent label requirements. A failed propagation simply means that we cannot construct a legal labelling function meeting the required constraints, so we backtrack to any available alternatives. We now explain the details.

3.1 Propagating Forwards

A forward propagation essentially requires changing the label of a seed node in a partial solution \(\lambda \) from \(\mathbf {und}\) to \(\mathbf {in}\) and then following the direction of attacks to re-label any nodes that may have thus have been rendered illegally labelled. One important aspect of a forward propagation is that (if successful) it will generate a single solution \(\lambda ^{\prime }\) from a partial solution \(\lambda \) which, by construction, has less undecided nodes than \(\lambda \) itself. A forward propagation is carried out by the function propagateIN in Algorithm 2. Figure 2 illustrates the labelling function \(\lambda ^{\prime }\) obtained as the result of a successful forward propagation from \(X\!=\!\mathbf {in}\) and \(f\!=\!\varnothing \) and a failed forward propagation from \(W_2\!=\!\mathbf {in}\) and \(f\!=\!\varnothing \). The latter fails because by labelling \(W_2\) \(\mathbf {in}\), we must label U \(\mathbf {out}\), which then requires T to be labelled \(\mathbf {in}\), which in turn requires \(W_2\) to be labelled \(\mathbf {out}\), which is not possible.

figure b
Fig. 2.
figure 2

Results of forward propagations from \(X=\mathbf {in}\) and \(W_2=\mathbf {in}\).

If the forward propagation from a node X is successful, we must then ensure that all of X’s attackers are legally labelled \(\mathbf {out}\) in order to guarantee that the solution is legal. This is done by a backward propagation.

3.2 Propagating Backwards

In the example in Fig. 2, it is easy to see that \(\lambda ^{\prime }\) is not legal, since \(\lambda ^{\prime }(X)\!=\!\mathbf {in}\), \(Y_1 \rightarrow X\), but \(\lambda ^{\prime }(Y_1)\!=\!\mathbf {und}\). We can perform a backward propagation from X by performing one or more forward propagations using any of the attackers of each attacker of X as the seed. \(X^{-}=\{Y_1,W_2\}\), so we want a labelling function that labels at least one of the arguments in \(Y_1^{-}\) and in \(W_2^{-}\) \(\mathbf {in}\) (X itself already satisfies the latter). It is easy to see that the labelling function \(\lambda ^{\prime \prime }\!=\!\{X\!=\!U\!=\!W_1\!=\!\mathbf {in},Y_2\!=\!W_2\!=\!T\!=\!Y_1\!=\!\mathbf {out}\}\) satisfies these requirements.

Naturally, a backward propagation may also fail. Consider the network in Fig. 3. After a successful forward propagation from \(X\!=\!\mathbf {in}\), \(\text {f}\!=\!\varnothing \), and \(\lambda \)=all-\(\mathbf {und}\), we get the labelling function \(\lambda ^{\prime }\!=\!\{X\!=\!\mathbf {in},Y\!=\!\mathbf {out},W_1\!=\!W_2\!=\!W_3\!=\!\mathbf {und}\}\), which is not legal, since \(W_3 \rightarrow X\) and \(\lambda ^{\prime }(W_3)\ne \mathbf {out}\). So we attempt to backward propagate from X, \(\text {f}\!=\!\varnothing \) and \(\lambda ^{\prime }\). We need to label \(W_3\) \(\mathbf {out}\), which requires labelling \(W_2\!=\!\mathbf {in}\), which is not possible since it attacks itself, and thus the backward propagation fails. What this means in practice is that X cannot be part of any extension (this reasoning can be used in decision problems).

Fig. 3.
figure 3

Backward propagation.

Unlike a forward propagation, a backward propagation can generate multiple labelling functions. Consider the SCC S in the network in Fig. 4(L). A call to \(\texttt {propagateIN}(X,S,\text {f},\lambda ,\lambda ^{\prime })\) will succeed with \(\lambda ^{\prime }\!=\!\{X\!=\!\mathbf {in},Y\!=\!\mathbf {out},Z_1\!=\!Z_2\!=\!Z_3\!=\!Z_4\!=\!W_1\!=\!W_2\!=\!\mathbf {und}\}\). We must now legally label both \(W_1\) and \(W_2\) \(\mathbf {out}\). But here we have a choice between labelling \(Z_1\) or \(Z_2\) \(\mathbf {in}\). So both \(\varvec{\lambda }^{\varvec{\prime }}_{\varvec{C}}\!=\!\{X\!=\!\mathbf {in},Y\!=\!\mathbf {out},Z_1\!=\!\mathbf {in},W_1\!=\!W_2\!=\!Z_3\!=\!\mathbf {out},Z_2\!=\!Z_4\!=\!\mathbf {und}\}\) (Fig. 4(C)) and \(\varvec{\lambda }^{\varvec{\prime }}_{\varvec{R}}\!=\!\{ X\!=\!\mathbf {in},Y\!=\!\mathbf {out},Z_2\!=\!\mathbf {in},W_1\!=\!W_2\!=\!Z_4\!=\!\mathbf {out},Z_1\!=\!Z_3\!=\!\mathbf {und}\}\) (Fig. 4(R)) are returned in \(\varLambda \) from an invocation to \(\texttt {propagateOUT}(X,S,\text {f},\lambda ^{\prime },\varLambda )\).

Fig. 4.
figure 4

A sample network and two successful backward propagations from \(X=\mathbf {in}\).

There are two more important considerations to make. First, all of the attackers of the seed node must be labelled \(\mathbf {out}\). Therefore any solution returned by propagateOUT must satisfy this requirement. Our implementation approach in Algorithm 3 was to work with two lists. makeOuts contains the nodes that still need to be labelled \(\mathbf {out}\) and starts with all undecided attackers of the seed node (Algorithm 3, line 5). At least one solution must be found labelling all of these nodes \(\mathbf {out}\). If this is not possible, propagateOUT simply fails (Algorithm 3, line 27). This essentially complements propagateIN to guarantee the correctness of the algorithm. The solutions are stored in the list sols, which is initialised with the result of the forward propagation of the seed node (Algorithm 3, line 12). For each node in makeOuts, sols is replaced with a new set of satisfying solutions. Each successive node is then checked against all new solutions thus generated which, by construction, label \(\mathbf {out}\) all of the previously removed nodes in makeOuts. If we successfully exhaust all of the nodes in makeOuts, then propagateOUTsucceeds and returns all corresponding solutions (line 30). Otherwise, it fails and \(\varLambda \) is not updated.

figure c
Fig. 5.
figure 5

Undecided sub-cycles within solutions.

The story does not end here though, and this takes us to the second important consideration which has to do with completeness. The result of a successful backward propagation may still leave some nodes of an SCC in what are effectively induced sub-SCCs ring-fenced by \(\mathbf {out}\) -labelled nodes. Consider the network of Fig. 4(L) again. In order to legally label X \(\mathbf {in}\) we need to label \(W_1\) and \(W_2\) \(\mathbf {out}\). We have seen that this can be done by labelling either \(Z_1\) or \(Z_2\) \(\mathbf {in}\), giving us the solutions \(\varvec{\lambda }^{\varvec{\prime }}_{\varvec{C}}\) (extension \(\{X,Z_1\}\)) and \(\varvec{\lambda }^{\varvec{\prime }}_{\varvec{R}}\) (\(\{X,Z_2\}\)) of Fig. 4(C) and (R), respectively. However, \(\varvec{\lambda }^{\varvec{\prime }}_{\varvec{C}}\) leaves \(Z_2\) and \(Z_4\) undecided, whereas \(\varvec{\lambda }^{\varvec{\prime }}_{\varvec{R}}\) leaves \(Z_1\) and \(Z_3\) undecided. In order to break these cycles (and hence guarantee completeness w.r.t. all complete extensions), all we have to do is to simply treat \(Z_4\)\(Z_2\) and \(Z_3\)\(Z_1\) as “sub-SCCs” and restart the whole process from the same original conditioning solution but now with initial conditioned solutions \(\varvec{\lambda }^{\varvec{\prime }}_{\varvec{C}}\) and \(\varvec{\lambda }^{\varvec{\prime }}_{\varvec{R}}\) (see Fig. 5). This is implemented in lines 8 and 10 of Algorithm 4. In our example, \(\varvec{\lambda }^{\varvec{\prime }}_{\varvec{C}}\) will generate sub-solutions \(Z_4\) = \(\mathbf {in}\), \(Z_2\) = \(\mathbf {out}\) and \(Z_4\) = \(\mathbf {out}\), \(Z_2\) = \(\mathbf {in}\); whereas \(\varvec{\lambda }^{\varvec{\prime }}_{\varvec{R}}\) will generate sub-solutions \(Z_3\) = \(\mathbf {in}\), \(Z_1\) = \(\mathbf {out}\) and \(Z_3\) = \(\mathbf {out}\), \(Z_1\) = \(\mathbf {in}\). The search will eventually terminate because recursive calls are only made with initial solutions containing less \(\mathbf {und}\) labels than their parents’ and the fact that the argumentation graph is finite.

3.3 Combining All Steps

Algorithm 1 will attempt to label \(\mathbf {in}\) all candidate arguments that can be possibly labelled \(\mathbf {in}\). We then generate all possible solutions starting from each of these arguments with Algorithm 4. This requires to attempt to propagate forward from \(X=\mathbf {in}\) (line 3). If this is successful, it will generate a new labelling function \(\lambda ^{\prime \prime }\) with at least two less undecided arguments than \(\lambda ^{\prime }\). We then attempt to propagate backwards from \(\lambda ^{\prime \prime }\) (line 5), to guarantee that all attackers of X are legally labelled \(\mathbf {out}\). If this is successful, it will generate a number of possible solutions \(\varLambda ^{\prime }\), which we add to the current set of solutions (line 7). These solutions may still leave some undecided nodes, so we restart the process from each solution \(\sigma \) in \(\varLambda ^{\prime }\) and the remaining candidate undecided nodes (lines 8 and 10), adding again the results to the set of solutions (line 12). At this point, we can filter out the solutions that do not yield preferred extensions if needed (see Algorithm 5).

figure d
figure e

Proposition 1

(Soundness and Completeness). Let S be an SCC, f an admissible conditioning labelling function, and \(\lambda \) a labelling function for S conditioned by f (cf. Definition 1), then (1) all labelling functions returned by Algorithm 1 are legal; and (2) these are all the legal labelling functions for S.

Proof. Omitted, but soundness comes from the fact that lines 7 and 12 of Algorithm 4 only add legal labelling functions and completeness from the facts that all alternative solutions are tried in line 2 of Algorithm 1 and line 10 of Algorithm 4.

4 Analysis and Comparisons with Other Work

In Sect. 2, we briefly described the Modgil-Caminada’s algorithm for preferred extensions and mentioned that it could behave very inefficiently. In fact, Charwat et al. pointed out that for the class of argumentation frameworks \(\langle \mathcal A,\mathcal A^\mathrm{2} \rangle \), the algorithm produces n! branches (where \(n=|\mathcal A|\)), all with the same extension [8]. Since each node in each branch of execution corresponds to a transition step, the total number of transition steps is at least twice as many. In fact, it is \(n!+\sum _{i=1}^{n-1}\frac{n!}{(n-i)!} \ge 2n!\), to be precise. Although arguably unrealistic, this class of argumentation frameworks is particularly hard for Modgil-Caminada’s algorithm, but it is dealt with trivially by our algorithm, requiring only n steps to identify that no nodes can be possibly labelled \(\mathbf {in}\) and then producing the empty extension. This is because the higher the degree of attacks, the higher the degree of constraints and hence the lower the number of alternatives to check by our algorithm. Perhaps a more interesting class of frameworks to compare is what we call bi-directed cycle graphs involving a cycle with all nodes in both directions (see Fig. 6 (Start)). We now discuss the behaviour of both algorithms for this class of graphs. Modgil-Caminada’s algorithm would start with the all-\(\mathbf {in}\) labelling function and hence all nodes would be initially illegally labelled \(\mathbf {in}\). None is super-illegally labelled \(\mathbf {in}\), so the algorithm would iterate through all nodes, performing a transition step on each one and then recursively calling itself with the labelling functions resulting from the transitions. For the sake of argument, let us assume that the algorithm picks node \(A_1\) first. \(A_1\)’s label would be changed from \(\mathbf {in}\) to \(\mathbf {out}\). As it would become legally labelled \(\mathbf {out}\) and none of the nodes that it attacks is labelled \(\mathbf {out}\), the first transition step would result in the labelling TS1 of Fig. 6.Footnote 6 None of the nodes in TS1 are legally labelled \(\mathbf {in}\) or super-illegally labelled \(\mathbf {in}\), so the algorithm would then again iterate through all nodes that remain illegally labelled \(\mathbf {in}\) (4 in total). In the branches that pick a node adjacent to \(A_1\), say \(A_2\), the following would happen. The algorithm would change \(A_2\)’s label to \(\mathbf {out}\) (which is illegal), and then to \(\mathbf {und}\). \(A_1\) is the only node that \(A_2\) attacks and it is labelled \(\mathbf {out}\), but it is legally labelled so. The algorithm would then choose from one of the remaining illegally labelled nodes (of which there would be 3). If it agains picks an adjacent node, say \(A_3\), it would change its label to \(\mathbf {out}\) and then to \(\mathbf {und}\), and this process would continue until all nodes were re-labelled \(\mathbf {und}\). This sequence of transitions is depicted in graphs TS1, TS2,..., TS5 of Fig. 6. The algorithm would eventually pick \(A_3\) or \(A_4\) as an alternative choice to \(A_2\) and in those branches it would eventually produce the preferred extensions. However, the number of recursive calls would still remain close to factorial (See Fig. 7). Our algorithm by contrast would start with all nodes labelled \(\mathbf {und}\) and pick any initial seed node. In enumeration problems the choice is actually irrelevant as all eligible undecided nodes are attempted. In decision problems, we can start with an argument of interest and continue only if an appropriate extension can be constructed. If we start by propagating \(A_1=\mathbf {in}\), we are immediately forced to label \(A_2\) and \(A_5\) \(\mathbf {out}\), giving us only two further choices to generate the preferred extensions, i.e., either to label \(A_3=\mathbf {in}\) or to label \(A_4=\mathbf {in}\). Figure 7 shows the number of transition steps performed by Modgil-Caminada’s algorithm in bi-directed cycle graphs of up to 24 nodes and the number of recursive calls in our own algorithm (both implemented in EqArgSolver). For comparison, we included the factorial and \(2^x\) functions.

Fig. 6.
figure 6

Bi-directed cycle graph behaviour

Fig. 7.
figure 7

Transition steps \(\times \) calls to propagateIN and propagateOUT

In [6], Cerutti et al.’s proposed a meta-algorithm that decomposes the original argumentation framework into SCCs and uses a “base algorithm” at the base of the recursion to solve the original problem at the SCC level. As an illustration of the approach, the base algorithm employed a SAT solver. It should be possible to swap the algorithm here proposed for the call to the SAT solver [6, Line 19, Algorithm 2] or vice-versa using an appropriate translation of the problem, since a conditioning solution simply constrains the set of possible models. This investigation will appear in a forthcoming paper. Finally, Nofal et al. proposed algorithms for decision problems in the preferred semantics [13]. The algorithm presented here is not restricted to this semantics only. We will however compare the approaches of these algorithms and ours in future work.

5 Empirical Evaluation

Apart from the special cases discussed above, we also conducted some experiments to compare Modgil-Caminada’s algorithm with ours in randomly generated graphs. Our objective was not to conduct an extensive empirical evaluation between general solvers, as this will be done by the 2nd International Competition of Computational Models of Argumentation (ICCMA), but merely to provide a first-hand evaluation of the two labelling approaches. In order to eliminate any implementation factors that could directly affect the comparison between the two, they were both embedded within two versions of EqArgSolver which was invoked for the preferred semantics only. For further comparison we also recorded the results provided by Tweetysolver v1.2, which also uses decomposition into SCCs but uses a SAT solver for solutions. Tweetysolver was chosen because it is an off-the-peg easy-to-deploy solver and a “good enough” initial marker for the performance of SAT-based solvers in this class of problems.

We generated 3 datasets of 1,000 graphs each with maximum cardinality of 15, 25 and 35 nodes using probo’s SCC generator. The maximum number of SCCs in each graph was set to 2. Each dataset was divided into 10 sets of 100 graphs with probability \(p=0.1\), \(p=0.2\), ..., \(p=1\) of a node attacking another within an SCC. We submitted the 3,000 graphs thus generated to the solvers running on a PC with an Intel i7 4690 K processor and 32 Gb RAM. The left of Fig. 8 shows the comparative average time per graph successfully solved by each solver and the right shows the percentage of instances timed out within 180 s.

The graphs turned out to be rather too small to effectively stress test EqArgSolver using our algorithm. However, they clearly show the differences in performance between the two algorithms (and Tweetysolver). Both the version of EqArgSolver using our algorithm as well as Tweetysolver successfully solved all graphs submitted within the time limit. As expected, the version using Modgil-Caminada’s algorithm timed out more frequently the more nodes the datasets contained. For graphs with up to 15 nodes, it timed out in roughly \(10\%\) of the problems, increasing to \(40\%\) of timeouts in graphs with up to 25 nodes; and then to \(70\%\) timeouts in graphs with up to 35 nodes. The actual average time per graph successfully solved varied rather erratically in the version using Modgil-Caminada’s algorithm and this deserves further investigation. Our algorithm was clearly the fastest (just above 0 ms per graph on average). The execution times for Tweetysolver stayed relatively constant at around 1,000–1,250 ms per graph in all datasets. This shows some advancements in catching up with SAT reduction approaches.Footnote 7

Fig. 8.
figure 8

Average execution time and % of time-outs for graphs with up to 15, 25 and 35 nodes.

6 Conclusions and Future Work

It is well known that the computation of grounded extensions is simply a matter of propagation of the \(\mathbf {in}\) labels of unattacked arguments, which can be done very efficiently using the Discrete Gabbay-Rodrigues Iteration Schema [10]. In this paper we proposed a novel algorithm for the computation of all other complete extensions by looking for solutions to the SCCs of an argumentation framework. With minor modifications the algorithm can be used for the preferred and stable semantics as well.

The motivation for the development of this algorithm came from the following. In the solver GRIS [14], we used Modgil-Caminada’s algorithm to compute the preferred extensions of an argumentation framework. However, Modgil-Caminada’s algorithm proved very inefficient for all but the simplest graphs and can only compute the preferred extensions. We wanted a more efficient algorithm that could compute all complete extensions and that could also check argument acceptability without necessarily having to generate all extensions. The algorithm here proposed achieves all that and successfully replaced Modgil-Caminada’s algorithm in the solver EqArgSolver, which we submitted to the 2nd ICCMA (see http://argumentationcompetition.org/).

Given that solvers using reduction-based approaches to the computation of argumentation semantics took the top spots in the 1st ICCMA, the reader might ask if the development of direct algorithms and tools for argumentation semantics is worthwhile or whether we should simply concentrate on improving the reduction-based techniques. We would side with Cerutti et al.’s to argue that both approaches have a role to play [7] and combining them could be advantageous. In addition, we would claim that direct approaches are the only alternative in applications for which a translation to logic is either not possible at all or very cumbersome, e.g., in certain numerical argumentation networks.

We tested the new algorithm over tens of thousands of graphs of cardinality of up to 100,000 nodes. Rather than the number of nodes in the framework as a whole, it is the complexity and the number of SCCs involved that can stress a solver using the algorithm. Although some of these characteristics are unavoidable and intrinsic to the problem, the complexity could be reduced in our algorithm by avoiding multiple generation of the same solution arising in different search branches. As it stands, we attempt to label \(\mathbf {in}\) every candidate argument in an SCC in order to guarantee the completeness of the set of solutions found, but this could be improved. Optimisations in this area are under investigation.

A further point to make is that within an SCC we can start the algorithm at an argument of interest to aid in decision problems of argument acceptability. It should also be possible to work backwards from a specific argument to see if an extension containing it can be constructed. This is work in progress.

Finally, each \(\mathbf {in}\) labelling of a node forces the arguments that it attacks to be labelled \(\mathbf {out}\), which means that in each non-trivial SCC, each forward propagation reduces the complexity of the original problem by at least two arguments, but possibly many more in cases where the seed node attacks multiple arguments. We therefore expect the probability of attacks between nodes within an SCC to be inversely proportional to the execution time of our algorithm. This needs to be fully demonstrated and we also want to compare the performance of our algorithm with Nofal et al.’s [13] which, as for Modgil-Caminada’s algorithm, can only generate the preferred extensions.