=Paper=
{{Paper
|id=Vol-3236/paper9
|storemode=property
|title=A Labeling Based Backtracking Solver for Abstract Argumentation
|pdfUrl=https://ceur-ws.org/Vol-3236/paper9.pdf
|volume=Vol-3236
|authors=Lukas Kinder,Matthias Thimm,Bart Verheij
|dblpUrl=https://dblp.org/rec/conf/comma/KinderTV22
}}
==A Labeling Based Backtracking Solver for Abstract Argumentation==
https://ceur-ws.org/Vol-3236/paper9.pdf
A Labelling-based Solver for Computing Complete
Extensions of Abstract Argumentation Frameworks
Lukas Kinder1 , Matthias Thimm2 and Bart Verheij1,*
1
Bernoulli Institute of Mathematics, Computer Science and Artificial Intelligence, Nijenborgh 9, 9747 AG Groningen, The
Netherlands
2
Artificial Intelligence Group, University of Hagen, Universitätsstr. 11, 58097 Hagen, Germany
Abstract
THEIA is a labeling-based system computing the complete extensions of an abstract argumentation
framework. Like other backtracking solvers, THEIA does this by repeatedly choosing an argument and
labelling it until either a contradiction with respect to the labels is reached or a complete extension
is found. THEIA reduces the number of backtracking steps needed by using propagation techniques
that use a larger set of labels. These labels keep track of arguments that cannot be labeled IN, OUT or
UNDEC during a state in the search. THEIA is also using an extensive look-ahead strategy to prune
branches. It is shown that THEIA outperforms related labeling-based backtracking solvers by the use of
more sophisticated propagation and pruning rules and forward-looking strategy.
Keywords
Abstract argumentation, backtracking solvers
1. Introduction
Argumentation theory is a multidisciplinary area connected to philosophy, law and linguis-
tics [1, 2, 3, 4]. In recent years, argumentation has been extensively studied formally and
computationally, especially also since Phan Minh Dung presented abstract argumentation
frameworks [5] (see also [6]). Abstract argumentation frameworks are a simple but powerful
approach to formal argumentation. They represent arguments as nodes in a graph which
attack other arguments. Interpreting these graphs by finding meaningful sets of arguments
is a non-trivial task that may require significant computational time and effort. For instance,
so-called backtracking algorithms gradually label arguments to analyse the graph and backtrack
whenever contradicting labels are found. Examples of backtracking solvers are for example
[7, 8, 9, 10, 11, 12].
THEIA, the system presented here, enumerates the set of complete extensions of an abstract
argumentation framework. THEIA is in particular inspired by HEUREKA [7] and DREDD [8].
The system THEIA differs from HEUREKA and DREDD due to its use of more sophisticated rules
during propagation and pruning and by a forward looking strategy. The basic idea is to keep
SAFA’22: Fourth International Workshop on Systems and Algorithms for Formal Argumentation 2022, September 13,
2022, Cardiff, Wales, United Kingdom
*
The research reported in this paper is based on Lukas Kinder’s Bachelor thesis ‘THEIA: A labeling based backtracking
solver for abstract argumentation’ supervised by Bart Verheij (fse.studenttheses.ub.rug.nl/25428/), and
extended in collaboration with Matthias Thimm.
© 2022 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
CEUR
Workshop
Proceedings
http://ceur-ws.org
ISSN 1613-0073
CEUR Workshop Proceedings (CEUR-WS.org)
111
Lukas Kinder et al. CEUR Workshop Proceedings 111–123
↙
𝐴← →𝐵 𝐶↑
↓ ↘
𝐷 →𝐸 →𝐹
Figure 1: An argumentation framework. Note that argument C is attacking itself.
track of arguments that cannot be labeled 𝐼𝑁 , 𝑂𝑈 𝑇 , or 𝑈 𝑁 𝐷𝐸𝐶 while searching for complete
extensions. This can reduce the number of backtracking steps during the search as conflicting
labels can be discovered early.
This paper gives an overview of the relevant background and related work in Section 2.
Section 3 gives an overview of the system’s design, which elaborates on propagation tech-
niques, the look-ahead strategy and heuristics used. This is followed by an experimental
evaluation in Section 4 and a discussion in Section 5. The code of THEIA is available at
github.com/LukasKinder/THEIA.
2. Background
An abstract argumentation framework [5] is a tuple 𝐴𝐹 = ⟨𝒜, ℛ⟩. Here 𝒜 is the set of
arguments and ℛ ⊆ 𝒜 × 𝒜 is the attack relation. A pair (𝑎, 𝑏) ∈ ℛ can be interpreted as
argument 𝑎 attacking argument 𝑏. An example for an argumentation framework is shown in
Figure 1.
For an argument 𝑎𝑟𝑔 ∈ 𝒜, define 𝑎𝑟𝑔 + as the set of arguments that are attacked by 𝑎𝑟𝑔 and
𝑎𝑟𝑔 − as the set of arguments attacking 𝑎𝑟𝑔. Likewise, given a set of arguments 𝐴𝑟𝑔𝑠 ⊆ 𝒜,
define 𝐴𝑟𝑔𝑠+ = {𝑏 | ∃𝑎 ∈ 𝐴𝑟𝑔𝑠 : 𝑏 ∈ 𝑎+ } and 𝐴𝑟𝑔𝑠− = {𝑏 | ∃𝑎 ∈ 𝐴𝑟𝑔𝑠 : 𝑏 ∈ 𝑎− }.
An argumentation framework can be interpreted by finding meaningful sets of arguments.
A set 𝐸 ⊆ 𝒜 is conflict-free if there do not exist any 𝑎𝑟𝑔1 , 𝑎𝑟𝑔2 ∈ 𝐸 such that 𝑎𝑟𝑔1
attacks 𝑎𝑟𝑔2 . A set 𝐸 is admissible if 𝐸 is conflict-free and 𝐸 − ⊆ 𝐸 + . Further, a
set 𝐸 is complete if 𝐸 is admissible and there does not exist an argument 𝑎𝑟𝑔 such that
𝑎𝑟𝑔 ∈/ 𝐸 and 𝑎𝑟𝑔 − ⊆ 𝐸 + . The grounded set is the smallest (wrt. set inclusion) complete set.
More about relations and properties of these sets can be found in [5].
A variant of the above set-based interpretation of argumentation frameworks, is the labelling-
based interpretation [13]. Here, each argument is assigned a label 𝐼𝑁 , 𝑂𝑈 𝑇 or 𝑈 𝑁 𝐷𝐸𝐶 using
a labeling function ℒ.
ℒ : 𝒜 ↦−→ {𝐼𝑁, 𝑂𝑈 𝑇, 𝑈 𝑁 𝐷𝐸𝐶}
Define 𝑖𝑛(ℒ) = {𝑥|ℒ(𝑥) = 𝐼𝑁 }; 𝑜𝑢𝑡(ℒ) = {𝑥|ℒ(𝑥) = 𝑂𝑈 𝑇 }; 𝑢𝑛𝑑𝑒𝑐(ℒ) = {𝑥|ℒ(𝑥) =
𝑈 𝑁 𝐷𝐸𝐶}.
Definition 1. A labeling is is a complete labeling ℒ𝑐𝑜𝑚𝑝𝑙𝑒𝑡𝑒 if and only if:
• For all arguments 𝑎 ∈ 𝑖𝑛(ℒ𝑐𝑜𝑚𝑝𝑙𝑒𝑡𝑒 ) it holds that there does not exist an argument 𝑏 such
that (𝑏, 𝑎) ∈ ℛ and 𝑏 ∈ 𝑖𝑛(ℒ𝑐𝑜𝑚𝑝𝑙𝑒𝑡𝑒 ) or 𝑏 ∈ 𝑢𝑛𝑑𝑒𝑐(ℒ𝑐𝑜𝑚𝑝𝑙𝑒𝑡𝑒 ).
112
Lukas Kinder et al. CEUR Workshop Proceedings 111–123
• For all arguments 𝑎 ∈ 𝑜𝑢𝑡(ℒ𝑐𝑜𝑚𝑝𝑙𝑒𝑡𝑒 ) it holds that there exists an argument 𝑏 such that
(𝑏, 𝑎) ∈ ℛ and 𝑏 ∈ 𝑖𝑛(ℒ𝑐𝑜𝑚𝑝𝑙𝑒𝑡𝑒 ).
Note that this implicitly defines that for all arguments 𝑎 ∈ 𝑢𝑛𝑑𝑒𝑐(ℒ𝑐𝑜𝑚𝑝𝑙𝑒𝑡𝑒 ) it holds that there
exists an argument 𝑏 such that (𝑏, 𝑎) ∈ ℛ and 𝑏 ∈ 𝑢𝑛𝑑𝑒𝑐(ℒ𝑐𝑜𝑚𝑝𝑙𝑒𝑡𝑒 ) and there does not exist
an argument 𝑐 such that (𝑐, 𝑎) ∈ ℛ and 𝑐 ∈ 𝑖𝑛(ℒ𝑐𝑜𝑚𝑝𝑙𝑒𝑡𝑒 ). Note that ℒ𝑐𝑜𝑚𝑝𝑙𝑒𝑡𝑒 is a complete
labelling only if 𝑖𝑛(ℒ𝑐𝑜𝑚𝑝𝑙𝑒𝑡𝑒 ) is a complete extension [13].
2.1. Existing Solvers
In this work, we are interested in the problem of enumerating all complete extensions of a given
abstract argumentation framework 𝐴𝐹 , which is highly intractable [14]. This motivates the
need to develop sophisticated algorithms. A method that can be applied for this task is the DPLL-
algorithm (Davis-Putnam-Logemann-Loveland) [15]. The structure of a basic backtracking
algorithm is shown in Algorithm 1 (where the procedure to select the next argument and the
procedure propagateLabels are left unspecified, these are defined by the concrete system). Every
iteration an argument is chosen and each possible label for this argument is tried out. The
respective new label is then propagated to find labels of other arguments. This may cause a
contradiction if it is necessary to re-label an argument. A solution is reached once all arguments
got assigned a label. An intuitive way to think about this algorithm is that a search tree is
created in which new branches are generated whenever different labels of an argument are
tried out. This method is for example used by ArgTools [10], HEUREKA [7] and DREDD [8].
The above-mentioned systems are referred to as direct solvers, which directly work within
the formalism of abstract argumentation to solve problems [16]. However, the state of the art
in solvers for abstract argumentation typically rely on reductions to other problem-solving
paradigms such as SAT-solving or answer set programming. For example, 𝜇-toksia [17] is a
solver that makes iterative calls to a SAT-solver to enumerate all complete extensions.
Algorithm 1 The pseudo-code of a basic backtracking algorithm.
procedure findComplete(𝐴𝐹 )
if all arguments are labeled then
print(Solution(𝐴𝐹 ))
return
𝑎← − choose an unlabeled argument
for all labels do
label 𝑎 with the next label
if propagateLabels(𝐴𝐹 ) != CONTRADICTION then
findComplete(𝐴𝐹 )
113
Lukas Kinder et al. CEUR Workshop Proceedings 111–123
3. Algorithm Design
Our algorithm is following the basic structure of Algorithm 1. However, THEIA differs from
other direct solvers insofar as it uses a significantly extended set of propagation techniques, a
look-ahead strategy to find contradicting labels earlier, and chooses an argument to split the
search based on the exact amount of labels that can be propagated. These three components are
discussed in the following sections.
3.1. Additional Propagation Techniques
The procedure propagateLabels corresponds to unit propagation in SAT-solving [15]. It sets the
labels of further arguments, whose status is already determined by the set labels. For example,
if an argument has been labelled 𝐼𝑁 , it is clear that all arguments attacked by this argument
must be labelled 𝑂𝑈 𝑇 . Existing solvers [10, 7, 8] use this and similar rules to implement the
procedure propagateLabels.
In the following, we significantly extend the set of existing propagation rules by introducing
additional labels. The labels 𝑁 𝑂𝑇 𝐼𝑁 , 𝑁 𝑂𝑇 𝑂𝑈 𝑇 and 𝑁 𝑂𝑇 𝑈 𝑁 𝐷𝐸𝐶 can be assigned for
arguments for which it is known that they cannot be labeled 𝐼𝑁 , 𝑂𝑈 𝑇 or 𝑈 𝑁 𝐷𝐸𝐶 respectively.
We refer to the labels 𝐼𝑁 , 𝑂𝑈 𝑇 and 𝑈 𝑁 𝐷𝐸𝐶 as final labels, and to the respective opposite
labels 𝑁 𝑂𝑇 𝐼𝑁 , 𝑁 𝑂𝑇 𝑂𝑈 𝑇 and 𝑁 𝑂𝑇 𝑈 𝑁 𝐷𝐸𝐶 as intermediate labels. We use the label
𝐵𝐿𝐴𝑁 𝐾 for unlabeled arguments. During the search, arguments with the label 𝐵𝐿𝐴𝑁 𝐾
may be relabeled to intermediate or final labels and arguments with intermediate labels may
still be relabeled to final labels.
We distinguish the propagation rules by the position of the argument that gets assigned a
label, relative to the argument that causes the rule to apply:
• Forward rule: Applying the propagation rule on an argument 𝑎𝑟𝑔 forces a new label on
an argument in 𝑎𝑟𝑔 + .
• Backward rule: Applying the propagation rule on an argument 𝑎rg forces a new label
on an argument in 𝑎𝑟𝑔 − .
• Sideward rule: Applying the propagation rule on an argument 𝑎𝑟𝑔 forces a new label
on an argument in (𝑎𝑟𝑔 + )− .
Table 1 contains propagation rules for argument labels. The three basecases can be applied
to arguments without considering the labels of other arguments. In practice, checking if a
propagation rule can be applied to an argument 𝑎 can be done in 𝒪(|𝑎+ |). This requires each
argument to keep track of how many attackers are labeled 𝑂𝑈 𝑇 , 𝑈 𝑁 𝐷𝐸𝐶 or 𝑁 𝑂𝑇 𝐼𝑁 .
Situations in which basecases can be applied are shown in Figure 6 and situations in which
the propagation rules can be applied are shown in Figure 7 in the appendix. Note that the
propagation rules 7 and 13, 9 and 14, 11 and 15 as well as 12 and 16 are all pairs that essentially
express the same. The difference is that the label assignment of the argument that causes the
rule to apply, is at a different position.
We omit the explanation of each of these rules, but give two examples:
• Rule 3: An argument that is attacked by at least one argument labeled 𝑈 𝑁 𝐷𝐸𝐶 and
otherwise only by arguments that cannot be relabeled to 𝐼𝑁 (I.e. 𝑂𝑈 𝑇 , 𝑈 𝑁 𝐷𝐸𝐶 and
114
Lukas Kinder et al. CEUR Workshop Proceedings 111–123
Table 1
A collection of propagation rules.
Argument 𝑎
Prerequisite Enforced label
has label:
−
- 𝑎 =∅ ℒ(𝑎) = 𝐼𝑁
Basecase - 𝑎 ∈ 𝑎− ℒ(𝑎) = 𝑁 𝑂𝑇 𝐼𝑁
- {𝑎} = 𝑎− ℒ(𝑎) = 𝑈 𝑁 𝐷𝐸𝐶
1.)ℒ(𝑎) = 𝑂𝑈 𝑇 (𝑎, 𝑏) ∈ ℛ ∧ ∀𝑐[(𝑐, 𝑏) ∈ ℛ −→ ℒ(𝑐) = 𝑂𝑈 𝑇 ] ℒ(𝑏) = 𝐼𝑁
2.)ℒ(𝑎) = 𝐼𝑁 (𝑎, 𝑏) ∈ ℛ ℒ(𝑏) = 𝑂𝑈 𝑇
Forward ℒ(𝑎) = 𝑂𝑈 𝑇 or
(𝑎, 𝑏) ∈ ℛ ∧ ∀𝑐[(𝑐, 𝑏) ∈ ℛ −→ ℒ(𝑐) ∈ {𝑂𝑈 𝑇, 𝑈 𝑁 𝐷𝐸𝐶,
rules 3.)ℒ(𝑎) = 𝑈 𝑁 𝐷𝐸𝐶 or ℒ(𝑏) = 𝑈 𝑁 𝐷𝐸𝐶
𝑁 𝑂𝑇 𝐼𝑁 }] ∧ ∃𝑑[(𝑑, 𝑏) ∈ ℛ ∧ ℒ(𝑑) = 𝑈 𝑁 𝐷𝐸𝐶]
ℒ(𝑎) = 𝑁 𝑂𝑇 𝐼𝑁
ℒ(𝑎) = 𝑁 𝑂𝑇 𝑂𝑈 𝑇 or
4.) (𝑎, 𝑏) ∈ ℛ ℒ(𝑏) = 𝑁 𝑂𝑇 𝐼𝑁
ℒ(𝑎) = 𝑈 𝑁 𝐷𝐸𝐶
ℒ(𝑎) = 𝑂𝑈 𝑇 or
5.) (𝑎, 𝑏) ∈ ℛ ∧ ∀𝑐[(𝑐, 𝑏) ∈ ℛ −→ ℒ(𝑐) ∈ {𝑁 𝑂𝑇 𝐼𝑁, 𝑂𝑈 𝑇 }] ℒ(𝑏) = 𝑁 𝑂𝑇 𝑂𝑈 𝑇
ℒ(𝑎) = 𝑁 𝑂𝑇 𝐼𝑁
ℒ(𝑎) = 𝑂𝑈 𝑇 or
6.) (𝑎, 𝑏) ∈ ℛ ∧ ∀𝑐[(𝑐, 𝑏) ∈ ℛ −→ ℒ(𝑐) ∈ {𝑂𝑈 𝑇, 𝑁 𝑂𝑇 𝑈 𝑁 𝐷𝐸𝐶}] ℒ(𝑏) = 𝑁 𝑂𝑇 𝑈 𝑁 𝐷𝐸𝐶
ℒ(𝑎) = 𝑁 𝑂𝑇 𝑈 𝑁 𝐷𝐸𝐶
(𝑏, 𝑎) ∈ ℛ ∧ ∀𝑐[(𝑐, 𝑎) ∈ ℛ −→ (𝑐 = 𝑏
7.)ℒ(𝑎) = 𝑂𝑈 𝑇 ℒ(𝑏) = 𝐼𝑁
∨ℒ(𝑐) ∈ {𝑂𝑈 𝑇, 𝑈 𝑁 𝐷𝐸𝐶, 𝑁 𝑂𝑇 𝐼𝑁 })]
8.)ℒ(𝑎) = 𝐼𝑁 (𝑏, 𝑎) ∈ ℛ ℒ(𝑏) = 𝑂𝑈 𝑇
Backward
9.)ℒ(𝑎) = 𝑈 𝑁 𝐷𝐸𝐶 (𝑏, 𝑎) ∈ ℛ ∧ ∀𝑐[(𝑐, 𝑎) ∈ ℛ −→ (𝑐 = 𝑏 ∨ ℒ(𝑐) = 𝑂𝑈 𝑇 )] ℒ(𝑏) = 𝑈 𝑁 𝐷𝐸𝐶
rules
ℒ(𝑎) = 𝑁 𝑂𝑇 𝑂𝑈 𝑇 or
10.) (𝑏, 𝑎) ∈ ℛ ℒ(𝑏) = 𝑁 𝑂𝑇 𝐼𝑁
ℒ(𝑎) = 𝑈 𝑁 𝐷𝐸𝐶
11.) ℒ(𝑎) = 𝑁 𝑂𝑇 𝐼𝑁 (𝑏, 𝑎) ∈ ℛ ∧ ∀𝑐[(𝑐, 𝑎) ∈ ℛ −→ (𝑐 = 𝑏 ∨ ℒ(𝑐) = 𝑂𝑈 𝑇 )] ℒ(𝑏) = 𝑁 𝑂𝑇 𝑂𝑈 𝑇
12.)ℒ(𝑎) = 𝑁 𝑂𝑇 𝑈 𝑁 𝐷𝐸𝐶 (𝑏, 𝑎) ∈ ℛ ∧ ∀𝑐[(𝑐, 𝑎) ∈ ℛ −→ (𝑐 = 𝑏 ∨ ℒ(𝑐) = 𝑂𝑈 𝑇 )] ℒ(𝑏) = 𝑁 𝑂𝑇 𝑈 𝑁 𝐷𝐸𝐶
ℒ(𝑎) = 𝑂𝑈 𝑇 or
(𝑎, 𝑏) ∈ ℛ ∧ ℒ(𝑏) = 𝑂𝑈 𝑇 ∧ (𝑐, 𝑏) ∈ ℛ ∧ ∀𝑑[(𝑑, 𝑏) ∈ ℛ
13.)ℒ(𝑎) = 𝑈 𝑁 𝐷𝐸𝐶 or ℒ(𝑐) = 𝐼𝑁
−→ (𝑑 = 𝑐 ∨ ℒ(𝑑) ∈ {𝑂𝑈 𝑇, 𝑈 𝑁 𝐷𝐸𝐶, 𝑁 𝑂𝑇 𝐼𝑁 })]
Sideward ℒ(𝑎) = 𝑁 𝑂𝑇 𝐼𝑁
rules (𝑎, 𝑏) ∈ ℛ ∧ ℒ(𝑏) = 𝑈 𝑁 𝐷𝐸𝐶 ∧ (𝑐, 𝑏) ∈ ℛ ∧ ∀𝑑[(𝑑, 𝑏) ∈ ℛ
14.)ℒ(𝑎) = 𝑂𝑈 𝑇 ℒ(𝑐) = 𝑈 𝑁 𝐷𝐸𝐶
−→ (ℒ(𝑑) = 𝑂𝑈 𝑇 ∨ 𝑑 = 𝑐)]
(𝑎, 𝑏) ∈ ℛ ∧ ℒ(𝑏) = 𝑁 𝑂𝑇 𝐼𝑁 ∧ (𝑐, 𝑏) ∈ ℛ ∧ ∀𝑑[(𝑑, 𝑏) ∈ ℛ
15.)ℒ(𝑎) = 𝑂𝑈 𝑇 ℒ(𝑐) = 𝑁 𝑂𝑇 𝑂𝑈 𝑇
−→ (ℒ(𝑑) = 𝑂𝑈 𝑇 ∨ 𝑑 = 𝑐)]
(𝑎, 𝑏) ∈ ℛ ∧ ℒ(𝑏) = 𝑁 𝑂𝑇 𝑈 𝑁 𝐷𝐸𝐶 ∧ (𝑐, 𝑏) ∈ ℛ ∧ ∀𝑑[(𝑑, 𝑏) ∈ ℛ
16.)ℒ(𝑎) = 𝑂𝑈 𝑇 ℒ(𝑐) = 𝑁 𝑂𝑇 𝑈 𝑁 𝐷𝐸𝐶
−→ (ℒ(𝑑) = 𝑂𝑈 𝑇 ∨ 𝑑 = 𝑐)]
𝑁 𝑂𝑇 𝐼𝑁 ) should get labeled 𝑈 𝑁 𝐷𝐸𝐶. This is because (in a complete labeling) an
argument that is not attacked by an argument labeled 𝐼𝑁 can not be labeled 𝑂𝑈 𝑇 and
argument that is attacked by an argument labeled 𝑈 𝑁 𝐷𝐸𝐶 can not be labeled 𝐼𝑁 , which
leaves 𝑈 𝑁 𝐷𝐸𝐶 as the only option.
• Rule 11: This rule is applied in a situation in which we have an argument for which it is
known that it cannot have the label 𝐼𝑁 . This means that it should not be the case that
all attackers are labeled 𝑂𝑈 𝑇 . Consequently, if all attackers except one argument 𝑏 are
labeled 𝑂𝑈 𝑇 , then 𝑏 should be marked with 𝑁 𝑂𝑇 𝑂𝑈 𝑇 .
It should be quite easy to see that all rules depicted in Table 1 are correct.
3.2. Look-Ahead
In each iteration, before an argument gets chosen to split the search, THEIA is testing every
possible label for all arguments with non-final labels (a similar idea had already been suggested
in [9]). Note that the number of combinations for this is 6 * 𝑛_𝑏𝑙𝑎𝑛𝑘 + 2 * 𝑛_𝑖𝑛𝑡𝑒𝑟𝑚𝑒𝑑𝑖𝑎𝑡𝑒
with 𝑛_𝑏𝑙𝑎𝑛𝑘 being the number of arguments labeled 𝐵𝐿𝐴𝑁 𝐾 and 𝑛_𝑖𝑛𝑡𝑒𝑟𝑚𝑒𝑑𝑖𝑎𝑡𝑒 being
the number of arguments having intermediate labels. After assigning a label to an argument,
this label is propagated and it is checked if this causes a contradiction (A contradiction is caused
115
Lukas Kinder et al. CEUR Workshop Proceedings 111–123
if a propagation rule forces a label on an argument that can not be relabeled based on its current
label). If this is the case, the argument permanently gets labeled the opposite label. For example
if labeling an argument 𝑁 𝑂𝑇 𝐼𝑁 was leading to a contradiction, then it gets labeled 𝐼𝑁 . If
assigning the opposite label also leads to a contradiction, then the whole branch needs to be
backtracked.
3.3. Choosing an Argument to Split the Search
THEIA repeatedly chooses an argument 𝑎𝑟𝑔 that does not have a final label yet to split the
search. For this argument two labels are selected and propagated respectively. If 𝑎𝑟𝑔 had the
label 𝐵𝐿𝐴𝑁 𝐾, then the two labels need to be a final label and the opposite of the the final
label (either 𝐼𝑁 /𝑁 𝑂𝑇 𝐼𝑁 , 𝑂𝑈 𝑇 /𝑁 𝑂𝑇 𝑂𝑈 𝑇 or 𝑈 𝑁 𝐷𝐸𝐶/𝑁 𝑂𝑇 𝑈 𝑁 𝐷𝐸𝐶). If 𝑎𝑟𝑔 had an
intermediate label, then there are only two distinct labels 𝑎𝑟𝑔 can be relabeled to. For example
if 𝑎𝑟𝑔 had the label 𝑁 𝑂𝑇 𝑂𝑈 𝑇 , then 𝑙1 and 𝑙2 need to be 𝐼𝑁 and 𝑈 𝑁 𝐷𝐸𝐶.
During the look-ahead phase, all possible labels of all arguments with nonfinal labels were
already tested out and propagated. Therefore, for all arguments 𝑌 with nonfinal labels and
for any label 𝑋 such that 𝑌 can be relabeled to 𝑋 we know the amount 𝑍 such that when
assigning label 𝑋 to argument 𝑌 and propagating this label causes 𝑍 other arguments to be
assigned a label.
The knowledge about the amount 𝑍 for every argument-label combination is used as a
heuristic to decide how to split the search, in the sense that an argument-label combination is
chosen such that the lowest amount of remaining solving time is expected. An intuitive heuristic
would be to choose the argument-label combination such that the sum of propagated labels in
both branches is maximal. However, the remaining solving time of a branch usually increases
exponentially with the number of unlabeled arguments. Therefore, being able to propagate
𝑛 labels in both resulting branches is usually much better than propagation 2𝑛 labels in one
branch and 0 in the other. This idea motivated us to experiment with three other heuristics
elaborated in the results section.
3.4. Combining All Steps
The pseudocode outlining the system THEIA is shown in Algorithm 2. Given an argumenta-
tion framework 𝐴𝐹 the basecases are used first to find the initial labels of arguments. The
propagation rules are recursively used to propagate labels for each option and the algorithm
backtracks as soon as a contradiction is found. The look-ahead method is not only used to
detect contradictions, but also to determine additional label assignments. A complete set is
found as soon as all arguments got assigned final labels.
Note that opposed to Algorithm 1, during label-propagation there will never be a contradiction.
This is because the look-ahead method already detects if labeling any argument with any label
leads to a contradiction and prunes the branch accordingly.
An example of how the complete extensions of an argumentation framework are found is
shown in Figure 2.
116
Lukas Kinder et al. CEUR Workshop Proceedings 111–123
Algorithm 2 THEIA
procedure findComplete(𝐴𝐹 )
ℒ← − such that ℒ(𝑎) = 𝐵𝐿𝐴𝑁 𝐾 for all 𝑎 ∈ 𝒜
for all 𝑎 ∈ 𝒜 and all basecases 𝑏 do
if 𝑏 enforeces label 𝑙 on 𝑎 then
propagateLabel(𝐴𝐹, ℒ, 𝑏, 𝑙)
findCompleteRec(𝐴𝐹, ℒ)
procedure findCompleteRec(𝐴𝐹, ℒ)
if lookAhead(𝐴𝐹, ℒ) = CONTRADICTION then
return
if ℒ is a complete labeling then
print all labels with label 𝐼𝑁
return
Choose an argument 𝑎 that can be relabeled to 𝑙1 or 𝑙2 .
for 𝑙 ∈ {𝑙1 , 𝑙2 } do
propagateLabel(𝐴𝐹, ℒ, 𝑎, 𝑙)
findCompleteRec(𝐴𝐹, ℒ)
reverse label assignments by propagateLabels() and findCompleteRec()
procedure propagateLabel(𝐴𝐹, ℒ, 𝑎, 𝑙)
ℒ(𝑎) ← −𝑙
for all propagation rules 𝑝 do
for all 𝑏, 𝑙_𝑛𝑒𝑤 such that applying 𝑝 on 𝑎 enforces label 𝑙_𝑛𝑒𝑤 on 𝑏 do
propagateLabel(𝐴𝐹, ℒ, 𝑏, 𝑙𝑛𝑒𝑤 )
4. Experimental Evaluation
The goal of our experimental evaluation is to compare the runtime behaviour of THEIA with
existing solvers on the problem of enumerating complete extensions (i. e., on the track EE-CO
of the ICCMA competitions; see argumentationcompetition.org).
4.1. Experimental Setup
We evaluate the runtime performance on the same benchmark data as used in the ICCMA15
(192 instances) and ICCMA19 (326 instances) competitions (we did not use the benchmark data
from the ICCMA17 and ICCMA21 competitions, due to the size of the solutions for these data
sets and our resource restrictions).
THEIA is written in the C programming language and is not using any external libraries. We
used four different heuristics for selecting the next argument during search, giving rise to four
different variants of our THEIA solver:
117
Lukas Kinder et al. CEUR Workshop Proceedings 111–123
𝐶 = 𝑁 𝑂𝑇 𝐼𝑁 Basecase 2
𝐹 = 𝑁 𝑂𝑇 𝐼𝑁 look-ahead
𝐶 = 𝑈 𝑁 𝐷𝐸𝐶 Rule 5, from F
↘ 𝐹 = 𝑈 𝑁 𝐷𝐸𝐶
↙
𝐵 = 𝑁 𝑂𝑇 𝐼𝑁 Rule 10, from F
𝐹 = 𝑂𝑈 𝑇
𝐸 = 𝑁 𝑂𝑇 𝐼𝑁 Rule 10, from F
𝐴 = 𝑁 𝑂𝑇 𝑈 𝑁 𝐷𝐸𝐶 look-ahead
𝐴 = 𝑁 𝑂𝑇 𝑂𝑈 𝑇 Rule 5, from B
𝐵 = 𝑁 𝑂𝑇 𝑈 𝑁 𝐷𝐸𝐶 Rule 6, from A
𝐷 = 𝑁 𝑂𝑇 𝐼𝑁 Rule 4, from A
𝐷 = 𝑁 𝑂𝑇 𝑈 𝑁 𝐷𝐸𝐶 Rule 6, from A
𝐸 = 𝑈 𝑁 𝐷𝐸𝐶 Rule 5, from D
𝐸 = 𝑁 𝑂𝑇 𝑈 𝑁 𝐷𝐸𝐶 Rule 6, from D
𝐷 = 𝑈 𝑁 𝐷𝐸𝐶 Rule 9, from E
𝐴 = 𝑈 𝑁 𝐷𝐸𝐶 Rule 9, from D
𝐵 = 𝑈 𝑁 𝐷𝐸𝐶 Rule 3, from A
↓ ↘ Solution:[]
𝐸 = 𝐼𝑁 𝐸 = 𝑂𝑈 𝑇
𝐷 = 𝑂𝑈 𝑇 Rule 8, from E 𝐷 = 𝐼𝑁 Rule 7, from E
𝐴 = 𝐼𝑁 Rule 7, from D 𝐴 = 𝑂𝑈 𝑇 Rule 8, from D
𝐵 = 𝑂𝑈 𝑇 Rule 2, from A 𝐵 = 𝐼𝑁 Rule 1, from A
Solution:[𝐴, 𝐸] Solution:[𝐵, 𝐷]
Figure 2: An example of a search graph produced by THEIA when solving the argumentation framework
in Figure 1. Labeling argument 𝐹 to 𝐼𝑁 would force 𝐵 and 𝐸 to be labeled 𝑂𝑈 𝑇 , which would
consequently force 𝐴 and 𝐷 to be labeled 𝐼𝑁 . However, if 𝐴 is labeled 𝐼𝑁 , then 𝐷 should instead be
labeled 𝑂𝑈 𝑇 . This contradiction is found using the look-ahead strategy, which causes 𝐹 to be labeled
𝑁 𝑂𝑇 𝐼𝑁 .
• THEIAmin : Given an argument-label combination that can split the search, lets call the
"short branch" the branch that results in a lower amount of labels propagated than the
other branch. The 𝑚𝑖𝑛-heuristic is choosing the argument-label combination with the
longest short branch.
• THEIAsum : The argument-label combination is chosen that maximises the sum of propa-
gated labels in both resulting branches.
1
• THEIAexp : The solving time of a branch is estimated using 3 20 *𝑛𝐵𝐿𝐴𝑁 𝐾 *
1
2 20 *𝑛𝐼𝑁 𝑇 𝐸𝑅𝑀 𝐸𝐷𝐼𝐴𝑇 𝐸 with 𝑛𝐵𝐿𝐴𝑁 𝐾 being the number of arguments labeled 𝐵𝐿𝐴𝑁 𝐾
and 𝑛𝐼𝑁 𝑇 𝐸𝑅𝑀 𝐸𝐷𝐼𝐴𝑇 𝐸 being the number of arguments with intermediate labels. The
argument-label combination is chosen that minimizes the cumulative estimated solving
time of both resulting branches.
• THEIAadp : The idea of this heuristic is that it adapts itself to the given argumentation
𝑛𝐵𝐿𝐴𝑁 𝐾
framework. The solving time of a branch is estimated using (3 − 3 * 𝑎𝑣𝑔𝐸𝑟𝑟) 1+𝑑𝑒𝑐𝐵𝑙𝑎𝑛𝑘 *
𝑛𝐼𝑁 𝑇 𝐸𝑅𝑀 𝐸𝐷𝐼𝐴𝑇 𝐸
(2 − 2 * 𝑎𝑣𝑔𝐸𝑟𝑟) 1+𝑑𝑒𝑐𝐼𝑛𝑡𝑒𝑟𝑚𝑒𝑑𝑖𝑎𝑡𝑒 with 𝑛𝐵𝐿𝐴𝑁 𝐾 being the number of arguments labeled
𝐵𝐿𝐴𝑁 𝐾 and 𝑛𝐼𝑁 𝑇 𝐸𝑅𝑀 𝐸𝐷𝐼𝐴𝑇 𝐸 being the number of arguments with intermediate
labels. 𝑎𝑣𝑔𝐸𝑟𝑟 is the proportion of branches that are backtracked and 𝑑𝑒𝑐𝐵𝑙𝑎𝑛𝑘 and
𝑑𝑒𝑐𝐼𝑛𝑡𝑒𝑟𝑚𝑒𝑑𝑖𝑎𝑡𝑒 are the average number of arguments with a 𝐵𝐿𝐴𝑁 𝐾 or intermediate
label respectively, that are relabeled each iteration. The values 𝑎𝑣𝑔𝐸𝑟𝑟, 𝑑𝑒𝑐𝐵𝑙𝑎𝑛𝑘 and
𝑑𝑒𝑐𝐼𝑛𝑡𝑒𝑟𝑚𝑒𝑑𝑖𝑎𝑡𝑒 are initially 0, but these values get approximated while the solver is
exploring the search tree of a given argumentation framework.
We compared the runtime performance of these four THEIA solvers with 𝜇-toksia version
2019.04.07 [17] and HEUREKA version 0.2 [7]. The 𝜇-toksia solver is based on iterative SAT
calls and can be regarded as the state-of-the-art solver for that problem, since that version won
118
Lukas Kinder et al. CEUR Workshop Proceedings 111–123
the EE-CO track in ICCMA 2019 and the competition of 2021 did not feature the EE-CO track.
The solver HEUREKA can be regarded as a baseline for direct approaches to solve EE-CO.
We used probo2 (available at github.com/aig-hagen/probo2) as evaluation environ-
ment and conducted the experiments on a dedicated server with Intel Xeon CPUs (3.4 GHz,
only a single CPU was used) with 192 GB RAM and running Ubuntu 20.04.4. We set a 600s
CPU-time cutoff time, as used in the ICCMA competitions.
4.2. Results
Table 3 and Table 2 show the results for the two benchmark data sets ICCMA15 and ICCMA19,
respectively. For each solver we report the number of correctly solved instances (Corr), the
number of times the solver could not give the correct answer within the given time (TO) and
the cumulative runtime over solved instances (RT). The performances of the solvers are further
compared in Figures 3 and 4. We also provide scatter plots for both benchmark data sets
comparing THEIAexp and 𝜇-toksia which are shown in Figure 5a and 5b, respectively.
Table 2
Results for ICCMA 2015
Solver Corr TO RT
𝜇-toksia 192 0 1790
THEIAexp 189 3 8545
THEIAsum 188 4 9962
THEIAadp 187 5 9989
THEIAmin 145 47 1364
HEUREKA 139 53 1298
Table 3
Results for ICCMA 2019
Solver Corr TO RT
𝜇-toksia 326 0 601
THEIAexp 326 0 3061
THEIAsum 326 0 4146
THEIAadp 326 0 4214
THEIAmin 303 23 3808
HEUREKA 285 41 943
We observe that all versions of THEIA timed out a significantly smaller number of times than
HEUREKA. Except for THEIAmin the amount of timeouts was almost as good as 𝜇-toksia, but
𝜇-toksia still dominated in regard to the cumulative runtime over solved instances. However,
as the scatter plots 5a and 5b show, the runtime differences between THEIAexp and 𝜇-toksia
are rarely larger than one order of magnitude (those are instances outside of the green bar) and
there is also a number of instances where THEIAexp outperformed 𝜇-toksia. Although the
overall performance of THEIA is still below that of 𝜇-toksia we see the results as a significant
step forward in the development of direct argumentation solvers.
119
Lukas Kinder et al. CEUR Workshop Proceedings 111–123
Figure 3: Cactus plot of runtimes for the ICCMA 2015 benchmark.
Figure 4: Cactus plot of runtimes for the ICCMA 2019 benchmark.
5. Summary and Conclusion
In this paper we presented the system THEIA that extends current backtracking solvers for
abstract argumentation by means of more refined propagation techniques and look-ahead
strategies to find complete sets. The results show a clear improvement over the backtracking
120
Lukas Kinder et al. CEUR Workshop Proceedings 111–123
(a) ICCMA 2015 (b) ICCMA 2019
Figure 5: Scatter plot comparing the performance in runtime between 𝜇-toksia (x-axis) and THEIAexp
(y-axis). The task was to enumerate the complete extensions of the argumentation frameworks of the
ICCMA 2015 benchmark (a) and the ICCMA 2019 benchmark (b).
solver HEUREKA. We were also able to reduce the performance gap between SAT-based solvers
like 𝜇-toksia and direct solvers.
In future work, it would be interesting to investigate which types of argumentation frame-
works THEIA is better or worse than other solvers, as well as to analyse how much the different
implemented mechanisms contribute to the performance.
References
[1] T. J. Bench-Capon, P. E. Dunne, Argumentation in artificial intelligence, Artificial intelli-
gence 171 (2007) 619–641.
[2] P. Baroni, D. Gabbay, M. Giacomin, L. van der Torre, Handbook of Formal Argumentation,
London, England: College Publications, 2018.
[3] K. Atkinson, P. Baroni, M. Giacomin, A. Hunter, H. Prakken, C. Reed, G. Simari, M. Thimm,
S. Villata, Towards artificial argumentation, AI magazine 38 (2017) 25–36.
[4] F. H. van Eemeren, B. Garssen, E. C. W. Krabbe, A. F. Snoeck Henkemans, B. Verheij,
J. H. M. Wagemans, Handbook of Argumentation Theory, Springer, Berlin, 2014.
[5] P. M. Dung, On the acceptability of arguments and its fundamental role in nonmonotonic
reasoning, logic programming and n-person games, Artificial intelligence 77 (1995) 321–
357.
[6] P. Baroni, F. Toni, B. Verheij, Introduction to the special issue ‘On the acceptability of
arguments and its fundamental role in nonmonotonic reasoning, logic programming and
n-person games: 25 years later’, Argument & Computation 11 (2020) 1–14.
[7] N. Geilen, M. Thimm, Heureka: a general heuristic backtracking solver for abstract
argumentation, in: Proceedings of the 2017 International Workshop on Theory and
Applications of Formal Argument (TAFA’17), 2017, pp. 143–149.
[8] M. Thimm, Dredd-a heuristics-guided backtracking solver with information propagation
121
Lukas Kinder et al. CEUR Workshop Proceedings 111–123
for abstract argumentation, in: The Third International Competition on Computational
Models of Argumentation (ICCMA’19), 2019.
[9] S. Nofal, K. Atkinson, P. E. Dunne, Looking-ahead in backtracking algorithms for abstract
argumentation, International Journal of Approximate Reasoning 78 (2016) 265–282.
[10] S. Nofal, K. Atkinson, P. E. Dunne, Algorithms for decision problems in argument systems
under preferred semantics, Artificial Intelligence 207 (2014) 23–51.
[11] S. Nofal, K. Atkinson, P. E. Dunne, Algorithms for argumentation semantics: labeling
attacks as a generalization of labeling arguments, Journal of Artificial Intelligence Research
49 (2014) 635–668.
[12] S. Nofal, K. Atkinson, P. E. Dunne, I. O. Hababeh, A new labelling algorithm for generating
preferred extensions of abstract argumentation frameworks, in: ICEIS, 2019.
[13] M. W. Caminada, D. M. Gabbay, A logical account of formal argumentation, Studia Logica
93 (2009) 109–145.
[14] M. Kröll, R. Pichler, S. Woltran, On the complexity of enumerating the extensions of abstract
argumentation frameworks, in: Proceedings of the 26th International Joint Conference on
Artificial Intelligence (IJCAI’17), 2017.
[15] A. Biere, M. Heule, H. van Maaren, T. Walsh (Eds.), Handbook of Satisfiability, volume 185
of Frontiers in Artificial Intelligence and Applications, IOS Press, 2009.
[16] F. Cerutti, S. A. Gaggl, M. Thimm, J. P. Wallner, Foundations of implementations for formal
argumentation, in: Handbook of Formal Argumentation, College Publications, 2018.
[17] A. Niskanen, M. Järvisalo, 𝜇-toksia: An efficient abstract argumentation reasoner, in:
Proceedings of the International Conference on Principles of Knowledge Representation
and Reasoning, volume 17, 2020, pp. 800–804.
122
Lukas Kinder et al. CEUR Workshop Proceedings 111–123
Appendix
(a) Basecase 1
(b) Basecase 2 (c) Basecase 3
Figure 6: A collection of structures of arguments that enforce a label on the node marked with "?".
Nodes with a thick border are necessary, nodes with a thin boarder are optional.
(a) Rule 1 (b) Rule 2 (c) Rule 3 (d) Rule 4
(e) Rule 5 (f) Rule 6 (g) Rule 7 and 13 (h) Rule 8
(k) Rule 11
(i) Rule 9 and 14 (j) Rule 10 and 15 (l) Rule 12 and 16
Figure 7: A collection of structures of arguments that enforce a label on the node marked with "?". A
Nodes with a thick border represent one or more arguments with a specific label. Nodes with a thin
boarder mark zero or more arguments with a specific label. The "[...]" marks arguments that can have
any label.
123