The third and fourth international competitions on computational models of argumentation: Design, results and analysis

2.1.Abstract argumentation

An Abstract Argumentation Framework (AF, for short) [30] is a tuple F=(A,→) where A is a set of arguments and → is a relation →⊆A×A. For two arguments a,b∈A, the relation a→b means that argument a attacks argument b. An argument a∈A is defended by S⊆A (in F) if for each b∈A such that b→a there is some c∈S such that c→b. A set E⊆A is conflict-free (in F) if and only if there are no a,b∈E with a→b. E is admissible (in F) if and only if it is conflict-free and each a∈E is defended by E. Finally, the range of E in F, i.e., E⊕, collects the same E and the set of arguments attacked by E: E⊕=E∪{a∈A|∃b∈E:b→a}. A directed graph can straightforwardly represent an AF: an example with five arguments is given in Fig. 1 (e.g., both arguments a and c attack b, but not vice-versa).

Fig. 1.

An example of an AF represented as a directed graph.

The collective acceptability of arguments depends on the definition of different semantics. Four of them are proposed by Dung in his seminal paper [30], namely the complete (CO), preferred (PR), stable (ST), and grounded (GR) semantics. In addition, other semantics have been defined in the literature that we also use for the competition: in particular, the semi-stable (SST) [25], stage (STG) [77], and ideal (ID) [31]. Semantics determine sets of jointly acceptable arguments, called extensions, by mapping each F=(A,→) to a set σ(F)⊆2A, where 2A is the power set of A, and σ parametrically stands for any of the considered semantics. The extensions under complete, preferred, stable, semi-stable, stage, grounded, and ideal semantics are defined as follows. Given F=(A,→) and a set E⊆A,

For a more detailed view of these semantics, please refer to [11]. Note that grounded and ideal extensions are uniquely determined and always exist [30,31]. Thus, they are also called single-status semantics. The other semantics introduced are multi-status semantics, where several extensions may exist. The stable semantics is the only case where an AF might possess no extension at all.

We report the definition of eight well-known problems in Abstract Argumentation, where the first six are decision problems:

Computational argumentation tools enable formalizing complex problems and understanding real-world situations where conflicting information must be considered to draw non-trivial conclusions. For example, verifying the acceptance of arguments and enumerating extensions is used in applications such as planning [67] and decision support [26]. For an in-depth discussion of the complexity results for the problems mentioned above, we refer to [32] and, in particular, to [51] for enumeration problems and [12,39] for counting problems.

2.2.Motivations to dynamic frameworks

In previous ICCMA editions, all the frameworks in each data set are static since all the AFs are sequentially passed as input to solvers, representing different and independent problem instances. Hence, all tasks are computed from scratch without taking any potentially useful knowledge from previous runs into account. However, AFs can be considered in practical applications as a temporary situation, which evolves when new knowledge becomes available that requires the addition or retraction of arguments and attacks. For example, users of online social networks [48] may engage in disputes and repeatedly add or retract arguments and attacks to express their point of view in response to the last move made by their adversaries in the ongoing digital conversation. Users often disclose as few arguments/attacks as possible in these situations. For this reason, ICCMA’19 also features additional tracks to evaluate solvers on dynamic Dung’s frameworks. The aim is to test those solvers dedicated to efficiently recomputing a solution after a minor change in the original AF. In this case, a problem instance consists of an initial framework (as for classical tracks) and an additional file storing a sequence of additions/deletions of attacks (between already existing arguments) on the initial framework, i.e. a list of modifications. This file has a simple text format, i.e. a sequence of +att(a,b) (attack addition) or −att(d,e) (attack deletion). The final single output must report the solution for the initial framework and each change. The dynamics of frameworks have attracted recent and broad interest in the computational argumentation community. We describe some related work, pointing to the research groups interested in organizing such a track.

In [23], the authors investigate the principles in which a grounded extension of a Dung’s AF does not change when the set of arguments/attacks is changed. The authors of [28] study how the extensions can evolve when a new argument is considered. The focus is on adding a single argument interacting with a non-attacked argument. Several properties are defined for the change operations according to how the extensions are modified. For instance, a change operation can be conservative if the set of extensions is the same after a change. The work in [27] addresses the problem of revising AFs when a new argument is added. In particular, the authors focus on the impact of new arguments on the set of initial extensions, introducing various kinds of revision operators that have different effects on the semantics. For instance, a decisive revision allows for making a decision by providing a revised extensions’ set with a unique non-empty extension. The authors of [13] propose a division-based method to divide the updated framework into two parts: “affected” and “unaffected”. Only the status of affected arguments is recomputed after updates. A matrix-reduction approach similar to the previous division method is presented in [79]. In [2], the authors compute complete, preferred, stable, and grounded semantics on an AF, given a set of updates. This approach finds a reduced (updated) AF sufficient to compute an extension of the whole AF and uses state-of-the-art algorithms to recompute an extension of the reduced AF only. In [3], the same authors extend their dynamic techniques to improve the skeptical acceptance of arguments in preferred extensions.

Modifications of AFs are also studied in the literature as a base to compute robustness measures of frameworks [22,59,64]. In particular, by adding/removing an argument/attack, the set of extensions satisfying a given semantics may or may not change. For instance, one could be interested in computing the number of modifications needed to change this set or measure the number of modifications needed to have a different set of extensions satisfying a desired semantics. In the latter case, the user is interested in estimating how distant two different points of view are. A similar approach has also been proposed in [14], where the problem of revising argumentation frameworks according to the acquisition of new knowledge is taken into account. While attacks among the old arguments remain unchanged, new arguments and attacks among them can be added. In particular, the authors introduce the notion of enforcing, namely the process of modifying an AF (and possibly changing its semantics) to obtain a desired set of extensions.

Since in ICCMA’19, the inclusion of a dynamic track was launched for the first time; the changes have been limited to only attacks (that could be added or removed), which is an essential modification one can perform on an AF. Indeed, the dynamic challenge fostered some research, which was one of the motivations for the proposed dynamic challenge. See for instance [1,3,4,62].

2.3.Motivations to approximate algorithms

Generally speaking, approximate algorithms are methods that can compute the solution to a problem faster than what exact algorithms can normally perform, but with a risk of providing an incorrect solution in some cases. This kind of approach had already been studied in the argumentation community before the organization of ICCMA 2021 [52,60,74]. Although not always correct, these algorithms can be highly necessary in situations where exact algorithms (e.g., SAT-based techniques) cannot solve the problem, or at least not fast enough to satisfy the needs of the users (e.g. if the argumentation framework is too large and the user expects a quick answer).

