# deciding_acceptance_in_incomplete_argumentation_frameworks__12bc7954.pdf The Thirty-Fourth AAAI Conference on Artificial Intelligence (AAAI-20) Deciding Acceptance in Incomplete Argumentation Frameworks Andreas Niskanen,1 Daniel Neugebauer,2 Matti J arvisalo,1 J org Rothe2 1Helsinki Insitute for Information Technology HIIT, Department of Computer Science, University of Helsinki, Finland 2Institut f ur Informatik, Heinrich-Heine-Universit at D usseldorf, Germany Expressing incomplete knowledge in abstract argumentation frameworks (AFs) through incomplete AFs has recently received noticeable attention. However, algorithmic aspects of deciding acceptance in incomplete AFs are still underdeveloped. We address this current shortcoming by developing algorithms for NP-hard and co NP-hard variants of acceptance problems over incomplete AFs via harnessing Boolean satisfiability (SAT) solvers. Focusing on nonempty conflict-free or admissible sets and on stable extensions, we also provide new complexity results for a refined variant of skeptical acceptance in incomplete AFs, ranging from polynomial-time computability to hardness for the second level of the polynomial hierarchy. Furthermore, central to the proposed SAT-based counterexample-guided abstraction refinement approach for the second-level problem variants, we establish conditions for redundant atomic changes to incomplete AFs from the perspective of preserving extensions. We show empirically that the resulting SAT-based approach for incomplete AFs scales at least as well as existing SAT-based approaches to deciding acceptance in AFs. 1 Introduction Abstract argumentation frameworks (AFs), as originally proposed by Dung (1995), are today one of the most important and widely-studied formalisms in the field of argumentation in AI. Recently, a natural generalization of AFs to so-called incomplete argumentation frameworks (IAFs) was proposed (Coste-Marquis et al. 2007; Baumeister et al. 2018). Modeling uncertainties in terms of the existence of attacks and arguments, IAFs allow to represent structural uncertainties which may arise from dynamic changes to an AF, local views of a global AF, or uncertainties in the underlying knowledge base from which the AF is instantiated. Considering universal and existential quantification over the uncertain parts of IAFs gives rise to the respective possible and necessary generalizations of the central skeptical and credulous acceptance problems in abstract argumentation. As shown by Baumeister, Neugebauer, and Rothe (2018) via an extensive complexity analysis, these generalizations have Copyright c 2020, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved. an impact on the computational complexity of acceptance when compared to acceptance problems in AFs. However, in their complexity analysis, Baumeister, Neugebauer, and Rothe (2018) allowed for empty sets of acceptable arguments (extensions) or the non-existence of extensions, which may produce trivial answers to the skeptical acceptance (SA) problem for certain semantics. In particular, it would be more meaningful to restrict the semantics to nonempty extensions and to require the existence of at least one extension for a yes answer to SA. While SA indicates whether the target argument is among the bestaccepted arguments in the AF with respect to the given semantics, the refined variant EXSA formally defined as SA with the additional condition that an extension exists indicates whether the target argument is actually and ultimately accepted in the IAF with respect to the semantics. To address this, we consider nonempty versions of the conflictfreeness and admissibility properties, and formally study the complexity of the variants of the more natural EXSA problem over IAFs. Furthermore, algorithmic techniques for deciding acceptance in IAFs have not been thoroughly studied to date, and there is no clear idea of whether the recent successes in developing practical system implementations often based on harnessing the power of Boolean satisfiability (SAT) solvers for reasoning about acceptance in AFs can be generalized to IAFs. In this work, we address this current shortcoming by developing the first practical algorithms for deciding acceptance in IAFs. In more detail, our contributions are the following. We present direct Boolean satisfiability (SAT) encodings for deciding necessary skeptical and possible credulous acceptance in IAFs for semantics under which the problems are NPor co NP-complete (Sect. 3). Highlighting potential issues with allowing the nonexistence of extensions in the earlier proposed acceptance problems over IAFs, we propose novel problem variants with the in-built requirement that the set of extensions must be nonempty. We provide complexity results for the new problem variants, ranging from polynomial-time to second-level completeness in the polynomial hierarchy under conflict-free, admissible, and stable semantics We establish conditions for what type of atomic changes are guaranteed to be redundant from the perspective of preserving extensions of completions of IAFs (Sect. 5). While of interest on their own, this analysis proves central as a basis of SAT-based counterexample-guided abstraction refinement (CEGAR) algorithms for IAFs. We develop SAT-based CEGAR algorithms for the problem variants which are complete for the second-level of the polynomial hierarchy (Sect. 6). We empirically evaluate the scalability of the proposed SAT-based approaches to deciding acceptance in IAFs, showing that the approaches scale at least as well as stateof-the-art SAT-based approaches to deciding acceptance in (standard) AFs (Sect. 7), and that the conditions for redundant atomic changes play a central role in the scalability of the CEGAR algorithms. 2 Incomplete AFs We formally define abstract argumentation frameworks and the evaluation semantics used in this work (an overview of other semantics is given by Baroni, Caminada, and Giacomin (2018)). Definition 1. An argumentation framework (AF) consists of a (here finite) set of arguments A and a binary attack relation R A A . Acceptable sets of arguments are identified via semantics, where a set E A is conflict-free (CF) if (a,b) R for all a,b E , and E defends a A if for all (b,a) R, there exists e E with (e,b) R. A CF set E is admissible (AD) if it defends all its members, and stable (ST) if it attacks all non-members. A set of arguments satisfying a semantics s is called an s extension, and we denote the set of all s extensions of AF as s(AF). Reasoning problems for AFs are captured by the VERIFICATION (VER) and two types of ACCEPTANCE decision problems. Definition 2. Let AF = A ,R be an AF, E A , a A , and s be a semantics. (AF,E ) s-VER if and only if E s(AF); (AF,a) s-CREDULOUS-ACCEPTANCE (s-CA) if and only if there exists E s(AF) with a E ; and (AF,a) s-SKEPTICAL-ACCEPTANCE (s-SA) if and only if for all E s(AF), it holds that a E . Since the empty set is always CF and AD, the answer to CF-SA and AD-SA is always a trivial no. More interesting problems are obtained when restricting both semantics to nonempty sets we denote these restricted semantics as CF =/0 and AD =/0, respectively. Clearly, for all instances with a nonempty set of arguments, CF-VER = CF =/0-VER and AD-VER = AD =/0-VER. Also, CA (and all its generalizations) do not distinguish between CF and CF =/0 or between AD and AD =/0. Baumeister et al. (2018) studied incomplete AFs (IAFs) as a generalization of AFs, where the existence of distinguished arguments and attacks may be uncertain. Definition 3. An IAF A ,A ?,R,R? consists of definite arguments A , uncertain arguments A ?, (conditionally) definite attacks R, and uncertain attacks R?. Arguments in A definitely exist; arguments in A ? may or may not exist; attacks in R exist if and only if both incident arguments exist; and attacks in R? may or may not exist, but can exist only if both incident arguments exist. An IAF with R? = /0 is called argument-incomplete and an IAF with A ? = /0 is called attack-incomplete. Definition 4. We use R|A = R (A A ) to denote the restriction of an attack relation to an argument set A . Any AF A ,R that satisfies A A (A A ?) and R|A R (R R?)|A is a completion of IAF A ,A ?,R,R? . For an IAF, we say that a property defined for AFs holds possibly if it holds for at least one of its completions, and a property holds necessarily if it holds for all its completions. Accordingly, Baumeister, Neugebauer, and Rothe (2018) define possible and necessary generalizations of the CA and SA problems, which extend both problems to IAFs: s-PCA, s-PSA, s-NCA, and s-NSA. 3 SAT Encodings We begin by providing SAT encodings for deciding acceptance in incomplete AFs for NP and co NP variants of the problem. These first encodings extend the standard encodings for argumentation semantics (Besnard and Doutre 2004) to the incomplete case by conditioning relevant parts of the formulas with the existence of an argument or an attack. These encodings also form the basis for the SAT-based counterexample-guided approach we develop in Section 6 for deciding acceptance in incomplete AFs for problems in the second level of the polynomial hierarchy. Consider now an input IAF IAF = A ,A ?,R,R? . We use variables xa and ya for all a A A ? and ra,b for all (a,b) R R?, with the following interpretations: ya = if and only if a A , ra,b = if and only if (a,b) R , and xa = if and only if a E s(AF ), where AF = A ,R is a completion of IAF defined by the ya and ra,b variables. Naturally, ya is always true for all definite arguments, and likewise ra,b is true for all definite attacks. Further, if an uncertain argument is not included in the completion, it cannot be accepted, and all incident attacks are not included. This information is encoded as (a,b) R ra,b (a,b) R? ra,b (b,a) R? rb,a Moving on to expressing IAF semantics, the formula (ya yb ra,b) ( xa xb) encodes conflict-free sets in a completion of IAF, expressing the fact that if two arguments and an attack between them are present in the completion, one cannot accept both of the arguments. Now, defining za (b,a) R R?(xb yb rb,a) for each b A A ?, the formula ϕAD(IAF) defined as (xa ya yb rb,a) zb encodes admissible sets. Nonempty admissible semantics can now be encoded as ϕAD =/0(IAF) = ϕAD(IAF) a A A ? xa. We express stable semantics with ϕST(IAF) = ϕCF(IAF) ( xa ya) za , setting the constraint that all arguments not included in the extension are attacked by the extension. Further, we note that complete semantics can be handled similarly via conditioning on the ya and ra,b variables. Now, for s {AD, ST}, the problem s-PCA is NPcomplete and can be decided by the input formula ϕs-PCA(IAF,a) = ϕ?(IAF) ϕs(IAF) xa which is satisfiable if and only if the target argument a is possibly credulously accepted in IAF. Note that a satisfying truth assignment also yields a completion of the input IAF and an s extension of the completion where the query is included. Similarly, for s {AD =/0, ST}, the problem s-NSA is co NP-complete (for AD =/0-NSA, we show this in Remark 1). The formula ϕs-NSA(IAF,a) = ϕ?(IAF) ϕs(IAF) xa is unsatisfiable if and only if the target argument a is necessarily skeptically accepted in IAF. A satisfying truth assignment yields a counterexample completion along with an s extension not containing the query. 4 Complexity under Extension Existence Whenever AF has no s extension, it trivially holds that (AF,a) s-SA, even though (AF,a) s-CA. This behavior is exhibited by all semantics that do not guarantee the existence of an extension in particular, the CF =/0, AD =/0, and ST semantics. Dunne and Wooldridge (2009) propose a refined version of SA for such semantics that, in addition, requires the existence of an extension for a yes answer. We call this problem EXISTENCE-AND-SKEPTICAL-ACCEPTANCE (EXSA). Formally, it is the intersection of SA and the EXISTENCE (EX) problem, or equivalently, of SA and CA. For a semantics s that guarantees s(AF) = /0 for every AF, it is clear that s-EXSA = s-SA. We define generalizations of the s-EXSA problem for IAFs, namely, the s-PEXSA and s-NEXSA problems. The former is defined as follows. Given: An IAF A ,A ?,R,R? and an argument a A . Question: Does there exist a completion AF = A ,R of A ,A ?,R,R? such that AF has an s extension and for each s extension E of AF , a E ? s-NEXSA is defined analogously, except that it quantifies universally (instead of existentially) over completions. Baumeister, Neugebauer, and Rothe (2018) fully characterize the computational complexity of all variants of the CA and SA problems for IAFs. The EXSA problem and its generalizations for IAFs, as well as the restricted CF =/0 and AD =/0 semantics, add new open cases to this complexity landscape, which we cover in this work. We characterize the computational complexity of all variants of the skeptical acceptance problem and in particular, of s-EXSA for the semantics CF =/0, AD =/0, and ST. Our results (together with previously known results) are summarized in Table 1. We assume the reader to be familiar with the required notions from computational complexity theory, in particular, the classes of the polynomial and the Boolean hierarchy (Papadimitriou 1995; Rothe 2005), and the concepts of hardness and completeness based on polynomial-time many-one reductions. In particular, we consider deterministic and nondeterministic polynomial time, P and NP, the class DP from the second level of the Boolean hierarchy with its canonical complete problem 3-SAT-UNSAT (which is the intersection of 3-SAT and 3-UNSAT), and the classes Σp 2 and Πp 2 from the second level of the polynomial hierarchy with their canonical complete problems Σ2SAT and Π2SAT. As noted earlier, s-EXSA differs from s-SA only for s {CF =/0, AD =/0, ST}, which is why we focus on these semantics here. Also, neither s-CA nor its generalizations distinguishes between CF and CF =/0 or between AD or AD =/0, so all problems based on s-CA for s {CF =/0, AD =/0} inherit the complexity of the same problem s -CA for the respective base semantics s {CF, AD}. Our first result is that all variants of SA for the CF =/0 semantics can be efficiently decided. This is due to the fact that an argument is in some conflict-free set if and only if it has no self-attack, and it is in all conflict-free sets if and only if all other arguments have self-attacks. Uncertainty in the IAF can easily be resolved to meet these criteria. Proposition 1. CF =/0-SA, CF =/0-EXSA, CF =/0-PSA, CF =/0PEXSA, CF =/0-NSA, and CF =/0-NEXSA are all in P. Next, we show DP-hardness of AD =/0-EXSA by reducing from the DP-complete problem 3-SAT-UNSAT. An illustration is given in Figure 1a. Our reduction bears some similarities to the one used by Dunne and Wooldridge (2009) in their proof that ST-EXSA is DP-hard. Our reduction is different, though, due to us having to avoid unwanted AD =/0 sets that do not include the target argument. Theorem 2. AD =/0-EXSA is DP-complete. All further results are based on the standard reduction from Σ2SAT and Π2SAT problems to decision problems in IAFs, defined by Baumeister, Neugebauer, and Rothe (2018). All hardness results obtained hold even in the special cases where either A ? = /0 or R? = /0. For STPEXSA, the proof of Theorem 17 by Baumeister, Neugebauer, and Rothe (2018) which shows Σp 2-hardness of STPSA is still valid and provides the same hardness result. Corollary 3. ST-PEXSA is Σp 2-complete. For AD =/0-PSA and AD =/0-PEXSA, we show Σp 2-hardness Table 1: Overview of complexity results for variants of the standard and the refined skeptical acceptance problems, with results marked by due to Rey (2014); marked by due to Dimopoulos and Torres (1996); marked by due to Dunne and Wooldridge (2009); and marked by due to Baumeister, Neugebauer, and Rothe (2018). New results are labeled with the respective theorem or proposition number. s-SA s-EXSA s-PSA s-PEXSA s-NSA s-NEXSA CF =/0 P (Prop. 1) P (Prop. 1) P (Prop. 1) P (Prop. 1) P (Prop. 1) P (Prop. 1) AD =/0 co NP-c. DP-c. (Thm. 2) Σp 2-c. (Thm. 4) Σp 2-c. (Thm. 4) co NP-c. Πp 2-c. (Thm. 5) ST co NP-c. DP-c. Σp 2-c. Σp 2-c. (Cor. 3) co NP-c. Πp 2-c. (Thm. 5) x1 1 x1 1 x1 2 x1 2 x1 3 x1 3 x2 1 x2 1 x2 2 x2 2 x2 3 x2 3 (a) (AF, ϕ2) AD =/0-EXSA if and only if formula ϕ1 is satisfiable and formula ϕ2 is unsatisfiable. y1 y1 y2 y2 (b) (AF, ϕ) AD =/0-PSA if and only if there is an assignment to the X variables such that ϕ is unsatisfiable. Figure 1: Illustrations of the reductions from SAT problems used in Theorem 2 (left) and Theorems 4 and 5 (right). by extending the standard reduction with additional definite attacks from argument ϕ against all literal arguments and all grounded arguments. The reduction is illustrated in Figure 1b, where either the top framed part or the bottom framed part is included to obtain either R? = /0 or A ? = /0. The dotted self-attack by ϕ is not included here. Our modification does not impair admissible sets that contain argument ϕ, but has the effect that argument ϕ is a member of all nonempty admissible sets unless formula ϕ is satisfiable. Theorem 4. AD =/0-PSA and AD =/0-PEXSA are Σp 2complete. Remark 1. As a special case, when both A ? = /0 and R? = /0, we obtain a reduction from 3-UNSAT to AD =/0-SA, which provides co NP-hardness of AD =/0-SA,1 and thus also of its generalization AD =/0-NSA. For AD =/0-NEXSA and ST-NEXSA, we show Πp 2hardness by adding the definite attack ( ϕ, ϕ) (dotted attack in Figure 1b). This change disables any admissible sets containing argument ϕ. Here, yes instances of Π2SAT produce AFs that have ϕ in all stable sets, and no instances produce AFs that have completions without any nonempty admissible sets. Theorem 5. AD =/0-NEXSA and ST-NEXSA are Πp 2complete. 5 Preservation of Extensions In this section, we describe atomic changes to completions (adding and removing arguments and attacks) that are guar- 1Using different techniques, Rey (2014) showed co NPhardness of AD =/0-SA. anteed to be redundant from the point of view of preserving a given s extension of the completion. As we will show later on, these observations will prove to be crucial in designing efficient algorithms for the second-level problems in this work. Let AF = A ,R be a completion, E s(AF ) an extension, where we denote IN(E ) = E , OUT(E ) = {a A | (b,a) R with b IN(E )}, and UNDEC(E ) = A \ (IN(E ) OUT(E )), and let s {AD =/0, ST} be a semantics. We begin by considering adding an argument a A ? \ A to the completion. If there is a definite attack (b,a) R with b IN(E ), then any attacks by a against arguments in E would be defended by E in the modified completion, which ensures that E stays an extension, both under nonempty admissible and stable semantics. Proposition 6. Let IAF = A ,A ?,R,R? be an incomplete AF, AF = A ,R a completion of IAF, E s(AF ), and a A ? \A . If there exists (b,a) R with b IN(E ), then E s(AF ) for AF = A {a},R R|A {a} . We continue by considering removing arguments a A ? A from the completion. Removing arguments (along with incident attacks) that are members of OUT(E ) or of UNDEC(E ) has no effect on the current extension E . Proposition 7. Let IAF = A ,A ?,R,R? be an incomplete AF, AF = A ,R a completion of IAF, E s(AF ), and a A ? A . If a IN(E ), then E s(AF ) for AF = A \ {a},R |A \{a} . The preservation of a stable extension when removing and adding attacks was first studied by (Rienstra, Sakama, and van der Torre 2015); our results for stable naturally coincide, and we further extend the results to admissible sets. Remov- ing an uncertain attack (b,a) R? R with the source b OUT(E ) has no effect on the extension E , and neither has an attack with the target a IN(E ). Further, the fact that E is admissible is not changed by removing attacks between UNDEC(E ) arguments or from UNDEC(E ) to OUT(E ) arguments. Proposition 8. Let IAF = A ,A ?,R,R? be an incomplete AF, AF = A ,R a completion of IAF, E s(AF ), and (b,a) R? R . If b IN(E ) or a OUT(E ), then E s(AF ) for AF = A ,R \{(b,a)} . Finally, adding an uncertain attack (b,a) R? \ R is only relevant if the source b OUT(E ) and if the target a IN(E ), assuming b,a A . This is due to the fact that attacks by OUT(E ) arguments are defended and thus inactivated by E . Similarly, adding any attacks against OUT(E ) arguments has no effect on E . Finally, the admissibility of E is not changed by adding attacks between UNDEC(E ) arguments or from IN(E ) arguments to UNDEC(E ) arguments. The assumption b,a A suffices, since if b A or a A , we would first need to add the argument in order to add the attack, and we only consider atomic changes. Proposition 9. Let IAF = A ,A ?,R,R? be an incomplete AF, AF = A ,R a completion of IAF, E s(AF ), and (b,a) R?\R with b,a A . If b OUT(E ) or a IN(E ), then E s(AF ) for AF = A ,R {(b,a)} . We note that there is a substantial amount of research on the dynamic aspects of AFs (see (Doutre and Mailly 2018) for an overview), in particular on the impact of the addition and removal of arguments and attacks on the semantics, which we overview in Section 8. 6 Second-level Algorithms Complementing the complexity results, we develop an iterative SAT-based approach to s-PEXSA for s {AD =/0, ST}, both of which are Σp 2-complete and hence beyond the reach of polynomial-size direct SAT encodings. In particular, we develop a SAT-based counterexample-guided abstraction refinement (CEGAR) approach for these problems. In solving the problems, we are essentially looking for a witness completion in which the query argument is skeptically accepted, i.e., included in every s extension. The CEGAR approach, presented in pseudocode as Algorithm 1, is based on the idea of starting with an NP abstraction of the problem at hand, overapproximating the set of witnesses for the actual problem to be solved. Concretely, we use the corresponding s-PCA problem as the NP abstraction via ABSTRACTION(IAF,a) = ϕs-PCA(IAF,a). If ABSTRACTION(IAF,a) is unsatisfiable, we can reject the query, as it is not even possibly credulously accepted. If it is satisfiable, we know that a is credulously accepted in the completion AF = EXTRACT(τ) = A ,R given by the satisfying truth assignment τ via A = {a A A ? | τ(ya) = }, R = {(a,b) R R? | τ(ra,b) = }. Algorithm 1 CEGAR for possible existence and skeptical acceptance for s {AD =/0, ST}. Input: IAF = A ,A ?,R,R? , a A . 1: ϕ ABSTRACTION(IAF,a) 2: while true do 3: (sat,τ) SAT(ϕ) 4: if sat = false then return reject 5: AF EXTRACT(τ) 6: (sat,τ) SAT(CHECK(IAF,AF ,a)) 7: if sat = false then return accept 8: ϕ ϕ REFINE(IAF,AF ) 9: end while We continue by checking whether it is skeptically accepted, which is accomplished with the input formula CHECK(IAF,AF ,a) = ϕs-NSA(IAF,a) COMPLETION(IAF,AF ), where COMPLETION(IAF,AF ) is defined by a (A A ?)\A ya (a,b) R ra,b (a,b) (R R?)\R ra,b and encodes the current completion AF . If CHECK(IAF,AF ,a) is unsatisfiable, this proves that we have successfully found a witness completion for skeptical acceptance of a, and can accept the argument. If it is satisfiable, this is not the case as we have shown that there exists an extension E s(AF ) not containing the query argument, so we refine the abstraction by adding the clause REFINE(IAF,AF ) = COMPLETION(IAF,AF ) to the SAT solver, excluding the current completion, and continue iteratively. We would ideally like to exclude all completions which still possess the counterexample E as an s extension, since these would only cause more undesired iterations in the CEGAR algorithm. Due to results in Section 5, the following strong refinement is also valid, and excludes certain other completions which contain the counterexample extension: REFINE(IAF,AF ,E ) = a A ? IN(E ) ya a A ?\A (b,a) R,b IN(E ) (a,b) R? R (IN(E ) OUT(E )) ra,b (a,b) (R?\R ) ((IN(E ) UNDEC(E )) IN(E )) ra,b. While our focus is on the Σp 2-complete problems of AD =/0-PEXSA and ST-PEXSA, a similar CEGAR approach can be obtained for the Πp 2-complete problem AD-NCA by modifying Algorithm 1 as follows. We initialize the abstraction with ϕAD-NSA(IAF,a), since we are now looking for a counterexample, i.e., a completion AF where a is not credulously accepted. We check using ϕAD-PCA(IAF,a) COMPLETION(IAF,AF ) whether the counterexample candidate is not valid, that is, whether there is an extension containing a, implying credulous acceptance for that completion, in which case we refine the abstraction by excluding the completion. Finally, the roles of accept and reject are naturally swapped. The problem ST-NCA, which is also Πp 2-complete, requires more modifications, since the abstraction initialized with ϕST-NSA(IAF,a) only considers those AFs which have a stable extension not containing a, that is, we would end up accepting a even though there might exist completions without a stable extension. If the abstraction becomes unsatisfiable, we iteratively call the SAT solver with input formula ϕST-PCA(IAF,a), excluding the completion using the refinement. Finally, we check using ϕ?(IAF) ϕCF(IAF) whether there still are completions; if so, we reject the query, since these completions have no stable extension, and otherwise we accept it. 7 Experiments We continue by an overview of results from an empirical evaluation of the scalability of the approaches to acceptance problems in incomplete AFs presented in this paper. Our implementation uses Glucose 4.1 (Audemard and Simon 2018) as the underlying SAT solver, and is available in open source via https://bitbucket.org/andreasniskanen/ taeydennae. The experiments were run on Intel Xeon E52680 v4 2.4-GHz, 256-GB machines with Cent OS 7. We set a per-instance time limit of 900 seconds and a per-instance memory limit of 64 GB. We generated incomplete AFs based on the ICCMA 2017 (Gaggl et al. 2016) benchmarks as follows. For each AF, we select a query argument uniformly at random from the set of arguments. Now, for each probability p {0.05,0.1,0.15,0.2}, we generated three incomplete AFs: one where each argument (except for the query) is uncertain with probability p, one where each attack is uncertain with probability p, and one where each argument and attack is uncertain with probability p. We used the ICCMA 2017 benchmark set A for problems on the second level and the set B for problems on the first level, in-line with the complexity of the acceptance problems for which these sets were used in ICCMA 2017. This resulted in a total of 4200 IAFs for each of the two ICCMA 2017 benchmark sets. For the NP-complete problems AD-PCA and ST-PCA, and the co NP-complete problems AD =/0-NSA and ST-NSA, the mean run times (with timeouts included as the timeout limit of 900 seconds) are visualized in Figure 2, 3, and 4 (left) for different values of p and argument-incompleteness or attack-incompleteness. Interestingly, the empirical hardness of the instances does not increase as incompleteness is increased; in fact, we are able to solve the corresponding incomplete instance sets in general faster than for p = 0, which is exactly the original ICCMA benchmark set (i.e., normal acceptance problems over AFs), especially when introducing attack-incompleteness. Indeed, the maximum number of timeouts (28/350) is observed on ST-NSA for p = 0. 0.00 0.05 0.10 0.15 0.20 0 20 40 60 80 100 NP encodings mean run time (seconds) AD PCA ST PCA NEAD NSA ST NSA 0.00 0.05 0.10 0.15 0.20 0 50 100 150 200 250 300 CEGAR for PEx SA mean run time (seconds) NEAD (strong) ST (strong) NEAD (trivial) ST (trivial) Figure 2: Mean run times (with timeouts included as 900s) for purely argument-incomplete AFs for the problems on the first (left) and the second (right) level. 0.00 0.05 0.10 0.15 0.20 0 20 40 60 80 100 NP encodings mean run time (seconds) AD PCA ST PCA NEAD NSA ST NSA 0.00 0.05 0.10 0.15 0.20 0 50 100 150 200 250 300 CEGAR for PEx SA mean run time (seconds) NEAD (strong) ST (strong) NEAD (trivial) ST (trivial) Figure 3: Mean run times (with timeouts included as 900s) for purely attack-incomplete AFs for the problems on the first (left) and the second (right) level. 0.00 0.05 0.10 0.15 0.20 0 20 40 60 80 100 NP encodings mean run time (seconds) AD PCA ST PCA NEAD NSA ST NSA 0.00 0.05 0.10 0.15 0.20 0 50 100 150 200 250 300 CEGAR for PEx SA mean run time (seconds) NEAD (strong) ST (strong) NEAD (trivial) ST (trivial) Figure 4: Mean run times (with timeouts included as 900s) for general incomplete AFs for the problems on the first (left) and the second (right) level. The Σp 2-complete problems AD =/0-PEXSA and ST-PEXSA are solved via the CEGAR approach. Similarly, we show the mean run times (with timeouts included) in Figure 2, 3, and 4 (right). In contrast to the NP encodings, introducing uncertainty makes the instances significantly harder to solve. We suspect this to be due to the fact that the number of potential completions to guess and check is exponential in the number of uncertain elements. However, the strong refinements, resulting from the analysis presented in Section 5, significantly speed-up the CEGAR approach; mean run times when using the trivial refinement are considerably higher than when using the strong refinement, especially for AD =/0-PEXSA, to the extent that the strong refinements are central in making the CEGAR approach viable for deciding acceptance in incomplete AFs. As a concrete example, for AD =/0-PEXSA the average runtime over solved instances is only 24.3 seconds with p = 0.2 on general IAFs using the strong refinement, with 104/350 timeouts, as compared to 39.6 seconds and 225/350 timeouts for the trivial refinement, indicating that we improve especially with respect to the number of timeouts. 8 Related work Other models that, like IAFs, aim to represent uncertainty or dynamics in abstract AFs include Partial AFs (PAFs), Control AFs (CAFs), and various types of probabilistic AFs. For PAFs (which are interchangeable with attack-incomplete AFs), Cayrol, Devred, and Lagasquie-Schiex (2007) develop new, dedicated semantics, opposed to the approach of IAFs, where the semantics of an incomplete AF are derived from the standard semantics via its completions. CAFs due to Dimopoulos, Mailly, and Moraitis (2018) were developed to capture strategic scenarios and, like IAFs, feature uncertain elements. Even though CAFs have a more specific role, IAF problems can be represented by corresponding CAFs problems, indicating that algorithmic and complexity results for IAFs could be reused to fuel similar results for CAFs. Finally, different types of quantitative uncertainty in AFs were proposed, where a numerical probability is associated with individual arguments or attacks (Pr AFs due to Li, Oren, and Norman (2011)); with elements in an underlying knowledge base from which the AF is created (Rienstra 2012); or with entire substructures of the AF (Hunter 2014). Of these models, only Pr AFs are similar to IAFs in that they allow independently uncertain arguments and attacks. However, the increased expressiveness due to the explicit probabilities as opposed to the unquantified uncertainty in IAFs comes at the cost of FP#P-completeness for most reasoning problems in Pr AFs, as shown by Fazzinga, Flesca, and Parisi (2015). Closely related to the analysis presented in Section 5, Cayrol, Dupin de Saint-Cyr, and Lagasquie-Schiex (2010) study the problem of adding an argument and incident attacks, specifically by studying necessary and sufficient conditions for satisfying different properties, also defining the atomic changes (adding and removing arguments and attacks) we study in the context of incomplete AFs. However, their focus is on grounded and preferred semantics, whereas we consider admissible and stable semantics. Semantical change when removing an argument along with incident attacks was studied by Bisquert et al. (2011) under preferred, stable, and grounded semantics, also focusing on the satisfaction of properties of extensions. The preservation of the grounded extension was studied by Boella, Kaci, and van der Torre (2009; 2010) when removing arguments and attacks, or adding attacks; again, we focus on admissible and stable extensions. Finally, the work of Rienstra, Sakama, and van der Torre (2015) focuses on the preservation of grounded, complete, preferred, stable, and semistable labelings under changes to the attack structure, and their results for the stable semantics coincide with ours. The problem of adding an argument along with incident attacks is also related to expansions (Baumann and Brewka 2010; Baumann 2012b; 2012a), where sets of new arguments along with incident attacks are added to an AF. Likewise, removing arguments has been studied in the form of deletions (Baumann 2014). There may be potential for using further theoretical results of expansion, deletion, and update equivalence in order to strengthen the refinement in the CEGAR algorithm. However, equivalence is a considerably more general concept, as it concerns preserving all extensions of a given AF, whereas in our approach we are interested in preserving just the counterexample. The SAT-based approaches developed in this work continue the successful line of work on applying SAT-based approaches to reason about argument acceptance in standard AFs (Dvoˇr ak et al. 2014; Cerutti, Giacomin, and Vallati 2019) and dynamic problems in AFs, including extension (Wallner, Niskanen, and J arvisalo 2017) and status (Niskanen, Wallner, and J arvisalo 2016) enforcement. The strong refinements we develop may also be applicable for other hard problems dealing with dynamic aspects of argumentation frameworks; so far, similar ideas have only been applied in the specific context of the NP-complete problem of extension enforcement under grounded semantics (Niskanen, Wallner, and J arvisalo 2018), in contrast to the second-level problems we develop algorithms for here. 9 Conclusion Incomplete AFs are a natural generalization of Dung s abstract argumentation frameworks, allowing for representing uncertainties that may arise in various settings. This work makes progress in computational aspects of incomplete AFs in terms of both theory and practice, focusing on acceptance problems. From the theoretical perspective, we proposed natural refinements of the skeptical acceptance problem and its generalizations over incomplete AFs, and provided complexity results for the new variants. From the practical perspective, we developed the first algorithmic approaches to acceptance in incomplete AF, covering both first-level (via direct SAT encodings) and second-level (via SAT-based counterexample-guided abstraction refinement) acceptance problems. Combining theory and practice, we also provided conditions for atomic changes to completions of incomplete AFs being redundant in terms of preserving an extension of a completion. This analysis is central to scaling up the SAT-based algorithms for second-level acceptance problems by allowing for significantly stronger abstraction refinement steps. The promising empirical results encourage further work on extending the SAT-based approach to acceptance in incomplete AFs to cover further semantics and problem variants; this also calls for further analysis towards strong refinements for the CEGAR approach. Acknowledgements This work has been financially supported in part by Academy of Finland (grants 276412, 312662, 322869), University of Helsinki Doctoral Programme in Computer Science, and by DFG grant RO 1202/14-2. Audemard, G., and Simon, L. 2018. On the Glucose SAT solver. Int. J. Artif. Intell. Tools 27(1):1 25. Baroni, P.; Caminada, M.; and Giacomin, M. 2018. Abstract argumentation frameworks and their semantics. In Handbook of Formal Argumentation. College Publications. 159 236. Baumann, R., and Brewka, G. 2010. Expanding argumentation frameworks: Enforcing and monotonicity results. In Proc. COMMA, volume 216 of FAIA, 75 86. IOS Press. Baumann, R. 2012a. Normal and strong expansion equivalence for argumentation frameworks. Artif. Intell. 193:18 44. Baumann, R. 2012b. What does it take to enforce an argument? Minimal change in abstract argumentation. In Proc. ECAI, volume 242 of FAIA, 127 132. IOS Press. Baumann, R. 2014. Context-free and context-sensitive kernels: Update and deletion equivalence in abstract argumentation. In Proc. ECAI, volume 263 of FAIA, 63 68. IOS Press. Baumeister, D.; Neugebauer, D.; Rothe, J.; and Schadrack, H. 2018. Verification in incomplete argumentation frameworks. Artif. Intell. 264:1 26. Baumeister, D.; Neugebauer, D.; and Rothe, J. 2018. Credulous and skeptical acceptance in incomplete argumentation frameworks. In Proc. COMMA, volume 305 of FAIA, 181 192. IOS Press. Besnard, P., and Doutre, S. 2004. Checking the acceptability of a set of arguments. In Proc. NMR, 59 64. Bisquert, P.; Cayrol, C.; Dupin de Saint-Cyr, F.; and Lagasquie-Schiex, M. 2011. Change in argumentation systems: Exploring the interest of removing an argument. In Proc. SUM, volume 6929 of LNCS, 275 288. Springer. Boella, G.; Kaci, S.; and van der Torre, L. 2009. Dynamics in argumentation with single extensions: Abstraction principles and the grounded extension. In Proc. ECSQARU, volume 5590 of LNAI, 107 118. Springer. Boella, G.; Kaci, S.; and van der Torre, L. 2010. Dynamics in argumentation with single extensions: Attack refinement and the grounded extension (extended version). In Proc. Arg MAS, volume 6057 of LNCS, 150 159. Springer. Cayrol, C.; Devred, C.; and Lagasquie-Schiex, M. 2007. Handling ignorance in argumentation: Semantics of partial argumentation frameworks. In Proc. ECSQARU, volume 5590 of LNAI, 259 270. Springer. Cayrol, C.; Dupin de Saint-Cyr, F.; and Lagasquie-Schiex, M. 2010. Change in abstract argumentation frameworks: Adding an argument. J. Artif. Intell. Res. 38:49 84. Cerutti, F.; Giacomin, M.; and Vallati, M. 2019. How we designed winning algorithms for abstract argumentation and which insight we attained. Artif. Intell. 276:1 40. Coste-Marquis, S.; Devred, C.; Konieczny, S.; Lagasquie Schiex, M.; and Marquis, P. 2007. On the merging of Dung s argumentation systems. Artif. Intell. 171(10):730 753. Dimopoulos, Y., and Torres, A. 1996. Graph theoretical structures in logic programs and default theories. Theoret. Comput. Sci. 170(1):209 244. Dimopoulos, Y.; Mailly, J.; and Moraitis, P. 2018. Control argumentation frameworks. In Proc. AAAI, 4678 4685. AAAI Press. Doutre, S., and Mailly, J. 2018. Constraints and changes: A survey of abstract argumentation dynamics. Argument & Computation 9(3):223 248. Dung, P. M. 1995. On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games. Artif. Intell. 77(2):321 357. Dunne, P., and Wooldridge, M. 2009. Complexity of abstract argumentation. In Argumentation in Artificial Intelligence. Springer. 85 104. Dvoˇr ak, W.; J arvisalo, M.; Wallner, J. P.; and Woltran, S. 2014. Complexity-sensitive decision procedures for abstract argumentation. Artif. Intell. 206:53 78. Fazzinga, B.; Flesca, S.; and Parisi, F. 2015. On the complexity of probabilistic abstract argumentation frameworks. ACM T. Comput. Log. 16(3):22. Gaggl, S. A.; Linsbichler, T.; Maratea, M.; and Woltran, S. 2016. Introducing the second international competition on computational models of argumentation. In Proc. SAFA, volume 1672 of CEUR Workshop Proceedings, 4 9. CEURWS.org. Hunter, A. 2014. Probabilistic qualification of attack in abstract argumentation. Int. J. Approx. Reason. 55(2):607 638. Li, H.; Oren, N.; and Norman, T. 2011. Probabilistic argumentation frameworks. In Proc. TAFA, volume 7132 of LNAI, 1 16. Springer. Niskanen, A.; Wallner, J. P.; and J arvisalo, M. 2016. Optimal status enforcement in abstract argumentation. In Proc. IJCAI, 1216 1222. AAAI Press. Niskanen, A.; Wallner, J. P.; and J arvisalo, M. 2018. Extension enforcement under grounded semantics in abstract argumentation. In Proc. KR, 178 183. AAAI Press. Papadimitriou, C. 1995. Computational Complexity. Addison-Wesley, 2nd edition. Reprinted with corrections. Rey, L. 2014. Complexity of abstract argumentation. Master s thesis, Heinrich-Heine-Universit at D usseldorf, Institut f ur Informatik, D usseldorf, Germany. Rienstra, T.; Sakama, C.; and van der Torre, L. 2015. Persistence and monotony properties of argumentation semantics. In Proc. TAFA, volume 9524 of LNCS, 211 225. Springer. Rienstra, T. 2012. Towards a probabilistic Dung-style argumentation system. In Proc. AT, volume 918 of CEUR Workshop Proceedings, 138 152. CEUR-WS.org. Rothe, J. 2005. Complexity Theory and Cryptology. An Introduction to Cryptocomplexity. EATCS Texts in Theoretical Computer Science. Springer. Wallner, J. P.; Niskanen, A.; and J arvisalo, M. 2017. Complexity results and algorithms for extension enforcement in abstract argumentation. J. Artif. Intell. Res. 60:1 40.