argumentation, reasoning, preferred semantics, algorithms Formal argumentation is a research field within the area of knowledge representation and reasoning that ofers a great variety of formalis2m],sa[nd the(abstract) argumentation framework (AF) introduced by Dung [3] is a core area of research. In an argumentation framework, arguments are modelled as abstract entities and we consider directed attacks between them as the only relation. Reasoning in argumentation frameworks is via acceptability semantics, which are functions that return sets of arguments, calleedxtensions, considered jointly acceptable. A fundamental property of acceptable sets is admissibility, which requires that a set of arguments is conflict-free and also defends all of its members against attacks from the other arguments. For instapnrcefee,rtrehdeextensions are then simply defined as the⊆-maximal admissible set3s].[ One can then define diferent reasoning problems based on these semantic4s].[ One of the most prominent ones is the problemskeopftical reasoning wrt. some semantics, i. e., deciding whether a given argument is contained in every extension wrt. the given semantics. In general, most of these reasoning problems are non-tr4a]c.tEaspbelcei[ally because of that, algorithms to eficiently compute these problems are of great importance in order to apply argumentation in practice.
ceur-ws.org
In this work, we introduce a noSvaetl-based algorithm for solving the problem of skeptical reasoning wrt. preferred semantics. This algorithm is built upon recent results on the characterisation of preferred semantics as a vacuous-reduct semant1i4c]s. E[ssentially, our algorithm searches through complete extensions and looks for one that disproves the skeptical acceptance of the query argument by being incompatible with it. In contrast to existing work, the algorithm does not maximise each complete extension and instead continues searching for new complete extensions containing unvisited arguments. Our algorithm also employs efective preprocessing measures, outlined by Liao and[H15u]a,tnog simplify computation. Thus, our algorithm is able to solve the problem of skeptical preferred reasoning without having to actually compute the preferred extensions, similar to the approach of Thimm et al. [9]. Moreover, we show that our algorithm is sound and complete and our experiments show that it significantly outperforms current state-of-the-art solvers on most benchmarks.
To summarise, the contribution of this work is twofold: • We introduce a novel algorithm for skeptical reasoning wrt. preferred semantics and show that it is sound and complete (Secti3o)n, • We implement our algorithm and evaluate it against state-of-the-art argumentation solvers (Section4).
In Section2 we introduce the necessary background on abstract argumentation, i5nwSection discuss related work and Sect6iocnoncludes the paper.
We consider abstract argumentation as introduced by3D].uTnhge[central notion is tahbestract argumentation framework (AF), which is a tupleF = (A, R)whereA is a finite set of arguments anRd is the attack relatRion⊆ A × A. For any two argument,s ∈ A, we say tha t attacks if ( , ) ∈ R, sometimes also written aRs . For a set of argument⊆s A we denote withF| = (, R ∩ ( × )) therestriction of F to . Furthermore, for a se⊆t A we define the set of arguments attacked by (attacking) in F respectively as F+ = { ∈ A ∣ ∃ ∈ ∶ R },
F− = { ∈ A ∣ ∃ ∈ ∶ R }.
If = { } is a singleton set, we also w ri+te(respectively− ) for readability. Moreover, we say that
F F is conflict-free if we have ∩ F+ = ∅. The set defends an argument ∈ A if for all ∈ − there is F some ∈ such tha tR . Furthermor e, is calledadmissible if it is conflict-free and defends all ∈ , i. e., we have that∩ F+ = ∅ and F− ⊆ F+ . We denote withad(F) the admissible sets oFf.
We can now impose further constraints on admissible sets to obtain diferent argumentation semantics [16]. In particular, an admissible s⊆etA is called a • complete (CO) extension if for every ∈ A, if defends then ∈ , • preferred (PR) extension if there exists no admissib l′e with ⊊ ′, • grounded (GR) extension if is complete and there is no compl e′tewith ′ ⊊ .
For a given argumentation framewFor=k (A, R) and a semantic s∈ { CO, PR, GR}, we denote with( F) the set of -extensions oFf.
Example 1. Consider the argumentation framewFordkepicted in Figur1e. The complete extensions of F are{ }, { , , } and{ , , , ℎ}. Note that, for instan{ce,,} is admissible, but not complete since it also defends. Furthermore{, , , } and{ , , , ℎ} are the preferred extensionsFo.fFinally{, } is the minimal complete extension and thus the unique grounded extenFsi.on of ℎ
is contained in a l-lextensions oFf,
Example 2. Consider again the argumentation framewFoirnkFigure1. For complete and preferred semantics the argumen t, s, , andℎ are credulously accepted, w hi, le, and are not credulously accepted wrt. any semantics. For the grounded sem anistibcosth the only credulously and skeptically accepted argument.
For complete and preferred semant icis,also skeptically accepted. Interestingly, wihsinleot skeptically accepted wrt. complete semantics, it is however skeptically accepted wrt. preferred semantics, since it is contained in both preferred extensions, cf. Exa1.mple
The computational complexity of these problems has been well studied, we refer the interested reader to [4] for an overview. The prevalent strategy to solve many of these problems is reducing them to satisfiability problems (Sat) and using a dedicateSdat-solver for solving those, c5f,. 8[].
In particular, we want to highlight two results which are of importance for our work. The problem SE-GR is inP, i. e., computing the grounded extension of an AF can be done in polynomial time. Secondly, the problem of skeptical reasoning wrt. preferred sem(aDnSt-iPcRs)is Π2-complete. Most importantly, that means it cannot be solved by a siSnagtl-ecall and it is one of the more dificult decision problems in abstract argumentation. In particular, the pDroSb-PlRemwill be the main focus of this work.
In this section, we present our main contribution, a novel algorithm for skeptical reasoning wrt. preferred semantics. We first outline in Sect3i.o1nthe underlying ideas of our algorithm, which are based on a combination of results and characterisations from the literature. Afterwards we describe theSat-encoding used by our approach (Secti3o.2n). Finally, we present our algorithm for skeptical reasoning wrt. preferred semantics (Sec3t.3io) nand show that it is sound and complete in Sec3t.4i.on
Our approach is built on the concepctoounfterexample guided abstraction refinement (CEGAR) [17].
This concept is widely used by argumentation sol8v,e9r]s a[nd has been pioneered by thCeEGARTIX
system [7] for the domain of abstract argumentation. Given an argumentation frFamaenwdoark
query argument, the general idea is to find complete extensions of sub-frameworFksaotftacking the
query argument. The general procedure of our algorithm consists of the following steps:
(
During each step, we actively check whether the query argument is attacked by the current (partial) counterexample, which can allow us to terminate sooner.
Let us start with considering the relevant notions and results from the literature that our algorithm built upon. LeFt = (A, R)be an arbitrary argumentation framework∈anAdis the query argument in question.
Simplifying the Argumentation Framework. The first step in our approach is simplifying the problem instance, without afecting the result, to accelerate the subsequent problem solving process. This kind of preprocessing is an important part of many problem solving paradigms, for instance Sat-solving 1[8]. In the context of abstract argumentation, this can mean replacing parts of the argumentation framework with simplified structu1r9e]so[r removing parts of the framework altoge1t5h]e.r [ In this work, we consider only the latter approach.
The simplification performed by our algorithm consists essentially of two steps:
(
The first step is based on the principle Dofirectionality for argumentation semantics and has already been outlined by Liao and Huan1g5][. For that, for some argumentation frameFwo=rk(A, R), we ifrst define the set of unattacked sets of F.
UA(F) = { ⊆ A ∣ ∄ ∈ (A ∖ ) ∶ ∈ F− }
Principle 1. Let be a semantics. We say thatsatisfies Directionality if and only if for all argumentation frameworksF and every se t∈ UA(F) it holds th a(tF| ) = { ∩ ∣ ∈ ( F)}.
Essentially, the above principle states that the computation of an extension for a ssehmouanldtics only depend on its attackers (and in turn on their attackers and so on). As has been shown by Baroni and Giacomin2[0], both the complete and preferred semantics saDtiirsefcytionality.
Proposition 1. Complete and preferred semantics satisfy Directionali.ty
Now we can determine an unattacke d∈setUA(F)that contains the query argum eanntd restrict the argumentation framework to simplify the computation without afecting the acceptance status of the query argument.
A simple but efective way to achieve this is to consider the argumreelnevtasnt for . For two arguments, ∈ A we say tha t is relevant for if there exists a directed path fr omto . We then define the set of argumentrselevant for in F as follows.
RelF ( ) = { } ∪ { ∈ A ∣ is relevant fo r}
(
Example 3. Consider again the argumentation framewFoirnkFigure1. We examine the argume nt. It is easy to observe thRaetl ( ) = { , , , , , ℎ, }. Note that for bothand there exists no directed path to thus they are not relevant f.oSrimilarly, we also havReelF ( ) = { , } andRelF ( ) = A1. argumen t.
For convenience, we explicitly define th atis always relevant for itself. Notably, this notion of relevance has already been used1i5n],[but also recently been defined in the context of acceptance explanations by Borg and Be2x1[]. It is then easy to see thRaetlF ( ) is an unattacked setFoffor any Corollary 1. For all AFs F = (A, R) and arguments ∈ A it holds that RelF ( ) ∈ UA(F).
According to the directionality property, this allows us to restrict the input argumentation framewor to just the arguments relevant for the qubeerfoyre performing further calculations. This does not only allow us to ignore arguments that are only attacked by the query, but also enables us to disregard unrelated components of the argumentation framework entirely.
The second simplification we perform is explicitly computing the grounded extension of the AF, which can be done in polynomial tim4e].[For that we utilise the simple iterative procedure for computing the grounded extension that has been outline3d].bAys[we will show in the following paragraphs, we can then remove the grounded extension and everything attacked by it from the argumentation framework, to simplify the subsequently creSaatte-dencoding.
Iterating Complete Extensions We are concerned with the problem of skeptical reasoning wrt. preferred semantics. This, however, does not mean, that we have to explicitly compute preferred extensions to solve this proble9m]. [Instead, we will primarily consider complete extensions.
The main notion underlying our algorithm is-rtehdeuct introduced by Baumann et2a2l]. [ Definition 1. LetF = (A, R)be an AF and ⊆ A. We define the -reduct of F as F = (A′, R′)with A′ = A ∖ ( ∪ F+ ),
R′ = R ∩ (A′ × A′).
Essentially, the reduct allows us to remove the part ofFthtehaAtFis already “resolved” b.y -reduct oFf is the argumentation framewFor{k, , } depicted in Figur2e.
Example 4. Consider again the argumentation framewFoirnkFigure1. Let = { , , }, then the
Based on this concept, the notionvaocfuous reduct semantics has been introduced14[].
Definition 2. Let be a semantics anFd is an AF. We say thaFt is -vacuous if ( F) ⊆ {∅}. set ⊆ A is a -extension if is a -extension and it holds thFa tis -vacuous.
Definition 3.
Let, be argumentation semantics aFnd= (A, R) is an argumentation framework. A non-empty -extension. We denote wit h(F) the set of a ll -extensions oFf.
Intuitively, a s etis a extension oFf if it is -extension oFf and in the reducFt there exists no Example 5. Consider again the argumentation framewFoirnkFigure1. Let us consider the vacuous reduct semanticcsfad, i. e., the conflict-free sets such that the reduFct contains no non-empty admissible set2s. Examine, for instance, the se1t= { , , }. Clearl y 1 is conflict-free inF. The reduct F 1 is depicted in Figur2e. It is easy to verify th∅atis the only admissible setFof1, thus 1 is a cfad-extension ofF. On the other hand, the conflict-free s{e,t , } is not acfad-extension, because there is the admissible s{eℎt} in the reducFt { , , }.
Of particular interest to us, is the fact that the preferred semantics can be characterised as a vacuous reduct semantics, as shown b1y4,[23].
Proposition 2. For any AF F = (A, R). It holds that
PR(F) = adad(F) = COCO(F).
We will utilise this in our algorithm for skeptical preferred reasoning to verify whether some complete extension is preferred by checking whether the redFuctis CO-vacuous.
Constructing the Counterexample In the course of executing the algorithm we construct diferent complete extensions in diferent restrictions and reducts of the original argumentation framework. What allows us to combine them to construct a proper counterexample for skeptical acceptance is the concept ofModularisation of argumentation semantics introduced by Baumann2e4t].al. [ Principle 2. Let be a semantics. We say thatsatisfies Modularisation if and only if for all argumentation frameworkFsit holds that, i1f ∈ ( F) and 2 ∈ ( F 1) then 1 ∪ 2 ∈ ( F).
As shown by Baumann et a[l2.4], Modularisation is satisfied by both complete and preferred semantics. Proposition 3. Complete and preferred semantics satisfy Modularisatio.n
This concept will prove useful for our algorithm and allows us to combine partial results into a proper counterexample for skeptical acceptance.
Example 6. Consider again the argumentation framewFodrekpicted in Figur1e. We have the complete extensio{n} and in the reducFt{ }, there is for instance the complete exten{s,io}nand, as already seen in Exampl1e, the union{ } ∪ { , } is a complete extension Fof. Notably, this combined set then also serves as a counterexample for skeptical acceptance of the arignuFm.ent
Our algorithm for skeptical preferred reasoning, like most state-of-the-art approaches, utilises a reduction toSat. In the following, we will briefly describe tShaet-encoding used for computing complete extensions. The encodings are built on stanSdaatr-dencodings for AFs6[, 25], used in similar fashion by many argumentation solve8r,s1[3].
LetF = (A, R) be an argumentation framework. Let us first introduce basic notion. We consider propositional logic and we model the acceptance (rejection) of an arg∈uAmewnrtt. to some extension ⊆ A with the propositional variaibnl e(out ). We will then define formulae over these atoms with the usual connective¬s,: ∧, ∨. Let ∶ { in } ∈A ∪ {out } ∈A ↦ {True, False} be some interpretation over the arguments Fof representing some extensio⊆n A. Then, if in is True in , then ∈ , otherwis e ∉ . Analogously, iofut is True in , then ∈ + , otherwis e ∉ + .
F F
Our encoding for complete semantics then consists of the following components. (E3q)umaotdioelns basic conditions for acceptance: an argument cannot be accepted and rejected at the same time, if an attack erof is accepted, thenis rejected and ifis rejected, then one of its attackers must be accepted. Recall that a complete extension is conflict-free, defends all its members and includes all
arguments that it defends. Conflict-Freeness is modelleΨd biyn Equation(
∈A ∈ −F ∈ −F ΨF = ΨF ∧ ⋀ ⋀ ¬in ∨ ¬in
∈A ∈ −F ΨF = Ψ ∧ ⋀
F
⋀ ¬in ∨ out ∈A ∈ −F ΨCFO = ΨF ∧ ⋀∈A (in ∨ ⋁∈−F ¬out ) As has been shown in6[], every model oΨfCO corresponds to a complete extensioFn.oIfn particular,
F for some argumentation framewFor=k (A, R) and a model of ΨCO we define the corresponding F complete extensio n of F as follows:
Beyond that, we also utilise the following clause inSeavte-crayll which ensures that the computed complete extension is non-empty.
= { ∈ A ∣ ( in ) = True} ΨF = ⋁ in
∈A CF () =
⋁ in ∈A∖
First, we introduce some notatiGonro.unded(F) denotes the iterative algorithm computing the grounded extension of Dun[3g]. We writeSat(Ψ)for a call to tShaet-solver that returTnrsue if Ψ is satisfiable andFalse otherwise. Furthermore, we wrWitietness(Ψ)for a call to tShaet-solver that returns the se t for some model of Ψ, if Ψ is satisfiable, otherwise it returFnaslse. We also utilise a complement clausCeF () defined as for some set of argument⊆s A. This clause, for each found complete extensi,oensures not only that thSeat-solver does not find as a solution again, but also tha t ′anwyith ′ ⊆ is no valid witness in any followinSgat-call.
Our novel algorithm for deciding skeptical acceptance wrt. preferred semantics is shown in
Algorithm1. For the inputF = (A, R)and some ∈ A, the algorithm returYnes if is skeptically accepted
wrt. preferred semanticsFi n,otherwise it returns a complete exte nsoiofnF that serves as a witness
for the non-acceptance o. fIn detail, the procedure of our algorithm works as follows:
(
c) Otherwise, add a complement clause ∪fo r ′ and continue wit(h2)(lines 22-25).
Input: F = (A, R), ∈ A Output: ⊆ A, otherwiseYes 1: F ← F |RelF( ) 2: GR ← Grounded(F ) 3: if ∈ GR then 4: return Yes 5: if ∈ G+R,F then 6: return GR
As the following result shows, our algorithm is indeed sound and complete. For so(mF e, i)n, pitut returnsYes if and only if the query argume nits skeptically accepted wrt. preferred semantFic.s in The full proof of Theore m1can be found in the extended version of this pa2p6e]r, a[vailable onli3n.e Theorem 1. Algorithm 1 is sound and complete for the problem DS-PR.
Note that the algorithm is still sound and complete if we use the eΨnacdofdoirnagdmissibility F instead of the encoding for complete semantics. This follows easily via Pro2p4o.sition 3https://doi.org/10.5281/zenodo.16022972 4Early experiments showed however that usΨinCOg is slightly faster in practice, see a2l5s]ofo[r a detailed performance
F analysis of diferent types of semantical encodings.
In case the query argumentis not skeptically accepted wrt. preferred semantics, the algorithm
returns a witness that serves as a counterexample for the non-acce p t.aAnscaelorfeady mentioned
before, this output is not necessarily a preferred extension that does not contai n.tIhnestqeuaedr,y
Algorithm1 returns three diferent types of witnesses, depending on the situation:
(
Importantly, as follows from the proof of Theo1r,etmhe witness produced by Algorit1hmis in any case suficient to prove that the query is not skeptically accepted wrt. preferred semantics. Corollary 2. Let F = (A, R) be an argumentation framework and ∈ A and ∉ ⋂∈ PR(F) . Let ⊆ A be the output of Algorithm 1 for the input F = (A, R), ∈ A. Then, there exists a preferred extension ∈ PR(F ) with ⊂ and ∉ .
The following section will show the feasibility of our approach in practice and that it significantly outperforms state-of-the-art approaches in most cases.
To evaluate the performance of our novel algorithm for skeptical preferred reasoning, we conducted an evaluation and compared its runtime to that of current state-of-the-art argumentation solvers. In th following, we will briefly describe the implementation of our algorithm as well as the experimental setup. Finally, we will present the results of the evaluation and provide an ablationSsattu-dsoylwverrts..
We implemented Algorith1min C++ as part of an argumentation solver which we craeldluecdto. For all calls of the foSramt(⋅),Witness(⋅)reducto uses theSat-solverCaDiCal 2.1.3 [27]. The computation oFf |RelF ( ) and the functioGnrounded(F ) are implemented directly in C++ via simple iterative procedures. The implementation is open source and available o5n. GitHub
For the evaluation of our algorithm, we consider the benchmark datasIenttesronfattihoenal Competition on Computational Models of Argumentation (ICCMA). We consider the decision probleDmS-PR and make use of the appropriate datasets from all competitioInCsC,iM.eA.,’15 toICCMA’23 [28, 29, 30, 13].
Table1 summarises some key statistics for the considered benchmark sets. Note ItChCaMt Ath’2e1 dataset is comprised of particularly large instances compared to all other benchmark sets.
To evaluate the performance of our algorithm for skeptical preferred reasoning, we consider the runtime per instance and compare it to that of current state-of-the-art argumentation solvers. Beside ou solverreducto (version 2.13), we consider all competitors from the IlCaCteMsAt’23 for the evaluation: -toksia [8]: written inC++, uses an iterativSeat-basedCEGAR approach [7]. Available are two versions, one withGlucose [31] and one withCryptoMiniSat [32] as theSat-solver.
Fudge [9]: written inC++, Sat-based approach witChaDiCal [27] as theSat-solver that solves the problem by computing admissible sets attacking admissible sets that contain the query argument. Crustabri [33]: written in Rust, iteratSiavte-based approach witChaDiCal [27] as theSat-solver. PORTSAT [34]: written in Rust, enumerates preferred extensions with the help of a portfolio of diferent Sat-solvers.
The experimental evaluation has been conducted witphrotbho2e benchmarking suite for argumentation solvers3[5]. All experiments where executed on a machine running Ub2u0n.0t4uwith an Intel Xeon E53.4 GHz CPU and192 GB of RAM. We used a per-instance time-out12o0f0 seconds.
The results of our experiments are summarised in T2a.bFloer each benchmark set, we also consider thevirtual best solver (VBS), which is computed by taking the best runtime for each instance from all competing solvers. Solvers are ranked in increasing order according to the number of unsolved instances and in case of ties by total runtime.
In generalr, educto solves the most instances out of all the considered solversICfoCrMtAh’e15, ICCMA’17, ICCMA’19 andICCMA’23 benchmark sets. On all of these datarseedtuscto also has the best PAR2 score and contributes the most instances to the VBS, i. e., it has the fastest runtime of any solver on the most instances. The total runtime is also generally the lowesICt,CoMnAly’1f7oris it higher than that o-ftoksia (Glucose) andCrustabri.
This is simply due to the fact thraetducto solves significantly more instances of the dataset. Especially on the easier benchmark sIeCtCsMA’15 andICCMA’19, where most solvers are able to solve all instances, the total runtime and PAR2 srceodruecotfo is significantly lower than that of all competitors.
Only on theICCMA’21 dataset ,-toksia (Glucose) solves more instances thraenducto and is also faster on almost all instances.ICTCheMA’21 dataset generally consists of only very large instances, compared to the other benchmark sets (cf. T1a)b.lIen addition to that, for all of the instances the simplification steps employed by our approach are not applicable, i. e., the AFs have the empty set as the grounded extension and all arguments in the AF are relevant for the query argument. We presume this is the reason for the worse performancreeodfucto, in combination with a less eficienStat-encoding compared t o-toksia. Notably, all other solvers, apart fr-toomksia (Glucose), includin g -toksia (CMSat), still perform significantly worse thraenducto on theICCMA’21 dataset.
Let us take a closer look at the most rIeCcCenMtA’23 dataset. The simplification steps outlined in Section3.1 allow us to reduce the s|iAze| of an instance b5y8.2% on average. More specifically, restricting the AF to the arguments relevant for the query removes on38a.2v%eroafgtehe arguments, and “resolving” the grounded extension removes an3o1t.h7%erof the remaining arguments. Figu3are visualises the performance of each solver onICtChMeA’23 dataset. In particular, it shows the number of solved instances of each solver given the per-instance runtime. As one rceadnusceteo, performs significantly better than all other solvers on this dataset. Moreove3rb, gFivgeusrae direct comparison of reducto and -toksia (Glucose), the two best ranked solvers, onItChCeMA’23 dataset. Markers above the diagonal line are instances wrheedruecto is faster and below-toksia is faster. As we can see, the performance of both solvers is within one order of magnitude of each other for the majority of (c) Results forICCMA’19 (326 instances).
(d) Results forICCMA’17 (350 instances).
PAR2 #VBS
Solver
RT
PAR2 #VBS instances. However,educto is clearly faster for almost all instances. That is also consistent with the fact tharteducto contributes the most instances to the VBS for all datasetI CsCexMcAep’2t1.
To evaluate the impact of the utilSiasetd-solver we conducted a small ablation study oICnCtMheA’23 benchmark set. BesideCsaDiCal 2.1.3 [27], we also considered thSeat-solversGlucose 4.2.1 [31], CryptoMiniSat (CMSat) 5.11.21 [32] andMergeSat 4.0 [36]. In Table3 we summarise the results forreducto based on the diferentSat-solvers on thIeCCMA’23 dataset. As we can seCe,aDiCal significantly outperforms the othSeart-solvers. While thCeMSat andMergeSat versions ofreducto perform quite similarly, tGhleucose version clearly performs worse than the others. This is in contrast to -toksia, whereGlucose performs clearly better tChaMnSat on all benchmarks. Interestingly, all versions contribute a significant amount of instances to the VBS, hoCwaeDvieCral contributes the most. It should also be noted that all versiroendsuocfto are faster than all other solvers, cf. 2Taa.ble
The problem of skeptical reasoning wrt. preferred semantics is a focal point of argumentation research, and there exist many diferent approaches in the literature to tackle it. Like our approach, many of them are based onCEGAR [17]. The -toksia solver 8[] uses the same approach as CEGARTIX7][, without shortcuts. Given an argumentation framFewaonrdk some argumen t, it searches for a complete extensio nof F that does not conta.inIt then iteratively maxim isetso try and obtain a preferred extensio n′ with ′ ⊇ and ∉ ′. If no such ′ exists, a complement clause is added to theSat-encoding and the search for complete extensions withcountinues. Simplifications are not applied in the latest version.
While our approach is fairly similar, there are some important diferences. First of all, we employ simplifications, as outlined in Secti3o.1n. We also utilise shortcuts by checking whether the query argumen t is attacked by some found non-empty complete exte ns,isoinmilar to CEGARTIX. We also additionally use a clause to ensure non-emptiness, which is not used in other approaches. However, the key diference is that for each found complete extensi,owne only check once whether there is a larger complete extension (by searching for a non-empty complete extension in theFre).dMucetaning, we efectively search through diferent complete extensions that each contain at least one never before visited argument, instead of trying to maximise each one. Thus, we narrow down the search field with each iteration but grant more freedom for the complete extensions to be computed.
A quite diferent approach is employed by thFuedge solver 9[]. It uses a conflict-driven approach and directly searches for admissible sets that attack admissible set that contain the query argument As already mentioned before, this is diferent to our approach, since we do not actively search for acceptable sets that attack the query, but rather check if that is the case during the search.
In this work, we considered the problem of skeptical reasoning wrt. preferred semantics, i. e., deciding whether every preferred extension of an argumentation framework contains some specific argument. We introduced a novel algorithm that first simplifies the problem instance and subsequently searches through non-empty complete extensions of the simplified argumentation framework. Instead of maximising these extensions, our approach checks whether they directly attack the query argument and continues searching for extensions that contain unvisited arguments. We implemented this approach in the solverreducto. As our experimental results show, the combination of these simplifications and the search procedure allowresducto to outperform current state-of-the-art solvers on most benchmarks.
Regarding future work, we intent to further refine the undeSralyti-nengcoding, cf. the work of [25]. Furthermore, the simplification steps ofer an interesting point for further research. First of all, there are other possibilities for more sophisticated preproc1e9s]sitnhgat[ could be of use. Moreover, preprocessing is not used at all by many of the existing solvers and thus it would be interesting to study its efectiveness in the context of the other algorithms for skeptical preferred reasoning.
The research reported here was partially supported by the Deutsche Forschungsgemeinschaft (grant 550735820).
[16] P. Baroni, D. Gabbay, M. Giacomin, L. van der Torre (Eds.), Handbook of Formal Argumentation,
College Publications, 2018. [17] E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, H. Veith, Counterexample-guided abstraction refinement for symbolic model checking, J. ACM 50 (2003) 752–794. [18] A. Biere, M. Järvisalo, B. Kiesl, Preprocessing in SAT solving, in: A. Biere, M. Heule, H. van Maaren, T. Walsh (Eds.), Handbook of Satisfiability - Second Edition, volume 3F3ro6notifers in Artificial Intelligence and Applications , IOS Press, 2021, pp. 391–435. [19] W. Dvorák, M. Järvisalo, T. Linsbichler, A. Niskanen, S. Woltran, Preprocessing argumentation frameworks via replacement patterns, in: Logics in Artificial Intelligence - 16th European Conference, JELIA 2019, Proceedings, volume 11468LoNfCS, Springer, 2019, pp. 116–132. [20] P. Baroni, M. Giacomin, On principle-based evaluation of extension-based argumentation semantics, Artificial Intelligence 171 (2007) 675–700. [21] A. Borg, F. Bex, Minimality, necessity and suficiency for argumentation and explanation, Int. J.
Approx. Reason. 168 (2024) 109143. [22] R. Baumann, G. Brewka, M. Ulbricht, Revisiting the foundations of abstract argumentation semantics based on weak admissibility and weak defense, in: The Thirty-Fourth AAAI Conference on Artificial Intelligence, AAAI 2020, AAAI Press, 2020, pp. 2742–2749. [23] L. Blümel, M. Thimm, Revisiting vacuous reduct semantics for abstract argumentation, in: ECAI 2024 - 27th European Conference on Artificial Intelligence, IOS Press, 2024, pp. 3517–3524. [24] R. Baumann, G. Brewka, M. Ulbricht, Shedding new light on the foundations of abstract argumentation: Modularization and weak admissibility, Artificial Intelligence 310 (2022) 103742. [25] F. Cerutti, M. Giacomin, M. Vallati, How we designed winning algorithms for abstract argumentation and which insight we attained, Artificial Intelligence 276 (2019) 1–40. [26] L. Bengel, J. Sander, M. Thimm, A Reduct-based Approach to Skeptical Preferred Reasoning in
Abstract Argumentation (Extended Version), Zenodo, 2025. [27] A. Biere, T. Faller, K. Fazekas, M. Fleury, N. Froleyks, F. Pollitt, Cadical 2.0, in: A. Gurfinkel, V. Ganesh (Eds.), Computer Aided Verification - 36th International Conference, CAV 2024, volume 14681 of Lecture Notes in Computer Science, Springer, 2024, pp. 133–152. [28] M. Thimm, S. Villata, The first international competition on computational models of argumentation: Results and analysis, Artificial Intelligence 252 (2017) 267–294. [29] S. A. Gaggl, T. Linsbichler, M. Maratea, S. Woltran, Design and results of the second international competition on computational models of argumentation, Artificial Intelligence 279 (2020). [30] S. Bistarelli, L. Kotthof, J.-M. Lagniez, E. Lonca, J.-G. Mailly, J. Rossit, F. Santini, C. Taticchi, The third and fourth international competitions on computational models of argumentation: Design, results and analysis, Argument & Computation 0 (2024) 1–73. [31] G. Audemard, L. Simon, On the glucose SAT solver, Int. J. Artif. Intell. Tools 27 (2018) 1840001:1–1840001:25. [32] M. Soos, K. Nohl, C. Castelluccia, Extending SAT solvers to cryptographic problems, in: Theory and Applications of Satisfiability Testing - SAT 2009, 12th International Conference, SAT 2009, Proceedings, volume 5584 oLfecture Notes in Computer Science, Springer, 2009, pp. 244–257. [33] J. Lagniez, E. Lonca, J. Mailly, A sat-based approach for argumentation dynamics, in: Proceedings of the 23rd International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2024, ACM, 2024, pp. 2351–2353. [34] S. Declercq, Q. J. Capellini, C. Yang, J. Delobelle, J.-G. Mailly, Portsat: A portfolio of sat solvers for abstract argumentation, ICCMA 2023 (2023) 32. [35] J. Klein, M. Thimm, probo2: A benchmark framework for argumentation solvers, in: Computational Models of Argument - Proceedings of COMMA 2022, volume 35F3roonftiers in Artificial Intelligence and Applications, IOS Press, 2022, pp. 363–364. [36] N. Manthey, The mergesat solver, in: Theory and Applications of Satisfiability Testing - SAT 2021 - 24th International Conference, Proceedings, volume 12L8N31CoS,f Springer, 2021, pp. 387–398.