Abstract solvers for Dung’s argumentation frameworks

Abstract

Abstract solvers are a quite recent method to uniformly describe algorithms in a rigorous formal way via graphs. Compared to traditional methods like pseudo-code descriptions, abstract solvers have several advantages. In particular, they provide a uniform formal representation that allows for precise comparisons of different algorithms. Recently, this new methodology has proven successful in declarative paradigms such as Propositional Satisfiability and Answer Set Programming. In this paper, we apply this machinery to Dung’s abstract argumentation frameworks. We first provide descriptions of several advanced algorithms for the preferred semantics in terms of abstract solvers. We also show how it is possible to obtain new abstract solutions by “combining” concepts of existing algorithms by means of combining abstract solvers. Then, we implemented a new solving procedure based on our findings in cegartix, and call it cegartix+. We finally show that cegartix+ is competitive and complementary in its performance to cegartix on benchmarks of the first and second argumentation competition.

Keywords

Abstract argumentation abstract solvers

1. Introduction

Dung’s concept of abstract argumentation [23] is nowadays a core formalism in Artificial Intelligence [4,46]. The problem of solving certain reasoning tasks on such frameworks is the centerpiece of many advanced higher-level argumentation systems. The problems to be solved can however be intractable and might even be hard for the second level of the polynomial hierarchy [24,26]. Thus, efficient and advanced algorithms have to be developed in order to deal with real-world size data within reasonable performance bounds. The argumentation community is currently facing this challenge [17]: Already the second edition [27] of the solver competition [50,51] was held in 2017. Thus, the number of new algorithms and systems is steadily increasing, and we expect this to continue in the (near) future. Being able to precisely analyze and compare already developed and new algorithms is a fundamental step in order to understand the ideas behind such high-performance systems, and to build a new generation of more efficient algorithms and solvers.

Usually, algorithms are presented by means of pseudo-code descriptions, but other communities have experienced that analyzing such algorithms on this basis may not be fruitful. More formal descriptions, which allow, e.g. for a uniform representation, and are more amenable to comparison and to state formal results, have thus been developed: a successful approach in this direction is the concept of abstract solvers [44]. Hereby, one characterizes the possible states of computation as nodes of a graph, and the techniques (i.e., the computation steps in the algorithms) as arcs between nodes. In this way, the whole solving process amounts to a path in the graph. This concept proved successful for SAT [44], and also has been applied to several variants of Answer Set Programming [6,36,37].

In this paper, we apply abstract solvers to certain problems in Dung’s argumentation frameworks. In order to understand whether abstract solvers are well suited also for this domain, we consider quite advanced algorithms for solving problems that are hard for the second level of the polynomial hierarchy – the considered algorithms range from dedicated [45] to reduction-based [13,25] approaches (see [19] for a survey). We show that abstract solvers allow for convenient algorithms design resulting in a clear and mathematically precise description. Moreover, formal properties of the algorithms (i.e. correctness) are easily specified by means of related graph properties (i.e. reachability). We then illustrate how abstract solvers allow to highlight in a more clear way similarities and differences among solving algorithms: This paves the way for a uniform view of the three solving algorithms mentioned above, thus simplifying the combination of concepts implemented in different solvers in order to define new abstract solutions. We propose one such combination and, in order to test its viability, we implemented the outcome of this combination inside the well-known cegartix solver [25] and show that the resulting solver cegartix+ is complementary in terms of performance w.r.t. cegartix for certain tasks under the preferred semantics. We do so by using benchmarks of the first and second argumentation competition, as well as instances from earlier work. This is an interesting result which shows that a combination based on abstract solvers is proven to be also useful in practice (for similar observations, see [36,44]). We finally show (with focus on cegartix), how reasoning tasks under further semantics, other than preferred, can be solved with this framework, and demonstrate how optimizations are easily added to our abstract solvers in a modular way.

To sum up, our main contributions are as follows:

We provide a full formal description of recent algorithms [13,25,45] for reasoning tasks under the preferred semantics in terms of abstract solvers, thus enabling a comparison of these approaches at a formal level.

We outline how our formal descriptions can be used to gain more insight into the algorithms, and how certain combinations can pave the way for new solutions.

We implement such a new solution inside cegartix and analyze its performance.

We show how other semantics and optimizations can be incorporated to our abstract solvers.

The paper is structured as follows. Section 2 introduces the required preliminaries about abstract argumentation frameworks and abstract solvers. Then, Section 3 shows how our target algorithms are reformulated in terms of abstract solvers and introduces a new solving algorithm obtained from combining concepts from the target algorithms. Implementation and experimental analysis of the combined algorithm can be found in Section 4. Section 5 presents abstract solver representations of algorithms for reasoning tasks under other semantics, and indicates how shortcuts can be easily and modularly added. Section 6 provides a discussion of related research and Section 7 closes the paper with final remarks. We only include the full proofs of representative lemmata and theorems in the main body of the paper. The remaining proofs can be found in the Appendix.

The current paper extends and differs from an earlier version [8] as follows: (i) a new combination of abstract solvers is presented, which is easier to understand and more amenable to be implemented than the one in [8], (ii) an implementation and experimental evaluation of the newly proposed algorithm are discussed, (iii) we apply additional and modified transition rules of algorithms for other semantics and optimizations (i.e. short-cuts) to the algorithms, with related formal results, and (iv) a detailed analysis of related work is provided.

2. Preliminaries

In this section we first review (abstract) argumentation frameworks [23] and their semantics (see [1] for an overview), and then introduce abstract solvers [44] on the concrete instance describing the Davis–Putnam–Logemann–Loveland (dpll) procedure for SAT solving [20].

2.1. Abstract argumentation frameworks

An argumentation framework (AF) is a pair $F = (A, R)$ where A is a finite1

¹
In the literature also infinite AFs have been considered. We refer to [3] for the effects this has on semantics.

set of arguments and

R \subseteq A \times A

is the attack relation. Semantics for argumentation frameworks assign to each AF

F = (A, R)

a set

σ (F) \subseteq 2^{A}

of extensions. We consider here for σ the functions

adm

com

, and

prf

, which stand for admissible, complete, and preferred semantics. Towards the definitions of the semantics we need some formal concepts. For an AF

F = (A, R)

, 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 is a

c \in S

, such that

(c, b) \in R

holds.

Fig. 1.

AF F with $prf (F) = {{a, c}, {a, d}}$ .

Definition 1.

Let $F = (A, R)$ be an AF. A set $S \subseteq A$ is conflict-free (in F), denoted $S \in cf (F)$ , if there are no $a, b \in S$ such that $(a, b) \in R$ . For $S \in cf (F)$ , it holds that

$S \in adm (F)$ iff each $a \in S$ is defended by S;

$S \in com (F)$ iff $S \in adm (F)$ and for each $a \in A$ defended by S, $a \in S$ holds;

$S \in prf (F)$ iff $S \in adm (F)$ and there is no $T \in adm (F)$ with $T \supset S$ , or equivalently,

$S \in prf (F)$ iff $S \in com (F)$ and there is no $T \in com (F)$ with $T \supset S$ .

Example 1.

Consider the AF $F = ({a, b, c, d}, {(a, b), (b, c), (b, d), (c, d), (d, c)})$ depicted in Fig. 1 where nodes of the graph represent arguments and edges represent attacks. The extensions of F under admissible, complete, and preferred semantics are as follows: $adm (F) = {\emptyset, {a}, {a, c}, {a, d}}$ , $com (F) = {{a}, {a, c}, {a, d}}$ , and $prf (F) = {{a, c}, {a, d}}$ .

Given an AF $F = (A, R)$ , an argument $a \in A$ , and a semantics σ, the problem of skeptical acceptance ( $Skep t_{σ}$ ) asks whether it is the case that a is contained in all σ-extensions of F; the problem of credulous acceptance ( $Cre d_{σ}$ ) asks if a is contained in at least one σ-extension. While skeptical acceptance is trivial for $adm$ and decidable in polynomial time for $com$ , it is $Π_{2}^{P}$ -complete2

The class $Π_{2}^{P} = {coNP}^{NP}$ denotes the class of problems $P$ , such that the complementary problem $\overline{P}$ can be decided by a nondeterministic polynomial time algorithm that has (unrestricted) access to an $NP$ -oracle.

for

prf

, see [21,23,24].

2.2. Abstract solvers for SAT

Most SAT solvers are based on the Davis–Putnam–Logemann–Loveland (dpll) procedure [20]. We give an abstract solver for dpll following the work of Nieuwenhuis et al. [44]. The abstract solver is described by assigning a graph to each instance of the problem, where nodes and edges represent states and transitions of the actual solver, respectively. We start with basic notation for Boolean logic.

For a Conjunctive Normal Form (CNF) formula φ (resp. a set of literals M), we denote the set of atoms occurring in φ (resp. in M) by $atoms (φ)$ (resp. $atoms (M)$ ). A literal is an atom a or its negation $\neg a$ . The complement $\overline{l}$ of literal l is defined as $\overline{a} = \neg a$ and $\overline{\neg a} = a$ . We identify a consistent set E of literals (i.e. a set that does not contain a literal and its complement) with an assignment to $atoms (E)$ as follows: if $a \in E$ then a maps to $true$ , while if $\neg a \in E$ then a maps to $false$ . By $Sat (φ)$ we refer to the set of satisfying assignments of φ.

We now introduce an abstract procedure for deciding whether a CNF formula is satisfiable. A decision literal is a literal annotated by d, as in $l^{d}$ . An annotated literal is a literal, a decision literal or the false constant ⊥. For a set X of atoms, a record relative to X is a string E composed of annotated literals over X without repetitions. For instance, ∅, $\neg a^{d}$ and $a \neg a^{d}$ are records relative to the set ${a}$ . We say that a record E is inconsistent if it contains ⊥ or both a literal l and its complement $\overline{l}$ , and consistent otherwise. Moreover, by $unsat$ we represent an inconsistent and decision-free record. We sometimes identify a record with the set containing all its elements without annotations, i.e. with an assignment to the atoms. For example, we identify the consistent record $b^{d} \neg a$ with the consistent set ${\neg a, b}$ of literals, and so with the assignment which maps a to $false$ and b to $true$ . Finally, $| E |$ denotes the number of literals in record E.

Each CNF formula φ determines its dpll graph ${DP}_{φ}$ . The set of nodes (states) of ${DP}_{φ}$ consists of the records relative to $atoms (φ)$ and two distinguished states $Accept$ and $Reject$ . The edges of the graph ${DP}_{φ}$ are specified by the transition rules presented in Fig. 2. A node in the graph is terminal if no edge originates from it; in practice, the terminal nodes are $Accept$ and $Reject$ . The initial state of the abstract solver is the empty record ∅. In solvers, generally the oracle rules are chosen with the preference order according to the order in which they are stated in Fig. 2. An exception is the failing rule, which has a higher priority than all the oracle rules.

Fig. 2.

The transition rules of ${DP}_{φ}$ .

Intuitively, every state of the dpll graph represents some hypothetical state of the dpll computation whereas a path in the graph is a description of a process of search for a satisfying assignment of a given CNF formula. The rule ${Decide}_{}$ asserts that we make an arbitrary decision to add a literal or, in other words, to assign a value to an atom. Since this decision is arbitrary, we are allowed to backtrack at a later point. The rule ${UnitPropagate}_{}$ asserts that we can add a literal that is a logical consequence of our previous decisions and the given formula. The rule ${Backtrack}_{}$ asserts that the present state of computation is failing but can be fixed: at some point in the past we added a decision literal whose value we can now reverse. The rule ${Fail}_{}$ asserts that the current state of computation has failed and cannot be fixed. The rule ${Succeed}_{}$ asserts that the current state of computation corresponds to a successful outcome.

To decide the satisfiability of a CNF formula it is enough to find a path in ${DP}_{φ}$ leading from state ∅ to a terminal state. If it is $Accept$ , then the formula is satisfiable, and if it is $Reject$ , then it is unsatisfiable. Since there is no infinite path, a terminal state is always reached. The following result states this observation formally.

Theorem 2.1.

For any CNF formula φ, the graph ${DP}_{φ}$ is finite and acyclic; any terminal state of ${DP}_{φ}$ reachable from the initial state other than $Reject$ is $Accept$ ; the record in the state preceding $Accept$ corresponds to satisfying assignment of φ; and $Reject$ is reachable if and only if φ is unsatisfiable.

