A Versatile Framework for Formula-Based Enforcement and Synthesis in Abstract Argumentation

1 Introduction

Formal argumentation has become a prominent research area in artificial intelligence over the past decades, with applications spanning from reasoning over inconsistent logical knowledge bases [Besnard and Hunter, 2008] to decisionmaking [Amgoud et al., 2008], negotiation [Dimopoulos et al., 2019], persuasion [Hunter, 2018] and legal reasoning [Atkinson and Bench-Capon, 2023], among others. Among the most central topics, abstract argumentation frameworks (AFs) [Dung, 1995] are directed graphs where nodes are arguments and edges are attacks between those arguments. Arguments acceptability is evaluated through different semantics which specify jointly acceptable sets of arguments called extensions [Baroni et al., 2018]. Argumentation dynamics has emerged as a central research direction in computational argumentation [Doutre and Mailly, 2018] with various forms of enforcement [Baumann and Brewka, 2010; Dyrkolbotn, 2014; Wallner et al., 2017; Haret et al., 2018; Dauphin and Satoh, 2018; Xu et al., 2018; Baumann and Brewka, 2019; Borg and Bex, 2021; Baumann et al., 2021; Heine and Ulbricht, 2024] studied as central computational problems. In enforcement, the goal is to modify an original AF in order to satisfy a given constraint on the acceptance status of specific arguments, e.g., so that a set of arguments is an extension [Baumann and Brewka, 2010; Baumann, 2012; Coste-Marquis et al., 2015; Wallner et al., 2017; Niskanen et al., 2018] or is (credulously or skeptically) accepted [Kontarinis et al., 2013; Doutre et al., 2014; Niskanen et al., 2016; Dauphin and Satoh, 2018]. Among the possible solution AFs, those obtained by minimizing syntactic change to the original AF-i.e., by applying as few modifications as possible to the set of arguments or the attack structure-have been widely investigated from both formal and computational perspectives [Baumann, 2012; Baumann and Brewka, 2013; Doutre et al., 2014; Coste-Marquis et al., 2015; Niskanen et al., 2016; Wallner et al., 2017; Niskanen et al., 2018; Ulbricht and Baumann, 2019; Craandijk and Bex, 2022; Heine and Ulbricht, 2024].

While applying minimal syntactic change is a desirable property from various perspectives such as efficiency and simplicity, in some situations a semantic notion of change is more appropriate [Coste-Marquis et al., 2014a; CosteMarquis et al., 2014b; Diller et al., 2018; Baumann and Brewka, 2019]. For example, consider a medical diagnostic system that has been reliably assisting practitioners for some time but is later found by experts to produce an incorrect inference. The systemmust be corrected, but ideally in a way that preserves its other, validated conclusions. The repair should therefore be as localized as possible, affecting only the erroneous outcome-i.e., minimizing semantic change.

We introduce formula-based enforcement, a general framework for enforcement in abstract argumentation allowing various forms of constraints on the resulting AF, including ones for minimizing syntactic or semantic change. Specifically, we use three sets of propositional formulas to express different forms of hard or soft constraints: the first set specifies which semantic constraints must be satisfied by an extension of the AF; the second set forbids extensions of the AF from satisfying specific constraints; and the third set imposes constraints on the attack relation of the result. Each of these constraints can either be hard or soft. This novel framework has both theoretical and practical significance. For example, consider a diagnostic system that initially deems δ1 and δ2 acceptable diagnoses while rejecting δ3. If medical experts later determine that only δ1 should be accepted, our approach seamlessly updates the system to preserve δ1, reject δ2, and continue rejecting δ3, while approaches based purely on minimizing syntactic change could lead to an AF with unwanted additional extensions (including some that contain δ3).

The paper is structured as follows. We begin with a motivating medical diagnosis example, illustrating real-world scenarios which cannot be fully addressed by existing enforcement methods. We then provide the necessary formal background on abstract argumentation and argumentation dynamics. Next, we introduce our formula-based enforcement framework, and show that it generalizes various existing approaches to enforcement [Coste-Marquis et al., 2015; Niskanen et al., 2016; Heine and Ulbricht, 2024] and synthesis [Niskanen et al., 2019] in abstract argumentation. We analyze the computational complexity of the corresponding decision problem under five central extension-based semantics, establishing results ranging from NP to ΣP3 -completeness. For solving ΣP 2 -complete variants of formula-based enforcement, building on earlier algorithmic approaches to hard problems in argumentation dynamics [Niskanen et al., 2016; Wallner et al., 2017; Niskanen et al., 2019; Niskanen and J¨arvisalo, 2020], we develop an exact algorithm based on maximum satisfiability (MaxSAT) solving [Bacchus et al., 2021] and counterexample-guided abstraction refinement (CEGAR) [Clarke et al., 2003; Clarke et al., 2004]. Finally, we empirically evaluate an implementation of the MaxSATbased CEGAR algorithm on a novel form of enforcement in which both semantic and syntactic change is minimized. 1

2 Motivation

