# controllability_of_control_argumentation_frameworks__a3541a57.pdf

Controllability of Control Argumentation Frameworks

Andreas Niskanen1 , Daniel Neugebauer2 and Matti J arvisalo1

1HIIT, Department of Computer Science, University of Helsinki, Finland 2Institut f ur Informatik, Heinrich-Heine Universit at D usseldorf, Germany

Control argumentation frameworks (CAFs) allow for modeling uncertainties inherent in various argumentative settings. We establish a complete computational complexity map of the central computational problem of controllability in CAFs for five key semantics. We also develop Boolean satisfiability based counterexample-guided abstraction refinement algorithms and direct encodings of controllability as quantified Boolean formulas, and empirically evaluate their scalability on a range of NPhard variants of controllability.

1 Introduction

Argumentation is a vibrant area of artificial intelligence research. Various argumentative settings intrinsically involve uncertainties about the existence and relationships between arguments due to different forms of dynamics underlying argumentation [Doutre and Mailly, 2018]. Extending the central formal model of Dung s abstract argumentation frameworks (AFs) [Dung, 1995] to such settings, control argumentation frameworks (CAFs) [Dimopoulos et al., 2018] were recently proposed as a unifying framework to capture uncertainties about the existence of arguments and attacks between arguments. Syntactically, CAFs generalize AFs by allowing for specifying control, uncertain, and fixed arguments, which give rise to uncertainties about the attack relation. CAFs have already proved to be a natural way to approaching argumentation-based negotiation in settings where knowledge of the opponent s profile is incomplete [Dimopoulos et al., 2019] as a suitable formalism for opponent modeling, i.e., modeling uncertainties about an opponent profile. Lifting the well-studied acceptance problems in AFs, controllability is an analogous central computational problem in CAFs. Reminiscent of particular computational problems in the study of argumentation dynamics [Coste-Marquis et al., 2007; Cayrol et al., 2010; Booth et al., 2013; Coste-Marquis et al., 2014; Doutre et al., 2014; de Saint-Cyr et al., 2016; Diller et al., 2018], in particular non-strict extension enforcement under normal expansions [Baumann and Brewka, 2010; Baumann, 2012; Coste-Marquis et al., 2015], credulous controllability of a set T of arguments refers to being able to

use the control arguments of a CAF to ensure that T is contained in some extension of every AF (completion) resulting from instantiating the uncertain part of the CAF. Analogously, skeptical controllability asks if T can be ensured to be contained in all extensions of every completion of the CAF. Unlike for acceptance [Dvor ak and Dunne, 2018] and extension enforcement [Wallner et al., 2017] in AFs, the complexity of variants of controllability in CAFs under central argumentation semantics has not been established, apart from (bounds for) specific semantics [Dimopoulos et al., 2018]. Furthermore, while controllability in CAFs has already been harnessed computationally for argumentation-based negotiation [Dimopoulos et al., 2019], there is significant room for developing computational approaches to controllability and evaluating the empirical hardness of controllability. In this paper, we establish a complete complexity map of skeptical and credulous controllability under several central argumentation semantics for both general CAFs and so-called simplified CAFs. In particular, we establish tight connections between controllability in CAFs and acceptance in incomplete argumentation frameworks (IAFs) [Baumeister et al., 2018b], and apply these observations to obtain tight complexity results for CAFs via generalizing recent results for acceptance in IAFs [Baumeister et al., 2018a]. On the algorithmic side, we present both direct quantified Boolean satisfiability (QBF) encodings improving on [Dimopoulos et al., 2018] in terms of compactness of the encodings and Boolean satisfiability (SAT) based counterexample-guided abstraction refinement procedures for controllability, and provide first results on the empirical hardness of reasoning about controllability with the approaches.

2 Argumentation Frameworks

We recall standard argumentation frameworks [Dung, 1995] and standard AF semantics [Baroni et al., 2018], incomplete AFs [Baumeister et al., 2018b] as useful for our results, and control AFs [Dimopoulos et al., 2018] which we focus on.

Definition 1. An argumentation framework (AF) is a pair F = (A, R) with a non-empty finite set of arguments A and an attack relation R A A. An argument a A is defended by a set S A iff for each (b, a) R there is a c S with (c, b) R. The characteristic function of F for a set S A is FF (S) = {a A | a is defended by S}. The range

Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence (IJCAI-20)

of S is S+ F = S {a A | (b, a) R, b S}.

Semantics σ map each AF to a collection of (jointly accepted) subsets of arguments. We consider the admissible (adm), complete (com), preferred (prf ), stable (stb), and grounded (grd) semantics.

