New stochastic local search approaches for computing preferred extensions of abstract argumentation

Abstract

Several efficient SAT-based methods for computing the preferred extensions in (abstract) argumentation frameworks (AF) are proposed lately. However, only complete SAT solvers have been exploited so far. It is a natural question that how the appealing stochastic local search (SLS) approach could advance the performance. In this paper, we developed two SLS algorithms for computing the preferred extensions in AF, and a complete one which combines the strength of the better one with complete SAT solvers. Our first SLS algorithm Ite-CCA_EP works by calling an SLS SAT solver Swcca in an iterative manner with adaptive heuristics. Our second SLS algorithm Inc-CCA_EP realized an incremental version of Swcca, specially designed for computing the preferred extensions in AF. Though Ite-CCA_EP and Inc-CCA_EP do not guarantee completeness, they notably outperform a state-of-the-art solver consistently on most benchmarks with non-empty preferred extensions. Experimental results also show that Inc-CCA_EP is more efficient than Ite-CCA_EP, which inspired the design of a novel complete algorithm called CCASAT_EP that uses Inc-CCA_EP as an efficient preprocessor. Further experiments show that CCASAT_EP is competitive to the state-of-the-art methods.

Keywords

Abstract argumentation stochastic local search preferred semantics

1. Introduction

Dung’s theory of (abstract) argumentation frameworks (AF) provides a general model for computational argumentation [18]. AF takes only the inter-relations of arguments into account on an abstract level. An AF consists of a set of arguments and the directed attack relations between them.

Charwat et al. present a selection of evaluation methods for AF, and they group these methods into two categories: the reduction approaches and the direct approaches [16]. In the reduction approaches, SAT-based argumentation systems show good efficiency on solving the reasoning problems in AF. For preferred semantics, CEGARTIX system [19] and ArgSemSAT system [13–15] are two representative SAT-based argumentation systems, which both rely on iteratively calling complete SAT solvers. Each of the above two systems is ranked 1st or 2nd in the SE-PR (determining some extension under preferred semantics), DS-PR (deciding whether the given argument is skeptical inferred under preferred semantics) and EE-PR (determining all extensions under preferred semantics) tracks of the first International Competition on Computational Models of Argumentation (ICCMA’15) [33].1

¹
http://argumentationcompetition.org/2015/

ArgSemSAT has also excellent performance on other tracks in the competition. Nofal et al. also propose some algorithms for decision problems in argument systems under preferred semantics, which are not SAT-based algorithms but direct algorithms [29]. SAT-based algorithms for computing preferred semantics always encode AFs to CNF formulae. Preferred extensions cannot be computed by a single call to a SAT solver using an encoding that is polynomial in the input. Both CEGARTIX and ArgSemSAT compute preferred extensions based on complete semantics. CEGARTIX encodes complete semantics function to corresponding CNF formula directly, which means that an argument is mapped to two values: in and out, and range variables are added which make the encoding CNF formula be polynomial in the size of the AF. However, ArgSemSAT encodes complete semantics function to corresponding CNF formula based on labelling, in which every argument has three values: in, out and undec. Besnard et al. introduce the methods of SAT encodings for admissible semantics, complete semantics and stable semantics etc. [4].

There are two popular kinds of algorithms for SAT: conflict driven clause learning (CDCL), and stochastic locals search (SLS). CDCL approaches evolved from famous DPLL, and many techniques have been integrated, such as clause-learning and backjumping [9,22,32], restart [1,31], as well as efficient branching heuristics [34]. SLS algorithms are typically incomplete i.e., they cannot determine with certainty that an input formula is unsatisfiable. However, SLS algorithms have surprising efficiency on finding solutions for satisfiable random instances. The efficiency of SLS algorithms mostly depend on the heuristic methods selected by them. An efficient heuristic method named configuration checking (CC) [12] has been proposed to handle the cycling problem, i.e., local search returns to a candidate solution that has been visited recently. Afterwards, the CC heuristics has been successfully applied to solving SAT [11,25] and Max-SAT [10,26]. The SLS algorithm Swcca (smoothed weighting and configuration with aspiration) [11] is designed based on the heuristics named configuration checking with aspiration (CCA), which is an improvement of CC heuristics, to solve SAT problems. It has the advantages of stable, easy modification and high efficiency. CCA heuristics enhances the CC heuristics with an aspiration mechanism, and allows a variable with a great score to be flipped even if its configuration is not changed. Compared to other SLS algorithms, Swcca has a high efficiency based on CCA heuristics. For example, in literature [11], the experiments on random 3-SAT instances show that Swcca2

http://lcs.ios.ac.cn/~caisw/SAT.html

significantly outperforms Sparrow2011 [2], the winner of the random satisfiable category of the SAT Competition 2011, which is considered to be the best local search solver for random 3-SAT instances at that time.

A preliminary version of this paper has been published in ECAI 2016 with short paper [28]. In literature [28], Inc-CCA_EP is introduced, but many details are omitted.

This paper contributes to compute Dung’s preferred extensions based on the SLS algorithm for SAT. Two novel approaches Ite-CCA_EP and Inc-CCA_EP are proposed, and we compare them with other state-of-the-art systems for random AF instances with non-empty preferred extensions. Because Ite-CCA_EP and Inc-CCA_EP do not know whether they have found all preferred extension or not, they cannot automatically terminate. That property is similar to SLS algorithms’ in Max-SAT [10,26], which cannot automatically terminate too. For those SLS algorithms, they are terminated manually, i.e. the cutoff time has to be determined.

Because of the high efficiency of SLS algorithms, integrating them to complete algorithms can improve the efficiency of complete algorithms. For example, CCAnr+glucose is ranked 2nd in “sequential, Hard-combinatorial SAT” track of SAT Competition 20143

http://www.satcompetition.org/2014/

(CCAnr is a SLS algorithm, and glucose is a complete SAT solver), and CCLS_to_akmaxsat is ranked 3rd in “Unweighted Max-SAT – Random” track of Max-SAT Evaluation 2015.4

⁴

http://www.maxsat.udl.cat/15/index.html

So we integrate Inc-CCA_EP served as preprocessors to complete algorithm, and design a novel complete algorithm CCASAT_EP for computing preferred extensions. Then we compare CCASAT_EP with the state-of-the-art AF systems CEGARTIX and ArgSemSAT for enumerating preferred extensions on random AF instances. Our methods for computing preferred extensions are designed based on computing all complete extensions. But CEGARTIX and ArgSemSAT can directly compute preferred extensions.

This paper is organized as follows. Section 2 recalls the basic concepts of argumentation frameworks and preferred semantics. Section 3 recalls the CCA heuristics and Swcca algorithm. Section 4 introduces the two proposed approaches while Section 5 describes the test setting and comments the experimental results. Section 6 concludes the paper.

