Novel Algorithms for Abstract Dialectical Frameworks based on Complexity Analysis of Subclasses and SAT Solving

1 Introduction

Over the last decade, argumentation has become a major field in AI research [Bench-Capon and Dunne, 2007] and an increasing number of applications (see [Atkinson et al., 2017] for a survey) encourages the development of computational models of argumentation. Within this field, Dung's abstract argumentation frameworks (AFs for short) [Dung, 1995] have received notable attention which resulted in a multitude of methods for solving reasoning problems in such frameworks [Charwat et al., 2015]. Systems implementing such methods participate in a dedicated competition [Thimm and Villata, 2017], where procedures which rely on (multiple) calls to SAT solvers have been proven successful [Dvoˇr´ak et al., 2014; Cerutti et al., 2014].

Despite the popularity of AFs, their conceptual simplicity - an AF is just a directed graph with nodes as abstract arguments and edges representing individual attacks - has also often turned out to be overly limiting. Therefore, generalizations of AFs introducing further link types such as support or collective attacks [Nielsen and Parsons, 2007; Cayrol and Lagasquie-Schiex, 2013] or imposing quantitative aspects have been presented. Abstract dialectical frameworks (ADFs for short) [Brewka and Woltran, 2010; Brewka et al., 2017b] constitute one of the most comprehensive generalizations of AFs available. By equipping every argument with an acceptance condition, ADFs are capable of modeling arbitrary relations between arguments. Potential applications in legal reasoning [Al-Abdulkarim et al., 2016], online dialog systems [Neugebauer, 2017], text exploration [Cabrio and Villata, 2016], and the instantiation of defeasible theories [Strass, 2014] have already been proposed.

The power of ADFs comes with a price: compared to AFs, the computational complexity increases by one step in the polynomial hierarchy for nearly all reasoning tasks [Strass and Wallner, 2015], with the hardest problems being Π P3 - complete. Therefore, the identification of fragments which yield decreased complexity, or even tractability, is of high interest. So far, only the class of bipolar ADFs [Brewka and Woltran, 2010] has been shown to be unaffected by the increase in complexity compared to AFs. Recent work [Keshavarzi, 2017] has investigated further subclasses but without an explicit complexity analysis. Existing implementations of ADFs deal with the complexity by employing reductions either to QBF [Diller et al., 2015] or to ASP [Strass and Ellmauthaler, 2017; Brewka et al., 2017a], but barely exploit potential shortcuts for ADFs of lower complexity.

In this work, we aim towards more efficient systems for ADFs and provide (1) a careful complexity analysis of ADF subclasses together with investigations whether ADFs being "close" to a subclass remain easier; and (2) SAT-based implementations which make use of these insights. For AFs such analyses can be found in [Dvoˇr´ak et al., 2012; 2014] and have been implemented in the Cegartix system. More specifically, our main contributions are as follows:

• We investigate the complexity of two further subclasses: acyclic ADFs and concise ADFs. The first class, which restricts the graph underlying the ADF to be acyclic, yields dramatic gains in complexity for the majority of reasoning tasks. The second class is defined with respect to a semantics for which the ADFs are required to yield only a single solution. This also leads to a certain decrease in the complexity. As all these fragments impose rather strict requirements, we further show that many of the computational advantages also hold for ADFs which have constant distance to these subclasses (for this analysis we also include bipolar ADFs).
• Based on our observations we design novel algorithms for ADF reasoning, in particular, for the problems of skeptical and credulous acceptance under preferred semantics. We provide an implementation based on incremental SAT solving, which is not only novel in combining ADF solving with SAT, but is also complexity sensitive as it takes advantage of the input ADFs being in (low distance to) advantageous fragments.
• Finally, we provide an experimental evaluation of our new approach which shows that it is capable of outperforming state-of-the-art systems for ADFs.

2 Background

We recall the syntax and semantics of ADFs from [Brewka et al., 2017b]. We assume a fixed and finite set of arguments A. An interpretation is a function I mapping arguments to one of the three truth values I : A → {t, f , u}. That is, an interpretation maps each argument to either true (t), false (f ), or undefined (u). An interpretation I is two-valued if I(a) ∈ {t, f} for all a ∈ A, and trivial (denoted Iu) if I(a) = u for all a ∈ A. For a two-valued interpretation I, I(ϕ) extends to the evaluation of a formula ϕ under I as usual. I is equally or more informative than J, denoted by J ≤i I, if J(a) ∈ {t, f} implies J(a) = I(a) for all a ∈ A. We denote by <i the strict version of ≤i, i.e., J <i I if J ≤i I and ∃a ∈ A s.t. J(a) = u and I(a) ∈ {t, f}.

