Decomposition-Guided Reductions for Argumentation and Treewidth

1 Introduction

Argumentation is a widely applied framework for modeling and evaluating arguments and its reasoning with various applications. Many different directions of argumentation theory have been successfully perused in the area of AI [Amgoud and Prade, 2009; Maher, 2016; Rago et al., 2018]. Popular frameworks are abstract argumentation (Dung's framework) [Dung, 1995; Rahwan, 2007] or logic-based argumentation [Besnard and Hunter, 2008].

In abstract argumentation, one describes arguments by notions that state acceptability with respect to an abstract framework, such as stable or admissible. Such arguments are then called extensions of a framework. In the logic-based method, one aims for inclusion-minimal consistent sets Φ of formulas (the support) that entail a claim α, which is encoded by a Boolean formula. If such a pair exists, then one calls (Φ, α) an argument. In this context, we consider three central decision problems. The first, ARG, asks, given a set ∆ of formulas, the so-called knowledge-base (KB), and a formula α, whether there exists a subset Φ ⊆ ∆ such that (Φ, α) is an argument in ∆. The two further problems of interest are ARG-Check, which asks whether a given set is a support for a given claim, and ARG-Rel, for which-besides given KB and claim-a formula has to be contained in the support.

∗The work is supported by Austrian Science Fund (FWF), Grants Y698 and P32830, the Vienna Science and Technology Fund, Grant WWTF ICT19-065, and the DFG (ME4279/1-2) under 247444366.

Example 1. (A1) Support: We have enoughmoney (xem) and there is no travel restriction, so we can travel (xtr). Claim: We can travel toMontreal (xtM). (A2) Support: Corona cases are increasing (xC) and governments are imposing travel restrictions. Claim: We cannot travel to anywhere anymore. Formalizing these yields: A1 : Φ1 = {xem, xtr, (xem ∧ xtr) → xtM}, α1 = {xtM}, A2 : Φ2 = {xC, xC → ¬xtr}, α2 = {¬xtr}. Each argument supports its claim, whereas, together they are conflicting, as A2 attacks A1.

The computational complexity of abstract argumentation has been studied quite in-depth for different problems and fragments of existence [Dunne and Bench-Capon, 2002; Dvoˇr´ak and Woltran, 2010; Dvoˇr´ak, 2012], (projected) counting [Baroni et al., 2010; Fichte et al., 2019], and enumeration [Kr¨oll et al., 2017] with results mostly on the first or second level of the polynomial hierarchy. Similarly for logic-based argumentation, ARG was shown to be Σp 2 - complete [Parsons et al., 2003]. More in-depth works consider the dichotomy between classes of tractability and intractability [Creignou et al., 2011; Creignou et al., 2014]. Also, more fine-grained analyzes when incorporating additional structure have been established [Dvoˇr´ak et al., 2012; Fichte et al., 2019; Lampis et al., 2018], for example, treewidth, which is defined on graph representations of the input. Treewidth k of an instance describes the hardness for evaluating the instance (bucket elimination) [Dechter, 1999; Cygan et al., 2015], when designing an algorithm that avoids backtracking and brute-forces only f(k) times. Treewidth is particularly interesting for analyzing the complexity, as abstract argumentation solvers oftentimes employ solvers based on SAT and extensions [Brochenin et al., 2018; Charwat et al., 2015; Alviano, 2018], which can solve instances of low treewidth fast [Atserias et al., 2011; Bacchus et al., 2003]. However, employing low treewidth only works in practical settings if the reduction to (extensions of) SAT is not already very expensive in the treewidth; more precisely, if there are reductions from problems of abstract argumentation to SAT or 2-QBF that linearly preserve the treewidth and can be computed reasonably fast. Surprisingly, this is unknown for abstract argumentation. For logic-based argumentation even bounded treewidth results are missing.

Contributions. In more detail, we address these questions:

1. We present decomposition-guided reductions (DG) for abstract argumentation problems when parameterized by treewidth. Our DG reductions are guided by a tree decomposition and allow to compile argumentation problems into SAT or 2-QBF with low (tree)width overhead.
2. We confirm that such reductions cannot be significantly improved under the exponential time hypothesis (ETH).
3. Furthermore, we consider the setting of logic-based argumentation. We establish new upper bounds using DG reductions and lower bounds by reducing from 2-QBF (ARG and ARG-Rel) or SAT (ARG-Check).

Related Works. Upper bounds by reductions to QBF for problems in abstract argumentation and treewidth under admissible and preferred semantics have been considered [Lampis et al., 2018]. Dynamic programming algorithms and lower bounds have been established for various semantics [Fichte et al., 2019]. We go beyond and present a systematic approach for the full set of standard semantics that linearly preserves the treewidth. Hecher [2020] recently established reductions that employ decompositions for answerset programming. Various works considered QBF and ETH lower bounds for treewidth [Chen, 2004; Lampis and Mitsou, 2017]. Solvers that explicitly exploit treewidth proved useful in various applications, e.g., model counting [Hecher et al., 2020] and QBF [Charwat and Woltran, 2019].

2 Preliminaries

We assume familiarity with computational complexity [Pippenger, 1997], graph theory [Bondy and Murty, 2008], and Boolean logic [Biere et al., 2009].

Quantified Boolean Formulas. Let ℓ be a positive integer, which we call (quantifier) rank later, and ⊤ and ⊥ be the constant always evaluating to 1 and 0, respectively. For a Boolean formula F, we abbreviate by var(F) the variables occurring in F and F(X1, . . . ,Xl) to indicate that X1, . . . ,Xl ⊆ var(F). A quantified Boolean formula φ (in prenex normal form), qBf for short, is an expression of the form φ = Q1X1.Q2X2. · · · QℓXℓ.F (X1, . . . , Xℓ), where for 1 ≤ i ≤ ℓ, we have Qi ∈ {∀, ∃} and Qi ̸= Qi+1, the Xi are disjoint, non-empty sets of Boolean variables, and F is a Boolean formula. We let matrix(φ) := F and we say that φ is closed if var(matrix(F)) = ⋃i∈ℓ Xi. We evaluate φ by ∃x.φ ≡ φ[x ↦→ 1] ∨ φ[x ↦→ 0] and ∀x.φ ≡ φ[x ↦→ 1] ∧ φ[x ↦→ 0] for a variable x. W.l.o.g. we assume that matrix(φ) = ψCNF ∧ ψDNF, where ψCNF is in CNF (disjunction of conjunctions of literals) and ψDNF is in DNF (conjunction of disjunctions of literals). Then, depending on Qℓ, either ψCNF or ψCNF is optional, more precisely, ψCNF might be ⊤, if Qℓ = ∀, and ψDNF is allowed to be ⊤, otherwise. The problem ℓ-QBF asks, given a closed qBf φ = ∃X1.φ′ of rank ℓ, whether φ ≡ 1 holds. The problem #ℓ-QBF asks, given a closed qBf ∃X1.φ of rank ℓ, to count assignments α to X1 such that φ[α] ≡ 1. For brevity we might omit ℓ.

Tree Decompositions and Treewidth. For a rooted (directed) tree T = (N, A) with root root(T ) and a node t ∈ N, we let children(t) be the set of all nodes t′ , which have an edge (t, t′ ) ∈ A. Let G = (V, E) be a graph. A tree decomposition (TD) of a graph G is a pair T = (T, χ), where T is a rooted tree, and χ is a mapping that assigns to each node t of T a set χ(t) ⊆ V , called a bag, such that:

1. for each s lying on any r-t-path: χ(r) ∩χ(t) ⊆ χ(s).

Then, definewidth(T ) :=maxt of T |χ(t)|-1. The treewidth tw(G) of G is the minimum width(T ) over all tree decompositions T of G. Observe that for every vertex v ∈ V , there is a unique node t∗ with v ∈ χ(t∗ ) such that either t∗ = root(T) or there is a node t of T with children(t)={t∗ } and v /∈ χ(t). We refer to the node t∗ by last(v). For arbitrary but fixed w ≥ 1, it is feasible in linear time to decide if a graph has treewidth at most w and, if so, to compute a TD of width w [Cygan et al., 2015]. In this work, we assume only TDs (T, χ), where for every node t of T, we have that |children(t)| ≤ 2. Such a TD can be obtained from any TD in linear time without increasing the width.

Treewidth and qBfs. For a given qBf φ with matrix(φ) = ψCNF ∧ ψDNF, we define the primal graph Gφ = Gmatrix(φ), whose vertices are var(matrix(φ)). Two vertices of Gφ are adjoined by an edge, whenever the corresponding variables share a clause or term of ψCNF or ψDNF, respectively.

Let tower(i, p) be tower(i-1, 2p ) if i > 0 and p otherwise. Further, we assume that poly(n) is any polynomial for given positive integer n. The following result is known for QBF.

Proposition 2 (Chen, 2004). For any arbitrary qBf φ of quantifier rank ℓ > 0, the problem ℓ-QBF can be solved in time tower(ℓ,O(tw(Gϕ))) · poly(|var(φ)|).

Assuming the exponential time hypothesis (ETH) [Impagliazzo et al., 2001], one cannot significantly improve this runtime in the worst case. Intuitively, the ETH implies that neither SAT=1-QBF nor #SAT=#1-QBF can be decided in time better than 2o(|var(ϕ)|) for an arbitrary formula ϕ.

Proposition 3 (Fichte et al., 2020). Under ETH, for any arbitrary qBf ϕ of quantifier rank ℓ > 0, problem ℓ-QBF cannot be solved in time tower(ℓ, o(tw(Gϕ))) · poly(|var(ϕ)|).

Abstract Argumentation. We use Dung's argumentation framework [Dung, 1995] and consider only non-empty and finite sets of arguments A. An (argumentation) framework (AF) is a directed graph F = (A, R) where A is a set of arguments and R ⊆ A × A, a pair of arguments representing direct attacks of arguments. An argument s ∈ S, is called defended by S in F if for every (s′ , s) ∈ R, there exists s′′ ∈ S such that (s′′ , s′ ) ∈ R. The family defF (S) is defined by defF (S) := {s | s ∈ A, s is defended by S in F}. In abstract argumentation, one strives for computing so-called extensions, which are subsets S ⊆ A of the arguments that have certain properties. The set S of arguments is called conflictfree in S if (S × S) ∩ R = ∅; S is admissible in F if (1) S is conflict-free in F, and (2) every s ∈ S is defended by S in F. Let S+ R := S ∪ {a | (b, a) ∈ R, b ∈ S } and S be admissible. Then, S is a) complete in F if defF (S) = S; b)

preferred in F, if no S′ ⊃ S exists that is admissible in F; c) semi-stable in F if no admissible set S′ ⊆ A in F with S+ R ⊊ (S′ )+R exists; and d) stable in F if every s ∈ A\S is attacked by some s′ ∈ S. A conflict-free set S is stage in F if there is no conflict-free set S′ ⊆ A in F with S+ R ⊊ (S′ )+R . For a semantics S ∈ {adm, comp, pref, semiSt, stab, stag}, we write S(F) for the set of all extensions of semantics S in F. Given an AF F = (A, R). Then, problem S asks if S(F ) ̸= ∅ and #S asks to compute |S(F)|. The problems cS and sS question for c ∈A and s ∈A, whether c is in some S ∈ S(F) ("credulously accepted") and s is in every S ∈ S(F) ("skeptically accepted"), respectively. Finally, problem #cS asks for c ∈ A, to compute |{S | S ∈ S(F), c ∈ S}|.

