Instantiations and Computational Aspects of Non-Flat Assumption-based Argumentation

1 Introduction

Formal argumentation constitutes a prominent branch of AI that studies and develops computational approaches to reason argumentatively [Baroni et al., 2018]. The heterogeneity of this field is reflected in various formalizations and application domains, such as legal reasoning, medical sciences, and e-democracy [Atkinson et al., 2017]. Computational approaches to solve key reasoning tasks are critical to the deployment of formal argumentation.

Argumentation formalisms are often classified as either abstract or structured . Abstract argumentation [Dung, 1995] is concerned with acceptability of arguments based exclusively on the relations between them. Structured argumentation formalisms [Besnard et al., 2014] capture an entire argumentative workflow [Caminada and Amgoud, 2007]: starting from knowledge bases, a process of argument generation or instantiation is prescribed, upon which semantics can be deployed to find acceptable arguments or conclusions thereof.

Computational approaches to structured argumentation have gained increased attention in the research community. The biannual International Competition on Computational Models of Argumentation (ICCMA) [Thimm and Villata, 2017; Gaggl et al., 2020; Lagniez et al., 2020; Bistarelli et al., 2021; J¨arvisalo et al., 2023] has recently included a dedicated track for assumption-based argumentation (ABA) [Bondarenko et al., 1997]-one of the prominent approaches to structured argumentation . Several algorithmic approaches to ABA or other well-known structured argumentation formalisms like ASPIC+ [Modgil and Prakken, 2013] have been proposed recently [Craven and Toni, 2016; Lehtonen et al., 2017; Bao et al., 2017; Karamlou et al., 2019; Lehtonen et al., 2020; Lehtonen et al., 2021a; Lehtonen et al., 2021b; Diller et al., 2021; Lehtonen et al., 2022b; Thimm, 2017; Lehtonen et al., 2022a; Lehtonen et al., 2023].

Within this surge of algorithmic efforts, many solutions focus on restricted fragments of structured argumentation. For instance, most algorithms for ABA (e.g. [Craven and Toni, 2016; Lehtonen et al., 2021a; Diller et al., 2021]) focus on the flat ABA fragment, which imposes a strong restriction on the knowledge base by excluding derivations of 'assumptions'. The general ABA language, not restricted to the flat fragment and referred to in this paper as non-flat ABA, is able to capture more expressive settings such as auto-epistemic reasoning [Bondarenko et al., 1997] and multi-agent settings where merging information from different sources can result in a non-flat knowledge base [Ulbricht et al., 2024]. More broadly, non-flat ABA can capture situations where dependencies between assumptions need to be taken into account, and is therefore strictly more expressive than flat ABA. However, the few algorithms for non-flat ABA heavily restrict the kind of ABA frameworks (ABAFs) to which they apply (in [Karamlou et al., 2019] to bipolar ABA frameworks [Cyras et al., 2017]). A possible reason for the focus on flat ABA is the lower computational complexity. As shown by Dimopoulos et al. (2002) and ˇCyras et al. (2021a), all major reasoning tasks exhibit a one level jump in the polynomial hierarchy when going from flat to non-flat ABA, which, again, reflects the increased expressiveness of the general (not-flat) case.

In this paper we fill this gap and address computational challenges of non-flat ABA. In particular, we investigate algorithmic approaches to reasoning in non-flat ABA, establish new theoretical insights and evaluate them in practice.

Algorithms for flat ABAFs can be divided into (i) instantiating a semantics-preserving argumentation framework (AF) [Dung, 1995] and then performing the reasoning task in the AF; and (ii) direct approaches operating on the given ABAF without instantiation. There are benefits to instantiation-based approaches, such as explainability in the form of more abstract, cognitively tractable explanations [ ˇCyras et al., 2021b]. For performance, direct approaches, specifically ones using modern declarative methods, such as answer set programming (ASP) [Gelfond and Lifschitz, 1988; Niemel¨a, 1999], typically have an edge over instantiation-based solvers in structured argumentation (e.g. [Lehtonen et al., 2021a; Lehtonen et al., 2023]). However, in the case of non-flat ABA this might plausibly not be the case. A recent instantiation [Ulbricht et al., 2024] translates a given non-flat ABAF into a bipolar AF (BAF) [Amgoud et al., 2008] such that reasoning in the constructed BAF is computationally milder compared to the initial ABAF . This is in contrast to the classical translation of flat ABAFs into AFs, where the complexity of reasoning is as high for the AFs.

In this work, we study the advantage this lower complexity can give for reasoning in non-flat ABAFs via instantiation to BAFs. While ideally the resulting BAF would be of polynomial size, similarly to a recently proposed translation from flat ABA to AF [Lehtonen et al., 2023], we show that this is impossible in non-flat ABA. Instead, we investigate redundancies that can be eliminated to optimize the instantiation.