An ADF is a tuple D = (A,L,C) where A is a set of arguments, L ⊆ A×A is a set of links, and C = {ϕa}a∈A is a collection of acceptance conditions for arguments a ∈ A, each given by a propositional formula over the parents of an argument: parD(a) = {b ∈ A | (b, a) ∈ L}.

The semantics of ADFs are based on the characteristic operator ΓD mapping interpretations to updated interpretations and defined for an ADF D as ΓD(I) = J with

where ϕ[I] is the formula obtained from ϕ with each argument that I assigns to either true or false being replaced by the corresponding truth constant, i.e., ϕ[I] = ϕ[x ↦→ ⊤ | I(x) = t][x ↦→ ⊥ | I(x) = f ]; arguments assigned to undefined are not modified in the resulting formula.

The intuition behind the characteristic operator is that an argument a is assigned true (false) if all completions of the given interpretation I satisfy (do not satisfy) the acceptance condition of a. A completion of an interpretation I is a twovalued interpretation J such that I ≤i J.

Definition 2.1. Given an ADF D, an interpretation I

• is admissible in D iff I ≤i ΓD(I);
• is complete in D iff I = ΓD(I);
• is grounded in D iff I is the least fixed-point of ΓD;
• is preferred in D iff I is ≤i-maximal admissible in D.

Conflict-free interpretations are defined by weakening the condition of admissible interpretations: I is conflict-free in D if, for all a ∈ A, I(a) = t implies ϕa[I] is satisfiable, and I(a) = f implies ϕa[I] is refutable (a formula is refutable if it is not a tautology). This differs from admissibility by requiring satisfiability instead of a tautology and refutability instead of unsatisfiability. A conflict-free interpretation I is a naive interpretation in D if there is no conflict-free interpretation J in D s.t. I <i J. We refer to the set of all conflict-free, naive, admissible, complete, grounded, and preferred interpretations of an ADF D as cf(D), nai(D), adm(D), com(D), grd(D), and prf(D), respectively. In any ADF D, it holds that prf(D) ⊆ com(D) ⊆ adm(D) ⊆ cf(D).

We denote the update of an interpretation I with truth value x ∈ {t, f , u} for argument b by I|bx , i.e., I|bx (b) = x and I|bx (a) = I(a) for a ̸= b. In an ADF D = (A,L,C), a link (b, a) ∈ L is called (i) supporting (in D) if for every two-valued interpretation I, I(ϕa) = t implies I|bt (ϕa) = t; (ii) attacking (in D) if for every two-valued interpretation I, I(ϕa) = f implies I|bt (ϕa) = f . D is called bipolar if each link (b, a) ∈ L is attacking or supporting.

The most important reasoning problems in ADFs are credulous and skeptical acceptance, existence of a non-trivial interpretation, and verification of an interpretation. They are defined as follows for semantics σ, given ADF D=(A, L, C):

• Credσ: Given a ∈ A, is there an I ∈ σ(D) s.t. I(a) = t?
• Skeptσ : Given a ∈ A, is I(a) = t for all I ∈ σ(D)?
• Existsσ: Is there an I ∈ σ(D) with I ̸= Iu?
• Verσ: Given an interpretation I, is I ∈ σ(D)?

Example 2.2. Let D = ({a, b, c},L,C) be an ADF with ϕa = b, ϕb = a, and ϕc = ¬a. It holds that I = {a ↦→ t, b ↦→ t, c ↦→ f} and I ′ = {a ↦→ f , b ↦→ f , c ↦→ t} are preferred in D and Iu is grounded in D. Further, a is credulously but not skeptically accepted under preferred semantics.

The known complexity results are shown in Table 1.

3 Complexity of Subclasses

In this section we present our complexity results for subclasses of ADFs, which are summarized in Table 2 (top).

Bipolar ADFs. It has been shown that reasoning in bipolar ADFs is easier [Strass and Wallner, 2015], when for each link its type is known. The results are shown in Table 2 (top left).

Acyclic ADFs. This class is defined as follows.