Definition 2. Let F = (A, R) be an AF. A set S A is conflict-free in F, denoted by S cf (F), if there are no x, y S with (x, y) R. For S cf (F), it holds that

S adm(F) if S FF (S), S com(F) if S = FF (S), S prf (F) if S is a subset-maximal admissible set,

S stb(F) if S+ F = A, and S grd(F) if S is the subset-minimal complete set.

If S σ(F) for a semantics σ, we call S a σ-extension. An argument a A is skeptically accepted if a T σ(F), and credulously accepted if a S σ(F).

Incomplete argumentation frameworks [Baumeister et al., 2018b; Baumeister et al., 2018a] allow for representing unquantified uncertainty in an AF via uncertain arguments and attacks. We denote the restriction of an attack relation R to a set of arguments A by R|A = R (A A ).

Definition 3. An incomplete argumentation framework (IAF) is a tuple I = (A, A?, R, R?), where R, R? (A A?) (A A?) with A A? = and R R? = . The set A? consists of uncertain arguments and the set R? of uncertain attacks. An IAF is (purely) argument-incomplete if R? = . A completion of I is an AF F = (A , R ) with A A (A A?) and R|A R (R R?)|A . An argument a A is possibly skeptically (credulously) accepted in I if it is skeptically (credulously) accepted in a completion of I; and necessarily skeptically (credulously) accepted in I if it is skeptically (credulously) accepted in all completions of I.

A control argumentation framework [Dimopoulos et al., 2018] consists of three parts: the fixed, the uncertain, and the control part. Control AFs allow for modeling the problem of finding a subset of the control part such that no matter what the state of the uncertain part, a certain target is reached.

Definition 4. A control argumentation framework (CAF) is a triple C = (F, C, U), where

F = (AF , RF ) is the fixed part with RF (AF AU) (AF AU),

U = (AU, RU R U ) is the uncertain part with RU, R U (AF AU) (AF AU), where R U is symmetric and irreflexive,

C = (AC, RC) is the control part with RC (AC (AF AU AC)) ((AF AU AC) AC),

AF , AU, and AC are pairwise disjoint sets of arguments, and RF , RU, R U and RC are pairwise disjoint sets of attacks. A subset Aconf AC is a control configuration. A completion of CAF C is an AF F = (A , R ) with A = AF AC A U, where A U AU and (RF RC)|A R (RF RC RU R U )|A satisfying (a, b) R or (b, a) R for all (a, b) R U .

Figure 1: An example CAF (F, C, U) with AF ={a, b, c}, AC={d}, AU={e}, RF ={(b, a), (c, b)}, RC={(d, c), (d, e)}, RU={(a, c)}, and R U ={(b, e), (e, b)}.

Note that we assume symmetry and irreflexitivity to R U without loss of generality. We focus on the controllability problem over control AFs, which asks to decide if there is a control configuration such that for all completions of the control AF, a subset of arguments is credulously or skeptically accepted. Definition 5. Let C = (F, C, U), T AF , and let σ be an AF semantics. The CAF C is skeptically (credulously) controllable wrt. T and σ if, for some control configuration Aconf AC, T is included in every (some) σ-extension of every completion of Cconf = (F, Cconf, U), where Cconf = (Aconf, RC|AF AU Aconf). The CAF in Figure 1 is not credulously controllable w.r.t. {a} for any of the five semantics σ we consider, since no matter whether the control argument d is included, there are completions that do not have a in any σ-extension. The CAF is, however, skeptically controllable w.r.t. {a} under stb using Aconf = since each completion either has a unique stable extension containing a or no stable extension at all.

3 Complexity of Controllability We establish tight complexity results for credulous and skeptical controllability as summarized in Table 1. We assume knowledge of the complexity classes in the polynomial hierarchy (ΣP 0=ΠP 0=P, ΣP i+1=NPΣP i , and ΠP i+1=co NPΣP i ) and the notions of hardness and completeness [Arora and Barak, 2009]. We start from simplified CAFs [Dimopoulos et al., 2018], which are CAFs with no uncertain part, i.e., AU = RU = R U = , denoted by (F, C, ). First, we establish that the restriction of the controllability problem in simplified CAFs to singleton target sets (called the conclusion problem) is equivalent to possible acceptance in argument-incomplete IAFs. Control arguments in such CAFs directly correspond to the IAFs uncertain arguments, so that both notions of completion (and all derived problems) coincide. Lemma 1. Given an IAF I = (A, A?, R, ), argument q A, and semantics σ, q is possibly skeptically (credulously) accepted under σ iff the CAF C = (F, C, ), where AF = A, AC = A?, RF = R|A and RC = R \ (R|A), is skeptically (credulously) controllable with respect to {q} and σ. This yields hardness of credulous controllability for simplified CAFs via a reduction from possible credulous acceptance in argument-incomplete IAFs. We extend the earlier NPcompleteness result for controllability under stb [Dimopoulos et al., 2018] to all five semantics that we consider here. Theorem 2. Credulous controllability for simplified CAFs is NP-complete under σ {adm, com, prf , stb, grd}.

Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence (IJCAI-20)