In more detail, our main contributions are:

• We present a result based on compilability theory, suggesting that an instantiation in BAFs cannot avoid an exponential number of arguments. Section 3.1
• Motivated by the lower complexity in instantiated BAFs compared to non-flat ABAFs, we show how to efficiently instantiate BAFs. We present three redundancy notions for argument generation. Section 3.2
• Towards a greater reach for applications, we also identify fragments of non-flat ABA with milder complexity: atomic and additive non-flat ABAFs. Section 3.3
• We propose two algorithmic approaches for reasoning in non-flat ABAFs. The first one efficiently instantiates a BAF via ASP using our redundancy notions, followed by SAT-based reasoning on the BAF. Section 4
• The second one performs reasoning directly on the given non-flat ABAF using iterative ASP calls, similarly to state-of-the-art approaches for other beyond-NP structured argumentation problems. Section 5
• We show empirically that both algorithms are competitive, with relative performance depending on the benchmark set. This contrasts with the dominance of noninstantiation approaches for other structured argumentation formalisms. Section 6

We focus on complete, grounded, stable and a completebased version of preferred semantics. In a technical appendix [Lehtonen et al., 2024], we expand on proof details, encodings, and how to approach admissible-based semantics, which was shown to be more involved [Ulbricht et al., 2024].

2 Background

We recall preliminaries for assumption-based argumentation frameworks (ABAFs) [Bondarenko et al., 1997; ˇCyras et al., 2018], bipolar argumentation frameworks (BAFs) [Amgoud et al., 2008], instantiation of BAFs to capture ABAFs [Ulbricht et al., 2024] and basics of computational complexity

.

Assumption-based Argumentation. We assume a deductive system (L, R), with L restricted to a set of atoms and R a set of rules over L. A rule r∈R has the form a0←a1, . . . , an with ai ∈L. We denote the head of r by head(r) = a0 and the (possibly empty) body of r with body(r) = {a1, . . . , an}. Definition 2.1. An ABAF is a tuple (L,R,A, ), where (L,R) is a deductive system, A ⊆ L is a non-empty set of assumptions, and : A→L is a (total) contrary function.

Here, we focus on finite ABAFs, i.e., L and R are finite.

An atom p ∈ L is derivable from assumptions S ⊆ A and rules R⊆R, denoted by S ⊢R p, if there is a finite rooted labeled tree G such that the root is labeled with p, the set of labels for the leaves of G is S or S ∪ {⊤}, and for every inner node v of G there is a rule r ∈ R such that v is labelled with head(r), the number of children of v is |body(r)| and every child of v is labelled with a distinct a ∈ body(r) or ⊤ if body(r) = ∅. We call such a G a tree-based argument. A sub-argument of G is a finite rooted labelled sub-tree G′ such that the leafs of G′ are a subset of the leafs of G. We will denote with AD the set of all tree-based arguments of an ABAF D. Following Toni (2014), we will often compactly denote a tree-based argument with root p and leafs S as S ⊢ p.

For S ⊆A, we let S = {a | a ∈ S}. By ThD(S) = {p ∈ L | ∃S′ ⊆S : S′ ⊢R p} we denote the set of all conclusions derivable from S. Note that S ⊆ ThD(S) as each a ∈A is derivable via {a} ⊢∅ a. For S ⊢ p ∈AD, we let asms(S ⊢ p)=S; for E⊆AD we let asms(E) = ⋃x∈E asms(x).

Definition 2.2. Let D = (L,R,A, ) be anABAF, S, T ⊆A, and a ∈ A. The closure cl (S) of S is cl (S)=ThD(S)∩A. S is closed iff S = cl (S); S attacks T iff b ∈ ThD(S) for some b ∈ T; S defends a iff for each closed V ⊆ A s.t. V attacks a, S attacks V ; S defends itself iff S defends each b ∈ S.

An ABAF where each set of assumptions is closed is called flat. We refer to an ABAF not restricted to be flat as non-flat. For a ∈ A, we also say S attacks a if S attacks the singleton {a}, and we write cl (a) instead of cl ({a}).

A set S ⊆ A is conflict-free in D, denoted E ∈ cf (D), if E is not self-attacking; S is admissible, denoted S ∈ adm(D), if S is closed, conflict-free and it defends itself. We focus on grounded, complete, ⊆-maximal complete, and stable ABA semantics (abbr. grd, com, prf ′ , stb), as follows. 1

Definition 2.3. Let D = (L,R,A, ) be an ABAF and S ⊆ A be a set of assumptions s.t. S ∈ adm(S). We say