In the first organization of an approximate track at ICCMA, the focus was on the simplest problems related to the acceptability (credulous or skeptical) of arguments from the point of view of the nature of the answer, not from the point of view of complexity (see Section 3.2). However, some interesting ideas could be implemented for future ICCMA competitions, as discussed in Section 9.2.

3.1.Tracks and tasks at ICCMA’19

ICCMA’19 let solvers participate in 7 classical tracks, the same as in ICCMA’17. Each track is named after the name of a semantics (CO, PR, ST, SST, STG, GR, and ID). Then, tasks are characterized by a problem and the semantics for which the problem is solved. In ICCMA’19, the following well-known problems are considered:

For single-status semantics (GR and ID) the problem EE is equivalent to SE, and DS is equivalent to DC. Also, note that the DC problem returns the same results when computed for CO and PR, but to allow participation in the PR track without implementing tasks on the CO semantics (or vice versa), both the two tasks were maintained. The tasks selected in ICCMA’19 were:

The combination of problems with semantics amounts to 24 tasks overall. In addition, 4 new tracks were dedicated to the solution of problems over dynamic frameworks, this time using the semantics originally proposed in [30]: σ∈{CO,PR,ST,GR}. In this case, a problem instance consists of an initial framework and an additional file storing a sequence of additions/deletions of attacks (see Section 4 for more details). The dynamics tasks adopted in the competition are:

In this case, the combination of problems with semantics amounts to a total of 14 tasks. Tasks in dynamic tracks are invoked by appending “D” to the end of the intended task: for instance, EE-PR-D denotes the enumeration task with the preferred semantics. In total, ICCMA’19 is composed of 11 tracks that collect 38 different tasks. Each participating solver can compete in an arbitrary set of tasks. If a solver supports all track’s tasks (e.g. the track on complete semantics), it also automatically participates in the corresponding track.

3.2.Tracks and tasks at ICCMA’21

The first difference between ICCMA’19 and ICCMA’21 is the removal of the grounded semantics (GR) from the competition since it is not considered a challenging issue (recall that computing the grounded extension can be done linearly with respect to the number of arguments). Then, the competition was divided into two “main” tracks, one for exact algorithms and the other for approximate algorithms. In the exact track, the EE task was replaced with a counting task:

The second track, dedicated to approximate algorithms, has 6 sub-tracks corresponding to the semantics. In this case, the focus is on decision problems. Therefore, the approximate track of ICCMA’21 consists of the following tasks:

4.1.Input format

Each benchmark instance, that is, each AF, is represented in two different file formats: trivial graph format (tgf) and aspartix format (apx), both used in previous editions of ICCMA. tgf88 is a simple text-based adjacency list file format for describing graphs. The format consists of a list of node labels and a # character followed by a list of edges, which specify node pairs and an optional edge label. For example, 12#12 represents a framework with two arguments and an attack from the first to the second one. The apx format is described in [37]. This format is more oriented to computational argumentation problems, but the encoded information is, in practice, very similar to tgf, even if arguments and attacks are always associated with a specific label. The previous example with arguments named a and b corresponds to “arg(a). arg(b). att(a,b).”.

A novel format for dynamic AFs is introduced. For each (dynamic) problem instance, two files are required: the initial framework (either in apx or tgf format) and a text file with a list of changes to apply. The file with changes declares a list of modifications (one per line) of the initial framework. The file format with changes is inspired by the original tgf and apx formats. The format used for modifications is illustrated in the example below.

Example 4.1.

The initial framework of Fig. 1 is provided in a file myExample.apx with the following content:

arg(a).
arg(b).
arg(c).
arg(d).
arg(e).
att(a,b).
att(c,b).
att(c,d).
att(d,c).
att(d,e).

The second file contains the list of modifications to be sequentially performed on the initial AF. The name of this file has to be the same as the first one but with a different extension .apxm instead of .apx. In this example, myExample.apxm is:

+att(b,c).
-att(a,b).
+att(e,d).

Applying these changes to the initial file produces three frameworks, represented in Fig. 2.

Fig. 2.

The three AFs obtained from the modifications in myExample.apxm.

A second example shows the same framework in the tgf format.

Example 4.2.

Example 4.1 is considered using the tgf format. The file with modifications needs to have suffix .tgfm. Hence, the same changes are represented in myExample.tgfm:

+2 3
-1 2
+5 4

We obtain the three additional frameworks as shown in Fig. 3.

Fig. 3.

The three AFs obtained from the modifications in myExample.tgfm.

To generate the problem instances for the new tracks, a subset of the frameworks used in classical tracks was selected. A sequence of modifications was produced for each of the selected frameworks, where attacks were added only between existing arguments. No new argument was introduced during this process. Further details can be found in Section 5.3. For a modification file with n changes, a solver must compute solutions for n different frameworks by applying the modifications in sequence (starting at the top of the file).

4.2.Output format

The output format of ICCMA’17 has been retained, except for the EE task. The printed standard output for the DC and DS tasks was either YES or NO. For the SE task, the list of arguments belonging to the returned extension is encoded as, e.g., [a1,a2,a4]. For EE, the list of extensions is returned as illustrated in the example in Fig. 4. Solutions for CE (introduced in ICCMA’21) are simply the number of extensions printed on the standard output. Non-existence of solutions (e.g. in case of ST) was encoded by [], while an empty extension is simply described as [[]].

Fig. 4.

We here show the output format of both EE and SE-D tasks. In this specific example, the output corresponds to the result of the EE-PR task on the AF in Fig. 1.

For the dynamic tracks, all answers were output in the form of a list where the first element represents the solution of the required task on the initial framework; each following element in this list is the answer returned for the (i+1)th framework that incorporates the first i changes in the modification file, with i∈[1..n] and n being the total number of changes in the modification file. DC-σ-D and DS-σ-D tasks returned a list of YES or NO, one for each modification including the initial framework; for example [YES,YES,NO]. The SE-σ-D tasks required a list as shown in Fig. 4: one extension found for each modification. The EE-D tasks needed one more level of indentation, i.e. Fig. 4 repeated for every modification and with one more pair of delimiting square parentheses, since a set of extensions needed to be returned for each modification.

5.1.Participants at ICCMA’19