General CAFs Simplified CAFs Semantics Credulous Skeptical Credulous Skeptical admissible ΣP 3-c trivial NP-c trivial complete ΣP 3-c ΣP 2-c NP-c NP-c preferred ΣP 3-c ΣP 3-c NP-c ΣP 3-c stable ΣP 3-c ΣP 2-c NP-c ΣP 2-c grounded ΣP 2-c ΣP 2-c NP-c NP-c

Table 1: Computational complexity of controllability

Proof. Let C = (F, C, ) be a simplified CAF and T AF be a set of target arguments. NP-membership is by nondeterministically guessing a control configuration Aconf AC and a σ-extension E of the AF (AF Aconf, (RF RC)|AF Aconf), and checking in polynomial time if T E and E is a σextension, with the exception of prf ; here, however, it suffices to check admissibility instead of preferredness of E as every admissible set is a subset of some preferred extension. Hardness follows from Lemma 1 by reduction from possible credulous acceptance under σ in argument-incomplete IAFs, which is NP-complete [Baumeister et al., 2018a].

For AFs, credulous acceptance under grd coincides with skeptical acceptance under both grd and com. Thus skeptical controllability under grd and com are equivalent to credulous controllability under grd. This yields NP-completeness also for skeptical controllability in simplified CAFs. Corollary 3. The skeptical controllability problem for simplified CAFs is NP-complete under σ {com, grd}. For skeptical controllability under stb, we derive ΣP 2completeness, strengthening the NP-hardness result of [Dimopoulos et al., 2018]. Theorem 4. Skeptical controllability for simplified CAFs is ΣP 2-complete under stb. Proof. (Sketch.) As possible skeptical acceptance in argument-incomplete IAFs is ΣP 2-complete under stb [Baumeister et al., 2018a], a reduction by Lemma 1 establishes ΣP 2-hardness for skeptical controllability under stb. For membership, guess a control configuration and use an NP-oracle to check whether every argument in T is skeptically accepted under stb [Dimopoulos and Torres, 1996].

Similarly, as skeptical acceptance in AFs under prf is ΠP 2-complete [Dunne and Bench-Capon, 2002] and possible skeptical acceptance in argument-incomplete IAFs under prf is ΣP 3-complete [Baumeister et al., 2018a], we have ΣP 3completeness of skeptical controllability in simplified CAFs under prf via an analogous proof. Theorem 5. Skeptical controllability for simplified CAFs is ΣP 3-complete under prf . Finally, we note that skeptical acceptance for adm is trivial, since the empty set is always admissible, so no argument can ever be in all adm sets. We turn to skeptical controllability for general CAFs. We establish ΣP 2-completeness of skeptical controllability for general CAFs under stb, strengthening the membership result of [Dimopoulos et al., 2018].

Theorem 6. Skeptical controllability for general CAFs is ΣP 2-complete under stb.

Proof. Let (F, C, U) be a CAF and T AF a target. ΣP 2membership follows from the quantifier representation of the problem: Is there a control configuration such that, for all completions F = (A , R ) and for all sets of arguments S A with T S, it holds that S stb(F )? Each of the quantifiers is polynomial-length-bounded and the condition S stb(F ) is in P. Note that this representation checks whether every set S not containing T is not stable, instead of checking whether every stable extension contains T, which is clearly equivalent. Hardness follows from hardness in simplified CAFs.

Similarly, for prf we establish ΣP 3-completeness.

Theorem 7. Skeptical controllability for general CAFs is ΣP 3-complete under prf .

Proof. Let (F, C, U) be a CAF and T AF a target. ΣP 3membership follows from the quantifier representation of the problem: Is there a control configuration such that, for all completions F = (A , R ) and for all sets of arguments S A with T S, it holds that S adm(F ) or there exists a set S S with S adm(F )? Each of the quantifiers is polynomial-length-bounded and the conditions S adm(F ) and S adm(F ) are in P. Hardness follows from hardness in simplified CAFs.