1 In the paper we show results for grd, com, stb and prf ′ defined as ⊆-maximal complete sets (a variant to the usual prf semantics given as ⊆-maximal admissible sets). We give results for adm and the standard prf in [Lehtonen et al., 2024]. Although the intersection of all complete sets has been originally termed well-founded semantics [Bondarenko et al., 1997], we stick to the usual convention in the argumentation literature and call it "grounded".

• S ∈ com(D) iff it contains every T ⊆ A it defends,
• S ∈ prf ′ (D) iff S is ⊆-maximal in com(D),
• S ∈ grd(D) iff S = ⋂T∈com(D) T, and
• S ∈ stb(D) iff S attacks each x ∈ A \ S.

In this paper we stipulate that the empty intersection is interpreted as ∅, thus if com(D) = ∅, then grd(D) = ∅.

Example 2.4. We let D be an ABAF with assumptions A = {a, b, c}, rules R = {(p ← a), (q ← b), (c ← p, q)}, and b = p. The set {a, c} is (⊆-maximal) complete and stable in D since {a, c} is unattacked and {a} attacks b. Note that {a, b} is not closed since cl ({a, b}) = {a, b, c}.

Bipolar Argumentation. Bipolar argumentation features adversarial and supportive relations between arguments.

Definition 2.5. A bipolar argumentation framework (BAF) F is a tuple F = (A, Att, Sup) where A represents a set of arguments, Att ⊆ A × A models attack, and Sup ⊆ A × A models support between them.

Thus, in the tradition of Dung's abstract argumentation frameworks (AFs) (1995), arguments in BAFs are considered abstract, but BAFs extend AFs by integrating support. We call F = (A, Att) the underlying AF of F = (A, Att, Sup). For two arguments x, y ∈ A, if (x, y) ∈ Att ((x, y) ∈ Sup) we say that x attacks (supports) y as well as x attacks (supports) (the set) E ⊆ A given that y ∈ E.

We utilize the BAF semantics introduced by Ulbricht et al. (2024). For a set E ⊆ A, we let cl(E) = E ∪ {a ∈ A | ∃e ∈ E : (e, a) ∈ Sup}. The set E is closed if E = cl(E); E is conflict-free in F, denoted E ∈ cf (F), if for no x, y ∈ E, (x, y) ∈ Att; E defends a ∈ A if E attacks each closed set S ⊆ A which attacks a. The characteristic function of F is Γ(E) = {a ∈ A | E defends a}. We say E is admissible, denoted E ∈ adm(F), if E is closed, conflictfree, and E ⊆ Γ(E).

Definition 2.6. Let F be a BAF. For a set E ∈ adm(F),

• E ∈ com(F) iff E = Γ(E);
• E ∈ grd(F) iff E = ⋂S∈com(F) S;
• E ∈ prf ′ (F) iff E ⊆-maximal in com(F);
• E ∈ stb(F) iff E attacks all a ∈ A \ E.

ABA and Bipolar Argumentation. Each ABAF can be captured as a BAF as follows [Ulbricht et al., 2024].

Definition 2.7. For an ABAF D = (L,R,A, ), the instantiated BAF FD = (A, Att, Sup) is given by A = AD and

Example 2.8. The ABAF from Example 2.4 yields the following BAF, with attacks as solid and supports as dashed lines, and arguments depicted as trees (with root at the top).

This BAF construction captures semantics for ABAFs, as recently shown [Ulbricht et al., 2024].

Theorem 2.9. Let D be an ABAF, FD = (A,Att, Sup) the associated BAF, and σ ∈ {com, prf ′ , grd, stb}. Then

• if E ∈ σ(FD), then asms(E) ∈ σ(D), and
• if S ∈ σ(D), then {x ∈ A | asms(x) ⊆ S} ∈ σ(FD).

Computational Complexity. We assume the reader to be familiar with the polynomial hierarchy. We focus on the credulous reasoning task. For a BAF F and a semantics σ, an argument a ∈ A is credulously accepted if a ∈ E for some E ∈ σ(F); for an ABAF D and a semantics σ, a conclusion p ∈ L is credulously accepted if p ∈ ThD(E) for some E ∈ σ(D). The induced decision problems are denoted by CredBAF σ and CredABA σ , respectively. We note that CredCcom = CredCprf ′ for C ∈ {BAF,ABA}.

Deciding credulous reasoning for non-flat ABA is Σ P2 - complete for complete, DP2-complete for grounded, and NP-complete for stable semantics [Dimopoulos et al., 2002; ˇCyras et al., 2021a]. As recently shown [Ulbricht et al., 2024], the corresponding decision problems for BAFs exhibit lower complexity for main semantics: DP-completeness for grounded and NP-completeness for complete and stable.