Consider an argumentation-based diagnostic system built from medical expertise to automate diagnoses such as eye diseases (e.g., [Kakas et al., 2019]). Using expert-defined argumentation theories, the system derives diagnoses from patient symptoms and clinical indicators, supporting tasks such as emergency triage in ophthalmology. However, its diagnoses may sometimes differ from those obtained by physicians after full examination. In such cases, the systemmust revise its argument-based knowledge by incorporating medical exam results, for instance by adding or removing attacks between arguments so that outcomes align with the ground truth. Any proposed revisions must be validated by experts.

We assume two types of arguments: δ-arguments, supporting diagnoses from observed symptoms, and α-arguments, concerning parameters (e.g., age, medical history) or clinical indicators (e.g., intraocular pressure). This distinction, however, can be omitted. We now examine these cases in detail (considered in Section 4) assuming stable semantics for evaluating argument acceptability. In each scenario, Fa represents the system-diagnosed diseases and Fb represents the medical exam results (green arguments in both graphs). We illustrate possible revisions to Fa to incorporate these results, noting that alternative revisions may also exist.

1 Sketches of proofs and additional results are included in the supplementary material: https://hal.science/hal-05623895.

In Figure (1a), δ2 is the disease diagnosed by the system while δ1 is the disease diagnosed by the medical exam. By updating the attack relation-adding (α2, δ2) and removing (α2, δ1)-δ1 becomes the only acceptable δ argument and the system's unique decision, belonging to the extension E = {δ1, α2, α3}. This illustrates a case where one argument is added to the conclusions while another is removed.

In Figure (1c), δ2 is the disease diagnosed by the system and is confirmed by the medical exam. However, an additional non-contradictory disease, δ3, previously omitted, is also identified and must belong to the same extension as δ2. To include δ3 among the conclusions, the attack (α2, δ3) is removed, resulting in the extension E = {δ2, δ3, α2, α3}.

In Figure (1e), δ2 is diagnosed by the system but not confirmed by the medical exam, while a new disease, δ3-not initially suggested by medical experts-is identified. Consequently, δ2 must be removed from the conclusions, and δ3 added. This is accomplished by deleting the attack (α2, δ3) and adding (α2, δ2), resulting in δ3 being accepted in the (unique) extension E = {δ3, α2, α3}.

In Figure (1g), the system cannot choose between δ1 and δ2, both credulously accepted in E1 = {δ1, α3} and E2 = {δ2, α3}. The medical exam confirms δ1 and rules out δ2, requiring the removal of δ2. Deleting the attack (α3, α1) leads to the unique extension E = {δ1, α1, α3}, reaching the target.

In Figure (1i), the system diagnoses δ2, while the medical exam identifies both δ1 and δ2 as potential diseases. Since δ1 and δ2 are in conflict, both should be credulously accepted. Making δ1 credulously accepted, while keeping it separate from δ2, is achieved by deleting the attack (α2, δ1), resulting in two extensions: E1 = {δ1, α2, α3} and E2 = {δ2, α2, α3}.

Finally, in Figure (1k), the system cannot produce a diagnosis, as both δ1 and δ2 are rejected. The medical exam, however, identifies δ1 as the diagnosed disease, requiring it to be added to the conclusions. Adding the attack (α3, α2) makes δ1 accepted, yielding the unique extension E = {δ1, α1, α3}.

3 Abstract Argumentation and Dynamics

An abstract argumentation framework (AF) [Dung, 1995] is a directed graph F = (A,R) where A is a (finite) set of arguments and R ⊆ A×A is an attack relation. Arguments acceptability is based on the notion of extensions, i.e., sets of collectively acceptable arguments, defined via various semantics. Most semantics are based on conflict-free sets and the notion of defense. Formally, a set E ⊆ A is conflict-free if for all a, b ∈ E, (a, b) ̸∈ R. A set E ⊆ A defends an argument a ∈ A if for all (b, a) ∈ R there exists c ∈ E with (c, b) ∈ R. A conflict-free set is admissible if it defends all its elements. An admissible set is a complete extension if it contains all the arguments that it defends. The ⊆-maximal admissible sets are the preferred extensions, and the unique ⊆-minimal complete extension is the grounded extension. Finally, a conflict-free set is a stable extension if it attacks all the arguments outside of it. We denote by σ(F) the set of σ-extensions of F, with σ ∈ {cf, ad, co, pr, gr, stb} standing (resp.) for conflict-free, admissible, complete, preferred, grounded, and stable semantics. The arguments credσ(F) = ⋃ σ(F) (resp. skepσ(F) = ⋂ σ(F)) are credulously (resp. skeptically) accepted. Finally, given E ∈ σ(F), the set of rejected arguments is E O = {a ∈ A | ∃b ∈ E s.t. (b, a) ∈ R}. See [Dung, 1995; Baroni et al., 2018] for more details on semantics.