Skeptical controllability under com and grd coincides with credulous controllability under grd. Hence it suffices to consider credulous controllability among the three. We make use of earlier proofs of hardness in the context of IAFs [Baumeister et al., 2018a]. Intuitively, we modify the general reduction from QSAT to IAFs [Baumeister et al., 2018a, Definition 9] by incorporating the control part of CAFs to simulate a partial truth assignment, similarly as uncertain arguments of IAFs are used to simulate an assignment in the reduction to IAFs. This gives a reduction from X Y Z-CNF-SAT to CAFs. As in [Baumeister et al., 2018a], we observe a crucial connection between the total assignments over the CNF formula and the σ-extensions of the completions of the corresponding CAF under σ {adm, com, prf , stb}: a truth assignment satisfies the formula iff there is a completion with a σ-extension containing a particular query argument. This reduction (see Figure 2) yields ΣP 3-completeness of credulous controllability in general CAFs under σ {adm, com, prf , stb}. Thus we close the gap from [Dimopoulos et al., 2018] between ΣP 3membership and ΣP 2-hardness under stb.

Theorem 8. Credulous controllability for general CAFs is ΣP 3-complete under σ {adm, com, prf , stb}.

Proof. (Sketch.) Let (F, C, U) be a CAF and T AF a target. ΣP 3-membership is by the quantifier representation: Is there a control configuration s.t. for all completions F = (A , R ) there is a set T E A such that E σ(F )? Each of the quantifiers is polynomial-length-bounded and the condition E σ(F ) is in P for all considered semantics except prf , which we can again exchange for adm. Hardness follows by a reduction illustrated in Figure 2.

Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence (IJCAI-20)

Figure 2: CAF created by the reduction of Theorem 8 for the CNF formula ϕ = c1 c2 with clauses c1=x1 z1 and c2=z1 y1. We have AU={g1}, AC={conf1}, RC={(conf1, x1)}, and all other arguments and attacks are in F. There is a control configuration for (F, C, U) such that for all completions, {ϕ} is a subset of some σ-extension iff ( τ{x1})( τ{y1})( τ{z1})[c1 c2]=true. For Theorem 9, we have Z= , and there is a control configuration for (F, C, U) such that for all completions, { ϕ} is a subset of the grounded extension iff ( τ{x1})( τ{y1})[c1 c2]=false.

The same reduction for Z = gives a reduction from X Y -CNF-SAT to credulous controllability under grd for CAFs. As in simplified CAFs, this problem coincides with skeptical controllability under both grd and com. Similarly to [Baumeister et al., 2018a], we prove hardness using an equivalence between completions of the CAF containing a particular query argument in the grounded extension and satisfying total truth assignments to the input formula.

Theorem 9. For general CAFs, credulous controllability under grd and skeptical controllability under σ {com, grd} are ΣP 2-complete.

Proof. (Sketch.) Let (F, C, U) be a CAF and T AF a target. ΣP 2-membership is derived from the quantifier representation: Is there a control configuration such that, for all completions F = (A , R ), T G holds (where G grd(F ) is the grounded extension of F )? Each of the quantifiers is polynomial-length-bounded and the condition T G with G grd(F ) is in P. Hardness follows by a reduction as illustrated in Figure 2.

4 Controllability as QBFs

We present QBF encodings of controllability covering the considered problem variants (except for skeptical controllability under prf , the encoding of which is presumably more complicated). Our encodings are more compact than those presented in [Dimopoulos et al., 2018]. Consider controllability of a CAF C = (F, C, U) w.r.t. a target set T AF under semantics σ {adm, com, stb}. Let A = AF AU AC and R = RF RU R U RC. We declare Boolean variables xa and ya for each a A, and ra,b for each (a, b) R, with the interpretations that for a model τ, τ(ya) = 1 iff a Aτ, τ(ra,b) = 1 iff (a, b) Rτ, and τ(xa) = 1 iff a E σ(F τ), where F τ = (Aτ, Rτ) is a completion of C under the control configuration Aτ conf = {a AC | τ(ya) = 1}. As a basis of the QBF encodings (as well as the CEGAR approach described in the next section), we capture semantics by conditioning standard SAT encodings of AF semantics [Besnard and Doutre, 2004] on the uncertain parts of a given CAF, similarly as for IAFs in [Niskanen et al., 2020].

We encode completions with ϕ?(C) = V

(a,b) RF RC ra,b V

a AU AC ya xa V

(a,b) RU R U ra,b V

(b,a) RU R U rb,a V

(a,b) R U (ya yb) (ra,b rb,a) . The formulas ϕcf (C) = V