3 BAF Generation in Theory

For instantiation-based algorithms the number of arguments is critical for the run time performance. Direct instantiation methods which compute all tree-based arguments may yield unfeasibly large argumentation graphs. This has already been pointed out for flat ABA, which motivated the study of means to reduce their size [Lehtonen et al., 2023]. In this section, we analyze redundancies for the non-flat case as well. However, our first observation is that the computation of exponentially many arguments can in general not be avoided for non-flat ABA. A result of this kind is, to the best of our knowledge, novel for structured argumentation.

3.1 A Lower Bound For Non-Flat Instantiations

We give a formal line of reasoning that it is impossible to instantiate a given non-flat ABAF in a "reasonable" way and thereby obtain a polynomial-sized graph (i.e., AF or BAF).

In more detail, we show a complexity result based on compilability theory [Cadoli et al., 2002] stating that, unless the polynomial hierarchy collapses, one cannot transform a given non-flat ABAF D into some structure χ with the following properties: i) χ is of polynomial size w.r.t. D; and ii) in χ one can decide in polynomial time whether a given set E of assumptions is admissible or complete in D. Since verifying admissible sets in non-flat ABA is NP-complete, it is clearly impossible to construct such χ in polynomial time. However, we do not need this restriction. That is, even given exponential time, such χ cannot be constructed. Conceptually, this result excludes usual argument-centric instantiations of D into AFs or BAFs, because here we expect checking whether a set of arguments is admissible to be tractable.

That is, under complexity theoretic assumptions, our result states that it is impossible to apply instantiations of D into a polynomial-sized AF or BAF which have the usual correspondences between sets of arguments and sets of assumptions.

Theorem 3.1. Unless the polynomial hierarchy collapses one cannot transform a non-flat ABAF into a polynomial-sized AF or BAF from which one can in polynomial-time decide whether a given set of assumptions is admissible or complete.

3.2 Towards Feasible BAF Instantiations

The previous subsection shows that instantiation of non-flat ABAFs will require exponentially many arguments in general. We strive to construct as few as possible nonetheless. We identify three redundancy notions to reduce the number of arguments. We consider an arbitrary but fixed semantics σ ∈ {com, grd, stb, prf ′ } throughout this subsection.

DerivationRedundancy. We call the first notion derivation redundant arguments as it spots "inefficient" derivations.

Definition 3.2. For an ABAF D and its set of arguments AD, we call an argument (S ⊢ p) ∈ AD derivation redundant iff there is an argument (S′ ⊢ p) ∈ AD with S′ ⊊ S.

Example 3.3. Recall Example 2.4. Suppose we consider an ABAF D′ by setting R′ = R ∪ {c ← p}. Then we would obtain a new argument {a} ⊢ c. Then the existing argument A3 representing {a, b} ⊢ c becomes derivation redundant.

We observe that derivation redundant arguments can be removed without altering the sets of accepted assumptions.

Proposition 3.4. Let D be an ABAF and FD the corresponding BAF. Let x ∈ AD be derivation redundant and let G be the BAF after removing the argument x from FD. Then

Expendable Arguments. We derive another redundancy notion based on the conclusion of arguments: if x = (S ⊢ p) is an argument where p is neither an assumption nor a contrary, then x merely represents an intermediate derivation step. Arguments of this kind do not need to be instantiated if one is interested in assumption extensions only.

Definition 3.5. For an ABAF D and its set of arguments AD we call an argument (S ⊢ p) ∈ AD expendable iff p /∈ A∪A.

Example 3.6. In our Example 2.4, for instance the argument A2 representing {b} ⊢ q is expendable since q is neither a contrary nor an assumption.

Since arguments of this kind have no out-going attacks, they do not contribute to the semantics of the instantiated BAF. However, keep in mind that we still construct relevant super-arguments of expendable ones.

Proposition 3.7. Let D be an ABAF and FD the corresponding BAF. Let x ∈ AD be an expendable argument and let G be the BAF after removing the argument x from FD. Then

Assumption Redundancy. This final redundancy notion is specific to non-flat ABAFs. It states that arguments that make use of assumptions in intermediate steps can be neglected. This requires rules with assumptions in their head and is thus not possible for flat ABA.

Definition 3.8. For an ABAFD = (L,R,A, ) and its set of arguments AD, an argument x = (S ⊢ p) ∈ AD is assumption redundant iff it contains a sub-argument x′ s.t.

• x′ is a proper sub-argument of x, i.e., x′ ̸= x,
• x is of the form S′ ⊢ a where S′ ⊆ S and a ∈ A.