TDs for AFs. Consider for AF F = (A,R) the primal graph GF , where we simply drop the direction of every edge, i.e., GF = (A,R′ ) where R′ := {{u, v} | (u, v) ∈ R}. For any TD T = (T, χ) of GF and any node t of T, we let Rt := R∩ {(a, b) | a, b ∈ χ(t)} be the bag attacks of t.

Logic-based Argumentation. We study logic-based argumentation (LA) [Besnard and Hunter, 2008] using notions of Creignou et al. [2014]. Given sets Φ and ∆ of Boolean formulas and a Boolean formula α, the tuple (Φ, α) is an argument for α if (1) Φ is consistent, (2) Φ |= α, and (3) Φ is subset-minimal w.r.t. (2). In case of Φ ⊆ ∆, tuple (Φ, α) is an argument in ∆. We call α the claim, Φ the support of the argument, and ∆ the knowledge-base. We consider the following problems. The problem ARG (argument existence) asks, given a set of formulas ∆ and a formula α, is is there a set Φ ⊆ ∆ such that (Φ, α) is an argument in ∆? The problem ARG-Check (verification) asks, given a set of formulas Φ and a formula α, is is (Φ, α) an argument? The problem ARG-Rel (relevance) asks, given a set of formulas ∆, and formulas ψ ∈ ∆ and α, is is there a set Φ ⊆ ∆ with ψ ∈ Φ such that (Φ, α) is an argument in ∆? Note that for deciding ARG and ARG-Rel, Condition (3) above is irrelevant.

