{'fraction_non_alphanumeric': 0.06073780448820408, 'fraction_numerical': 0.0072885365385844895, 'mean_word_length': 3.936770120988953, 'pattern_counts': {'":': 1, '<': 6, '<?xml version=': 0, '>': 2, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 13, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Admissibility in Strength-based Argumentation: Complexity and Algorithms (Extended Version with Proofs)

Recently, Strength-based Argumentation Frameworks (StrAFs) have been proposed to model situations where some quantitative strength is associated with arguments. In this setting, the notion of accrual corresponds to sets of arguments that collectively attack an argument. Some semantics have already been defined, which are sensitive to the existence of accruals that collectively defeat their target, while their individual elements cannot. However, until now, only the surface of this framework and semantics have been studied. Indeed, the existing literature focuses on the adaptation of the stable semantics to StrAFs. In this paper, we push forward the study and investigate the adaptation of admissibility-based semantics. Especially, we show that the strong admissibility defined in the literature does not satisfy a desirable property, namely Dung's fundamental lemma. We therefore propose an alternative definition that induces semantics that behave as expected. We then study computational issues for these new semantics, in particular we show that complexity of reasoning is similar to the complexity of the corresponding decision problems for standard argumentation frameworks in almost all cases. We then propose a translation in pseudo-Boolean constraints for computing (strong and weak) extensions. We conclude with an experimental evaluation of our approach which shows in particular that it scales up well for solving the problem of providing one extension as well as enumerating them all.


Introduction
Among widespread knowledge representation and reasoning techniques proposed in the literature of Artificial Intelligence over the last decades, Abstract Argumentation [1] is an intuitive but yet powerful tool for dealing with conflicting information. Since then, the initial work of Dung has been actively extended and enriched in many directions, e.g. considering other kinds of relations between arguments [2] or additional information associated with arguments or attacks [3,4]. Among them, Strength-based Argumentation Frameworks (StrAFs) [5] allow to associate a quantitative information with each argument. This information is a weight that intuitively represents the intrinsic strength of an argument, and is then naturally combined with attacks between arguments to induce a defeat relation that allows either to confirm an attack between two arguments or to cancel it, if the attacked argument is stronger than the attacker (w.r.t. their respective weights). StrAFs extend further this notion of defeat among arguments by building a defeat that is based on a collective attack of a group of arguments (or accrual) and by offering associate semantics. Within these semantics, arguments can collectively defeat arguments that they cannot defeat individually. Intuitively speaking, these accrual-sensitive semantics allow some kind of compensation among arguments, where the accumulation of weak arguments can create a synergy and get rid of a stronger one they collectively attack. This reasoning approach allows to produce extensions that are not considered when applying classical semantics.
In [5] the authors presented the basics of StrAFs inspired by Dung's semantics for abstract argumentation along with some theoretical and computational results concerning classical issues related to abstract argumentation (i.e. acceptability semantics, semantics inclusion, extensions existence and verification, etc.). In this paper we propose a state of the art advancement in StrAFs by presenting original theoretical and computational results related to different aspects. More particularly the contribution of this work lies into the following aspects. The semantics proposed in [5] exist in two versions (namely strong, and weak). Roughly speaking, a set is strongly conflict-free iff none of its elements attacks another one, whereas a set is weakly conflict-free iff it does not contain any (successful) accrual against one of its elements. After detecting that strong admissibility fails to satisfy a desirable property in Dung's abstract argumentation frameworks, namely his Fundamental Lemma [1], we propose an alternative definition for strong admissibility in order to remedy this issue and we define new admissibility-based semantics for StrAFs. Furthermore, we study the complexity of reasoning with these semantics and in particular we show that, surprisingly, the complexity does not increase with respect to the complexity of reasoning with standard AFs. For computing the extensions under these semantics, we propose algorithms based on pseudo-Boolean constraints.

Background Notions
We assume that the reader is familiar with abstract argumentation [1]. We consider finite argumentation frameworks (AFs) A, R , where A is the set of arguments, and R ⊆ A × A is the attack relation. We will use cf(AF ) and ad(AF ) to denote, respectively, the conflict-free and admissible sets of an AF AF , and co(AF ), pr(AF ) and st(AF ) for its extensions under the complete, preferred and stable semantics. For more details on the semantics of AFs, we refer the interested reader to [1,6].
A Strength-based Argumentation Framework (StrAF) [5] is a triple StrAF = A, R, S where A and R are arguments and attacks, and S : A → N is a strength function. An example of such a StrAF is depicted at Figure 1, where nodes represent arguments, edges represent attacks, and the numbers close to the nodes represent the arguments strength. These strengths intuitively represent the intrinsic robustness associated with an argument and allow to induce a defeat  Figure 1: A StrAF Example relation: an argument a defeats another argument b when a attacks b and the strength associated with b does not overcome that with a. This framework also offers the notion of collective defeat, i.e. sets of arguments that can jointly defeat their target while they cannot do so separately. First, we call an accrual a set of arguments that collectively attack a same target, i.e. a set κ ⊆ A s.t. ∃c ∈ A s.t. ∀ a ∈ κ, (a, c) ∈ R. Moreover, we say that κ is an accrual that attacks c. Then, for κ ⊆ A an accrual, κ attacks κ iff ∃a ∈ κ s.t. κ attacks a. Example 1. Consider again StrAF from Figure 1. We can observe several examples of accruals, e.g. κ 1 = {a 1 , a 2 } and κ 2 = {a 1 , a 3 }, that both attack a 4 . Notice that any attack (a i , a j ) ∈ R induces an accrual {a i } attacking a j .
We need to assess the collective strength of an accrual. Definition 1 (Collective Strength). Let StrAF = A, R, S be a StrAF and κ = {a 1 , ..., a n } ⊆ A be an accrual. Then the collective strength associated with κ is coval ⊕ (κ) = ⊕(S(a 1 ), . . . , S(a n )) where ⊕ is an aggregation operator.
The operator ⊕ must satisfy some properties discussed in [5]. An example of suitable operator is ⊕ = . If ⊕ is clear from the context, we simply write coval for coval ⊕ . Definition 2 (Collective Defeat). Let StrAF = A, R, S be a StrAF, a ∈ A, and ⊕ an aggregation operator. Then, an accrual κ defeats a with respect to coval ⊕ , denoted by κ ⊕ a, iff κ ⊆ A is an accrual that attacks a and coval ⊕ (κ) ≥ S(a). If ⊕ is clear from the context, we use κ a instead of κ ⊕ a.
• S defends an element a ∈ A iff for all accruals κ 1 ⊆ A, if κ 1 ⊕ a, then there exists an accrual κ 2 ⊆ S s.t.
Intuitively, strongly conflict-free sets are "classically" conflict-free, i.e. there is no attack between two arguments members of such a set. On the contrary, weakly conflict-free sets are "defeat-free": attacks between arguments are permitted as long as they do not result in a defeat neither individual nor collective. We use (respectively) cf ⊕ S and cf ⊕ W to denote these sets (or simply cf S and cf W when ⊕ is clear from the context). Then, admissibility and extension-based semantics can be defined either strong or weak. Namely: Definition 5 (Semantics for StrAFs [5]). Given StrAF = A, R, S a StrAF, ⊕ an aggregation operator, and S ⊆ A a strong (resp. weak) conflict-free set, • S is a strong (resp. weak) admissible set iff S defends all elements of S.
• S is a strong (resp. weak) preferred extension iff S is a ⊆-maximal strong (resp. weak) admissible set.
For σ an extension-based semantics and X ∈ {S, W } meaning respectively strong and weak, we use σ ⊕ X (StrAF ) to denote the X-σ extensions of StrAF . We drop ⊕ from the notation where there is no possible ambiguity.
It is proven in [5] that Dung's AFs are a subclass of StrAFs, where strong and weak semantics coincide. This result is useful for proving complexity results. However, in [5] authors only focus on complexity issues for the (weak and strong) stable semantics.

Admissibility-based Semantics for StrAFs
In our study, we investigate computational issues for admissibility-based semantics. A formal definition of (weak or strong) complete semantics is missing in [5], but matching the definition of (weak or strong) admissibility with the classical definition of the complete semantics, a straightforward definition can be stated as follows: Definition 6. Let StrAF = A, R, S be a StrAF, and ⊕ an aggregation operator. A strong (resp. weak) admissible set S ⊆ A is a strong (resp. weak) complete extension of StrAF if S contains all the arguments that it defends. Now we study these semantics and in particular, we show that surprisingly this intuitive definition of the complete semantics based on strong admissibility fails to satisfy a desirable property, namely the Fundamental Lemma, which states that admissible sets can be extended by the arguments that they defend. This leads us to redefine strong admissibility (and the associated complete and preferred semantics) in Section 3.1. On the contrary, the definition of weak admissibility is proved to be suitable in Section 3.2.

Revisiting Strong Admissibility
First, we observe that the usual inclusion relation between the preferred and complete semantics is not satisfied for the strong semantics of StrAFs. Moreover, the universal existence of complete extensions does not hold either.  The StrAF from Figure 2 shows that the Fundamental Lemma does not hold for strong semantics of StrAFs: {a} is strongly admissible, and defends c, but {a} ∪ {c} is not strongly admissible. A way to solve this issue is to redefine strong admissibility: Definition 7 (Strong Semantics Revisited). Let StrAF = A, R, S be a StrAF and ⊕ an aggregation operator. A set S ∈ cf S (StrAF ) strongly defends an argument a if S defends a against all the accruals that defeat it, i.e. ∀κ ⊆ A s.t. κ a, ∃κ ⊆ S s.t. κ κ, and S ∪ {a} is strongly conflict-free. Then, a set S ⊆ A is strongly admissible if it is strongly conflict-free and it strongly defends all its elements. Moreover, • S is a strong preferred extension iff S is a ⊆-maximal strong admissible set.
• S is a strong complete extension iff S contains all the arguments that it strongly defends.
If we consider again the StrAF from Figure 2, observe that this time, the strongly admissible set {a} does not strongly defends c, since {a, c} is not strongly conflict-free. Thus {a} is a strong complete extension of this StrAF, following Definition 7. Now, Dung's Fundamental Lemma can be adapted to strong admissibility. Lemma 1 (Fundamental Lemma for Strong Admissibility). Let StrAF = A, R, S be a StrAF and ⊕ an aggregation operator. Let S ⊆ A be a strongly admissible set, and a, a two arguments that are strongly defended by S against all their defeaters. Then, S = S ∪ {a} is strongly admissible.
Proof. The proof follows the definitions of strong defense and strong admissibility: since S strongly defends all its elements, and strongly defends a, then S = S ∪ {a} is strongly conflict-free and strongly defends all its elements, hence it is strongly admissible. Proof. Reasoning with a proof by contradiction, suppose that there is a strong preferred extension S of StrAF , which is not a strong complete extension. Since S is strongly admissible, it means that it strongly defends an argument a ∈ A \ S. According to Lemma 1, S ∪ {a} is strongly admissible. Thus we have a strongly admissible set S ⊃ S, which contradicts the fact that S is a strong preferred extension (i.e. a ⊆-maximal strong admissible set). This concludes the proof that S is a strong complete extension.
This guarantees the existence of at least one strong complete extension for any StrAF: since ∅ is a strong admissible set for any StrAF , then StrAF admits some ⊆-maximal strong admissible sets, i.e. pr S (StrAF ) = ∅, which implies co S (StrAF ) = ∅. Finally, we prove that the new definition of strong admissibility does not change the fact that strong stable extensions are strongly admissible (and even strong preferred). Proof. Let S ∈ st S (StrAF ) be a strong stable extension. By definition, S is strongly conflict-free. Let us prove that it is strongly admissible, i.e. it strongly defends all its elements. Since it is strongly conflict-free, we only need to prove that it (classically) defends all its elements. Indeed, given a ∈ S, the fact that S ∪ {a} is strongly conflict-free is obvious. Let κ be an accrual that defeats a. The strong conflict-freeness of S implies that there is no b ∈ κ belonging to S, i.e. κ ⊆ A \ S. Then, since S defeats all the arguments in A \ S (because it is a strongly stable extension), S defeats all the arguments in κ. So a is strongly defended. Which proves that S is admissible. Now, prove that it is a strongly preferred extension. Assume that it is not, i.e. ∃S ∈ ad S (StrAF ) s.t. S ⊂ S . This implies the existence of an argument b ∈ S \ S. Since S is strongly stable, there is some accrual κ ⊆ S that defeats b.
This implies that S is not strongly conflict-free, which contradicts the assumption that S is a strongly admissible set. So we conclude that no such S exists, i.e. S is strongly preferred.

Properties of the Weak Semantics
Regarding now weak semantics as defined in [5], the usual result still holds for StrAFs. Lemma 2 (Fundamental Lemma for Weak Admissibility). Let StrAF = A, R, S be a StrAF and ⊕ an aggregation operator. Given S ⊆ A a weakly admissible set, and a, a two arguments that are defended by S, Proof.
1. Suppose that S is weakly admissible and S defends a. We need to prove that S ∪ {a} is weakly conflict-free. Reasoning with a proof by contradiction, suppose it is not the case. We split the reasoning in two parts: ∃κ ⊆ S ∪ {a} s.t. κ a, or κ a with a ∈ E.
(a) First case: ∃κ ⊆ S ∪ {a} s.t. κ a. It means that there is an accrual κ ⊆ S s.t. κ a. By hypothesis S defends a against κ, it means that ∃κ ⊆ S s.t. κ κ, thus S is not weakly conflict-free. Contradiction. (b) Second case: ∃κ ⊆ S ∪ {a} s.t. κ a with a ∈ S. By hypothesis, S defends itself against all its defeaters, so ∃κ ⊆ S s.t. κ κ. Since κ ⊆ S ∪ {a}, either κ defeats a (thus case (a) applies, and this is a contradiction), or κ defeats some argument from S, which is also a contradiction.
2. Obvious from the fact that S defends a .

Proposition 4. For any StrAF and ⊕, pr
Similarly to what we have noticed previously for strong admissibility, ∅ is weakly admissible for any StrAF. This implies the existence of at least one weak preferred extension, and then one weak complete extension for any StrAF. Notice that, contrary to the case of stable semantics [5], we do not have co S (StrAF ) ⊆ co W (StrAF ). This comes from the fact that our strong and weak complete semantics are not based on the same notion of defense. However, we observe that each strong complete extension is included in some weak preferred (and complete) extension. We prove that this is true for any StrAF. Proposition 5 (Strong/Weak Semantics Relationship). Given StrAF = A, R, S and ⊕ an aggregation operator, Proof. The results holds because each strongly admissible set is also a weakly admissible set. Indeed, E ∈ ad S (StrAF ) is (by definition) strongly conflict-free, which implies its weak conflict-freeness. It also strongly defends all its elements, which implies that it (classically) defends all its elements. Thus E ∈ ad W (StrAF ). Then, for any E ∈ co S (StrAF ), by definition E ∈ ad S (StrAF ), thus E ∈ ad W (StrAF ). Since weak preferred extension are ⊆-maximal weakly admissible set, the existence of Notice finally that we do not need a counterpart to Proposition 3: the definition of semantics based on weak admissibility is not modified, so the result from [5, Proposition 1] still holds in this case.

Dung Compatibility
Previous work on StrAFs showed that this framework generalizes Dung's AF, with a correspondence of StrAF semantics with AF semantics in this case. Following the new definition of strong admissible sets, one might fear that this property does not hold for strong admissibility-based semantics. However, we show here that it still does, as well as for weak complete semantics. Let us recall the transformation of an AF into a StrAF [5]. Definition 8. Given an argumentation framework AF = A, R , the StrAF associated with AF is StrAF AF = A, R, S with S (a) = 1, ∀a ∈ A and coval = .
Observation 1. Since all the arguments have the same strength, (a, b) ∈ R implies {a} b, thus strong and weak conflict-freeness coincide in StrAF AF .
We also recall useful lemmas from [5]. Lemma 3. Let AF = A, R be an AF, and StrAF AF = A, R, S its associated StrAF. The set S ⊆ A is conflict-free in AF iff it is strongly conflict-free in StrAF AF .
Lemma 3 is obvious from the definition of strong conflict-freeness. Then Lemma 4 is useful for proving Dung Compatibility in the context of weak semantics. Lemma 4. Let AF = A, R be an AF, and StrAF AF = A, R, S its associated StrAF. The set S ⊆ A defends the argument a ∈ A in AF iff S ⊆ A defends the argument a ∈ A in StrAF AF .
See [5] for the proof of this Lemma. We can also state a stronger version, that will be useful for proving that Dung Compatibility holds with the revisited definition of strong admissibility. Lemma 5. Let AF = A, R be an AF, and StrAF AF = A, R, S its associated StrAF. The set S ⊆ A defends the argument a ∈ A in AF iff S ⊆ A strongly defends the argument a ∈ A in StrAF AF .
Proof. Let us suppose that S ⊆ A defends the argument a ∈ A in AF . This means that for each b ∈ A such that (b, a) ∈ R, ∃c ∈ S such that (c, b) ∈ R. Moreover, from the Fundamental Lemma by [1], S ∪ {a} is admissible, hence it is conflict-free. This implies the strong conflict-freeness of S ∪ {a}. Now, let us consider an accrual Now we suppose that S ⊆ A strongly defends the argument a ∈ A in StrAF AF , i.e. S ∪ {a} is strongly conflict-free, and for all accruals κ 1 that defeat a, ∃κ 2 ⊆ S such that κ 2 κ 1 . Since all arguments strengths are equal to 1, every argument b ∈ A attacking a corresponds to an accrual κ 1 = {b} defeating a. So ∃κ 2 ⊆ S such that κ 2 κ 1 = {b}, and thus ∃c ∈ κ 2 ⊆ S such that (c, b) ∈ R. So we conclude that S defends the argument a in AF .
Now we can state the following proposition, that extends Dung Compatibility from [5] to the semantics studied in this paper. Proposition 6 (Dung Compatibility). Let AF = A, R be an AF, and StrAF AF = A, R, S from Def. 8. For σ ∈ {ad, pr, co}, σ(AF ) = σ X (StrAF AF ), for X ∈ {S, W }.
Proof. From Lemmas 3 and 5, S is admissible in AF iff S is strongly admissible in StrAF AF . So the ⊆-maximal admissible sets in AF coincide with the ⊆-maximal strong admissible sets in StrAF AF , hence Dung Compatibility for strong preferred semantics. For strong complete semantics, notice that an admissible set S defends (in AF ) an argument a ∈ A \ S iff S strongly defends a in StrAF AF , thus S is a complete extension of AF iff it is a strong complete extension of StrAF AF , and similarly for weak complete semantics using Lemma 4. Results for weak admissibility and weak preferred semantics come from [5].

Complexity and Algorithms
Now we provide some insight on computational issues for admissibility-based semantics of StrAFs, i.e. we identify the computational complexity of several classical reasoning problems under these semantics, and we provide algorithms (based on pseudo-Boolean encoding) for solving them. While the complexity results are generic regarding the choice of ⊕, the algorithms focus on ⊕ = .

Complexity Analysis
We assume that the reader is familiar with basic notions of complexity, and otherwise we refer the interested reader to [7] for details on complexity in formal argumentation, and [8] for a more general overview of computational complexity.
We focus on three classical reasoning problems in abstract argumentation, namely verification ("Is a given set of arguments an extension?"), credulous acceptability ("Is a given argument member of some extension?") and skeptical acceptability ("Is a given argument member of each extension?"). Formally, for σ ∈ {ad, pr, co} and X ∈ {S, W }: • σ-X-Ver: Given StrAF = A, R, S and S ⊆ A, is S a member of σ X (StrAF )?
• σ-X-Cred: Given StrAF = A, R, S and a ∈ A, is a in some S ∈ σ X (StrAF )?
We recall that these reasoning problems are already considered only for the (weak and strong) stable semantics in [5]. In the following, we assume a fixed ⊕, that can be computed in polynomial time. This is not a very strong assumption, since it is the case with the classical aggregation operators (e.g. , max, . . . ). Proposition 6 implies that the complexity of reasoning with standard AFs provides a lower bound complexity of reasoning with StrAFs. So we focus on identifying upper bounds. Proposition 7 (Verification). For X ∈ {S, W }, σ-X-Ver ∈ P , for σ ∈ {ad, co}, and pr-X-Ver is coNP-complete.
Proof. Let us start with strong (resp. weak) admissible sets. Given S ⊆ A, to verify whether S is a strong (resp. weak) admissible set, one must: • check whether it is a strong (resp. weak) conflict-free set: doable in polynomial time (see [5]), • for each κ s.t. κ S (that can be identified in polynomial time by checking the attackers of S), check whether ∃κ ⊆ S s.t. κ κ (doable in polynomial time by checking the attackers of κ).
Now we focus on strong (resp. weak) complete semantics. One first needs to check (polynomially) whether S is a strong (resp. weak) admissible set. If yes, then check whether it defends some a ∈ S (doable in polynomial time by checking if there are accruals κ defeating a, and whether some κ ⊆ S defeats κ). For strong complete semantics, restrict this part to arguments a ∈ A \ S s.t. S ∪ {a} is strongly conflict-free (this can also be verified in polynomial time). Thus co-X-Ver ∈ P , for X ∈ {S, W }.
Finally, for checking whether a set S ⊆ A is a strong (resp. weak) preferred extension, first check whether it is strongly (resp. weakly) admissible, then non-deterministically guess a proper superset S ⊃ S, and check whether S is strongly (resp. weakly) admissible. A positive answer proves that S is not a strong (resp. weak) preferred extension. Hence pr-X-Ver ∈ coNP, for X ∈ {S, W }. Then, Dung compatibility (Proposition 6) and known complexity results about AFs [7] prove that pr-X-Ver is coNP-complete.

Proof.
A classical non-deterministic algorithm can be used for checking the credulous acceptability of an argument a: guess a set of arguments S ⊆ A s.t. a ∈ S, then (polynomially) check whether S is a strong (resp. weak) admissible set. This approach guarantees that ad-X-Cred ∈ NP, for X ∈ {S, W }. Since the verification is also polynomial for strong (resp. weak) complete extensions, the reasoning holds for proving that co-X-Cred ∈ NP. Finally, from known complexity results [7] and Dung compatibility (Proposition 6), we deduce that ad-X-Cred and co-X-Cred are NP-hard, thus we conclude that these problems are NP-complete.
Finally, since strong (resp. weak) preferred extensions are ⊆-maximal strong (resp. weak) admissible sets, credulous acceptability under strong (resp. weak) preferred semantics is equivalent to credulous acceptability under strong (resp. weak) admissibility. So pr-X-Cred is NP-complete too.
We give an upper bound for the complexity of skeptical acceptance under the strong (resp. weak) complete semantics. A non-deterministic algorithm solves it by guessing a set of arguments S ⊆ A s.t. a ∈ S, and checking (in polynomial time) whether S is a strong (resp. weak) complete extension. So co-X-Skep ∈ coNP.
Finally, known complexity results [7] and Dung compatibility (Proposition 6) allow us to deduce that pr-X-Skep is Π P 2 -hard for X ∈ {S, W }. Then, this problem is solved by non-deterministically guessing a set of arguments S ⊆ A s.t. a ∈ S, and then checking (with a coNP oracle) that S is not a strong (resp. weak) preferred extension (proving that a is not skeptically accepted). This proves that pr-X-Skep is actually Π P 2 -complete.
Proposition 10 summarizes the results given above. Proposition 10. The complexity of the decision problems σ-X-Ver, σ-X-Cred and σ-X-Skep is as described in Table 1. Table 1: Complexity of reasoning for σ X with σ ∈ {ad, co, pr} and X ∈ {S, W }. Trivial means that all instances are trivially "NO" instances, and C-c means C-complete, for C a complexity class in the polynomial hierarchy.

σ-X-Ver σ-X-Cred σ-X-Skep
As it is the case for the strong (resp. weak) stable semantics [5], we prove here that the higher expressivity of StrAFs (compared to AFs) does not come at the price of a complexity blow-up. Only the case of skeptical acceptability under strong (resp. weak) complete semantics requires a deeper analysis, since we only provide the coNP upper bound. We observe that the choice of the weak or strong variant of the semantics does not have an impact on the complexity of reasoning.

Algorithms
For computing the strong (resp. weak) admissible sets and complete extensions, we propose a translation of StrAF semantics in pseudo-Boolean (PB) constraints [9]. Such a constraint is an (in)equality i w i × l i #k where w i and k are positive integers, and # ∈ {>, ≥, =, =, ≤, <}. l i is a literal, i.e.
Determining whether a set of PB constraints has a solution is a NP-complete problem, that generalizes the Boolean satisfiability (SAT) problem. Despite the high complexity of this problem, it can be efficiently solved in many cases, see e.g. [10,11].
Strong and Weak Conflict-freeness Now we describe our PB encoding of StrAF semantics. For ensuring selfcontainment of the paper, we recall the encoding of strong and weak conflict-freeness [5]. Given StrAF = A, R, S and coval = , we define a set of Boolean variables {x i | a i ∈ A} associated with each argument, where x i = 1 means that a i belongs to the set of arguments characterized by the solutions of the PB constraints. Then, strong conflict-freeness is encoded by: (1) ∀(a i , a j ) ∈ R, add the constraint x i + x j ≤ 1 and weak conflict-freeness is encoded by: (1') ∀a ∈ A, add the constraint ai∈Γ − (a) S(a i ) × x i < x × S(a) + x × M with M an arbitrary large natural number that is greater than the sum of the strengths of the arguments (i.e. M > a∈A S(a)), Γ − (a) = {b | (b, a) ∈ R} is the set of attackers of a ∈ A, and x is the Boolean variable associated with a. 1 A solution to the set of constraints (1) (resp. (1')) yields a strong (resp. weak) conflict-free set E = {a i | x i = 1}. We prove this claim with Proposition 11. First, let us introduce some notations. Given S ⊆ A, ω S : {x i | a i ∈ A} → {0, 1} is a mapping s.t. ω S (x i ) = 1 iff a i ∈ S. Proposition 11. Given StrAF = A, R, S and S ⊆ A, S ∈ cf S (StrAF ) (resp. S ∈ cf W (StrAF )) iff ω S satisfies the set of constraints (1) (resp. (1')).
Proof. We start with strong conflict-freeness. Suppose that S is strongly conflict-free. This means that, for any attack (a i , a j ) ∈ R, at most one of a i and a j belongs to S, i.e. at most one x i and x j is equal to one, hence x i + x j ≤ 1.
On the contrary, suppose that ω S satisfies the set of constraints (1). This means that, for any two arguments a i , a j ∈ S (i.e. both x i and x j are equal to 1), if there is an attack between them, the constraint x i + x j ≤ 1 is falsified. This is a contradiction with the hypothesis that ω S satisfies the constraint, thus there cannot be an attack between arguments in S, i.e. S is strongly conflict-free. Now we focus on weak conflict-freeness. Suppose that S is weakly conflict-free. This means that there is no κ ⊆ S and a ∈ S s.t. κ a. First, if S is actually strongly conflict-free, then all the constraints from the set (1') with an argument a ∈ S in the right-hand part are trivially satisfied (they are reduced to 0 < S(a), because x j = 0 for any attacker a j ∈ A \ S of a). Now consider the case where S is weakly conflict-free without being strongly conflict-free. This means that there are attacks between arguments in S. Consider some a ∈ S that is attacked by at least one argument b ∈ S. The constraint from the set (1') with a in its right-hand side becomes aj ∈S,(aj ,a)∈R S(a j ) < S(a). This constraint is satisfied iff the accrual κ = {a j ∈ S | (a j , a) ∈ R} (and any κ ⊆ κ) does not defeat a. This is the case since S is weakly conflict-free. Finally, consider the constraints from (1') with some argument a ∈ S on the right-hand side. The right-hand side is reduced to M , which is arbitrarily large, thus the constraint is satisfied. Now suppose that ω S is a solution of the set of constraints (1'). For any a ∈ S without any attack in S, the constraint with a on the right-hand side is trivially satisfied (it becomes 0 < S(a)). Then, for any a ∈ S with some attackers in S, the constraint with a on the right-hand side becomes aj ∈S,(aj ,a)∈R S(a j ) < S(a). This constraint is satisfied iff the accrual κ = {a j ∈ S | (a j , a) ∈ R} (and any κ ⊆ κ) does not defeat a, hence the conclusion.
Strong and Weak Admissibility For encoding strong (resp. weak) admissibility, one must add to the set of constraints (1) (resp. (1')) some new constraints that represent the strong defense (resp. defense) property. To do so, one needs to introduce new Boolean variables {y i | a i ∈ A} s.t. y i = 1 means that a i is defeated by the set of arguments characterized by the solution of the PB constraints. Then, three constraints are added (the same ones for strong and weak admissibility): The sets of constraints (2) and (3) ensure that y = 1 iff a is defeated by some κ ⊆ E = {a i | x i = 1}, and the constraints (4) ensure that E defends all its elements. The following proposition shows the correctness of the encodings. Proposition 12. Given StrAF = A, R, S and S ⊆ A, S ∈ ad S (StrAF ) (resp. S ∈ ad W (StrAF )) iff ω S satisfies the sets of constraints (1) (resp. (1')), (2), (3) and (4).
Proof. We start with strong admissibility. Suppose that S is a strongly admissible set. Strong conflict-freeness implies that ω S satisfies the set of constraints (1) (see Proposition 11). Now, let a be an argument defeated by some accrual κ ⊆ S. The constraint from set (2) with a on the right-hand side becomes aj ∈S,(aj ,a)∈R S(a j ) ≥ y × S(a). The constraint is satisfied, since the sum of the strengths of the arguments in κ is greater than the strength of a, the value of y does not matter. The constraint from set (3) with a on the right-hand side becomes aj ∈S,(aj ,a)∈R S(a j ) ≤ y × S(a) + y × M . Since the collective strength of the attackers of a in κ is greater than the strength of a, the constraint is satisfied when y = 1 (recall that M is an arbitrary large integer). Now consider an argument a that is not defeated by any accrual κ ⊆ S. This means that the sum of the strengths of the arguments in S that attack a is lesser than the strength of a, thus the constraint aj ∈S,(aj ,a)∈R S(a j ) ≥ y × S(a) is satisfied iff y = 0. Then, the constraint aj ∈S,(aj ,a)∈R S(a j ) ≤ y × S(a) + y × M is satisfied for any value of y (since the collective strength of the attacks of a in S is lesser than the strength of a, and lesser than M ).
Observe that ω S satisfies both the sets of constraints (2) and (3), and implies that y = 1 iff the associated argument a is defeated by some accrual κ ⊆ S. Now we focus on the set of constraints (4). For any argument a ∈ A \ S, the right-hand side of the constraint is reduced to M , which is (by definition) greater than the left-hand side. Thus the constraint is satisfied. Now consider some argument a ∈ S. The constraint becomes S(a 1 ) × y 1 + S(a 2 ) × y 2 + · · · + S(a n ) × y n ≤ S(a). Recall that a is defended against all the accruals κ s.t. κ a (because of the strong admissibility of S). For all the attackers a j that are defeated by S, y j = 0. Let Att a = {a j ∈ Γ − (a) | S a j } be the set of attackers of a that are not defeated by S. The constraint can be re-written aj ∈Atta S(a j ) ≤ S(a). The constraint is satisfied, because otherwise Att a would be an accrual that defeats a and that is not defeated by S, which is impossible because of the strong admissibility of S. Now we prove the opposite direction, i.e. we suppose that ω S satisfies the sets of constraints (1), (2), (3) and (4). The satisfaction of the constraints (1) implies that S is strongly conflict-free (see Proposition 11). We must prove that S strongly defends all its elements. Let a ∈ S be an argument. Strong conflict-freeness of S implies that S ∪ {a} is strongly conflict-free, thus S strongly defends a iff S "classically" defends a, i.e. ∀κ ⊆ A s.t. κ a, ∃κ ⊆ S that defeats κ.
Consider an argument a s.t. ω S (y) = 0. Then the constraints from the sets (2) and (3), with a on the right-hand side, become (respectively) aj ∈S,(aj ,a)∈R S(a j ) ≥ 0 (which is trivially satisfied) and aj ∈S,(aj ,a)∈R S(a j ) ≤ S(a). This last constraint implies that a is not defeated by κ = {a j ∈ S | (a j , a) ∈ R} nor any κ ⊆ κ, i.e. there is no κ ⊆ S s.t. κ a. On the contrary, consider a s.t. ω S (y) = 1. The constraint from (2) with a in the right-hand side becomes aj ∈S,(aj ,a)∈R S(a j ) ≥ S(a). This means that there is an accrual κ = {a j ∈ S | (a j , a) ∈ R} ⊆ S s.t. κ a. So, for any a ∈ A, ω S (y) = 1 iff a is defeated by some κ ⊆ S. Now look at the constraints from the set (4). For any a ∈ A \ S, ω S (x) = 0, so the constraint with a on the right-hand side becomes S(a 1 ) × y 1 + S(a 2 ) × y 2 + · · · + S(a n ) × y n ≤ M , which is trivially satisfied. Now for a ∈ S, ω S (x) = 1, thus the constraint becomes S(a 1 ) × y 1 + S(a 2 ) × y 2 + · · · + S(a n ) × y n ≤ S(a). The left-hand side can be reduced to the sum of the strengths of the attackers of a that are not defeated. Since the constraint implies that this strength is lesser than the strength of a, there is no accrual κ that defeats a and that is not in turn defeated by some κ ⊆ S. So we can conclude that S strongly defends all its elements, and thus it is strongly admissible.
The proof is analogous for weak admissibility.
Proof. Let S ⊆ A be a strong complete extension of StrAF . Strong admissibility and Proposition 12 imply that ω S satisfies the set of constraints (1), (2), (3) and (4). Let us focus on the set of constraints (5). For any a ∈ S, ω S (x) = 1, and the constraint is trivially satisfied (the right-hand side becomes 0). Now consider a ∈ A \ S. Let us define Att a = {a j ∈ A | (a j , a) ∈ R, ω S (y j ) = 0} the set of attackers of a that are not defeated by any κ ⊆ S, and T ar a = {a k ∈ A | (a, a k ) ∈ R, a k ∈ S}. The constraint becomes aj ∈Atta S(a j ) + |T ar a | × M ≥ S(a). Suppose first that T ar a = ∅, i.e. there is no argument in S attacked by a. The constraint is then aj ∈Atta S(a j ) ≥ S(a). Since S is a strong complete extension, it does not strongly defend a, i.e. there is an accrual κ ⊆ Att a s.t. κ a, and κ ⊆ S with κ κ. This implies that the collective strength of the arguments in κ is greater than the strength of a, which means that the constraint is satisfied. No, if T ar a = ∅, the constraint is satisfied as well because of |T ar a | × M on the left-hand side. Now, for the other direction of the proof, let us suppose that ω S satisfies the set of constraints (1), (2), (3), (4) and (5). The satisfaction of the sets (1), (2), (3) and (4) implies that S is strongly admissible (see Proposition 12). Let us show that S is a strong complete extension, i.e. it does not strongly defend any a ∈ A \ S. Reasoning towards a contradiction, suppose that there is a ∈ A \ S that is strongly defended by S. a ∈ A \ S implies that ω S (x) = 0, so the constraint from the set (5) becomes S(a 1 ) × y 1 + S(a 2 ) × y 2 + · · · + S(a n ) × y n + M × x 1 + · · · + M × x m ≥ S(a). Let Att a = {a j ∈ A | (a j , a) ∈ R, ω S (y j ) = 0} be the set of attackers of a that are not defeated by any κ ⊆ S and T ar a = {a k ∈ A | (a, a k ) ∈ R, a k ∈ S} the set of arguments in S that are attacked by a. The constraint can then be rewritten aj ∈Atta S(a j ) + |T ar A | × M ≥ S(a). Since the constraint is satisfied, it means that • either there is an accrual κ = Att a s.t. κ a, and there is no κ ⊆ S with κ κ; • or there is an argument a k ∈ S such that (a, a k ) ∈ R, i.e. S ∪ {a} is not strongly conflict-free.
In both cases, there is a contradiction with the assumption that S strongly defends a. So there is no such a: S is a strong complete extension.
The proof for weak complete semantics is analogous.
Acceptability and Verification Obtaining one (resp. each) solution for one of the sets of constraints defined previously corresponds to obtaining one (resp. each) extension of the StrAF under the corresponding semantics. For checking whether a given argument a i is credulously accepted, one simply needs to add the constraint x i = 1. If a solution exists, then it corresponds to an extension that contains a i , proving that this argument is credulously accepted. Otherwise, a i is not credulously accepted. For skeptical acceptability, one needs to add the constraint x i = 0. In this case, a solution exhibits an extension that does not contain a i , thus this argument is not skeptically accepted. In the case where no solution exists, then the argument is skeptically accepted. Finally, for checking whether a set of arguments S ⊆ A is an extension, one needs to add the constraints x i = 1 for each a i ∈ S, as well as x i = 0 for each a i ∈ A \ S. A solution exists for the new set of constraints iff S is an extension under the considered semantics.
Strong and Weak Preferred Semantics Finally, let us mention an approach to handle reasoning with strong and weak preferred semantics. Because of the higher complexity of skeptical reasoning under these semantics (recall Proposition 10), it is impossible (under the usual assumption that the polynomial hierarchy does not collapse) to find a (polynomial) encoding of these semantics in PB constraints. However, PB solvers can be used as oracles to find (with successive calls) preferred extensions. Algorithm 1 describes our method to do this for strong preferred semantics (replacing (1) by (1') provides an algorithm for weak preferred semantics). At start, we add the four constraints corresponding to a strong (resp. weak) admissible set and solve the instance, with the PB solver as a coNP oracle. Then we force the arguments within the extension to stay in the next one by adding the constraint on line 4. To avoid getting the same solution as in the previous step, we make sure that at least one argument outside the previous extension will be in the next one (line 5). This method iteratively extends an admissible set into a preferred extension, that is finally returned when the solver cannot find any (larger) solution.

Experimental Evaluation
For estimating the scalability of our method based on pseudo-Boolean constraints, we present now some results obtained from our experimental evaluation using two prominent PB solvers: Sat4j [12] and RoundingSat [11]. While Sat4j is based on saturation, RoundingSat uses the division rule (see [11] for a discussion on both approaches). We focus here on the most relevant results; full results are presented in the appendix.
Benchmark Generation We generate benchmarks in a format adapted to StrAFs, inspired by ASPARTIX formalism [13]. We consider two classes of randomly generated graphs. First, with the Erdös-Rényi model (ER) [14], given a set of arguments A, and p ∈ [0, 1], we generate a graph such that for each (a, b) ∈ A × A, a attacks b with a probability p. We consider two values for the probability, namely p ∈ {0.1, 0.5}. Then, with the Barabási-Albert (BA) model [15], a graph of n nodes is grown by attaching new nodes with m edges that are preferentially attached to existing nodes with a high degree. These types of graphs have been frequently used for studying computational aspects of formal argumentation, in particular during the ICCMA competitions [16]. The choice of a generation model provides the arguments A and attacks R. We attach a random strength S(a) ∈ {1, . . . , 20} to each a ∈ A. For each generation model, we build 20 StrAFs for each |A| ∈ {5, 10, 15, . . . , 60}. Parameters (p ∈ {0.1, 0.5} for ER, m = 1 for BA) are chosen to avoid graphs with a high density of attacks, that would prevent the existence of meaningful extensions (e.g. non-empty ones). Larger StrAFs (with |A| ∈ {5, 10, . . . , 250}) have been generated with the same parameters (p ∈ {0.1, 0.5} for ER, m = 1 for BA) for studying the problem of providing one extension.

Experimental Setting
The experiments were run on a Windows computer (using Windows Subsystem for Linux), with an Intel Core i5-6600K 3.50GHz CPU and 16GB of RAM. The timeout is set to 600 seconds (same as the timeout at ICCMA [17]).

Results
We are interested in the semantics σ X , with σ ∈ {pr, st, co} and X ∈ {S, W }. The encodings for st X (X ∈ {S, W }) are those proposed in [5], while the encoding for the other semantics are those described in Section 4.2. For each generated StrAF , and each of these semantics σ X , the two tasks we are interested in consist in enumerating all extensions and finding one extension. We first focus on the runtime for enumerating σ X extensions, which provides an upper bound of the runtime for solving other classical reasoning tasks. To do so, we use a Python script that converts a StrAF into a set of PB constraints. The set of extensions is then obtained in a classical iterative way: once an extension is returned by the PB solver, we add a new constraint that forbids this extension, and we call again the solver on this updated set of PB constraints. This process is repeated until the set of constraints becomes unsatisfiable, which means that all the extensions have been obtained. Concerning the preferred extensions, this iterative approach is combined with Algorithm 1. In order to measure the performance of our approach, and since there is no other computational approach for StrAF semantics yet, we also implemented a so-called naive algorithm that enumerates all sets of arguments and then checks, for each of them, if it is a σ X extension. Figure 3 presents the average runtimes w.r.t. instance sizes (i.e. |A|) for various semantics and StrAF families as described before. As a first result, we observe in Figure 6a that runtime for enumerating extensions (with the PB approach) is reasonable (i.e. less than a minute) for most of the cases considered in our study, when the PB approach is used, while the naive approach reaches the timeout for most of the large instances (in particular, all the instances with |A| ≥ 45). The average runtimes are higher in only two situations: the enumeration of strong preferred and strong complete extensions, with the BA graphs. However, even in such situations where the enumeration is harder (e.g. for pr S -extensions on BA graphs, as depicted on Figure 3b), the PB solvers clearly outperform the naive algorithm, which reaches the timeout in every instance when |A| ≥ 30, while the PB approach can enumerate extensions for larger graphs.
(a) coW on ER graphs (p = 0.1) (b) pr S on BA graphs Figure 3: Enumeration runtime We also study the classical problem of providing one extension, for StrAFs of larger sizes (recall that here |A| ∈ {5, 10, . . . , 250}). Figure 4 shows that the PB solvers (in particular, Sat4j) provide one extension for these large graphs under two minutes, even for the preferred semantics (which is the hardest one, in our study, from the computational point of view). Concerning the respective performances of the two PB solvers, Figure 4 shows that RoundingSat processes faster for fast-to-compute instances (i.e. the smallest ones), while Sat4j outperforms it for instances of larger size. While we do not have explanations for this phenomenon, a plausible assumption is that it is related to the difference of the underlying algorithms (saturation for Sat4j and division rule for RoundingSat). Similar things have been observed for SAT solvers used in the case of standard AFs [18]. As a general conclusion on our experimental analysis, we observe that the PB approach for reasoning with StrAFs generally scales up well, for both problems of enumerating extensions and providing one extension.

Conclusion
Strength-based Argumentation Frameworks (StrAFs) have originally been proposed in [5]. Contrary to this work, in this paper we focused on admissibility-based semantics. We showed that the weak admissibility-based semantics defined in the original work satisfy some expected properties, namely Dung's Fundamental Lemma. However, the definition for strong admissibility proposed in [5] does not yield semantics that behave as expected. This has conducted us to revisit the definition of strong admissibility, and this allowed us to introduce strong complete and preferred semantics. We have also enhanced the StrAFs literature by studying the computational complexity of classical reasoning problems for these semantics, and we have shown that it is the same as for the corresponding tasks in Dung's framework, in spite of the increase of expressivity. Then we have proposed a method based on pseudo-Boolean constraints for computing the extensions of a StrAF under the various semantics defined in this paper, and we have empirically evaluated the scalability of this approach for the new semantics defined in this paper, as well as the (weak and strong) stable semantics from [5].
As future work we have identified several promising research tracks, including the study of (weak and strong) grounded semantics, and tight complexity results for the skeptical reasoning under the (weak and strong) complete semantics. We are also interested in an analysis of the relation between StrAFs and other frameworks, in particular the comparison of the signatures of StrAFs semantics and SETAFs semantics [19,20,21]. Finally, we want to study argument strength and accrual in a context of structured argumentation.

A Experimental Results
This section describes additional experimental results, not presented in the main part of the paper because of space constraints.
(a) ER graphs with p = 0.1 (b) ER graphs with p = 0.5 (c) BA graphs