Example 3.9. Suppose we augment Example 2.4 with the additional rule "a ← b". This would lead to a novel argument A7 for p by first applying the rule "a ← b" and then "p ← a". However, since a is an assumption itself, it is more efficient to infer p from a directly, which is represented by the argument A1. Thus A7 would be assumption redundant.

As for the other redundancy notions, arguments of this kind can be removed without altering the semantics.

Proposition 3.10. Let D be an ABAF and FD the corresponding BAF. Let x ∈ AD be an assumption redundant ar-

Summary. With our redundancy notions, the instantiated BAF can be reduced as follows. From AD we construct the set A∗D of non-redundant arguments by i) first removing all derivation redundant arguments from AD; ii) then removing all expendable arguments from the result of i); and finally iii) removing all assumption redundant arguments from the result of ii). Now we define the redundancy-free core of D.

Definition 3.11. Let D = (L,R,A, ) be an ABAF. The BAF G = (A,Att, Sup) is the non-redundant core of D where A = {(S, p) | S ⊢ p is an argument in A∗D }, Att is the set of all attacks between arguments in A, and Sup is the set of all supports between arguments in A.

Due to Propositions 3.4, 3.7 and 3.10 this representation is semantically equivalent.

Corollary 3.12. Let D be an ABAF and FD its corresponding BAF. If G is the redundancy-free core of D, then we have that {asms(E) | E ∈ σ(FD)} = {asms(E) | E ∈ σ(G)}.

By our previous results, the non-redundant core preserves the semantics of the given ABAF, since only redundant arguments are omitted and the representation streamlined. By applying this representation, we still have exponentially many arguments in general, but finiteness is guaranteed.

Proposition 3.13. The redundancy-free core G of an ABAF D has at most |2A| · |L| arguments.

3.3 Fragments

As we just saw, non-flat ABA instantiations will in general have exponentially many arguments. In this subsection, we investigate fragments inducing fewer arguments. Since reasoning in BAFs is milder than in non-flat ABAFs, we expect such fragments to admit lower complexity. Indeed, if the core computation is polynomial, then the complexity drops.

Proposition 3.14. Let C be a class of ABAFs s.t. the nonredundant core of D can be computed in polynomial time. Then, the computational complexity of reasoning problems in D is not harder than in the instantiated BAF, i.e., CredABA σ is in NP for σ ∈ {adm, com, prf ′ , stb} and in DP for σ = grd .

Indeed, in our empirical evaluation in Section 6 we will see that these fragments are milder in practice as well.

Atomic ABAFs The first fragment we consider is atomic, which has been studied for flat ABA as well [Rapberger and Ulbricht, 2023; Lehtonen et al., 2023]. For an ABAF to be atomic, each rule body element has to be an assumption.

Definition 3.15. Let D = (L,R,A, ) be an ABAF. A rule r ∈ R is called atomic if body(r) ⊆ A. The ABAF D is called atomic if each rule r ∈ R is atomic.

For flat ABA, this means that D has |R| + |A| arguments (each rule induces exactly one tree-based argument) [Lehtonen et al., 2023]. In contrast, the same is not immediate for non-flat ABA as the derivation of assumptions is allowed. Nevertheless, due to our notion of assumption redundancy from Definition 3.8, we can show that the number of nonredundant arguments is indeed linear in D.

Proposition 3.16. The non-redundant core of atomic ABAFs D consists of at most |R| + |A| many arguments.

Example 3.17. Consider an ABAF D with A = {a, b, c}, rules R = {(p ← a), (q ← b), (a ← c)}, and an arbitrary contrary function. D is atomic since each rule body consists of assumptions. While it is possible to construct more that |R| + |A| arguments (by applying "a ← c" and then "p ← a"), these additional arguments are assumption redundant.

As a consequence, Proposition 3.14 applies to the class of atomic ABAFs, inducing lower complexity of reasoning.

Additive Closure In an atomic ABAF, each non-redundant argument has a derivation depth of 1. We can also bound the body size of rules, obtaining so-called additive ABAFs.

Definition 3.18. We call an ABAF D = (L,R,A, ) additive if for each rule r ∈ R it holds that |body(r)| ≤ 1.

The reason for calling ABAFs of this kind additive is that they induce an additive ThD mapping, that is, for each set S of assumptions, ThD(S) = ⋃s∈S ThD(s).

Example 3.19. Consider an ABAF D with A = {a, b, c}, L = A ∪ {p, q, r, s}, rules R = {(p ← a), (q ← b), (r ← p), (s ← q)}, and an arbitrary contrary function. This ABAF is additive since each rule body has size one. Consequently, each constructible argument is based on one assumption only (in contrast to e.g. A3 in Example 2.8 relying on a and b).