For the third edition, the competition received 9 solver submissions from research groups in Austria, Finland, France, Germany, Italy, Romania, and the UK. Table 2 lists the solvers, related participants, and affiliations. Table 3 shows the tasks all the solvers participated in: 3 solvers were submitted to all the tracks, including dynamic ones. The authors of the solvers used different techniques to implement their applications. In particular, 4 solvers were based on transforming argumentation problems to SAT, 1 on the transformation to ASP, 1 relied on machine learning, and 3 were built on tailor-made algorithms. Following the alphabetical order, we provide a summary of each solver and refer the reader to the official abstract for a more detailed discussion.99

Argpref is a solver specialized in computing the ideal semantics. It implements a SAT-with-preferences approach to computing the backbone of a propositional encoding of admissible sets. Then, it applies polynomial-time post-processing to construct the ideal extension. Insights into the techniques used for the implementation are provided in [66].

An early version of Aspartix-V19 (simply Aspartix in the following) participated in ICCMA’15 and also was the reference solver in ICCMA’17. ASPARTIX delegates the main reasoning to an answer set programming (ASP) solver with argumentation semantics and reasoning tasks encoded via ASP rules. We refer to [35] for details on the version submitted to ICCMA’19.

CoQuiAAS v3.0 (simply CoQuiAAS in the following) participated in ICCMA’15, ICCMA’17 and ICCMA’19. Compared to the version used in ICCMA’17 (see [53] for details), the latest implementation of CoQuiAAS introduces changes also to handle dynamics. The full knowledge of the dynamics is exploited through a formula in which attacks can be activated/deactivated by using assumptions. CoQuiAAS has also been endowed with an integrated maximal satisfiable subsets (MSS) solver that took advantage of the approach proposed in [44] (the previous version resorted to an external solver). Other adjustments have been made to obtain an output compliant with the specifications of ICCMA’19.

EqArgSolver was first submitted to ICCMA’17 [68]. The version presented in ICCMA’19 has been improved with a series of changes aimed at increasing efficiency, readability, and software maintenance. First of all, the implementation of AFs and solutions has been moved to dedicated class objects. Then, to facilitate the representation of solutions, EqArgSolver associates each argument with an internal identifier determined by the position of the argument itself within the topological structure of the AF. The internal representation of solutions also changes, going from an approach with unordered maps (which was highly inefficient in terms of memory requirements) to the use of simple vectors of unsigned integers.

The Mace4/Prover9 solver relies on the combined search capabilities of two tools: Prover9, an automated theorem prover for first-order and equational logic, and Mace4, which searches for finite models and counterexamples. The authors tuned search parameters for the specific task of labeling AFs. In the pre-processing phase, arguments receive a weight depending on the number of outgoing attacks and then are ordered in a decreasing way. The first argument in the ranking (the one that attacks the most) is set to In, and the satisfiability is checked using Mace4. If the test fails, that argument is changed to Out, and the next argument in the ranking is set to In. The procedure continues until either a solution is found or all arguments have been tested. This method is expected to work well in finding a single extension, as Mace4’s domain size may cause a model explosion.

The μ-toksia solver made its debut in ICCMA’19; it is a purely SAT-based implementation, in the sense that all the reasoning by the system is performed by calls to a Boolean satisfiability (SAT) solver, including polynomial-time computations such as the grounded semantics, as well as incremental checks for the persistence of (non-)solutions under changes in the dynamic tasks. As shown in a KR20 paper [63], for DC and DS tracks, μ-toksia was able to scale much more and resulted in the best solver when tested against ICCMA’17 benchmarks instances. For a careful explanation of its implementation, refer to [63].

The Pyglaf reasoner competed in ICCMA’17 and ICCMA’19. It reduces problems to circumscription by means of linear encodings. Circumscription is a non-monotonic logic formalizing common sense reasoning by means of a second-order semantics, which essentially enforces minimizing the extension of some predicates. The circumscription solver extends the SAT solver glucose and implements an algorithm based on unsatisfiable core analysis. A thorough implementation description can be found in [5].

Taas-dredd implements a DPLL-like approach (Davis, Putnam, Logemann, Loveland), which performs an exhaustive search iteratively trying possible acceptability values for the arguments until a valid labeling is found or backtracking is needed. The search order is guided by domain-independent heuristics that aim to minimize backtracking steps; information propagation is used to infer acceptability values once certain decisions are made. Additional information and source codes can be found on the Taas project web page.1010

Yonas, first introduced in ICCMA’19, consists of an experimental abstract argumentation solver based on a combination of Deep Reinforcement-learning (DRL) and Monte Carlo Tree Search (MCTS). The implementation is realized in Python and PyTorch (a deep learning framework). The solver works with two main phases: pre-training and runtime. In the former phase, the DRL model is trained on a benchmark AFs set from ICCMA’17. During the runtime phase, the solver uses MCTS to search for solutions to a specific problem. The tree search is guided by a set of probabilities computed by the deep neural net, and the moves taken by MCTS feedback into the training of the neural net.

5.2.Participants in ICCMA’21

ICCMA’21 received 9 solver submissions as well from research groups in Austria, Finland, Germany, Italy, and the UK. The solvers and their developers are listed in Table 4, while Table 5 shows the solvers’ participation in sub-tracks. The participation of a solver in a sub-track means that it solves all the tasks in the sub-track. We also summarize in Table 6 the tasks supported by all solvers participating in the classical and exact tracks of the ICCMA’19 and ICCMA’21 competitions. Three of the submitted solvers, namely Aspartix, μ-toksia, and Pyglaf, are an updated version of those participating in the 2019 competition. Similarly to ICCMA’19, various techniques are used by the solvers, namely 3 solvers use the transformation of argumentation problems to SAT, 1 uses a transformation to ASP, 1 uses constraint programming, 1 is based on machine learning, and finally 3 are built on tailor-made algorithms.

AFGCN1111 proposes an approximate algorithm based on a Graph Convolutional Network model, trained on data from the previous editions of ICCMA. It extends the work described in [60].

A-Folio DPDB1212 is a portfolio using a method specifically designed for counting problems, based on tree decompositions: if the tree-width is smaller than a given threshold, then DPDB [40] (an approach initially designed for model counting in propositional logic) is used to determine the number of extensions. If the tree-width is too large, then μ-toksia [63] is used to enumerate the extensions, and this enumeration is used to obtain the number of extensions. Finally, for other tasks (SE, DC, DS), μ-toksia is directly used.

Aspartix-V21 [34] (when clear from the context, we only write Aspartix), based on ASP encoding of abstract argumentation, is an update of Aspartix-V which already participated to ICCMA’15 and ICCMA’19.

ConArg1313 is a solver based on constraint programming. The solver submitted to ICCMA’21 is an update of the version that participated in previous editions. More details on the approach can be found in [18,21].