In this work, we assume w.l.o.g. that the KB ∆ is a set of clauses (CNF) and that α is in DNF. This simplifies presentation, but is not a hard restriction, as problems ARG and ARG-Rel remain Σp 2 -, whereas ARG-Check remains DPcomplete [Parsons et al., 2003; Creignou et al., 2011].

TDs for LA. In order to apply treewidth for logic-based argumentation, we let ∆ be a set of clauses and α be a Boolean formula in DNF. Then, the primal graph G(∆,α) := G∆∧α, where ∆ is viewed as a CNF formula. Further, for any TD T = (T, χ) of G(∆,α) and any node t of T , let ∆t :={φi | φi ∈ ∆, var(φi) ⊆ χ(t)} be the bag knowledge base of t.

Example 4. Consider the argument (Φ1, α1) from Example 1. Notice that the support Φ1 can be written in CNF as Φ1 = {xem, xtr, ¬xem ∨ ¬xtr ∨ xtM} and α1 = {xtM}. Then, G(Φ,α) has {xem, xtr, xtM} as the set of vertices and there are edges between all three, because they share a clause.

3 Decomposition-Guided Reductions for AFs

We briefly discuss a new type of reductions below.

3.1 Decomposition-Guided Reductions to QBF

Inspired by recent related work [Hecher, 2020], we introduce so-called decomposition-guided reductions as follows. A decomposition-guided (DG) reduction R is a function that takes both an instance I of a problem P and a TD T = (T, χ) of GI, and returns a qBf ϕ in time tower(ℓ, o(width(T )))·poly(|var(ϕ)|). The time restriction ensures that R does not already solve the resulting qBf (cf. Proposition 2). The way a DG reduction is constructed, it has to yield a TD T ′ = (T, χ′ ) of Gϕ. So, the idea of such a DG reduction is to construct ϕ from a TD node's point of view. Thereby, for each node t of T, the constructed bag χ′ (t) functionally depends on the original bag χ(t), but also on the constructed bags χ′ (t1), . . . , χ′ (to) of its child nodes {t1, . . . , to} = children(t). This gives rise to a function f that takes a tree decomposition node t, its bag χ(t) and a set χ′ (children(t)) := {χ′ (ti) | ti ∈ children(t)} of constructed bags for the child nodes of t. Figure 1 illustrates that function f taking a node t, its original bag χ(t), as well as χ′ (children(t)), to construct each bag χ′ (t) = f(t, χ(t), χ′ (children(t))). Then, since width(T ) is bounded by O(maxt of T (|χ(t)|)), also the treewidth of the resulting qBf is at most O(maxt of T (|f(t, χ(t), χ′ (children(t))|)). Intuitively, DG reductions are guided by a TD T = (T, χ) and adhere to ideas of dynamic programming along TD T . However, the DG reduction has to ensure that T ′ is a TD of Gϕ.