(a,b) R(ea,b ( xa xb)), ϕadm(C) = ϕcf (C) V

(b,a) R(xa (eb,a zb)), ϕcom(C) = ϕadm(C) V

(b,a) R((eb,a zb) xa), and ϕstb(C) = ϕcf (C) V

a A(ya (xa za)) capture the semantics σ {adm, com, stb} of the completions, where za = W (b,a) R(xb yb rb,a) for a A and ea,b = ya yb ra,b for (a, b) R. In particular, ϕ?(C) ϕσ(C) V t T xt is satisfiable iff there is a control configuration Aconf AC, a completion of C, and a σ-extension of the completion containing all arguments in T. Now, first consider skeptical controllability under σ {com, stb}. Let X = {ya | a AC} and Y = {ya | a AU} {ra,b | (a, b) RU R U } {xa, za | a AF AU AC}. We have that

X Y ϕσ(C) _

is false iff C is skeptically controllable w.r.t. T under σ. In particular, this is the negation of the QBF in [Dimopoulos et al., 2018], and circumvents the issue of incompatible assignments to universally quantified variables, such as ya yb ra,b rb,a for some (a, b) R U , in the encoding of [Dimopoulos et al., 2018]. Our encoding is also more compact, as we do not have to encode ϕσ(C) in CNF, which would require as many auxiliary variables as there are clauses in ϕσ(C) using a standard translation. For credulous controllability under σ {adm, stb}, we use an auxiliary variable ξ interpreted as τ(ξ) = 1 iff τ does not correspond to a valid completion, encoded as ϕ (C) = W (a,b) RU R U ( ya ra,b) W (a,b) R U (ya yb ra,b rb,a). Let X = {ya | a AC}, Y = {ya | a AU} {ra,b | (a, b) RU R U }, and Z = {xa, za | a AF AU AC} {ξ}. Then the QBF

X Y Z ξ ϕσ(C)

is true iff C is credulously controllable w.r.t. T and σ. If ξ is true quantified existentially after the universal quantifier over the variables representing the completion the corresponding completion must be invalid to satisfy the formula. If ξ is false and the formula is satisfied, the target is reached.

5 Controllability by SAT-Based CEGAR As an alternative to QBFs, we develop SAT-based counterexample-guided abstraction refinement (CEGAR) [Clarke et al., 2003; Clarke et al., 2004] procedures for controllability. The algorithms cover all considered problem variants except skeptical controllability under prf , which can be handled similarly as skeptical controllability under com with an additional subset-maximization procedure. CEGAR works on an NP-abstraction, and iteratively queries a SAT solver for a candidate solution and checks

Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence (IJCAI-20)

Algorithm 1 CEGAR for skeptical controllability Input: CAF C = (F, C, U), target T AF , σ {com, stb}. 1: ϕ ϕσ(C) 2: while true do 3: (result, τ) SAT(ϕ V t T xt) 4: if result = sat then 5: (result, τ) SAT(ϕ ψ(Aτ conf) W t T xt) 6: if result = unsat then return Aτ conf 7: ϕ ϕ REFINECONTROL(Aτ conf) 8: else 9: if σ = stb then return reject 10: while true do 11: (result, τ) SAT(ϕ) 12: if result = unsat then break 13: ϕ ϕ REFINECONTROL(Aτ conf)

14: ϕ ϕ \ ϕstb(C) 15: (result, τ) SAT(ϕ ) 16: if result = sat then return Aτ conf 17: else return reject

for counterexamples to the candidate using the same solver, refining the abstraction until a valid solution is found or all candidates have been ruled out. First consider second-level complete skeptical controllability under σ {com, stb}. As outlined in Algorithm 1, we initialize the abstraction using the SAT encoding ϕσ(C) (line 1). Then, we iteratively solve the abstraction with the additional clauses V t T xt ensuring that T is in a σextension of the completion (line 3). If the abstraction is satisfiable (line 4), we obtain the corresponding control configuration Aτ conf (recall Section 4). Given Aτ conf, we check for a counterexample (line 5) as a completion where one of the target arguments is not in a σ-extension. We encode the control configuration using ψ(Aτ conf) = V a Aτ conf ya V a AC\Aτ conf ya and the counterexample query via W t T xt. If there is no counterexample, we have found a valid control configuration and return (line 6). If we obtain a counterexample a completion F τ and an extension Eτ σ(F τ) with T Eτ we refine the abstraction by adding the clause REFINECONTROL(Aτ conf) = W a ADDARGσ(τ) ya W a REMARGσ(τ) ya (line 7), where ADDARGstb(τ) = {a AC | b Eτ, (b, a) RF } and REMARGstb(τ) = {a AC | a Eτ} characterize arguments whose addition or removal can alter the counterexample extension Eτ = {a A | τ(xa) = 1} under stb [Niskanen et al., 2020]. For complete semantics, we have ADDARGcom(τ) = ADDARGstb(τ), and REMARGcom(τ) = {a AC | a Eτ A \ (Eτ)+ F τ }, that is, for removal we need to also consider removing arguments that are not attacked by Eτ. If there is no solution to the abstraction (line 8), if σ = stb we reject (line 9) since C is then not controllable. The case σ = stb is more delicate as there may be a control configuration for which no completion has a stable extension, making C controllable. Thus we filter out all control configurations admitting a completion with a stable extension (lines 10 13). Finally, we check if there still are control configurations left