Argumentation dynamics has received considerable attention in recent years [Doutre and Mailly, 2018; Baumann et al., 2021]. Notably, in extension enforcement [Baumann and Brewka, 2010], given an AF F and a set of arguments T , the goal is to find an AF F ′ such that T is (included in) an extension of F ′ . Most of existing work focuses on minimizing syntactic change, i.e., F ′ must be as close as possible to F (w.r.t. the number of attacks added or deleted) [Baumann, 2012; Coste-Marquis et al., 2015; Wallner et al., 2017]. In status enforcement [Niskanen et al., 2016], given an AF F and disjoint sets of arguments P and N, the goal is to find an AF F ′ so that all arguments in P are credulous (resp. skeptical) conclusions of F ′ , and no argument in N is a credulous (resp. skeptical) conclusion of F ′ . Again, F ′ must be as close as possible to F w.r.t. the attack relation. Other related notions [Niskanen et al., 2019; Heine and Ulbricht, 2024] are formally described in Section 4.1, where we show that they can be captured as specific instances of formula-based enforcement studied in this work.

4 Formula-Based Enforcement

In this section, we formally define formula-based enforcement. Given a finite set of arguments A, we consider three sets of propositional variables, namely IN(A) = {ina | a ∈ A}, OUT(A) = {outa | a ∈ A} and ATT(A) = {atta,b | a, b ∈ A} which we use to specify semantic and syntactic constraints (either hard or soft) on the resulting solution AF.

Definition 1. A formula-based enforcement instance is a tuple I = (A, Φ+, Φ-, ΦR, w, σ), where Φ+ and Φ- are sets of propositional formulas over IN(A) ∪ OUT(A), ΦR is a set of propositional formulas over ATT(A), w: Φ+ ∪ Φ- ∪ ΦR → N ∪ {∞} is a weight function, and σ is a semantics.

Intuitively, formulas in Φ+ express semantic constraints on what should hold in an extension, while formulas in Φ- express constraints which should not hold in any extension of the solution AF. In turn, ΦR constrain the attack relation of the solution AF. Finally, w determines whether a constraint is hard (w(φ) = ∞) or soft (w(φ) < ∞). For instance, to require an argument a to be credulously but not skeptically accepted, while being attacked by b which is not credulously accepted, we need the formulas ina (a ∈ E for some extension E) and ¬ina (a ̸∈ E ′ for some extension E ′ ) in Φ+, inb in Φ-, and attb,a in ΦR. We continue by formally defining how an AF satisfies each of these formulas: we associate the attacks of the AF, as well as each of its extension, with a truth assignment, and then make use of propositional satisfiability.

Definition 2. For an AF F = (A,R), we define τ F : ATT(A) → {0, 1} as the truth assignment mapping τ F (atta,b) = 1 iff (a, b) ∈ R. For an extension E ∈ σ(F), we define τ E : IN(A) ∪ OUT(A) → {0, 1} mapping τ E (ina) = 1 iff a ∈ E, and τ E (outa) = 1 iff a ∈ E O . Given an instance I = (A, Φ+, Φ-, ΦR, w, σ), an AF F = (A, R) satisfies

• φ ∈ Φ+ if there exists E ∈ σ(F) s.t. τ E satisfies φ;
• φ ∈ Φ- if there is no E ∈ σ(F) s.t. τ E satisfies φ;
• φ ∈ ΦR if τ F satisfies φ.

We write F |= φ if F satisfies a formula φ ∈ Φ+ ∪Φ- ∪ΦR.

Let I be a formula-based enforcement instance. An AF F is a solution of I if it satisfies each formula φ ∈ Φ+ ∪ Φ- ∪ ΦR with w(φ) = ∞, i.e., all of the hard constraints. Weights of soft constraints are used to compare the quality of different solutions of I. The cost of an AF F is the sum of the weights of formulas in Φ+ ∪ Φ- ∪ ΦR not satisfied by F. Formally,

An AF F is an optimal solution of I if it achieves minimum cost over all AFs with the same set of arguments, i.e., there is no AF F ′ = (A, R′ ) with COST(I, F ′ ) < COST(I, F).

The proposed approach offers a generic and versatile framework that captures various enforcement and synthesis problems in the literature. For example, hard constraints in Φ+ and Φ- can be used to describe knowledge on the acceptance status of arguments, which must be incorporated into the current AF by revising it in a syntactically minimal sense, which in turn is achieved by including soft constraints in ΦR describing the attack structure of the AF. On the other hand, in a pure synthesis setting the set ΦR is empty, whereas the sets Φ+ and Φ- can be used to describe positive and negative examples on the extensions of the inferred AF. This formulabased approach is proposed because it allows us to furnish the technical mechanisms to achieve the simultaneous capture and minimization of syntactic and semantic changes within a single unified framework.

4.1 Relation with other forms of enforcement

We continue by formally proving connections to well-known forms of enforcement and synthesis approaches, specifically by showing how they are captured as instances of formulabased enforcement. We begin by introducing several notations for useful formulas. Given F = (A,R), we define the set of formulas (unit clauses) ΦF = {atta,b | (a, b) ∈ R} ∪ {¬atta,b | (a, b) ̸∈ R} capturing the syntax of F. For a set of arguments T ⊆ A, we define several formulas. To represent that T must be included in an extension, we define φT⊆ = ∧a∈T ina; for representing that T is an extension, we define φT= = φT⊆ ∧ ∧a∈A\T ¬ina. Finally, to constrain T to be the rejected set w.r.t. an extension (i.e. T = E O with E an extension), we define φTout = ∧a∈T outa ∧ ∧a∈A\T ¬outa. Finally, to characterize syntactic change, we use the symmetric difference between A and B, A△B = (A \ B) ∪ (B \ A).