2. Argumentation frameworks and preferred semantics

In this section, we introduce (abstract) argumentation frameworks [18] and recall the preferred semantics we study in this paper.

Definition 1.
An argumentation framework (AF) is a pair $F = (A, R)$ where A is a set of arguments and $R \subseteq A \times A$ is the attack relation. The pair $(a, b) \in R$ means that a attacks b, also denoted as $a \to b$ .
Definition 2.
Given an AF $F = (A, R)$ :
a set $S \subseteq A$ is conflict-free if $∄ a, b \in S$ s.t. $a \to b$ ;

an argument $a \in A$ is acceptable with respect to a set $S \subseteq A$ if $\forall b \in A$ s.t. $b \to a$ , $\exists c \in S$ s.t. $c \to b$ ;

a set $S \subseteq A$ is admissible if S is conflict-free and every element of S is acceptable w.r.t. S;

an admissible set $S \subseteq A$ is complete iff each argument which is acceptable w.r.t. S, belongs to S.

An argumentation framework semantics is defined as a function σ which maps each AF $F = (A, R)$ to a set $σ (F) \subseteq 2^{A}$ of extensions. Dung has introduced four fundamental semantics, namely complete, grounded, stable, preferred semantics [18]. The functions $adm$ , $com$ and $prf$ stand for admissible, complete and preferred extensions respectively.

Here we need to recall the function definitions of admissible, complete and preferred semantics only.
Definition 3.
Let $F = (A, R)$ be an AF. $cf (F)$ denotes the collection of conflict-free sets of F. For a conflict-free set $S \in cf (F)$ , it holds that:
$S \in adm (F)$ , if S is admissible;

$S \in com (F)$ , if S is complete;

$S \in prf (F)$ , if $S \in adm (F)$ and there is no $T \in adm (F)$ with $S \subset T$ .

Dung has also proved that: 1) each complete extension is an admissible extension, but not vice versa; 2) each preferred extension is a complete extension, but not vice versa [18]. The scale of each conjunctive normal form (CNF) formula encoded from complete semantics function is usually bigger than the scale of corresponding CNF formula encoded from admissible semantics function, and more variables will be created in the encoding of complete semantics function. SLS methods usually select variables to flip according to all heuristic values of all variables. So, more variables and clauses will reduce the efficiency of heuristic selections, and we attempt to compute all complete extensions based on computing admissible extensions firstly, and then compute preferred extensions based on complete extensions.

A CNF formula is a conjunction of clauses, normally expressed as a set. For a CNF formula Φ, a model is a complete assignment which satisfies all clauses in Φ. Given a CNF formula, the SAT problem consists in determining whether there is any model for it or not.

In this paper, we use $V (G)$ to denote the set of all variables appearing in the CNF formula G. Given an AF $F = (A, R)$ , a key problem of instantiating the SAT-based framework is how the AF reasoning tasks are encoded as CNF formulae. Let $φ_{adm} (F)$ be the CNF formula which corresponds to the expression of admissible semantics of F. Then the set of variables $V (φ_{adm} (F)) = {v_{a} ∣ a \in A}$ is in correspondence with A. The intuition behind a model of $φ_{adm} (F)$ is that $v_{a}$ is true iff a is in an admissible extension. $φ_{adm} (F)$ is shown as follows [4]: $\begin{matrix} (1) & \begin{matrix} φ_{adm} (F) \\ = \underset{(b, a) \in R}{⋀} ((\neg v_{a} \lor \neg v_{b}) \\ \land (\neg v_{a} \lor \underset{(c, b) \in R}{⋁} v_{c})) . \end{matrix} \end{matrix}$

Obviously, the right-hand side of formula (1) is a CNF formula. Given a model P, let $α (P)$ be the set of positive literals in P. Then, a model P of $φ_{adm} (F)$ is in correspondence with a preferred extension of F iff there is no model Q with $α (P) \subset α (Q)$ .

In formula (1), if every variable is assigned to 0, $φ_{adm} (F)$ is satisfiable. The admissible extension corresponding to above model is empty, and empty admissible extension appears in all $φ_{adm} (F)$ . Our SLS algorithms assume the preferred extension to be non-empty. So in order to avoid finding above model, we associate the clause $⋁_{a \in A} v_{a}$ with $φ_{adm} (F)$ . we use $φ_{adm - ne} (F)$ to represent above formula, and it is shown as follows: $\begin{matrix} (2) & \begin{matrix} φ_{adm - ne} (F) \\ = \underset{(b, a) \in R}{⋀} ((\neg v_{a} \lor \neg v_{b}) \\ \land (\neg v_{a} \lor \underset{(c, b) \in R}{⋁} v_{c})) \land \underset{a \in A}{⋁} v_{a} . \end{matrix} \end{matrix}$

Algorithm 1
Simplification

Based on formula (2), we can compute admissible extensions which are non-empty. Obviously, $⋁_{a \in A} v_{a}$ contains all variables in $φ_{adm - ne} (F)$ . So that is a very long clause. Actually, short clauses can play a greater role in SAT solver. That is why SAT solvers with clause-learning expect to learn more short clauses [32]. We can use Lemma 1 to simplify this clause.
Lemma 1.
Given two clauses $l \lor C_{i}$ and $\neg l \lor C_{j}$ , if $C_{i} ⊧ C_{j}$ , ${l \lor C_{i}, \neg l \lor C_{j}} \equiv {l \lor C_{i}, C_{j}}$ .
Proof.
$C_{i} ⊧ C_{j}$ , so $l \lor C_{i} ⊧ l \lor C_{j}$ . According to extension rule [24], ${l \lor C_{j}, \neg l \lor C_{j}} \equiv {C_{j}}$ , so ${l \lor C_{i}, \neg l \lor C_{j}} \equiv {l \lor C_{i}, C_{j}}$ is established. □

In formula (1), there are only two kinds of clauses: one kind of clauses contains exactly two negative literals, the other kind of clauses contains one negative literal and some other positive literals (the number of positive literals can be 0). If we add some new clause in which all literals are positive to $φ_{adm - ne} (F)$ , this clause can also be easily simplified by Lemma 1.

Original clauses can also be simplified based on Lemma 1. So we design a simplifying process based on Lemma 1, which is described in Algorithm 1.
3. CCA heuristics and Swcca algorithm

The basic concept of CC is configuration which establishes a connection between a variable with truth values of all its neighboring variables. We use $V (Φ)$ to denote the set of all variables that appear in the CNF formula Φ. $N (x) = {y ∣ y \in V (Φ) and y occurs in at least one clause with x}$ is the set of all neighboring variables of a variable x. The formal definition is given as follows:

Definition 4 ([11]).