FUDGE [72] uses SAT reductions to solve argumentation problems. While most of the reductions are similar to standard approaches in the literature, reasoning with the preferred and ideal semantics benefits from a new method proposed by the authors of the solver [73]. Roughly speaking, it uses a characterization of skeptical acceptability under the preferred semantics, where only some specific admissible sets are used. It means that the solver can avoid the cost of computing all the maximal admissible sets.

HARPER++1414 is an approximate solver relying on the grounded extension. The idea is quite simple: for all the semantics considered, the DC task is solved by answering YES exactly for the arguments that belong to the grounded extension and NO otherwise, and for DS the answer is NO for arguments attacked by the grounded extension, and YES otherwise.

MatrixX [45] represents some properties of arguments (attacks and defence) as matrices and uses an approach inspired by Knuth’s X algorithm for exact cover [47].

μ-toksia1515 is a solver based on SAT reductions; the solver submitted to ICCMA’21 is an updated version of the solver submitted to ICCMA’19. More details can be found in [63].

Pyglaf [6] transforms abstract argumentation tasks into circumscription and uses a SAT solver to obtain the result. Previous versions of the solver have been submitted to ICCMA’17 and ICCMA’19, see [5] for more details.

5.3.Benchmark selection for ICCMA’19

Starting from ICCMA’17, the competition welcomes argumentation solvers and the benchmarks on which the evaluations are performed. Six benchmarks have been submitted to ICCMA’17,1616 each of which focused on a specific theme, from generating particularly difficult instances to practical scenarios such as traffic networks and planning problems. Opening up to benchmarks in the competition goes toward testing the performance of argumentation solvers on real problems.

A total of 326 AF instances were selected for ICCMA’19 from the ones that were used in ICCMA’171717 and two new benchmarks submitted to ICCMA’19.1818 The selected benchmarks serve two primary purposes. Firstly, we intend to assess the progress of solvers for argumentation problems in comparison to the previous edition of the competition. Thus, we have included instances from ICCMA’17. Secondly, we aim to scrutinize the behavior of different solvers with more practical benchmarks and closer to real-world instances. By doing so, we can identify the most effective solvers to offer solutions to real problems. While testing difficult instances can push solver limits, we aimed to compare solver performance across all collected benchmarks. As pointed out in [69], a good number of instances adopted in ICCMA’17 were too hard for all the solvers submitted in that competition. For example SemBuster is a group of 16 AFs, having between 60 and 7500 arguments, which were classified as 2 very easy, 1 easy, 3 medium, 9 hard, 1 too hard, for what concerning the EE-PR track [42]. However, 15 out of these 16 AFs could not be enumerated at all in the EE-CO track [69]. ICCMA’17 instances on which all the submitted solvers did not score more than 0 points were counted: out of 350 instances, we obtained 114 AFs in EE-STG, 69 in EE-CO, 53 in EE-PR, 41 in EE-SST, 30 in EE-ST. In practice, these AFs did not participate in the evaluation of the solvers (that is, 10-30% of the tested AFs). While none of the DC and DS tasks showed this characteristic, all the SE tasks (except SE-CO) presented more than 20 “void” instances. Even on 5 AFs in the SE-GR track, no solver could find a solution before the timeout (these instances have more than 500,000 arguments).

The instances chosen for the competition, which avoided those that were overly hard, were selected using ConArg [18,21], a solver developed by some of the authors of this paper.1919 Only the instances ConArg could solve under extended time and memory conditions were selected from the benchmarks. ConArg used an allocation of 10 times the competition constraints’ time limit and memory space to solve the problems (see Section 5.7). As a result, the dataset consists of relatively easy instances. Detailed results in Appendix A show that, in ICCMA’19, no instance was left unsolved by all the participants. Therefore, all the selected 326 AFs were practically used in the tests. ConArg was also used as the reference solver to check the correctness of solutions returned by participants. However, it should be noted that some of the chosen instances were still challenging, as 1315 out of 46618 attempts to solve various tasks per each solver and instance ended with timeouts.

About two third of the instances were selected from ICCMA’17 benchmarks (i.e., 204). The number of selected instances for each class of ICCMA’17 are reported in A; their features are summarised in [42]. The remaining instances (i.e., 122) came from the two new benchmarks that were submitted to ICCMA’19. Only those AFs that ConArg could solve with extended conditions were selected. The first new set of benchmark instances, named ICCMA19B1, was submitted by Bruno Yun and Madalina Croitoru. It is a practically oriented benchmark on logic-based AFs instantiated from inconsistent knowledge bases expressed using Datalog^±, a language widely used in the Semantic Web. In the competition, only those instances from the Small and Medium classes (as labeled by the authors proposing the benchmarks) were used. The second set of new benchmark instances, hereafter referred to as ICCMA19B2, was produced by a benchmark generator supplied by Billy D. Spelchan and Gao Yong. Instead of a random model generating directed graphs D(n,q), where n is the number of vertices and p the edge probability, the authors propose D(n,p,q), where q is the probability of the attack to be mutual. The motivation is that with D(n,q), the existence of an extension in such a random AF is almost always guaranteed, making it less helpful in testing exact solvers (e.g. while testing the existence of a stable extension). In Table 7, we report the main statistics about the instances coming from these new datasets adopted in ICCMA’19. All such AFs are connected and have at least one cycle.

To sum up, Fig. 5 reports the distribution of benchmark instances: labels from A1 until T4 come from ICCMA’17, while the other three labels (S, M, and N) come from the two new benchmarks, described in the following paragraphs.2020 A reports the exact number of frameworks selected from each sub-benchmark.

Fig. 5.

The distribution of AF instances in the ICCMA’19 benchmark, selected from different benchmarks taken from ICCMA’17 (from A1 to T4), and from the two new submissions: S(mall) and M(edium) instances from ICCMA19B1, while N represents the instances from ICCMA19B2.

Dynamic-tasks benchmark-instances. All the introduced AFs and generators are intended for classical tasks in argumentation. Therefore, a generator was developed to produce benchmarks for dynamic tracks that create files with changes to AFs (see Section 4.1). Each addition/removal of an edge has an equal probability of 0.5. In removal, the attack to be deleted is selected among all the original attacks using a uniform distribution (it is impossible to remove a newly added attack). In case of addition, the two adjacent arguments are selected by using a uniform distribution, avoiding the generation of self-attacks and attacks that are already in. The generator reads both apx and tgf formats and produces apxm/tgfm modifications (see Section 4.1). The same 326 instances have been used for the dynamic tracks, including eight modifications to each AF, for a total of 2934 instances.