Note that Bipolar ABA [Cyras et al., 2017] is a special kind of non-flat ABA restricted to being both atomic and additive.

As suggested by the previous example, each argument in an additive ABAF has the form {} ⊢ p or {a} ⊢ p for some assumption a. This induces the following bound.

Proposition 3.20. The non-redundant core of an additive ABAF D consists of at most (|A| + 1) · |L| many arguments.

Also in this case, Proposition 3.14 is applicable, including the computational benefits of lower complexity.

4 Algorithms for Non-flat ABA via BAFs

We introduce an approach for solving reasoning problems in non-flat ABA by instantiating a BAF and solving the corresponding reasoning problem in the BAF. We focus on credulous reasoning for complete (and so preferred′ ) and stable semantics. We employ efficient declarative methods, namely Listing 1: ProgramΠgen arg

1 {in(X) : assumption(X)}. 2 derivable(X) ← assumption(X), in(X). 3 derivable(X) ← head(R,X), usable_rule(R). 4 usable_rule(R) ← head(R,_), derivable(X) : body(R,X).

answer set programming (ASP) [Gelfond and Lifschitz, 1988; Niemel¨a, 1999] for generating arguments, and Boolean satisfiability (SAT) [Biere et al., 2021] for BAF reasoning.

4.1 BAF Generation

We introduce a novel approach for generating non-redundant arguments (see Section 3.2) from an ABAF, using the stateof-the-art ASP solver CLINGO [Gebser et al., 2016].

Firstly, we present an ABAF D = (L,R,A, ) with R = {r1, . . . , rn} in ASP as follows.

ABA(D) ={assumption(a). | a ∈ A} ∪ {head(i, b). | ri ∈ R, b = head(ri)} ∪ {body(i, b). | ri ∈ R, b ∈ body(ri)} ∪ {contrary(a, b). | b = a, a ∈ A}.

Then, we introduce the ASP program Πgen arg (see Listing 1), which by itself enumerates each assumption set and determines what can be derived from it. The following procedure limits redundancy in the set of arguments. 2 Firstly, by Proposition 3.4, we eliminate derivation redundant arguments. We use CLINGO heuristics [Gebser et al., 2013] for this, adding the heuristic that each assumption is by default not in. Secondly, by Proposition 3.7, one retains semantic equivalence even if expendable arguments are ignored. As we are interested in credulous acceptance, we also construct arguments for atoms whose acceptance we want to query. Optionally, instead of a query atom, a set of atoms can be specified, so that the acceptance of any of these atoms can be decided from a single BAF. We enumerate answers to ABA(D) ∪ Πarg gen together with a constraint that derivable(a) holds, for each atom of interest a, resulting in answer sets corresponding to non-derivation redundant, nonexpendable arguments for a. The attack and support relations over the arguments can be straightforwardly determined based on the assumptions and conclusion of each argument.

4.2 SAT Encodings for BAFs

We move on to proposing SAT encodings that capture the BAF semantics of interest , following Definition 2.6. Our encodings are based on the standard SAT encodings for AFs [Besnard and Doutre, 2004] with modifications to capture the additional aspects of BAFs. Given a BAF F = (A, Att, Sup) and the closure cl(a) of each argument a ∈ A (which can be precomputed in polynomial time), we capture conflict-free, closed, self-defending, and complete sets of arguments, respectively, as follows. We use variables xa for a ∈ A to denote that a is in the extension.

Conflict-freeness is encoded as for AFs: cf(F) = ∧(a,b)∈Att (¬xa ∨ ¬xb). For closedness, if an argument a is in an extension, then each argument b that a supports must be in the extension, too: closed(F) = ∧(a,b)∈Sup (¬xa∨xb).

2 We chose to include assumption redundant arguments still, leaving their elimination to future work.

Note that a set of arguments E defends an argument b if and only if E attacks the closure of every argument a that attacks b [Ulbricht et al., 2024, Lemma 3.4]. Thus an extension E defends itself iff it holds that, if b ∈ E, then for each a that attacks b, some argument d that attacks an argument c in the closure of a must be in the extension.

For a complete extension E, any argument b must be in E if it holds that an argument in the closure of each argument a that attacks b is attacked by an argument in the extension.

Taken together, we encode complete semantics by com(F) = cf(F) ∧ closed(F) ∧ self defense(F) ∧ defended(F).

To decide credulous acceptance under σ ∈ {com, stb} , we add the clause cred(F, α) = ∨a∈Aα xa where Aα ⊆ A is the set of arguments concluding α.