We start with (argument-fixed) extension enforcement [Coste-Marquis et al., 2015; Wallner et al., 2017].

Definition 3. An extension enforcement instance is a tuple (F, T , σ) where F = (A,R), T ⊆ A is a set of arguments, and σ an argumentation semantics. A solution of the enforcement problem is an AF F ′ = (A,R′ ) such that there exists E ∈ σ(F ′ ) with T ⊆ E (non-strict enforcement). A solution is optimal if it minimizes |R△R′ |.

Proposition 1. Let (F, T , σ) be an instance of nonstrict extension enforcement, and define I NSTR = (A, {φT⊆ }, ∅,ΦF ,w, σ) as the formula enforcement instance where w(φT⊆ ) = ∞, and w(φ) = 1 for all φ ∈ ΦF . It holds that F ∗ is an optimal solution to (F, T , σ) iff F ∗ is an optimal solution to I NSTR .

Other forms of extension enforcement can also be captured, including enforcement under different forms of expansions [Baumann and Brewka, 2010; Baumann, 2012]; roughly speaking, an expansion is a modification of an AF where only addition of arguments and attacks is allowed, but no argument or attack is removed. This can be captured as formula-based enforcement via hard constraints in ΦR that guarantee that F ∗ is a suitable expansion of F, and using a bounded number of auxiliary arguments (i.e., constructing the result on the set of arguments A′ with A ⊂ A′ ).

We move on to status enforcement [Niskanen et al., 2016].

Definition 4. A credulous status enforcement instance is a tuple (F, P,N, σ) where F = (A,R), P,N ⊆ A, and σ is a semantics. A solution of the enforcement problem is F ′ = (A,R′ ) such that P ⊆ credσ(F ′ ) and N ∩ credσ(F ′ ) = ∅. A solution is optimal if it minimizes |R△R′ |.

Proposition 2. Let (F,P,N, σ) be an instance of credulous status enforcement, and define I CRED = (A,ΦP ,ΦN ,ΦF ,w, σ) as the formula enforcement instance where ΦP = {ina | a ∈ P}, ΦN = {¬ina | a ∈ N}, w(φ) = ∞ for all φ ∈ ΦP ∪ ΦN , and w(φ) = 1 for all φ ∈ ΦF . It holds that F ∗ is an optimal solution to (F, P,N, σ) iff F ∗ is an optimal solution to I CRED .

We continue with rejection enforcement [Heine and Ulbricht, 2024] where the goal is to ensure that a set of arguments is rejected, i.e., is exactly the set of arguments E O attacked by an extension E.

Definition 5. A rejection enforcement instance is a tuple (F, T , σ) where F = (A,R), T ⊆ A, and σ is a semantics. A solution of the rejection enforcement instance is an AF F ′ = (A,R′ ) such that T = E O for some E ∈ σ(F ′ ). Moreover, F ′ is consensus preserving if σ(F) ⊆ σ(F ′ ). Finally, F ′ is optimal if it minimizes |R△R′ |.

The original definition of rejection enforcement uses expansions. As discussed previously, expansions are captured by adding suitable hard constraints to ΦR and auxiliary arguments. For readability, we disregard these constraints here.

Proposition 3. Let (F, T , σ) be a rejection enforcement instance, and define I REJ = (A, {φS= | S ∈ σ(F)}, {φTout},ΦF ,w, σ) where w(φ) = ∞ for all φ ∈ Φ+ ∪ Φ-, and w(φ) = 1 for all φ ∈ ΦF . It holds that F ∗ is a consensus preserving optimal solution to (F, T , σ) iff it is an optimal solution to I REJ .

Finally, we show a connection to AF synthesis [Niskanen et al., 2019]: given positive examples of extensions and negative examples of non-extensions, we need to find F such that positive examples are extensions of F and no negative example is an extension. Examples which are not satisfied incur a cost, and the goal is to find a solution of minimum cost.

Definition 6. An AF synthesis instance is a tuple (A, E+, E-, σ) where A is a finite set of arguments, E+ and E- are sets of weighted extensions (S, w) with S ⊆ A and w > 0 an integer, and σ is a semantics. A solution of the synthesis problem is an AF F = (A,R). The cost of an F is ∑(S,w)∈E+|S̸∈σ(F) w + ∑(S,w)∈E-|S∈σ(F) w. An AF is optimal if it achieves minimum cost.