Next, we present DG reductions for problems originating from abstract argumentation that linearly preserve treewidth. These problems serve as a demonstration of DG reductions. To this end, we assume for the rest of this section that F = (A, R) is an AF and that T = (T, χ) is a given TD of GF .

3.2 Stable Extensions

First, we compute stable extensions via a reduction to SAT, i.e., such that the extensions are represented via a Boolean formula. To this end, we start with the following reduction. We use a variable ea for every argument a ∈ A, which indicates whether a is in the extension or not. These variables are part of the extension variables E := {ea | ea ∈ A}. We use sub-formulas confR(E) and inOrXR(E) to ensure conflictfreeness and to determine that every argument is either in the extension or attacked by the extension, respectively. More formally, we let confR(E) := ∧(a,b)∈R(¬ea ∨ ¬eb) and inOrXR(E) := ∧a∈A(∨(b,a)∈R eb ∨ ea).

These definitions can be used to encode stab, but also #cstab: ∃E.confR(E) ∧ inOrXR(E) ∧ ec. While confR(E) already preserves the treewidth, inOrXR(E) does not. This is witnessed by the observation that formula inOrXR(E) could cause dense parts in the primal graph of the formula.

DG Reduction. Consequently, one needs to split inOrXR(E) in order to linearly preserve the treewidth. To this end, we design a DG reduction, where we also consider the TD T . We split inOrXR(E) with the help of auxiliary variables of the form dta for every node t of T and argument a ∈ A to indicate whether a is attacked ("defeated") by an argument b ∈ χ(t) of the extension. This leads to defeated variables D := {dta | a ∈ A, t in T}.