Proposition 4.1. Given an ABAF D = (L,R,A, ), σ ∈ {com, stb} and α ∈ L, let F be the BAF constructed from D via the procedure of Section 4.1. Then σ(F) ∧ cred(F, α) is satisfiable iff α is credulously accepted under σ.

5 ASP Algorithms for Non-flat ABA

In this section we introduce an ASP-based approach for credulous acceptance in non-flat ABA without constructing arguments. We propose a counterexample-guided abstraction refinement (CEGAR) [Clarke et al., 2004; Clarke et al., 2003] algorithm for complete semantics, inspired by stateof-the-art algorithms for other problems in structured argumentation, including flat ABA, that are hard for the second level of the polynomial hierarchy [Lehtonen et al., 2021b; Lehtonen et al., 2022b; Lehtonen et al., 2022a]. For stable semantics, we propose an ASP encoding , reflecting the fact that credulous acceptance is NP-complete under stable semantics.

We use ASP to generate candidates based on an abstraction of the original problem, and another ASP solver to verify whether a counterexample to the candidate being a solution exists. We use the ASP encoding of ABAFs from Section 4.1, and the notation solve(Π) to refer to solving the ASP program Π and assume that solve(Π) either returns an answer set or reports that the program is unsatisfiable. Details of the ASP programs are available in [Lehtonen et al., 2024].

We introduce Algorithm 1 for credulous acceptance under complete semantics. As subprocedures, we introduce Algorithm 1: Credulous acceptance, complete semantics

Require: ABA framework F = (L,R,A, ), s ∈ L

Ensure: return YES if s is credulously accepted under complete semantics in F , NO otherwise

• 1: while C := solve(Πabs) do
• 2: flag := T
• 3: if solve(Πnot adm(C)) unsatisfiable then
• 4: for a ∈ A s.t. a /∈ C and a not attacked by C do
• 5: if solve(Πdefends(C, a)) then flag := F; break
• 6: if flag = T then return YES
• 7: Add constraint excluding C to Πabs
• 8: return NO

three ASP programs: the abstraction Πabs , a program that checks for a counterexample to admissibility Πnot adm, and Πdefends(C, a) for checking counterexamples to completeness, i.e., if particular assumptions are defended. The abstraction Πabs admits as answers closed and conflict-free assumption sets from which the query is derivable, along with a stronger condition for complete semantics. Namely, if an assumption is not in the candidate and not attacked by the set of undefeated assumptions, the candidate cannot be complete (since this assumption cannot be attacked by any closed assumption set in particular, and is thus defended by the candidate). The program Πnot adm is satisfiable iff a closed set of assumptions that is not attacked by the candidate attacks the candidate, implying that the candidate is not admissible. Finally, given a candidate C ⊆ A and an assumption a ∈ A, the program Πdefends(C, a) is satisfiable iff there is a set of assumptions that is not attacked by C, is closed, and attacks a. In such a case the candidate does not defend a.

Algorithm 1 iteratively generates candidates (Line 1) and checks admissibility (Line 3). In case a candidate is admissible, it is further checked whether there is an assumption that is not in the candidate or attacked by the candidate (Line 4), such that this assumption is defended by the candidate (Line 5). If not, the candidate is complete and thus the queried atom is credulously accepted (Line 6). Otherwise (if C is either not admissible or not complete) the abstraction is refined by excluding the candidate from further consideration (Line 7). Finally, if no complete assumption set is found, the queried atom is not credulously accepted (Line 8).

Proposition 5.1. Given an ABAF D = (L,R,A, ) and a query α ∈ L, Algorithm 1 outputs YES if and only if α is credulously accepted under complete semantics in D.

Stable semantics can be encoded by slightly adapting the encoding for flat ABAFs [Lehtonen et al., 2021a]. Namely, we add a constraint for the assumption set being closed. For finding the credulous acceptance of s ∈ L, we add a constraint requiring that s is derivable from the assumption set.

6 Empirical Evaluation

We present an evaluation of the algorithms proposed in Sections 4 and 5, named ABABAF 3 and ASPFORABA 4 , respectively. We implemented both approaches in Python, using CLINGO (version 5.5.1) [Gebser et al., 2016] for ASPFORABA and for generating the arguments in ABABAF. We used PYSAT (version 0.1.7) [Ignatiev et al., 2018] with GLUCOSE (version 1.0.3) [Audemard and Simon, 2009; E´en and S¨orensson, 2003] as the SAT solver in ABABAF. We used 2.50 GHz Intel Xeon Gold 6248 machines under a per-instance time limit of 600 seconds and memory limit of 32 GB.

3 Available at https://bitbucket.org/lehtonen/ababaf.

4 Available at https://bitbucket.org/coreo-group/aspforaba.

