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.
← ↓ → → ↑
↙ →↘ 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 techniques, 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.
An abstract argumentation framework [
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 [
A variant of the above set-based interpretation of argumentation frameworks, is the
labellingbased interpretation [
ℒ : →↦− { , , } 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 ∈ (ℒ). • 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 [
In this work, we are interested in the problem of enumerating all complete extensions of a given
abstract argumentation framework , which is highly intractable [
The above-mentioned systems are referred to as direct solvers, which directly work within
the formalism of abstract argumentation to solve problems [
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 ifndComplete( )
Our algorithm is following the basic structure of Algorithm 1. However, THEIA difers 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.
The procedure propagateLabels corresponds to unit propagation in SAT-solving [
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 diference is that the label assignment of the argument that causes the rule to apply, is at a diferent 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
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 [
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.
The pseudocode outlining the system THEIA is shown in Algorithm 2. Given an argumentation 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. Algorithm 2 THEIA procedure findComplete( ) ℒ− ← such that ℒ() = for all ∈ for all ∈ and all basecases do if enforeces label on then
propagateLabel(, ℒ, , ) ifndCompleteRec( , ℒ) 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(, ℒ, , ) ifndCompleteRec( , ℒ) 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(, ℒ, , )
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).
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 diferent heuristics for selecting the next argument during search, giving rise to four diferent variants of our THEIA solver: = = look-ahead = Rule 6, from A = Rule 6, from A = Rule 6, from D
↙ =↓ = Rule 8, from E = Rule 7, from D = Rule 2, from A
Solution:[, ] = Basecase 2 = look-ahead = Rule 5, from F ↘
= = Rule 7, from E = Rule 8, from D = Rule 1, from A
Solution:[, ] ↘ = = Rule 10, from F = Rule 10, from F = Rule 5, from B = Rule 4, from A = Rule 5, from D = Rule 9, from E = Rule 9, from D = Rule 3, from A
Solution:[]
• 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 propagated labels in both resulting branches.
The solving time of a branch is estimated using 3 210 * * • THEIAexp: 2 210 * 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 [
We used probo2 (available at github.com/aig-hagen/probo2) as evaluation environment 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 cutof time, as used in the ICCMA competitions.
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.
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 diferences 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.
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 (a) ICCMA 2015 (b) ICCMA 2019 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 frameworks THEIA is better or worse than other solvers, as well as to analyse how much the diferent implemented mechanisms contribute to the performance.
(a) Basecase 1