5.4.Benchmark selection for ICCMA’21

For the benchmark selection of ICCMA’21, a call for benchmarks was launched, which was unfortunately unsuccessful: no set of instances nor any generator was submitted. This leads to two paths: selecting a subset of ICCMA’19 instances and generating new ones. The ICCMA’19 instances were selected to be challenging enough to distinguish efficient solvers while still being solvable by some of them. Building the benchmark for ICCMA’21 in this way also allows for evaluating solver evolution from 2019 to 2021. Then, the hardest instances among the ones used at ICCMA’19 were selected, ranking the instances by two criteria: for a given AF F, we counted how many times a solver reached the timeout on F (for any problem and any semantics) during ICCMA’19. We also computed the average runtime of all solvers for solving any problem under any semantics on F. Then, we selected all the AFs such that the number of timeouts is greater or equal to 6, or the average runtime is greater or equal to 60 seconds. This means that all the instances that can be considered too easy (having almost no timeout or being solved in under a minute) were discarded, leading to a set of 107 AFs. Their distribution is described in Fig. 6. Most of them are actually instances from ICCMA’17 (datasets A1 to T4), while only 12 AFs have been selected from those submitted in response to the call for benchmarks at ICCMA’19. Detailed numbers of instances are provided in Appendix A.

Fig. 6.

The distribution of AF instances in the ICCMA’21 benchmark, selected from different benchmarks taken from ICCMA’19. A1 to T4 represent the instances from ICCMA’17, S(mall) and M(edium) are the instances from ICCMA19B1, while N represents the instances from ICCMA19B2.

ICCMA’21 also proposed a new approach for generating AFs considering underlying tree structures. More precisely, a tree T that will be used as a skeleton for the AF is first constructed (Fig. 7a). T is a perfectly balanced d-tree of height h generated randomly, where d and h are fixed and given as parameters. Then, each node of the tree is associated with a fresh local AF graph (fresh in the sense where each AF’s arguments are disjointed, see Fig. 7b). To link local AFs together, for each AF AN rooted to a node N of T, attacks between arguments of AN and arguments coming from AFs present in the left or right subtree of N are added (Fig. 7c). The final AF is the set of local AFs and the added attacks (see Fig. 7d).

Fig. 7.

AFs generation process.

The number of arguments k that are used to be linked to outside AFs is fixed and is given as a parameter. For a given AF AN, let A be the set of arguments selected to be linked. Then, for each AF AN′ present in the left or right sub-tree of N, a percentage r of arguments A′ of AN′ are selected to interact with A. r is chosen randomly between [l,u] such that 0⩽l<u⩽1 and l, u are given as parameters. Once A and A′ are identified, each pair (a,a′)∈A×A′ is considered and the attack (a,a′) or (a′,a) is added with a probability one-half.

For the local AF, two random generators have been considered that are based on the following random graph generators:2121

The values nb, mb and ne are integers and pe is between ]0,1]. Let us observe that Barabasi-Albert only constructs undirected graphs, which differs from what is required to construct AFs. To overcome this issue, two graphs called the attack graph A and the defense graph D were constructed to generate an AF. Then, for each lexicographically ordered edge (a1,a2) of A (respectively D) an attack (a1,a2) (respectively (a2,a1) is added. In order to keep the correct number of edges, A and D are generated with ⌈12×mb⌉ (respectively ⌈12×mr⌉) edges for the Barabasi-Arbert model.

The numbers that are used for generating the local AFs have default values nb=1000, mb=70, ne=300, and pe=0.1. Then, two last parameters are used for generating the tree structure: these parameters are d (tree depth) and w (tree-width). Finally, once these parameters are fixed, the last thing to decide is the type of the local AFs. For a given instance, either all they are of type Erdös-Rényi, or all are of type Barabasi-Albert, or they are randomly chosen between one of them.

The details of the distribution of these instances are available online in a CSV file where the first column indicates the type of the local AFs (E for Erdös-Rényi, B for Barabasi-Albert, and BE for the random choice of one of them), the second and third columns give the tree depth and tree-width, and the last column gives the number of instances.2222 With all the combinations of parameters, we have 180 types of instances: 60 for each local AF type (E, B, BE). These 60 types of instances correspond to the combination of d∈{5,…,10} and w∈{1,…,10}.

The motivation for developing this benchmark generation model was twofold: first of all, it seemed intuitive that (some) large debates could be split into smaller, loosely connected debates. This is the case, for instance, in presidential elections, where arguments about (e.g.) the economy are strongly connected, arguments about environmental issues are strongly connected, but arguments about the economy are (comparatively) only loosely connected to the ones about the environment. This is based solely on intuition, as there is no formal evidence to support it for the moment. The second motivation was that community-based graphs could offer interesting instances that can be solved by “clever” algorithms that take into account the properties of the graph while being hard for purely SAT-based approaches.2323 The challenges posed by community-based instances have already been observed in other domains (e.g. SAT, [61]), as well as the ability of the proposed model to provide challenging instances (see [56]).

Notes. A tool has been developed by the organizers of ICCMA’21 specifically for the purpose of translating from APX to TGF format. The source code and the description of how to use the tool are available online.2424

Approximate track benchmark selection. The set of benchmarks used for the approximate track is a subset of the ones used for the complete track, containing all the instances for which the winner of ICCMA’19 (μ-toksia) could determine the result in 4 hours. The arguments in the acceptance request are the same as those in the exact tracks.

5.5.Scores and ranking at ICCMA’19

Each solver was given 4 GB of RAM to compute the results of tasks in both the classical and dynamic tracks. The timeout to compute an answer for the dynamic track was 5 minutes for each framework/change: half of the time in the classical track for a single instance, that is 10 minutes. Time and memory limits mimic previous competitions (also to have some comparison). All runs were done on Intel Sandy Bridge CPUs with 16 cores clocked at 2.6 GHz and 64 GB of RAM, using up to all 16 cores for different runs.

The solvers were given all instances in the tracks they participated in to solve. For each instance, a solver got (0,1] points if it delivered the correct result (it could be incomplete, see below); −5 points if it delivered an incorrect result; 0 points if the result was empty (e.g. the timeout was reached without an answer) or if it was not parsable (e.g. some unexpected error message). For SE, DC, and DS, the assigned score was 1 if the solver returned the correct answer (respectively “yes”, “no”, or just an extension). For EE, a solver received a (0,1] fraction of points depending on the fraction of found enumerated extensions (1 if it returned all of them).

For the dynamic tracks, a result was considered correct and complete if, for n changes in a file, n+1 correct and complete results were provided by a solver (initial AF plus modifications). In ICCMA’19, there are 8 changes per file, so n=8. The score for a correct and complete result was 1, as usual. A partial (incomplete) result was considered correct if it gave fewer than n+1 answers, but each of the given answers was correct and complete (with respect to the corresponding static tasks). These rules applied to all the problems (SE, DC, DS, EE) in the dynamic track. A correct but incomplete result scored a value in (0,1], depending on the fraction of correct sub-solutions returned. If the considered dynamic task involved enumeration (i.e. EE) and the last solution a solver provided was correct but partial, then the whole answer was evaluated as if the last problem instance was not solved at all, considering the answer as partial and correct, and assigning a fraction of 1/n points, depending on the fraction of returned enumerated extensions. This exception does not penalize solvers that incrementally enumerate extensions; otherwise, the last solution would globally count as incomplete if a timeout occurs during enumeration. If any sub-solutions were incorrect, the overall output was considered incorrect (−5 points). Otherwise, if no answer was given, 0 points were assigned (for instance, due to a timeout).

The ranking of solvers for a track was based on the sum of scores over all tasks of a considered track. Ties were broken by the solver’s total time to return the correct results. Note that to ensure that each task had the same impact on the evaluation of a track, all tasks for one semantics had the same number of instances.

5.6.Scores and ranking at ICCMA’21

For the 2021 edition, the competition has been run on a computer cluster where each machine has an Intel Xeon E5-2637 v4 CPU and 128GB of RAM. The runtime limit for each instance is 600 seconds for the “exact” track and 60 seconds for the “approximate” track. The memory limit is the machine’s memory, i.e. 128GB. Each sub-track has one ranking, i.e., six rankings for the “exact” track and six rankings for the “approximate” track. To be ranked, a solver must participate in the full sub-track (without obligation to participate in all the (sub)tracks). The scoring system is slightly different between both tracks.

For the “exact” track, any wrong result on an instance i in a sub-track conducts to the exclusion of the solver from the said sub-track. It does not prevent the solver from being ranked for other sub-tracks if there are no wrong results for these other ones. Then, the score of a solver S on the instance i is

On the contrary, wrong results do not lead to an exclusion in the “approximate” track:

Then, the score of the solver S for the task T is

When two solvers have the same score for a given sub-track, the cumulated runtime over the instances correctly solved is used as a tie-break rule (the fastest is the best).

5.7.Reference solvers

In the ICCMA argumentation competitions, only a reference solver is usually used to check the results correctness. For instance, solutions for all instances in ICCMA’15 were computed using Tweety [71,75], a collection of libraries for logical aspects of artificial intelligence and knowledge representation, while Aspartix-D was employed as the reference solver in ICCMA’17 [37,42]. No proof can be given that ConArg has no errors, but 100% of the competition’s instances were solved by obtaining the same results as the solvers able to solve such instances. In ICCMA’19, ConArg [18,21], was utilized as the reference solver of the competition. The output of solvers was compared among themselves and with the output produced by ConArg to ensure the correctness and completeness of the answers. Additionally, ConArg was used to select benchmark instances, as mentioned in Section 5.3. ConArg (i.e., argumentation with constraints) is a Constraint-programming tool developed by some of the authors of this paper, based on Gecode,2525 an efficient C++ toolkit for developing constraint-based systems and applications. ConArg and Conarglib (its software-library version) are among the official projects supported by Gecode. The two main goals of this tool are to i) to solve further problems linked to weighted problems [19], and ii) to improve its performance over classical semantics, by using a benchmark assembled with random graph-models [20].

