Abstract solvers for Dung’s argumentation frameworks
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.
Dung’s concept of abstract argumentation  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 : Already the second edition  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 . 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 , 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  to reduction-based [13,25] approaches (see  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  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  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 , (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.
In this section we first review (abstract) argumentation frameworks  and their semantics (see  for an overview), and then introduce abstract solvers  on the concrete instance describing the Davis–Putnam–Logemann–Loveland (dpll) procedure for SAT solving .
2.1.Abstract argumentation frameworks
An argumentation framework (AF) is a pair where A is a finite11 set of arguments and is the attack relation. Semantics for argumentation frameworks assign to each AF a set of extensions. We consider here for σ the functions , , and , which stand for admissible, complete, and preferred semantics. Towards the definitions of the semantics we need some formal concepts. For an AF , an argument is defended (in F) by a set if for each such that , there is a , such that holds.
Let be an AF. A set is conflict-free (in F), denoted , if there are no such that . For , it holds that
iff each is defended by S;
iff and for each defended by S, holds;
iff and there is no with , or equivalently,
iff and there is no with .
Consider the AF 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: , , and .
Given an AF , an argument , and a semantics σ, the problem of skeptical acceptance () asks whether it is the case that a is contained in all σ-extensions of F; the problem of credulous acceptance () asks if a is contained in at least one σ-extension. While skeptical acceptance is trivial for and decidable in polynomial time for , it is -complete22 for , see [21,23,24].
2.2.Abstract solvers for SAT
Most SAT solvers are based on the Davis–Putnam–Logemann–Loveland (dpll) procedure . We give an abstract solver for dpll following the work of Nieuwenhuis et al. . 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 (resp. ). A literal is an atom a or its negation . The complement of literal l is defined as and . 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 as follows: if then a maps to , while if then a maps to . By 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 . 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, ∅, and are records relative to the set . We say that a record E is inconsistent if it contains ⊥ or both a literal l and its complement , and consistent otherwise. Moreover, by 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 with the consistent set of literals, and so with the assignment which maps a to and b to . Finally, denotes the number of literals in record E.
Each CNF formula φ determines its dpll graph . The set of nodes (states) of consists of the records relative to and two distinguished states and . The edges of the graph 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 and . 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.
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 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 asserts that we can add a literal that is a logical consequence of our previous decisions and the given formula. The rule 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 asserts that the current state of computation has failed and cannot be fixed. The rule 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 leading from state ∅ to a terminal state. If it is , then the formula is satisfiable, and if it is , then it is unsatisfiable. Since there is no infinite path, a terminal state is always reached. The following result states this observation formally.
For any CNF formula φ, the graph is finite and acyclic; any terminal state of reachable from the initial state other than is ; the record in the state preceding corresponds to satisfying assignment of φ; and 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 is reachable from the initial state iff φ is satisfiable follows directly.
Figure 3 presents two paths in from the initial state ∅ to the terminal state . Every edge is annotated on the left by the name of the transition rule that gives rise to this edge in . Thus, Theorem 2.1 asserts that φ is satisfiable; moreover, the record where the rule is applied corresponds to a satisfying assignment of φ, i.e. .
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 (see (*)) where 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 such that always assigns the decision literal to true by default, i.e. to substitute rule in Fig. 2 with the following rule , where a represents an atom instead of a literal:
Let us call the resulting graph , whose nodes correspond to the nodes of graph. We can state the following theorem.
For any CNF formula φ, the graph is finite and acyclic; any terminal state of reachable from the initial state is either or ; the record in the state preceding corresponds to a maximal satisfying assignment of φ, and 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  (implemented in the tool ArgSemSat ) for extension enumeration, and an algorithm for deciding skeptical acceptance of cegartix . Moreover, we abstract the dedicated approach for enumeration of . 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 .
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 , each step is delegated to a SAT solver. The direct approach from , 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 . 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 , the variables they use are denoted by . For this set it holds that , i.e. there is an atom for each argument. The states of all the graph representations we will define are either
(1) an annotated triple where , is a set of sets of arguments, and both and E are records over ; or
(2) for ; or
(3) a distinguished state or .
The intended meaning of a state is that ϵ is the set of already found preferred extensions of F (visited part of the search space), 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 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 and correspond to different lower level computations, typically SAT calls, while 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 to 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 state, contain several subpaths consisting exclusively of either states or states, and finally end in the state (for enumeration algorithms) or in one of the states or (for acceptance algorithms).
The remaining states denote terminated computation: contains all solutions to the enumeration problem, while or denote an answer to a decision problem.
The SAT-based algorithms construct formulas by a function f s.t. for all possible arguments of f. The formulas are adapted from . The argument α is relevant only for cegartix to decide skeptical acceptance of α. Finally, we use 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.
Let E be a record. E can be written as where are strings of non-decision literals and are all the decision literals of E. We define the sequence representation of E as . For two sequence representations of records and , we say that is lexicographically smaller than , , if for the first index n where and differ with , or if and for all we have .
Consider the records , , and . The sequence representations of these records are given by , , and . The lexicographic ordering is .
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 and such that .
Let , be sets of sets of arguments, , , , be records, and . We define the following strict partial orders (i.e. irreflexive and transitive binary relations):
iff , where is the lexicographic order.
The strict partial order < on states is defined such that for any two states and , iff
(i) , or
(ii) and , or
(iii) and and , or
(iv) and and and .
Consider the states , , , , and . It holds that . First, holds due to . Moreover, is because of . Furthermore, holds since . Finally, observe that can be written, in the spirit of Definition 2, as , where ∅ denotes the empty string. Hence we obtain and similarly . We get since .
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 ) 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.
We now represent PrefSat as an abstract solver. The graph for an AF F and a vector of functions is defined by the states over and the transition rules presented in Fig. 4. Its initial state is . We assume the functions and that generate CNF formulas for , a record E, and an argument such that:
In words, the models of the formula represent the complete extensions of F such that no superset is contained in ϵ. Moreover, the models of 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 the set ϵ represents preferred extensions found as of now, 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 corresponds to different kinds of SAT calls.
As the oracle rules with annotation coincide with the ones of (cf. Fig. 2), their role is to search for a satisfying assignment of . That is, if a rule is applied to the state for i, the formula is unsatisfiable. Conversely, when a rule is applied from that state, the formula is satisfied by E. Notice that and might shift i to reflect a change of type of SAT calls. When , 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 . In case of success, is applied and the procedure is repeated, since the current complete extension might still not be maximal. Failure by means we have found a preferred extension.
Again consider the AF F depicted in Fig. 1. We have seen in Example 1 that F has two preferred extensions, namely and . Figure 5 shows a possible path in the graph . As expected, the computation terminates in the state . 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 we represent an inconsistent and decision-free record.
It remains to show correctness of by showing that we reach a terminal state containing all preferred extensions of F. First observe that the oracle rules are exactly taken from 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:
For any AF F and , if is applied from state in the graph then ; if is applied then is unsatisfiable.
We continue with a lemma stating that only preferred extensions which have not been found at this point are added to ϵ.
For any AF F, if the rule is applied from state in the graph then and .
Let be the state from which is applied. This means, by Lemma 3.1, that is unsatisfiable, hence, by the definition of formula , there is no with . To get it remains to show that . Observe that is applied at least once, since every AF has a complete extension. Moreover, the value of is only updated by applications of or . In both cases corresponds to a complete extension of F, due to the definitions of the formula or , respectively, and Lemma 3.1. Therefore is a complete extension of F.
Since the initial state is , an application of must precede . From this application of it follows from Lemma 3.1 that there is a record such that . Moreover every application of updates by a proper superset of itself. Therefore and also , in particular . □
Now we are ready to show correctness of .
For any AF F, the graph is finite, acyclic and the only terminal state reachable from the initial state is where .
In order to show that is finite, consider some state of . Since both E and are records over , and F is finite by definition, the number of possible records E and is finite. Similarly, there is only a finite number of sets of sets of arguments ϵ. Finally, only contains states with . Thus the number of states is finite in the graph .
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 and representing the states before and after the application of a rule. First of all, the i-oracle rules (i.e. , , and ) fulfill because of (iv). For all of these rules , and , but is lexicographically smaller than , therefore . Moreover, fulfills due to (i) since by Lemma 3.2. guarantees because of (ii). Finally, fulfills due to (iii), since the -oracle rules work on the formula and the extension associated with a satisfying assignment of that formula must be a proper superset of . Therefore, by transitivity of <, or any two states and such that is reachable from in it holds that , showing that the graph is acyclic.
The only terminal state reachable from the initial state is (via rule ) for some since all states of have and for each there is a rule with the condition “no other rule applies”. It remains to show that, when state is reached, ϵ coincides with . Since elements are only added to ϵ by application of the rule we know from Lemma 3.2 that for each it holds that . To reach , the rule must have been applied from a state . This means, by the definition of and Lemma 3.1, that for each complete extension S of F there is some such that . Hence . □
3.2.SAT-based algorithm for acceptance
cegartix  is a SAT-based tool for deciding several acceptance questions for AFs. Here we focus on Algorithm 1 of  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 for an AF F, an argument α and a vector of functions is defined by the states over and the rules in Fig. 4 replacing the rules for and adding the rules and as depicted in Fig. 6. The initial state is . For we assume the functions and such that:
The graph is similar to . Again, the models of the formulas and 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 . The graph differs in case of failure in a state annotated by or . When all the preferred extensions have been enumerated, i.e. the -oracle ends with an application of , we can report a positive outcome with , since we have ensured that α belongs to all of them. If we arrive at , i.e. when a preferred extension has been found, it is necessary to check whether α belongs to it, and this is done via rules and that either lead to or give the control to the level.
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 of F. Accordingly, the possible path of the graph which is depicted in Fig. 7 (with base semantics ) terminates in the -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 . For checking whether a is skeptically accepted in F, a possible path in the graph (again with base semantics ) is shown in Fig. 8. As expected, the path terminates in the state .
Again, we get the following from Theorem 2.1:
For any AF , argument , , and , if is applied from state in the graph then ; if is applied then 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.
For any AF F, if the rule is applied from state in the graph with then and .
For any AF , argument , and , the graph is finite, acyclic and any terminal state reachable from the initial state is either or ; is reachable iff α is not skeptically accepted in F w.r.t. .
Finally note that from Theorem 3.6 it follows that is reachable from the initial state if and only if α is skeptically accepted by F, which completes the correctness statement for .
3.3.Dedicated approach for enumeration
Algorithm 1 of  presents a direct approach for enumerating preferred extensions. One function is important for this algorithm, which is called IN-TRANS. Given an AF , it marks an argument as belonging to the currently built extension, and marks all attackers and all attacked arguments 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 does not attack a and a attacks ” of the rule .
The graph for an AF F is defined by the states over and the transition rules presented in Fig. 9. Its initial state is . The structure of the graph is similar to that of . 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 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 rule only adds atoms positively, which is useful in Algorithm 2 of  as it ensures maximality of final assignments. When a record assigning all arguments is found, the rule 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 , and the process continues. In both and , the use of one of the rules or 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.
A possible path in the graph 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 , 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.
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.
For any AF F, if the rule is applied from state in the graph then and .
For any AF F, the graph is finite, acyclic and the only terminal state reachable from its initial state is where .
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 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 (which must not contain the queried argument), by means of a series of further SAT calls annotated with .
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 by by abstaining from the condition that the queried argument must not be contained in the σ-extension. Hence, a single modified SAT call to returns a preferred extension which has not been found already.
Given an AF F, an argument α and a base semantics , the graph representing the new algorithm for deciding skeptical acceptance of α in F w.r.t. is defined by the states of and the transition rules presented in Fig. 11. Its initial state is . As we can see, the graph describes exactly the intuition behind the new proposal. A new label 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 such that:
Then, the outcome of the rules is treated similarly, through the rules, to the graph presented in Section 3.2.
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 is guaranteed to be an admissible (and preferred) set.
From Theorem 2.2 we know that the -oracle rules give a maximal satisfying assignment of :
For any AF , argument , and , if is applied from state in the graph then and with ; if is applied then is unsatisfiable.
To be sure that maximal satisfying assignments correspond to preferred extensions, it has to hold that the atoms occurring in which do not correspond to arguments of the AF do not affect maximality. To this end we make the following assumption.
Given an AF , a set of sets of arguments ϵ, a record E relative to , and an argument , for each , where , it holds that iff .
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.
For any AF F, if the rule is applied from state in the graph with then and .
For any AF , argument , and , the graph is finite, acyclic and any terminal state reachable from the initial state is either or ; is reachable iff α is not skeptically accepted in F w.r.t. .
(1) 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 replaced by ). Consider two states and representing the states before and after the application of a rule. First of all, the -oracle rules (i.e. , , and ) fulfill because of (iv). For all of these rules , and , but is lexicographically smaller than , therefore . Moreover, fulfills due to (i) since by Lemma 3.10. guarantees because of (ii). Finally, fulfills due to (ii), since , and and result in terminal states. Therefore, by transitivity of <, or any two states and such that is reachable from in it holds that , showing that the graph is acyclic.
(2) Any terminal state of reachable from the initial state is either or : This is immediate by the existence of the rule with condition “no other rule applied” and the fact that the rules and are complete in the sense that if one rule does not apply the other rule applies and vice versa.
(3) is reachable from the initial state iff α is not skeptically accepted by F w.r.t. .
(⇒): Assume is reachable. Hence also with is reachable. Moreover was applied at a state , meaning, by Lemma 3.9, that and with . Taking into account Assumption 1 this means, by the definition of , that is a ⊆-maximal σ-extension, i.e. a preferred extension. Since we get that α is not skeptically accepted.
(⇐): Assume α is not skeptically accepted by F w.r.t. . Hence there is some with . Now assume, towards a contradiction, that is not reachable. This means by (1) and (2), that is reachable. Hence is applicable from a state . By the definition of and Lemma 3.9, this means that there is no σ-extension S of F such that . Now note that 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 it holds that , a contradiction. □
Again it is important to note that from Theorem 3.11 it follows that is reachable from the initial state if and only if α is skeptically accepted by F, which completes the correctness statement for .
For the AF F from Fig. 1, a possible path in is depicted in Fig. 12. It correctly results in , as c is not skeptically accepted in F w.r.t. . Figure 13, on the other hand, shows a possible path in . Note that both paths are shorter than the ones of 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.
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.33
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  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 is conjunctively added to for , 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 .
The variants of cegartix considered in our experiments are:
(1) ceg: version with com as a base semantics, which was the setting employed in both editions of the competition. Past experiments (, on different benchmark graphs) overall showed similar or better performance of this version compared to that with adm as a base semantics.
(2) ceg+-com: new version implementing the combination in Section 3.4 with com as a base semantics.
(3) ceg+-adm: new version implementing the combination in Section 3.4 with adm as a base semantics.
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.
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 sets44
ICCMA’15: These are 192 AFs with three arguments to be queried for, from the competition in the year 2015 . 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 , 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 , 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 were created as randomly generated digraphs, with a fixed set of arguments and a probability to include an attack for each with probability . For each parameter choice 10 AFs were created.
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 ( 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.
|Median runtime||Timeouts||Uniquely solved|
|Benchmark||ceg||ceg+-com||ceg+-adm||ceg||ceg+-com||ceg+-adm||by ceg||by ceg+-com or ceg+-adm|
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.
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 , 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  deciding skeptical (resp. credulous) acceptance w.r.t. other, namely stage  and semi-stable , 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 in an AF , defined as , i.e. S together with all arguments it attacks. Stage () and semi-stable () semantics are then defined as follows:
Given an AF F,
, if and there is no such that ;
, if and there is no such that , or equivalently,
, if and there is no such that .
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 , a uniform characterization of θ is as follows: Given an AF F, iff and there is no such that .
Algorithms for skeptical (resp. credulous) acceptance w.r.t. these semantics are presented in Algorithms 2 and 3 of  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 for a semantics , an AF F, and argument α, and a vector of functions is defined by states over and the transition rules of (Figs 4 and 6) with additional oracle rules for index (i.e. we have for , , and now) and the rules and 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 .
The initial state of is . For we assume functions , and such that:
Functions and coincide with the ones for preferred semantics, except that they compare ranges of extensions. The new function does the additional check described above.
Likewise, the graph abstracting the cegartix-algorithm for credulous acceptance w.r.t. semi-stable and stage semantics coincides with with the exception that the outcomes of the rules and are swapped, i.e. the application of leads to and the application of leads to . 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 and , which contain the condition instead of compared to the functions and for skeptical acceptance:
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.
For , any AF and an argument , if one of the rules or is applied from state in the graph (resp. ) then and .
For , any AF and , the graph (resp. ) is finite, acyclic and any terminal state reachable from the initial state is either or ; is reachable from the initial state iff α is not skeptically accepted (resp. not credulously accepted) in F w.r.t. .
Finally note again that from Theorem 5.2 it follows that is reachable from the initial state if and only if α is skeptically accepted (resp. credulously accepted) in F, which completes the correctness statement for (resp. ).
5.2.Shortcuts for cegartix-algorithms
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  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 () attacking the queried argument. To this end we define for a given AF , an argument and a vector of oracle functions as the graph 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 . For we assume a function such that
The initial state is .
For any AF , argument , and , the graph is finite, acyclic and any terminal state reachable from the initial state is either or ; is reachable iff α is skeptically accepted in F w.r.t. .
The use of abstract solvers was initiated by Nieuwenhuis et al. . 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 , 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  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 . 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 . Other works on abstract solvers are , 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 , 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.  and are studied in a more general way in . Even more recently, abstract solvers for satisfiability of Quantified Boolean Formulas  and cautious reasoning in ASP  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,  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  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  and CoQuiAAS  (system descriptions of all participating solvers can be found in ). 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.
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  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.
1 In the literature also infinite AFs have been considered. We refer to  for the effects this has on semantics.
2 The class denotes the class of problems , such that the complementary problem can be decided by a nondeterministic polynomial time algorithm that has (unrestricted) access to an -oracle.
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.
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.
Proof of Lemma 3.5.
Let be the state from which is applied. The state must have been achieved by the application of from a state . This means, by the definition of formula and Lemma 3.4, that there is no with . For it remains to show that . Observe that an update of the value of is only done by an application of or . In both cases corresponds to a σ-extension of F, since it is a satisfying assignment of one of the formulas and and therefore guaranteed to be a σ-extension of F.
Since the initial state is , an application of must precede . From this application of it follows that there is some record such that holds. Moreover every application of updates by a proper superset of itself. Therefore and also , in particular . □
Proof of Theorem 3.6.
(1) is finite and acyclic: In order to show finiteness note that the states of coincide with the states of , there is just an additional option for i. Hence finiteness follows from Theorem 3.3. In order to show that is acyclic we have to show that the rules that differ in from (i.e. the ones listed in Fig. 6) are increasing with respect to the ordering < from Definition 3: fulfills due to (i) by Lemma 3.5, guarantees because of (ii), and and end in terminal states.
(2) Any terminal state of reachable from the initial state is either or : Consider the state . If then there is a rule with the condition “no other rule applies”, hence ς cannot be a terminal state. If , the rules and are complete in the sense that if one rule does not apply the other rule applies and vice versa. Therefore only and can be terminal states.
(3) is reachable from the initial state iff α is not skeptically accepted in F w.r.t. : (⇒): Assume is reachable. Hence also with is reachable. Moreover was applied at a state , meaning, by Lemma 3.4, that is unsatisfiable, i.e. there is no σ-extension S with . It remains to show that . That is by the fact that there must be a preceding application of the rule from some state with being a σ-extension of F by the definition of and Lemma 3.4. Now as , , and , we have that α is not skeptically accepted by F w.r.t. . (⇐): Assume α is not skeptically accepted by F w.r.t. . Hence there is some with . Now assume, towards a contradiction, that is not reachable. This means by (1) and (2), that is reachable. Hence is applicable from a state . By the definition of and Lemma 3.4, this means that there is no σ-extension S of F with and . Now note that is the only rule where elements are added to ϵ. Moreover, by Lemma 3.5, we know that elements added are preferred extensions of F. But therefore for each with it holds that , a contradiction. □
Proof of Lemma 3.7.
The application of from state must have been preceded by from the state which only differs from in i. We now analyze the record E as it is constructed by the rules , and . The application of adds literal a, literal is added by for all b being in conflict with a in F. Therefore is conflict-free in F. Moreover is admissible since if “there is an argument α such that does not attack α and α attacks ”, then is applied instead of . To get it remains to show that there is no with . Assume there is such an . Then there must be some with . Now observe that the graph first adds a to the record and afterwards . Therefore S must have been discovered in advance. But then , hence is applied instead of . □
Proof of Theorem 3.8.
Since states of consist of the same elements as states of , finiteness of follows in the same way as in Theorem 3.3.
To show that is acyclic we will, again as in the proof of Theorem 3.3, show that each transition rule of is increasing w.r.t. a strict partial order on states. To this end we define the strict partial order such that for any two states and , iff
(i) , or
(ii) and , or
(iii) and and ,
The only terminal state reachable from the initial state is since all states of have and for each there is a rule with the condition “no other rule applies”. It remains to show that, when state is reached, ϵ is the set of preferred extensions of F. Since elements are only added to ϵ by rule we know from Lemma 3.7 that for each it holds that . On the other hand, the oracle rules guarantee that each conflict-free set S of F a set with is reached. If S is then admissible and maximal w.r.t. ϵ (which contains only preferred extensions of F as observed before), S is added to ϵ. Therefore each is contained in ϵ. □
Proof of Lemma 3.10.
Let be the state from which is applied. The state must have been achieved by the application of from a state This means, by the definition of formula , Assumption 1, and Lemma 3.9, that , , and is maximal with these properties. Since ϵ is initially empty and, as we argue, only preferred extensions of F are added, it follows that and . □
Proof of Lemma 5.1.
Let be the state from which or is applied. Other rules of index have not changed , hence was the outcome of the application of . By definition of this means that . To get it remains to show that . Observe that is applied at least once, since every AF has a σ-extension. Moreover, the value of is only updated by applications of or . In both cases corresponds to a σ-extension of F, since is a satisfying assignment of the formula or , respectively. Therefore .
Since the initial state is , an application of must precede . From this application of it follows that there is a record such that . Moreover every application of updates by a proper superset of itself. At some point, must be applied, leading to a state with , hence again . Finally, oracle rules with index do not change , hence when is applied from state it holds that . □
Proof of Theorem 5.2.
We show the result for , the proof for very similar.
(1) is finite and acyclic: Finiteness is immediate by Theorem 3.6, since is defined over the same states as – with the only exception of containing a set of extension-ranges instead of extensions, which makes no difference in this matter. For acyclicity all rules have to be increasing w.r.t. <. This was already shown for the rules in Figs 4 and 6. It also follows for the oracle rules for index as the fact that oracle rules are increasing w.r.t. < is independent from the index. Finally, the rule is increasing due to condition (i) in Definition 3 by Lemma 5.1 and leads to a terminal state.
(2) Any terminal state of reachable from the initial state is either or : For any possible state with there is a rule with the condition “no other rule applies”, hence ς cannot be a terminal state. Therefore only and can be terminal states.
(3) is reachable from the initial state iff α is not skeptically accepted in F w.r.t. θ: (⇒): Assume is reachable. It must have been reached by application of from a state . By definition of this means that , and . Moreover we know from Lemma 5.1 that , i.e. that there is no with and therefore also not with . Hence and since , we conclude that α is not skeptically accepted in F w.r.t. θ. (⇐): Assume α is not skeptically accepted in F w.r.t. θ. Hence there is some with . Now assume, towards a contradiction, that is not reachable, meaning, by (1) and (2), that is reachable. Hence is applicable from a state . By the definition of , this means that there is no σ-extension S of F such that and . Now note that is the only rule where elements are added to ϵ. By Lemma 5.1, such elements are ranges of θ-extensions of F. But therefore for each with it holds that , a contradiction to α not being skeptically accepted in F w.r.t. θ. □
Proof of Theorem 5.3.
Finiteness is inherited from . For acyclicity we consider < from Definition 3, but extending by adding for . With this, is increasing due to (ii) as the set of extensions ϵ will stay empty during the application of rules of index . results in a terminal state and finally, also the oracle rules are increasing, as this is independent from the index.
A -state cannot be terminal since if “no other rule applies”, is applied, resulting in . Hence any terminal state reachable from the initial state is either or .
Since the shortcut can only reject instances it follows from Theorem 3.6 that if is reachable then α is skeptically accepted in F w.r.t. . If, on the other hand, is not reachable, then is reached either by application of or by application of . In the first case we again know from Theorem 3.6 that α is not skeptically accepted (note that leads to state , which is just the initial state of ). In the second case there is some which attacks α, therefore also a which attacks α, hence . Again α is not skeptically accepted in F w.r.t. . □
P. Baroni, M.W.A. Caminada and M. Giacomin, An introduction to argumentation semantics, The Knowledge Engineering Review 26: (4) ((2011) ), 365–410. doi:10.1017/S0269888911000166.
R. Baumann, Splitting an argumentation framework, in: Proceedings of the 11th International Conference on Logic Programming and Nonmonotonic Reasoning, LPNMR 2011, J.P. Delgrande and W. Faber, eds, Lecture Notes in Computer Science, Vol. 6645: , Springer, (2011) , pp. 40–53.
R. Baumann and C. 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, T. Eiter, H. Strass, M. Truszczynski and S. 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.
P. Besnard and S. 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 T. Schaub, eds, (2004) , pp. 59–64.
R. Brochenin, Y. Lierler and M. Maratea, Abstract disjunctive answer set solvers, in: Proceedings of the 21st European Conference on Artificial Intelligence, ECAI 2014, T. Schaub, G. Friedrich and B. O’Sullivan, eds, Frontiers in Artificial Intelligence and Applications, Vol. 263: , IOS Press, (2014) , pp. 165–170.
R. Brochenin, Y. Lierler and M. Maratea, Disjunctive answer set solvers via templates, Theory and Practice of Logic Programming 16: (4) ((2016) ), 465–497. doi:10.1017/S1471068415000411.
R. Brochenin, T. Linsbichler, M. Maratea, J.P. Wallner and S. 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, E. Black, S. Modgil and N. Oren, eds, Lecture Notes in Computer Science, Vol. 9524: , Springer, (2015) , pp. 40–58.
R. Brochenin and M. 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, M. Gavanelli, E. Lamma and F. Riguzzi, eds, Lecture Notes in Computer Science, Vol. 9336: , Springer, (2015) , pp. 205–217.
R. Brochenin and M. 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, T. Eiter, Y. Lierler and F. Toni, eds, CEUR Workshop Proceedings, Vol. 1433: , CEUR-WS.org, (2015) .
M. Caminada, W. Carnielli and P.E. Dunne, Semi-stable semantics, Journal of Logic and Computation 22: (5) ((2012) ), 1207–1254. doi:10.1093/logcom/exr033.
T. Castell, C. Cayrol, M. 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, W. Wahlster, ed., Wiley, Chichester, (1996) , pp. 350–354.
F. Cerutti, P.E. Dunne, M. Giacomin and M. 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, E. Black, S. Modgil and N. Oren, eds, Lecture Notes in Computer Science, Vol. 8306: , Springer, (2014) , pp. 176–193.
F. Cerutti, M. Giacomin and M. Vallati, ArgSemSAT: Solving argumentation problems using SAT, in: Proceedings of the 5th International Conference on Computational Models of Argument, COMMA 2014, S. Parsons, N. Oren, C. Reed and F. Cerutti, eds, Frontiers in Artificial Intelligence and Applications, Vol. 266: , IOS Press, (2014) , pp. 455–456.
F. Cerutti, M. Giacomin and M. Vallati, Algorithm selection for preferred extensions enumeration, in: Proceedings of the 5th International Conference on Computational Models of Argument, COMMA 2014, S. Parsons, N. Oren, C. Reed and F. Cerutti, eds, Frontiers in Artificial Intelligence and Applications, Vol. 266: , IOS Press, (2014) , pp. 221–232.
F. Cerutti, M. Giacomin, M. Vallati and M. 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, C. Baral, G.D. Giacomo and T. Eiter, eds, AAAI Press, (2014) , pp. 42–51.
F. Cerutti, N. Oren, H. Strass, M. Thimm and M. Vallati, A benchmark framework for a computational argumentation competition, in: Proceedings of the 5th International Conference on Computational Models of Argument, COMMA 2014, S. Parsons, N. Oren, C. Reed and F. Cerutti, eds, Frontiers in Artificial Intelligence and Applications, Vol. 266: , IOS Press, (2014) , pp. 459–460.
F. Cerutti, M. Vallati and M. 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, P. Baroni, T.F. Gordon, T. Scheffler and M. Stede, eds, Frontiers in Artificial Intelligence and Applications, Vol. 287: , IOS Press, (2016) , pp. 207–218.
G. Charwat, W. Dvořák, S.A. Gaggl, J.P. Wallner and S. 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.
M. Davis, G. Logemann and D. Loveland, A machine program for theorem proving, Communications of the ACM 5: (7) ((1962) ), 394–397. doi:10.1145/368273.368557.
Y. Dimopoulos and A. 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.
S. Doutre and J. Mengin, Preferred extensions of argumentation frameworks: Query answering and computation, in: Proceedings of the 1st International Joint Conference on Automated Reasoning, IJCAR 2001, R. Goré, A. Leitsch and T. Nipkow, eds, Lecture Notes in Computer Science, Vol. 2083: , Springer, (2001) , pp. 272–288.
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.
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.
W. Dvořák, M. Järvisalo, J.P. Wallner and S. Woltran, Complexity-sensitive decision procedures for abstract argumentation, Artificial Intelligence 206: ((2014) ), 53–78. doi:10.1016/j.artint.2013.10.001.
W. Dvořák and S. 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.
S.A. Gaggl, T. Linsbichler, M. Maratea and S. 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), M. Thimm, F. Cerutti, H. Strass and M. Vallati, eds, (2016) , pp. 4–9. https://www.dbai.tuwien.ac.at/iccma17/Introducing_ICCMA17.pdf.
S.A. Gaggl, N. Manthey, A. Ronca, J.P. Wallner and S. 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.
M. Gebser, B. Kaufmann and T. Schaub, Conflict-driven answer set solving: From theory to practice, Artificial Intelligence 187: ((2012) ), 52–89. doi:10.1016/j.artint.2012.04.001.
M. 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.
M. Järvisalo and I. 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.
J. Lagniez, E. Lonca and J. 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.
B. 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.
B. 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.
Y. Lierler, Abstract answer set solvers, in: Proceedings of the 24th International Conference on Logic Programming, ICLP 2008, M.G. de la Banda and E. Pontelli, eds, Lecture Notes in Computer Science, Vol. 5366: , Springer, (2008) , pp. 377–391.
Y. 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.
Y. Lierler, Relating constraint answer set programming languages and algorithms, Artificial Intelligence 207: ((2014) ), 1–22. doi:10.1016/j.artint.2013.10.004.
Y. Lierler and M. 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.
Y. Lierler and M. Truszczynski, Modular answer set solving, in: Late-Breaking Developments in the Field of Artificial Intelligence, AAAI Workshops, Vol. WS-13-17: , AAAI, (2013) .
Y. Lierler and M. Truszczynski, Abstract modular inference systems and solvers, in: Proceedings of the 16th International Symposium on Practical Aspects of Declarative Languages, PADL 2014, M. Flatt and H. Guo, eds, Lecture Notes in Computer Science, Vol. 8324: , Springer, (2014) , pp. 49–64.
Y. Lierler and M. Truszczynski, An abstract view on modularity in knowledge representation, in: Proceedings of the 29th AAAI Conference on Artificial Intelligence, AAAI 2015, B. Bonet and S. Koenig, eds, AAAI Press, (2015) , pp. 1532–1538.
Y. Lierler and M. Truszczynski, On abstract modular inference systems and solvers, Artificial Intelligence 236: ((2016) ), 65–89. doi:10.1016/j.artint.2016.03.004.
S. Modgil and M.W.A. Caminada, Proof theories and algorithms for abstract argumentation frameworks, in: Argumentation in Artificial Intelligence, I. Rahwan and G.R. Simari, eds, Springer, (2009) , pp. 105–129.
R. Nieuwenhuis, A. Oliveras and C. 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.
S. Nofal, K. 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.
I. Rahwan and G.R. Simari (eds), Argumentation in Artificial Intelligence, Springer, (2009) . doi:10.1007/978-0-387-98197-0.
E.D. Rosa, E. Giunchiglia and M. Maratea, Solving satisfiability problems with preferences, Constraints 15: (4) ((2010) ), 485–515. doi:10.1007/s10601-010-9095-y.
R. Sebastiani, Lazy satisfiability modulo theories, Journal of Satisfiability, Boolean Modeling and Computation 3: (3–4) ((2007) ), 141–224.
M. Thimm and S. Villata, System descriptions of the first International competition on computational models of argumentation (ICCMA’15), 2015. arXiv:1510.05373.
M. Thimm and S. 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.
M. Thimm, S. Villata, F. Cerutti, N. Oren, H. Strass and M. 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.
B. 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.
J.P. Wallner, G. Weissenbacher and S. Woltran, Advanced SAT techniques for abstract argumentation, in: Proceedings of the 14th International Workshop on Computational Logic in Multi-Agent Systems, CLIMA 2013, J. Leite, T.C. Son, P. Torroni, L. van der Torre and S. Woltran, eds, Lecture Notes in Computer Science, Vol. 8143: , Springer, (2013) , pp. 138–154.