where ϕ#stab(E, D) is a CNF consisting of Formulas (1)-(3):

Intuitively, Formulas (1) guide information of defeated arguments along the TD and Formulas (3) ensure that an argument is either in the extension or defeated. Since the reduction is constructed for each node of T, it is easy to see that the DG reduction is correct and preserves the (tree)width linearly.

Theorem 5 (TW-Awareness). Let F = (A,R) be an AF and T = (T, χ) be a TD of F of width k. Then, the DG reduction R#cstab→#SAT(F, T ) constructs a qBf ψ that linearly preserves the width, i.e., tw(Gmatrix(ψ)) ∈ O(k).

Proof (Sketch). We construct a TD T ′ = (T, χ′ ) of Gψ as follows. For every node t of T , we let χ′ (t) := χ(t) ∪ {ea, dta | a ∈ χ(t)} ∪ {dt′ a | a ∈ χ(t) ∩ χ(t′ ), t′ ∈ children(t)}. Since |children(t)| ≤ 2, we have that |χ′ (t)| ≤ 5 · |χ(t)|.

Interestingly, it is not expected that one can significantly improve (decrease) the treewidth in such a DG reduction.

Theorem 6 (TW-LB). Let F = (A,R) be an AF and T be a TD of F . Under ETH, the DG reduction R#cstab→#SAT(F, T ) cannot be significantly improved, i.e., there is no reduction R′ from cstab to SAT yielding a qBf ψ in time 2o(tw(GF )) · poly(|A|) with tw(Gψ) ∈ o(tw(GF )).

Proof (Sketch). Assume towards a contradiction that there is such a reduction R′ . Then, we apply R′ in order to solve cstab for F in time 2o(tw(GF )) · poly(|A|), which contradicts ETH [Fichte et al., 2019].

3.3 Admissible Extensions

Similar to above, for computing admissible extensions, we follow a plain reduction to SAT. As above, we use extension variables E as well as sub-formula confR(E) to determine conflict-freeness. Further, we require defR(E) to ensure that attackers of the extension are defeated, respectively.

Then, these definitions can be used to encode adm as follows: ∃E.(confR(E) ∧ defR(E)). While confR(E) already preserves the treewidth, defR(E) does not, which is witnessed by the same argument as for inOrXR(E) above.

DG Reduction. Towards a DG reduction, one needs to split defR(E) in order to linearly preserve the treewidth. Similar to above, we split defR(E) with the help of auxiliary variables, namely the defeated variables D. However, we also need further auxiliary variables of the form na for every argument a ∈ A to indicate whether a never attacks an argument of the extension. These variables are referred to by the no-attacking variables N := {na | a ∈ A}.

Then, we define DG reduction Radm→SAT(F, T ) to SAT

Thereby, Formulas (4) define na and Formulas (5) generalize Formulas (3) towards admissible semantics.

Lifting to #cadm. In order to bijectively preserve admissible extensions of F, we add to ϕadm(E,D,N) the following Formulas (6), (7), which finally results in ϕ#adm(E,D,N):