In [29], the authors classify the ConArg approach among “reduction-based implementations”, where first the problem is reduced to the target formalism (in this case, constraints), then a solver for that formalism is executed and, finally, the obtained output is interpreted as solutions of the original problem. The search phase takes advantage of classical techniques in Constraint-programming, such as local consistency, different heuristics for trying to assign values to variables, and complete search-tree with branch-and-bound. Models in Gecode are implemented using spaces. A space is home to variables, propagators (implementations of constraints), and branchers (implementations of branching, describing the shape of the search tree).

To prevent any issues caused by instances that the reference solver could not solve, the organizers of the ICCMA’19 competition aimed to avoid their usage. The authors of [69] proved that nearly 23% of all AFs of ICCMA’17 could not be enumerated by any solver, and some participant in the competition was erroneously scored positively for instances that no solver could solve. For this reason, one of the criteria for selecting instances in ICCMA’19 was that they had to be solvable by the reference solver. Since ConArg is not the best performance solver, it used 10 times the time and 10 times the memory space granted in the competition constraint to solve the problems. As shown in [69], ConArg solved 76.92% (20 out of 26) of the problems solved by only one solver in ICCMA’17, which, in our opinion, guarantees to have not only easy instances.

Concerning the ICCMA’21 competition, a tool named RUBENS,2626 developed by some authors of this paper was used to perform initial checks on the submitted solvers. RUBENS is a library designed to generate test cases automatically using translation rules. It comes with some pre-built test generators and an interface allowing users to create new ones with minimal effort. The RUBENS checker then executes the software to be tested on the generated test cases, and if the software produces an unexpected result, an error message is thrown. Using this tool allowed us to discover some issues in two solvers, providing the authors with few instances and allowing them to correct their solvers before the competition. A reference solver was not taken into consideration for the exact track. Instead, the obtained results for each instance were examined to identify any inconsistencies. This allowed us to discover that another solver was incorrect for a sub-track. Unfortunately, this solver could not be fixed in time to participate in the considered sub-track. The same methods could not be used for the approximate track due to the incomplete nature of the algorithms. Therefore, the 2019 version of μ-toksia was considered a reference solver, as described in Section 5.4. The correctness of the solvers in ICCMA’21 was ensured by taking advantage of the work done by the organizers of the 2019 edition. For both complete and incomplete ICCMA’21 tracks, the global results were aggregated by a dedicated tool, mETRICS.2727

6.1.Statistical significance of results

To determine whether the runtime differences of the solvers are significant, we conducted a Wilcoxon signed-rank test [78], a non-parametric test for paired samples which compares the probability that a random value from the first group is greater than its dependent value from the second group. In our case, each group contains the execution time of a solver, given a particular task, against all instances solved by both solvers. The results obtained are trustworthy since the following assumptions are fulfilled: i) the dependent variable is continuous, ii) paired observations are randomly and independently drawn, and iii) paired observations come from the same population. Upon comparison, the test generates a p-value for each sample pair, and statistical significance is determined if the p-value falls below a certain threshold, most commonly 0.05. Performing tests to compare the runtimes for all solvers participating in ICCMA’17, 19, and 21 was not possible due to the different machine configurations on which the performance of the solvers was computed, which results in execution times that are not directly comparable. Therefore, we conducted the test on participant solvers in the ICCMA’19 classic tracks.3030 We discuss below the results of tests.

