# optimal_status_enforcement_in_abstract_argumentation__8ddd511b.pdf Optimal Status Enforcement in Abstract Argumentation Andreas Niskanen and Johannes P. Wallner and Matti Järvisalo Helsinki Institute for Information Technology HIIT, Department of Computer Science, University of Helsinki, Finland We present complexity results and algorithms for optimal status enforcement in abstract argumentation. Status enforcement is the task of adjusting a given argumentation framework (AF) to support given positive and negative argument statuses, i.e., to accept and reject specific arguments. We study optimal status enforcement as the problem of finding a structurally closest AF supporting given argument statuses. We establish complexity results for optimal status enforcement under several central AF semantics, develop constraint-based algorithms for NP and second-level complete variants of the problem, and empirically evaluate the procedures. 1 Introduction Argumentation is a central topic in modern Artificial Intelligence research [Bench-Capon and Dunne, 2007], motivated by a range of applications in domains such as legal reasoning, multi-agent systems, and decision support [Bench-Capon et al., 2009; Mc Burney et al., 2012; Amgoud and Prade, 2009]. Argumentation frameworks (AFs) [Dung, 1995] have become the graph-based formal model of choice for many approaches to argumentation in AI, with semantics defining sets of jointly acceptable arguments, i.e., extensions. Computational approaches with system implementations for reasoning over AFs have recently received notable attention. Two central AF reasoning problems are skeptical and credulous acceptance, i.e., determining if a given argument is supported by a given AF and AF semantics in terms of the argument belonging to all resp. some extensions of the AF. These problems are static (or non-dynamic ), i.e., defined over a fixed AF. As argumentation is inherently a dynamic process, understanding AF dynamics is an important research problem [Baumann, 2012a; Baumann and Brewka, 2015; Bisquert et al., 2013; Coste-Marquis et al., 2014a; 2014b; Delobelle et al., 2015; Diller et al., 2015]. Central to AF dynamics is the question of how a given AF itself should be adjusted in analogy with belief change in light of new knowledge on the arguments the AF should support. Computational approaches to reasoning about AF dynamics are currently at an early stage of development com- pared to systems for static AF reasoning problems. Extension enforcement [Baumann, 2012b; Bisquert et al., 2013; Coste-Marquis et al., 2015; Wallner et al., 2016] where, given an AF and a subset of arguments, the task is to find a structurally closest AF that contains the specified subset as (part of) an extension is one of few AF dynamics problems for which first computational approaches have been recently proposed [Coste-Marquis et al., 2015; Wallner et al., 2016]. In this work we focus on status enforcement, a form of AF reasoning that brings together concepts from static credulous/skeptical acceptance and AF dynamics, most closely, extension enforcement. Status enforcement is the task of adjusting a given argumentation framework (AF) to support given positive and negative argument statuses, i.e., adjusting an AF to accept and reject credulously or skeptically specific arguments. Intuitively, by enforcing credulously sets of positive and negative argument statuses, any solution AF to the status enforcement problem supports a point of view in terms of the positive arguments, at the same time ruling out support for the negative arguments. In the skeptical counterpart, the positive arguments must be supported without any conflicting points of views . In this work we take on the task of optimal status enforcement, i.e., finding a structurally closest AF wrt changes to the attack structure of the AF, supporting given argument statuses. Our main contributions are the following. (i) For understanding status enforcement, we establish fundamental properties of the problem with connections to extension enforcement and static acceptance problems. (ii) We establish the computational complexity of optimal status enforcement under central AF semantics (conflict-free, admissible, stable, complete, grounded, and preferred) and parameterizations wrt negative statuses of arguments. Specifically, we identify polynomial-time solvable and NPand second-level P 2 -complete variants of the problem. (iii) We give algorithms for optimal status enforcement, including direct constraint encodings for the NP-complete variants, and counterexample-guided abstraction refinement algorithms based on constrained optimization solvers for variants complete for the second-level of the polynomial hierarchy; and empirically evaluate a prototype implementation of the approaches. Our status enforcement system implementation together with benchmarks used in this paper, as well as full formal proofs of our complexity results, are available via http://www.cs.helsinki.fi/group/coreo/pakota/. Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence (IJCAI-16) 2 Preliminaries We recall argumentation frameworks (AFs) [Dung, 1995] and main acceptability AF semantics [Baroni et al., 2011]. Definition 1. An argumentation framework (AF) is a pair F = (A, R) where A is a finite set of arguments and R A A is the attack relation. The pair (a, b) 2 R means that a attacks b. An argument a 2 A is defended (in F) by a set S A if, for each b 2 A such that (b, a) 2 R, there exists a c 2 S such that (c, b) 2 R. Example 1. Let F = (A, R) be an AF with A = {a, b, c, d} and R = {(a, b), (b, c), (c, d)}. The corresponding graph representation is shown in Figure 1a. Semantics for AFs are defined through functions σ which assign to each AF F = (A, R) a set σ(F) 2A of extensions. We consider for σ the functions stb, adm, com, grd, and prf , which stand for stable, admissible, complete, grounded, and preferred, respectively. Definition 2. Given an AF F = (A, R), the characteristic function FF : 2A ! 2A of F is FF (S) = {a 2 A | a is defended by S}. Moreover, for a set S A, the range of S is S+ R = S [ {b | (a, b) 2 R, a 2 S}. Definition 3. Let F = (A, R) be an AF. A set S A is conflict-free (in F), if there are no a, b 2 S, such that (a, b) 2 R. We denote the collection of conflict-free sets of F by cf (F). For a conflict-free set S 2 cf (F), it holds that S 2 stb(F) iff S+ S 2 adm(F) iff S FF (S); S 2 com(F) iff S = FF (S); S 2 grd(F) iff S is the least fixed-point of FF ; S 2 prf (F) iff S 2 adm(F) and there is no T 2 adm(F) with S T. For any AF F it holds that cf (F) adm(F) com(F) prf (F) stb(F). We use σ-extension to refer to an extension under a semantics σ. As for enforcement operators [Baumann, 2012b; Coste Marquis et al., 2015; Wallner et al., 2016], strict enforcement requires that the given set P of arguments has to be a σ-extension, while in non-strict enforcement P is required to be part of a σ-extension. We denote the set of attack structures that strictly enforce P under σ for F by enf σ s (F, P) = {R0 | F 0 = (A, R0), P 2 σ(F 0)}, and by enf σ ns(F, P) = {R0 | F 0 = (A, R0), 9E 2 σ(F 0) st E P} the non-strict enforcement. The number of changes of an enforcement is the symmetric difference |R R0| of two attack structures R and R0, i.e., |R \ R0| + |R0 \ R|. The optimization problem for extension enforcement is then as follows. Extension enforcement (x 2 {s, ns}) Input: AF F = (A, R), P A, and semantics σ. Task: Find an AF F = (A, R ) with R 2 arg min R02enf σ 3 Optimal Status Enforcement In this section we define and give properties of the optimal status enforcement problem. The operators underlying status enforcement modify the attack structure of a given AF F based on two given sets of arguments, P and N, where P \ N = ;. From here on, we will consistently use P and N to denote the sets of arguments that are to be so-called positively and negatively enforced, respectively. We will consider both credulous and skeptical variants of the status enforcement problem. For the credulous case, the pair (P, N) is said to be enforced in an AF F 0 if (i) each argument in P is credulously accepted in F 0; and (ii) each argument in N is not credulously accepted in F 0. In the dual, skeptical case, for (P, N) to be enforced in F 0 we require that (i) each argument in P is skeptically accepted in F 0; and (ii) each argument in N is not skeptically accepted, in F 0. In status enforcement, we are given an AF F and the two subsets of its arguments, P and N, and the task is to find an AF F 0 that is structurally close to F and in which (P, N) is enforced. Formally, we define the modified attack structures for a given AF F = (A, R) for credulous status enforcement as follows. We denote by cred(F, P, N, σ) the set {R0 | F 0 = (A, R0), P σ(F 0), N \ σ(F 0) = ;}. In words, in the modified AF F 0, all arguments in P are credulously accepted (in the union of all σ-extensions), and each argument in N is not credulously accepted (excluded from the union of σ-extensions). For skeptical status enforcement, we denote by skept(F, P, N, σ) the set {R0 | F 0 = (A, R0), P σ(F 0), N \ σ(F 0) = ;}. In words, in all modified attack structures each argument in P is contained in all σ-extensions, while each argument in N is excluded from at least one σ-extension. Note that, by definition, A T σ(F 0) if σ(F 0) = ;. From the considered semantics in this paper, only the stable semantics may admit no extensions for a given AF. This means that if N = ;, every positive set P A can be skeptically enforced under stable semantics by an AF F 0 that has no stable extensions. In light of this, we require for skeptical enforcement from here on that σ(F 0) 6= ;, i.e., the modified AF admits at least one σextension. In summary, optimal status enforcement is defined as follows. Optimal Credulous Status Enforcement Input: AF F = (A, R), P, N A, and semantics σ. Task: Find an AF F = (A, R ) with R 2 arg min R02cred(F,P,N,σ) Optimal Skeptical Status Enforcement Input: AF F = (A, R), P, N A, and semantics σ. Task: Find an AF F = (A, R ) with R 2 arg min R02skept(F,P,N,σ) Figure 1: Examples: (a) An AF; (b) (e) Status enforcement under preferred semantics: enforcing P = {d} (b) credulously, (c) skeptically; enforcing P and N = {a} (d) credulously, (e) skeptically. Example 2. In AF F in Figure 1a, the set {a, c} is the unique preferred extension. By introducing an attack from b to a (Figure 1b) which yields AF F 0, we change the preferred extensions to prf (F 0) = {{a, c}, {b, d}}. Thus, under preferred semantics, d is credulously accepted in F 0. To enforce a positive skeptical status to d under preferred semantics, one can introduce an attack from a to c in F (Figure 1c). For enforcing P = {d} and N = {a} under preferred semantics, Figure 1d illustrates credulous status enforcement. Here the attack from b to a ensures that there is an admissible set containing d, and the self-attack on a enforces that this argument is not contained in any conflict-free set. For skeptical status enforcement with the same sets P and N, Figure 1e shows an optimal modification. In this AF we have two preferred extensions {a, d} and {b, d}, which implies that d is skeptically accepted under preferred semantics, while a is not skeptically accepted under preferred semantics, although a is still contained in one preferred extension. We now show fundamental properties of the status enforcement operators. We begin with connecting them to extension enforcement. First, in case of so-called unique-status semantics, i.e., semantics σ that admit exactly one extension for each AF F (|σ(F)| = 1), non-strict extension enforcement and enforcing credulous and skeptical statuses coincide when N = ;. From the semantics considered in this paper, grounded semantics is a unique-status semantics. Further, strict extension enforcement coincides with enforcing credulous and skeptical statuses when N = A \ P. Proposition 1. Let F = (A, R) be an AF, P A, N = A \ P, and σ a unique-status semantics. It holds that ns(F, P) = cred(F, P, ;, σ) = skept(F, P, ;, σ); enf σ s (F, P) = cred(F, P, N, σ) = skept(F, P, N, σ). A further observation is that if we enforce P to be contained in (or equal to) a σ-extension by an AF F 0, then F 0 also enforces positive credulous statuses to arguments in P. Further, if we enforce a positive skeptical status to a set of arguments P by an AF F 0, then F 0 also enforces a positive credulous status to all arguments in P. Recall that we require for enforcing positive skeptical statuses that at least one σ-extension exists in the modified AF. Proposition 2. The following inclusions hold for any AF F = (A, R), P A, N = A \ P, x 2 {ns, s}, and semantics σ. x(F, P) cred(F, P, ;, σ); enf σ s (F, P) skept(F, ;, N, σ); skept(F, P, ;, σ) cred(F, P, ;, σ). An important question is which pairs of (P, N) can be enforced credulously or skeptically. For all the semantics we consider, there is always an enforcing AF for credulous status enforcement, while for enforcing skeptical statuses, there always exists a solution under complete, grounded, and preferred semantics. Proposition 3. Let F = (A, R) be an AF, P, N A two disjoint sets, σ 2 {cf , adm, com, grd, prf , stb}, and σ0 2 {com, grd, prf }. It holds that cred(F, P, N, σ) 6= ; and skept(F, P, N, σ0) 6= ;. Proof. (sketch) For enforcing credulous statuses, it holds that for AF F 0 = (A, R0) with R0 = {(n, n) | n 2 N} we have R0 2 cred(F, P, N, σ), except in the case with σ = stb and N A. In that case, let x0 2 (A \ N) be an arbitrary but fixed argument. It holds that R00 2 cred(F, P, N, stb) for F 00 = (A, R00) with R00 = {(x0, n) | n 2 N}. For enforcing skeptical statuses under complete, grounded, and preferred semantics, note that A \ N is the grounded and unique complete and preferred extension of F 0. Enforcing skeptical statuses is trivial under conflict-free, admissible, and other semantics that always admit the empty extension. To see this, note that T σ(F) = ; if ; 2 σ(F). Proposition 4. Let F = (A, R) be an AF, P, N A two disjoint sets, and σ a semantics. Further, let R = skept(F, P, N, σ). If σ admits the empty extension for all AFs, i.e. for all AFs F 0 we have ; 2 σ(F 0), then R = 2A A if P = ;, and R = ; otherwise. For stable semantics, the possibility of enforcing skeptical statuses depends on whether we have N = A or not. This is because if E 2 stb(F), then E contains at least one argument (except for the trivial AF with A = ;). Thus, enforcing a negative skeptical status to all arguments in a framework under stable semantics is not possible. Otherwise, if N A, one can construct an AF with only attacks originating from an arbitrary argument in A \ N to all arguments in N. Proposition 5. Let F = (A, R) be an AF. It holds that skept(F, ;, A, stb) = ;. If P, N A are two disjoint sets with N A, then skept(F, P, N, stb) is non-empty. As is the case for credulous and skeptical acceptance in the static, non-dynamic case, enforcing credulous statuses for admissible sets and complete and preferred semantics coincides. Further, enforcing credulous and skeptical statuses under grounded semantics coincides with enforcing skeptical statuses under complete semantics. Proposition 6. Let F = (A, R) be an AF, P, N A two disjoint sets. It holds that cred(F, P, N, adm)=cred(F, P, N, com)=cred(F, P, N, prf ) and cred(F, P, N, grd)=skept(F, P, N, grd)=skept(F, P, N, com). 4 Complexity Considering the computational complexity of optimal status enforcement, we focus on the following decision problems. Given an AF F = (A, R), two disjoint sets P, N A, a semantics σ, and an integer k 0, the question is to decide whether there is an R0 2 cred(F, P, N, σ) (resp. R0 2 skept(F, P, N, σ)) s.t. F 0 = (A, R0) and |R R0| k, i.e., whether there is an enforcing AF with at most k modifications to the attack structure. We distinguish between the general status enforcement problem and the restricted case where N = ;, i.e., without negative status to be enforced. Table 1 summarizes our results. We begin with status enforcement for conflict-free sets, which corresponds simply to addition or removal of selfattacks on the given sets of arguments. Proposition 7. Optimal credulous status enforcement for conflict-free sets is polynomial-time solvable. Skeptical status enforcement for conflict-free and admissible sets is trivial, since the empty set is always conflict-free and admissible (see also Proposition 4). Credulous and skeptical status enforcement coincides under grounded semantics, which in turn coincides with nonstrict extension enforcement under grounded semantics if N = ; (Proposition 1). For complexity of status enforcement under grounded semantics, the following result is a corollary of a previously established NP-completeness result for extension enforcement [Wallner et al., 2016, Theorem 3]. Corollary 8. Credulous and skeptical status enforcement under grounded semantics is NP-complete, even if N = ;. As a further corollary, skeptical status enforcement under complete semantics is NP-complete (see Proposition 6). Corollary 9. Skeptical status enforcement under complete semantics is NP-complete, even if N = ;. For credulous status enforcement, it turns out that for the remaining semantics the complexities of the general case and the restricted case with N = ; are presumably different. Intuitively, hardness for the restricted case follows from the fact that checking whether an argument is credulously accepted without modifications is NP-hard for these semantics. Proposition 10. Credulous status enforcement with N = ; is NP-complete under admissible, complete, stable, and preferred semantics. Proof. (sketch) Let F = (A, R) be an AF and P A. Membership follows from guessing a new AF F 0, for each argu- Table 1: Complexity results for status enforcement. N = ; N unrestricted σ credulous skeptical credulous skeptical Conflict-free in P trivial in P trivial Admissible NP-c trivial P 2 -c trivial Stable NP-c P 2 -c Complete NP-c NP-c P 2 -c NP-c Grounded NP-c NP-c NP-c NP-c Preferred NP-c in P ment p 2 P a set of arguments Ep with p 2 Ep, and checking whether each guessed set Ep is a σ-extension. Verifying whether a set is a σ-extension can be checked in polynomial time for all considered semantics except preferred semantics, for which it suffices to check whether the set is admissible. Hardness follows in all cases from a straightforward reduction from the static credulous acceptance problem for an argument a (an NP-complete problem for all considered semantics [Dimopoulos and Torres, 1996]), and constructing an instance for credulous status enforcement with P = {a}, and allowing zero modifications (k = 0). In contrast, credulous status enforcement under stable, admissible, complete, and preferred semantics is P 2 -complete if N 6= ;. Intuitively, the jump in complexity is due to co NPcompleteness of verifying that an argument is not credulously accepted in a given AF. Thus the problem can be decided by a non-deterministic guess of a new attack structure and verifying that all negative statuses are credulously enforced. Theorem 11. Credulous status enforcement under stable, admissible, complete, and preferred semantics is P 2 -complete. Complexity of skeptical status enforcement under stable semantics is established similarly as for credulous status enforcement under that semantics. Here second-level hardness comes from the fact that verifying skeptical acceptance in a fixed AF is co NP-complete under stable semantics. Corollary 12. Skeptical status enforcement under stable semantics is P 2 -complete, even if N = ;. For skeptical status enforcement under preferred semantics we show membership in P 3 , which is due to the fact that checking skeptical acceptance in a fixed AF under preferred semantics is P 2 -complete [Dunne and Bench-Capon, 2002]. Proposition 13. Enforcing skeptical acceptance under preferred semantics is in P 5 Algorithms We present declarative encodings of optimal status enforcement for NP variants of the problem, and, based on the encodings, develop counterexample-guided abstraction refinement (CEGAR) [Clarke et al., 2003] algorithms based on maximum satisfiability (Max SAT) and SAT solvers for optimally solving P 2 complete variants of status enforcement. In detail, we provide Max SAT encodings for N = ; under admissible and stable semantics, and CEGAR for P 2 credulous status enforcement for arbitrary N under admissible and stable, as well as skeptical status enforcement under stable semantics. This covers all the non-trivial problem variants considered (except for grounded) by Proposition 6. For background on Max SAT, recall that for a Boolean variable x, there are two literals, x and x. A clause is a disjunction (_) of literals. A truth assignment is a function from variables to true (1) and false (0). Satisfaction is defined as usual. A Partial Max SAT (or simply Max SAT) instance consists of hard clauses 'h and soft clauses 's. An assignment is a solution to a Max SAT instance ('h, 's) if satisfies 'h. The cost of , c( ), is the number of clauses in 's not satisfied by . A solution to a Max SAT instance ' is optimal if c( ) c( 0) for any solution 0 to '. Let F = (A, R) be an AF, and P, N A disjoint sets of arguments whose statuses are to be enforced under a semantics σ. To encode the credulous status enforcement problem in Max SAT, we define variables xp a for each a 2 A and p 2 P and ra,b for each a, b 2 A. Now (xp a) = 1 corresponds to a 2 Ep, where Ep is any σ-extension containing the enforced argument p. Likewise, (ra,b) = 1 iff (a, b) 2 R0, where R0 is a solution attack structure. For skeptical status enforcement, instead of variables xp a, we define variables xn a for each a 2 A and n 2 N as indicators for a 2 En, where En is any σ-extension that does not include the argument n. For both credulous and skeptical status enforcement, the soft clauses encode modifications to the attack structure by 's = V a,b2A a,b, where ra,b if (a, b) 2 R, ra,b if (a, b) 62 R. For credulous status enforcement, the hard clauses are (cred, F, P, N, σ) = σ(F) encodes semantics σ so that the xp a variables correspond to Ep 2 σ(F 0) with F 0 = (A, R0) and R0 defined via the attack variables ra,b. For conflict-freeness, we have , for admissible sets we use formula 'p adm(F) defined as and for stable semantics stb(F) = 'p If N = ;, each satisfying assignment to (cred, F, P, ;, σ) corresponds to an R0 2 cred(F, P, ;, σ) and vice versa, for σ 2 {adm, com, prf , stb}. Note that the encodings allow for capturing several refinements of the problem. For example, refinements of the optimality criterion, e.g., more elaborate cost models for expressing relative strength of, or confidence in, attacks can be accounted for by using non-unit weights on the soft clauses; similarly, hard constraints on changes to the attack structure can be enforced by making the corresponding soft clauses hard. Also, enforcing the existence of σ-extensions attacking certain arguments is possible. Furthermore, e.g., a bounded number of additional arguments can also be allowed. For N 6= ;, due to second-level hardness, we propose a CEGAR approach described as Algorithm 1 which relies on iterative (Max)SAT calls to solve status enforcement optimally. We first apply Max SAT to (cred, F, P, N, σ) to generate a candidate solution (Line 3), which optimally solves the subproblem of enforcing each argument in P to be accepted credulously, at the same time enforcing that each generated witness extension does not include arguments in N. We then check whether this candidate is also a solution for the status enforcement problem by asking whether in the modified AF there exists a σ-extension containing some n 2 N via Algorithm 1 CEGAR-based status enforcement for AF F = (A, R), P, N A, σ 2 {adm, stb}, M 2 {cred, skept} 1: χ (M, F, P, N, σ) 2: while true do 3: (c, ) MAXSAT(χ, 's) 4: result SAT(CHECK(M, A, , P, N, σ)) 5: if result = unsatisfiable then return (c, ) 6: else χ χ REFINE( ) a SAT-check in Line 4. If no such σ-extension exists, represents an optimal solution to the credulous status enforcement instance. Otherwise we refine the initial formula by excluding the current candidate attack structure and ask for another modification to the AF. For checking whether there is a σ-extension containing an n 2 N in the AF F 0 = (A, R0), with R0 defined via truth assignment , we use formulas CHECK(cred, A, , P, N, σ) = φσ(A, ) W n2N xn. Formula φσ(A, ) encodes credulous acceptance in the static case with φcf (A, ) = V (ra,b)=1( xa _ xb) for conflict-free sets. Here, variables xa for a 2 A encode that a is in the σ-extension. For admissible sets and stable extensions we define φadm(A, ) = φcf (A, ) φstb(A, ) = φcf (A, ) If a candidate is not successfully verified, we refine formula χ of Algorithm 1 with REFINE( ) = For skeptical status enforcement under stable semantics we slightly adapt Algorithm 1 by using (skept, F, P, N, σ) = CHECK(skept, A, , P, N, stb) = φstb(A, ) W p2P xp. For the special case N = ;, we enforce a stable extension containing P via . 6 Experiments We have implemented the Max SAT encodings and the CEGAR-procedures, obtaining the first system for optimal status enforcement. Here we present an overview of an empirical evaluation of the system. We generated benchmark instances following essentially a standard model for random directed graphs.1 For each |A| 2 {20, 40, . . . , 200} and p 2 {0.05, 0.1, . . . , 0.35}2, we 1Based on an initial evaluation, the ICCMA 15 argumentation system competition [Thimm et al., 2016] instances are currently too large in terms of the number of arguments to be suitable as basis for status enforcement benchmarks. 2Non-trivial instances arose mainly with p 0.35. number of arguments mean cpu time (incl. timeouts) 20 40 60 80 100 120 140 160 180 200 0 100 200 300 400 500 600 700 800 900 5,0 4,0 3,0 2,0 1,0 number of arguments mean cpu time (incl. timeouts) 20 40 60 80 100 120 140 160 180 200 0 100 200 300 400 500 600 700 800 900 1,0 skept 2,0 skept 5,0 skept 1,5 skept 2,2 skept 5,1 skept 1,5 cred 2,2 cred 5,1 cred Figure 2: Credulous admissible (N = ;) (left), CEGAR on credulous (N 6= ;) and skeptical stable (right). generated ten random AFs with |A| arguments by including individual attacks with probability p. For each AF, we randomly picked 5 arguments, of which we enforced |P| 2 {1, 2, . . . , 5} positively, and finally picked |N| 2 {0, 1, 2, 5} arguments from the set A \ P to be enforced negatively. We used Open WBO [Martins et al., 2014] as the Max SAT solver, and ran the experiments on 2.83-GHz Intel Xeon E5440 4core nodes with 32-GB RAM and Debian GNU/Linux 8 under 900-second per-instance timeout. We provide results for two central AF semantics, admissible and stable, for both credulous and skeptical variants of optimal status enforcement. Mean runtimes with timeouts included as 900s are shown in Figure 2 for the NP problems of credulous status enforcement with |N| under admissible semantics (left) and for the P 2 skeptical and credulous status enforcement problems under stable semantics (right). In summary, the procedures generally scale up to at least 100 arguments. As expected, increasing the size of P makes the problem harder (left); with |P| = 2, the approach still scales to 200 arguments and beyond. For the harder case |P| = 5, most (65/70) instances are solved at |A| = 80, after which timeouts start increasing linearly, with 68/70 timeouts at |A| = 200. For the CEGAR approach (right), credulous status enforcement is easier than skeptical under stable semantics. Interestingly, the empirical hardness of skeptical status enforcement under stable semantics is not significantly affected by different choices for size of P and N. 7 Related Work A majority of argumentation system implementations for AFs [Cerutti et al., 2014; Dvoˇrák et al., 2014; Egly et al., 2010; Nofal et al., 2014] focus on the static problems of skeptical and credulous acceptance under different semantics; the ICCMA 15 argumentation system competition [Thimm et al., 2016] also focused on these problems. Status enforcement, as focused on in this work, adopts the notions of skeptical and credulous acceptance into a dynamic setting. There is recent work focusing on different revision operators for AFs [Baumann, 2012a; Baumann and Brewka, 2015; Bisquert et al., 2013; Booth et al., 2013; Coste-Marquis et al., 2014a; 2014b; Delobelle et al., 2015; Diller et al., 2015; Liao et al., 2011]. Operators giving rise to computational problems concerning dynamics of AFs can be categorized into ones based on semantical [Booth et al., 2013; Coste-Marquis et al., 2014a; 2014b; Diller et al., 2015] and structural [Baumann, 2012b; Delobelle et al., 2015; Coste-Marquis et al., 2015; Wallner et al., 2016] notions of distance between AFs. Status enforcement falls into the structural distance category. As for the problem statement of optimal status enforcement, [Doutre et al., 2014; Kontarinis et al., 2013] suggest a similar problem setting (though in the latter in terms of subset-minimal instead of optimal structural changes). However, no algorithms for optimal status enforcement are proposed. Only few systems exist for enforcement problems; for extension enforcement, two have been recently proposed [Coste-Marquis et al., 2015; Wallner et al., 2016]. The closest to this work is [Wallner et al., 2016], with CEGAR-style algorithms for second-level extension enforcement problems. 8 Conclusions We presented properties, complexity analysis, and algorithms for optimal status enforcement as a form of AF dynamics in abstract argumentation. Complexity of optimal status enforcement ranges from polytime-solvable to (at least) completeness for the second level of the polynomial hierarchy. We also proposed and evaluated a first prototype system for optimal status enforcement via employing Max SAT solvers. Acknowledgments This work has been funded by Academy of Finland under grants 251170 COIN, 276412, and 284591. References [Amgoud and Prade, 2009] L. Amgoud and H. Prade. Using arguments for making and explaining decisions. Artificial Intelligence, 173(3-4):413 436, 2009. [Baroni et al., 2011] P. Baroni, M. Caminada, and M. Gi- acomin. An introduction to argumentation semantics. Knowledge Engineering Review, 26(4):365 410, 2011. [Baumann and Brewka, 2015] R. Baumann and G. Brewka. AGM meets abstract argumentation: Expansion and revision for Dung frameworks. In Proc. IJCAI, pages 2734 2740. AAAI Press, 2015. [Baumann, 2012a] R. Baumann. Normal and strong expan- sion equivalence for argumentation frameworks. Artificial Intelligence, 193:18 44, 2012. [Baumann, 2012b] R. Baumann. What does it take to enforce an argument? Minimal change in abstract argumentation. In Proc. ECAI, volume 242 of FAIA, pages 127 132, 2012. [Bench-Capon and Dunne, 2007] T.J.M. Bench-Capon and P.E. Dunne. Argumentation in artificial intelligence. Artificial Intelligence, 171(10-15):619 641, 2007. [Bench-Capon et al., 2009] T.J.M. Bench-Capon, H. Prakken, and G. Sartor. Argumentation in legal reasoning. In Argumentation in Artificial Intelligence, pages 363 382. Springer, 2009. [Bisquert et al., 2013] P. Bisquert, C. Cayrol, F. Dupin de Saint-Cyr, and M. Lagasquie-Schiex. Enforcement in argumentation is a kind of update. In Proc. SUM, volume 8078 of LNCS, pages 30 43. Springer, 2013. [Booth et al., 2013] R. Booth, S. Kaci, T. Rienstra, and L. W. N. van der Torre. A logical theory about dynamics in abstract argumentation. In Proc. SUM, volume 8078 of LNCS, pages 148 161. Springer, 2013. [Cerutti et al., 2014] F. Cerutti, M. Giacomin, M. Vallati, and M. Zanella. An SCC recursive meta-algorithm for computing preferred labellings in abstract argumentation. In Proc. KR, pages 42 51. AAAI Press, 2014. [Clarke et al., 2003] E.M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement for symbolic model checking. Journal of the ACM, 50(5):752 794, 2003. [Coste-Marquis et al., 2014a] S. Coste-Marquis, S. Konieczny, J. Mailly, and P. Marquis. On the revision of argumentation systems: Minimal change of arguments statuses. In Proc. KR, pages 52 61. AAAI Press, 2014. [Coste-Marquis et al., 2014b] S. Coste-Marquis, S. Konieczny, J. Mailly, and P. Marquis. A translationbased approach for revision of argumentation frameworks. In Proc. JELIA, volume 8761 of LNCS, pages 397 411. Springer, 2014. [Coste-Marquis et al., 2015] S. Coste-Marquis, S. Konieczny, J. Mailly, and P. Marquis. Extension enforcement in abstract argumentation as an optimization problem. In Proc. IJCAI, pages 2876 2882. AAAI Press, 2015. [Delobelle et al., 2015] J. Delobelle, S. Konieczny, and S. Vesic. On the aggregation of argumentation frameworks. In Proc. IJCAI, pages 2911 2917. AAAI Press, 2015. [Diller et al., 2015] M. Diller, A. Haret, T. Linsbichler, S. Rümmele, and S. Woltran. An extension-based approach to belief revision in abstract argumentation. In Proc. IJCAI, pages 2926 2932. AAAI Press, 2015. [Dimopoulos and Torres, 1996] Y. Dimopoulos and A. Tor- res. Graph theoretical structures in logic programs and default theories. Theoretical Computer Science, 170(12):209 244, 1996. [Doutre et al., 2014] S. Doutre, A. Herzig, and L. Perrussel. A dynamic logic framework for abstract argumentation. In Proc. KR, pages 62 71. AAAI Press, 2014. [Dung, 1995] P.M. Dung. On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games. Artificial Intelligence, 77(2):321 358, 1995. [Dunne and Bench-Capon, 2002] P.E. Dunne and T.J.M. Bench-Capon. Coherence in finite argument systems. Artificial Intelligence, 141(1/2):187 203, 2002. [Dvoˇrák et al., 2014] W. Dvoˇrák, M. Järvisalo, J.P. Wallner, and S. Woltran. Complexity-sensitive decision procedures for abstract argumentation. Artificial Intelligence, 206:53 78, 2014. [Egly et al., 2010] U. Egly, S.A. Gaggl, and S. Woltran. Answer-set programming encodings for argumentation frameworks. Argument & Computation, 1(2):147 177, 2010. [Kontarinis et al., 2013] D. Kontarinis, E. Bonzon, N. Maudet, A. Perotti, L. van der Torre, and S. Villata. Rewriting rules for the computation of goal-oriented changes in an argumentation system. In Proc. CLIMA, volume 8143 of LNCS, pages 51 68. Springer, 2013. [Liao et al., 2011] B.S. Liao, L. Jin, and R. C. Koons. Dynamics of argumentation systems: a division-based method. Artificial Intelligence, 175(11):1790 1814, 2011. [Martins et al., 2014] R. Martins, V.M. Manquinho, and I. Lynce. Open-WBO: A modular Max SAT solver. In Proc. SAT, volume 8561 of LNCS, pages 438 445, 2014. [Mc Burney et al., 2012] P. Mc Burney, S. Parsons, and I. Rahwan, editors. Arg MAS 2011 Revised Selected Papers, volume 7543 of LNCS. Springer, 2012. [Nofal et al., 2014] S. Nofal, K. Atkinson, and P. E. Dunne. Algorithms for decision problems in argument systems under preferred semantics. Artificial Intelligence, 207:23 51, 2014. [Thimm et al., 2016] M. Thimm, S. Villata, F. Cerutti, N. Oren, H. Strass, and M. Vallati. Summary report of the first international competition on computational models of argumentation. AI Magazine, 37(1):102 104, 2016. [Wallner et al., 2016] J.P. Wallner, A. Niskanen, and M. Järvisalo. Complexity results and algorithms for extension enforcement in abstract argumentation. In Proc. AAAI. AAAI Press, 2016.