On the Impact of SAT Solvers on Argumentation Solvers

Keywords

• Abstract argumentation SAT solvers

1. Introduction

argumentation frameworks [ 12 ] and control argumentation frameworks [ 13,14 ]. The question that arises now is \does the choice of the SAT solver have an impact on the e ciency of the argumentation solver?". To answer this question, we have conducted a preliminary study where we compare the original CoQuiAAS solver with a modi ed version based on Glucose [ 15 ] instead of Minisat [ 16 ]. This choice comes from the fact that CoQuiAAS (using Minisat) was the second best solver at the last ICCMA competition, while the winner -toksia was based on Glucose. We have compared the e ciency of both versions of CoQuiAAS on the four classical reasoning tasks for the stable and complete semantics: given an AF, produce one extension or enumerate all the extensions; given an AF and an argument, check credulous acceptance and skeptical acceptance for this argument. Depending on the pair (task, semantics), we observe various results, that actually yield new open questions. While, in some cases, both versions of the solver are globally equivalent for most instances, in some other cases the relative e ciency of the solvers highly depends on the instance. There are also some instances that are not solved by one solver within the speci ed timeout, while they are quickly solved by the other solver. This suggests that there may be a link between the properties of the instances (e.g. the type of graph structure) and the best suited SAT solver. Thus, an interesting approach for solving e ciently di erent instances of AFbased reasoning may rely on a portfolio of SAT solvers.

In Section 2, we recall the basic notions of abstract argumentation, and the translations of AF semantics into propositional logic that are used by the solvers. Then, Section 3 describes our experimental protocol and results. Finally, Section 4 concludes the paper by highlighting some interesting research tracks that emerge from our experiments.

2. Background Notions

2.1. Abstract Argumentation

An argumentation framework (AF) [ 1 ] is a directed graph F = hA; Ri where A is the set of arguments, and R A A is the attack relation. For a; b 2 A, we say that a attacks b if (a; b) 2 R. Moreover, a set S A defends an argument c 2 A if, 8b 2 A s.t. (b; c) 2 R, 9a 2 S s.t. (a; b) 2 R. Di erent notions of collective acceptance of arguments are de ned by Dung, based on the notion of extension, i.e. some set of arguments that are jointly acceptable. An extension semantics is a function that maps an AF to its set of extensions. Most semantics rely on basic notions: S A is con ict-free i 8a; b 2 S, (a; b) 62 R; and S A is admissible i S is con ict-free and S defends all its elements.

We introduce the extension semantics that are used in this work.

S A is a stable extension (denoted S 2 ST (F )) i S is con ict-free and 8b 2 A n S, 9a 2 S s.t. (a; b) 2 R; S A is a complete extension (denoted S 2 CO(F )) i S is admissible and 8a 2 A that is defended by S, a 2 S.

We are interested in four classical reasoning problems. SEEEDCDSGiven F = hA; Ri, give some S 2 (F ).

Given F = hA; Ri, give each S 2 (F ).

Given F = hA; Ri and a 2 A, is there S 2 (F ) s.t. a 2 S?

Given F = hA; Ri and a 2 A, is a 2 S true for each S 2 (F )?

We recall that reasoning with AFs is generally intractable, in particular, DCST and DC-CO are NP-complete, and DS-ST is coNP-complete [ 17 ]. This explains the popularity of SAT-based approaches for reasoning with AFs.

2.2. Propositional Encoding

Now, we give the propositional encodings of the stable and complete semantics that are used in SAT-based argumentation solvers, especially in CoQuiAAS [ 5 ]. These encodings come from [ 18 ]. The idea is to use argument names as propositional variables in formulas such that a set of arguments is an extension i it is a model of the formula. More precisely, given F = hA; Ri an AF, we de ne SCTO == VVaa22AA((a(a$!VV(b(;ba;)a2)2RR::b)b) ^ (a $ V (b;a)2R(W(c;b)2R c))) where the models of exactly correspond to the -extensions of F , for 2 fST; COg. Then, solving the problem SE- (resp. EE- ) corresponds to computing one model (resp. all the models) of , while DC- (resp. DS- ) is solved by checking whether ^ a is satis able (resp. ^ :a is unsatis able), where a is the queried argument for acceptance.

3. Experiments

We have used two versions of CoQuiAAS: the original version, where the underlying SAT solver is Minisat, and a modi ed version where Minisat is replaced by Glucose. For comparing their relative e ciency, we have used the benchmark from ICCMA 2017, since they were speci cally chosen for the speci c semantics and reasoning tasks at hand [ 3 ]. The timeout was set to 600 seconds, and the experiments were run on Ubuntu 18.04, with a 2.16GHz CPU and 4GB of RAM.

We have rst computed the Penalized Average Runtime (PAR10), i.e. for each reasoning task, the solvers are associated with the average runtime for all the instances, where a timeout is penalized as ten times the actual timeout. As shown on Table 1, except for SE-ST, there is no signi cant di erence between both solvers. For all the other pairs (task, semantics), either both versions of the solvers are very e cient, or both face a high number of timeout (thus, the PAR10 score is around several thousands).

But then, we look at the results in more detail. We have compared the results of both solvers for each instance. Figures 1 and 2 present parts of the results, for the stable and complete semantics respectively. In each sub gure, one point corresponds to one instance, where its abscissa is the runtime obtained by CoQuiAAS with Minisat, and the ordinate is the runtime obtained by CoQuiAAS with Glucose. Some pairs (task, semantics) are omitted for space reason.