Proposition 4. Let (A,E+,E-, σ) be an instance of AF synthesis, and define I SYNTH = (A,ΦE+ ,ΦE- , ∅,w, σ) as the formula enforcement instance where ΦE+ = {φS= | (S,wS) ∈ E+}, ΦE- = {φS= | (S,wS) ∈ E-}, and for each (S,wS) ∈ E+ ∪ E-, w(φS=) = wS. It holds that F ∗ is an optimal solution to (A, E+, E-, σ) iff F ∗ is an optimal solution to I SYNTH .

4.2 Novel forms of enforcement and synthesis

Our framework can capture novel notions of synthesis and enforcement. Starting with synthesis, we can express complex constraints that need to be satisfied by the result, e.g. ((¬ina∧ ¬inb) → inc) ∈ Φ+ requires that if there is an extension which does not contain a nor b, then c belongs to the extension. Moreover, formulas can capture credulous (resp. skeptical) constraints, i.e., those which must be satisfied by some (resp. each) extension. For instance, (ina ∨ inb) ∈ Φ+ results in an AF that has at least one extension that contains either a or b, whereas the formula (¬ina ∧ ¬inb) ∈ Φ-, induces an AF where either a or b belongs to every extension.

In the context of enforcement, an important feature of the formula-based approach is its capability to model both semantic (i.e., w.r.t. the acceptance of arguments) and syntactic (i.e., w.r.t. the structure of the AF) change. These notions can also be combined in various ways. For example, one can give more priority to syntactic change by specifying larger weights to the corresponding constraints. When it is equally important to keep the structure of the AF as well as the acceptance status of its arguments, we can use the same weight for each formula. The formula-based enforcement framework also allows for minimizing semantic change and syntactic change in a lexicographic way by selecting suitable weights. For instance, assigning to "syntactic" formulas φ ∈ ΦR the weight w(φ) = 1, and to "semantic" formulas φ ∈ Φ+ ∪ Φ- the weight w(φ) = |ΦR|+1, induces higher priority to semantic change, and lower priority to syntactic change.

We also distinguish between hard and soft constraints, with hard constraints specified using infinite weights. For instance, assume a scenario where both α and β must absolutely be credulously accepted, and if possible they should be accepted together, i.e., in the same extension (but if it is not possible, then they might be accepted in different extensions). Finally, syntactic change |R△R′ | should be minimized. In this case we define the formula enforcement instance with Φ+ = {inα, inβ, inα ∧ inβ}, Φ- = ∅, ΦR = {atta,b | (a, b) ∈ R} ∪ {¬atta,b | (a, b) ̸∈ R}. The unit clauses in Φ+ are hard constraints with w(inα) = w(inβ) = ∞, while the third formula has weight w(inα ∧ inβ) = |A|2 + 1 higher than the number of formulas in ΦR, which in turn have unit weight.

The following concept illustrates how lexicographic optimization can be applied to capture more advanced forms of enforcement. An instance of credulous status enforcement with soft joint acceptance constraints (F, P, N , P ∧, N ∧, σ), is an extension of credulous status enforcement (Def. 4), where P ∧, N ∧ are collections of positive and negative target sets. The goal is to enforce as many positive target sets collectively (in the sense of non-strict extension enforcement), and as few negative target sets as possible (reminiscent of positive and negative examples in AF synthesis). We use the following notation: given a set U, a set A ⊆ U, and a set of sets B ⊆ 2U , L(A, B) is true iff there is a set S ∈ B s.t. A ⊆ S.

Definition 7. An instance of credulous status enforcement with soft joint acceptance constraints is a tuple (F,P,N,P ∧,N ∧, σ), where F = (A,R), P,N ⊆ A, P ∧,N ∧ ⊆ 2A, and σ is an argumentation semantics. A solution of the enforcement problem is an AF F ′ = (A,R′ ) such that each p ∈ P is credulously accepted w.r.t. σ, no n ∈ N is credulously accepted w.r.t. σ, and F ′ minimizes ∑S+∈P ∧[¬L(S+, σ(F ′ ))] + ∑S-∈N ∧[L(S-, σ(F ′ ))]. A solution is syntactically optimal if it minimizes |R△R′ |.

We extend the notation φT⊆ from a set of arguments T to a collection of sets S by defining φS⊆ = {φT⊆ | T ∈ S}.

Proposition 5. Let (F,P,N,P ∧,N ∧, σ) be an instance of credulous status enforcement with soft joint acceptance constraints, and define I CRED SEM,SYN = (A,ΦP ∪ ΦP ∧ ,ΦN ∪

ΦN ∧ ,ΦF ,w, σ) as the formula-based enforcement instance with ΦP = {ina | a ∈ P}, ΦP ∧ = φP ∧ ⊆ , ΦN = {ina | a ∈ N}, ΦN ∧ = φN ∧ ⊆ , w(φ) = ∞ for all φ ∈ ΦP ∪ ΦN , w(φ) = |A|2 + 1 for all ΦP ∧ ∪ ΦN ∧ , and w(φ) = 1 for all ΦF . It holds that F ∗ is a syntactically optimal solution to (F,P,N,P ∧,N ∧, σ) iff F ∗ is an optimal solution to I CRED SEM,SYN .