Lacking a standard benchmark library for non-flat ABA, we generated two benchmark sets adapted from flat ABA benchmarks [J¨arvisalo et al., 2023]. Set 1 has the following parameters: number of atoms in {80, 120, 160, 200}, ratio of atoms that are assumptions in {0.2, 0.4}, ratio of assumptions occurring as rule heads in {0.2, 0.5}, and both number of rules deriving any given atom and rule size (number of atoms in the body of rule) selected at random from the interval [1, n] for n ∈ {1, 2, 5}. We call the maximum rules per atom mr and maximum rule size ms; instances with ms = 1 are additive. For benchmark set 2, we limited mr and ms to {2, 5}, and generated instances a certain distance from atomic. For this, a slack parameter specifies how many atoms in each rule body can be non-assumptions. Here slack is 0, 1 or 2, the first resulting in atomic ABAFs. We generated 5 instances for each combination of parameters for both benchmark sets.

Table 1 summarizes results for credulous acceptance under complete semantics. On benchmark set 1 (Table 1, left), generally ABABAF performs better than ASPFORABA when the parameters take lower values. ABABAF outperforms ASPFORABA when ms = 1, corresponding to additive ABA frameworks, but also for ms = 2 when mr is 1 or 2. ASPFORABA, on the other hand, performs best with mr = 5. The results for benchmark set 2 (for credulous acceptance under complete semantics) can be seen in Table 1 (right). On atomic instances (slack = 0) ABABAF outperforms ASPFORABA. As the slack increases, the performance of ABABAF decreases, while ASPFORABA somewhat improves. Evidently, ABABAF is able to take advantage of the lower complexity of additive and atomic instances. The results suggest that the approaches are complementary and their relative performance varies by parameters.

We show the run times of both algorithms against the number of arguments a given instance gives rise to in Figure 1 (for instances solved byABABAF; timeouts of ASPFORABA shown as 600 seconds). For ABABAF, there is a clear correlation between run time and size of the constructed BAF, as can be expected given that the arguments construction is timeconsuming and the BAF is the input for a SAT call. In contrast, BAF size does not predict run time for ASPFORABA, since ASPFORABA does not instantiate arguments.

We also evaluated our algorithms under stable semantics. As expected given the lower complexity compared to complete semantics, ASPFORABA performs better, solving all instances. On the other hand, ABABAF constructs the BAF for stable semantics too, and accordingly the performance of ABABAF is significantly worse than ASPFORABA, with multiple timeouts. This highlights that a crucial component in the performance of ABABAF on complete semantics is the lower complexity of deciding acceptance in BAF compared to the corresponding ABAF.

7 Conclusion

Efficient algorithmic solutions for assumption-based argumentation are widely studied; however, despite the wide variety of different solvers for assumption-based reasoning, most existing approaches only focus on the flat ABA fragment. In this work we investigated theoretical foundations and algorithms for non-flat ABA reasoning, which has higher complexity than in flat ABA.

Our redundancy notions gave rise to two fragments of ABA, i.e., atomic and additive ABA, in which reasoning exhibits the same complexity as for flat ABA. We proposed two algorithmic approaches, one instantiating a BAF and one without argument construction. The former faces an exponential number of arguments in general, but we proposed and applied redundancy notions, and employed stateof-the-art solving techniques. For the latter, we adapted state-of-the-art algorithms for structured argumentation. We showed empirically that, in contrast to previous instantiationbased approaches for structured argumentation, our novel instantiation-based approach is able to outperform the direct approach, in particular for problems on the second level of the polynomial hierarchy.

For future work, we want to extend our implementation to further common semantics and reasoning tasks such as skeptical acceptance ; this is an additional challenge, since e.g. skeptical reasoning under preferred semantics lies on the third level of the polynomial hierarchy. Another promising line of future work is to develop methods for computing explanations for ABA in spirit of the work by Dung et al. (2006), utilizing our instantiation-based implementation.

Acknowledgements

This research was funded by the Austrian Science Fund (FWF) P35632 and University of Helsinki Doctoral Programme in Computer Science DoCS; by the European Research Council (ERC) under the European Union's Horizon 2020 research and innovation programme (grant agreement No. 101020934, ADIX) and by J.P. Morgan and by the Royal Academy of Engineering under the Research Chairs and Senior Research Fellowships scheme; by the Federal Ministry of Education and Research of Germany and by S¨achsische Staatsministerium f ¨ur Wissenschaft, Kultur und Tourismus in the programme Center of Excellence for AI-research "Center for Scalable Data Analytics and Artificial Intelligence Dresden/Leipzig", project identification number: ScaDS.AI. The authors wish to thank the Finnish Computing Competence Infrastructure (FCCI) for supporting this project with computational and data storage resources.