We start with the stable semantics. For DS-ST (Figure 1a), we observe that some instances are close to an axis, which means that the runtime is almost 0 for one of the solvers, but around several dozens (or even hundreds) of seconds for the other one. This is even more signi cant for DC-ST (Figure 1b), where almost all the instances are in this situation. This means that, some instances are hard to solve with Minisat, and easy to solve with Glucose, while some other instances are in the opposite situation. We observe again the same result for the complete semantics, see e.g. DC-CO at Figure 2b. A particularly interesting phenomenon concerns EE-CO (Figure 2a): many instances are solved by Minisat while reaching timeout with Glucose, and vice-versa.

4. Conclusion

This paper presents a preliminary study of the impact of the underlying SAT solver on the e ciency of argumentation solvers. Although we wish to extend this work, with the inclusion of other SAT solvers, the existing results already suggest some interesting research tracks. Indeed, we have observed that, depending on the use of Minisat or Glucose (i.e. the SAT solvers that were the most successful at ICCMA 2019), some instances may be really hard to solve (even sometimes impossible to solve within the xed time limit), or on the contrary very quick. None of the solvers has really dominated the other one. A similar study has been conducted recently [ 19 ] and draws the same conclusion. Future work includes a more detailled study of the di erences between the instances that are easy to solve for one solver, and hard for the other one. Properties like e.g. the presence of cycles or self-attacks, or the density of attacks, may play a role in the choice of the SAT solver. Another interesting idea is to use a portfolio of SAT solvers [ 20 ]: instead of using a speci c SAT solver, we can run in parallel several ones, and stop as soon as one of them nds the solution. This would allow to bene t from the power of the di erent SAT solving algorithms at once. Another option to optimize the use of SAT solvers consists in ne-tuning the solvers. This requires a deep analysis of how the solver's performance is a ected by the type of AF for the di erent con gurations of solvers parameters. Finally, di erent SAT encodings of the AF and semantics may have some e ects on the SAT solvers runtime. (b) DC-ST

References

[1] Dung PM . On the Acceptability of Arguments and its Fundamental Role in Nonmonotonic Reasoning, Logic Programming and n-Person Games . Artif Intell . 1995 ; 77 ( 2 ): 321 { 358 .

[2] Thimm M , Villata S. The rst international competition on computational models of argumentation: Results and analysis . Artif Intell . 2017 ; 252 : 267 { 294 .

[3] Gaggl SA , Linsbichler T , Maratea M , Woltran S . Design and results of the Second International Competition on Computational Models of Argumentation . Artif Intell . 2020 ; 279 .

[4] Bistarelli S , Kottho L , Santini F , Taticchi C . Containerisation and Dynamic Frameworks in ICCMA'19 . In: Proc. of SAFA 2018 ; 2018 . p. 4 { 9 .

[5] Lagniez J , Lonca E , Mailly JG . CoQuiAAS: A Constraint-Based Quick Abstract Argumentation Solver . In: Proc. of ICTAI 2015 ; 2015 . p. 928 { 935 .

[6] Cerutti F , Giacomin M , Vallati M. How we designed winning algorithms for abstract argumentation and which insight we attained . Artif Intell . 2019 ; 276 :1{ 40 .

[7] Dvorak W , Jarvisalo M, Wallner JP , Woltran S . Complexity-sensitive decision procedures for abstract argumentation . Artif Intell . 2014 ; 206 : 53 { 78 .

[8] Alviano M. Argumentation Reasoning via Circumscription with Pyglaf . Fundam Inform . 2019 ; 167 ( 1-2 ):1{ 30 .

[9] Niskanen A , Jarvisalo M. -toksia: An E cient Abstract Argumentation Reasoner . In: Proc. of KR 2020 ; 2020 . To appear.

[10] Wallner JP , Niskanen A , Jarvisalo M. Complexity Results and Algorithms for Extension Enforcement in Abstract Argumentation . J Artif Intell Res . 2017 ; 60 :1{ 40 .

[11] Niskanen A , Wallner JP , Jarvisalo M. Optimal Status Enforcement in Abstract Argumentation . In: Proc. of IJCAI 2016 ; 2016 . p. 1216 { 1222 .

[12] Niskanen A , Neugebauer D , Jarvisalo M , Rothe J . Deciding Acceptance in Incomplete Argumentation Frameworks . In: Proc. of AAAI 2020 ; 2020 . .

[13] Dimopoulos Y , Mailly J , Moraitis P. Control Argumentation Frameworks . In: Proc. of AAAI 2018 ; 2018 . p. 4678 { 4685 .

[14] Niskanen A , Neugebauer D , Jarvisalo M. Controllability of Control Argumentation Frameworks . In: Proc. of IJCAI-PRICAI 2020 ; 2020 . .

[15] Audemard G , Simon L . Predicting Learnt Clauses Quality in Modern SAT Solvers . In: Proc. of IJCAI 2009 ; 2009 . p. 399 { 404 .

[16] Een N, Sorensson N. An Extensible SAT-solver . In: Proc. of SAT 2003 ; 2003 . p. 502 { 518 .

[17] Dvorak W , Dunne PE . Computational Problems in Formal Argumentation and their Complexity . In: Baroni P, Gabbay D , Giacomin M , van der Torre L, editors. Handbook of Formal Argumentation . College Publications; 2018 . p. 631 { 688 .

[18] Besnard P , Doutre S. Checking the acceptability of a set of arguments . In: Proc. of NMR 2004 ; 2004 . p. 59 { 64 .

[19] Klein J , Thimm M. Revisiting SAT Techniques for Abstract Argumentation . In: Proc. of COMMA 2020 ; 2020 . To appear.

[20] Balyo T , Sanders P , Sinz C. HordeSat: A Massively Parallel Portfolio SAT Solver . In: Proc. of SAT 2015 ; 2015 . p. 156 { 172 .