Algorithm 2 CEGAR for credulous controllability Input: CAF C = (F, C, U), target T AF , σ {adm, stb}. 1: ϕ ϕσ(C) 2: while true do 3: (result, τ) SAT(ϕ V t T xt) 4: if result = unsat then return reject 5: ϕ ϕ (ψ(Aτ conf) REFINE(F τ)) 6: while true do 7: (result, τ) SAT(ϕ ψ(Aτ conf) W t T xt) 8: if result = sat then 9: (result, τ) SAT(ϕ χ(F τ) V t T xt) 10: if result = unsat then break 11: ϕ ϕ (ψ(Aτ conf) REFINE(F τ)) 12: else 13: if σ = stb then return Aconf 14: while true do 15: (result, τ) SAT(ϕ ψ(Aτ conf)) 16: if result = unsat then break 17: ϕ ϕ (ψ(Aτ conf) REFINE(F τ))

18: ϕ ϕ \ ϕstb(C) 19: (result, τ ) SAT(ϕ ψ(Aτ conf)) 20: if result = unsat return Aτ conf 21: else SAT(ϕ χ(F τ)); break

22: ϕ ϕ REFINECORE(Aτ conf)

(lines 14 15). If there are, we return the corresponding control configuration (line 16), and otherwise reject (line 17). Algorithm 2 for credulous controllability under σ {adm, stb} a third-level complete problem solves the abstraction ϕσ(C) (line 1) iteratively under the constraint V t T xt (line 3). If unsatisfiable, there is no valid control configuration (line 4). Otherwise, we begin the search for a counterexample, i.e., a completion for the current control configuration that has no extension containing the target. The current completion F τ is not such a counterexample, so we refine the abstraction via ψ(Aτ conf) REFINE(F τ) (line 5), where REFINE(F τ) is exactly the so-called strong refinement earlier proposed for IAFs [Niskanen et al., 2020]. We iteratively search for a completion F τ with Eτ σ(F τ) and T Eτ (line 7). If such a candidate counterexample is found (line 8), we check if F τ is a counterexample by checking if there is a further extension containing T (line 9), encoding the completion via χ(F τ) = V a Aτ ya V a A\Aτ ya V (a,b) Rτ ra,b V (a,b) R\Rτ ra,b. If there is no such extension, we have a counterexample to Aτ conf (line 10). Otherwise, we refine the abstraction (line 11). If no counterexample candidate F τ is found (line 12), if σ = stb we return the current Aτ conf (line 13). The case σ = stb is more complex as we need to check if some completion has no stable extension, in which case the target would not be reached. This is checked similarly as in Algorithm 1 (lines 14 21), with the distinctions that SAT calls are performed under the current configuration via ψ(Aconf) (lines 15 and 19) and that the refinement is on completions (line 17). When we exit the inner loop, we have a counterexample F τ

Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence (IJCAI-20)

0.01 1.00 100.00

0.01 1.00 100.00

CAQE running time (s)

CEGAR running time (s)

0.01 1.00 100.00

0.01 1.00 100.00

CAQE running time (s)

CEGAR running time (s)

0.01 1.00 100.00

0.01 1.00 100.00

CAQE running time (s)

CEGAR running time (s)

0.01 1.00 100.00

0.01 1.00 100.00

CAQE running time (s)

CEGAR running time (s)

Figure 3: QBF vs CEGAR: skeptical controllability under com (left), stb (left center) and credulous under adm (right center), stb (right).

with no E σ(F τ), T E. On line 10 this was deduced via the SAT solver reporting unsatisfiability, while on line 21 we make an additional SAT solver call which is guaranteed to be unsatisfiable. Therefore in both cases the SAT solver provides an unsatisfiable core U χ(F τ) containing exactly those units in χ(F τ) used in the unsatisfiability proof. Thus, we refine the control configuration via REFINECORE(Aτ conf) = W a (AC\Aτ conf), ya U ya W a Aτ conf,ya U ya.

