Keywords

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

Argumentation is a core area of modern artificial intelligence research, with strong connections to knowledge representation and classical and non-monotonic logics. Argumentation frameworks (AFs) [23], a central graph-based knowledge representation formalism, provide a formal basis for abstract argumentation.

Motivated also by practical applications, AFs under various semantics give rise to important—and often computationally very hard—reasoning problems over AFs. This includes what we refer to as static (or non-dynamic) AF reasoning tasks, such as the much studied problems of skeptical and credulous acceptance of arguments. Static AF reasoning tasks have been extensively studied, to the point that today several systems implementing static AF reasoning [13, 14, 24, 26, 30, 31, 33] are available. Most often these systems are based on declarative approaches, using propositional satisfiability (SAT) solver technology or extensions thereof for solving the core reasoning task at hand [13, 14, 24, 26]. However, argumentation is intrinsically a dynamic process, and hence understanding and reasoning about the dynamics of AFs is a central and recent direction of research [8–10, 12, 18, 19, 21, 22, 29, 34]. In contrast to static AF reasoning problems, few system implementations are currently available for reasoning about different aspects of AF dynamics [17, 29, 34].

In this paper, we describe in detail Pakota, a system for optimal extension enforcement [8, 12, 17, 34] and status enforcement [29], two recently proposed hard computational problems dealing with dynamics (in connection to belief change) in abstract argumentation. In short, enforcement deals with the question of how a given AF should be revised (changed) in order for it to support (in terms of, e.g., skeptical or credulous acceptance) specific arguments.

Pakota implements algorithms for solving optimally—in terms of structural modifications to a given AF—various variants of NP-complete and \(\mathrm{\Sigma }_{2}^{P}\)-complete extension and status enforcement problems under various AF semantics, being the first system for optimal enforcement in its generality. Pakota is based on NP-encoding enforcement problems using the Boolean optimization paradigm of maximum satisfiability (MaxSAT), and further implements counterexample-guided abstraction refinement (CEGAR) [15, 16] algorithms based on SAT and MaxSAT solvers for \(\mathrm{\Sigma }_{2}^{P}\)-complete enforcement.

2 Enforcement in Abstract Argumentation

We start by reviewing argumentation frameworks and their semantics [7, 23], and the extension enforcement and status enforcement problems central to this work.

2.1 Argumentation Frameworks

Definition 1

An argumentation framework (AF) is a pair \(F=(A,R)\), where A is a finite set of arguments and \(R \subseteq A \times A\) is the attack relation. The pair \((a,b) \in R\) means that a attacks b. An argument \(a \in A\) is defended (in F) by a set \(S \subseteq A\) if, for each \(b \in A\) such that \((b,a) \in R\), there exists a \(c \in S\) such that \((c,b) \in R\).

Semantics for AFs are defined by functions \(\sigma \) which assign to each AF \(F=(A,R)\) a set \(\sigma (F)\subseteq 2^A\) of extensions. We consider for \(\sigma \) the functions \({ stb }\), \( adm \), \( com \) and \( prf \), which stand for stable, admissible, complete and preferred, respectively.

Definition 2

Given an AF \(F =(A,R)\), the characteristic function \(\mathcal {F}_F: 2^A \rightarrow 2^A\) of F is \(\mathcal {F}_F(S) = \{a \in A \mid a \text{ is } \text{ defended } \text{ by } S\}\). Moreover, for a set \(S\subseteq A\), the range of S is \(S^+_R=S\cup \{a \in A \mid (b,a) \in R, b \in S\}\).

Definition 3

Let \(F=(A,R)\) be an AF. A set \(S\subseteq A\) is conflict-free (in F), if there are no \(a, b \in S\) such that \((a,b) \in R\). We denote the collection of conflict-free sets of F by \( cf (F)\). For a conflict-free set \(S \in cf (F)\), it holds that

  • \(S\in { stb }(F)\) iff \(S^+_R = A\);

  • \(S\in adm (F)\) iff \(S \subseteq \mathcal {F}_F(S)\);

  • \(S\in com (F)\) iff \(S=\mathcal {F}_F(S)\);

  • \(S\in prf (F)\) iff \(S\in adm (F)\) and there is no \(T\in adm (F)\) with \(S\subset T\);

