# decompositionguided_reductions_for_argumentation_and_treewidth__10876481.pdf Decomposition-Guided Reductions for Argumentation and Treewidth Johannes Fichte1 , Markus Hecher2,3 , Yasir Mahmood4 , Arne Meier4 1UC Berkeley, Berkeley, USA 2TU Wien, Vienna, Austria 3University of Potsdam, Germany 4 Leibniz Universit at Hannover, Germany johannes.fichte@berkeley.edu, hecher@dbai.tuwien.ac.at, {mahmood, meier}@thi.uni-hannover.de Argumentation is a widely applied framework for modeling and evaluating arguments and its reasoning with various applications. Popular frameworks are abstract argumentation (Dung s framework) or logic-based argumentation (Besnard Hunter s framework). Their computational complexity has been studied quite in-depth. Incorporating treewidth into the complexity analysis is particularly interesting, as solvers oftentimes employ SAT-based solvers, which can solve instances of low treewidth fast. In this paper, we address whether one can design reductions from argumentation problems to SAT-problems while linearly preserving the treewidth, which results in decomposition-guided (DG) reductions. It turns out that the linear treewidth overhead caused by our DG reductions, cannot be significantly improved under reasonable assumptions. Finally, we consider logic-based argumentation and establish new upper bounds using DG reductions and lower bounds. 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 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. 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. Example 1. (A1) Support: We have enough money (xem) and there is no travel restriction, so we can travel (xtr). Claim: We can travel to Montreal (xt M). (A2) Support: Corona cases are increasing (x C) and governments are imposing travel restrictions. Claim: We cannot travel to anywhere anymore. Formalizing these yields: A1 : Φ1 = {xem, xtr, (xem xtr) xt M}, α1 = {xt M}, A2 : Φ2 = {x C, x C 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 2complete [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 Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence (IJCAI-21) 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), q Bf 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)) = S i ℓXi. We evaluate φ by x.φ φ[x 7 1] φ[x 7 0] and x.φ φ[x 7 1] φ[x 7 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 q Bf φ = X1.φ of rank ℓ, whether φ 1 holds. The problem #ℓ-QBF asks, given a closed q Bf 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. V = S t of T χ(t) and E S t of T {{u, v} | u, v χ(t)} 2. for each s lying on any r-t-path: χ(r) χ(t) χ(s). Then, define width(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 q Bfs. For a given q Bf φ 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 q Bf φ 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 q Bf ϕ 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 def F (S) is defined by def F (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 def F (S) = S; b) Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence (IJCAI-21) 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, semi St, 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 c S and s S 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 #c S 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 xt M} and α1 = {xt M}. Then, G(Φ,α) has {xem, xtr, xt M} 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 fol- χ(t5) t5 T : f(t3, χ(t3), {χ (t1), χ (t2)}) f(t1, χ(t1), ) f(t2, χ(t2), ) f(t4, χ(t4), ) T : f(t5, χ(t5), {χ (t3), χ (t4)}) Figure 1: Illustration of a DG reduction R from problem P to QBF, where we take an instance I of problem P and a TD T = (T, χ) of GI. Then, since the DG reduction is constructed for each node t of T, it immediately yields a TD T = (T, χ ) of Gϕ of the resulting q Bf ϕ. Each bag χ (t) of a node t of T functionally depends on t, χ(t), as well as χ (t ) of every child node t children(t). lows. 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 q Bf ϕ in time tower(ℓ, o(width(T ))) poly(|var(ϕ)|). The time restriction ensures that R does not already solve the resulting q Bf (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 q Bf 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 conf R(E) and in Or XR(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 conf R(E) := V (a,b) R( ea eb) and in Or XR(E) := V (b,a) R eb ea). These definitions can be used to encode stab, but also #cstab: E.conf R(E) in Or XR(E) ec. While conf R(E) already preserves the treewidth, in Or XR(E) does not. This is witnessed by the observation that formula in Or XR(E) could Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence (IJCAI-21) cause dense parts in the primal graph of the formula. DG Reduction. Consequently, one needs to split in Or XR(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 in Or XR(E) with the help of auxiliary variables of the form dt a 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 := {dt a | a A, t in T}. Then, we define a DG reduction R#cstab #SAT(F, T ) by R#cstab #SAT(F, T ) := E, D.ϕ#stab(E, D) ec, where ϕ#stab(E, D) is a CNF consisting of Formulas (1) (3): t children(t), a χ(t ) (b,a) Rt eb for every t of T, a χ(t) (1) conf R(E) (2) ea dlast(a) a for every a A. (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 q Bf ψ 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, dt a | 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 q Bf ψ 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 conf R(E) to determine conflict-freeness. Further, we require def R(E) to ensure that attackers of the extension are defeated, respectively. Let def R(E) := V (b,a) R(W (c,b) R ec ea). Then, these definitions can be used to encode adm as follows: E.(conf R(E) def R(E)). While conf R(E) already preserves the treewidth, def R(E) does not, which is witnessed by the same argument as for in Or XR(E) above. DG Reduction. Towards a DG reduction, one needs to split def R(E) in order to linearly preserve the treewidth. Similar to above, we split def R(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 Radm SAT(F, T ) := E, D, N.ϕadm(E, D, N), where ϕadm(E, D, N) consists of Formulas (1), (2) and (4), (5): na eb for every (a, b) R (4) ea na dlast(a) a for every a A. (5) 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): na ea for every a A (6) na dlast(a) a for every a A. (7) 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.[conf R(E) def R(E) ( E E conf R( E) def R( E))], where encoding E E accordingly is not difficult. Towards a DG reduction, we keep reusing conf R( 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 from D, N, respectively. Then, we define a DG reduction R#pref #2-QBF(F, T ) := E, D, N. E, D, N, Q.[ϕ#adm(E, D, N) (ϕ E E(E, E, Q) ϕ#adm( E, D, N))], where ϕ#adm is constructed as above and ϕ E E(E, E, Q) is in DNF consisting of Formulas (8) (11): ea ea for every a A (8) (qa ea ea) for every a A (9) t children(t) qt _ a χ(t) qa) for every t of T (10) qroot(T ). (11) Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence (IJCAI-21) 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#csemi St #2-QBF(F, T ) := E, D, N. E, D, N, Q.[ϕ#adm(E, D, N) ec (ϕ E+ R E+ R(E, E, Q) ϕ#adm( E, D, N))], 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: ea ea dlast(a) a for every a A (12) dlast(a) a ea dlast(a) a for every a A (13) Similar to Formulas (9), we define qa for ranges of E and E, corresponding to (qa ( ea dlast(a) a ) ea dlast(a) a ): qa ea dlast(a) a for every a A (14) qa ea for every a A (15) qa dlast(a) a for every a A (16) ea ea dlast(a) a qa for every a A (17) dlast(a) a ea dlast(a) a qa for every a A (18) DG Reduction for #cstage. Analogously to above, we immediately obtain a DG reduction from #cstage to #2-QBF by R#cstage #2-QBF(F, T ) := E. E, Q.[conf R(E) ec (ϕ E+ R E+ R(E, E, Q) conf R( E))]. 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#c S #2-QBF for S {semi St, stage} is correct, i.e., #c S on F coincides with #2-QBF on R#c S #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#c S #2-QBF(F, T ) for S {semi St, stage} constructs q Bf ψ with tw(Gmatrix(ψ)) O(k). Under ETH, there is no reduction from c S to 2-QBF yielding q Bf ψ in time tower(2, o(tw(GF ))) poly(|A|) with tw(Gψ) o(tw(GF )). 4 A Complexity 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) := V Ci ( ei Ci) and ent ,α(E, N) := W 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 = S 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 q Bf ψ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(α)|). Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence (IJCAI-21) Abstract Argumentation Logic-based Argumentation cstab, cadm, ccomp, cpref, spref / #cpref csemi St, cstage, ARG ARG-Check #cstab, #cadm, #ccomp #csemi St, #cstage ARG-Rel TW-Awareness O(k) O(k) O(k) O(k) O(k) O(k) O(k) O(k) O(k) O(k) O(k) O(k) O(k) O(k) O(k) TW-LB (ETH) Ω(k) Ω(k) Ω(k) Ω(k) Ω(k) Ω(k) / open Ω(k) Ω(k) Ω(k) Ω(k) Ω(k) Ω(k) Ω(k) Ω(k) Ω(k) Runtime UB 2O(k) poly(n) 22O(k) poly(n) 22O(k) poly(n) 22O(k) poly(n) 22O(k) poly(n) 22O(k) poly(n) 2O(k) poly(n) 2O(k) poly(n) 2O(k) poly(n) Runtime LB (ETH) 2o(k) poly(n) 22o(k) poly(n) / open 22o(k) poly(n) 22o(k) poly(n) 22o(k) poly(n) 22o(k) poly(n) 2o(k) poly(n) 2o(k) poly(n) 2o(k) poly(n) Table 1: Overview of results, where k = tw(GF ) and n = |A| for given AF F = (A, R) of abstract arg., and k = tw(G( ,α)), n = |var( ) var(α)| for an instance ( , α) of logic-based arg. Bold results form new contributions; for known results see [Lampis et al., 2018; Fichte et al., 2019]. : While DG reductions preserving widths are new, reductions for linearly preserving treewidth are known for adm and pref [Lampis et al., 2018]. TW-Awareness refers to the treewidth increase caused by DG reductions, TW-LB (ETH) refers to treewidth lower bounds of DG reductions under ETH, UB are runtime upper bounds, and LB (ETH) are runtime lower bounds under ETH. 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 q Bf ψ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 q Bfs where each subformula contains one quantifier, but no alternation within each subformula. Then, we argue that the resulting q Bfs 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 and M i, respectively. Then, ψARG-Check consists of the n+2 q Bfs of the following three forms. (i) M.Φ, (ii) M.(W 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 q Bf, which together with (ii) results in two q Bfs. By slightly abusing notation, we refer to these two q Bfs (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 q Bf ψ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? Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence (IJCAI-21) References [Alviano, 2018] Mario Alviano. The Pyglaf Argumentation Reasoner. In ICLP 17. [Amgoud and Prade, 2009] Leila Amgoud and Henri Prade. Using arguments for making and explaining decisions. Artif. Intell., 173(3-4), 2009. [Atserias et al., 2011] Albert Atserias, Johannes Klaus Fichte, and Marc Thurley. Clause-learning algorithms with many restarts and bounded-width resolution. J. Artif. Intell. Res., 40, 2011. [Bacchus et al., 2003] Fahiem Bacchus, Shannon Dalmao, and Toniann Pitassi. Algorithms and complexity results for #SAT and Bayesian inference. In FOCS 03. [Baroni et al., 2010] Pietro Baroni, Paul E. Dunne, and Giuseppe De Giacomo, editors. In COMMA 10. [Besnard and Hunter, 2008] Philippe Besnard and Anthony Hunter. Elements of Argumentation. MIT Press, 2008. [Biere et al., 2009] Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors. Handbook of Satisfiability, volume 185 of FAIA. IOS Press, 2009. [Bondy and Murty, 2008] John A. Bondy and Uppaluri S. R. Murty. Graph theory, volume 244 of Graduate Texts in Mathematics. Springer, 2008. [Brochenin et al., 2018] Remia Brochenin, Thomas Linsbichler, Marcoa Maratea, Johannes P. Wallner, and Stefan Woltran. Abstract solvers for Dung s argumentation frameworks. Argument & Computation, 9(1), 2018. [Charwat and Woltran, 2019] G unther Charwat and Stefan Woltran. Expansion-based QBF solving on tree decompositions. Fundam. Inform., 167(1-2), 2019. [Charwat et al., 2015] G unther Charwat, Wolfgang Dvoˇr ak, Sarah A. Gaggl, Johannes P. Wallner, and Stefan Woltran. Methods for solving reasoning problems in abstract argumentation a survey. Artif. Intell., 220, 2015. [Chen, 2004] Hubie Chen. Quantified constraint satisfaction and bounded treewidth. In ECAI 04. [Creignou et al., 2011] Nadia Creignou, Johannes Schmidt, Michael Thomas, and Stefan Woltran. Complexity of logic-based argumentation in Post s framework. Arg. & Comp., 2(2-3), 2011. [Creignou et al., 2014] Nadia Creignou, Uwe Egly, and Johannes Schmidt. Complexity classifications for logicbased argumentation. ACM Trans. Comput. Log., 15(3), 2014. [Cygan et al., 2015] Marek Cygan, Fedor V. Fomin, Łukasz Kowalik, Daniel Lokshtanov, Marcin Pilipczuk D aniel Marx, Michał Pilipczuk, and Saket Saurabh. Parameterized Algorithms. Springer, 2015. [Dechter, 1999] Rina Dechter. Bucket elimination: A unifying framework for reasoning. Artif. Intell., 113(1), 1999. [Dung, 1995] Phan Minh Dung. On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games. Artif. Intell., 77(2), 1995. [Dunne and Bench-Capon, 2002] Paul E. Dunne and Trevor J. M. Bench-Capon. Coherence in finite argument systems. Artif. Intell., 141(1/2):187 203, 2002. [Dvoˇr ak, 2012] Wolfgang Dvoˇr ak. Computational aspects of abstract argumentation. Ph D thesis, TU Wien, 2012. [Dvoˇr ak and Woltran, 2010] Wolfgang Dvoˇr ak and Stefan Woltran. Complexity of semi-stable and stage semantics in argumentation frameworks. Inf. Proc. Letters, 110(11), 2010. [Dvoˇr ak et al., 2012] Wolfgang Dvoˇr ak, Reinhard Pichler, and S. Woltran. Towards fixed-parameter tractable algorithms for abstract argumentation. Artif. Intell., 186, 2012. [Fomin and Kratsch, 2010] Fedor V. Fomin and Dieter Kratsch. Exact Exponential Algorithms. Texts in Theoretical Computer Science. EATCS Series. Springer, 2010. [Fichte et al., 2019] Johannes K. Fichte, Markus Hecher, and Arne Meier. Counting complexity for reasoning in abstract argumentation. In AAAI 19. [Fichte et al., 2020] Johannes K. Fichte, Markus Hecher, and Andreas Pfandler. Lower Bounds for QBFs of Bounded Treewidth. In LICS 20. [Hecher et al., 2020] Markus Hecher, Patrick Thier, and Stefan Woltran. Taming high treewidth with abstraction, nested dynamic programming, and database technology. In SAT 20. [Hecher, 2020] Markus Hecher. Treewidth-aware reductions of normal ASP to SAT - is normal ASP harder than SAT after all? In KR 20. [Impagliazzo et al., 2001] Russell Impagliazzo, Ramamohan Paturi, and Francis Zane. Which problems have strongly exponential complexity? J. Comput. Syst. Sci., 63(4), 2001. [Kr oll et al., 2017] Markus Kr oll, Reinhard Pichler, and Stefan Woltran. On the complexity of enumerating the extensions of abstract argumentation frameworks. In AAAI 17. [Lampis and Mitsou, 2017] Michael Lampis and Valia Mitsou. Treewidth with a quantifier alternation revisited. In IPEC 17. [Lampis et al., 2018] Michael Lampis, Stefan Mengel, and Valia Mitsou. QBF as an alternative to courcelle s theorem. In SAT 18. [Maher, 2016] Michael J. Maher. Resistance to corruption of strategic argumentation. In AAAI 16. [Parsons et al., 2003] Simon Parsons, Michael J. Wooldridge, and Leila Amgoud. Properties and complexity of some formal inter-agent dialogues. J. Logic Comput., 13(3), 2003. [Pippenger, 1997] Nicholas Pippenger. Theories of computability. Cambridge University Press, 1997. [Rago et al., 2018] Antonio Rago, Oana Cocarascu, and Francesca Toni. Argumentation-based recommendations: Fantastic explanations and how to find them. In IJCAI 18. [Rahwan, 2007] Iyad Rahwan. Argumentation in artificial intelligence. Artif. Intell., 171(10-15), July 2007. Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence (IJCAI-21)