In addition to using P ∧ to model that as many extensions as possible need to be preserved, note that semantic distance in terms of credulously accepted arguments can be minimized by including ⋃ σ(F ) into P and A \ ⋃ σ(F ) into N .

Finally, we demonstrate our framework's instantiation through the real-world cases of the medical diagnosis problem introduced in Section 2. Through these instantiations, the target argumentation framework Fb is obtained from Fa. For Case 1: Φ+ = {inδ1 , inα2 , inα3 }, Φ- = {inδ2 }, ΦR = {attα2,δ1 , attα3,α1 , attα1,α2 , attα2,α1 , attδ1,δ2 , attδ2,δ1 , attα1,δ2 }∪{¬attδ1,α2 , ¬attδ1,α3 , ¬attα3,α2 , ¬attα2,α3 , ¬attα3,δ2 , ¬attδ2,α3 , ¬attα1,δ1 , ¬attδ1,α1 , ¬attα3,δ1 }. We do not repeat ΦR for the other cases since it is similar. For Case 2: Φ+ = {inδ2 , inδ3 , inα2 , inα3 , inδ2 ∧ inδ3 } and Φ- = {inδ1 }. In this case inδ2 ∧ inδ3 ∈ Φ+ encodes the requirement that δ2 and δ3 must belong to the same extension. For Case 3: Φ+ = {inδ3 , inα2 , inα3 } and Φ- = {inδ1 , inδ2 }. For Case 4: Φ+ = {inδ1 , inα1 , inα3 } and Φ- = {inδ2 }. For Case 5: Φ+ = {¬inδ1 , inδ1 , ¬inδ2 , inδ2 , inα2 , inα3 } and Φ- = {inδ1 ∧ inδ2 }. In this case, ¬inδ1 , inδ1 ,¬inδ2 and inδ2 encode the requirement that δ1 and δ2 must be credulously accepted, while inδ1 ∧ inδ2 ∈ Φexpresses that they cannot belong to the same extension. Finally, for Case 6: Φ+ = {inδ1 , inα1 , inα3 } and Φ- = {inδ2 }.

In all these cases, formulas φ ∈ Φ+ ∪ Φ- are hard constraints (w(φ) =∞). In contrast, formulas φ′ ∈ ΦR are soft constraints with w(φ′ ) = 1, representing the initial AF. Consequently, our method computes a new AF (i.e., Fb) that is as close as possible (in syntactic terms) to the original (i.e., Fa) while ensuring all semantic constraints are satisfied. We emphasize that our approach is capable of capturing all these cases, as well as their combinations, whereas existing approaches in the literature are unable to do so.

5 Complexity Results

We study the complexity of the following problem: given I = (A, Φ+, Φ-, ΦR, w, σ), and a non-negative integer k ∈ N, is there an AF F = (A, R) with COST(I, F) ≤ k?

As usual, grounded semantics exhibits lower complexity than admissible, complete and stable semantics, which are in turn more tractable than preferred semantics.

Proposition 6. Formula-based enforcement is NP-complete for σ = gr; ΣP 2 -complete for σ ∈ {ad, co, stb}; and ΣP 3 - complete for σ = pr.

Restricted variants of formula-based enforcement may exhibit milder complexity than the general case.

Proposition 7. Formula-based enforcement under σ ∈ {ad, co, stb} is NP-complete when Φ- = ∅.

Algorithm 1 MaxSAT-based CEGAR for formula enforcement. Input: Arguments A, sets of formulas Φ+,Φ-,ΦR, weight function w, semantics σ ∈ {ad, stb}.

• 1: (φhard, φsoft) ← ABSTRACTIONσ(A,Φ+,Φ-,ΦR,w)
• 2: while true do
• 3: (result, τ ) ← MAXSAT(φhard, φsoft)
• 4: if result = unsat then return false
• 5: R←ATTACKSTRUCTURE(τ); F ← (A,R)
• 6: φcex ← COUNTEREXAMPLEσ(Φ-,w,F, τ)
• 7: (result, τcex) ← SAT(φcex)
• 8: if result = unsat then return F
• 9: E ←EXTENSION(τcex)
• 10: φhard ←φhard ∧ REFINE(Φ-,w,F, E, τcex)

6 Algorithms

Now we present an algorithm for solving ΣP 2 -complete formula enforcement under admissible and stable semantics. 2 Our approach is based on using a MaxSAT solver [Bacchus et al., 2021] in an iterative counterexample-guided abstraction refinement (CEGAR) [Clarke et al., 2003; Clarke et al., 2004] procedure. The core idea is to iteratively solve an abstraction in NP, i.e., an over-approximation of the set of (optimal) solutions, obtaining solution candidates. At each iteration we check whether the current candidate is a valid solution by searching for a counterexample. If a counterexample is found, the abstraction is refined by adding a constraint which prevents the counterexample from occurring in future iterations. This continues until no counterexamples are found-i.e., the candidate solution is valid-or there are no more solutions to the abstraction, i.e., the problem has no solution either.

