Optimal Status Enforcement in Abstract Argumentation

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; McBurney 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 compared 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 NP- and second-level ⌃P2 -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/.

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+ R = A;
• ÷ 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; CosteMarquis 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

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

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

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

Optimal Skeptical Status Enforcement

Input: AF F = (A↪ R), P↪ N ✓ A, and semantics σ. Task: Find an AF F ⇤ = (A↪ R⇤ ) with

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 .

• ÷ enf σns (F↪ P ) = cred(F↪ P↪ ;↪ σ) = skept (F↪ P↪ ;↪ σ);

Proposition 1. Let F = (A↪R) be an AF, P ✓ A, N = A ∩ P , and σ a unique-status semantics. It holds that

• ÷ 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 σ.

• ÷ enf σs (F↪ P) ✓ skept(F↪ ;↪ N↪ σ);
• ÷ enf σx (F↪ P) ✓ cred(F↪ P↪ ;↪ σ);
• ÷ 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 argument 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 ⌃P2 -complete if N 6= ;. Intuitively, the jump in complexity is due to coNPcompleteness 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 ⌃P2 -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 coNP-complete under stable semantics.

Corollary 12. Skeptical status enforcement under stable semantics is ⌃P2 -complete, even if N = ;.

For skeptical status enforcement under preferred semantics we show membership in ⌃P3 , which is due to the fact that checking skeptical acceptance in a fixed AF under preferred semantics is ⇧P2 -complete [Dunne and Bench-Capon, 2002].

Proposition 13. Enforcing skeptical acceptance under preferred semantics is in ⌃P3 .

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 (MaxSAT) and SAT solvers for optimally solving ⌃P2 -complete variants of status enforcement. In detail, we provide MaxSAT encodings for N = ; under admissible and stable semantics, and CEGAR for ⌃P2 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 MaxSAT, 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 MaxSAT (or simply MaxSAT) instance consists of hard clauses 'h and soft clauses 's. An assignment ⌧ is a solution to a MaxSAT instance ('h↪ 's) if ⌧ satisfies 'h. The cost of ⌧, c(⌧), is the number of clauses in 's not satisfied by ⌧ . A solution ⌧ to a MaxSAT 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 MaxSAT, we define variables xpa for each a 2 A and p 2 P and ra↪b for each a↪ b 2 A. Now ⌧(xpa ) = 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 xpa , we define variables xna 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 = Va↪b2A ↵a↪b, where

For credulous status enforcement, the hard clauses are

where 'pσ (F) encodes semantics σ so that the xpa 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 'pcf (F) = Va↪b2A ⇣≻ra↪b _≻xpa _≻xpb ⌘, for admissible sets we use formula 'padm (F) defined as

and for stable semantics

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 applyMaxSAT 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↪ ⌧) ^ Wn2N 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

If a candidate is not successfully verified, we refine formula χ of Algorithm 1 with

For skeptical status enforcement under stable semantics we slightly adapt Algorithm 1 by using

CHECK(skept↪A↪ ⌧↪ P↪N↪ stb) = φstb(A↪ ⌧) ^ Wp2P ≻xp. For the special case N = ;, we enforce a stable extension containing P via .

6 Experiments

We have implemented the MaxSAT 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 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 OpenWBO [Martins et al., 2014] as the MaxSAT 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.

1 Based 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.

2 Non-trivial instances arose mainly with p  0▷35.

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 ⌃P2 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 RelatedWork

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 MaxSAT solvers.

Acknowledgments

This work has been funded by Academy of Finland under grants 251170 COIN, 276412, and 284591.