Definition 3.1. An ADF D = (A,L,C) is acyclic if the directed graph (A, L) is acyclic.

In acyclic ADFs we have arguments without parents (initial arguments) whose acceptance conditions are constant. This implies that |com(D)| = 1 [Keshavarzi, 2017], which follows from a bottom-up propagation of the acceptance conditions.

Proposition 3.2 ([Keshavarzi, 2017]). Any acyclic ADF has a unique two-valued complete interpretation.

Based on this result, one can compute the grounded (unique preferred) interpretation in polynomial time. Furthermore, credulous and skeptical reasoning coincide for complete based semantics and can be decided in polynomial time.

Corollary 3.3. For acyclic ADFs, Credσ, Skeptσ , Verτ are in P for σ ∈ {adm, grd, com, prf} and τ ∈ {grd, com, prf}.

Acyclicity does not help in verifying whether an interpretation is admissible (or conflict-free): e.g., asking whether it is admissible to assign a non-initial argument to true and its parents to undefined still requires to consider all completions.

Proposition 3.4. For acyclic ADFs, Veradm is coNP-complete and Vercf is NP-complete.

However, existence of non-trivial conflict-free or naive interpretations is trivial: an initial argument has a constant acceptance condition (can always be true or false).

In contrast, credulous acceptance under cf and nai remains as hard as in the general case. An argument may be false in the unique preferred interpretation, but true in a naive one.

Example 3.5. Let D = (X ∪ {y},L,C) be an ADF with ϕx = ⊤ for x ∈ X and ϕy = φ. Then, {x ↦→ u | x ∈ X} ∪ {y ↦→ t} ∈ cf(D) iff φ is satisfiable (J(y) = f for J ∈ prf(D) if φ evaluates to f when all X are assigned true).

Proposition 3.6. For acyclic ADFs, Credσ is NP-complete (σ∈{cf, nai}); Vernai is DP-complete; Skept nai is coNP-hard.

Concise ADFs. The subclass of concise ADFs is characterized by the existence of exactly one σ-interpretation.

Definition 3.7. An ADF D is concise for semantics σ (or σconcise) if |σ(D)| = 1.

For cf-concise (resp. adm-concise) ADFs there is only one interpretation that is conflict-free (resp. admissible), namely Iu. Hence, problems Credσ, Skeptσ , Existsσ (σ ∈ {cf, adm}) are always false, while Verσ is positive only for Iu.

Proposition 3.8. For σ ∈ {cf, adm}, it holds that Credσ, Skeptσ , Existsσ, and Verσ are trivial for σ-concise ADFs.

In σ-concise ADFs Credσ and Skeptσ coincide. Complexity under nai, except Skept nai , does not deviate from ADFs.

Proposition 3.9. For nai-concise ADFs, Crednai, Skept nai , and Existsnai are NP-complete; Vernai is DP-complete.

Proof (Sketch). Given a formula φ over X, let Dφ = (X ∪ {z}, L, C) with ϕx = ¬x for x ∈ X, and ϕz = φ ∨ ¬z. For any I ∈ cf(Dφ) we have I(x) = u. We have I(z) = t for some I ∈ cf(Dφ) iff ϕz[I] is satisfiable iff φ is satisfiable. Finally, I(z) ̸= f in every I ∈ cf(Dφ), as ϕz[I] is then a tautology. Hence, cf(Dφ) = {Iu, {z ↦→ t} ∪ {x ↦→ u | x ∈ X}} if φ is satisfiable and cf(Dφ) = {Iu} otherwise.

Since grounded semantics is a unique-status semantics it holds that any ADF is grd-concise. Further, the grounded interpretation is the least complete interpretation, and, thus, reasoning under grd and com coincides for com-concise ADFs.

Proposition 3.10. For com-concise ADFs, Credcom, Skept com , and Existscom are coNP-complete; Vercom is DP-complete.

Due to Valiant and Vazirani [1986] the SAT problem is NP-hard under randomized reductions if the formula has at most one model. Briefly, these reductions produce a set of instances s.t. "yes" instances are translated to a set with a certain lower bound on the number of "yes" instances. The result was generalized to quantified Boolean formulas by Dunne [2009]. Using [Strass and Wallner, 2015, Reduction 3.2], we can show the following result.

Proposition 3.11. For prf-concise ADFs, Credprf, Skept prf , and Existsprf are Σ P2 -complete under randomized reductions; Verprf is Π P2 -complete under randomized reductions.