For background on SAT and MaxSAT, recall that for a Boolean variable x, there are two literals, x and ¬x. A clause C is a disjunction (∨) of literals. A conjunctive normal form (CNF) formula φ is a conjunction (∧) of clauses. A truth assignment τ maps each variable in φ to 0 (false) or 1 (true), and extends to literals via τ(¬x) = 1 - τ(x), to clauses via τ(C) = max{τ(l) | l ∈ C}, and to CNF formulas via τ(φ) = min{τ(C) | C ∈ φ}. Given a CNF formula φ, the Boolean satisfiability problem (SAT) asks whether there is an assignment τ with τ(φ) = 1. If there is, φ is satisfiable, and otherwise φ is unsatisfiable. In the MaxSAT problem [Bacchus et al., 2021], we are given a set of hard clauses φhard and a set of weighted soft clauses φsoft consisting of pairs (C,wC). The task is to find a truth assignment τ with τ(φhard) = 1 which minimizes the cost ∑(C,wC)∈φsoft wC(1 - τ (C)).

We begin by detailing our MaxSAT encoding of the NP abstraction, which, in line with Proposition 7, relaxes the constraints expressed by formulas in Φ- . The atta,b variables for each a, b ∈ A are directly used in the encoding to represent the solution AF. For each φ ∈ Φ+, we declare fresh variables inφa and outφa for each a ∈ A, representing an extension witnessing the satisfaction of φ. Then, for each φ ∈ Φ+ and

2 The algorithm can be adapted to complete semantics as well; however, our focus is on the new form of credulous status enforcement, for which admissible and complete semantics coincide.

ψ ∈ Φ+ ∪ Φ-, we let ψφ = ψ[ina ↦→ inφa | a ∈ A][outa ↦→ outφa | a ∈ A], that is, ψφ is the formula ψ with variables ina and outa replaced with variables corresponding to formula φ. Finally, for each φ ∈ Φ- with w(φ) < ∞, we declare a fresh variable satφ to indicate the satisfaction of φ.

Our algorithm is presented as Algorithm 1. We start by initializing an abstraction (line 1) as a MaxSAT instance (φhard, φsoft). The hard clauses are defined as

where the first conjunction encodes for each formula φ ∈ Φ+ a σ-extension witnessing its satisfaction, and the latter two enforce that each formula φ ∈ Φ+ ∪ ΦR with w(φ) = ∞ must be satisfied. To encode a σ-extension, we define EXTφσ (A, Φ-, w) as ∧a∈A(outφa ↔ ∨b∈A(attb,a ∧ inφb )) ∧ SEMφσ (A) ∧ AUXφ(Φ-, w), where the first conjunction encodes the interpretation of out-variables, SEMφσ (A) encodes the semantics-in line with MaxSAT encodings for extension and status enforcement [Wallner et al., 2017; Niskanen et al., 2016]-via SEMφcf (A) = ∧a,b∈A(atta,b → (¬inφa ∨ ¬inφb )), SEMφad (A) = SEMφcf (A) ∧ ∧a,b∈A((attb,a ∧ inφa ) → outφb ), and SEMφstb (A) = SEMφcf (A) ∧ ∧a∈A(inφa ∨ outφa ). Finally, AUXφ(Φ-,w) = ∧ψ∈Φ-,w(ψ)=∞ ¬ψφ ∧ ∧ψ∈Φ-,w(ψ)<∞(¬satψ ∨ ¬ψφ), accounting for negative formulas by stating that for ψ ∈ Φ-, if w(ψ) = ∞ or satψ is set to true, ψ is not satisfied by the witnessing extension for φ. 3 The weighted soft clauses φsoft are {(φ,w(φ)) | φ ∈ ΦR,w(φ) < ∞} ∪ {(φφ,w(φ)) | φ ∈ Φ+,w(φ) < ∞} ∪ {(satφ, w(φ)) | φ ∈ Φ-, w(φ) < ∞}, directly modeling the cost function of formula-based enforcement.

We iteratively solve the abstraction, querying a MaxSAT solver for a candidate solution (line 3). If no candidate solution exists, there is no solution to the formula-based enforcement problem either, and we return false (line 4). Otherwise, we extract the candidate attack structure R from the optimal MaxSAT solution τ via ATTACKSTRUCTURE(τ) = {(a, b) ∈ A × A | τ(atta,b) = 1}. It remains to check whether F = (A,R) is an optimal solution to the formulabased enforcement problem by searching for a counterexample, namely an extension which satisfies a formula φ ∈ Φfor which either w(φ) = ∞ or τ(satφ) = 1. We construct a propositional formula (line 6), defined as

Here, SEMσ(F) is the SAT encoding of semantics σ [Besnard and Doutre, 2004], i.e., SEMcf(F) = ∧(a,b)∈R(ina ∨ inb), SEMad(F) = SEMcf (F)∧ ∧a∈A(ina → ∨(b,a)∈A outb), and SEMstb(F) = SEMcf (F) ∧ ∧a∈A(ina ∨ outa).

3 When Φ+ = ∅, we use a trivial formula to encode an arbitrary σ-extension and add the same constraints on negative formulas.