So, R#cadm→#SAT(F, T ) :=∃E,D,N.ϕ#adm(E,D,N) ∧ ec. As before, this reduction linearly preserves the (tree)width and it is not expected that the treewidth increase can be significantly reduced. Consequently, we obtain similar results to Theorems 5 and 6 for problems #cadm and cadm, which can be solved by enforcing that the argument of concern is in the extension. We can further lift the reduction for problems ccomp and #ccomp, as shown in an extended (self-archived) version.

3.4 Preferred Extensions

Reusing the definitions from above, one can reduce pref to 2-QBF, where we use a set ˜E of fresh variables obtained from E s.t. ˜E := {˜ ea | ea ∈ E}, by: ∃E.∀ ˜E.[confR(E) ∧ defR(E)∧( ˜E̸⊃E∨¬confR( ˜E)∨¬defR( ˜E))], where encoding ˜E̸⊃E accordingly is not difficult.

Towards a DG reduction, we keep reusing confR( ˜E) over variables ˜E. However, checking equality needs to be guided along the TD. We use inequality variables qa (qt ), indicating that ea ↔ ¬˜ ea (for some a ∈ A below t), respectively. We define Q := {qt , qa | t of T, a ∈ A}. Eventually, use fresh sets ˜D, ˜N of variables obtained fromD, N, respectively.

Then, we define a DG reduction R#pref→#2-QBF(F, T ) :=

where ϕ#adm is constructed as above and ϕ ˜E̸⊃E (E, ˜E,Q) is in DNF consisting of Formulas (8)-(11):

Formulas (8) allow the extension over E to contain an argument not in ˜E, Formulas (9) define inequality and Formulas (10) guide inequality along the TD. Finally, with Formulas (11), equal extensions over E and ˜E are allowed. These formulas can be converted to DNF easily, where, e.g., Formulas (9) result in (qa ∧¬˜ ea) ∨ (qa ∧ ea) ∨ (˜ ea ∧ ¬ea ∧ ¬qa).

As before, the (tree)width is preserved linearly. While cpref can be already decided via cadm, one can solve spref with this reduction above by adding clause ¬es and inverting the result.

3.5 Semistable and Stage Extensions

The idea from above can be reused in order to design DG reduction R#csemiSt→#2-QBF(F, T ) :=

where ϕ ˜E+ R ̸⊃E+ R (E, ˜E,Q) is in DNF and consists of Formulas (10), (11), and (12)-(18) below. Similar to Formulas (8), Formulas (12) and (13) allow that E+ R might contain arguments not in ˜E+ R :

Similar to Formulas (9), we define qa for ranges of E and ˜E, corresponding to ¬(qa ↔ (˜ ea ∨ ˜ dlast(a) a ) ∧ ¬ea ∧ ¬dlast(a) a ):

Indeed, these reductions are correct and treewidth-aware.

Theorem 7 (Correctness). Given an AF F = (A,R) and a TD T = (T, χ) of GF . Then, the DG reduction R#cS→#2-QBF for S ∈ {semiSt, stage} is correct, i.e., #cS on F coincides with #2-QBF on R#cS→#2-QBF(F, T ).

Theorem 8 (TW-Awareness TW-LB). Given an AF F = (A,R) and a TD T =(T, χ) of GF of width k. Then, the DG reduction R#cS→#2-QBF(F, T ) for S ∈ {semiSt, stage} constructs qBf ψ with tw(Gmatrix(ψ)) ∈ O(k). Under ETH, there is no reduction from cS to 2-QBF yielding qBf ψ in time tower(2, o(tw(GF ))) · poly(|A|) with tw(Gψ) ∈ o(tw(GF )).

4 AComplexity Study for Logic-Based Arg.

4.1 Argument Existence and Relevance

We reduce an instance (∆, α) of ARG to an instance of 2-QBF. Let ∆ = {Ci, | 1 ≤ i ≤ n} be a collection of clauses and α be a Boolean formula in DNF. We use a variable ei for each i to encode whether Ci is contained in the support. Consequently, let the support variables E be defined by E := {ei | 1 ≤ i ≤ n}. Then, let M be the set of variables over var(∆). Moreover, let N := var(∆∪ {α}) and let ˜N denote the renaming of variables in N. That is ˜N := {˜xi | xi ∈ N} and each ˜xi is a fresh variable. Finally, by ˜ C, ˜α and ˜ ∆ denote C, α and ∆ over renamed variables. Now, let cons∆(E,M) := ∧Ci∈∆(¬ei ∨ Ci) and ent∆,α(E, ˜N) := ∨Ci∈∆(ei ∧¬ ˜ Ci)∨ ˜α. Then, we construct ψ′ARG = ∃E,M.∀ ˜N.(cons∆(E,M) ∧ ent∆,α(E, ˜N)).