6 Empirical Evaluation We overview results from an evaluation of the QBF and CEGAR approaches to controllability. We used the QBF solver CAQE 4.0.0 [Tentrup, 2019] with the Bloqqer [Heule et al., 2015] preprocessor and the flag --qdo to obtain assignments corresponding to control configurations. For CEGAR we used the Glucose 4.1 SAT solver [Audemard and Simon, 2018]. The experiments were run on Intel Xeon E5-2680 v4 2.4-GHz, 256-GB nodes with Cent OS 7 under a per-instance 900-s time and 64-GB memory limit. The implementation, benchmarks, and runtime data are available online. We generated CAFs from the 2019 ICCMA competition AFs (http://argumentationcompetition.org/2019/iccma-

caqe skept com

caqe cred stb

0 50 100 150 200 250 300

cegar skept com

cegar cred stb

Figure 4: Mean runtimes: QBF (top) and CEGAR (bottom), skeptical under com (left) and credulous under stb (right) with different values of p C (rows) and p U (columns).

instances.tar.gz) as follows. For each AF, the query argument from ICCMA 2019 is the singleton target. For each p C {0.05, 0.1, 0.15, 0.2}, each non-query argument is a control argument with probability p C. For each p U {0, 0.05, 0.1, 0.15, 0.2}, each argument (apart from control and query arguments) is uncertain with probability p U. Each attack is uncertain with probability p U/2 unless the source or the target is a control argument, and has uncertain direction with probability p U/2 unless the reverse direction is already a fixed or an uncertain attack. The rest of the arguments and attacks remain fixed. This yielded a total of 6520 CAFs, out of which 1304 are simplified CAFs with no uncertain part. We consider skeptical controllability under com and stb and credulous controllability under adm and stb. The relative efficiency of the approaches depends on the instance (see Figure 3). In general, runtimes do not correlate well with instance sizes, but rather with the benchmark domain of the original AF. Interestingly Bloqqer is able to solve a noticeable number of the QBF instances (i.e., without calling CAQE), those are shown in red. The QBF approach exhibits fewer timeouts, most noticeably on skeptical controllability under stb. The relative mean runtimes (Figure 4) depend on the problem variant. For skeptical under com, increasing both p C and p U tends to increase empirical hardness, with CEGAR exhibiting lower mean runtimes. The effect of p C is more modest on credulous under stb, where the mean runtimes of the QBF approach are considerably lower than for CEGAR.

7 Conclusions We provided complexity results for credulous and skeptical controllability in CAFs under five central semantics. Almost all cases are complete for the second or third level of the polynomial hierarchy. Due to this, we presented two declarative approaches, based on direct QBF encodings and SAT-based CEGAR, to controllability, and first results on the empirical hardness of controllability. Covering further semantics, developing further CEGAR refinement strategies, and evaluating different QBF solvers are directions for further work.

Acknowledgments This work was financially supported by Academy of Finland grants 276412, 312662, 322869 and Univ. Helsinki Do CS doctoral programme. Computational resources were provided by FGCI (urn:nbn:fi:research-infras-2016072533).

Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence (IJCAI-20)

