In this paper we introduce AASExts, an algorithm for computing admissible argumentation stage extensions-a.k.a. semi-stable extensions. Admissible argumentation stage extensions play a decisive role in unifying two lines of research in formal argumentation: admissible-based extensions as suggested by Dung in his seminar paper; and the traditional approach based on dialectical evaluation of the defeat status of arguments. In this paper, we improve techniques developed for other semantics, notably preferred semantics, as well as leverage-for the first time-recent advances in All-SAT community. We prove our proposed algorithm is sound and complete, and we show empirically that our implementation significantly outperforms even sophisticated ASP-based and SAT-based reduction approaches on existing benchmarks.
Research based on Dung’s model of argumentation [
However, as noted by Rescher [25] among others, dialectical argumentation has
two main characteristics. On the one side, arguments in favour of a conclusion can be
challenged by other (counter)arguments. On the other side, the acceptability status of an
argument—or of its conclusion—depends on the stage of the argumentation process, i.e.
the process of supporting or opposing arguments. Following this intuition, the
acceptability status of an argument can be either undefeated or defeated [29]. Any argument
attacked by an undefeated argument should be defeated, and any defeated argument
must be attacked by at least one undefeated argument: this idea will then be re-named
as labelling [
Copyright c 2020 for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
An argumentation stage [29], then, is a set of arguments whose acceptability status
is either undefeated or defeated w.r.t. to the conditions above. Arguments whose
acceptability status is neither undefeated nor defeated do not belong to such a stage. This
naturally leads to a notion of argumentation stage extension as a maximum—w.r.t. set
inclusion—argumentation stage. However, as shown in [30], this notion of
argumentation stage does not guarantee the admissibility property proposed by Dung [
To unify these two lines of research, Verheij [30] proposed the notion of
admissible argumentation stage extension as an argumentation stage with an admissible set of
undefeated arguments: this notion will be then re-named as semi–stable extension [
Wallner et al. [31] proposed SSTMCS, an algorithm for computing admissible stage
extensions exploiting algorithms for computing minimal correction sets (MCS) [20, 21],
i.e. subset-minimal sets of clauses of a formula. argmat-sat [24] reimplemented a very
similar idea and scored first during the 2017 edition of the International Competition
on Computational Models of Argumentation. An alternative system, Aspartix [
In this paper, we improve recent advancements in exploiting SAT solvers as
NPoracles [
In order to adhere to the current terminological standards [
ArgSemSAT. 6 http://argumentationcompetition.org/2017/index.html https://github.com/federicocerutti/
An argumentation framework [
Definition 1. An argumentation framework (AF ) is a pair xA; Ry where A is a set of arguments and R A A.
an argument a will be denoted as a tb : b Ñ au, the set of arguments attacked by a will be denoted as a tb : a Ñ bu.
Db P E s.t. b Ñ a; a Ñ E iff Db P E s.t. a Ñ b; E Ñ S iff Db P E; a P S s.t. b Ñ a; E tb | Da P E; b Ñ au and E tb | Da P E; a Ñ bu.
Each argumentation framework has an associated directed graph where the vertices are the arguments, and the edges are the attacks.
The basic properties of conflict–freeness, acceptability, and admissibility of a set of arguments are fundamental for the definition of argumentation semantics. Definition 2. Given an AF
xA; Ry: – a set S A is a conflict–free set of if E a; b P S s.t. a Ñ b; – an argument a P A is acceptable with respect to a set S A of
b Ñ a, D c P S s.t. c Ñ b; – the function F : 2A Ñ 2A such that F pSq
called the characteristic function of ; – a set S A is an admissible set of if S is a conflict–free set of element of S is acceptable with respect to S, i.e. S F pSq.
and every ta | a is acceptable w.r.t. Su is
An argumentation semantics prescribes for any AF a set of extensions, denoted as E p q, namely a set of sets of arguments satisfying the conditions dictated by . Here we need to recall the definitions of stable (denoted as ST), preferred (denoted as PR), and admissible argumentation stage or semi–stable (denoted as SST) semantics. Definition 3. Given an AF
xA; Ry: – a set S A is a stable extension of , i.e. S P ESTp q, iff S is a conflict-free set of and S Y S A; – a set S A is a preferred extension of , i.e. S P EPRp q, iff S is a maximal (w.r.t.
set inclusion) admissible set of ; – a set S A is a semi–stable extension of , i.e. S P ESSTp q, iff S is an admissible set where S Y S (i.e. its range) is maximal (w.r.t. set inclusion).
It is immediate to see that if a stable extension exists, the semi–stable extensions
coincide with the stable extensions.
7 In this paper we consider only finite sets of arguments: see Baroni et al. [
xA; Ry, if ESTp q
Proof. Immediate from Definitions 2 and 3.
The notion of complete extension has been introduced as an auxiliary definition
[
Each extension S implicitly defines a three-valued labelling of arguments, or
dialectical evaluation: an argument a is labelled in (undefeated [29]) iff a P S; is labelled
out (defeated [29]) iff D b P S s.t. b Ñ a; is labelled undec if neither of the above
conditions holds. In the light of this correspondence, argumentation semantics can be
equivalently defined in terms of labellings rather than of extensions [
xA; Ry, a labelling of is a labelling of A. The set of all labellings of is denoted as Lp q.
Given a labelling Lab, it is possible to write inpLabq for tA|LabpAq outpLabq for tA|LabpAq outu and undecpLabq for tA|LabpAq undecu.
Complete labellings can be defined as follows. inu,
– Labpaq – Labpaq – Labpaq out; in; in ^ Dc P a : Labpcq undec.
The stable, preferred, and semi–stable labelling can then be defined on the basis of complete labellings.
Lp q is – a stable labelling
labelled undec; – a preferred labelling of
arguments labelled in; – a semi–stable labelling of arguments labelled undec; xA; Ry be an argumentation framework. A labelling Lab P if it is a complete labelling of
and there is no argument if it is a complete labelling of
maximising the set of if it is a complete labelling of minimising the set of
In order to show the connection between extensions and labellings, let us recall
the definition of the function Ext2Lab,[
Definition 7. Given an AF xA; Ry and a conflict–free set S A, the corresponding labelling Ext2LabpSq is defined as Ext2LabpSq Lab, where – Labpaq
in ô a P S – Labpaq – Labpaq out ô D b P S s.t. b Ñ a undec ô a R S ^ E b P S s.t. b Ñ a
Caminada [
semi–stable) labelling of if and only if there is a complete (stable, preferred, semi– stable) extension S of such that Lab Ext2LabpSq.
Proof. See Baroni et al. [
A propositional formula over a set of boolean variables is satisfiable iff there exists
a truth assignment of the variables such that the formula evaluates to True. Checking
whether such an assignment exists is the satisfiability (SAT) problem. Following Cerutti
et al. [
We reuse the same encoding that Cerutti et al. [
Oaq^ p Ia _
Uaq ^ p
Oa _
Uaq Ia ^
Oa ^
Ua © aPA ^ ^ ^ ^ ^ © aPA © © aPA
© ta | a ©
Hu © aPA tb | bÑau aPA tb | bÑau
Oa _ © Ua _
Ia _ Ob ª tb | bÑau
Ib Ua _
Ib ª tb | bÑau
Ub Labpaq ^ Dc P a encodes in CNF the conditions Labpaq in ñ @b P a Labpbq out; out ñ Db P a : Labpbq in; Labpaq undec ñ @b P a Labpbq in : Labpcq undec; together with the requirement of it being a total function.
Overview of AASExts In this section we introduce AASExts, our proposal for computing semi–stable extensions. To this aim, let us first consider the following intermediate theoretical results.
Firstly, to strictly expand the range of a complete extension—in order to minimise the set of undecided arguments given a complete labelling Lab—it is necessary to transform a label from undec into in or out. However, no constraints should be imposed on the arguments labelled either in or out in Lab. Those arguments are free to change their labels, provided that they do not become undec.
plete labelling.
@Lab1 P Lp q such that undecpLabq undecpLab1q Da P A such that Labpaq undec and Lab1paq tin; outu, and Eb P A such that Labpbq undec and Lab1pbq undec.
xA; Ry be an argumentation framework and Lab P Lp q a comProof. Immediate from Definition 5.
Secondly, given the freedom of argument labelled in or out to swap their labels mentioned above, there might be multiple semi–stable labellings having the same set of undec arguments: they differ on the basis of the labels of the remaining arguments labelled either in or out.
stable labelling.
tLab1|Lab1 is complete and undecpLab1q undecpLabqu.
xA; Ry be an argumentation framework and Lab P Lp q a semi– undecpLabqu Proof. First, semi–stable labellings are complete by Definition 6. On the other hand, given a complete labelling Lab1 such that undecpLab1q undecpLabq, undecpLab1q is minimal since Lab is semi–stable, thus Lab1 is semi–stable.
AASExts resorts to several external functions: STExts, SS, I A, U A, and ALLSS. STExts is an algorithm for computing stable extensions. For the sake of completeness, Algorithm 1 shows a straightforward implementation of STExts: all the complete labellings with no undec arguments are enumerated at line 2 and their in arguments form stable extensions, cf. Definitions 6 and 7, and Proposition 2.
SS is a SAT solver—in this paper we used MiniSAT [
ALLSS is a solver for the All-SAT problem: in this paper we used the proposal illustrated in [34]. The All-SAT problem [22] deals with determining all the satisfying assignments that exist for a given propositional logic formula. A typical All-SAT solver is based on iteratively computing satisfying assignments using a traditional Boolean satisfiability (SAT) solver and adding blocking clauses which are the complement of the total/partial assignments.
xA; Ry
Output: ESTp q 2A 1: ESTp q :
H 2: for each st P ALLSS 3: ESTp q : 4: end for 5: return ESTp q
aPA ESTp q Y tI Apstqu ^
Ua
do
AASExts is presented in Algorithm 2. At first it checks whether stable extensions exist (l. 1–4): in that case ESTp q ESSTp q (Proposition 1).
Otherwise, it enforces a disjunctive clause to find at least one argument labelled in (l. 5) and then (l. 9–16) it starts the process to find a complete labelling with minimal set of undec arguments (Lemma 1), i.e. a semi–stable labelling.
Then it enumerates (l. 19–23) all the semi–stable labellings that share the same set of undec arguments (Lemma 2) before searching for a new semi–stable labelling with a different set of undec arguments (Definition 6).
xA; Ry be an argumentation framework: AASExtsp q ESSTp q.
Proof ((Sketched due to space constraints)). The proof is analogous to [11, Theorem 2],
and it builds on top of Proposition 1, Lemmas 1 and 2, and Definition 6. From
Proposition 1, if stable extensions exist, they also are semi–stable. Otherwise, a CEGAR-like
[
To illustrate the algorithm, let us consider the following example evolving the one introduced by Verheij [30].
Example 1. Let 1 xA1; R1y where A1 ta; b; c; d; e; fu and R1 txa; by; xb; ay; xa; cy; xc; dy; xd; ey; xe; cy; xf; fyu.
With reference to Example 1—depicted in Figure 1—let us suppose at l. 10 of Algorithm 2 the compl assignment identified is such that the corresponding labelling Labcompl xinpLabcomplq; outpLabcomplq; undecpLabcomplqy xtbu; tau; tc; d; e; fuy. Then l. 13 of Algorithm 1 enforces that arguments in inpLabcomplq Y outpLabcomplq ta; bu can be labelled either in or out; and l. 14 requires that at least one argument belonging to undecpLabcomplq tc; d; e; fu should be labelled either in or out.
During the second execution of the loop (l. 9–16), at l. 10 the only compl1 assignment that satisfies the additional constraints is such that Labcompl1 xta; du; tb; c; eu; tfuy. Similarly as above, Algorithm 2 tries to label f either in or out, but at the third execution of the loop (l. 9–16) there is no further assignment able to satisfy such an additional constraint, therefore the loop is exited with sstcand compl1 a variable assignment equivalent to a semi-stable labelling.
It is worth noticing that ESTp 1q H because f is self-defeating and it is isolated from the rest of the framework, therefore in this case ESSTp 1q ESTp 1q. However, if we restrict 1 to the set of arguments ta; b; c; d; eu, i.e. we ignore f and its self-defeating attack, then the stable and semi–stable extensions would coincide.
Finally, it also worth noticing that ESSTp 1q EPRp 1q. Indeed, there is another maximal admissible set of arguments, namely tbu, i.e. a second preferred extension. However, its range—tb; au—is not maximal. 4
Evaluation of AASExts In this section, we present the result of a large experimental analysis comparing the performance of AASExts with respect to state-of-the-art approaches, on sets of differentlyshaped AF s.
We implemented AASExts in C++. As per SS, we relied on MiniSAT [
We randomly generated 2,500 AF s based on five different graph models:
BarabasiAlbert [
Erdo¨s-Re´nyi graphs [
Input: xA; Ry
Output: ESSTp q 2A 1: ESSTp q : STExtspxA; Ryq 2: if ESSTp q H then 3: return ESSTp q 4: end if 5: ocnf : ^ Ia
aPA 25: end if 26: until (sstcand 27: if ESSTp q 28: ESSTp q 29: end if 30: return ESSTp q
H) H then tHu scale-free power-law distribution. This is generally the case when: (i) networks expand continuously by the addition of new nodes, and (ii) new nodes attach preferentially to sites that are already well connected. Moreover, Watts and Strogatz [32] show that many biological, technological and social networks are neither completely regular nor completely random, but something in the between. They thus explored simple models of networks that can be tuned through this middle ground: regular networks rewired to introduce increasing amounts of disorder. These systems can be highly clustered, like regular lattices, yet have small characteristic path lengths, like random graphs, and they are named small-world networks by analogy with the small-world phenomenon.
The AF s have been generated by using AFBenchGen2 [
The fourth set has been generated using the code provided in Probo [
In our experimental analysis we considered SSTMCS [31] and Aspartix [
Experiments have been run on a cluster with computing nodes equipped with 2.5 Ghz Intel Core 2 Quad Processors, 4 GB of RAM and Linux operating system. A cutoff of 600 seconds was imposed to compute the extensions for each AF similarly to what chosen in ICCMA 17. For each solver we recorded the overall result: success (if it solved the considered problem), crashed, timed-out or ran out of memory. Unsuccessful runs—crashed, timed-out or out of memory—were assigned a runtime equal to the cutoff.
Performance are measured in terms of IPC score and Penalised Average Runtime. The IPC score, borrowed from the planning community and exploited in recent editions of the International Planning Competition [28],10 is defined as follows. For a solvers S and an AF a, scorepS; aq is defined as: scorepS; aq $ 0 &
1 % 1 log10p TTaapSq q otherwise if a is not successfully analysed where TapSq is the CPU time needed by a solver S to successfully analyse the AF a and Ta is the CPU-time needed by the best considered solver, otherwise. The total IPC score is the sum the scores achieved on each considered AF . Runtimes below 1.0 sec get by default the maximal score of 1.
The Penalised Average Runtime (PAR score) is a real number calculated by counting (i) runs that fail to solve the considered problem as ten times the cutoff time (PAR10) 8 http://argumentationcompetition.org/2015/results.html 9 https://helios.hud.ac.uk/scommv/storage/SemiStable2017 10 http://www.icaps-conference.org/index.php/Main/Competitions and (ii) runs that succeed as the actual runtime. PAR scores are commonly used in automated algorithm configuration, algorithm selection, and portfolio construction, [19] because using them allows runtime to be considered while still placing a strong emphasis on high instance set coverage.
In the following we rely on the Wilcoxon Signed-Rank Test (WSRT) in order to identify significant subsets of data [33]. The Wilcoxon Signed-Rank test is used for comparing performance in terms of PAR10 of two solvers. From this perspective, “no correlation” between the observed results indicates that it is equally like that, given an AF from the considered set of benchmarks, one solver provides a solution faster than the second solver, than the vice-versa. For the purposes of this analysis, the Wilcoxon sign-rank test is appropriate because it does not require any knowledge about the sample distribution, and makes no assumption about the distribution. In our analysis we considered that the null-hypothesis, i.e. the performance of compared solvers is statistically similar, is accepted when p-value ¡ 0:05. Otherwise, the null-hypothesis is rejected, and therefore the compared solvers performance is statistically different. 4.2
Table 1 shows the performance, in terms of PAR10, coverage and IPC score, of the considered approaches on the different testing sets.
Firstly, for each testing set, the performance of the solver that achieved the best PAR10 score are always statistically better than those of the other considered solvers.
Secondly, leaving aside the benchmarks of Barabasi—discussed in the following—
AASExts shows outstanding performance. This is specially the case of Erdo¨s-Re´nyi
and Watts-Strogatz benchmarks, where the current state-of-the-art approaches often—
if not always—fail to provide an answer in the given time. This seems consistent with
some problems highlighted by Cerutti et al. [
The case of Barabasi-Albert benchmarks shows the main weakness of AASExts, namely the maximisation process where labels are left free to float between in and out. Figure 2 depicts a (small) example of an AF that would belong to the BarabasiAlbert benchmark—the actual benchmarks are composed of hundreds of arguments, Figure 2 is for illustration purpose only. Given the large occurrence of cycles in such a structure, AASExts will spend a substantial amount of time within the inner loop (cf. Algorithm 2 l. 9–16) seeking for a maximal range, especially if the first assignment from SS (cf. Algorithm 2 l. 10) contains a large set of undec arguments. A way to mitigate this situation is to hack the MiniSAT code in order to prioritise a specific set of variables, i.e. injecting in MiniSAT the knowledge that it should search towards a maximal range. It is of little surprise that SSTMCS results to be the best solver in this case since it exploits efficient techniques for computing minimal correction sets (MCS) [20, 21] that are subset-minimal sets of clauses of a formula, thus solving the dual problem of maximising the range, namely to minimise the set of undec arguments.
Lastly, the similarities of the results between SemiStableM and StableM suggest that the introduction of the self-defeating argument for enforcing the absence of stable extensions—cf. Example 1 and Figure 1—has no significant impact on solvers’ performance. AASExts performs slightly better—according to the IPC metric—on the StableM domain no doubt because a large of benchmark instances (61%) have a stable extension, and thus it can fully exploit the All-SAT solver.
However, it is interesting to note that the coverage is slightly higher in the case of SemiStableM. If an AF in StableM has a stable extension, AASExts will compute the semi-stable extensions by using STExts. However, the AF in SemiStableM, derived from the previous one by adding a self-defeating argument, will not have a stable extension and thus AASExts cannot exploits STExts. In 0.2% of AF s in SemiStableM, the a16 a22 a9 a18 a13 a7 a23 a14 a5 a15 a2 a12
a8 a19 a21 a0 a4 a17 a1 a25 procedure in AASExts identifies semi-stable extensions before the cut-off time, while it fails when searching for stable extensions in the corresponding original AF in StableM. We will investigate further this behaviour to identify the reasons those relatively rare cases are potentially problematic for the All-SAT solver exploited by STExts. 5
In this paper we introduced AASExts, an efficient algorithm for computing admissible argumentation stage extensions, a.k.a. semi-stable extensions, in abstract argumentation. We proved its correctness and we demonstrated its performance against existing approaches in literature, and overall this approach scored second at the ICCMA 2017 for the semi-stable semantics track. Moreover, to our knowledge, this is the first approach exploiting results from the All-SAT research to solve abstract argumentation problems.
An experimental analysis conducted on a large number of AF s based on five different graph models, has shown that: (i) AASExts is generally able to deliver better performance than existing state-of-the-art approaches; (ii) the main weakness of AASExts comes from its maximisation process, that can hardly cope with cases in which labels keep floating between in and out values, as in the Barabasi-Albert set, and (iii) the introduction of self-defeating arguments for enforcing the absence of stable extensions has no significant impact on considered solvers’ performance.
As part of future work, we aim at deriving an efficient algorithm for computing (non-admissible) argumentation stage extensions, as well as for the skeptical/credulous acceptance of arguments. Moreover, we believe that it is the right time to start computing semantics evaluation considering the inner argument structure, therefore we will look at structured argumentation and how to identify argumentation stages, as well as other Dung’s related semantics, possibly without the need of first deriving a Dung’s argumentation framework as an intermediate system of representation. 18. Gaggl, S.A., Linsbichler, T., Maratea, M., Woltran, S.: Design and results of the second international competition on computational models of argumentation. Artificial Intelligence 279, 103193 (2020). https://doi.org/https://doi.org/10.1016/j.artint.2019.103193 19. Hoos, H.H.: Automated algorithm configuration and parameter tuning. In: Autonomous search, pp. 37–71. Springer (2012) 20. Liffiton, M.H., Sakallah, K.A.: Algorithms for Computing Minimal Unsatisfiable Subsets of
Constraints. Journal of Automated Reasoning 40(1), 1–33 (sep 2007) 21. Marques-Silva, J., Heras, F., Janota, M., Previti, A., Belov, A.: On computing minimal correction subsets. In: Proceedings of the Twenty-Third international joint conference on Artificial Intelligence. pp. 615–622. AAAI Press (2013) 22. McMillan, K.: Applying SAT Methods in Unbounded Symbolic Model Checking. In: Proc.
CAV. pp. 303–323. CAV ’02, Springer-Verlag, London, UK, UK (2002) 23. Niemela¨, I.: Logic programs with stable model semantics as a constraint programming paradigm. Annals of Mathematics and Artificial Intelligence 25, 241–273 (1999) 24. Pu, F., Ya, H., Luo, G.: argmat-sat: Applying SAT Solvers for Argumentation Problems based on Boolean Matrix Algebra. http://argumentationcompetition.org/2017/ argmat-sat.pdf (2017) 25. Rescher, N.: Dialectics: A controversy-oriented approach to the theory of knowledge. Suny
Press (1977) 26. Thimm, M., Villata, S., Cerutti, F., Oren, N., Strass, H., Vallati, M.: Summary Report of The First International Competition on Computational Models of Argumentation. AI Magazine (2016) 27. Thimm, M., Villata, S., Cerutti, F., Oren, N., Strass, H., Vallati, M.: Summary report of the first international competition on computational models of argumentation. AI Magazine 37(1), 102 (2016) 28. Vallati, M., Chrpa, L., Grzes, M., McCluskey, T.L., Roberts, M., Sanner, S.: The 2014 international planning competition: Progress and trends. AI Magazine 36(3), 90–98 (2015) 29. Verheij, B.: The influence of defeated arguments in defeasible argumentation. In: WOCFAI.
vol. 95, pp. 429–440. Citeseer (1995) 30. Verheij, B.: Two approaches to dialectical argumentation:admissible sets and argumentation stages. In: Meyer, J.J., van der Gaag, L.C. (eds.) Proceedings of the Eighth Dutch Conference on Artificial Intelligence (NAIC’96). pp. 357–368. Utrecht, NL (1996) 31. Wallner, J.P., Weissenbacher, G., Woltran, S.: Advanced sat techniques for abstract argumentation. In: Proceedings of the 14th International Workshop on Computational Logic in Multi-Agent Systems. pp. 138–154 (2013) 32. Watts, D.J., Strogatz, S.H.: Collective dynamics of ’small-world’ networks. Nature 393(6684), 440–442 (1998) 33. Wilcoxon, F.: Individual comparisons by ranking methods. Biometrics Bulletin 1(6), 80–83 (1945) 34. Yu, Y., Subramanyan, P., Tsiskaridze, N., Malik, S.: All-SAT Using Minimal Blocking Clauses. In: 2014 27th International Conference on VLSI Design and 2014 13th International Conference on Embedded Systems. pp. 86–91. IEEE (jan 2014). https://doi.org/10.1109/VLSID.2014.22