4 Distance to Subclasses

In this section we extend our subclasses to ones containing ADFs that have a constant distance to bipolar ADFs, acyclic ADFs, or concise ADFs (for results see Table 2 (bottom)).

Distance to Bipolar ADFs. We analyze the complexity of ADFs which have a limited number of non-bipolar links.

Definition 4.1. An ADF D is k-bipolar for some integer k ≥ 0 if for each a ∈ A it holds that |{(b, a) ∈ L?D }| ≤ k.

For a k-bipolar ADF D, the (non-)polarity of links is known and L-D , L+D , and L?D denote the links of D which are attacking, supporting and neither of the two, respectively.

The main ingredient for the complexity of k-bipolar ADFs is a generalization of why BADFs exhibit milder complexity [Strass and Wallner, 2015]: to test validity of ϕ[I], fix the values of bipolar parents and check the remaining completions of I, the number of which is bounded by 2k .

Lemma 4.2. Given a k-bipolar ADF D, an interpretation I, and an argument a ∈ A, deciding whether ϕa[I] is a tautology and deciding whether ϕa[I] is unsatisfiable is in P.

It follows that reasoning on k-bipolar and bipolar ADFs has the same complexity; the proof uses the generic results of [Strass and Wallner, 2015, Theorem 3.18] and Lemma 4.2.

Theorem 4.3. Let k ≥ 0 be a constant and σ ∈ {cf, nai, adm, com, grd, prf}. It holds that the complexity of Verσ, Existsσ, Skeptσ , and Credσ coincides for k-bipolar and bipolar ADFs.

Distance to Acyclic ADFs. An ADF is k-acyclic if removing links from parents of k arguments results in acyclicity.

Definition 4.4. An ADF D = (A,L,C) is k-acyclic if there is a set B ⊆ A with |B| ≤ k s.t. (A, L \ (A × B)) is acyclic.

By fixing a truth value assignment on B and then computing the grounded interpretation on the resulting acyclic ADF (via polynomially many NP oracle calls) we get a potential preferred interpretation of the original ADF. By trying out all such assignments (bounded by 3k ), we enumerate prf(D).

Proposition 4.5. For k ≥ 0, Credσ, Existsσ, Skept prf , Verprf are in ∆ P2 for k-acyclic ADFs and σ ∈ {adm, com, prf}.

Reasoning under grd is not easier on k-acyclic ADFs, since, intuitively, the undefined value may be propagated.

Proposition 4.6. For 1-acyclic ADFs, it holds that Credgrd, Skept grd , and Existsgrd are coNP-complete.

The proof of this result relies on a small odd-attack-cycle so that an argument can be assigned to true iff a formula is unsatisfiable. This can be generalized to show the next results.

Corollary 4.7. For 1-acyclic ADFs, Credσ, Skeptσ , Existsσ, Verσ, and Vergrd are coNP-hard for σ ∈ {adm, com, prf}.

Existence of non-trivial conflict-free (naive) interpretations in k-acyclic ADFs is trivial if k < |A| and decidable in polynomial time if k ≥ |A|. In the former case, there is an argument not depending on itself (which can be assigned true or false without conflict). In the latter case, one can enumerate all truth value assignments and check for conflict-freeness.

Distance to Concise ADFs. An ADF has distance k to a σ-concise ADF if there are at most k σ-interpretations.

Definition 4.8. An ADF D is k-σ-concise for a semantics σ and some integer k ≥ 0 if |σ(D)| ≤ k.

In terms of complexity, membership carries over from general ADFs and hardness follows from concise ADFs. We can recycle the reduction from the proof of Proposition 3.9 to obtain the hardness part of the following result.

Proposition 4.9. For k-cf-concise ADFs it holds that Credcf, Existscf, and Vercf are NP-complete for every k ≥ 2.

An upper bound on the number of interpretations is beneficial for skeptical acceptance. Under prf, it allows to decide the problem with a polynomial number of Σ P2 -oracle calls. Key is that Σ P2 -membership of Existsadm can be adapted to the problem Exists>adm , asking whether there is an adm interpretation strictly more informative than a given interpretation.

Theorem 4.10. For k-prf-concise ADFs, Skept prf is in ∆ P3 .

