A ConArg-based Library for Abstract Argumentation‹ Stefano Bistarelli, Fabio Rossi, Francesco Santini Department of Mathematics and Computer Science, Italy [bista,rossi,francesco.santini]@dmi.unipg.it Abstract. We present ConArgLib, a C++ library implemented to help programmers solve some of the most important problems related to extension-based Abstract Argumentation. The library is based on ConArg, which exploits Constraint Programming and, in particular, Gecode, a toolkit for developing constraint-based systems and applications. Given a semantics, such problems consist, for example, in enumerating all the extensions, and checking the credulous or sceptical acceptance of an argu- ment passed as parameter. The goal is to let programmers use the library to quickly develop programs on top of it, as, for instance, implementing decision-making procedures based on the strongest arguments. 1 Introduction We present ConArgLib, a C++ library implemented to help programmers solve some intractable problems related to extension-based Abstract Argumentation [12]. The library is based on a revised search engine developed for ConArg [3], a stand-alone solver submitted to ICCMA15 [19] and (in its revised version) to ICCMA17 1 , that is the International Competition on Computational Models of Argumentation. The search engine exploits Gecode 2 , a toolkit for developing constraint-based systems and applications. An Abstract Argumentation Framework (AAF ) is simply a pair xArgs , Ry consisting of a set Args whose elements are called arguments, and of a bi- nary relation R on Args , called “attack” relation. For example, the framework xta, b, cu, tRpa, bq, Rpb, cquy has three arguments labelled as a, b, and c, and there is an attack between a and b, and b and c. A framework can be simply represented as a directed graph, where nodes are arguments, and edges model attacks. The sets of arguments (or extensions [12]) to be considered are then defined under different semantics, which represent different degrees of scepticism. Most of them are based on both the notion of conflict-freedom (extensions must not contain attacks), and the notion of defence: in the previous AAF, b attacks c, but a defends c since it attacks b. ‹ Research supported by project “Argumentation 360” (funded by Dept. of Mathemat- ics and Computer Science, University of Perugia), and project “REMIX” (funded by Banca d’Italia and Fondazione Cassa di Risparmio di Perugia). 1 http://www.dbai.tuwien.ac.at/iccma17/. 2 http://www.gecode.org. Recent years have seen researchers drawing their attention on computational aspects of Abstract Argumentation; in particular, on tools that are capable to solve classical problems, as, given a semantics, i) the enumeration of extensions satisfying it, ii) the verification whether a subset of arguments satisfies it, iii) and iv) the sceptical and credulous acceptance of an argument (if an argument belongs to resp. all or at least one of the extensions), v) the existence of at least one extension, and finally vi) the non-emptiness of at least one extension, i.e., if different from H. In addition to AAFs [12], ConArgLib also solves a weighted extension of them we present in [2, 6]: semiring-based Weighted Abstract Argumentation Frame- works (simply WAAFs in the following), where attacks are associated with a value (taken an algebraic structure, i.e., a c-semiring [5]) representing e.g., a strength score or an uncertainty degree. Then, in [2] we study two different re- laxations of WAAFs: the first one is related to the new weighted defence we propose in [6], by checking the difference between the composition of inward and outward attack-weights. The second one is related to how much inconsistency we are willing to tolerate inside an extension; such an amount is computed by aggregating the weights of the attacks between any two arguments inside an extension. These relaxations are correlated: allowing a small conflict may lead to have more arguments into an extension, and consequently result in a stronger or weaker defence. To code the library we take advantage of Constraint Programming (CP) [18] since the problems i-vi can be intractable [11], depending on the semantics. Despite the plethora of aforementioned solvers, as far as we know, ConArgLib represents the first attempt to provide a fast implementation of a library to sup- port the solution of problems in Abstract Argumentation. The end programmer can use it to directly develop her own applications, instead of interfacing to an external solver: as an example, solving the existence of a non-empty extension, and the credulous/sceptical acceptance of arguments can be used to set-up a decision-making procedure by ranking the arguments, and then to select the decision supported by the strongest ones. The paper is organised as follows: in Sec. 2 we provide the necessary back- ground on Dung’s AAFs [12], and c-semirings [5], i.e., the general algebraic structure we use to parametrise weights in WAAFs in [2, 6], whose presentation concludes this section. In Sec. 3 we provide a description of ConArgLib. Then, in Sec. 4 we report some implementation details to explain the engine of the library. Finally, in Sec. 5 we wrap up the paper with general conclusions and ideas about future work. 2 Background This section is structured in three parts: first we collect the main background notions about AAFs [12] (Sec. 2.1), then we introduce c-semirings (Sec. 2.2), and finally semiring-based WAAFs (Sec. 2.3). 2.1 Abstract Argumentation Frameworks In his pioneering work [12], Dung proposed Abstract Frameworks for Argumen- tation, where an argument is an abstract entity whose role is solely determined by its relations to other arguments: Definition 1 (Argumentation Frameworks [12]). An Abstract Argumen- tation Framework (AAF) is a pair xArgs , Ry of a set Args of arguments and a binary relation R on Args , called attack relation. @ai , aj P Args , ai R aj (or Rpai , aj q) means that ai attacks aj (R is asymmetric). An argumentation semantics is the formal definition of a method (either declarative or procedural) ruling the argument evaluation process. In the exten- sion-based approach, a semantics definition specifies how to derive from an AAF a set of extensions, where an extension B of an AAF xArgs , Ry is simply a subset of Args . In Def. 2 we define the first semantics, which is at the basis of all the others: Definition 2 (Conflict-free [12]). A set B Ď Args is conflict-free iff no two arguments a and b in B exist such that a attacks b. All the other semantics presented in this section rely (explicitly or implicitly) upon the concept of defence: Definition 3 (Defence [12]). An argument c is defended by a set B Ď Args (or B defends b) iff for any argument a P Args , if Rpa, cq then Db P B s.t., Rpb, aq. An admissible set of arguments according to Dung must be a conflict-free set which defends all its elements. Formally: Definition 4 (Admissible [12]). A conflict-free set B Ď Args is an admissible set iff each argument in B is defended by B. The following four definitions elaborate on conflict-freedom and admissibility: Definition 5 (Complete [12]). An admissible set B Ď Args is a complete extension iff each argument which is defended by B is in B. Definition 6 (Preferred [12]). A preferred extension is a maximal (w.r.t. set inclusion) admissible set of Args . The definition of stage [20] and semi-stable [10] semantics is based on the idea of prescribing the maximisation not only of the arguments included in an extension (as for the preferred extension), but also of those attacked by it: Definition 7 (Stage [20] and semi-stable [10]). Given a set B Ď Args , the range of B is defined as B Y B ` , where B ` “ ta P Args : B attacks au. B is a stage extension iff is a conflict-free set with maximal (wrt. set inclusion) range. B is semi-stable extension iff B is a complete extension with maximal (w.r.t. set inclusion) range. a b c d e Fig. 1. An example of AAF. Finally, the stable semantics corresponds to the most stringent among all: Definition 8 (Stable [12]). A conflict-free set B Ď Args is a stable extension iff for each argument which is not in B, there exists an argument in B that attacks it. The last three semantics, i.e., the grounded [12], ideal [13], and eager [9], enforce a sceptical approach: these semantics that always yields exactly one extension. Definition 9 (Grounded [12]). The grounded extension is the minimal (w.r.t. set inclusion) complete extension [12]. Definition 10 (Ideal [13]). B Ď Args is ideal iff B is admissible and @B 1 s.t. B 1 is preferred, B Ď B 1 . The ideal extension is the maximal (w.r.t. set inclusion) ideal set. Definition 11 (Eager [9]). B Ď Args is eager iff B is admissible and @B 1 s.t. B 1 is semi-stable, B Ď B 1 . The eager extension is the maximal (w.r.t. set inclusion) eager set. If σ P tcf , adm, com, prf , sst, stg, stbu respectively stand for conflict-free and admissible sets, complete, preferred, semi-stable, stage, and stable semantics, and ξσ pF q is the set of all the extensions satisfying σ on a framework F , then we have ξstb pF q Ď ξsst pF q Ď ξprf pF q Ď ξcom pF q Ď ξadm pF q Ď ξcf pF q, and ξstb pF q Ď ξstg pF q Ď ξcf pF q. Moreover, if grd, ide, and eag are respectively the grounded, ideal, and eager extension, then we have that grd Ď ide Ď eag [9]. Consider the AAF F “ xA, Ry in Fig. 1, with A “ ta, b, c, d, eu and R “ tpa, bq, pc, bq, pc, dq, pd, cq, pd, eq, pe, equ. For example we have that ξadm pF q corre- sponds to tH, tau, tcu, tdu, ta, cu, ta, duu, ξcom pF q “ ttau, ta, cu, ta, duu, ξstb pF q “ tta, cu, ta, duu, ξstb pF q “ tta, duu, and ξgrd “ ttauu. 2.2 C-semirings C-semirings [5] are commutative (b is commutative) and idempotent semirings (i.e., ‘ is idempotent), where ‘ defines a complete lattice: every subset of ele- ments have a least upper bound, or lub, and a greatest lower bound, or glb. Definition 12 (C-semirings [5]). A commutative semiring is a tuple S “ xS, ‘, b, K, Jy such that S is a set, J, K P S, and ‘, b : S ˆ S ÝÑ S are binary operators making the triples xS, ‘, Ky and xS, b, Jy commutative monoids (semi-groups with identity), satisfying i) @s, t, u P S.s b pt ‘ uq “ ps b tq ‘ ps b uq (distributivity), and ii) @s P S.sbK “ K (annihilator). If @s, t P S.s‘psbtq “ s, S is said to be absorptive, and consequently ‘ is idempotent. In short, c-semirings are defined as commutative and absorptive semirings. The idempotency of ‘ leads to the definition of a partial ordering ďS over the set S (S is a poset). Such partial order is defined as s ďS t if and only if s ‘ t “ t, and ‘ returns the lub of s and t. This intuitively means that t is “better” than s. Some more properties can be derived on c-semirings [5]: i) both ‘ and b are monotone over ďS , ii) b is intensive (i.e., s b t ďS s), and iii) xS, ďS y is a complete lattice. K and J are respectively the bottom and top elements of such lattice. When also b is idempotent, i) ‘ distributes over b, ii) b returns the glb of two values in S, and iii) xS, ďS y is a distributive lattice. Some well-known instances of c-semirings in the literature are: Sboolean “ xtfalse, trueu, _, ^, false, truey3 , Sfuzzy “ xr0, 1s, max, min, 0, 1y, Sbottleneck “ xR` Y t`8u, max, min, 0, 8y, Sprobabilistic “ xr0, 1s, max, ˆ, 0, 1y (or Viterbi semiring), Sweighted “ xR` Y t`8u, min, `, `8, 0y. Although c-semirings have been historically used as monotonic structures, the need of removing values has raised in local consistency algorithms [2]. A solution comes from residuation theory [8], which allows for obtaining a division operator that represents a “weak” inverse of b. Definition 13 (Division). A c-semiring S is residuated if the set tx P S | t b x ď su admits a maximum for all elements s, t P S, denoted s m t. Since a complete4 tropical-semiring is also residuated, we have that all the classical instances of c-semiring presented above are residuated, i.e., each element in S admits an “inverse”, which can be also unique: Definition 14 (Unique invertibility). If S is absorptive and invertible, then it is uniquely invertible iff it is cancellative, i.e., @s, t, u P S.psbu “ tbuq^pu ‰ 0q ñ s “ t. Since all the previously listed instances of c-semirings are cancellative, they are uniquely invertible as well. For instance, # 0 if b ě a mintx | b ` x ě au “ weighted a ´ b if a ą b # 1 if b ď a maxtx | minpb, xq ď au “ fuzzy a if a ă b 3 Boolean c-semirings can be used to model crisp problems and classical Argumenta- tion [12]. 4 S is complete if it is closed with respect to infinite sums, and the distributivity law holds also for an infinite number of summands. 2.3 Semiring-based Weighted AAFs In the beginning of this section we rephrase some of the classical definitions given in Sec. 2.1, with the purpose of parametrising them with the notion of weighted attack and c-semiring. The following definition reshapes the notion of WAAF into semiring-based WAAF [2], called WAAF S : Definition 15 (Semiring-based WAAF). A semiring-based Weighted AAF (WAAF S ) is a quadruple xArgs , R, W, Sy, where S is a c-semiring xS, ‘, b, K, Jy, Args is a set of arguments, R the attack binary-relation on Args , and W : Args ˆ Args ÝÑ S is a binary function. Given a, b P Args and Rpa, bq, then W pa, bq “ s means that a attacks b with a weight s P S. Moreover, we require that Rpa, bq iff W pa, bq ăS J. In Fig. 2 we provide an example of a weighted interaction graph describing the WAAF S defined by Args “ ta, b, c, d, eu, R “ tpa, bq, pc, bq, pc, dq, pd, cq, pd, eq, pe, equ, with W pa, bq “ 7, W pc, bq “ 8, W pc, dq “ 9, W pd, cq “ 8, W pd, eq “ 5, W pe, eq “ 6, and S “ xR` Y t8u, min, `, 8, 0y (i.e., the weighted semiring). Therefore, each attack is associated with a semiring value that represents the “strength” of an attack between two arguments. We can consider the weights in Fig. 2 as supports to the associated attack, as similarly suggested in [14]. A semiring value equal to the top element of the c-semiring J represents a no-attack relation between two arguments. In Def. 16 we define the attack strength for a set of arguments that attacks an argument, a different set of arguments, or an argument that attacks a set of arguments; Â the former and the latter are what we need to define w-defence. We use to indicate the set-wise version of b: Definition 16 (Attacks to/from sets of arguments). Given a WAAF S , WF “ xArgs , R, W, Sy, – a set of arguments â B attacks an argument a with a weight of k P S if W pB, aq “ W pb, aq “ k. bPB – an argumentâa attacks a set of arguments B with a weight of k P S if W pa, Bq “ W pa, bq “ k. bPB â B attacks a set of arguments D with a weight k P S if – a set of arguments W pB, Dq “ W pb, dq “ k. bPB,dPD 8 7 8 5 a b c d e 6 9 Fig. 2. An example of WAAF, adding weights to Fig. 1. For example, looking at Fig. 2 we have that W pta, cu, bq “ 15, W pc, tb, duq “ 17, and W pta, cu, tb, duq “ 24. We are now ready to define our version of weighted defence, i.e., w-defence: Definition 17 (w-defence (Dw ) [6]). Given a WAAF S , WF “ xArgs , R, W, Sy, B Ď Args w-defends b P Args from a P Args s.t. Rpa, bq, iff W pa, B Y tbuq ěS W pB, aq; B w-defends b iff it defends b from any a s.t. Rpa, bq. Definition 17 can be relaxed to γ-defence, which is parametrised on a threshold- value γ: such γ is used to consider arguments that are not “fully” w-defended [6], i.e., for which W pa, B Y tbuq ğS W pB, aq: Definition 18 (γ-defence (Dγ ) [2]). Given xArgs , R, W, S “ xS, ‘, b, K, Jyy and γ P S, B Ď Args γ-defends b P Args iff @a P Args such that Rpa, bq we have that W pB, aq ‰ J and ´ ¯ W pa, B Y tbuq m W pB, aq ěS γ Considering the example in Fig. 2, for instance tdu 1-defends d from c (i.e., γ “ 1): ´ ¯ W pc, tduq ´ W ptdu, cq ď 1, since 9 ´ 8 “ 1 and 1 ď 1. Having defined Dγ as a relaxation of Dw , we can redefine all the classical semantics in Sec. 2.1 by exploiting both the notion of i) an inconsistency amount α inside an extension (to be tolerated), and ii) Dγ . In Def. 19 we redefine conflict-free sets: conflicts can be now part of the solution up to a cost-threshold α. They are now called α-conflict-free sets: Definition 19. (α-conflict-free sets) Given a WAAF S , WF “ xArgs , R, W, Sy, a set of arguments B Ď Args is α-conflict-free iff W pB, Bq ěS α. With respect to the WAAF S in Fig. 2, while the set ta, b, cu is not conflict-free in the crisp version of the problem (since it includes the attacks between a and b, and between c and b), ta, b, cu is instead 15-conflict-free because W pa, bq ` W pc, bq “ 15. For instance, ta, b, cu is also 16-conflict-free because it is a 15- conflict-free (15 ěS 16 in the weighted semiring).5 Therefore, in α-conflict-free extensions we tolerate an internal inconsistency-amount better than α. Dγ leads to the definition of αγ -admissible sets. Definition 20. (αγ -admissible sets) Given WF “ xArgs , R, W, Sy, an α- conflict-free set B Ď Args is αγ -admissible iff the arguments in B are γ-defended by B from the arguments in Args zB. 5 In the weighted semiring, ďS is equivalent to ě over Real numbers, while in the probabilistic and fuzzy semirings, ěS corresponds to ě over Real numbers in the interval r0..1s. For instance, the set td, eu in Fig. 2 is 111 -admissible, since it is 11-conflict- free, and d defends itself (and the whole td, eu) from c by paying a penalty of 9 ´ 8 ď 1. Four semantics that refine αγ -admissibility are introduced from Def. 21 to Def. 23: Definition 21 (αγ -complete). Given xArgs , R, W, Sy, an αγ -admissible B Ď Args is αγ -complete iff each argument b P Args that is γ-defended by B and s.t. W pB Y tbu, B Y tbuq ěS α is in B (i.e., b P B). For instance, the set ta, du in Fig. 2 is complete according to [12] (i.e., not considering weights), but it is not 00 -complete because d is not able to w-defend ta, du from c. However, ta, du is 01 -complete by considering the weighted semiring and allowing γ “ 1. Note that ta, du also 1-defends argument e, but ta, d, eu is not 01 -complete if we keep α “ 0: bringing e inside would lead to an internal conflict of W pd, eq ` W pe, eq “ 11. Definition 22 (αγ -preferred). An αγ -preferred extension is a maximal (with respect to set inclusion) αγ -admissible subset of Args . Still considering Fig. 2, ta, cu and ta, du are the two preferred extensions according to [12] (i.e., not considering weights). However, ta, cu is the only 00 - preferred extension, while tta, cu, ta, duu is the set of 01 -preferred extensions. Finally, we define αγ -stable semantics. Definition 23. (αγ -stable semantics) Given xArgs , R, W, Sy, an αγ -admissible set B is also an αγ -stable extension iff @a R B, Db P B.W pb, aq ‰ J, and B Y tau is not αγ -admissible. For example, considering the problem in Fig. 2 as unweighted (i.e., as a classical AAF), the set ta, du corresponds to the only stable extension. However, considering weights, this set is not 00 -stable, because W pc, dq ğS W pta, du, cq, i.e., 9 ę 8. However, it is 01 -stable, since W pc, dq m W pta, du, cq “ 9 ´ 8 ď 1 satisfies γ “ 1. Thus, in such example there is no 00 -stable extension. When α “ J and γ “ J, JJ -semantics are equivalent to their classic coun- terpart in Sec. 2.1 [2]. 3 The Library ConArgLib is available for Linux 64bit platform, and it has been compiled with gcc 4.9.2 and glibc 2.19 (using Debian 8). The pre-compiled package is freely available online.6 ConArgLib sits on the layer offered by Gecode 5.1.0, which implements the search engine. Given a semantics σ, and the set of extensions ξσ pF q that satisfy σ over a framework F , the decision problems solved by ConAr- gLib are: 6 http://www.dmi.unipg.it/conarg/. Enumeration. Given F “ xArgs , Ry and a semantics σ, this problem consists in enumerating all B P ξσ pF q. Credulous Acceptance. Given F “ xArgs , Ry, a semantics σ, and an argu- ment a P Args , a is credulously accepted if DB P ξσ pF q, a P B. Sceptical Acceptance. Given F “ xArgs , Ry, a semantics σ, and an argument a P Args , a is sceptically accepted if @B P ξσ pF q, a P B. Verification. Given F “ xArgs , Ry, a semantics σ, and a subset of arguments B, the verification of B consists in checking if B P ξσ pF q. Existence. Given F “ xArgs , Ry and a semantics σ, this problem corresponds to checking whether ξσ pF q ‰ H. Non-emptiness. Given F “ xArgs , Ry and a semantics σ, this problem corre- sponds to checking whether there is any B P ξσ pF q for which B ‰ H. The complexity of extension enumeration is reported in [17]. The complexity of the other previouslt presented problems, e.g., credulous/sceptical acceptance, can be instead found in [11], [16], and [15]. We now introduce the functions we can use to solve each of the six problems previously introduced. Besides “Admissible”, each of the four following functions can also be called by replacing it with “ConflictFree”, “Complete”, “Preferred”, “SemiStable”, “Stable”, “Grounded”, “Ideal”, “Stage”, and “Eager”; hence the library implements all the classical semantics in Sec. 2.1: s e t ∗ GetAdmissibleEnum ( ) ; s t r i n g GetAdmissibleCred ( s t r i n g &sArg ) ; s t r i n g G e t A d m i s s i b l e S c e p t ( s t r i n g &sArg ) ; b o o l I s A d m i s s i b l e ( v e c t o r &vecExtToCheck ) ; s e t ∗ G e t A d m i s s i b l e E x i s t ( ) ; s e t ∗ NonEmptinessAdmissible ( ) ; In addition, other functions have been coded to solve the relaxed framework presented in [2, 6]. It is then possible to pass as input parameters the chosen semiring (see in the following for implemented ones), the amount of internal re- laxation (dAlpha), and the amount of relaxation on the defence (dGamma). All the following functions are presented for the admissible semantics, but by re- placing “Admissible” sub-strings with “ConflictFree”, “Complete”, “Preferred”, “Stable”, or “Grounded”, it is possible to find a solution for the corresponding semantics (all the semantics in Sec. 2.3): s e t ∗ GetAdmissibleEnum ( double dAlpha , double dGamma) ; s e t ∗ G e t A d m i s s i b l e E x i s t ( double dAlpha , double dGamma) ; s t r i n g GetAdmissibleCred ( s t r i n g &sArg , double dAlpha , double dGamma) ; s t r i n g G e t A d m i s s i b l e S c e p t ( s t r i n g &sArg , double dAlpha , double dGamma) ; bool I s A d m i s s i b l e ( v e c t o r &vecExtToCheck , double dAlpha , double dGamma) ; s e t ∗ NonEmptinessAdmissible ( double dAlpha , double dGamma) ; The following semirings are at the moment defined and implemented in ConArgLib: xtfalse, trueu, _, ^, false, xr0, 1s, max, min, 0, 1y, and xR` Y t`8u, min, `, `8, 0y. #define CL SRTYPE BOOLEAN 0 #define CL SRTYPE FUZZY 1 #define CL SRTYPE WEIGHTED 2 The following calls are instead used to manage the library: bool L o a d F i l e ( s t r i n g &sInputFileName ) ; void P r i n t S o l ( s e t ∗ p s e t S o l ) ; void F r e e S o l ( s e t ∗ p s e t S o l ) ; bool E n g i n e I s I n i t i a l i z e d ( ) ; i n t G e t S o l u t i o n s C o u n t ( s e t ∗ p s e t S o l ) ; double GetFuzzyBestValue ( ) ; double GetFuzzyWorstValue ( ) ; double GetWeightedBestValue ( ) ; double GetWeightedWorstValue ( ) ; LoadFile is used to load the description of an AAF by passing a file path. For classical AAFs we use ASPARTIX format (apx ), which corresponds to a text file with a list of arguments, expressed as “arg(argumentName).”, and a list of attacks between them, e.g., “att(argument1Name, argumentName2).”. To represent WAAFs as proposed in Sec. 2.3, we have modified the apx format into wapx : the list of arguments is expressed in the same way, while attacks are associated with a score, i.e., att(argumentName1, argumentName2):-score. PrintSol is used to print all the solutions: hence, it is meaningful for the enumeration, existence, and non-emptiness problems. FreeSol deallocates the passed set of solutions from dynamic memory. EngineIsInitialized checks if the search engine has been correctly ini- tialised; for instance, it checks whether a semiring type has been already selected. GetSolutionsCount returns the number of solutions for the last solved problem (it is meaningful in case of enumeration). GetFuzzyBestValue and GetFuzzyWorstValue can be used by the pro- grammer to respectively retrieve the top and bottom elements in fuzzy semiring (see Sec. 2.2). The same holds for GetWeightedBestValue and GetWeight- edWorstValue, w.r.t. the weighted semiring. The following group of functions collects the functionalities to configure how solutions are found and printed. SetShowSolutions sets if the set of solutions is printed on the screen or silenced, besides being saved in memory. SetRequestedSolutions stops the search as soon as a given number (input parameter) of solutions is found, while SetRequestedAllSolutions returns all the found solutions (these functions are meaningful only for the enumeration problem). SetStatistics prints the search statistics obtained from Gecode: specifically, it returns the number of failed nodes in search tree, the number of nodes ex- panded, the maximum depth during search, the number of restarts, and, finally, the number of posted no-goods. SetProboOutput sets the output of requested problems to be compliant with Probo 7 , which is the benchmark framework used for computational argu- mentation competitions (i.e., ICCMA15 and ICCMA17). SetPercentOutput also prints the rate of appearance (as percentage) of each argument in the current solutions. It can be used in combination with solving the enumeration problem over any semantics, in order to understand the degree of acceptability of each argument. SetSilentMode trims part of the output, e.g., removes messages concerning the kind of problem being solved. All these function are also replicated with “Get” instead of “Set” in order to know how parameters are currently set. Finally, ResetDefaults restores them to the initial values (e.g., output is not silenced by default). void S e t S h o w S o l u t i o n s ( bool bFlag ) ; void S e t R e q u e s t e d S o l u t i o n s ( long lRS ) ; void SetRequestedAllSolutions () ; void S e t S t a t i s t i c s ( bool b S t a t ) ; void SetProboOutput ( bool bProbo ) ; void SetPercentOutput ( bool b P e r c e n t ) ; void S e t S i l e n t M o d e ( bool bSilentMode ) ; void Se tS how So lut io ns C ou nt ( bool bShowSolutionsCount ) ; bool GetShowSolutions ( ) ; long GetRequestedSolutions () ; bool GetStatistics () ; bool GetProboOutput ( ) ; bool GetPercentOutput ( ) ; bool GetSilentMode ( ) ; void ResetDefaults () ; An example of a program using ConArgLib is shown in Fig. 3: the code finds all the admissible sets and prints them on the screen. The example in Fig. 4 shows instead how to verify that the set ta, du is a 01 -stable extension (see Def. 23) according to the weighted semiring. 4 Implementation Details In this section we overview some technical details of the search engine, that is how we have implemented constraints and heuristics. Gecode supports the devel- opment of new constraints, branching strategies, and search engines. Constraints can be defined over Integers, Booleans, Sets, and Floats. In the following, args[] is the array of Boolean variables (i.e., instances of the class BoolVar ) that rep- resents the whole set of arguments Args ; Boolean variables can only take 0 or 1 values (i.e., two integer values). An array of Boolean variables can be cre- ated with BoolVarArray args[](space, |Args |, 0, 1), where space is the associated search-space. 7 https://sourceforge.net/projects/probo/. #i n c l u d e ”AFEngine . h” AFEngine ∗ a f = new AFEngine ( ) ; s t r i n g sFileName1 = ” f i l e . apx ” ; a f ´>L o a d F i l e ( sFileName1 ) ; s e t ∗ t s e t S o l = a f ´>GetAdmissibleEnum ( ) ; a f ´>P r i n t S o l ( t s e t S o l ) ; c o u t << a f ´>G e t S o l u t i o n s C o u n t ( t s e t S o l ) << ” s o l u t i o n ( s ) found ” << e n d l ; a f ´>F r e e S o l ( t s e t S o l ) ; Fig. 3. An example of a small program created by using ConArgLib. Function decla- rations are imported from AFEngine.h. Then a new engine is created, and a frame- work is imported from file. This piece of code finds and prints all the admissible sets in that framework. The output printed on the screen for the example in Fig. 1 is rrcs, ra, cs, ra, d s, rd s, rs, rass 6 solution(s) found. #i n c l u d e ”AFEngine . h” AFEngine ∗ a f = new AFEngine ( ) ; s t r i n g sFileName2 = ” f i l e . wapx” ; a f ´>L o a d F i l e ( sFileName ) ; v e c t o r vecArgs ; vecArgs . push back ( ” a ” ) ; vecArgs . push back ( ”d” ) ; a f ´>SetSemiringType (CL SRTYPE WEIGHTED) ; i f ( a f ´>I s S t a b l e ( vecArgs , 0 , 1 ) ) c o u t << ” {a , d} i s a s t a b l e e x t e n s i o n ” ; else c o u t << ” {a , d} i s not a s t a b l e e x t e n s i o n ” ; Fig. 4. A piece of code that verifies if ta, du is a 01 -stable extension, using the weighted semiring; the answer is positive on the example in Fig. 1. Constraints for modelling conflict-free-sets are based on the first order logic formula @a, b P Aarg s.t. Rpa, bq, then a ñ b (ąą is the implication operator in Gecode): r e l ( space , a r g s [ i ] >> ! a r g s [ j ] ) The procedure to enforce the constraints for modelling admissibility first sets conflict-free constraints, and then checks if at least one defender (c) of each attacker (b) of Ž i.e., taken in an extension together with a: @a, b, c P Aarg Źa is true, then a ñ p cq. In this case, we deal with two different cases: when pb,aqPR pc,bqPR an argument args[i] is attacked but has no defender, then it has not to be taken (IRT EQ imposes equality, with 0 in this case): r e l ( space , a r g s [ i ] , IRT EQ , 0 , IPL SPEED ) Otherwise, if an argument has at least one defender, then we use the clause constraint, where c is a Boolvar array that represents all the arguments ci Ž that defend a from each attacker b, and such a clause constraints models a _ ci ci Pc c l a u s e ( space , BOT AND, a , c , 0 ) IPL SPEED is a Gecode flag set to optimise propagation for execution per- formance, at the expense of memory use. Constraints for stable extensions are obtained by imposing Ź admissible con- straints and enforcing the formula @a P Args , then a ô b. This is mod- pb,aqPR elled as r e l ( space , m bvaArgs [ i ] , IRT EQ , 1 ) in case args[i] is never attacked (then it has to be taken). Otherwise, if args[i] has one or more attackers the constraint is l i n e a r ( space , a , x , IRT GR , 0 ) ; Given a “ rargsris, b1 , . . . , bn s, where bi , . . . bn are the n attackers of args[i], the previous constraint enforces argsris ` x1 ¨ b1 ` ¨ ¨ ¨ ` xn ¨ bn ą 0; in this case, x is a vector of weights all set to 1 (with size n ` 1). Hence, either an argument a or at least one of its attackers bi have to be true. We now introduce how we enumerate and verify preferred extensions. First of all, we set the constraints to find admissible sets, including constraints for conflict-freedom. Afterwards, we use the following branching strategy: branch ( space , a r g s , INT VAR DEGREE MAX( ) , INT VALUES MAX( ) ) ; During search, at each step such a strategy selects the variable with the highest degree (i.e., the number of dependant propagators) and tries to assign it to true. This last condition automatically leads to finding a preferred extension: Proposition 1 (Branching for preferred). By imposing only constraints to find admissible sets, a branching strategy INT VALUES MAX always terminates with a preferred extension. This approach incrementally builds an extension by adding as more (“admis- sible”) arguments as possible: eventually, it is not possible to find an admissible set that includes it. In order to enumerate all preferred extensions, it is enough to i) launch the search using Prop. 1, ii) record the obtained solution, iii) remove it from the set of possible future solutions, and iv) restart search. The i-iv loop is terminated when no further solution is found. To verify if a given set B is a preferred exten- sion, we set admissible constraints, and then we use Prop. 1 by first assigning to true all the arguments in B. As soon as we find a solution different from B, then we obtain that B is not a preferred extension. 4.1 Constraints for WAAFs Constraints for WAAFs in Sec. 2.3 are similar to the ones proposed in this section for classical Abstract Argumentation [12]: in addition, we add some more constraints to limit the internal inconsistency and the difference between attack and defence weights to be less than resp. α and γ. In the following piece of code, the first constraint binds extensionCost to the aggregation (parametric w.r.t. the chosen semiring) of the weights of all attacks “active” in the considered set of arguments. Then, still depending on the semiring, such a value is compared against α: r e l ( space , e x t e n s i o n C o s t == s e m i r i n g T i m e s O p e r a t i o n ( activeAttacks ) ) ; i f ( m s t r u c t ´>GetSemiringType ( ) == WEIGHTED) r e l ( space , e x t e n s i o n C o s t , FRT LQ, a l p h a ) ; i f ( m s t r u c t ´>GetSemiringType ( ) == FUZZY) r e l ( space , e x t e n s i o n C o s t , FRT GQ, a l p h a ) ; Concerning γ-defence (see Def. 18), the ˆ of all the attackers (A) and de- fenders (B) of an argument is computed and compared against γ. Expr posts a Boolean expression and returns its value, which is then checked to be true: expr ( space , SemiringXAIsGammaWorseEqualThanXB (B, A) ) ; i f ( m s t r u c t ´>GetSemiringType ( ) == WEIGHTED) expr ( space , ( SemiringXOperation (B) ´ SemiringXOperation (A) ) <= gamma) ; i f ( m s t r u c t ´>GetSemiringType ( ) == FUZZY) expr ( space , ( SemiringXOperation (B) ´ SemiringXOperation (A) ) >= gamma) ; 5 Conclusion We have presented ConArgLib, a C++ software library designed to offer to the end user functions to solve classical tasks in Abstract Argumentation: extension enumeration, existence, and verification, and credulous/sceptical acceptance of arguments. The engine at the core of the library offers good performance, and is the first attempt to provide such functionalities as a software library. In the future, we plan to extend the library by providing higher-level func- tions, e.g., to check if two frameworks are equivalent on some given semantics. Moreover, we would like to implement a recent different definition of grounded semantics for semiring-based WAAFs [7], which, contrarily to all the other pro- posals in the literature for Weighted Argumentation Frameworks, always returns one extension as result, as in the classical formulation [12]. Finally, we will im- plement coalition-based extensions [4] and voting systems as in [1]. References 1. Benedetti, I., Bistarelli, S.: From argumentation frameworks to voting systems and back. Fundam. Inform. 150(1), 25–48 (2017) 2. Bistarelli, S., Rossi, F., Santini, F.: A relaxation of internal conflict and defence in weighted argumentation frameworks. In: European Conference on Logics in Arti- ficial Intelligence, JELIA. LNCS, vol. 10021, pp. 127–143. Springer (2016) 3. Bistarelli, S., Santini, F.: Conarg: A constraint-based computational framework for argumentation systems. In: International Conference on Tools with Artificial Intelligence. pp. 605–612. ICTAI ’11, IEEE Computer Society (2011) 4. Bistarelli, S., Santini, F.: Coalitions of arguments: An approach with constraint programming. Fundamenta Informaticae 124(4), 383–401 (2013) 5. Bistarelli, S., Montanari, U., Rossi, F.: Semiring-based constraint satisfaction and optimization. Journal of the ACM 44(2), 201–236 (1997) 6. Bistarelli, S., Rossi, F., Santini, F.: A collective defence against grouped attacks for weighted abstract argumentation frameworks. In: Florida Artificial Intelligence Research Society Conference, FLAIRS. pp. 638–643. AAAI Press (2016) 7. Bistarelli, S., Santini, F.: A Hasse diagram for weighted sceptical semantics with a unique-status grounded semantics. In: Logic Programming and Nonmonotonic Reasoning, LPNMR. LNCS, vol. 10377, pp. 49–56. Springer (2017) 8. Blyth, T.S., Janowitz, M.F.: Residuation theory, vol. 102. Pergamon press Oxford (1972) 9. Caminada, M.: Comparing two unique extension semantics for formal argumen- tation: ideal and eager. In: Belgian-Dutch conference on artificial intelligence (BNAIC). pp. 81–87 (2007) 10. Caminada, M.: Semi-stable semantics. In: Computational Models of Argument: Proceedings of COMMA 2006. Frontiers in Artificial Intelligence and Applications, vol. 144, pp. 121–130. IOS Press (2006) 11. Charwat, G., Dvořák, W., Gaggl, S.A., Wallner, J.P., Woltran, S.: Methods for solving reasoning problems in abstract argumentation: A survey. Artificial Intelli- gence 220(0), 28 – 63 (2015) 12. Dung, P.M.: On the acceptability of arguments and its fundamental role in non- monotonic reasoning, logic programming and n-person games. Artificial Intelligence 77(2), 321–357 (1995) 13. Dung, P.M., Mancarella, P., Toni, F.: A dialectic procedure for sceptical, assumption-based argumentation. In: Proceedings of the 2006 conference on Com- putational Models of Argument (COMMA). pp. 145–156. IOS Press (2006) 14. Dunne, P.E., Hunter, A., McBurney, P., Parsons, S., Wooldridge, M.: Weighted ar- gument systems: Basic definitions, algorithms, and complexity results. Artif. Intell. 175(2), 457–486 (2011) 15. Dunne, P.E.: The computational complexity of ideal semantics. Artif. Intell. 173(18), 1559–1591 (2009) 16. Dvorák, W.: Computational Aspects of Abstract Argumentation. Ph.D. thesis, Technische Universität Wien (2012), http://permalink.obvsg.at/AC07812708 17. Kröll, M., Pichler, R., Woltran, S.: On the complexity of enumerating the exten- sions of abstract argumentation frameworks. In: International Joint Conference on Artificial Intelligence, IJCAI. pp. 1145–1152. ijcai.org (2017) 18. Rossi, F., van Beek, P., Walsh, T.: Handbook of Constraint Programming. Elsevier Science Inc., New York, NY, USA (2006) 19. Thimm, M., Villata, S., Cerutti, F., Oren, N., Strass, H., Vallati, M.: Summary report of the first international competition on computational models of argumen- tation. AI Magazine 37(1), 102 (2016) 20. Verheij, B.: Two approaches to dialectical argumentation: admissible sets and ar- gumentation stages. Dutch Conference on Artificial Intelligence 96, 357–368 (1996)