Given a CNF formula Φ and s the current assignment to $V (Φ)$ , the configuration of a variable $v \in V (Φ)$ is a vector $C_{v}$ consisting of truth values of all variables in $N (v)$ under s (i.e., $C_{v} = s |_{N (v)}$ , which is the assignment restricted to $N (v)$ ).

Given a CNF formula Φ, the CC heuristics can be described as follows [11]: When selecting a variable to flip, for a variable $v \in V (Φ)$ , if the configuration of v has not been changed since v’s last flip, which means the circumstance of v never changes, then it is forbidden to be flipped.

In the implementation of CC, each clause $c \in Φ$ is associated with a positive integer number $w (c)$ as its weight. $cost (Φ, s)$ denotes the total weight of all unsatisfied clauses under the assignment s. Let $score (v) = cost (Φ, s) - cost (Φ, s^{'})$ , measuring the benefit of flipping v, where $s^{'}$ is obtained from s by flipping v. Any element in the array confChange is an indicator for a variable. $confChange [v] = 1$ means the configuration of variable v has been changed since v’s last flip; and $confChange [v] = 0$ means the configuration of variable v has not been changed since v’s last flip.

CC heuristics: A configuration changed decreasing (CCD) variable v is a variable with both $confChange [w] = 1$ and $score (v) > 0$ . The CC heuristics switches between the greedy mode and the diversification mode. In the greedy mode, the CCD variable with the greatest score is selected. If there are no CCD variables, CC switches to diversification mode, where clause weights are updated, and the oldest variable in a uniformly random unsatisfied clause is picked to flip.

CCA heuristics: A significant decreasing (SD) variable v is a variable with $score (v) > g$ , where g is a positive integer large enough. In the literature [11], g is set to the averaged clause weight w over all clauses. CCA heuristics gives a chance to SD variables. The SD variable with the greatest score is selected to flip if there are no CCD variables. If there are neither CCD variables nor SD variables, CCA switches to diversification mode just like CC. In diversification mode, CCA randomly selects a unsatisfied clause C according to the weights of all unsatisfied clauses. Then CCA selects the oldest variable in C according to the timestamp array.

The basic process of Swcca is as follows: Beginning with a random complete assignment of truth values to variables; initializing heuristic information; in each subsequent search step, a variable is chosen and flipped based on CCA heuristics, and updating heuristic information. For more details, please refer to the literature [11].

4. Enumerating preferred extensions based on CCA heuristics

We are now in a position to introduce our first proposed procedure, called Ite-CCA_EP and listed in Algorithm 2, to enumerate the preferred extensions of an AF $F = (A, R)$ based on iteratively calling Swcca.

Algorithm 2

Ite-CCA_EP

In subsequent algorithms, $flip (s, v)$ is a function which flips v in s and returns the flipping result. Ite-CCA_EP enumerates preferred extensions by starting from the identified admissible extension. After searching an admissible extension, it expands this admissible extension to get a superset of this admissible extension, which is in correspondence with a complete extension. Ite-CCA_EP only saves the complete extensions which are not some subset of any other complete extension in searching process. So if all complete extensions have been searched by Ite-CCA_EP, Ite-CCA_EP can get all preferred extensions according to the definition of preferred semantics.

In order to improve the efficiency of searching process, we use Strategy 1 to further simplify $φ_{adm - ne} (F)$ . We use Strategy 2 to expand an admissible extension, the result is in correspondence with an complete extension.

Strategy 1.

Unit propagation is executed in Line 3 (in Algorithm 2). Some arguments may attack themselves, and these arguments will not appear in any conflict-free extension. So those arguments will not appear in any admissible extension or preferred extension. The formal description of creating unit clauses in encoding process is that: Given an AF $F = (A, R)$ , $\neg v_{a} \in φ_{adm - ne} (F)$ , if $\exists a \in S$ s.t. $a \to a$ . Unit propagation can be completed in polynomial time. So we employ $Φ = unit - propagation (Φ_{0})$ to reduce the scale of $φ_{adm - ne} (F)$ , in which Φ is the reduced result. Strategy 1 can reduce the search time of single calling of Swcca. The basic process of unit-propagation is described as Algorithm 3.

Algorithm 3

unit-propagation

Strategy 2.

After Ite-CCA_EP searches a model T which is in correspondence with an admissible extension S, if T is still a model after flipping any negative literal in it, we flip that negative literal and can get a superset of S. Strategy 2 is completed in Lines 10–11 (in Algorithm 2). After executing Strategy 2, we can get a model $T^{'}$ in which only flipping any negative literal will falsify Φ. It should be noted that the admissible extension corresponding to $T^{'}$ may not be a preferred extension, because after simultaneously flipping two or more negative literals in $T^{'}$ , $T^{'}$ may still be a model. But, actually, $T^{'}$ is in correspondence with a complete extension.

Theorem 1.

After executing Strategy 2 in Lines 10–11 (in Algorithm 2 ), the model is in correspondence with a complete extension.

Proof.

Let S be the admissible extension corresponding to the model T after executing Strategy 2. Then, for each argument $a \notin S$ , $S \cup {a}$ is not an admissible extension. So each argument which does not belong to S, is not acceptable with respect to S or has attack relation with S. Because S is conflict-free, each argument which has attack relation with S is not acceptable with respect to S. S is conflict-free and every element of S is acceptable with respect to S. So each argument which is acceptable with respect to S, belongs to S. Theorem 1 is established. □

In Algorithm 2, the heuristic information appeared in Ite-CCA_EP mainly contains the scores of all variables, the weights of all clauses and the time stamps of all flipping variables [11]. All possible extensions will be saved as $E_{p}$ in Line 1. $φ_{adm - ne} (F)$ is constructed in Line 2. Strategy 1 is executed in Line 3. A random complete assignment is created in Line 4. The heuristic information is initialized in Lines 5–7. Since Ite-CCA_EP is an incomplete algorithm, it does not know whether all possible preferred extensions have been found or not. So, we use maxsteps to control the end of Ite-CCA_EP in Line 8. Whether the current s is a model of $φ_{adm - ne} (F)$ or not is judged in Line 9. Strategy 2 is implemented in Lines 10–11. In Line 12, merge function is used to add a new complete extension to $E_{p}$ , the basic process is implemented by judge whether the new complete extension is a superset of some extension in $E_{p}$ . New complete extension is added to $E_{p}$ , if it is not a subset of any extension in $E_{p}$ . In order to avoid searching an admissible extension which is the subset of any admissible extension searched before, we simplify Φ after adding $⋁_{\neg v i \in s} v_{i}$ to it in Line 13 by calling simplification function. After a complete extension has been found, all parameters are initialized again in Lines 14–17. It employs CCA heuristics to pick flipping variable in Line 18, in which v is the picking result. In Lines 19–21, it executes the flipping works just like Swcca.

After adding $⋁_{\neg v i \in s} v_{i}$ to Φ, Ite-CCA_EP initializes a complete assignment and heuristic information again in Lines 14–17. So many heuristic values calculated before will be lost. The lost heuristic values can play an important role for follow-up search, so incremental idea has been adopted to many solvers for different problems [21,23,30]. In order to reuse these heuristic values, we design Inc-CCA_EP algorithm based on an incremental implementation of Swcca. Inc-CCA_EP is listed in Algorithm 4.

Algorithm 4

Inc-CCA_EP

In Algorithm 4, we also add Strategy 1 and Strategy 2 to Inc-CCA_EP. The differences between Inc-CCA_EP and Ite-CCA_EP are that the former updates heuristic information after flipping a variable in Strategy 2 in Lines 12–13, and adds heuristic information of new clause after adds this clause to Φ in Lines 16–17. In Inc-CCA_EP, heuristic information is initialized only once, and it conserves all heuristic information after finding a model.

Theorem 2.

If the CNF formula Φ in Algorithm 4 (resp. Algorithm 2 ) is unsatisfiable after executing Inc-CCA_EP (resp. Ite-CCA_EP), Inc-CCA_EP (resp. Ite-CCA_EP) finds all preferred extensions of the input AF.

Proof.

After executing Inc-CCA_EP, that Φ in Algorithm 2 or Algorithm 4 is unsatisfiable means there are no more admissible extensions. If there are no more admissible extensions, Strategy 2 can guarantee that any admissible extension of input AF is a subset of some extension in $E_{p}$ or contained by $E_{p}$ , and merge function can get all preferred extensions from the searching result of Inc-CCA_EP or Ite-CCA_EP. So Inc-CCA_EP (resp. Ite-CCA_EP) finds all preferred extensions if Φ is unsatisfiable. Theorem 2 is established. □

Now, we introduce the complete CCASAT_EP algorithm which is listed in Algorithm 5.

Algorithm 5

CCASAT_EP

In Algorithm 5, CCASAT_EP use Inc-CCA_EP to search for complete extensions firstly, and the result is saved as $E_{p}$ . The parameter maxsteps is used to control the end of Inc-CCA_EP. Because the executing time of Inc-CCA_EP only relies on maxsteps, a good maxsteps is required for guaranteeing the efficiency of CCASAT_EP. It should make the value of maxsteps as close to the actual search time of Inc-CCA_EP as possible. The actual search time of Inc-CCA_EP begins from start to end of last solution searched by it. After Inc-CCA_EP exhausts all maxsteps times of searching attempts, CDCL approach is invoked. It uses complete SAT solver to decide the satisfiability of Φ in Line 4, and Φ is the CNF formula after executing Inc-CCA_EP. We also use Strategy 2 to accelerate CCASAT_EP in Lines 5–6. $merge (E_{p}, s)$ in Line 7 is same as the merge functions in Ite-CCA_EP and Inc-CCA_EP. CCASAT_EP stops when Φ is unsatisfiable, which is controlled by the while loop in Line 4.

Theorem 3.

CCASAT _EP is a complete algorithm for enumerating preferred extensions.

Proof.

First we show that termination is guaranteed. CCASAT_EP adds $⋁_{\neg v i \in s} v_{i}$ to Φ in Line 8. That can guarantee that CCASAT_EP does not find any subset of the preferred extension corresponding to this model. So the number of models of Φ is decreasing with the loop in Line 4. CCASAT_EP can terminate if the number of models of Φ is 0. Because CCASAT_EP and Inc-CCA_EP add $⋁_{\neg v i \in s} v_{i}$ to Φ after finding a complete extension, there is no complete extension which is a superset of any complete extension in $E_{p}$ after Φ is unsatisfiable. If Φ is unsatisfiable, there also must not be any complete extension which is incomparable to the ones in $E_{p}$ . So merge function can get all preferred extensions. Then Theorem 3 is established. □

Inc-CCA_EP and Ite-CCA_EP are two incomplete algorithms for enumerating preferred extensions, so it is not clear whether the found preferred extensions are really preferred extensions. Accuracy rate is an important parameter to measure incomplete algorithms, which is the proportion of instances which are correctly solved in all instances. Swcca has high efficiency and accuracy rate. For example, Swcca has 100% of accuracy rate on the random large 3-SAT instances with 35000 variables from the SAT Competition 2011 [11].

5. Experimental results

CEGARTIX5

⁵
http://www.dbai.tuwien.ac.at/research/project/argumentation/cegartix/

and ArgSemSAT6

⁶

http://sourceforge.net/projects/argsemsat/

are two efficient AF reasoners for enumerating preferred extensions, and they are ranked 1st and 2nd on EE-PR track of ICCMA’15 respectively, so we compare our approaches with them. CEGARTIX and ArgSemSAT can directly compute preferred extensions, which are different from our methods designed based on computing complete extensions. Dimopoulos et al. have designed an SLS algorithm for stable semantics, but they have not implemented SLS algorithm for preferred semantics [17], so we do not compare our approaches with their works. To assess empirically the performance of two proposed approaches with respect to CEGARTIX and ArgSemSAT, we do the experiments on benchmarks which are used in ICCMA’15 firstly.

5.1. Testing Ite-CCA_EP and Inc-CCA_EP on benchmarks in ICCMA’15

Table 1
A comparison between Inc-CCA_EP with the state of the art

Benchmarks Inc-CCA_EP Ite-CCA_EP Com-CCA_EP CEGARTIX ArgSemSAT

solving time sat-time

gr-small(24) 24.35(24) 0.137 26.92(24) 28.41(24) 33.69 27.65

gr-medium(24) 109.47(24) 0.329 113.92(24) 117.36(24) 101.77 68.95

gr-large(24) 768.66(24) 2.864 778.83(24) 793.93(24) 553.31 338.64

st-small(24) 53.06(18) 461.501 68.73(18) 50.88(19) 344.007 3148.88

st-medium(24) 68.95(20) 306.151 169.53(20) 157.78(18) 412.789 1909.48

scc-small(22) 0.23(22) 0.07 0.46(22) 0.55(22) 1.74 2.68

scc-medium(18) 3.36(18) 0.076 3.89(18) 4.42(18) 8.26 11.76

scc-large(16) 1.45(15) 0.305 4.94(14) 6.76(12) 28.14 104.63

Benchmarks	Inc-CCA_EP	Ite-CCA_EP	Com-CCA_EP	CEGARTIX	ArgSemSAT
gr-small(24)	24.35(24)	0.137	26.92(24)	28.41(24)	33.69	27.65
gr-medium(24)	109.47(24)	0.329	113.92(24)	117.36(24)	101.77	68.95
gr-large(24)	768.66(24)	2.864	778.83(24)	793.93(24)	553.31	338.64
st-small(24)	53.06(18)	461.501	68.73(18)	50.88(19)	344.007	3148.88
st-medium(24)	68.95(20)	306.151	169.53(20)	157.78(18)	412.789	1909.48
scc-small(22)	0.23(22)	0.07	0.46(22)	0.55(22)	1.74	2.68
scc-medium(18)	3.36(18)	0.076	3.89(18)	4.42(18)	8.26	11.76
scc-large(16)	1.45(15)	0.305	4.94(14)	6.76(12)	28.14	104.63

In order to test the effect of computing preferred extensions based on admissible semantics and Strategy 2, with respect to computing preferred extensions based on complete semantics, we simply implement the algorithm Com-CCA_EP which is an alternative of the algorithm with the encoding of complete semantics instead of encoding of admissible semantics and Strategy 2. Com-CCA_EP also adopts incremental searching process. Our experiments are conducted on the PC with a quad-core Intel(R) Core(TM) i7-3700, 4 GByte RAM and Ubuntu 14.04 operating system. Because Inc-CCA_EP, Ite-CCA_EP and Com-CCA_EP cannot finish their search processes automatically even if they have found all preferred extensions, we use actual search time to measure their efficiencies.

The comparing results on benchmarks in ICCMA’15 are shown in Table 1. In Table 1, the numbers in brackets in first column represent the size of corresponding kind of instances, and the numbers in brackets in second column, fourth column and fifth column represent the numbers of instances which are correctly solved by Inc-CCA_EP, Ite-CCA_EP and Com-CCA_EP respectively. Whether the found preferred extensions by Inc-CCA_EP or Ite-CCA_EP are really preferred extensions or not can be judged based on Theorem 2, this method is also applicable for Com-CCA_EP. In Table 1, the solving time of SLS algorithms begins from start to end of last solution searched by it. The SLS algorithms do not terminate from themselves. If the time since the last solution searched by some SLS algorithm exceeds 100 s, we terminate this SLS algorithm. Then we can record the time in which last solution is searched by Inc-CCA_EP, when we use Inc-CCA_EP to solve some instance. The above method is also applicable for Ite-CCA_EP and Com-CCA_EP. The sat-time of Inc-CCA_EP is used to compute remainder admissible extensions based on CDCL approach, this process is executed as Lines 4–9 in Algorithm 5. We list the sum time of solving all instances in each row for every solver, since the instances with same kind are greatly different. The unit of time is second.

From Table 1, we can see that Inc-CCA_EP and Ite-CCA_EP have similar accuracy rate, but the solving time of Inc-CCA_EP is evidently shorter than Ite-CCA_EP’s. Both Inc-CCA_EP and Ite-CCA_EP can not completely solve instances in st-small and st-medium, the reason is that methods of local search are incomplete, and they are not appropriate to solve instances with some special structures. Comparing Inc-CCA_EP with Com-CCA_EP, we can see that Inc-CCA_EP is evidently better than Com-CCA_EP. So, computing preferred extensions based on admissible semantics and Strategy 2 is more suitable for SLS algorithms.

Based on the comprehensive consideration on searching time and sat-time of Inc-CCA_EP, we can see that, Inc-CCA_EP has the best efficiency for solving the instances in scc-small and scc-medium. The efficiency of Inc-CCA_EP is better than ArgSemSAT’s for the instances in st-small and st-medium, and worse than CEGARTIX’s for these instances. Overall, ArgSemSAT has best efficiency for the instances with gr kind, and the efficiency of Inc-CCA_EP is worst for these instances.

The capacity of benchmarks in ICCMA’15 is too small, and the distribution of these benchmarks is not regular, which causes that we can not set appropriate maxsteps for CCASAT_EP on these instances. So in order to get appropriate maxsteps for CCASAT_EP, we further test Inc-CCA_EP on benchmarks, which are regularly generated with different graph-models, in literature [8]. Because Ite-CCA_EP and Com-CCA_EP is far slower than Inc-CCA_EP, so we do not test the ability of Ite-CCA_EP in remaining experiments.

5.2. Testing Inc-CCA_EP on benchmarks with different graph-models

In literature [8], benchmarks are generated with three different graph-models which include Erdős–Rényi, Kleinberg and Barabasi–Albert. The above graph-models are also used to compare other reasoning-tools in AF [5–7].

In the Erdős–Rényi model [20], a graph is constructed by randomly connecting n nodes. Each edge is included in the graph with probability p independent from every other edge. Clearly, as p increases from 0 to 1, the model becomes more likely to include graphs with more edges. In [8], Bistarelli et al. set $p = 2.5 \times log (n) \div n$ .

The Kleinberg [27] (small-world) graph-model adds a number of directed long-range random links to an $n \times n$ lattice network (vertices as nodes of a grid). Links have a non-uniform distribution that favours edges to close nodes over more distant ones. In literature [8], each node u has four local connections, one to each of its neighbours, and in addition 1 or more long-range connection to some node v, where v is randomly chosen according to probability proportional to $d^{- θ}$ where d is the lattice distance between u and v and θ is the clustering exponent. Bistarelli et al. set $θ = 0.9$ , in order to have a high clustering coefficient. Given a node, each link is directed towards its neighbours: edges are created in both directions between neighbours. Each long-distance connection has a tail in the considered node.

During the generation of Barabasi–Albert (scale-free) graphs, at each time step a new vertex is created and connected to existing vertices according to the principle of “preferential attachment” [3], whereby vertices with higher degree have a higher probability of being selected for attachment. At a given step, the probability p of creating an edge between an existing vertex v and the newly added vertex is $p = (degree (v) + 1) = (e + n)$ . e and n are respectively the number of edges and nodes currently in the network. Thus, p is not an input parameter. Scale-free networks are widely observed in natural and human-made systems, including the Internet, the World Wide Web, citation networks, and social networks. Big hub-nodes in scale-free networks are responsible for the so-called small-world phenomenon, where most nodes can be reached from every other by a small number of hops.

In order to set appropriate maxsteps for CCASAT_EP, we need to know the solving ability of Inc-CCA_EP on different graph-models. In our experiments, maxsteps used in CCASAT_EP is replaced by cutoff time which is relatively stable and easily observed in experiments. Cutoff time used in CCASAT_EP means that the executing time of Inc-CCA_EP in CCASAT_EP is fixed as cutoff time.

We are fortunate to get all experimental instances in [8]. In those instances, we omit some easy instances which can be solved in less than 0.01 s by CEGARTIX, and also omit some hard instances which cannot be solved by any of the solvers. Inc-CCA_EP can not solve instances with empty preferred extension, so we test it on instances with non-empty preferred extensions in this part. The result is shown as Table 2. In Table 2, we use ER, Kle and BA to indicate Erdős–Rényi, Kleinberg and Barabasi–Albert respectively. The data in the second column of Table 2 contains the argument number of corresponding instances, and the instance numbers which are listed in brackets. The unit of time is second.

Table 2
Searching time of Inc-CCA_EP on instances with different graph-models

Benchmarks Inc-CCA_EP

solved max-sr-time avg-sr-time

ER 200(83) 73 3.24 0.12

300(84) 69 10.09 0.37

400(83) 60 13.22 2.18

500(86) 62 190.05 31.93

Kle 36(100) 100 0.2 0.1

49(100) 100 46.20 23.10

BA 1200(91) 91 0.02 0.02

1700(89) 89 0.03 0.02

2500(86) 86 0.04 0.03

5000(88) 88 0.13 0.10

10000(89) 89 0.55 0.47

20000(89) 89 2.09 1.96

Benchmarks	Inc-CCA_EP
ER	200(83)	73	3.24	0.12
300(84)	69	10.09	0.37
400(83)	60	13.22	2.18
500(86)	62	190.05	31.93
Kle	36(100)	100	0.2	0.1
49(100)	100	46.20	23.10
BA	1200(91)	91	0.02	0.02
1700(89)	89	0.03	0.02
2500(86)	86	0.04	0.03
5000(88)	88	0.13	0.10
10000(89)	89	0.55	0.47
20000(89)	89	2.09	1.96

In Table 2, max-sr-time and avg-sr-time represent the maximum searching time and average searching time of Inc-CCA_EP for corresponding kind of instances. From Table 2, we can get the accuracy rate, maximum searching time and average searching time of Inc-CCA_EP for different graph-models.

For Erdős–Rényi graph-models, Inc-CCA_EP can not solve all instances, and the solving time is not stable, which means that differences of solving time for instances of same kind are great. For example, for the instances with 500 arguments, the maximum searching time of Inc-CCA_EP is 190.05 s, but the average searching time is 31.93 s. The running time of CCASAT_EP consists of the cutoff time for Inc-CCA_EP and the time of calling complete SAT solver. The solving time of Inc-CCA_EP is greatly different on instances of Erdős–Rényi graph-models. If we set a long cutoff time for Inc-CCA_EP, much time is wasted for easy instances. If we set a short cutoff time for Inc-CCA_EP, the performance of Inc-CCA_EP for solving hard instances is suppressed, and the time of calling complete SAT solver is long for most hard instances. The instable searching time leads the situation that we can not set cutoff as maximum searching time or average searching time. So, we should set cutoff time of Inc-CCA_EP in CCASAT_EP less than the average searching time for Erdős–Rényi graph-models.

For Kleinberg graph-model, Inc-CCA_EP solves all instances, and the solving time is relatively stable. The maximum searching time is twice of average searching time. In order to reduce wasted searching time of Inc-CCA_EP and the time of calling CDCL approach, we should set the cutoff time of CCASAT_EP a little bigger than average searching time of Inc-CCA_EP for Kleinberg graph-model.

For Barabasi–Albert graph-model, Inc-CCA_EP solves all instances, and the solving time is stable. The maximum searching time is close to average searching time. So, we should set the cutoff time of CCASAT_EP as maximum searching time of Inc-CCA_EP for Kleinberg graph-model. Then the performance of Inc-CCA_EP can be sufficiently employed.

5.3. Testing CCASAT_EP on benchmarks with different graph-models

In order to show the impact of cutoff time on the performance of CCASAT_EP and identify the value of cutoff time for different graph-models, we test the efficiency of CCASAT_EP with different cutoff time for three graph-models. There are many instances with different scales in each graph-models, so we select one kind of instances for each graph-models. The results are shown as Figs 1–3.

Fig. 1.

The impact of cutoff time on the performance of CCASAT_EP for instances with 400 arguments in Erdős–Rényi graph-model.

Fig. 2.

The impact of cutoff time on the performance of CCASAT_EP for instances with 36 arguments in Kleinberg graph-model.

Fig. 3.

The impact of cutoff time on the performance of CCASAT_EP for instances with 10000 arguments in Barabasi–Albert graph-model.

In Figs 1–3, when the cutoff time is 0, CCASAT_EP solves instances without preprocessing of Inc-CCA_EP. We can see that, for all kinds of graph-models, the preprocessing of Inc-CCA_EP can improve the efficiency of CCASAT_EP, if the value of cutoff time is appropriate.

For Erdős–Rényi graph-models, the solving time of CCASAT_EP is least when the value of cutoff time is approximately equal to 0.436 s which is one fifth of average searching time of Inc-CCA_EP for this kind of instances. For Kleinberg graph-model, the solving time of CCASAT_EP is least when the value of cutoff time is approximately equal to 0.15 s which is 1.5 times of average searching time of Inc-CCA_EP for this kind of instances. For Barabasi–Albert graph-model, the solving time of CCASAT_EP is least when the value of cutoff time is approximately equal to 0.55 s which is the maximum searching time of Inc-CCA_EP for this kind of instances.

Table 3

A comparison between CCASAT_EP with the state of the art

Benchmarks		CCASAT_EP		CEGARTIX	ArgSemSAT

		cutoff time	solving time
Erdős–Rényi	200(100)	0.010	0.063	0.063	0.073
	300(100)	0.061	0.307	0.466	0.898
	400(100)	0.436	5.883	8.053	21.142
	500(100)	10.643	290.249	276.420	1477.267
Kleinberg	36(100)	0.15	0.241	1.896	8.800
Kleinberg	49(100)	34.68	37.862	191.482	844.448
Barabasi–Albert	1200(91)	0.02	0.051	0.206	0.394
	1700(89)	0.03	0.072	0.294	0.592
	2500(86)	0.04	0.106	1.056	0.691
	5000(88)	0.13	0.264	1.111	1.354
	10000(89)	0.56	0.879	2.592	2.988
	20000(89)	2.09	2.984	6.240	6.942

We get all appropriate cutoff time of CCASAT_EP for different graph-models through experimentally evaluating. Then we test the efficiency of CCASAT_EP on three graph-models. The results are shown as Table 3, and the solving time of the state of the art is also listed. The best cutoff time of CCASAT_EP for different graph-models is listed in third column. The data in second column of Table 3 contains the argument number of corresponding instances, and the instance numbers which are listed in brackets. The runtime in Table 3 is average solving time of each solver in each row. The unit of time is second.

From Table 3, we can see that, CCASAT_EP has the best efficiency for most instances. Overall, CCASAT_EP is the best algorithms for enumerating preferred extensions of three graph-models. CEGARTIX ranks second, and ArgSemSAT ranks third.

For Erdős–Rényi graph-models, the efficiency of CCASAT_EP is close to CEGARTIX’s and evidently better than ArgSemSAT’s. Though we set cutoff time for CCASAT_EP as one third of average searching time of Inc-CCA_EP, it still wasted much time for useless searching for some easy instances and some instances with empty preferred extension. For some hard instances and unsolved instances of Inc-CCA_EP, the cutoff time is relative small, so CCASAT_EP calls many times of CDCL approach. So, the solving time of CCASAT_EP is a little longer than CEGARTIX’s for Erdős–Rényi graph-models. We set cutoff time according to the number of arguments in this paper. There are many parameters, such as the frequency of attacks among arguments, density, treewidth etc., which effect the difficulties of AF instances. Existing benchmarks cannot support us to set cutoff time for Inc-CCA_EP according to above parameters, and we will solve this problem in next works. ArgSemSAT exploits encoding method based on labelling, in which every argument has three values. ArgSemSAT integrates two alternative SAT solvers: PrecoSAT and Glucose, which are different from minisat used in CEGARTIX and CCASAT_EP. The encoding method and SAT solver used in CEGARTIX and CCASAT_EP are more efficient for instances with Erdős–Rényi graph-models with respect to ArgSemSAT, so ArgSemSAT is weaker than CEGARTIX and CCASAT_EP.

For Kleinberg graph-model and Barabasi–Albert graph-model, the searching time of Inc-CCA_EP is stable, and Inc-CCA_EP efficiently solves all instances. So, CCASAT_EP efficiently solves those instances with our cutoff time. We can see that, CCASAT_EP always has the best efficiency for instances with above two graph-models.

We further give the computing functions of cutoff time for different graph-models. Because Kleinberg graph-model only has two appropriate kinds of instances which are listed in Table 3, we don’t need to give the computing function of cutoff time for this graph-model. We get the computing functions of cutoff time for Erdős–Rényi and Barabasi–Albert graph-models through curve fitting, and the curve fitting results are shown as Fig. 4 and Fig. 5. In Fig. 4 and Fig. 5, the scatters are the cutoff time listed in Table 3, and the curves are in correspondence with computing functions of cutoff time.

Fig. 4.

The curve fitting result of cutoff time for Erdős–Rényi.

Fig. 5.

The curve fitting result of cutoff time for Barabasi–Albert graph-models.

The computing function of cutoff time for Erdős–Rényi graph-model is shown as follows: $\begin{matrix} cter = 0.0000012 \times e^{0.032 \times | A |}, \end{matrix}$ in which, $| A |$ is the argument number, and the unit of $cter$ is second.

The computing function of cutoff time for Barabasi–Albert graph-model is shown as follows: $\begin{array}{rcl} ctba & = & 0.000000005 \times | A |^{2} \\ + 0.000005 \times | A | + 0.0012, \end{array}$ in which, $| A |$ is the argument number, and the unit of $ctba$ is second.

Though we have given the computing functions of cutoff time, and CCASAT_EP is the best algorithms for enumerating preferred extensions of three graph-models, the cutoff time is not unified, which means that the cutoff time cannot be set if the graph-model of input instances is unknown. That is the weakness of CCASAT_EP. This weakness also belongs to other similar algorithms for solving SAT or Max-SAT. In SAT Competition and Max-SAT Evaluation, the instances are usually hard for all solvers, and the solving ability (the number of instances solved in fixed time) is the unique standard to compare different solvers. So, both CCLS_to_akmaxsat and CCEHC_to_akmaxsat (which rank 2nd and 3th in many tracks of Max-SAT Evaluation respectively) set the cutoff time of preprocessing as 10 s directly. The existing AF benchmarks are relatively simple for all solvers, and we focus on the comparison of efficiency of different solvers, so we must set appropriate cutoff time in CCASAT_EP for instances with different graph-models. We believe that more and more hard AF instances will be found, then we can fix cutoff time for CCASAT_EP (just like CCLS_to_akmaxsat and CCEHC_to_akmaxsat) to compare its solving ability with other solvers’.

6. Conclusions

In this paper, we innovatively exploit stochastic local search for enumerating preferred extensions in abstract argumentation. Two algorithms: Ite-CCA_EP and Inc-CCA_EP are proposed based on Swcca for enumerating preferred extensions in abstract argumentation. Ite-CCA_EP is realized based on iterative calling of Swcca, so much useful heuristic information calculated in the iterative process is neglected. Inc-CCA_EP is an improvement of Ite-CCA_EP, which adopts incremental idea to call Swcca. Experimental results show that Inc-CCA_EP is better than Ite-CCA_EP.

Because Ite-CCA_EP and Inc-CCA_EP are designed based on stochastic local search, they cannot automatically terminate. Experimental results show that Inc-CCA_EP significantly outperform Ite-CCA_EP, and is better than the state-of-the-art systems on most AF instances with non-empty preferred extensions.

Learning from the success of CCAnr+glucose and CCLS_to_akmaxsat, we integrate Inc-CCA_EP as a preprocessor into complete algorithm, and CCASAT_EP is proposed. Through setting appropriate cutoff time, CCASAT_EP outperforms CEGARTIX and ArgSemSAT which are two best systems for enumerating preferred in abstract argumentation.

Lately, ICCMA 2017 has been conducted. In ICCMA 2017, more benchmarks with different graph-models are used. Based on the experiments in this paper, our methods will be also efficient for the benchmarks in ICCMA 2017 after appropriate cutoff time is set.

Next, we will attempt to further improve the ability of Inc-CCA_EP. The heuristic methods used in Inc-CCA_EP do not consider the special form in the CNF formulae converted by AF instances. So we intend to design better heuristic functions which make Inc-CCA_EP be more efficient for abstract argumentation. On the other hand, we intend to design new heuristic functions which consider some hard problems.

Footnotes

Acknowledgements

This work was supported by the National Natural Science Foundation of China under Grant Nos. 61300049, 61502197, 61503044 and 61763003; and the Natural Science Research Foundation of Jilin Province of China under Grant No. 20180101053JC.

References

Atseria,

J.K.

Fichte and

Thureley, Clause-learning algorithms with many restarts and bounded-width resolution, Journal of Artificial Intelligence Research 40 (2011), 353–373.

Balint and

Frohlich, Improving stochastic local search for SAT with a new probability distribution, in: Proceedings of the 13th Theory and Applications of Satisfiability Testing, Springer, Edinburgh, UK, 2010, pp. 10–15.

A.L.

Barabasi and

Albert, Emergence of scaling in random networks, Science 286(5439) (1999), 509–512. doi:10.1126/science.286.5439.509.

Besnard and

Doutre, Checking the acceptability of a set of arguments, in: Proceedings of the 10th International Workshop on Non-Monotonic Reasoning, Whistler, Canada, 2004, pp. 59–64.

Bistarelli,

Rossi and

Santini, Efficient solution for credulous/sceptical acceptance in lower-order Dung’s semantic, in: Proceedings of the 26th IEEE International Conference on Tools with Artificial Intelligence, IEEE Computer Society, Limassol, Cyprus, 2014, pp. 800–804.

Bistarelli,

Rossi and

Santini, Benchmarking hard problems in random abstract AFs: The stable semantics, in: Proceedings of the 5th Conference on Computational Models of Argument, IOS Press, Pitlochry, Scotland, 2014.

Bistarelli,

Rossi and

Santini, A first comparison of abstract argumentation reasoning-tools, in: Proceedings of the 21st European Conference on Artificial Intelligence, IOS Press, Prague, Czech Republic, 2014, pp. 969–970.

Bistarelli,

Rossi and

Santini, A comparative test on the enumeration of extension in abstract argumentation, Fundamenta Informaticae 140(3–4) (2015), 263–278. doi:10.3233/FI-2015-1254.

M.L.

Bonet and

Buss, Improved separations of regular resolution from clause learning proof systems, Journal of Artificial Intelligence Research 49 (2014), 669–703.

10.

Cai,

Luo,

Thornton and

Su, Tailing local search for partial MaxSAT, in: Proceedings of the 28th AAAI Conference on Artificial Intelligence, AAAI Press, Québec City, Québec, Canada, 2014, pp. 2623–2629.

11.

Cai and

Su, Configuration checking with aspiration in local search for SAT, in: Proceedings of the 26th AAAI Conference on Artificial Intelligence, AAAI Press, Toronto, Ontario, Canada, 2012, pp. 434–440.

12.

Cai,

Su and

Sattar, Local search with edge weighting and configuration checking heuristics for minimum vertex cover, Artificial Intelligence 75(9–10) (2011), 1672–1696. doi:10.1016/j.artint.2011.03.003.

13.

Cerutti,

P.E.

Dunne,

Giacomin and

Vallati, Computing preferred extensions in abstract argumentation: A SAT-based approach, in: Proceedings of the 2nd Theory and Applications of Formal Argumentation, Springer, Beijing, China, 2013, 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, IOS Press, Scottish Highlands, UK, 2014, pp. 455–456.

15.

Cerutti,

Giacomin,

Vallati and

Zanella, An SCC recursive meta-algorithm for computing preferred labellings in abstract argumentation, in: Proceedings of the 14th Principles of Knowledge Representation and Reasoning, AAAI Press, Vienna, Austria, 2014.

16.

Charwat,

Dvorak,

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.

17.

Dimopoulos and

Sideris, Towards local search for answer sets, in: Proceedings of the 18th International Conference on Logic Programming, Springer, Copenhagen, Denmark, 2002, pp. 363–377.

18.

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.

19.

Dvorak,

Jarvisalo,

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.

20.

Erdős and

Rényi, On the evolution of random graphs, Bulletin of the Institute of International Statistics 38(4) (1961), 343–347.

21.

Koenig and

Likhachev, D* Lite, in: Proceedings of the 18th AAAI Conference on Artificial Intelligence, AAAI Press, Edmonton, Alberta, Canada, 2002, pp. 476–483.

22.

Laitinen,

T.A.

Junttila and

Niemelä, Extending clause learning SAT solvers with complete parity reasoning, in: Proceedings of the IEEE 24th International Conference on Tools with Artificial Intelligence, IEEE Computer Society, Athens, Greece, 2012, pp. 65–72.

23.

Li,

Jiang and

Xu, Incremental MaxSAT reasoning to reduce branches in a branch-and-bound algorithm for MaxClique, in: Proceedings of the 9th International Conference on Learning and Intelligent Optimization, Springer, Lille, France, 2015, pp. 268–274. doi:10.1007/978-3-319-19084-6_26.

24.

Lin,

Sun and

Zhang, Theorem proving based on the extension rule, Journal of Automated Reasoning 31(1) (2003), 11–21. doi:10.1023/A:1027339205632.

25.

Luo,

Cai,

Su and

Wu, Clause states based configuration checking in local search for satisfiability, IEEE Transactions on Cybernetics 45(5) (2015), 1014–1027.

26.

Luo,

Cai,

Wu,

Jie and

Su, CCLS: An efficient local search algorithm for weighted maximum satisfiability, IEEE Transactions on Computers 64(7) (2015), 1830–1843. doi:10.1109/TC.2014.2346196.

27.

Martel and

Nguyen, Analyzing Kleinberg’s (and other) small-world models, in: Proceedings of the 23rd Annual ACM Symposium on Principles of Distributed Computing, ACM, Newfoundland, Canada, 2004, pp. 179–188.

28.

D.D.

Niu,

Liu and

Lü, A new stochastic local search approach for computing preferred extensions of abstract argumentation, in: Proceedings of the 22nd European Conference on Artificial Intelligence, IOS Press, The Hague, The Netherlands, 2016, pp. 1652–1653.

29.

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.

30.

Oral and

Polat, MOD* Lite: An incremental path planning algorithm taking care of multiple objectives, IEEE Transactions on Cybernetics 46(1) (2016), 245–257. doi:10.1109/TCYB.2015.2399616.

31.

Pipatsrisawat and

Darwiche, On the power of clause-learning SAT solvers with restarts, in: Proceedings of the 15th Principles and Practice of Constraint Programming, Springer, Lisbon, Portugal, 2009, pp. 654–668.

32.

Pipatsrisawat and

Darwiche, On the power of clause-learning SAT solvers as resolution engines, Artificial Intelligence 175 (2011), 512–525. doi:10.1016/j.artint.2010.10.002.

33.

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.

34.

D.A.D.

Tompkins,

Balint and

H.H.

Hoos, Captain jack: New variable selection heuristics in local search for SAT, in: Proceedings of the 14th Theory and Applications of Satisfiability Testing, Springer, Ann Arbor, MI, USA, 2011, pp. 302–316.

Benchmarks		Inc-CCA_EP

		solved	max-sr-time	avg-sr-time
ER	200(83)	73	3.24	0.12
	300(84)	69	10.09	0.37
	400(83)	60	13.22	2.18
	500(86)	62	190.05	31.93
Kle	36(100)	100	0.2	0.1
Kle	49(100)	100	46.20	23.10
BA	1200(91)	91	0.02	0.02
	1700(89)	89	0.03	0.02
	2500(86)	86	0.04	0.03
	5000(88)	88	0.13	0.10
	10000(89)	89	0.55	0.47
	20000(89)	89	2.09	1.96

New stochastic local search approaches for computing preferred extensions of abstract argumentation

Abstract

Keywords

1. Introduction

1 http://argumentationcompetition.org/2015/

Definition 4 ([11]).

4. Enumerating preferred extensions based on CCA heuristics

5 http://www.dbai.tuwien.ac.at/research/project/argumentation/cegartix/

Footnotes

Acknowledgements

References

¹
http://argumentationcompetition.org/2015/

⁵
http://www.dbai.tuwien.ac.at/research/project/argumentation/cegartix/