For most of the results (354 out of 383 tests), we obtain p-value <0.05. In other words, the difference between the sample change and the expected change is big enough to be statistically significant. For the remaining 29 solver pairs with p-value ⩾0.05, we cannot exclude the hypothesis that the difference between their runtimes follows a symmetric distribution around zero. This means that there is no evidence of a statistically significant difference between the two distributions, and it cannot be concluded with sufficient confidence that there is a dissimilarity between the performances of the two compared solvers. Two solvers in particular, μ-toksia and Mace4-Prover9, frequently present high p-values when tested with the other solvers.

Table 8 shows the results of the Wilcoxon signed-rank tests, conducted between Mace4-Prover9 and other solvers, that presented a p-value ⩾0.05. Mace4-Prover9 performs closely to the solvers listed in the table for the tasks it participates in. For instance, in the SE-CO task, Mace4-Prover9 and eqargsolver are ranked sixth and seventh, respectively. It is worth noting that mu-toksia, the best overall solver in ICCMA’19, never appears in Table 8, so its performance compared to Mace4-Prover9 cannot be questioned.

The findings in Table 9 suggest a statistically non-significant difference in performance between μ-toksia and Taas-dredd, which, however, ranked first and last, respectively, for the tasks DC-CO, DC-PR, DS-PR, EE-CO and SE-CO. It appears that Taas-dredd’s behaviour varies considerably depending on the benchmark instances, possibly due to the quality of the heuristics used. Nevertheless, when compared on average, Taas-dredd performs much worse than μ-toksia for all tasks and again, these results do not undermine the validity of the rankings obtained.

6.2.Comparison with ICCMA’17 solvers

The first four solvers in ICCMA’17 were compared with the overall winner of ICCMA’19 to quantify the improvements of solvers achieved in two years. The past solvers were also dockerized by asking the participants of ICCMA’17 for those older versions (the participant himself dockerized Pyglaf).

Table 10 shows the scores for Argmat-sat, ArgSemSAT, CoQuiAAS’17, Pyglaf’17, and μ-toksia’19 on the ICCMA’19 benchmark instances. It can be noted that CoQuiAAS’17 has a negative score due to his erroneous behaviour in some tasks of ICCMA’17. μ-toksia also ranks first among these solvers, obtaining two points more than Pyglaf in 2017. Except for the EE and ST tracks, Argmat-sat performed very well as well. μ-toksia shows better time performance for 20 out of 24 tasks compared to Argmat-sat, while memory consumption is better for Argmat-sat in 15 out of 24 tracks. Only considering completed problem instances, the total time for μ-toksia is 8.2% less than Argmat-sat, while the maximum memory consumption is 112% more for Argmat-sat.3131 B, Table 21 provides detailed results about Argmat-sat ’17, Pyglaf ’17, and μ-toksia in terms of the total time taken to solve the instances in a task, and the maximum memory consumption across all instances in a given task.

6.3.Comparison between dynamic and non-dynamic solvers

Finally, the performance of dynamic versions of solvers was compared to the performance of their static equivalents. The benchmark instances and eight modifications each were used for comparison (see Section 5.3). Instances suitable for non-dynamic solvers were also generated by applying the modifications. This comparison considered the total time taken to solve each instance and its modifications for the successfully solved instances, and it was performed for the three solvers submitted to dynamic tracks, namely CoQuiAAS, μ-toksia, and Pyglaf. In Appendix B, Table 22 shows the performance differences – the performance advantage of the dynamic solvers is evident.

On average, the dynamic versions of CoQuiAAS, μ-toksia, and Pyglaf improved their performance over their non-dynamic versions by respectively 81.87%, 27.61%, and 86.54%. The difference between μ-toksia and the other two solvers is probably because it already shows excellent performance in its non-dynamic version, thus outlining a performance limit for both non-dynamic and dynamic tools. In C, Fig. 26a, Fig. 26b and Fig. 26c report the sum of the times of successful instances considering a solver and its dynamic version, respectively, CoQuiAAS, μ-toksia and Pyglaf. Figure 12 shows the percentage improvement per task by considering the three different solvers.

Fig. 12.

Percentage performance-improvement of a dynamic solver over its non-dynamic version. Values on the ordinate are computed as 100−(Tdynamic×100÷Tnon-dynamic), where T corresponds to the sum of all solved instances in each task. The bars in the chart correspond to tasks in the legend, read in top-bottom firstly, left-right secondly direction.

We also show the differences in performance of CoQuiAAS, μ-toksia, Pyglaf, and their dynamic version with respect to the single problem and the semantics. Figure 13 reports the sum of the times, aggregated by problem, of successful instances considering a solver and its dynamic version. In Appendix C, Figs 27a to 27c report the sum of the times, aggregated by semantics, of successful instances considering a solver and its dynamic version.

Fig. 13.

The sum of the time (logarithmic scale) aggregated by the problem of successful instances for each track, considering CoQuiAAS, μ-toksia, and Pyglaf, together with their dynamic versions. Times are reported in Table 22 in B.

7.1.Exact track

Compared to the previous edition, the main result of the competition is that there is no global winner (μ-toksia, in 2019). Indeed, A-Folio-DPDB won two sub-tracks (CO and ST), PYGLAF won two sub-tracks (PR, SST), ASPARTIX-V21 won one sub-track (STG) and FUDGE won one sub-track (ID). This is a combination of new solvers (A-Folio-DBDP, FUDGE) and updated versions of solvers that already participated in ICCMA (ASPARTIX and PYGLAF). While all these solvers use some reduction to SAT or ASP in some cases, A-Folio-DPDB is the first ICCMA winner based on tree-width analysis of the instances.

Figure 14 shows the runtime of solving each instance in the exact track for each solver participating in the sub-tracks dedicated to the complete and semi-stable semantics (other semantics are plotted in C). We observe that some groups of instance seem (in general) easier than some other ones. The data is plotted such that instances are sorted in the lexicographical order. This means that the instances on the left side correspond to some of the instances selected from ICCMA’19 (their benchmark names start with A and B), while the instances at the center correspond mainly to the new instances generated for ICCMA’21. This is in line with the intuition that the new instances should be hard for solvers that do not consider the AFs’ structure. However, notice that the other instances selected from ICCMA’19 (on the right side, with benchmark names starting with M, n, S, or T) are in some cases easy (e.g. Fig. 14a) and in some cases hard, even harder than the new instances from ICCMA’21 (e.g. Fig. 14b).