We use “\(\sigma \)-extension” to refer to an extension under a semantics \(\sigma \in \{{ stb }, adm , com , prf \}\).

Example 1

As an example AF, consider \(F=(A,R)\) with three arguments, \(A= \{a,b,c\}\), and attacks \(R= \{(a,b),(b,a),(b,c),(c,b),(c,a)\}\), with a graphical illustration shown in Fig. 1(a). This AF has the following stable extensions which, in this particular case, coincide with the preferred extensions: \({ stb }(F)=\{ \{b\},\{c\}\}\).

When comparing attack structures of two AFs \(F=(A,R)\) and \(F'=(A,R')\) with the same set of arguments, we make use of the cardinality of the symmetric difference of the attack relations defined by \(\vert R \Delta R' \vert = \vert R \setminus R' |+ |R' \setminus R \vert \).

Fig. 1.
figure 1

An argumentation framework (a); enforcing \(\{a,b\}\) to be a stable extension (b); credulous (c) and skeptical (d) status enforcement of \(P=\{a,b\}\), \(N=\emptyset \) under stable semantics

Full size image

2.2 Extension Enforcement

We continue by recalling the problem of extension enforcement [8, 17, 34], where we are given an AF \(F=(A,R)\) and a subset \(T \subseteq A\) of its arguments, and the goal is to modify the attack structure R such that T becomes (a subset of) an extension under the semantics \(\sigma \) in the modified AF \(F^\prime = (A,R^\prime )\).

Strict enforcement requires that the given set T of arguments has to be exactly a \(\sigma \)-extension. In non-strict enforcement, T is required to be a subset of some \(\sigma \)-extension. We denote the set of attack structures that strictly enforce T under \(\sigma \) for F by

$$ enf ^{}_{}(s,F,T,\sigma )=\{R' \mid F'=(A,R'),\; T\in \sigma (F')\},$$
$$\text{ and } \text{ by } enf ^{}_{}(ns,F,T,\sigma ) =\{R' \mid F'=(A,R'),\; \exists T'\in \sigma (F')\; : \; T' \supseteq T\}$$

for non-strict enforcement. The number of changes of an enforcement is the size of the symmetric difference of the attack structures R and \(R'\). From the computational perspective, we view extension enforcement as an optimization problem, seeking to minimize the number of changes to the attack structure.

figure a

Example 2

Consider AF F from Example 1 (shown in Fig. 1(a)). For enforcing set \(\{a,b\}\) to be a stable extension, an optimal solution AF is shown in Fig. 1(b) where the mutual attacks between a and b are removed. In this modified AF both \(\{a,b\}\) and \(\{c\}\) are stable extensions.

In the corresponding decision problem we are given in addition an integer \(k \ge 0\) and are asked whether it is possible to enforce T with \(|R \Delta R'| \le k\). We recall the computational complexity results from [34] for this decision problem in Table 1. Note that non-strict extension enforcement under admissible, complete, and preferred semantics coincide; thus it suffices to implement an algorithm for one of these problems to cover all three.

Table 1. Complexity of extension and status enforcement.
Full size table

2.3 Status Enforcement

In the status enforcement problem [29] we are given an AF \(F=(A,R)\) and two disjoint subsets \(P,N \subseteq 2^A\), \(P \cap N = \emptyset \). The goal is to enforce the arguments in P positively and arguments in N negatively, i.e., to modify the attack structure R so that all arguments in P are credulously or skeptically accepted and all arguments in N are not accepted in the modified AF \(F^\prime = (A,R^\prime )\).

For credulous status enforcement, we denote the set of attack structures that enforce (P, N) under \(\sigma \) for F by

$$ cr (F,P,N,\sigma ) = \{R' \mid F'=(A,R'), P \subseteq \bigcup \sigma (F'), N \cap \bigcup \sigma (F') = \emptyset \},$$

and, for skeptical status enforcement,

$$ sk (F,P,N,\sigma ) = \{R' \mid F'=(A,R'), P \subseteq \bigcap \sigma (F'), N \cap \bigcap \sigma (F') = \emptyset \}.$$

For \(\sigma ={ stb }\) we additionally require for skeptical status enforcement that a solution AF \(F'\) has at least one stable extension. Like extension enforcement, we view status enforcement as an optimization problem, where the goal is to minimize the cardinality of the symmetric difference of the original and the modified attack structures R and \(R^\prime \).

figure b
figure c

Example 3

For the AF from Example 1, we see in Fig. 1(c) credulous and (d) skeptical status enforcement for \(P=\{a,b\}\), \(N=\emptyset \) under the stable semantics. In the modified AF shown in Fig. 1(c) we have added an attack from a to c, which results in an AF where \(\{a\}\), \(\{b\}\), and \(\{c\}\) are all stable extensions. In the AF shown in Fig. 1(d) we have removed the mutual attacks between a and b, and removed the attack from c to b. This results in \(\{a,b\}\) being the unique stable extension of this modified AF.

The decision problem corresponding to status enforcement is the following: given an AF \(F=(A,R)\), positive and negative sets \(P,N\subseteq A\) of argument statuses, a semantics \(\sigma \), and an integer \(k \ge 0\), can the statuses in P and N be enforced under \(\sigma \) with at most k modifications to the attack structure R. The computational complexity of the decision problem was established in [29]; Table 1 provides an overview. Note that credulous status enforcement under the admissible, complete, and preferred semantics coincide [29].

3 Maximum Satisfiability

For solving variants of extension and status enforcement problems, Pakota employs constraint optimization encodings using (partial) maximum satisfiability (MaxSAT for short) as the underlying declarative language. In MaxSAT, for each variable x, we have two literals, x and \(\lnot x\). A clause is a disjunction (\(\vee \)) of literals. A truth assignment is a function from variables to \(\{0,1\}\). A clause c is satisfied by a truth assignment \(\tau \), \(\tau (c) = 1\), if \(\tau (x) = 1\) for a literal x in c or \(\tau (x) = 0\) for a literal \(\lnot x\) in c; otherwise \(\tau \) does not satisfy c, \(\tau (c) = 0\). An instance \(\varphi = (\varphi _h,\varphi _s)\) of the MaxSAT problem consists of a set \(\varphi _h\) of hard clauses, and a set \(\varphi _s\) of soft clauses. Any truth assignment \(\tau \) which satisfies each hard clause is a solution to \(\varphi \). The cost of a solution is defined by \(\textsc {cost}(\varphi ,\tau ) = \sum _{c \in \varphi _s} (1-\tau (c))\), which is the number of soft clauses not satisfied by \(\tau \). A solution \(\tau \) is optimal for \(\varphi \) if \(\textsc {cost}(\varphi ,\tau ) \le \textsc {cost}(\varphi ,\tau ^\prime )\) for all solutions \(\tau ^\prime \) to \(\varphi \). The output of a MaxSAT solver is an optimal solution to \(\varphi \).

4 Pakota

The Pakota system is implemented in the C++ programming language. The source code is available at http://www.cs.helsinki.fi/group/coreo/pakota/ under the MIT license. In what follows, we describe the main components and system architecture of the system (Sect. 4.1) and main features of Pakota (Sect. 4.2), detail the implemented algorithms (Sect. 4.3), input and output specifications (Sect. 4.4), and usage (Sect. 4.5).

Fig. 2.
figure 2

System architecture of Pakota

Full size image

4.1 System Architecture

The system architecture of Pakota is shown in Fig. 2. Pakota accepts input for the extension enforcement problem and for the credulous and skeptical status enforcement problem in the so-called APX format (see Sect. 4.4), which is parsed into an enforcement instance. The algorithms implemented in Pakota that solve the given enforcement instance form the main component of the system and are described in Sect. 4.3, employing a MaxSAT solver, or, for problem variants beyond NP, interacting MaxSAT and SAT solvers. Pakota offers a generic MaxSAT interface for plugging in the MaxSAT solver of choice and already includes MaxSAT solvers Open-WBO [27] (version 1.3.1) and LMHS [32] (version 2015.11), and the SAT solvers MiniSAT [25] (version 2.2.0, included with LMHS) and Glucose [4–6] (version 3.0, included with Open-WBO). We detail usage of the MaxSAT interface in Sect. 4.2.

The implemented algorithms for the enforcement problems can be classified according to whether they solve an NP problem or a second-level problem. For the former, the enforcement instance is encoded in a MaxSAT instance and the solution given by a MaxSAT solver is decoded to construct a solution AF to the enforcement problem, again in the APX format. In the case that the given task is a second-level problem, the algorithms implement a counterexample-guided abstraction refinement procedure, thereby iteratively querying the MaxSAT solver to construct candidate solutions and checking whether the candidate is indeed a solution to the enforcement problem via a SAT solver. In case the candidate is a solution, the decoded AF is returned in the APX format. Otherwise, i.e., in case the candidate is a non-solution, the current MaxSAT encoding is iteratively refined until an actual optimal solution is found.

4.2 Features

Supported Semantics and Reasoning Modes. An overview of the semantics and reasoning modes currently supported by Pakota is given in Table 2. Implementation of different parameter choices are discussed in more detail in Sect. 4.3.

MaxSAT and SAT Solver Interfaces. Essentially any MaxSAT solver whose source code is available can be plugged into the system. This is enabled in Pakota by offering two interfaces, MaxSATSolver.h and SATSolver.h. By creating new classes that implement these interfaces and defining the pure virtual functions declared in them, one can compile and link these to the Pakota system, which will then use the corresponding MaxSAT and SAT solvers for solving the enforcement problems. As an implementation-level detail, note that, if the MaxSAT solver uses a SAT solver internally, which is usually the case, an easy solution to potential naming conflicts is to use the same SAT solver as the SAT solver in CEGAR procedures within Pakota. The source code of Pakota already includes implementations of these interfaces for two different MaxSAT solvers, Open-WBO [27] and LMHS [32], allowing the use of these solvers simply by editing the MAXSAT_SOLVER parameter in the included Makefile before compiling.

MaxSAT and IP Encodings. In addition to directly solving extension and status enforcement instances, Pakota can for the NP variants of the problems output the internal MaxSAT encodings both in the standard WCNF MaxSAT input format as well as integer programs (IPs) in the standard LP format (applying the standard textbook encoding of MaxSAT as IP [3]). The latter option allows for calling state-of-the-art IP solvers, such as CPLEX or Gurobi, on the encodings.

4.3 Algorithms

Depending on the inherent complexity of the problems, Pakota solves the extension or status enforcement problem at hand by either encoding the problem in MaxSAT (NP-complete problems), or within a counterexample-guided abstraction refinement (CEGAR) scheme utilizing a MaxSAT solver in an iterative or incremental fashion (problems complete for the second level of polynomial hierarchy). Table 2 provides details, depending on the chosen parameters and semantics, for each problem variant, whether it is solved via direct encoding to MaxSAT (detailed in Fig. 3) or via a MaxSAT-based CEGAR algorithm (detailed as Algorithms 1 and 2).

Table 2. Extension and status enforcement problems currently supported by Pakota.
Full size table

Encoding NP Enforcement in MaxSAT. Let \(F=(A,R)\) be an AF. We utilize Boolean variables \(x_a\) and \(x^p_a\) for \(a,p \in A\), and variables \(r_{a,b}\) for \(a,b \in A\). The intended meaning of these variables is that if \(x_a\) (\(x^p_a\)) is assigned true in an assignment then a is contained in a \(\sigma \)-extension in a specific AF. The AF we are referring to is either directly encoded in the formula or encoded via a truth assignment on variables \(r_{a,b}\), i.e., if \(r_{a,b}\) is assigned true, then there is an attack from a to b. For all considered problems, soft clauses are defined by \(\varphi _s(F) = \bigwedge _{a,b \in A} r_{a,b}^\prime \), where \(r_{a,b}^\prime \) is \(r_{a,b}\) if \((a,b) \in R\), and \(\lnot r_{a,b}\) if \((a,b) \not \in ~R\). Violating a soft clause corresponds to an attack being removed or added, and incurs an associated unit cost.

Hard clauses are problem dependent. The complete list of encodings used in Pakota is provided in Fig. 3. In particular, refers to encodings for extension enforcement for strict (\(s\)) and non-strict (\(ns\)) modes. The other parameters are an AF \(F=(A,R)\), a semantics \(\sigma \in \{ adm , com ,{ stb }, prf \}\), and \(T\subseteq A\). For encoding the semantics, we adapt Boolean formulas from [11], originally presented for static AF reasoning problems. We also note that [17] apply similar encodings to ours in an integer programming based approach to the specific case of extension enforcement under admissible semantics.

Figure 2 shows for each NP-complete extension enforcement problem the corresponding MaxSAT encoding for which it holds that an optimal MaxSAT solution directly corresponds to an optimal solution for the extension enforcement problem. For instance, to optimally solve non-strict extension enforcement under the admissible semantics, we encode the input AF and set of arguments to be enforced via formula and subsequently call to compute an optimal MaxSAT solution \((c,\tau )\), with cost c and assignment \(\tau \), from which we can infer an optimal solution to the corresponding problem by extracting a new AF \(F' = (A,R')\) with \(R' = \{(a,b) \mid \tau (r_{a,b}) = 1\}\).

For the NP-complete status enforcement problems of credulous status enforcement under the admissible and stable semantics with empty negative set \(N=\emptyset \), we implemented an analogous procedure. For the input to this problem, i.e., AF \(F=(A,R)\) and positive set \(P\subseteq A\), we give the MaxSAT solver the encoding , with \(\sigma \in \{ adm ,{ stb }\}\). From an optimal MaxSAT solution we can infer an optimal solution to the status enforcement problem similarly as for extension enforcement by generating a new AF \(F' = (A,R')\) with \(R' = \{(a,b) \mid \tau (r_{a,b}) = 1\}\).

The remaining encodings in Fig. 3 are used in our CEGAR algorithms for the second-level complete problems.

Fig. 3.
figure 3

Encoding extension and status enforcement

Full size image

Counterexample-guided Abstraction Refinement. Pakota implements the second-level complete problems arising in status enforcement and extension enforcement by a counterexample-guided abstraction refinement (CEGAR) approach. Concretely, we let a MaxSAT solver compute a candidate solution from an NP abstraction of the second-level complete problem, and subsequently check whether the candidate is a solution with a SAT solver. In case a solution is found, i.e., the SAT solver reports unsatisfiability, we extract from the MaxSAT solution an optimal solution to the enforcement problem. Otherwise, we call the MaxSAT solver again on a refined formula which includes further hard clauses extracted from the counterexample delivered by the SAT solver.

The CEGAR algorithms implemented in Pakota are shown in Algorithm 1 for extension enforcement, and in Algorithm 2 for status enforcement. We describe the algorithm for extension enforcement, as the CEGAR algorithm for status enforcement is similar (the main difference lies in the used formulas).

For extension enforcement, we implemented the second-level complete problem of strict extension enforcement under the preferred semantics as shown in Algorithm 1. Given an AF \(F=(A,R)\), a set \(T \subseteq A\) to enforce, we define the initial hard clauses \(\varphi _h\) to be the same as for the NP-complete strict extension enforcement problem under the complete semantics. In the while-loop, we call the MaxSAT solver on this set of hard clauses augmented with the same soft clauses, \(\varphi _s(F)\), as for the NP-complete variants. From an optimal solution \(\tau \) delivered by the MaxSAT solver, we check whether this candidate is a solution to strict extension enforcement under the preferred semantics using the formula (see Fig. 3). If the SAT solver reports unsatisfiability of this formula, we terminate and return the AF encoded in \(\tau \). Otherwise we refine, i.e., increment, the hard clauses by (see again Fig. 3 for details).

For status enforcement we implemented Algorithm 2. For a given input to the second-level complete problems for status enforcement we consider here, i.e., credulous status enforcement under the admissible and stable semantics, and skeptical status enforcement under the stable semantics, this algorithm computes an optimal solution AF. The input for this problem consists of an AF \(F=(A,R)\) and sets \(P,N\subseteq A\).

figure d

4.4 Input Format

For extension enforcement, the input AF and enforcement request are specified using the following predicates, extending the APX format for specifying AFs.

  • arg(X): X is an argument

  • att(X,Y): there is an attack from X to Y

  • enf(X): enforce argument X

Example 4

The enforcement of argument a for the AF in Fig. 4(a) is specified in the Pakota input format as shown in Fig. 4(b). On this input, Pakota may return the output shown in Fig. 4(c), i.e., the AF in Fig. 4(d).

Fig. 4.
figure 4

Example of Pakota input and output formats

Full size image

As in extension enforcement, for status enforcement the AF is represented using the arg and att predicates. The arguments to be positively and negatively enforced are represented via the pos and neg predicates, respectively. For example, pos(a). enforces argument a positively. The reasoning mode between credulous and skeptical is chosen from the command line.

4.5 Usage and Options

After compilation, the Pakota system is used from the command line with

$${\texttt {./pakota<file> <mode> <sem> [options]}}$$

The command line arguments enabling the choice of AF semantics and reasoning mode are the following.

figure e

Furthermore, command line options -h (for help message), -v (for version number), -o (for specifying output to file) and -t (for outputting NP-encodings in WCNF and LP formats) are available.

4.6 Benchmarks and Generators

The Pakota webpage also offers sets of benchmarks for both extension enforcement and status enforcement in the Pakota input format. Furthermore, we provide via the webpage our benchmark generator software, AfGen and EnfGen, which we used to generate the benchmark sets. The AF generator AfGen forms argumentation frameworks in APX format implementing the Erdős-Rényi random digraph model. The generator is called as

$${\texttt {./afgen<args> <prob>}}$$

where parameters \(\texttt {<args>}\) and \(\texttt {<prob>}\) specify the number of arguments and the probability of an attack in the output AF. The generator forms an argumentation framework with arguments \(1,\cdots ,\texttt {<args>}\), including an attack between each pair of arguments independently with probability \(\texttt {<prob>}\).

The enforcement instance generator EnfGen takes as input an AF in APX format, and produces an enforcement instance. It is called as

$${\texttt {./enfgen<file> <mode> <enfs>}}$$

where \(\texttt {<file>}\) is the input AF and \(\texttt {<mode>}\) is either \(\texttt {ext}\) or \(\texttt {status}\), corresponding to extension and status enforcement, respectively. In case of extension enforcement, \(\texttt {<enfs>}\) is an integer stating the number of arguments to be enforced, and for status enforcement, \(\texttt {<enfs>}\) is a pair of integers, corresponding to the number of positively and negatively enforced arguments. The generator reads the arguments from the AF and samples the enforced arguments uniformly at random without replacement.

5 Performance Overview

We empirically evaluate the impact of the choice of the underlying MaxSAT solver on the performance of Pakota on various NP-complete and \(\mathrm{\Sigma }_{2}^{P}\)-complete variants of extension and status enforcement. This complements the scalability experiments using only a single solver presented in [29, 34], as well as the comparison presented in [34] with the IP-based approach to extension enforcement under admissible semantics described in [17]. For the NP problems, we used five state-of-the-art MaxSAT solvers: MaxHS [20], Maxino [1], MSCG [28], Open-WBO [27], and WPM [2], using the newest MaxSAT Evaluation 2015 versions, as well as the commercial IBM CPLEX integer programming solver (version 12.6). For CEGAR, we compare the performance of Open-WBO and LMHS [32] as the underlying MaxSAT solvers, as supported by Pakota. The experiments were run on 2.83-GHz Intel Xeon E5440 quad-core machines with 32-GB RAM and Debian GNU/Linux 8 using a timeout of 900 seconds per instance.

Fig. 5.
figure 5

MaxSAT solver comparison on NP-complete extension enforcement. Left: non-strict admissible; middle: non-strict stable; right: strict complete

Full size image

We generated the benchmarks using our AfGen and EnfGen generators. For extension enforcement, for each number of arguments \(|A| \in \{25,50,\cdots \}\) and each edge probability \(p \in \{0.05,0.1,0.2,0.3\}\), we generated five AFs. For each AF, we generated five enforcement instances with |T| enforced arguments, for each \(|T|/|A| \in \{0.05,0.1,0.2,0.3\}\). We thus obtained 400 instances for each |A|. For status enforcement, for each \(|A| \in \{20,40,\cdots ,200\}\) and \(p \in \{0.05,0.1,\cdots ,0.35\}\), we generated 10 AFs. For each AF, we generated an enforcement instance containing \((|P|,|N|) \in \{(1,0),(2,0)\cdots ,(5,0),(5,1),(2,2),(1,5)\}\) positively and negatively enforced arguments. This gave a total of 560 status enforcement instances for each |A|.

An overview of the results, comparing the different underlying MaxSAT solvers, is provided in Fig. 5 (NP-complete extension enforcement), Fig. 6 (NP-complete status enforcement), and Fig. 7 (CEGAR for extension and status enforcement). Fig. 5 left and middle show the number of instances solved (x-axis) by different MaxSAT solvers under different per-instance timeouts (y-axis) for non-strict extension enforcement under the admissible (left) and stable semantics (middle). Interestingly, in both cases CPLEX performs well (although on admissible, on a majority of the instances is solved faster by most of the other solvers).

Fig. 6.
figure 6

NP-complete credulous status enforcement under admissible

Full size image

On strict extension enforcement under the complete semantics (Fig. 5 right), the median runtimes for CPLEX scale noticeably worse than for the rest of the solvers wrt the number of arguments. However, here we note that only CPLEX and Maxino were able to solve all instances; thus Maxino turned out to be clearly the best solver on strict complete. Fig. 6 provides an overview for credulous status enforcement under the admissible semantics. Here we observe that the so-called core-guided MaxSAT solvers perform the best, while the SAT-IP hybrid solver MaxHS—typically competitive mainly on weighted MaxSAT instances—performs the worst. We also observed similar performance under the stable semantics. Overall, for the NP-complete enforcement problems, CPLEX and Maxino tend to provide the best choice of solvers, but the choice of the single best solver tends to depend on the problem variant (strict/non-strict, semantics).

Turning to the \(\mathrm{\Sigma }_{2}^{P}\)-complete enforcement problems Fig. 7 gives an overview of the performance of Open-WBO and LMHS within our CEGAR procedures for strict extension enforcement under the preferred semantics (left), and credulous (middle) and skeptical (right) status enforcement under the stable semantics. Evidently, on these instances generated with our EnfGen, out of the two solvers Open-WBO provides the best MaxSAT solver for the CEGAR procedures.

Fig. 7.
figure 7

MaxSAT solver comparison within CEGAR. Left: strict extension enforcement under preferred; credulous (middle) and skeptical (right) status enforcement under stable

Full size image

6 Conclusions

The Pakota system is a first system implementation in its generality for solving NP-complete and \(\mathrm{\Sigma }_{2}^{P}\)-complete problem instances of extension enforcement and status enforcement—two related problems motivated by the study of dynamic aspects of argumentation frameworks. We provided a detailed overview of the Pakota system—available in open source—including the input-output format, system design, functionality, details on the underlying MaxSAT encodings and MaxSAT-based CEGAR algorithms implemented in Pakota, and its API allowing for plugging in different SAT and MaxSAT solvers used as core search engines. We also provided a detailed evaluation of the impact of the choice of MaxSAT solvers (including the use of the state-of-the-art integer programming system CPLEX) on the performance of Pakota on various variants of extension and status enforcement problems. In addition to Pakota, we also provide open-source benchmark generators for extension and status enforcement for the use of the research community at large through the Pakota system webpage. Future work on Pakota includes extensions to support further central AF semantics, including grounded, semi-stable, and stage.