Proof (Sketch). Let I = ∅. Construct a preferred interpretation I of D = (A, L, C) by starting with I = Iu and ask a Σ P2 oracle whether there is a J ∈ adm(D) with J >i I and no J ′ ∈ I with J ≤i J ′ . If yes, set I = J and repeat the oracle call. Otherwise, if I ̸= Iu, add I to I and proceed to find the next preferred interpretation. |prf(D)| is constant and a linear number of calls suffices to find a preferred interpretation.

Corollary 4.11. For k-nai-concise ADFs, Skept nai is in ∆ P2 .

For admissible and complete semantics, we consider it rather unlikely that Existsσ or Credσ get easier for k-σconcise ADFs with k ≥ 2. While we are not able to show Σ P2 -hardness under standard reductions, we can show it under randomized reductions giving rise to a slightly weaker result.

Proposition 4.12. Let σ ∈ {adm, com}. For k-σ-concise ADFs it holds that Existsσ and Credσ are Σ P2 -complete under randomized reductions for every k ≥ 2.

Finally, verifying admissibility of an interpretation does also not benefit from a bounded number of interpretations.

Proposition 4.13. For k-adm-concise ADFs it holds that Veradm is coNP-complete for every k ≥ 2.

Inspecting Theorem 4.3, the only problem for (k-)bipolar which is hard for the second level of the polynomial hierarchy is Skept prf . If, in addition to bipolarity, also the number of preferred interpretations is bounded, we can again show that a polynomial number of NP-oracle calls is sufficient.

Theorem 4.14. For k1-bipolar and k2-prf-concise ADFs it holds that Skept prf is in ∆ P2 .

5 Algorithms

We now present novel algorithms for ADF reasoning tasks based on results from Sections 3 and 4. We focus on Skept prf and Credadm (= Credprf), for which we present different approaches. The backbone of our algorithms are SAT solvers, to which we delegate (sub)problems that are in NP. A central subproblem is Exists>σ , which asks for a σ-interpretation strictly more informative than a given interpretation.

Proposition 5.1. Given σ ∈ {cf, nai, grd, adm, com, prf}, complexity of Exists>σ and Existsσ coincide for general, (k)- bipolar, and (k)-concise ADFs.

In what follows, we first define and discuss the encodings utilized in SAT calls, then present the base algorithms for the considered problems, and finally outline different concrete solving procedures resulting from the algorithms.

Encodings. Figure 1 shows the building blocks for the encodings, given an ADF D = (A, L, C) and an interpretation I. The formulas range over variables U = {st , sf | s ∈ A} ∪ {prs | (r, s) ∈ L}. Moreover, ϕ↓s denotes the acceptance condition ϕs where each occurrence of r ∈ parD(s) is replaced by prs . The encoding for Exists>cf is then given by ΦD,I cf = φI<i ∧ ∧s∈A(φΓs ∧ φpr s ). It is satisfiable iff there is a J ∈ cf(D) with I <i J. Intuitively, atoms st and sf represent the guess of an interpretation J, indicating that J(s) = t

Figure 1: Building blocks for encodings, given ADF D and interpretation I. Thereby, L⊖D = L-D \ L+D and L⊕D = L+D \ L-D .

(resp. J(s) = f). Subformula φI<i ensures I <i J. In order to have J ∈ cf(D), it must hold that, if J(s) = t (resp. J(s) = f) then ϕs[J] is satisfiable (resp. refutable). To this end, atoms prs represent the guess of a two-valued interpretation Js with Js ≥i J (cf. φpr s ) aiming to satisfy (resp. refute) ϕs. By that, ϕ↓s being true (resp. false) is equivalent with

ϕs[J] being satisfiable (resp. refutable), as is encoded by φΓs . For bipolar ADFs, Exists>adm is in NP. We use the encoding

ΦD,I adm,bip = φI<i ∧ φbip ∧ ∧s∈A(φΓs ∧ φpr s ) which is satisfiable iff there is a J ∈ adm(D) with I <i J. For J ∈ adm(D), ϕr[J] now has to evaluate to true (resp. false) under every completion of J if J(r) = t (resp. J(r) = f). Due to bipolarity, it suffices to check this for one particular completion of J, represented by psr for each s ∈ A. That is, if for some s ∈ parD(r) neither st nor sf is true, we can set psr according to the polarity of the link (s, r) and the value of I(r), as done by φbip. If all ϕ↓s evaluate according to the guess J under this particular valuation, J is admissible (cf. φΓs ).