A proof of this theorem can be found in [36, Prop. 1] and (using a slightly different statement) in [44, Lemma 2.9]. The fact that $Accept$ is reachable from the initial state iff φ is satisfiable follows directly.

Figure 3 presents two paths in ${DP}_{φ}$ from the initial state ∅ to the terminal state $Accept$ . Every edge is annotated on the left by the name of the transition rule that gives rise to this edge in ${DP}_{φ}$ . Thus, Theorem 2.1 asserts that φ is satisfiable; moreover, the record where the ${Succeed}_{}$ rule is applied corresponds to a satisfying assignment of φ, i.e. ${a, c, b}$ .

Fig. 3.

Examples of paths in ${DP}_{{a \lor b, \overline{a} \lor c}}$ .

The difference between the paths in Fig. 3 is that only the path on the left will be indeed followed by SAT solvers, given it adheres with the ordering followed by SAT solvers, while the path on the right applies ${Decide}_{}$ (see (*)) where ${UnitPropagate}_{}$ is applicable.

2.3. Abstract solvers for computing maximal satisfying assignments

We now define a modification of the graph presented in the previous sub-section that will be useful in the definition of a new solving algorithm in Section 3.4.

The goal of this graph is to compute a maximal satisfying assignment of a CNF formula in the sense that the set of atoms mapped to true is ⊆-maximal among all satisfying assignments. In order to do this it is enough to modify the graph ${DP}_{φ}$ such that ${Decide}_{}$ always assigns the decision literal to true by default, i.e. to substitute rule ${Decide}_{}$ in Fig. 2 with the following rule ${Decide}_{}^{≺}$ , where a represents an atom instead of a literal: $\begin{matrix} {Decide}_{}^{≺} & E & \Rightarrow E a^{d} & if \{\begin{matrix} E is consistent and \\ neither a nor \neg a occur in E \end{matrix} \end{matrix}$

Let us call the resulting graph ${DP}_{φ}^{≺}$ , whose nodes correspond to the nodes of ${DP}_{φ}$ graph. We can state the following theorem.

Theorem 2.2.
For any CNF formula φ, the graph ${DP}_{φ}^{≺}$ is finite and acyclic; any terminal state of ${DP}_{φ}^{≺}$ reachable from the initial state is either $Reject$ or $Accept$ ; the record in the state preceding $Accept$ corresponds to a maximal satisfying assignment of φ, and $Reject$ is reachable if and only if φ is unsatisfiable.

Proofs of this theorem can be found in [47, Theorem 2] and in [12, Prop. 1].
3. Algorithms for preferred semantics

In this section we first abstract two SAT-based algorithms for preferred semantics, namely PrefSat [13] (implemented in the tool ArgSemSat [14]) for extension enumeration, and an algorithm for deciding skeptical acceptance of cegartix [25]. Moreover, we abstract the dedicated approach for enumeration of [45]. Finally, in Section 3.4 we show how our graph representations can be used to develop a novel algorithm, by combining parts of cegartix and ${DP}_{}^{≺}$ .

A key insight of the SAT-based algorithms is that preferred extensions can be found by iterative computation of certain extensions of a base semantics (admissible or complete): first, any extension of the base semantics is computed, and then, in each step, a strictly bigger (w.r.t. subset) one is computed. As these subproblems are in $NP$ , each step is delegated to a SAT solver. The direct approach from [45], on the other hand, does not rely on external SAT solvers but uses a genuine procedure to compute preferred extensions. What the algorithms have in common is that they maintain a list of already found preferred extensions by which they constrain the search for new ones. All algorithms continue the search for new extensions until none can be found, the algorithm for skeptical acceptance just adds the constraint that the queried argument must not be contained.

We will present these algorithms in a uniform way via abstract solvers, abstracting from some minor tool-specific details. By presenting algorithms in such a uniform way, the relation among these algorithms becomes much clearer than by using, e.g. pseudo-code-based descriptions. In fact, common to all algorithms is a conceptual two-level architecture of computation, similar to Answer Set Programming solvers for disjunctive logic programs [6]. The lower level corresponds to a dpll-like search subprocedure, while the higher level part takes care of the specific theory and drives the overall algorithm. For PrefSat and cegartix, the subprocedures actually are delegated to a SAT solver, while the dedicated approach carries out a tailored search procedure. Such common architecture is difficult to spot by looking at the related pseudo-code descriptions, while it will be clear by employing abstract solvers.

Each algorithm uses its own data structures, and, by slight abuse of notation, for a given AF $F = (A, R)$ , the variables they use are denoted by $atoms (F)$ . For this set it holds that $A \subseteq atoms (F)$ , i.e. there is an atom for each argument. The states of all the graph representations we will define are either

an annotated triple ${(ϵ, E^{'}, E)}_{i}$ where $i \in {out, base, \max}$ , $ϵ \subseteq 2^{A}$ is a set of sets of arguments, and both $E^{'}$ and E are records over $atoms (F)$ ; or

$Ok (ϵ)$ for $ϵ \subseteq 2^{A}$ ; or

a distinguished state $Accept$ or $Reject$ .

The intended meaning of a state ${(ϵ, E^{'}, E)}_{i}$ is that ϵ is the set of already found preferred extensions of F (visited part of the search space), $E^{'}$ is a record representing the current candidate extension (which is admissible or complete in F and, for the SAT-based algorithms, has to be extended in the next iteration), E is a record that may be currently modified, and i refers to the current level of computation. Note that both E and $E^{'}$ are records, and they will be modified in the course of the computation; on the other hand found preferred extensions will be translated to a set of arguments before being stored in ϵ, and permanently left there unmodified. The annotation i denotes the current level of computation the procedure is in. Both annotations $base$ and $\max$ correspond to different lower level computations, typically SAT calls, while $out$ is used for states in which (simple) checks outside such procedures have to be made. Transition rules reflecting the higher level of computation shift these annotations, e.g. a shift from a $out$ to $base$ means that the algorithm is starting a call to a SAT solver. Transition rules mirroring rules “inside” a SAT solver do not modify i. A path through a graph made up of such states, representing a run of an algorithm, will then usually start in an $out$ state, contain several subpaths consisting exclusively of either $base$ states or $\max$ states, and finally end in the state $Ok (ϵ)$ (for enumeration algorithms) or in one of the states $Accept$ or $Reject$ (for acceptance algorithms).

The remaining states denote terminated computation: $Ok (ϵ)$ contains all solutions to the enumeration problem, while $Accept$ or $Reject$ denote an answer to a decision problem.

The SAT-based algorithms construct formulas by a function f s.t. $A \subseteq atoms (f (ϵ, E, F, α)) \subseteq atoms (F)$ for all possible arguments of f. The formulas $f (ϵ, E, F, α)$ are adapted from [5]. The argument α is relevant only for cegartix to decide skeptical acceptance of α. Finally, we use $e (E) = E \cap A$ to project the arguments from a record E on the set of arguments A.

We now define a strict partial order on states, that will be used to show acyclicity of graphs later in this section. First, we define a particular representation of records used for lexicographic comparison.

Definition 2.
Let E be a record. E can be written as $L^{0} l^{1} L^{1} \dots l^{p} L^{p}$ where $L^{0}, \dots, L^{p}$ are strings of non-decision literals and $l^{1}, \dots, l^{p}$ are all the decision literals of E. We define the sequence representation of E as $s (E) = | L^{0} | | L^{1} | \dots | L^{p} |$ . For two sequence representations of records $s (E_{1}) = x_{1} x_{2} \dots x_{k_{1}}$ and $s (E_{2}) = y_{1} y_{2} \dots y_{k_{2}}$ , we say that $s (E_{1})$ is lexicographically smaller than $s (E_{2})$ , $s (E_{1}) <_{lex} s (E_{2})$ , if $x_{n} < y_{n}$ for the first index n where $x_{n}$ and $y_{n}$ differ with $n ⩽ min (k_{1}, k_{2})$ , or if $k_{1} < k_{2}$ and for all $n ⩽ min (k_{1}, k_{2})$ we have $x_{n} = y_{n}$ .
Example 2.
Consider the records $E_{1} = \neg b c^{d}$ , $E_{2} = \neg b c^{d} d^{d}$ , and $E_{1} = b c^{d} \neg d$ . The sequence representations of these records are given by $s (E_{1}) = 1 0$ , $s (E_{2}) = 1 0 0$ , and $s (E_{3}) = 1 1$ . The lexicographic ordering is $s (E_{1}) <_{lex} s (E_{2}) <_{lex} s (E_{3})$ .

The orders on states are now defined in a way that the graphs produced by the abstract solvers presented in this section only feature edges between states $ς_{1}$ and $ς_{2}$ such that $ς_{1} < ς_{2}$ .
Definition 3.
Let $ϵ_{1}$ , $ϵ_{2}$ be sets of sets of arguments, $E_{1}$ , $E_{2}$ , $E_{1}^{'}$ , $E_{2}^{'}$ be records, and $i_{1}, i_{2} \in {base, \max, out}$ . We define the following strict partial orders (i.e. irreflexive and transitive binary relations): $<_{ϵ}$ :
$ϵ_{1} <_{ϵ} ϵ_{2}$ iff $ϵ_{1} \subset ϵ_{2}$ .
$<_{E^{'}}$ :
$E_{1}^{'} <_{E^{'}} E_{2}^{'}$ iff $e (E_{1}^{'}) \subset e (E_{2}^{'})$ .
$<_{E}$ :
$E_{1} <_{E} E_{2}$ iff $s (E_{1}) <_{lex} s (E_{2})$ , where $<_{lex}$ is the lexicographic order.
$<_{i}$ :
$base <_{i} \max <_{i} out$ .

The strict partial order < on states is defined such that for any two states $ς_{1} = {(ϵ_{1}, E_{1}^{'}, E_{1})}_{i_{1}}$ and $ς_{2} = {(ϵ_{2}, E_{2}^{'}, E_{2})}_{i_{2}}$ , $ς_{1} < ς_{2}$ iff
$ϵ_{1} <_{ϵ} ϵ_{2}$ , or

$ϵ_{1} = ϵ_{2}$ and $i_{1} <_{i} i_{2}$ , or

$ϵ_{1} = ϵ_{2}$ and $i_{1} = i_{2}$ and $E_{1}^{'} <_{E^{'}} E_{2}^{'}$ , or

$ϵ_{1} = ϵ_{2}$ and $i_{1} = i_{2}$ and $E_{1}^{'} = E_{2}^{'}$ and $E_{1} <_{E} E_{2}$ .

Example 3.
Consider the states $ς_{1} = (\emptyset, out, c^{d}, b^{d} \neg d)$ , $ς_{2} = ({{a}}, base, c^{d}, b^{d} \neg d)$ , $ς_{3} = ({{a}}, \max, b \neg c, b^{d} \neg d)$ , $ς_{4} = ({{a}}, \max, b d^{d}, \neg b c^{d})$ , and $ς_{5} = ({{a}}, \max, b d^{d}, \neg b c^{d} d^{d})$ . It holds that $ς_{1} < ς_{2} < ς_{3} < ς_{4} < ς_{5}$ . First, $ς_{1} < ς_{2}$ holds due to $\emptyset \subset {{a}}$ . Moreover, $ς_{2} < ς_{3}$ is because of $base <_{i} \max$ . Furthermore, $ς_{3} < ς_{4}$ holds since $e (b \neg c) = {b} \subset {b, d} = e (b d^{d})$ . Finally, observe that $\neg b c^{d} d^{d}$ can be written, in the spirit of Definition 2, as $\neg b c^{d} \emptyset d^{d} \emptyset$ , where ∅ denotes the empty string. Hence we obtain $s (\neg b c^{d} d^{d}) = 1 0 0$ and similarly $s (\neg b c^{d}) = 1 0$ . We get $ς_{4} < ς_{5}$ since $s (\neg b c^{d}) = 1 0 <_{lex} 1 0 0 = s (\neg b c^{d} d^{d})$ .

One can check that all orders on elements are transitive and irreflexive. Therefore the construction of < also ensures these properties for the order on states.
3.1. SAT-based algorithm for enumeration

PrefSat (Algorithm 1 of [13]) is a SAT-based algorithm for finding all preferred extensions of a given AF. The algorithm maintains a list of visited preferred extensions. It first searches for a complete extension not contained in previously found preferred extensions. If such an extension is found, it is iteratively extended until we reach a subset-maximal complete extension, which is a preferred extension by definition. This preferred extension is stored, and we repeat the process.

This algorithm is realized by two subprocedures that are delegated to a SAT solver. The first has to generate a complete extension not contained in one of the enumerated preferred extensions, and the second searches for a complete extension that is a strict superset of a given one.

Fig. 4.

The rules of ${E NUM}_{\overline{f}}^{F}$ .

We now represent PrefSat as an abstract solver. The graph ${E NUM}_{\overline{f}}^{F}$ for an AF F and a vector of functions $\overline{f} = (f_{base}^{com}, f_{\max}^{com})$ is defined by the states over $atoms (F)$ and the transition rules presented in Fig. 4. Its initial state is ${(\emptyset, \emptyset, \emptyset)}_{base}$ . We assume the functions $f_{base}^{com}$ and $f_{\max}^{com}$ that generate CNF formulas for $ϵ \subseteq 2^{A}$ , a record E, and an argument $α \in A$ such that: $\begin{array}{l} {e (M) ∣ M \in Sat (f_{base}^{com} (ϵ, E, F, α))} = {S \in com (F) ∣ \neg \exists S^{'} \in ϵ : S \subseteq S^{'}}; \\ {e (M) ∣ M \in Sat (f_{\max}^{com} (ϵ, E, F, α))} = {S \in com (F) ∣ e (E) \subset S} . \end{array}$

In words, the models of the formula $f_{base}^{com} (ϵ, E, F, α)$ represent the complete extensions of F such that no superset is contained in ϵ. Moreover, the models of $f_{\max}^{com} (ϵ, E, F, α)$ represent the complete extensions of F strictly extending the extension represented by E. Hence, these are the formulas that are handed to a SAT solver in PrefSat in order to solve the necessary subprocedures.

We remark that α is not relevant for enumeration of extensions and only used for acceptance later on. In the interest of uniformity we keep it as parameter of the functions throughout the paper. Recall that in a state ${(ϵ, E^{'}, E)}_{i}$ the set ϵ represents preferred extensions found as of now, $E^{'}$ is a record for the complete extension found in the previous oracle run and E is a record for the complete extension that the current oracle is trying to build. The annotation $i \in {base, \max}$ corresponds to different kinds of SAT calls.

As the oracle rules with annotation $i \in {base, \max}$ coincide with the ones of ${DP}_{φ}$ (cf. Fig. 2), their role is to search for a satisfying assignment of $f_{i}^{com}$ . That is, if a ${Fail}_{i}$ rule is applied to the state ${(ϵ, E^{'}, E)}_{i}$ for i, the formula $f_{i}^{com} (ϵ, E^{'}, F, α)$ is unsatisfiable. Conversely, when a ${Succeed}_{i}$ rule is applied from that state, the formula $f_{i}^{com} (ϵ, E^{'}, F, α)$ is satisfied by E. Notice that ${Fail}_{i}$ and ${Succeed}_{i}$ might shift i to reflect a change of type of SAT calls. When $i = base$ , the oracle searches for a complete extension that is not contained in a preferred extension that has been found before. In case of failure all the preferred extensions have been found. In case of success, it is necessary to search whether there are strictly larger complete extensions than the one found. This is handled by the computation within states annotated by $\max$ . In case of success, ${Succeed}_{\max}$ is applied and the procedure is repeated, since the current complete extension might still not be maximal. Failure by ${Fail}_{\max}$ means we have found a preferred extension.

Example 4.

Again consider the AF F depicted in Fig. 1. We have seen in Example 1 that F has two preferred extensions, namely ${a, c}$ and ${a, d}$ . Figure 5 shows a possible path in the graph ${E NUM}_{\overline{f}}^{F}$ . As expected, the computation terminates in the state $Ok ({{a, d}, {a, c}})$ . Note that we abbreviate the parts of the path where we are “inside” the SAT-solver. Also, we only show literals over arguments of F, and do not state the extra literals that may have been assigned during the call to the SAT-solver. Recall that by $unsat$ we represent an inconsistent and decision-free record.

Fig. 5.

Path in ${E NUM}_{\overline{f}}^{F}$ where F is the AF from Fig. 1.

It remains to show correctness of ${E NUM}_{\overline{f}}^{F}$ by showing that we reach a terminal state containing all preferred extensions of F. First observe that the oracle rules are exactly taken from ${DP}_{φ}$ of Fig. 2, working on the third element of the state-triple. Moreover, this working record is always initialized with ∅ when a transition rule outside the oracle rules is applied. Therefore, we can immediately follow from Theorem 2.1:

Lemma 3.1.

For any AF F and $i \in {base, \max}$ , if ${Succeed}_{i}$ is applied from state ${(ϵ, E^{'}, E)}_{i}$ in the graph ${E NUM}_{(f_{base}^{com}, f_{\max}^{com})}^{F}$ then $E \in Sat (f_{i}^{com} (ϵ, E^{'}, F, α))$ ; if ${Fail}_{i}$ is applied then $f_{i}^{com} (ϵ, E^{'}, F, α)$ is unsatisfiable.

We continue with a lemma stating that only preferred extensions which have not been found at this point are added to ϵ.

Lemma 3.2.

For any AF F, if the rule ${Fail}_{\max}$ is applied from state ${(ϵ, E^{'}, E)}_{\max}$ in the graph ${E NUM}_{(f_{base}^{com}, f_{\max}^{com})}^{F}$ then $e (E^{'}) \in prf (F)$ and $e (E^{'}) \notin ϵ$ .

Proof.

Let ${(ϵ_{1}, E_{1}^{'}, E_{1})}_{\max}$ be the state from which ${Fail}_{\max}$ is applied. This means, by Lemma 3.1, that $f_{\max}^{com} (ϵ_{1}, E_{1}^{'}, F, α)$ is unsatisfiable, hence, by the definition of formula $f_{\max}^{com}$ , there is no $S \in com (F)$ with $S \supset e (E_{1}^{'})$ . To get $e (E_{1}^{'}) \in prf (F)$ it remains to show that $e (E_{1}^{'}) \in com (F)$ . Observe that ${Succeed}_{base}$ is applied at least once, since every AF has a complete extension. Moreover, the value of $E_{1}^{'}$ is only updated by applications of ${Succeed}_{base}$ or ${Succeed}_{\max}$ . In both cases $e (E_{1}^{'})$ corresponds to a complete extension of F, due to the definitions of the formula $f_{base}^{com}$ or $f_{\max}^{com}$ , respectively, and Lemma 3.1. Therefore $e (E_{1}^{'})$ is a complete extension of F.

Since the initial state is ${(\emptyset, \emptyset, \emptyset)}_{base}$ , an application of ${Succeed}_{base}$ must precede ${Fail}_{\max}$ . From this application of ${Succeed}_{base}$ it follows from Lemma 3.1 that there is a record $E^{'}$ such that $\neg \exists S \in ϵ : e (E^{'}) \subseteq S$ . Moreover every application of ${Succeed}_{\max}$ updates $E^{'}$ by a proper superset of itself. Therefore $e (E_{1}^{'}) \supseteq e (E^{'})$ and also $\neg \exists S \in ϵ : e (E_{1}^{'}) \subseteq S$ , in particular $e (E_{1}^{'}) \notin ϵ$ . □

Now we are ready to show correctness of ${E NUM}_{\overline{f}}^{F}$ .

Theorem 3.3.

For any AF F, the graph ${E NUM}_{(f_{base}^{com}, f_{\max}^{com})}^{F}$ is finite, acyclic and the only terminal state reachable from the initial state is $Ok (ϵ)$ where $ϵ = prf (F)$ .

Proof.

In order to show that ${E NUM}_{\overline{f}}^{F}$ is finite, consider some state ${(ϵ, E^{'}, E)}_{i}$ of ${E NUM}_{\overline{f}}^{F}$ . Since both E and $E^{'}$ are records over $atoms (F)$ , and F is finite by definition, the number of possible records E and $E^{'}$ is finite. Similarly, there is only a finite number of sets of sets of arguments ϵ. Finally, ${E NUM}_{\overline{f}}^{F}$ only contains states with $i \in {base, \max}$ . Thus the number of states is finite in the graph ${E NUM}_{\overline{f}}^{F}$ .

In order to show that it is acyclic recall the strict partial order < on states from Definition 3. We show that each transition rule is increasing w.r.t. < by referring to the conditions (i) to (iv) from Definition 3. To this end consider two states $ς_{1} = {(ϵ_{1}, E_{1}^{'}, E_{1})}_{i_{1}}$ and $ς_{2} = {(ϵ_{2}, E_{2}^{'}, E_{2})}_{i_{2}}$ representing the states before and after the application of a rule. First of all, the i-oracle rules (i.e. ${Backtrack}_{i}$ , ${UnitPropagate}_{i}$ , and ${Decide}_{i}$ ) fulfill $ς_{1} < ς_{2}$ because of (iv). For all of these rules $ϵ_{1} = ϵ_{2}$ , $E_{1}^{'} = E_{2}^{'}$ and $i_{1} = i_{2}$ , but $s (E_{1})$ is lexicographically smaller than $s (E_{2})$ , therefore $E_{1} <_{E} E_{2}$ . Moreover, ${Fail}_{\max}$ fulfills $ς_{1} < ς_{2}$ due to (i) since $e (E_{1}^{'}) \notin ϵ_{1}$ by Lemma 3.2. ${Succeed}_{base}$ guarantees $ς_{1} < ς_{2}$ because of (ii). Finally, ${Succeed}_{\max}$ fulfills $ς_{1} < ς_{2}$ due to (iii), since the $\max$ -oracle rules work on the formula $f_{\max}^{com}$ and the extension associated with a satisfying assignment $E_{1} = E_{2}^{'}$ of that formula must be a proper superset of $e (E_{1}^{'})$ . Therefore, by transitivity of <, or any two states $ς_{1}$ and $ς_{n}$ such that $ς_{n}$ is reachable from $ς_{1}$ in ${E NUM}_{\overline{f}}^{F}$ it holds that $ς_{1} < ς_{n}$ , showing that the graph is acyclic.

The only terminal state reachable from the initial state is $Ok (ϵ)$ (via rule ${Fail}_{base}$ ) for some $ϵ \subseteq 2^{A}$ since all states ${(ϵ, E, E^{'})}_{i}$ of ${E NUM}_{\overline{f}}^{F}$ have $i \in {base, \max}$ and for each $i \in {base, \max}$ there is a rule ${Succeed}_{i}$ with the condition “no other rule applies”. It remains to show that, when state $Ok (ϵ)$ is reached, ϵ coincides with $prf (F)$ . Since elements are only added to ϵ by application of the rule ${Fail}_{\max}$ we know from Lemma 3.2 that for each $T \in ϵ$ it holds that $T \in prf (F)$ . To reach $Ok (ϵ)$ , the rule ${Fail}_{base}$ must have been applied from a state ${(ϵ, E^{'}, E)}_{base}$ . This means, by the definition of $f_{base}^{com}$ and Lemma 3.1, that for each complete extension S of F there is some $T \in ϵ$ such that $S \subseteq T$ . Hence $ϵ = prf (F)$ . □

3.2. SAT-based algorithm for acceptance

cegartix [25] is a SAT-based tool for deciding several acceptance questions for AFs. Here we focus on Algorithm 1 of [25] for deciding skeptical acceptance w.r.t. preferred semantics of an argument α. Similarly to PrefSat, cegartix traverses the search space of a certain semantics, generates candidate extensions not contained in already visited preferred extensions, and maximizes the candidate until a preferred extension is found. The main differences to PrefSat are (1) the parametrized use of base semantics σ (the search space), which can be either admissible or complete semantics, and (2) the incorporation of the queried argument α. To prune the search space, α must not be contained in the candidate σ-extension before maximization. Again, we have two kinds of SAT-calls.

The graph ${S KEPT - PRF}_{\overline{f}}^{F, α}$ for an AF F, an argument α and a vector of functions $\overline{f} = (f_{base}^{σ}, f_{\max}^{σ})$ is defined by the states over $atoms (F)$ and the rules in Fig. 4 replacing the rules ${Fail}_{i}$ for $i \in {base, \max}$ and adding the rules ${Fail}_{out}$ and ${Succeed}_{out}$ as depicted in Fig. 6. The initial state is ${(\emptyset, \emptyset, \emptyset)}_{base}$ . For $σ \in {adm, com}$ we assume the functions $f_{base}^{σ}$ and $f_{\max}^{σ}$ such that: $\begin{array}{l} {e (M) ∣ M \in Sat (f_{base}^{σ} (ϵ, E, F, α))} = {S \in σ (F) ∣ α \notin S \land \neg \exists S^{'} \in ϵ : S \subseteq S^{'}}; \\ {e (M) ∣ M \in Sat (f_{\max}^{σ} (ϵ, E, F, α))} = {S \in σ (F) ∣ e (E) \subset S} . \end{array}$

Fig. 6.

Changed transition rules for ${S KEPT - PRF}_{\overline{f}}^{F, α}$ .

The graph ${S KEPT - PRF}_{\overline{f}}^{F, α}$ is similar to ${E NUM}_{\overline{f}}^{F}$ . Again, the models of the formulas $f_{base}^{com} (ϵ, E, F, α)$ and $f_{\max}^{com} (ϵ, E, F, α)$ represent the complete extensions of F which are not contained in any element of ϵ and extending the extension represented by E, respectively. In addition, the query argument α is required not to be contained in the extensions represented by the models of $f_{base}^{com} (ϵ, E, F, α)$ . The graph differs in case of failure in a state annotated by $base$ or $\max$ . When all the preferred extensions have been enumerated, i.e. the $base$ -oracle ends with an application of ${Fail}_{base}$ , we can report a positive outcome with $Accept$ , since we have ensured that α belongs to all of them. If we arrive at ${Fail}_{\max}$ , i.e. when a preferred extension has been found, it is necessary to check whether α belongs to it, and this is done via rules ${Succeed}_{out}$ and ${Fail}_{out}$ that either lead to $Reject$ or give the control to the $base$ level.

Example 5.

Again consider the AF F from Fig. 1 and note that skeptical acceptance of argument c is rejected as c is not contained in the preferred extension ${a, d}$ of F. Accordingly, the possible path of the graph ${S KEPT - PRF}_{\overline{f}}^{F, c}$ which is depicted in Fig. 7 (with base semantics $adm$ ) terminates in the $Reject$ -state.

On the other hand, argument a is skeptically accepted w.r.t. preferred semantics in F as it belongs to all preferred extensions enumerated in ${{a, d}, {a, c}}$ . For checking whether a is skeptically accepted in F, a possible path in the graph ${S KEPT - PRF}_{\overline{f}}^{F, a}$ (again with base semantics $adm$ ) is shown in Fig. 8. As expected, the path terminates in the state $Accept$ .

Fig. 7.

Reject-path for argument c in ${S KEPT - PRF}_{\overline{f}}^{F, c}$ .

Fig. 8.

Accept-path for argument a in ${S KEPT - PRF}_{\overline{f}}^{F, a}$ .

Again, we get the following from Theorem 2.1:

Lemma 3.4.

For any AF $F = (A, R)$ , argument $α \in A$ , $σ \in {adm, com}$ , and $i \in {base, \max}$ , if ${Succeed}_{i}$ is applied from state ${(ϵ, E^{'}, E)}_{i}$ in the graph ${S KEPT - PRF}_{\overline{f}}^{F, α}$ then $E \in Sat (f_{i}^{σ} (ϵ, E^{'}, F, α))$ ; if ${Fail}_{i}$ is applied then $f_{i}^{σ} (ϵ, E^{'}, F, α)$ is unsatisfiable.

The proof of the following results is almost identical to the ones of Lemma 3.2 and Theorem 3.3 and can be found in the Appendix.

Lemma 3.5.

For any AF F, if the rule ${Fail}_{out}$ is applied from state ${(ϵ, E^{'}, E)}_{out}$ in the graph ${S KEPT - PRF}_{(f_{base}^{σ}, f_{\max}^{σ})}^{F, α}$ with $σ \in {adm, com}$ then $e (E^{'}) \in prf (F)$ and $e (E^{'}) \notin ϵ$ .

Theorem 3.6.

For any AF $F = (A, R)$ , argument $α \in A$ , and $σ \in {adm, com}$ , the graph ${S KEPT - PRF}_{(f_{base}^{σ}, f_{\max}^{σ})}^{F, α}$ is finite, acyclic and any terminal state reachable from the initial state is either $Accept$ or $Reject$ ; $Reject$ is reachable iff α is not skeptically accepted in F w.r.t. $prf$ .

Finally note that from Theorem 3.6 it follows that $Accept$ is reachable from the initial state if and only if α is skeptically accepted by F, which completes the correctness statement for ${S KEPT - PRF}_{\overline{f}}^{F, α}$ .

3.3. Dedicated approach for enumeration

Algorithm 1 of [45] presents a direct approach for enumerating preferred extensions. One function is important for this algorithm, which is called IN-TRANS. Given an AF $F = (A, R)$ , it marks an argument $a \in A$ as belonging to the currently built extension, and marks all attackers ${b ∣ (b, a) \in R}$ and all attacked arguments ${b ∣ (a, b) \in R}$ as outside of this extension. Intuitively, IN-TRANS decides to accept a, and then propagates the immediate consequences to the neighboring nodes. It actually does an additional task. It labels the attacked arguments as “attacked”, and the attackers that are not yet labelled as attacked as “to be attacked”: this allows later to easily check the admissibility of the extension by just looking whether there is any argument “to be attacked”.

The algorithm is recursive, and stores the admissible extensions in a global variable. First, it checks whether all the arguments are marked as either belonging to or being outside the extension, and if so it returns after adding the extension to the global variable if the extension is actually admissible. Second, it applies the function IN-TRANS to some unmarked argument and calls itself recursively. Third, it reverts the effects of IN-TRANS, marks the argument it chose as outside of this extension, and calls itself recursively.

We have defined an equivalent representation of this algorithm that follows the framework of abstract solvers with binary logics as previously used in this article. Binary truth values are sufficient to represent the arguments marked, but we see the labels “attacked” and “to be attacked” as an optimization as they can be easily recovered at the end of the algorithm. Indeed, they correspond to the condition “there is an argument a such that $e (E)$ does not attack a and a attacks $e (E)$ ” of the rule ${Fail}_{out}$ .

Fig. 9.

The rules of the graph ${D IRECT}^{F}$ .

The graph ${D IRECT}^{F}$ for an AF F is defined by the states over $atoms (F)$ and the transition rules presented in Fig. 9. Its initial state is ${(\emptyset, \emptyset, \emptyset)}_{\max}$ . The structure of the graph is similar to that of ${E NUM}_{\overline{f}}^{F}$ . It differs from this graph in two ways. First, it has only one lower level of computation. Second, the rules of the oracle differ from the previous oracle rules since they are not a call to a SAT solver; we primed them to emphasize the difference.

More precisely, among the oracle rules, propagation (through ${Propagate}_{\max}^{'}$ rule) now only occurs so as to negatively add an atom if it attacks or is attacked by an atom of the extension being built. The ${Decide}_{\max}^{'}$ rule only adds atoms positively, which is useful in Algorithm 2 of [45] as it ensures maximality of final assignments. When a record assigning all arguments is found, the rule ${Succeed}_{\max}$ is applied so as to allow the test of the outer rules to be carried on. Differently to the algorithms presented so far, the extension associated to this record is only guaranteed to be conflict-free at this point and not admissible (or complete, depending on the chosen base semantics). When the record corresponds to a preferred extension, it is stored through ${Succeed}_{out}$ , and the process continues. In both ${Succeed}_{out}$ and ${Fail}_{out}$ , the use of one of the rules ${Backtrack}_{\max}^{'}$ or ${Fail}_{\max}$ is forced by making the record inconsistent. This way the process of browsing records is forced to continue.

A final comment is related to one of the main advantages of using abstract solvers, i.e. the fact that they allow to highlight in a more clear way similarities and differences among solving algorithms, as mentioned in Section 1. It is evident that our reformulation of the direct approach has allowed to present this algorithm by modification of the previous two solving procedures, by explicitly viewing it in the light of a backtrack-search process in a search space, more similar to a SAT-based procedure. This would not be obvious by considering, e.g. the pseudo-code description of the direct approach.

Example 6.

A possible path in the graph ${D IRECT}^{F}$ for the AF F in Fig. 1 is shown in Fig. 10. One difference can be seen by the fact that the result of the modified oracle rules may be contained in an already found preferred extension. Then ⊥ is added to the current record by ${Fail}_{out}$ , followed by backtracking to the last decision literal, if any. Moreover note that in Fig. 10 we explicitly write the state transitions due to modified oracle rules, in order to emphasize the difference to the SAT oracle rules used in the previous graphs.

Fig. 10.

Path in ${D IRECT}^{F}$ where F is the AF from Fig. 1.

We give the correctness statement of the abstract solver representing the direct approach after providing an intermediate lemma; proofs can again be found in the Appendix.

Lemma 3.7.

For any AF F, if the rule ${Succeed}_{out}$ is applied from state ${(ϵ, \emptyset, E)}_{out}$ in the graph ${D IRECT}^{F}$ then $e (E) \in prf (F)$ and $e (E) \notin ϵ$ .

Theorem 3.8.

For any AF F, the graph ${D IRECT}^{F}$ is finite, acyclic and the only terminal state reachable from its initial state is $Ok (ϵ)$ where $ϵ = prf (F)$ .

3.4. Combining algorithms

We now use the insights gained by the graph representations of the algorithms from the literature to define a new algorithm for skeptical acceptance w.r.t. preferred semantics. We do so by defining a new abstract solver which incorporates the modified dpll (cf. Section 2.3) into the graph representation of cegartix (cf. Section 3.2). This gives rise to a new algorithm which is not only of theoretical interest, but also leads to a more efficient solving procedure, as we will show in Section 4.

Now recall that, in PrefSat and cegartix, the two SAT calls annotated with $i \in {base, \max}$ basically amount to finding a maximal satisfying assignment, i.e. a preferred extension. This is done by iteratively extending the satisfying assignment found by the SAT call annotated with $base$ (which must not contain the queried argument), by means of a series of further SAT calls annotated with $\max$ .

But, given our result in Section 2.3, the “inner loop” of SAT calls for maximization is not strictly needed, and the two types of SAT calls can be substituted by a single modified call. More specifically, we replace $base$ by ${base}^{'}$ by abstaining from the condition that the queried argument must not be contained in the σ-extension. Hence, a single modified SAT call to ${base}^{'}$ returns a preferred extension which has not been found already.

Given an AF F, an argument α and a base semantics $σ \in {adm, com}$ , the graph ${MIX - PRF}_{f_{{base}^{'}}^{σ}}^{F, α}$ representing the new algorithm for deciding skeptical acceptance of α in F w.r.t. $prf$ is defined by the states of $atoms (F)$ and the transition rules presented in Fig. 11. Its initial state is ${(\emptyset, \emptyset, \emptyset)}_{{base}^{'}}$ . As we can see, the graph describes exactly the intuition behind the new proposal. A new label ${base}^{'}$ is employed to clearly differentiate with the other two-level architectures. Of course, in order to guarantee that the outcome of the modified SAT call is a preferred extension, we must assume the function $f_{{base}^{'}}^{σ} (ϵ, E, F, α)$ such that: $\begin{array}{l} {e (M) ∣ M \in Sat (f_{{base}^{'}}^{σ} (ϵ, E, F, α))} = {S \in σ (F) ∣ \neg \exists S^{'} \in ϵ : S \subseteq S^{'}} . \end{array}$

Then, the outcome of the ${base}^{'}$ rules is treated similarly, through the $out$ rules, to the graph ${S KEPT - PRF}_{\overline{f}}^{F, α}$ presented in Section 3.2.

Fig. 11.

The rules of ${MIX - PRF}_{\overline{f}}^{F, α}$ .

Considering the fact that the new solution always adds positive atoms to the current assignment, it looks similar to the direct approach; but there is a notable difference between the new algorithm and the direct approach. The outcome of the oracle-rules of the direct approach (cf. Fig. 9) is a conflict-free set which is not necessarily maximal (and in other rules admissibility and maximality is checked), whereas the outcome of the oracle-rules in the new algorithm modifying ${S KEPT - PRF}_{\overline{f}}^{F, α}$ is guaranteed to be an admissible (and preferred) set.

From Theorem 2.2 we know that the ${base}^{'}$ -oracle rules give a maximal satisfying assignment of $f_{{base}^{'}}^{σ} (ϵ, E^{'}, F, α)$ :

Lemma 3.9.

For any AF $F = (A, R)$ , argument $α \in A$ , and $σ \in {adm, com}$ , if ${Succeed}_{{base}^{'}}$ is applied from state ${(ϵ, E^{'}, E)}_{{base}^{'}}$ in the graph ${MIX - PRF}_{f_{{base}^{'}}^{σ}}^{F, α}$ then $E \in Sat (f_{{base}^{'}}^{σ} (ϵ, E^{'}, F, α))$ and $\neg \exists M \in Sat (f_{\max}^{σ} (ϵ, E^{'}, F, α))$ with $M \supset E$ ; if ${Fail}_{{base}^{'}}$ is applied then $f_{{base}^{'}}^{σ} (ϵ, E^{'}, F, α)$ is unsatisfiable.

To be sure that maximal satisfying assignments correspond to preferred extensions, it has to hold that the atoms occurring in $f_{{base}^{'}}^{σ}$ which do not correspond to arguments of the AF do not affect maximality. To this end we make the following assumption.

Assumption 1.

Given an AF $F = (A, R)$ , a set of sets of arguments ϵ, a record E relative to $atoms (F)$ , and an argument $α \in A$ , for each $M_{1}, M_{2} \in Sat (f_{base}^{σ} (ϵ, E, F, α))$ , where $σ \in {adm, com}$ , it holds that $M_{1} \subseteq M_{2}$ iff $e (M_{1}) \subseteq e (M_{2})$ .

It is important to note that the concrete formulas used in cegartix fulfill Assumption 1. Taking the assumption for granted in the rest of the paper, we are able to show correctness of the abstract solver representing the combined approach.

Lemma 3.10.

For any AF F, if the rule ${Fail}_{out}$ is applied from state ${(ϵ, E^{'}, E)}_{out}$ in the graph ${MIX - PRF}_{f_{{base}^{'}}^{σ}}^{F, α}$ with $σ \in {adm, com}$ then $e (E^{'}) \in prf (F)$ and $e (E^{'}) \notin ϵ$ .

Theorem 3.11.

For any AF $F = (A, R)$ , argument $α \in A$ , and $σ \in {adm, com}$ , the graph ${MIX - PRF}_{f_{{base}^{'}}^{σ}}^{F, α}$ is finite, acyclic and any terminal state reachable from the initial state is either $Accept$ or $Reject$ ; $Reject$ is reachable iff α is not skeptically accepted in F w.r.t. $prf$ .

Proof.

(1) ${MIX - PRF}_{f_{{base}^{'}}^{σ}}^{F, α}$ is finite and acyclic: Finiteness follows in the same way as in Theorem 3.3. In order to show acyclicity we show that each transition rule is increasing w.r.t. the strict partial order < from Definition 3 (with $base$ replaced by ${base}^{'}$ ). Consider two states $ς_{1} = {(ϵ_{1}, E_{1}^{'}, E_{1})}_{i_{1}}$ and $ς_{2} = {(ϵ_{2}, E_{2}^{'}, E_{2})}_{i_{2}}$ representing the states before and after the application of a rule. First of all, the ${base}^{'}$ -oracle rules (i.e. ${Backtrack}_{{base}^{'}}$ , ${UnitPropagate}_{{base}^{'}}$ , and ${Decide}_{{base}^{'}}^{≺}$ ) fulfill $ς_{1} < ς_{2}$ because of (iv). For all of these rules $ϵ_{1} = ϵ_{2}$ , $E_{1}^{'} = E_{2}^{'}$ and $i_{1} = i_{2}$ , but $s (E_{1})$ is lexicographically smaller than $s (E_{2})$ , therefore $E_{1} <_{E} E_{2}$ . Moreover, ${Fail}_{out}$ fulfills $ς_{1} < ς_{2}$ due to (i) since $e (E_{1}^{'}) \notin ϵ_{1}$ by Lemma 3.10. ${Succeed}_{base}$ guarantees $ς_{1} < ς_{2}$ because of (ii). Finally, ${Succeed}_{{base}^{'}}$ fulfills $ς_{1} < ς_{2}$ due to (ii), since $base <_{i} out$ , and ${Succeed}_{out}$ and ${Fail}_{{base}^{'}}$ result in terminal states. Therefore, by transitivity of <, or any two states $ς_{1}$ and $ς_{n}$ such that $ς_{n}$ is reachable from $ς_{1}$ in ${E NUM}_{\overline{f}}^{F}$ it holds that $ς_{1} < ς_{n}$ , showing that the graph is acyclic.

(2) Any terminal state of ${MIX - PRF}_{f_{{base}^{'}}^{σ}}^{F, α}$ reachable from the initial state is either $Reject$ or $Accept$ : This is immediate by the existence of the rule ${Succeed}_{{base}^{'}}$ with condition “no other rule applied” and the fact that the rules ${Fail}_{out}$ and ${Succeed}_{out}$ are complete in the sense that if one rule does not apply the other rule applies and vice versa.

(3) $Reject$ is reachable from the initial state iff α is not skeptically accepted by F w.r.t. $prf$ .

Assume $Reject$ is reachable. Hence also ${(ϵ, E^{'}, E)}_{out}$ with $α \notin e (E^{'})$ is reachable. Moreover ${Succeed}_{{base}^{'}}$ was applied at a state ${(ϵ, E^{″}, E^{'})}_{{base}^{'}}$ , meaning, by Lemma 3.9, that $E^{'} \in Sat (f_{{base}^{'}}^{σ} (ϵ, E^{″}, F, α))$ and $\neg \exists E^{‴} \in Sat (f_{\max}^{σ} (ϵ, E^{″}, F, α))$ with $E^{‴} \supset E^{'}$ . Taking into account Assumption 1 this means, by the definition of $f_{{base}^{'}}^{σ}$ , that $e (E^{'})$ is a ⊆-maximal σ-extension, i.e. a preferred extension. Since $α \notin e (E^{'})$ we get that α is not skeptically accepted.

Assume α is not skeptically accepted by F w.r.t. $prf$ . Hence there is some $T \in prf (F)$ with $α \notin T$ . Now assume, towards a contradiction, that $Reject$ is not reachable. This means by (1) and (2), that $Accept$ is reachable. Hence ${Fail}_{{base}^{'}}$ is applicable from a state ${(ϵ, E^{'}, E)}_{{base}^{'}}$ . By the definition of $f_{{base}^{'}}^{σ}$ and Lemma 3.9, this means that there is no σ-extension S of F such that $\neg \exists S^{'} \in ϵ : S \subseteq S^{'}$ . Now note that ${Fail}_{out}$ is the only rule where elements are added to ϵ. Moreover, by Lemma 3.10, we know that elements added are preferred extensions of F. But therefore for each $S \in σ (F)$ it holds that $\exists T \in prf (F) : S \subseteq T \land α \in T$ , a contradiction. □

Again it is important to note that from Theorem 3.11 it follows that $Accept$ is reachable from the initial state if and only if α is skeptically accepted by F, which completes the correctness statement for ${MIX - PRF}_{f_{{base}^{'}}^{σ}}^{F, α}$ .

Fig. 12.

Reject-path for argument c in ${MIX - PRF}_{f_{{base}^{'}}^{σ}}^{F, c}$ .

Fig. 13.

Accept-path for argument a in ${MIX - PRF}_{f_{{base}^{'}}^{σ}}^{F, a}$ .

Example 7.

For the AF F from Fig. 1, a possible path in ${MIX - PRF}_{f_{{base}^{'}}^{σ}}^{F, c}$ is depicted in Fig. 12. It correctly results in $Reject$ , as c is not skeptically accepted in F w.r.t. $prf$ . Figure 13, on the other hand, shows a possible path in ${MIX - PRF}_{f_{{base}^{'}}^{σ}}^{F, a}$ . Note that both paths are shorter than the ones of ${S KEPT - PRF}_{\overline{f}}^{F, α}$ in Figs 7 and 8, respectively.

Of course, in principle it is not clear whether the new abstract solution leads to computational advantages (see, e.g. [30,31] for a related discussion); however, the experimental analysis in Section 4 shows that this is the case.

4. Experiments

In order to test the viability of our proposed combination as introduced in Section 3.4, we have implemented an alternative version of cegartix following the new approach. The choice of cegartix is motivated by the fact that it has been one of the best AF solvers in both editions of the argumentation competition (http://argumentationcompetition.org). In particular, in the reasoning task of interest (skeptical acceptance under preferred semantics as in Section 3.2), cegartix was 2nd out of 11 solvers entering the track in the first competition, and highly competitive also in the second event.3

³
Comparisons of the performance of cegartix and other solvers can be found in [18,50].

4.1. Implementation

The main change done in cegartix was thus replacing the two inner SAT calls with a single call to a SAT solver with modified heuristics, and we obtained this by changing the internal heuristics of the clasp solver used by cegartix in the 2015 competition. clasp [29] is an ASP solver, but can act also as SAT solver with excellent results as shown in past SAT competitions, starting from 2009 to the most recent editions (see, e.g. http://www.satcompetition.org/). Moreover, for efficiency reasons, the implementation of cegartix slightly differs from the algorithm in Section 3.2, given that the condition $α \notin S$ is conjunctively added to $e (E) \subset S$ for $f_{\max}^{σ} (ϵ, E, F, α)$ , with the idea of guiding the search through counterexamples. Consequently, for comparing the two alternatives on the same implementation basis, the same is done for $f_{{base}^{'}}^{σ} (ϵ, E, F, α)$ .

The variants of cegartix considered in our experiments are:

ceg: version with com as a base semantics, which was the setting employed in both editions of the competition. Past experiments ([25], on different benchmark graphs) overall showed similar or better performance of this version compared to that with adm as a base semantics.

ceg+-com: new version implementing the combination in Section 3.4 with com as a base semantics.

ceg+-adm: new version implementing the combination in Section 3.4 with adm as a base semantics.

In our experiments, these three variants of cegartix were run with the same parameters.

The version of cegartix entering the competition included shortcuts, i.e. specific conditions that can lead the solver to find solutions earlier, before entering the main solving algorithm. Details for shortcuts will be presented in the next section. For this analysis, given the main goal is to test the new solution which applies to the core part of the algorithm and shortcuts could obfuscate the differences between algorithms, shortcuts have been disabled. Note, however, that the new variants can make use of the very same shortcuts. Therefore, it has to be noted that final implementations of the respective algorithms might show smaller gaps in performance, since they will all use the same shortcuts in the first place.

4.2. Benchmarks

For benchmarks, i.e., instances comprising of an AF and an argument for which one has to check skeptical acceptance under preferred semantics, we considered the following three benchmark sets4

⁴
Archives of the benchmark sets can be found at http://argumentationcompetition.org/2015/iccma2015_benchmarks.zip, http://www.dbai.tuwien.ac.at/iccma17/benchmarks/A.tar.gz, and http://www.dbai.tuwien.ac.at/research/project/argumentation/cegartix/files/clima.zip.

ICCMA’15: These are 192 AFs with three arguments to be queried for, from the competition in the year 2015 [50]. After cleaning this dataset from trivial queries (queried arguments not among the set of arguments in the AF), this resulted in 537 instances.

ICCMA’17: In this dataset, from the competition in the year 2017 [27], we have 300 AFs, divided into four categories (according to expected difficulty), which were used to compare solvers for the task of checking skeptical acceptance under preferred semantics (this set is called set “A” in the competition). The hardest category has two arguments to be queried for per AF, while all other three categories have one query argument. This results in 350 instances.

CLIMA: This is a set of AFs from our earlier work [53], which we included since it comprises of several AFs that were hard to solve by an earlier version of cegartix. Here we have 320 AFs and one query argument per AF. The AFs $F = (A, R)$ were created as randomly generated digraphs, with a fixed set of arguments $A \in {100, 150, 200, 225, 250, 300, 325, 350}$ and a probability to include an attack $(a, b)$ for each $a, b \in A$ with probability $p \in {0.1, 0.2, 0.3, 0.4}$ . For each parameter choice 10 AFs were created.

For each of the three benchmark sets, the AFs were given in the original dataset, while the arguments to be queried for were only given for ICCMA’15 and ICCMA’17. For the set CLIMA, we chose one argument in the AF to query at random, with uniform probability for each argument. Overall, this resulted in 1207 instances (AF and query).

4.3. Results

Experiments have been run on an AMD Opteron Processor 6308 3.5 GHz with 2 processors with each 2 physical cores; every of these cores puts at disposal 2 logical cores, for a sum of 192 GB ( $12 \times 16$ GB) of RAM. In our experiments we set a per-instance timeout of 600 sec.

We first show general runtime statistics in Table 1. More concretely, the table depicts median runtimes over the considered benchmark sets, as well as timeouts encountered in the runs. The last two columns list the number of instances that were uniquely solved by ceg or by the union of solved instances of ceg+-com and ceg+-adm, i.e., whether the original approach or the new approaches could contribute to uniquely solved instances.

Table 1
General runtime statistics from experiments

Median runtime Timeouts Uniquely solved

Benchmark ceg ceg+-com ceg+-adm ceg ceg+-com ceg+-adm by ceg by ceg+-com or ceg+-adm

All 1.01 1.14 1.28 57 61 71 6 11

ICCMA’15 0.77 0.93 0.76 0 0 0 0 0

ICCMA’17 9.75 7.96 23.30 45 47 60 5 8

CLIMA 1.04 1.1 0.99 12 14 11 1 3

	Median runtime	Timeouts	Uniquely solved
All	1.01	1.14	1.28	57	61	71	6	11
ICCMA’15	0.77	0.93	0.76	0	0	0	0	0
ICCMA’17	9.75	7.96	23.30	45	47	60	5	8
CLIMA	1.04	1.1	0.99	12	14	11	1	3

This table indicates that, regarding median runtime and timeouts, the new approaches generally do not fare (much) better than the original version of cegartix. In fact, median runtimes and timeouts overall increased when comparing new and original approaches, except for median running time of ceg+-com on benchmark ICCMA’17 and, to a small extent, ceg+-adm on benchmark CLIMA. A further observation is that the instances from benchmark ICCMA’15 are rather easy to solve.

Nevertheless, the uniquely solved instances indicate differences of the approaches w.r.t. runtime performance. Looking closer at these uniquely solved instances, when ceg+-com or ceg+-adm could solve an instance within the timeout limit and ceg could not, it was always the case that ceg+-adm solved the instance, while this was only sometimes the case for ceg+-com. That is, ceg+-adm contributes to all of the uniquely solved instances, while ceg+-com only to five of the eleven instances.

We next illustrate, via Fig. 14, the different runtime behaviors of the three cegartix implementations via scatter plots. In Fig. 14(a), the scatter plot between ceg and ceg+-adm is shown, while in Fig. 14(b), ceg is compared to ceg+-com and, finally, in Fig. 14(c), the scatter plot of the two new solvers is shown. Such plots show the running time of two solvers (on x and y axes) on each individual instance. A runtime directly on the diagonal implies the same runtime for both solvers on that instance.

Closer inspection of the figures suggests that the solver ceg and the two solvers ceg+-com and ceg+-adm are rather complementary in their runtime behavior on many (non-easy) instances. That is, apart from the uniquely solved instances (these are the ones on the “timeout” lines for one of the solvers), also several further instances showed different runtime behavior: in both Fig. 14(a) and Fig. 14(b) several instances can be seen below or above the diagonal.

Fig. 14.

Scatter plots of our experimental analysis. Black circles indicate instances with an AF that has an empty grounded extension, while a red cross indicates a non-empty grounded extension.

We hypothesize that a reason for the different runtimes, for original ceg and novel ceg+-com and ceg+-adm, stems from difficulties of ceg to find non-trivial (i.e., non-empty) admissible sets. To investigate towards this end, we have marked each instance of each scatter plot, in Figs 14(a)–(c), whether the corresponding AF has a non-empty grounded extension or not. When an AF has an empty grounded extension the corresponding symbol in the figure is a black circle, otherwise a red cross. An AF having a non-empty grounded extension can be seen as a kind of approximation of whether one can (easily) find a non-trivial admissible set. In Fig. 14(a) and Fig. 14(b), this categorization of the instances is, to some extent, reflected in the runtimes: many times when a novel solver outperformed ceg it is the case when the grounded extension is empty. When looking at Fig. 14(c), comparing running times of ceg+-com and ceg+-adm, the results suggest that on AFs with an empty grounded extension, ceg+-adm tends to be better w.r.t. running time, yet on AFs with a non-empty grounded extension, many instances, on that figure, are either in the diagonal or, in fact, trivial for ceg+-com, but not for ceg+-adm.

Although further research is needed, the characteristic of an AF having a (non-)empty grounded extension gives an indicator whether ceg or ceg+-com and ceg+-adm might be better to use for solving. This insight can be used, for instance, when compiling an algorithm selection for cegartix, in line with techniques studied in [15], to first compute the grounded extension, and then choose which heuristic to apply.

5. Extensions to the framework

In Section 3 we have analyzed three prominent algorithms from the literature dealing with preferred semantics. In this section we show that the modularity of the abstract solver approach allows us to give the graph representation of related algorithms with little effort. First, we abstract the algorithms from [25] deciding skeptical (resp. credulous) acceptance w.r.t. other, namely stage [52] and semi-stable [11], semantics, and then we exemplify how to incorporate shortcuts into the graph-representations for the algorithms of the same paper.

5.1. Core algorithms for semi-stable and stage semantics

Other semantics involving reasoning tasks lying in the second level of the polynomial hierarchy are stage and semi-stable (cf. Table 2). Their definitions make use of the concept of the range of a set of arguments $S \subseteq A$ in an AF $F = (A, R)$ , defined as $S_{F}^{+} = S \cup {a \in A ∣ \exists b \in S : (b, a) \in R}$ , i.e. S together with all arguments it attacks. Stage ( $stg$ ) and semi-stable ( $sem$ ) semantics are then defined as follows:

Definition 4.
Given an AF F,
$S \in stg (F)$ , if $S \in cf (F)$ and there is no $T \in cf (F)$ such that $T_{F}^{+} \supset S_{F}^{+}$ ;

$S \in sem (F)$ , if $S \in adm (F)$ and there is no $T \in adm (F)$ such that $T_{F}^{+} \supset S_{F}^{+}$ , or equivalently,

$S \in sem (F)$ , if $S \in com (F)$ and there is no $T \in com (F)$ such that $T_{F}^{+} \supset S_{F}^{+}$ .

Table 2
Complexity of decision problems for AFs

σ $Cre d_{σ}$ $Skep t_{σ}$

$prf$ $NP$ -c $Π_{2}^{P}$ -c

$sem$ $Σ_{2}^{P}$ -c $Π_{2}^{P}$ -c

$stg$ $Σ_{2}^{P}$ -c $Π_{2}^{P}$ -c

For semi-stable semantics the possible base semantics coincide with the ones for preferred semantics, that is admissible and complete, while stage semantics (yielding range-maximal conflict-free sets) uses conflict-free as base semantics. In other words, for the pairs $(σ, θ) \in {(adm, sem), (com, sem), (cf, stg)}$ , a uniform characterization of θ is as follows: Given an AF F, $S \in θ (F)$ iff $S \in σ (F)$ and there is no $T \in σ (F)$ such that $T_{F}^{+} \supset S_{F}^{+}$ .

Algorithms for skeptical (resp. credulous) acceptance w.r.t. these semantics are presented in Algorithms 2 and 3 of [25] by adaptation of the algorithm for skeptical acceptance w.r.t. preferred semantics described in Section 3.2. Similar to the algorithm for preferred semantics, the general skeptical acceptance procedure for semantics θ and base semantics σ first makes use of two SAT oracles to find a range-maximal σ-extension. The main difference to the algorithm for preferred semantics is that the maximization is concerned with the range of extensions instead of the extensions themselves. Moreover, since there can be different σ-extensions with the same range, another oracle has to be consulted in order to check whether there is a σ-extension with a range equal to the maximal one found before, which does not contain the queried argument. If such an extension exists, the algorithm returns with a negative answer to the skeptical acceptance problem w.r.t. θ. For credulous acceptance, the algorithm returns with a positive answer if the oracle call finds such a σ-extension which does contain the queried argument.

The graph $S KEPT - θ_{\overline{f}}^{F, α}$ for a semantics $θ \in {sem, stg}$ , an AF F, and argument α, and a vector of functions $\overline{f}$ is defined by states over $atoms (F)$ and the transition rules of ${S KEPT - PRF}_{\overline{f}}^{F, α}$ (Figs 4 and 6) with additional oracle rules for index $out$ (i.e. we have $i \in {base, \max, out}$ for ${Backtrack}_{i}$ , ${UnitPropagate}_{i}$ , and ${Decide}_{i}$ now) and the rules ${Fail}_{out}$ and ${Succeed}_{out}$ changed according to Fig. 15. In contrast to the graphs presented so far, ϵ now contains the ranges of the extensions already found. Moreover, the decision whether to add the range of the current extension and continue the search or to reject the given instance is based on another set of oracle rules – the ones indexed by $out$ .

Fig. 15.
The transition rules of the graph $S KEPT - θ_{\overline{f}}^{F, α}$ that differ from ${S KEPT - PRF}_{\overline{f}}^{F, α}$ .

The initial state of $S KEPT - θ_{\overline{f}}^{F, α}$ is ${(\emptyset, \emptyset, \emptyset)}_{base}$ . For $σ \in {adm, com, cf}$ we assume functions $f_{base}^{σ}$ , $f_{\max}^{σ}$ and $f_{out}^{σ}$ such that: $\begin{array}{l} {e (M) ∣ M \in Sat (f_{base}^{σ} (ϵ, E, F, α))} = {S \in σ (F) ∣ α \notin S \land \neg \exists S^{'} \in ϵ : S_{F}^{+} \subseteq S^{'}}; \\ {e (M) ∣ M \in Sat (f_{\max}^{σ} (ϵ, E, F, α))} = {S \in σ (F) ∣ {(e (E))}_{F}^{+} \subset S_{F}^{+}}; \\ {e (M) ∣ M \in Sat (f_{out}^{σ} (ϵ, E, F, α))} = {S \in σ (F) ∣ {(e (E))}_{F}^{+} = S_{F}^{+} \land α \notin S} . \end{array}$

Functions $f_{base}^{σ}$ and $f_{\max}^{σ}$ coincide with the ones for preferred semantics, except that they compare ranges of extensions. The new function $f_{out}^{σ}$ does the additional check described above.

Likewise, the graph $C RED - θ_{\overline{f}}^{F, α}$ abstracting the cegartix-algorithm for credulous acceptance w.r.t. semi-stable and stage semantics coincides with $S KEPT - θ_{\overline{f}}^{F, α}$ with the exception that the outcomes of the rules ${Fail}_{base}$ and ${Succeed}_{out}$ are swapped, i.e. the application of ${Fail}_{base}$ leads to $Reject$ and the application of ${Succeed}_{out}$ leads to $Accept$ . That is since a found witness (a θ-extension containing α) means that α is credulously accepted, while if exhaustive search does not reveal such a witness, it α is not credulously accepted. As the algorithm searches for extensions containing the queried argument α, two functions have to differ; we assume $g_{base}^{σ}$ and $g_{out}^{σ}$ , which contain the condition $α \in S$ instead of $α \notin S$ compared to the functions $f_{base}^{θ}$ and $f_{out}^{θ}$ for skeptical acceptance: $\begin{array}{l} {e (M) ∣ M \in Sat (g_{base}^{σ} (ϵ, E, F, α))} = {S \in σ (F) ∣ α \in S \land \neg \exists S^{'} \in ϵ : S_{F}^{+} \subseteq S^{'}}; \\ {e (M) ∣ M \in Sat (g_{out}^{σ} (ϵ, E, F, α))} = {S \in σ (F) ∣ {(e (E))}_{F}^{+} = S_{F}^{+} \land α \in S} . \end{array}$

The following results show correctness of the abstract solvers for acceptance problems w.r.t. semi-stable and stage semantics described in this section. The proofs, which follow the same structure as previous proofs, can be found in the Appendix.
Lemma 5.1.
For $(σ, θ) \in {(adm, sem), (com, sem), (cf, stg)}$ , any AF $F = (A, R)$ and an argument $α \in A$ , if one of the rules ${Fail}_{out}$ or ${Succeed}_{out}$ is applied from state ${(ϵ, E^{'}, E)}_{out}$ in the graph $S KEPT - θ_{(f_{out}^{σ}, f_{\max}^{σ}, f_{base}^{σ})}^{F, α}$ (resp. $C RED - θ_{(g_{out}^{σ}, f_{\max}^{σ}, g_{base}^{σ})}^{F, α}$ ) then $e (E^{'}) \in θ (F)$ and ${(e (E^{'}))}_{F}^{+} \notin ϵ$ .
Theorem 5.2.
For $(σ, θ) \in {(adm, sem), (com, sem), (cf, stg)}$ , any AF $F = (A, R)$ and $α \in A$ , the graph $S KEPT - θ_{(f_{out}^{σ}, f_{\max}^{σ}, f_{base}^{σ})}^{F, α}$ (resp. $C RED - θ_{(g_{out}^{σ}, f_{\max}^{σ}, g_{base}^{σ})}^{F, α}$ ) is finite, acyclic and any terminal state reachable from the initial state is either $Accept$ or $Reject$ ; $Reject$ is reachable from the initial state iff α is not skeptically accepted (resp. not credulously accepted) in F w.r.t. $prf$ .

Finally note again that from Theorem 5.2 it follows that $Accept$ is reachable from the initial state if and only if α is skeptically accepted (resp. credulously accepted) in F, which completes the correctness statement for $S KEPT - θ_{\overline{f}}^{F, α}$ (resp. $C RED - θ_{\overline{g}}^{F, α}$ ).
5.2. Shortcuts for cegartix-algorithms

σ	$Cre d_{σ}$	$Skep t_{σ}$
$prf$	$NP$ -c	$Π_{2}^{P}$ -c
$sem$	$Σ_{2}^{P}$ -c	$Π_{2}^{P}$ -c
$stg$	$Σ_{2}^{P}$ -c	$Π_{2}^{P}$ -c

When defining abstract solvers for the algorithms of cegartix in previous sections we restricted our attention to the core of the algorithm. In this section we show that the graphs presented so far can be easily extended in a modular way to capture the full algorithms.

We do so by abstracting the full Algorithm 1 of [25] for skeptical acceptance w.r.t. preferred semantics, including the shortcut computation performed at the beginning of the algorithm. By this shortcut, the algorithm immediately returns with a negative answer for the skeptical acceptance problem w.r.t. preferred semantics, if there is a σ-extension ( $σ \in {adm, com}$ ) attacking the queried argument. To this end we define ${F ULL - S KEPT - PRF}_{\overline{f}}^{F, α}$ for a given AF $F = (A, R)$ , an argument $α \in A$ and a vector of oracle functions $\overline{f}$ as the graph ${S KEPT - PRF}_{\overline{f}}^{F, α}$ from Section 3.2 with the following modifications:

We add the transition rules presented in Fig. 16.

Moreover, there is a set of oracle rules with index $pre$ . For $σ \in {adm, com}$ we assume a function $f_{pre}^{σ}$ such that $\begin{matrix} {e (M) ∣ M \in Sat (f_{pre}^{σ} (ϵ, E, F, α))} = {S \in σ (F) ∣ S attacks α} . \end{matrix}$

The initial state is ${(\emptyset, \emptyset, \emptyset)}_{pre}$ .

To represent the shortcut, a third level has been added, which precedes levels

base

and

\max

, so that we call this level

pre

. Note that ϵ and

E^{'}

are always ∅ at level

pre

. If the oracle rules with index

pre

lead to a record corresponding to a satisfying assignment of

f_{pre}^{σ}

(i.e. a σ-extension attacking α), the application of

{Succeed}_{pre}

leads to rejection; otherwise

{Fail}_{pre}

leads to the state

{(\emptyset, \emptyset, \emptyset)}_{base}

, which means we have arrived at

{S KEPT - PRF}_{\overline{f}}^{F, α}

. The resulting graph represents the full Algorithm 1 of [25].

Fig. 16.

The transition rules of the graph ${F ULL - S KEPT - PRF}_{\overline{f}}^{F, α}$ added to ${S KEPT - PRF}_{\overline{f}}^{F, α}$ .

Theorem 5.3.

For any AF $F = (A, R)$ , argument $α \in A$ , and $σ \in {adm, com}$ , the graph ${F ULL - S KEPT - PRF}_{(f_{base}^{σ}, f_{\max}^{σ}, f_{pre}^{σ})}^{F, α}$ is finite, acyclic and any terminal state reachable from the initial state is either $Accept$ or $Reject$ ; $Accept$ is reachable iff α is skeptically accepted in F w.r.t. $prf$ .

6. Related work

The use of abstract solvers was initiated by Nieuwenhuis et al. [44]. In that work the authors first presented an abstract solver for SAT, similar to our introduction of abstract solvers in Section 2.2. Then, they presented two extensions: (i) a description of Conflict-Driven Clause Learning SAT solving, i.e. involving backjumping and learning techniques, by means of modular addition of transition rules, but also by changing the definition of states to account for learned clauses, and (ii) they considered also Satisfiability Modulo Theories (SMT) problems with certain logics via a lazy approach [48], i.e. where the SAT calls are made to provide satisfying assignments of the Boolean abstraction of the SMT problem that are then checked for “SMT consistency”. Lierler [35] imported this methodology to Answer Set Programming (ASP), by first designing abstract solvers for some backtracking-based ASP solvers for non-disjunctive ASP solving, and then enhancing her approach to include backjumping and learning techniques [36]. Another extension for describing CASP solvers, i.e. systems able to deal with a combination of ASP and constraint programming, a language useful to represent and reason on hybrid domains, has been put forward in [37]. Other works on abstract solvers are [38], where solvers for different formalisms, e.g. ASP and SAT with Inductive Definitions, are compared by means of comparison of the related graphs, and the following series of papers where, starting from a developed concept of modularity in answer set solving [39], abstract modeling of solvers for multi-logic systems are presented [40–42].

If we turn our attention to the usage of abstract solvers for dealing with reasoning tasks beyond NP, the situation is less developed and only very recently few works have been put forward. Abstract solvers for certain disjunctive answer set solvers implementing basic backtracking have been introduced by Brochenin et al. [6] and are studied in a more general way in [7]. Even more recently, abstract solvers for satisfiability of Quantified Boolean Formulas [9] and cautious reasoning in ASP [10] have been presented.

Only few of the aforementioned works [36,44] have already aimed for the implementation of combinations of algorithms based on abstract solvers; thus, our practical results are particularly remarkable.

As far as other algorithms for the preferred semantics in the literature are concerned, we mention [22,43], where a labelling-based approach is employed. These algorithms differ in the initial labellings and how transitions are applied to argument labels. Moreover, [43] includes other semantics than preferred and also argument-based proof theories, another way to characterize an algorithm’s behavior but whose goal is not to be the basis for an implementation.

The argumentation solver competition 2015 [51] had eleven participating systems in the task of deciding skeptical acceptance of an argument w.r.t. preferred semantics. The first two places were taken by ArgSemSAT and cegartix, whose algorithms are described in terms of abstract solvers in Sections 3.1 and 3.2, respectively. The other solvers in the top five were LabSATSolver, ASPARTIX-V [28] and CoQuiAAS [32] (system descriptions of all participating solvers can be found in [49]). While LabSATSolver uses the same algorithm as ArgSemSAT for this particular task, ASPARTIX-V and CoQuiAAS are reduction-based approaches, using translations to ASP and a particular variant of Max-SAT, respectively. Thus, being based on reduction, their modeling via abstract solvers is less interesting for the abstract argumentation community, given that this would boil down to modeling, respectively, ASP and Max-SAT search algorithms. For this reason, they have not been considered in this paper.

7. Conclusions

In this paper we have shown the applicability and the advantages of using a rigorous formal way for describing certain algorithms for solving decision problems for abstract argumentation frameworks through graph-based abstract solvers instead of, e.g. pseudo-code-based descriptions. Both SAT-based and dedicated approaches for solving hard problems have been analyzed and compared, with focus on algorithms for the preferred semantics. Moreover, by combining abstract solvers, we have obtained a novel algorithm for skeptical acceptance. The algorithm has been implemented taking cegartix [25] as a starting point. An experimental analysis on the benchmark graphs of the first and second argumentation competition, as well as on graphs from earlier work, shows that the new algorithm is complementary to an existing algorithm in cegartix. The above analysis has focused, as said, on the well-studied preferred semantics, and on core algorithms. We have then shown how the machinery can be employed to describe algorithms for different semantics, e.g. semi-stable and stage semantics, as employed in cegartix, and for taking into account specific optimization techniques by means of modular addition of transition rules to the graphs describing the core parts of the algorithms.

As future work, we want to apply the concept of abstract solvers to other promising algorithms and optimization techniques for reasoning tasks in abstract argumentation. In particular, we plan to study certain approaches to the decomposition of AFs [2,16,33,34]. Moreover, we plan to extend our experimental analysis for the new version of cegartix by studying on which classes of AFs the new version is performing better than existing algorithms.

Footnotes

Acknowledgements

We thank Benjamin Kaufmann, member of the Potassco team, for suggesting how to modify the version of clasp employed in the experiments. This work has been funded by the Austrian Science Fund (FWF) through projects I1102, I2854 and P30168-N31, and by Academy of Finland through grants 251170 COIN and 284591.

Proofs

References

Baroni,

M.W.A.

Caminada and

Giacomin, An introduction to argumentation semantics, The Knowledge Engineering Review 26(4) (2011), 365–410. doi:10.1017/S0269888911000166.

Baumann, Splitting an argumentation framework, in: Proceedings of the 11th International Conference on Logic Programming and Nonmonotonic Reasoning, LPNMR 2011,

J.P.

Delgrande and

Faber, eds, Lecture Notes in Computer Science, Vol. 6645, Springer, 2011, pp. 40–53.

Baumann and

Spanring, Infinite argumentation frameworks – On the existence and uniqueness of extensions, in: Advances in Knowledge Representation, Logic Programming, and Abstract Argumentation – Essays Dedicated to Gerhard Brewka on the Occasion of His 60th Birthday,

Eiter,

Strass,

Truszczynski and

Woltran, eds, Lecture Notes in Computer Science, Vol. 9060, Springer, 2015, pp. 281–295.

T.J.M.

Bench-Capon and

P.E.

Dunne, Argumentation in artificial intelligence, Artificial Intelligence 171(10–15) (2007), 619–641. doi:10.1016/j.artint.2007.05.001.

Besnard and

Doutre, Checking the acceptability of a set of arguments, in: Proceedings of the 10th International Workshop on Non-Monotonic Reasoning, NMR 2004,

J.P.

Delgrande and

Schaub, eds, 2004, pp. 59–64.

Brochenin,

Lierler and

Maratea, Abstract disjunctive answer set solvers, in: Proceedings of the 21st European Conference on Artificial Intelligence, ECAI 2014,

Schaub,

Friedrich and

O’Sullivan, eds, Frontiers in Artificial Intelligence and Applications, Vol. 263, IOS Press, 2014, pp. 165–170.

Brochenin,

Lierler and

Maratea, Disjunctive answer set solvers via templates, Theory and Practice of Logic Programming 16(4) (2016), 465–497. doi:10.1017/S1471068415000411.

Brochenin,

Linsbichler,

Maratea,

J.P.

Wallner and

Woltran, Abstract solvers for Dung’s argumentation frameworks, in: Proceedings of the 3rd International Workshop on Theory and Applications of Formal Argumentation, TAFA 2015, Revised Selected Papers,

Black,

Modgil and

Oren, eds, Lecture Notes in Computer Science, Vol. 9524, Springer, 2015, pp. 40–58.

Brochenin and

Maratea, Abstract solvers for quantified Boolean formulas and their applications, in: Proceedings of the 14th International Conference of the Italian Association for Artificial Intelligence, AI*IA 2015,

Gavanelli,

Lamma and

Riguzzi, eds, Lecture Notes in Computer Science, Vol. 9336, Springer, 2015, pp. 205–217.

10.

Brochenin and

Maratea, Abstract answer set solvers for cautious reasoning, in: Proceedings of the Technical Communications of the 31st International Conference on Logic Programming, ICLP 2015,

M.D.

Vos,

Eiter,

Lierler and

Toni, eds, CEUR Workshop Proceedings, Vol. 1433, CEUR-WS.org, 2015.

11.

Caminada,

Carnielli and

P.E.

Dunne, Semi-stable semantics, Journal of Logic and Computation 22(5) (2012), 1207–1254. doi:10.1093/logcom/exr033.

12.

Castell,

Cayrol,

Cayrol and

D.L.

Berre, Using the Davis and Putnam procedure for an efficient computation of preferred models, in: Proceedings of the 12th European Conference on Artificial Intelligence, ECAI 1996,

Wahlster, ed., Wiley, Chichester, 1996, pp. 350–354.

13.

Cerutti,

P.E.

Dunne,

Giacomin and

Vallati, Computing preferred extensions in abstract argumentation: A SAT-based approach, in: Proceedings of the 2nd International Workshop on Theory and Applications of Formal Argumentation, TAFA 2013, Revised Selected Papers,

Black,

Modgil and

Oren, eds, Lecture Notes in Computer Science, Vol. 8306, Springer, 2014, pp. 176–193.

14.

Cerutti,

Giacomin and

Vallati, ArgSemSAT: Solving argumentation problems using SAT, in: Proceedings of the 5th International Conference on Computational Models of Argument, COMMA 2014,

Parsons,

Oren,

Reed and

Cerutti, eds, Frontiers in Artificial Intelligence and Applications, Vol. 266, IOS Press, 2014, pp. 455–456.

15.

Cerutti,

Giacomin and

Vallati, Algorithm selection for preferred extensions enumeration, in: Proceedings of the 5th International Conference on Computational Models of Argument, COMMA 2014,

Parsons,

Oren,

Reed and

Cerutti, eds, Frontiers in Artificial Intelligence and Applications, Vol. 266, IOS Press, 2014, pp. 221–232.

16.

Cerutti,

Giacomin,

Vallati and

Zanella, An SCC recursive meta-algorithm for computing preferred labellings in abstract argumentation, in: Proceedings of the 14th International Conference on Principles of Knowledge Representation and Reasoning, KR 2014,

Baral,

G.D.

Giacomo and

Eiter, eds, AAAI Press, 2014, pp. 42–51.

17.

Cerutti,

Oren,

Strass,

Thimm and

Vallati, A benchmark framework for a computational argumentation competition, in: Proceedings of the 5th International Conference on Computational Models of Argument, COMMA 2014,

Parsons,

Oren,

Reed and

Cerutti, eds, Frontiers in Artificial Intelligence and Applications, Vol. 266, IOS Press, 2014, pp. 459–460.

18.

Cerutti,

Vallati and

Giacomin, Where are we now? State of the art and future trends of solvers for hard argumentation problems, in: Computational Models of Argument – Proceedings of COMMA 2016,

Baroni,

T.F.

Gordon,

Scheffler and

Stede, eds, Frontiers in Artificial Intelligence and Applications, Vol. 287, IOS Press, 2016, pp. 207–218.

19.

Charwat,

Dvořák,

S.A.

Gaggl,

J.P.

Wallner and

Woltran, Methods for solving reasoning problems in abstract argumentation – A survey, Artificial Intelligence 220 (2015), 28–63. doi:10.1016/j.artint.2014.11.008.

20.

Davis,

Logemann and

Loveland, A machine program for theorem proving, Communications of the ACM 5(7) (1962), 394–397. doi:10.1145/368273.368557.

21.

Dimopoulos and

Torres, Graph theoretical structures in logic programs and default theories, Theoretical Computer Science 170(1–2) (1996), 209–244. doi:10.1016/S0304-3975(96)80707-9.

22.

Doutre and

Mengin, Preferred extensions of argumentation frameworks: Query answering and computation, in: Proceedings of the 1st International Joint Conference on Automated Reasoning, IJCAR 2001,

Goré,

Leitsch and

Nipkow, eds, Lecture Notes in Computer Science, Vol. 2083, Springer, 2001, pp. 272–288.

23.

P.M.

Dung, On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games, Artificial Intelligence 77(2) (1995), 321–358. doi:10.1016/0004-3702(94)00041-X.

24.

P.E.

Dunne and

T.J.M.

Bench-Capon, Coherence in finite argument systems, Artificial Intelligence 141(1/2) (2002), 187–203. doi:10.1016/S0004-3702(02)00261-8.

25.

Dvořák,

Järvisalo,

J.P.

Wallner and

Woltran, Complexity-sensitive decision procedures for abstract argumentation, Artificial Intelligence 206 (2014), 53–78. doi:10.1016/j.artint.2013.10.001.

26.

Dvořák and

Woltran, Complexity of semi-stable and stage semantics in argumentation frameworks, Information Processing Letters 110(11) (2010), 425–430. doi:10.1016/j.ipl.2010.04.005.

27.

S.A.

Gaggl,

Linsbichler,

Maratea and

Woltran, Introducing the second international competition on computational models of argumentation, in: Proceedings of the 1st International Workshop on Systems and Algorithms for Formal Argumentation (SAFA 2016),

Thimm,

Cerutti,

Strass and

Vallati, eds, 2016, pp. 4–9. https://www.dbai.tuwien.ac.at/iccma17/Introducing_ICCMA17.pdf.

28.

S.A.

Gaggl,

Manthey,

Ronca,

J.P.

Wallner and

Woltran, Improved answer-set programming encodings for abstract argumentation, Theory and Practice of Logic Programming 15(4–5) (2015), 434–448. doi:10.1017/S1471068415000149.

29.

Gebser,

Kaufmann and

Schaub, Conflict-driven answer set solving: From theory to practice, Artificial Intelligence 187 (2012), 52–89. doi:10.1016/j.artint.2012.04.001.

30.

Järvisalo and

T.A.

Junttila, Limitations of restricted branching in clause learning, Constraints 14(3) (2009), 325–356. doi:10.1007/s10601-008-9062-z.

31.

Järvisalo and

Niemelä, The effect of structural branching on the efficiency of clause learning SAT solving: An experimental study, Journal of Algorithms 63(1–3) (2008), 90–113. doi:10.1016/j.jalgor.2008.02.005.

32.

Lagniez,

Lonca and

Mailly, CoQuiAAS: A constraint-based quick abstract argumentation solver, in: Proceedings of the 27th IEEE International Conference on Tools with Artificial Intelligence, ICTAI 2015, IEEE Computer Society, 2015, pp. 928–935.

33.

Liao, Toward incremental computation of argumentation semantics: A decomposition-based approach, Annals of Mathematics and Artificial Intelligence 67(3–4) (2013), 319–358. doi:10.1007/s10472-013-9364-8.

34.

Liao, Efficient Computation of Argumentation Semantics, Intelligent Systems Series, Academic Press, 2014. ISBN 978-0-12-410406-8. http://store.elsevier.com/product.jsp?isbn=9780124104068.

35.

Lierler, Abstract answer set solvers, in: Proceedings of the 24th International Conference on Logic Programming, ICLP 2008,

M.G.

de la Banda and

Pontelli, eds, Lecture Notes in Computer Science, Vol. 5366, Springer, 2008, pp. 377–391.

36.

Lierler, Abstract answer set solvers with backjumping and learning, Theory and Practice of Logic Programming 11(2–3) (2011), 135–169. doi:10.1017/S1471068410000578.

37.

Lierler, Relating constraint answer set programming languages and algorithms, Artificial Intelligence 207 (2014), 1–22. doi:10.1016/j.artint.2013.10.004.

38.

Lierler and

Truszczynski, Transition systems for model generators – A unifying approach, Theory and Practice of Logic Programming 11(4–5) (2011), 629–646. doi:10.1017/S1471068411000214.

39.

Lierler and

Truszczynski, Modular answer set solving, in: Late-Breaking Developments in the Field of Artificial Intelligence, AAAI Workshops, Vol. WS-13-17, AAAI, 2013.

40.

Lierler and

Truszczynski, Abstract modular inference systems and solvers, in: Proceedings of the 16th International Symposium on Practical Aspects of Declarative Languages, PADL 2014,

Flatt and

Guo, eds, Lecture Notes in Computer Science, Vol. 8324, Springer, 2014, pp. 49–64.

41.

Lierler and

Truszczynski, An abstract view on modularity in knowledge representation, in: Proceedings of the 29th AAAI Conference on Artificial Intelligence, AAAI 2015,

Bonet and

Koenig, eds, AAAI Press, 2015, pp. 1532–1538.

42.

Lierler and

Truszczynski, On abstract modular inference systems and solvers, Artificial Intelligence 236 (2016), 65–89. doi:10.1016/j.artint.2016.03.004.

43.

Modgil and

M.W.A.

Caminada, Proof theories and algorithms for abstract argumentation frameworks, in: Argumentation in Artificial Intelligence,

Rahwan and

G.R.

Simari, eds, Springer, 2009, pp. 105–129.

44.

Nieuwenhuis,

Oliveras and

Tinelli, Solving SAT and SAT modulo theories: From an abstract Davis–Putnam–Logemann–Loveland procedure to DPLL(T), Journal of the ACM 53(6) (2006), 937–977. doi:10.1145/1217856.1217859.

45.

Nofal,

Atkinson and

P.E.

Dunne, Algorithms for decision problems in argument systems under preferred semantics, Artificial Intelligence 207 (2014), 23–51. doi:10.1016/j.artint.2013.11.001.

46.

Rahwan and

G.R.

Simari (eds), Argumentation in Artificial Intelligence, Springer, 2009. doi:10.1007/978-0-387-98197-0.

47.

E.D.

Rosa,

Giunchiglia and

Maratea, Solving satisfiability problems with preferences, Constraints 15(4) (2010), 485–515. doi:10.1007/s10601-010-9095-y.

48.

Sebastiani, Lazy satisfiability modulo theories, Journal of Satisfiability, Boolean Modeling and Computation 3(3–4) (2007), 141–224.

49.

Thimm and

Villata, System descriptions of the first International competition on computational models of argumentation (ICCMA’15), 2015. arXiv:1510.05373.

50.

Thimm and

Villata, The first international competition on computational models of argumentation: Results and analysis, Artificial Intelligence 252 (2017), 267–294. doi:10.1016/j.artint.2017.08.006.

51.

Thimm,

Villata,

Cerutti,

Oren,

Strass and

Vallati, Summary report of the first international competition on computational models of argumentation, AI Magazine 37(1) (2016), 102–104. doi:10.1609/aimag.v37i1.2640.

52.

Verheij, Two approaches to dialectical argumentation: Admissible sets and argumentation stages, in: Proceedings of the 8th Dutch Conference on Artificial Intelligence, NAIC 1996,

J.-J.C.

Meyer and

L.C.

van der Gaag, eds, 1996, pp. 357–368.

53.

J.P.

Wallner,

Weissenbacher and

Woltran, Advanced SAT techniques for abstract argumentation, in: Proceedings of the 14th International Workshop on Computational Logic in Multi-Agent Systems, CLIMA 2013,

Leite,

T.C.

Son,

Torroni,

van der Torre and

Woltran, eds, Lecture Notes in Computer Science, Vol. 8143, Springer, 2013, pp. 138–154.

Abstract solvers for Dung’s argumentation frameworks

Abstract

Keywords

1. Introduction

2. Preliminaries

2.1. Abstract argumentation frameworks

1 In the literature also infinite AFs have been considered. We refer to [3] for the effects this has on semantics.

3 Comparisons of the performance of cegartix and other solvers can be found in [18,50].

4.2. Benchmarks

4 Archives of the benchmark sets can be found at http://argumentationcompetition.org/2015/iccma2015_benchmarks.zip, http://www.dbai.tuwien.ac.at/iccma17/benchmarks/A.tar.gz, and http://www.dbai.tuwien.ac.at/research/project/argumentation/cegartix/files/clima.zip.

5.1. Core algorithms for semi-stable and stage semantics

7. Conclusions

Footnotes

Acknowledgements

Proofs

References

¹
In the literature also infinite AFs have been considered. We refer to [3] for the effects this has on semantics.

³
Comparisons of the performance of cegartix and other solvers can be found in [18,50].

⁴
Archives of the benchmark sets can be found at http://argumentationcompetition.org/2015/iccma2015_benchmarks.zip, http://www.dbai.tuwien.ac.at/iccma17/benchmarks/A.tar.gz, and http://www.dbai.tuwien.ac.at/research/project/argumentation/cegartix/files/clima.zip.