Intuitively, setting ei ∈ E to 1 implies that the corresponding Ci ∈ ∆ constitutes a support Φ. Then, ent∆,α(E, ˜N) achieves that whenever an assignment over variables ˜N is a model of each ˜ Ci, the assignment also models ˜α.

Theorem 9 (Correctness). Let (∆, α) be an instance of ARG. Then, there is a support Φ ⊆ ∆ such that (Φ, α) is an argument in ∆ if and only if ψ′ARG is true.

The two subformulas cons∆(E,M) and ent∆,α(E, ˜N) do not preserve the treewidth (one bag may contain variables from multiple clauses causing many ei). For this reason, we split the formula in order to linearly preserve the treewidth.

DG Reduction. Let T = (T, χ) be a TD of G(∆,α). Then, we define a labeled TD (LTD) T ′ = (T, χ, δ) of T , where labeling δ : T → ∆ is such that δ(t) ∈ ∆t and ∆ = ⋃t of T {δ(t)}. Note that an LTD can be easily obtained from any TD without changing the width by copying nodes accordingly. Next, we assume such an LTD T ′ = (T, χ, δ) of T . Then, we construct the following formula,

RARG→2-QBF(I, T ′ ) := ∃E,M.∀ ˜N.ϕARG(E,M, ˜N), where ϕARG is built for every node t of T by cons{δ(t)}(E,M) ∧ ent{δ(t)}(E, ˜N).

Indeed, both subformulas preserve the treewidth linearly.

Theorem 10 (TW-Awareness). Let I = (∆, α) be an instance of ARG, T be a TD of G(∆,α) of width k, and T ′ be an LTD of T . Then, the DG reduction RARG→2-QBF(I, T ′ ) constructs a qBf ψARG with tw(Gmatrix(ψARG)) ∈ O(k).

Proof (Sketch). For any given LTD T ′=(T, χ, δ) of T , the reduction yields a TD T2-QBF=(T, χ′ ) where the set T remains unchanged. Bag χ′ (t) for each node t is constructed by adding a renamed copy of variables in χ(t) and the support variable ei to χ(t), where ei is such that δ(t) = Ci.

This immediately yields the following runtime result.

Theorem 11 (Runtime UB). Let I = (∆, α) be an instance of ARG. Then, ARG can be solved in time tower(2,O(k)) · poly(|var(∆) ∪ var(α)|), where k = tw(GI).

Proof. We construct a TD T of GI of treewidth at most 5·k in time 2O(k) · poly(|var(∆) ∪ var(α)|) [Cygan et al., 2015] and LTD T ′ of T . Then, we use reduction RARG→2-QBF(I, T ′ ), which together with Proposition 2 establishes the result.

Unluckily, this can probably not be significantly improved.