By Thm. 4.3, Exists>adm ∈ NP for k-bipolar ADFs (formula size exponential in k). For s ∈ A let Xs = {r | ∃(r, s) ∈ L?D , I(r) = u} and V(Xs) be the set of two-valued interpretations over Xs. For IX ∈ V(Xs), let ϕ↓,IX s = ϕs[r ↦→ prs | (r, s) ∈ L, r /∈ Xs][r ↦→ IX(r) | (r, s) ∈ L, r ∈ Xs]. Let ΦD,I adm,kbip = φI<i ∧ φbip ∧ ∧s∈A(φΓk s ∧φpr s ), which differs from ΦD,I adm,bip by φΓk s , which is equal to φΓs if s has only bipolar incoming links and φΓ? s else. The values of the parents r connected through non-bipolar links (up to k; identified by prs ) are not determined by φbip. Instead, all completions IX of those r with J(r) = u (approximated by Xs) must be checked to satisfy (resp. refute) ϕ↓,IX s . This check can be disregarded if the values of IX(r) and J(x) differ for some non-bipolar parent r (done by the disjunctions in φΓ? s ).

Recall that the encodings not only decide the respective Exists>σ -problems, but also yield concrete interpretations J ∈ σ(D) with I <i J via assignments to variables st and sf .

Checking admissibility of an interpretation is also solved via SAT. We encode the complement, ¬Veradm, by ΦD,I ¬Veradm =

Algorithm 1 Skeptprf(D, α)

• 1: ρ ← ∅ 2: while I ← Exists>adm (D, Iu, ρ) do 3: while I ′ ←Exists>adm (D, I, ρ) do I ← I ′ 4: if I(α) ̸= t then reject else ρ ← ρ ∧ Refine>(I)
• 5: if ρ = ∅ then reject else accept

∧I(s)=t ps ∧ ∧I(s)=f ¬ps ∧ ∨I(s)=t ¬ϕ↓s ∨ ∨I(s)=f ϕ↓s with ϕ↓s = ϕs[r ↦→ pr | (r, s) ∈ L]. Variables ps represent a guess of an interpretation J ≥i I that acts as a witness for I /∈ adm(D) if either I(s) = t but ϕs[J] ≡ f (then ¬ϕ↓s is true), or I(s) = f but ϕs[J] ≡ t (then ϕ↓s is true) for some s ∈ A. Then, ΦD,I ¬Veradm is satisfiable iff I /∈ adm(D).

Algorithms. Algorithm 1 solves Skept prf (which is Π P3 -c) by implementing the idea of the membership proof of Theorem 4.10. It iteratively calls Exists>adm until a preferred interpretation is reached. Thereby, preferred interpretations already visited are ruled out by maintaining the formula ρ. This formula is refined in line 4 by Refine>(I) = ∨I(s)=t sf ∨ ∨I(s)=f st ∨ ∨I(s)=u (st ∨ sf ), i.e., all J ≤i I are excluded from now on. This is done internally, enabling incremental calls to the SAT solver. The algorithm rejects an instance if it finds a preferred interpretation such that the query argument is not mapped to t (or if it finds prf(D) = {Iu}) and accepts otherwise. By Theorem 4.10 the number of iterations in Algorithm 1 is polynomial in k for k-prf-concise ADFs, i.e., it is polynomially bounded by the number of interpretations.

Algorithm 2 implements the Σ P2 -hard problem Exists>adm for the general case. As an additional parameter, it takes the formula ρ encoding the search space of interpretations. Using the encoding ΦD,I cf , a SAT solver is employed to get a conflict-free interpretation J. If J is then found to be admissible by another SAT call using ΦD,J ¬Veradm , we can return J , otherwise we exclude J from the search space via refining ρ by Refine̸=(J) = ∨J(s)=t ¬st∨∨J(s)=f ¬sf ∨∨J(s)=u(st∨sf ).

Solvers. We denote Algorithm 1 by PRF-3, which uses Algorithm 2 for the Exists>adm subprocedure, and employs three levels of SAT which is in line with worst-case complexity. If the given ADF is bipolar, a SAT call with ΦD,I adm,bip decides Exists>adm , giving rise to PRF-BIP. Otherwise, the polarity of each link can be determined by two SAT calls as a preprocessing step, enabling Exists>adm to be decidable via a SAT

Algorithm 2 Exists>adm(D, I, ρ)