We call a SAT solver on the formula φcex (line 7). If it is unsatisfiable, we return the current solution F (line 8) as an optimal solution to the formula enforcement problem. Otherwise, we extract the counterexample extension EXTENSION(τcex) = {a ∈ A | τcex(ina) = 1} (line 9). We refine the abstraction by adding a constraint to φhard preventing E from reoccurring as an extension in subsequent candidate solutions. In particular, we adapt the strong refinement developed for extension and status enforcement [Niskanen and J¨arvisalo, 2020] to our setting. If there is a formula φ ∈ Φ- with w(φ) = ∞ satisfied by E, we add the clause

requiring that we change the attack structure so that the counterexample extension E no longer exists. If, in turn, there is a formula φ ∈ Φ- with w(φ) < ∞ and τ (satφ) = 0 satisfied by E, we instead add a set of clauses (satφ ∨ REFINE(F, E)) for each such formula φ. These clauses require that in order to set satφ to false, we need to change the attack structure so that E is no longer an extension.

7 Empirical Evaluation

Our implementation of the MaxSAT-based CEGAR algorithm from Section 6 is available online in open source at https://bitbucket.org/andreasniskanen/phiaf. We use PySAT (version 1.8.dev23) [Ignatiev et al., 2018] to interface with the MaxSAT solver RC2 [Ignatiev et al., 2019] and the SAT solver Glucose (version 3.0) [Audemard and Simon, 2009]. The experiments were run on 2.50-GHz Intel(R) Xeon(R) Gold 6248 CPUs. We imposed a 600-second per-instance time and a 32-GB memory limit and measured CPU time via runsolver [Roussel, 2011]. We generated benchmark instances for credulous status enforcement with soft joint acceptance constraints as follows. Our initial AFs are based on the D(n, p, q) random model [Gao, 2017] of AFs with n arguments, in which an attack between a pair of arguments exists with probability p, and is symmetric with conditional probability q. Given probability p, we set q = q(p) to the threshold of the phase transition exhibited by the model (specifically so that 4q/(1 + q)2 = p) to obtain nontrivial instances. For each n = 20, 30, . . . , 200 and p = 0.025, 0.05, 0.1, 0.2, 0.4, we sample 10 AFs F = (A, R) from D(n, p, q(p)). For each AF, we generate the input P,N,P ∧,N ∧ as follows. For P and N, we sample two sets S, T of n/10 arguments from A without replacement, and set P = (S ∪ ⋃ σ(F)) \ T and N = A \ P. Finally, for both P ∧ and N ∧, we sample 5 sets of size n/10 from A \ N. In total, this results in 950 input instances.

Our results are summarized in Table 1 for stable semantics and in Table 2 for admissible semantics. Under stable, the implementation scales up to 70 arguments, with > 80 % of instances solved up to n = 70 with < 65-second mean CPU times. Sparse input AFs seem to give rise to easier instances, as for p = 0.025 all instances are solvable up to n = 90, while for p ∈ {0.2, 0.4} this is the case up to n = 40. In contrast, enforcement under admissible semantics is in general empirically harder, with > 80%

of instances solved only up to n = 30. For an explanation, note that since we encode an extension for each argument in (⋃ σ(F) ∪P) \ N, | ⋃ σ(F)| directly affects the size of the initial MaxSAT encoding. In our setup 147/950 initial AFs satisfy | ⋃ ad(F)| - | ⋃ stb(F)| > 0, and this difference is ≈ 0.17n on average when nonzero. In addition, the number of iterations (i.e., solver calls) is considerably higher, averaging ≈ 2100 under admissible and ≈ 46 under stable. Intuitively, since there are considerably more admissible than stable extensions, counterexamples are more likely. Both effects are more pronounced on sparse AFs, which due to minimizing syntactic distance result in sparse candidate AFs.

8 Conclusion

We introduced a novel approach for argumentation dynamics based on the enforcement of formulas in the extensions of an abstract argumentation framework. This approach captures all existing notions of enforcement and synthesis proposed in the literature, as well as new variants that minimize both syntactic and semantic distance, such as status enforcement with soft joint acceptance constraints, which are not addressed by existing approaches and are introduced in this work. We pinpointed the exact complexity of the corresponding decision problem under five key semantics, and provided a computational approach for solving second-level-complete variants in the form of a MaxSAT-based CEGAR algorithm. Our evaluation demonstrates the scalability of the approach to 30-70 arguments.

Ethical Statement

There are no ethical issues.

Acknowledgments

Work financially supported by the Research Council of Finland (grant 347588), the EuroHPC Joint Undertaking and its members including top-up funding by Ministry of Education and Culture of Finland, and the French National Research Agency (ANR grants AIDAL ANR-22-CPJ1-0061-01, AGGREEY ANR-22-CE23-0005 and GRAIL ANR-25-CE235597). The authors thank the Finnish Computing Competence Infrastructure (FCCI) for computational and data storage resources.

Funded by the European Union. Views and opinions expressed are however those of the author(s) only and do not necessarily reflect those of the European Union or EuroHPC. Neither the European Union nor EuroHPC can be held responsible for them.