[Arora and Barak, 2009] S. Arora and B. Barak. Computational Complexity: A Modern Approach. Cambridge University Press, 2009. [Audemard and Simon, 2018] G. Audemard and L. Simon. On the Glucose SAT solver. Int. J. Artif. Intell. T., 27(1):1840001:1 1840001:25, 2018. [Baroni et al., 2018] P. Baroni, M. Caminada, and M. Giacomin. Abstract argumentation frameworks and their semantics. In Handbook of Formal Argumentation, chapter 4, pages 159 236. College Publications, 2018. [Baumann and Brewka, 2010] R. Baumann and G. Brewka. Expanding argumentation frameworks: Enforcing and monotonicity results. In COMMA, volume 216 of FAIA, pages 75 86. IOS Press, 2010. [Baumann, 2012] R. Baumann. What does it take to enforce an argument? Minimal change in abstract argumentation. In ECAI, volume 242 of FAIA, pages 127 132. IOS Press, 2012. [Baumeister et al., 2018a] D. Baumeister, D. Neugebauer, and J. Rothe. Credulous and skeptical acceptance in incomplete argumentation frameworks. In COMMA, volume 305 of FAIA, pages 181 192. IOS Press, 2018. [Baumeister et al., 2018b] D. Baumeister, D. Neugebauer, J. Rothe, and H. Schadrack. Verification in incomplete argumentation frameworks. Artif. Intell., 264:1 26, 2018. [Besnard and Doutre, 2004] P. Besnard and S. Doutre. Checking the acceptability of a set of arguments. In NMR, pages 59 64, 2004. [Booth et al., 2013] R. Booth, S. Kaci, T. Rienstra, and L. van der Torre. A logical theory about dynamics in abstract argumentation. In SUM, volume 8078 of LNCS, pages 148 161. Springer, 2013. [Cayrol et al., 2010] C. Cayrol, F. Dupin de Saint-Cyr, and M. Lagasquie-Schiex. Change in abstract argumentation frameworks: Adding an argument. J. Artif. Intell. Res., 38:49 84, 2010. [Clarke et al., 2003] E.M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement for symbolic model checking. J. ACM, 50(5):752 794, 2003. [Clarke et al., 2004] E.M. Clarke, A. Gupta, and O. Strichman. SAT-based counterexample-guided abstraction refinement. IEEE T-CAD, 23(7):1113 1123, 2004. [Coste-Marquis et al., 2007] S. Coste-Marquis, C. Devred, S. Konieczny, M. Lagasquie-Schiex, and P. Marquis. On the merging of Dung s argumentation systems. Artif. Intell., 171(10-15):730 753, 2007. [Coste-Marquis et al., 2014] S. Coste-Marquis, S. Konieczny, J. Mailly, and P. Marquis. On the revision of argumentation systems: Minimal change of arguments statuses. In KR, pages 52 61. AAAI Press, 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 IJCAI, pages 2876 2882. AAAI Press, 2015. [de Saint-Cyr et al., 2016] F. Dupin de Saint-Cyr, P. Bisquert, C. Cayrol, and M. Lagasquie-Schiex. Argumentation update in YALLA (Yet Another Logic Language for Argumentation). Int. J. Approx. Reasoning, 75:57 92, 2016. [Diller et al., 2018] M. Diller, A. Haret, T. Linsbichler, S. R ummele, and S. Woltran. An extension-based approach to belief revision in abstract argumentation. Int. J. Approx. Reasoning, 93:395 423, 2018. [Dimopoulos and Torres, 1996] Y. Dimopoulos and A. Torres. Graph theoretical structures in logic programs and default theories. Theor. Comput. Sci., 170(1-2):209 244, 1996. [Dimopoulos et al., 2018] Y. Dimopoulos, J. Mailly, and P. Moraitis. Control argumentation frameworks. In AAAI, pages 4678 4685. AAAI Press, 2018. [Dimopoulos et al., 2019] Y. Dimopoulos, J. Mailly, and P. Moraitis. Argumentation-based negotiation with incomplete opponent profiles. In AAMAS, pages 1252 1260. IFAAMAS, 2019. [Doutre and Mailly, 2018] S. Doutre and J. Mailly. Constraints and changes: A survey of abstract argumentation dynamics. Argument & Computation, 9(3):223 248, 2018. [Doutre et al., 2014] S. Doutre, A. Herzig, and L. Perrussel. A dynamic logic framework for abstract argumentation. In 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. Artif. Intell., 77(2):321 358, 1995. [Dunne and Bench-Capon, 2002] P.E. Dunne and T.J.M. Bench-Capon. Coherence in finite argument systems. Artif. Intell., 141(1/2):187 203, 2002. [Dvor ak and Dunne, 2018] W. Dvor ak and P.E. Dunne. Computational problems in formal argumentation and their complexity. In Handbook of Formal Argumentation, chapter 13, pages 631 687. College Publications, 2018. [Heule et al., 2015] M. Heule, M. J arvisalo, F. Lonsing, M. Seidl, and A. Biere. Clause elimination for SAT and QSAT. J. Artif. Intell. Res., 53:127 168, 2015. [Niskanen et al., 2020] A. Niskanen, D. Neugebauer, M. J arvisalo, and J. Rothe. Deciding acceptance in incomplete argumentation frameworks. In AAAI. AAAI Press, 2020. [Tentrup, 2019] L. Tentrup. CAQE and Qu Ab S: Abstraction based QBF solvers. Journal on Satisfiability, Boolean Modeling and Computation, 11(1):155 210, 2019. [Wallner et al., 2017] J.P. Wallner, A. Niskanen, and M. J arvisalo. Complexity results and algorithms for extension enforcement in abstract argumentation. J. Artif. Intell. Res., 60:1 40, 2017.

Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence (IJCAI-20)