Theorem 12 (Runtime LB). Let I = (∆, α) be an instance of ARG. Then, under ETH, ARG cannot be solved in time tower(2, o(tw(GI)) · poly(|var(∆) ∪ var(α)|).

One cannot expect to improve the DG reduction much.

Theorem 13 (TW-LB). Let I = (∆, α) be an instance of ARG. Under ETH, there is no reduction R′ from ARG to 2-QBF yielding a qBf ψARG in time tower(2, o(tw(GI))) · poly(| var(∆) ∪ var(α)|) with tw(GψARG ) ∈ o(tw(GI)).

Argument Relevance Problem (ARG-Rel). Consider the reduction for ARG again. The question of ARG-Rel now reduces to forcing one particular element of E in the solution. W.l.o.g., assume that ψ = C1 with C1 ∈ ∆. Then, (∆, α, ψ) ∈ ARG-Rel if and only if there is a support Φ that contains C1. This can be encoded by ∃E,M.∀ ˜N.(e1 ∧ ϕARG(E,M, ˜N)). The correctness proof, treewidth preservation, as well as upper bounds remain the same as for ARG.

Furthermore, notice that the problem ARG-Rel is as hard as the problem ARG. This is because an instance (∆, α) of ARG has a support Φ if and only if an instance (∆ ∪ {ψ}, α, ψ) of ARG-Rel has one, where ψ ̸∈ ∆ is a satisfiable formula over fresh variables not in var(∆). This implies that lower bounds under ETH transfer to ARG-Rel.

4.2 Argument Verification Problem

It seems challenging to reduce a given instance I = (Φ, α), where |Φ| = n, of ARG-Check to one instance of SAT as ARG-Check is DP-complete. A direct reduction encoding all three sub-questions (Φ is consistent, Φ |= α and no proper subset of Φ entails α) gives a 2-QBF instance. In the following, we reduce (Φ, α) to a collection of qBfs where each subformula contains one quantifier, but no alternation within each subformula. Then, we argue that the resulting qBfs have (tree)width linear in the width of a given TD T of G(Φ,α).

Let M := var(Φ) ∪ var(α). In order to encode three separate conditions, we use n + 1 many additional copies of variables of M, which we address with ˜M and M˜i for 1 ≤ i ≤ n. Finally, for a formula φ (resp., a clause Cj) over M, we write ˜ φ ( ˜ Cj) and φ˜i (Cj˜i ) for the corresponding formula (clause) over ˜M andM˜i , respectively.

Then, ψARG-Check consists of the n+2 qBfs of the following three forms. (i) ∃M.Φ, (ii) ∀ ˜M.(∨1≤i≤n ¬ ˜ Ci ∨ ˜α) and for 1 ≤ i ≤ n, (iii) ∃M˜i .(θi˜i ∧ ¬α˜i ), where θi = Φ\{Ci}, that is, the formula obtained from Φ by removing the i-th clause. The matrix of the Formula (ii) is in DNF, which encodes that for each assignment over variables in M, either it does not satisfy some clause Ci ∈ Φ or it satisfies α. Formulas (iii) encode that for each Ci ∈ Φ there is an assignment over M, such that the formula θi does not entail α. Notice that all n + 2 formulas are independent of each other, this is because each is constructed over a different set of variables. Further, one can merge Formula (i) with Formulas (iii) into one qBf, which together with (ii) results in two qBfs. By slightly abusing notation, we refer to these two qBfs (conjunction) by RARG-Check→QBF(I, T ) := ψARG-Check. Notice that reduction RARG-Check→QBF consists of several DG reductions corresponding to Formulas (i), (ii), and (iii).

Theorem 14 (Correctness). Let (Φ, α) be an ARG-Checkinstance. Then, (Φ, α) is an argument iff ψARG-Check is true.

The treewidth is preserved (independent copy variables).

Theorem 15 (TW-Awareness). Let I=(Φ, α) be an instance of ARG-Check and T = (T, χ) be a TD of GI of width k. Then, RARG-Check→QBF(I, T ) constructs a qBf ψARG-Check with tw(Gmatrix(ψARG-Check)) ∈ O(k).

This implies that ARG-Check can be solved in time 2O(tw(GI)) ·poly(|var(Φ) ∪ var(α)|). Moreover, we obtain the matching LB results, similar to Theorem 12 and and 13.

Theorem 16 (Runtime LB). Let I = (Φ, α) be an instance of ARG-Check. Then, under ETH, ARG-Check cannot be solved in time 2o(tw(GI)) · poly(|var(Φ) ∪ var(α)|).

5 Conclusions

Our results (summarized in Table 1) provide new theoretical insights and strengthen the applicability of solvers that implicitly solve instances by means of tree decompositions. They might also be helpful for solvers that are indirectly able to solve instances of low treewidth fast. We present new treewidth-aware lower bounds (under ETH) as well as tight upper complexity bounds for logic-based argumentation.

As future work, we plan to study practical implementation of this framework and thereby further verify its robustness. Another investigation regarding the strong ETH might underline the strength of our approach. As the reductions preserve the solutions bijectively, they are applicable in the enumeration complexity setting [Fomin and Kratsch, 2010], however a more rigorous approach might lead to further insights. Could other parameters obey similar types of reductions?