Controllability of Control Argumentation Frameworks

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

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 ∈ ⋂ σ(F), and credulously accepted if a ∈ ⋃ σ(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 .

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 (ΣP0 =ΠP0 =P, ΣPi+1=NPΣPi , and ΠPi+1=coNPΣPi ) 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}.

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 ΣP2 - completeness, strengthening the NP-hardness result of [Dimopoulos et al., 2018].

Theorem 4. Skeptical controllability for simplified CAFs is ΣP2 -complete under stb.

Proof. (Sketch.) As possible skeptical acceptance in argument-incomplete IAFs is ΣP2 -complete under stb [Baumeister et al., 2018a], a reduction by Lemma 1 establishes ΣP2 -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 ΠP2 -complete [Dunne and Bench-Capon, 2002] and possible skeptical acceptance in argument-incomplete IAFs under prf is ΣP3 -complete [Baumeister et al., 2018a], we have ΣP3 - completeness of skeptical controllability in simplified CAFs under prf via an analogous proof.

Theorem 5. Skeptical controllability for simplified CAFs is ΣP3 -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 ΣP2 -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 ΣP2 -complete under stb.

Proof. Let (F,C,U) be a CAF and T ⊆ AF a target. ΣP2 - membership 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 ΣP3 -completeness.

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

Proof. Let (F,C,U) be a CAF and T ⊆ AF a target. ΣP3 - membership 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 ΣP3 -completeness of credulous controllability in general CAFs under σ ∈ {adm, com, prf , stb}. Thus we close the gap from [Dimopoulos et al., 2018] between ΣP3 - membership and ΣP2 -hardness under stb.

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

Proof. (Sketch.) Let (F,C,U) be a CAF and T ⊆ AF a target. ΣP3 -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.

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 ΣP2 -complete.

Proof. (Sketch.) Let (F,C,U) be a CAF and T ⊆ AF a target. ΣP2 -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) = ∧a∈AF ya ∧ ∧(a,b)∈RF ∪RC ra,b ∧ ∧a∈AU∪AC (¬ya → (¬xa ∧ ∧(a,b)∈RU ∪R↔ U ¬ra,b ∧ ∧(b,a)∈RU ∪R↔ U ¬rb,a ))∧ ∧(a,b)∈R↔ U ((ya ∧ yb) → (ra,b ∨ rb,a)). The formulas ϕcf (C) = ∧(a,b)∈R(ea,b → (¬xa ∨ ¬xb)), ϕadm(C) = ϕcf (C) ∧ ∧a∈A ∧(b,a)∈R(xa → (eb,a → zb)), ϕcom(C) = ϕadm(C) ∧ ∧a∈A ∧(b,a)∈R((eb,a → zb) → xa), and ϕstb (C) = ϕcf (C) ∧ ∧a∈A(ya → (xa ∨ za)) capture the semantics σ ∈ {adm, com, stb} of the completions, where za = ∨(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) ∧ ∧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

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) = ∨(a,b)∈RU ∪R↔ U (¬ya ∧ ra,b) ∨ ∨(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

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

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(ϕ ∧ ∧t∈T xt) 4: if result = sat then 5: (result, τ ) ← SAT(ϕ ∧ ψ(Aτconf ) ∧ ∨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 ∧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 ) = ∧a∈Aτconf ya ∧ ∧a∈AC \Aτconf ¬ya and the counterexample query via ∨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 ) = ∨a∈ADDARGσ(τ) ya ∨ ∨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(ϕ ∧ ∧t∈T xt) 4: if result = unsat then return reject 5: ϕ←ϕ∧ (ψ(Aτconf ) → REFINE(F τ )) 6: while true do 7: (result, τ ) ← SAT(ϕ ∧ ψ(Aτconf ) ∧ ∨t∈T ¬xt) 8: if result = sat then 9: (result, τ ) ← SAT(ϕ ∧ χ(F τ ) ∧ ∧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 ∧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 τ ) = ∧a∈Aτ ya ∧ ∧a∈A\Aτ ¬ya ∧ ∧(a,b)∈Rτ ra,b∧∧(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 τ

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 ) =

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 CentOS 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/iccmainstances.tar.gz) as follows. For each AF, the query argument from ICCMA 2019 is the singleton target. For each pC ∈ {0.05, 0.1, 0.15, 0.2}, each non-query argument is a control argument with probability pC. For each pU ∈ {0, 0.05, 0.1, 0.15, 0.2}, each argument (apart from control and query arguments) is uncertain with probability pU . Each attack is uncertain with probability pU/2 unless the source or the target is a control argument, and has uncertain direction with probability pU/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 pC and pU tends to increase empirical hardness, with CEGAR exhibiting lower mean runtimes. The effect of pC 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 DoCS doctoral programme. Computational resources were provided by FGCI (urn:nbn:fi:research-infras-2016072533).