1: ρ ← ρ ∧ΦD,I cf 2: while true do 3: (τ, sat) ← SAT(ρ) 4: if sat then 5: J ←Extract(τ) #get interpretation by values of st , sf 6: if SAT(ΦD,J ¬Veradm ) then ρ ← ρ ∧ Refine̸=(J) else return J 7: else return fail

call using ΦD,I adm,kbip . We call this variant PRF-K-BIP. Adding shortcuts by (i) computing Credadm (rejecting if not accepted) and (ii) pre-computing grd(D) gives rise to PRF-K-BIP-OPT.

For Credadm with query argument s we get the procedure ADM-2 by adding st to ΦD,I cf in Algorithm 2 with parameters I = Iu and ρ = ∅. In the k-bipolar case ADM-K-BIP decides the problem by a single SAT call using ΦD,Iu adm,kbip ∧ st .

6 Experiments

We implemented above algorithms resulting in the system k++ADF, available in open source at www.cs.helsinki.fi/ group/coreo/k++adf. The implementation currently supports credulous and skeptical reasoning, and enumeration, under the semantics cf, nai, adm, com, prf, and grd, and includes MiniSAT 2.2.0 [E´en and S¨orensson, 2003] as the SAT solver. Here, we present an overview of the scalability of the approach, and a comparison to existing ADF systems.

We selected the most challenging instances from the YADF system page (www.dbai.tuwien.ac.at/proj/ adf/yadf/). These ADFs were generated from the AFs of domains ABA2AF, Planning, and Traffic from ICCMA 2017 (argumentationcompetition.org/2017/) as follows [Brewka et al., 2017a]. Given AF graphs, acceptance conditions are constructed by splitting parents into 5 groups, each constituting a subformula representing attack, group-attack, support, group-support, and exclusive or. The subfomulas are connected via ∧ or ∨ with equal probability, resulting in 300 ADFs (10 to 150 arguments for ABA2AF; 10 to 300 arguments else). Query arguments were selected by sampling uniformly at random from the set of all arguments.

For the experiments we used 2.83GHz Intel Xeon E5440 quad-core machines with 32GB RAM running Debian GNU/Linux, enforcing a 1800-sec. timeout per instance. We compared the performance of our system with goDiamond 0.6.6 [Strass and Ellmauthaler, 2017] with clingo 5.2.1 [Gebser et al., 2016], QADF 2.9.3 [Diller et al., 2015] with bloqqer 037 [Biere et al., 2011] and DepQBF 6.03 [Lonsing and Egly, 2017], and YADF 0.1.0 [Brewka et al., 2017a] with lpopt 2.2 [Bichler et al., 2016] and clingo 5.2.1.

We considered Credadm and Skept prf . Table 3 presents an overview of the mean running times and the number of timeouts, for each domain and solver considered. In the case of Credadm, ADM-K-BIP (a single SAT solver call) has the lowest mean running times (see also Figure 2 (center)). However, for the ABA2AF instances the algorithm ADM-2 produces less timeouts, albeit being slower on average. For Skept prf , the procedure PRF-K-BIP-OPT performs exceptionally well with the ABA2AF instances, also having the lowest mean running time for Planning. As can be seen also in Figure 2 (right), the experiments clearly demonstrate the viability and efficiency of our SAT-based approach, in particular when making use of k-bipolarity in PRF-K-BIP. The shortcuts used in PRF-K-BIPOPT then give another minor performance improvement.

The case of the ADM-K-BIP encoding vs the ADM-2 procedure for credulous reasoning under adm is shown in Figure 2 (left). The second level procedure performs better for some ABA2AF instances, even solving some of those for which the k-bipolar encoding produces a memory-out. We noticed that this happens when the parameter k exceeds a value of 15, and hypothesize this to be due to the size of the encoding.

7 Conclusion

In this work, we studied the complexity of subclasses of ADFs and incorporated these insights into a novel and competitive system based on incremental SAT solving. For future work, we plan to include further subclasses (see, e.g. [Polberg, 2016]) and tune the system by exploiting acyclicity.

Acknowledgments

We thank Matti J¨arvisalo for discussions on the CNF translation. This work has been supported by the Austrian Science Fund (FWF): P30168-N31, I2854, and Y698, the Academy of Finland grant 312662, and the Doctoral Programme in Computer Science (DoCS) at the University of Helsinki.