Fig. 14.

Time [s] taken for each correctly solved instance in the exact track for the semantics CO and SST – ICCMA’21.

On Fig. 15, which shows the cumulative runtime (in seconds) for the exact track (under the semantics CO and SST – other semantics are provided in C), the observations are consistent with the rankings of the competition. More precisely, well-ranked solvers solve more instances in less time, while the last-ranked solvers either fail to solve many instances or require much more time. Interestingly, some solvers seem more efficient on “easy” instances but cannot solve more challenging ones. Consider, for instance, μ-toksia (and its parallel version) for the semi-stable semantics (Fig. 15b), and compare it with Pyglaf. μ-toksia’s accumulated runtime is much lower than Pyglaf’s, but the former has provided an answer for much fewer instances (hence their final ranking).

Fig. 15.

Cumulative time [s] taken to correctly solve all instances in the exact track for the semantics CO and SST – ICCMA’21.

7.2.Approximate track

For the track dedicated to approximate algorithms, HARPER++ won two sub-tracks (CO, ID), while AFGCN won the other sub-tracks. However, an essential difference between both solvers is their runtime: AFCGN is much slower than HARPER++ in all cases, as can be seen in Fig. 16 (runtime for each instance, for the complete semantics) and Fig. 17 (cumulative runtime for the complete semantics).3232 This comes from the fact that HARPER++ mainly relies on the grounded extension, which can be computed in linear time (in the number of arguments). The detailed results for each pair (problem, semantics) are described in [55]: it shows that, in general, HARPER++ is more accurate for skeptical reasoning (DS) while AFGCN is more accurate for credulous reasoning (DC).

Fig. 16.

Time [s] taken for each correctly solved instance in the approximate track for the complete semantics – ICCMA’21.

Fig. 17.

Cumulative time [s] taken to correctly solve all instances in the approximate track for the complete semantics – ICCMA’21.

9.1.ICCMA 2019

The requirement for all submitted solvers to use Docker in ICCMA’19 saved much work in setting up solvers and ensuring they ran correctly. However, Docker containers cannot be run directly on most HPC infrastructure because of Docker’s security deficiencies. To leverage our HPC infrastructure to provide the large amount of computational resources required, the Docker containers were converted to Singularity containers,3333 which could be run without problems. The underlying virtualization is the same, and the conversion is straightforward; for the purposes of this competition, Docker and Singularity are equivalent.

JSON inspires the standardized output format required for submitted solvers but does not entirely conform to the JSON standard. Various pre-processing steps were implemented in ICCMA’19 that transformed the output format into JSON and handled simple cases directly. While this allowed us to use a standard JSON parser, the additional steps could have been avoided with simple modifications to the output format. It can be recommended that competition organizers require standard formats as far as possible to avoid implementing custom parsers.

As can be seen from the results of the competitions held in 2017 and 2019, the performance of participants relying on SAT varies greatly depending on the implementation of the SAT solver itself. Concerning solvers submitted to ICCMA’19, Argpref implements MiniSAT 2.2.0, a SAT-with-preferences based approach [36], μ-toksia and Pyglaf are both dependant on the Boolean SAT solver Glucose (version 4.1) [7,8], and Taas-dredd implements the DPLL-algorithm (Davis-Putnam-Logemann-Loveland) backtracking algorithm for SAT solving [15, Chapter 3]. In ICCMA’21, Pyglaf is still based on Glucose, FUDGE uses the SAT solver CaDiCaL 1.3.1,3434 while, differently from the 2019 edition, μ-toksia includes CryptoMiniSat (version 5.8.0) [70] as the underlying SAT solver.

Selecting the benchmarks to use could lead to errors in the evaluation phase. As shown in [69], 23% of AFs from ICCMA’17 could not be enumerated by any solver. To avoid potential issues, ICCMA’19 instances were limited to those solvable by ConArg, the reference solver. Indeed, the reference solver had a different time and memory limitation than the participant in the competition; ConArg was given 10 times the time and memory space used in the competition to solve problems. So, despite Conarg not having the best time and memory performance of other solvers, the benchmarks also included difficult (enough) instances. Indeed, ConArg is developed and maintained by some of the ICCMA’19 organizers, hence the decision to use it as a reference solver.

9.2.ICCMA 2021

The organizers of the 2021 edition appreciated the use of Docker in ICCMA’19. However, a part of the community did not receive it well. Furthermore, some technical difficulties were encountered, which prevented the organizers from using Docker again for ICCMA 2021. As a result, various issues arose when setting up the competition environment, such as ensuring that all the submitted solvers were correctly compiling or running.

The exceptional results of μ-toksia 2019 (even when compared to more recent solvers submitted to ICCMA 2021) may give the impression that choosing the “best” SAT solver is enough to solve all the argumentation problems. However, experimental evaluations [43,46] have shown that no SAT solver is strictly dominating the other ones for solving argumentation tasks, but each solver has its own strengths and weaknesses, depending on the problem to be solved, the semantics, and the instance. An exact characterization of which SAT solver is the best for each of these combinations is still an open question.

Moreover, beyond the SAT-based approaches, other approaches have been studied in the literature (e.g., based on graph decomposition [57] or backdoors [33]). These approaches seem promising but were mainly absent from ICCMA. However, let us notice that the success of A-FOLIO-DPDB for the counting task (using a technique based on the graph treewidth) confirms the interest of such approaches. So, we believe that one of the main challenges for the near future of the ICCMA competition is to provide challenging benchmarks that could not be solved by “simply” plugging a SAT solver but would require a more fine-grained analysis of the graph properties like those mentioned here. We have started this effort with our community-based benchmark generation approach.

We envision two last directions for improving the competition. Regarding the main track, it seems important to be able to guarantee the results of the solvers, e.g., providing not only a YES/NO answer to decision problems but also completing them with a certificate. This effort has been started by the recent ICCMA 2023, which requires a certificate with positive answers for credulous acceptability and negative answers for skeptical acceptability. Finding certificates for other cases is a challenge, but inspiration could be taken from other communities (e.g. in SAT competitions, UNSAT instances are certified as well3535).

Finally, regarding the approximate track, various important questions should be investigated, like the possibility of giving guarantees about the proximity between the correct result and the answer provided by the algorithms or approximate algorithms for computing one extension or the set of (skeptically or credulously) accepted arguments.