=Paper=
{{Paper
|id=Vol-2672/paper_7
|storemode=property
|title=On the Impact of SAT Solvers on Argumentation Solvers
|pdfUrl=https://ceur-ws.org/Vol-2672/paper_7.pdf
|volume=Vol-2672
|authors=Serigne Gning,Jean-Guy Mailly
|dblpUrl=https://dblp.org/rec/conf/comma/GningM20
}}
==On the Impact of SAT Solvers on Argumentation Solvers==
https://ceur-ws.org/Vol-2672/paper_7.pdf
68 Gning and Mailly / On the Impact of SAT Solvers on Argumentation Solvers
On the Impact of SAT Solvers on
Argumentation Solvers
Serigne GNING a Jean-Guy MAILLY b
a
Université de Paris
gning00@gmail.com
b
LIPADE, Université de Paris
jean-guy.mailly@u-paris.fr
Abstract. SAT-based approaches for reasoning with abstract argumen-
tation frameworks (AFs) have been dominating in recent years. Dif-
ferent SAT solvers have been used in the argumentation solvers that
performed well at the different occurrences of the International Com-
petition on Computational Models of Argumentation (ICCMA). Based
on this observation, the question of the impact of the underlying SAT
solver on the efficiency of the argumentation solver has arisen. We have
conducted a preliminary study that shows varied results when the SAT
solvers Minisat and Glucose are used. Our results suggest interesting
research tracks, like the study of the link between the AF instances and
the SAT solving algorithms, or the use of a portfolio of SAT solvers for
reasoning with AFs.
Keywords. Abstract argumentation, SAT solvers
1. Introduction
Abstract argumentation frameworks [1] are one of the most prominent models in
the domain of computational argumentation. The development of efficient com-
putational approaches has blown up in recent years, especially in relation with
the organisation of the International Competition on Computational Models of
Argumentation (ICCMA) since 2015 [2,3,4]. One of the general results of the
successive editions of ICCMA is the global domination of solvers based on SAT:
• CoQuiAAS [5], ArgSemSAT [6], LabSATSolver1 and Cegartix [7] in 2015;
• pyglaf [8], ArgSemSAT, argmat-sat,2 CoQuiAAS and argmat-dvisat 3 in
2017;
• µ-toksia [9], CoQuiAAS and pyglaf in 2019.
Moreover, SAT-based approaches have also been used for other purposes, like
extension enforcement [10], status enforcement [11], or reasoning with incomplete
Copyright c 2020 for this paper by its authors. Use permitted under Creative Commons
License Attribution 4.0 International (CC BY 4.0).
1 https://github.com/fbrns/LabSATSolver
2 https://sites.google.com/site/argumatrix/argmat-sat
3 https://sites.google.com/site/argumatrix/argmat-dvisat
Gning and Mailly / On the Impact of SAT Solvers on Argumentation Solvers 69
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 efficiency of the argumentation solver?”. To answer this question, we have
conducted a preliminary study where we compare the original CoQuiAAS solver
with a modified 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 efficiency 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 efficiency of the
solvers highly depends on the instance. There are also some instances that are not
solved by one solver within the specified 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 efficiently different instances of AF-
based 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 ∈ A, we say
that a attacks b if (a, b) ∈ R. Moreover, a set S ⊆ A defends an argument c ∈ A
if, ∀b ∈ A s.t. (b, c) ∈ R, ∃a ∈ S s.t. (a, b) ∈ R. Different notions of collective
acceptance of arguments are defined 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 conflict-free iff ∀a, b ∈ S, (a, b) 6∈ R; and S ⊆ A is admissible iff
S is conflict-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 ∈ ST (F )) iff S is conflict-free and
∀b ∈ A \ S, ∃a ∈ S s.t. (a, b) ∈ R;
• S ⊆ A is a complete extension (denoted S ∈ CO(F )) iff S is admissible
and ∀a ∈ A that is defended by S, a ∈ S.
We are interested in four classical reasoning problems.
70 Gning and Mailly / On the Impact of SAT Solvers on Argumentation Solvers
SE-σ Given F = hA, Ri, give some S ∈ σ(F ).
EE-σ Given F = hA, Ri, give each S ∈ σ(F ).
DC-σ Given F = hA, Ri and a ∈ A, is there S ∈ σ(F ) s.t. a ∈ S?
DS-σ Given F = hA, Ri and a ∈ A, is a ∈ S true for each S ∈ σ(F )?
We recall that reasoning with AFs is generally intractable, in particular, DC-
ST 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 proposi-
tional variables in formulas such that a set of arguments is an extension iff it is a
model of the formula. More precisely, given F = hA, Ri an AF, we define
V V
• φST = a∈A (a ↔ (b,a)∈R ¬b)
V V V W
• φCO = a∈A ((a → (b,a)∈R ¬b) ∧ (a ↔ (b,a)∈R ( (c,b)∈R c)))
where the models of φσ exactly correspond to the σ-extensions of F , for σ ∈
{ST, CO}. Then, solving the problem SE-σ (resp. EE-σ) corresponds to comput-
ing one model (resp. all the models) of φσ , while DC-σ (resp. DS-σ) is solved by
checking whether φσ ∧ a is satisfiable (resp. φσ ∧ ¬a is unsatisfiable), where a is
the queried argument for acceptance.
3. Experiments
We have used two versions of CoQuiAAS: the original version, where the under-
lying SAT solver is Minisat, and a modified version where Minisat is replaced
by Glucose. For comparing their relative efficiency, we have used the benchmark
from ICCMA 2017, since they were specifically chosen for the specific 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 first 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 significant difference between
both solvers. For all the other pairs (task, semantics), either both versions of the
solvers are very efficient, or both face a high number of timeout (thus, the PAR10
score is around several thousands).
Stable Semantics Complete Semantics
EE SE DS DC EE SE DS DC
CoQuiAAS + Minisat 3875.6 1.19 6.38 1.36 4854.52 375.06 1.46 1.52
CoQuiAAS + Glucose 3916.46 2175 6.39 0.48 4892.19 375.82 1.46 0.63
Table 1. PAR10 score for both versions of CoQuiAAS, rounded to 10−2 seconds
Gning and Mailly / On the Impact of SAT Solvers on Argumentation Solvers 71
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 subfigure, one point
corresponds to one instance, where its abscissa is the runtime obtained by Co-
QuiAAS 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 significant 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 efficiency 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 fixed 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 differences 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 specific SAT solver, we can run in parallel several ones,
and stop as soon as one of them finds the solution. This would allow to benefit
from the power of the different SAT solving algorithms at once. Another option to
optimize the use of SAT solvers consists in fine-tuning the solvers. This requires a
deep analysis of how the solver’s performance is affected by the type of AF for the
different configurations of solvers parameters. Finally, different SAT encodings of
the AF and semantics may have some effects on the SAT solvers runtime.
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 first international competition on computational models of
argumentation: Results and analysis. Artif Intell. 2017;252:267–294.
72 Gning and Mailly / On the Impact of SAT Solvers on Argumentation Solvers
(a) DS-ST
(b) DC-ST
Figure 1. Solvers runtime for the stable semantics: Minisat in abscissa; Glucose in ordinate
[3] Gaggl SA, Linsbichler T, Maratea M, Woltran S. Design and results of the Second Inter-
national Competition on Computational Models of Argumentation. Artif Intell. 2020;279.
[4] Bistarelli S, Kotthoff 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 Argu-
mentation 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] Dvorák W, Järvisalo 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, Järvisalo M. µ-toksia: An Efficient Abstract Argumentation Reasoner. In:
Proc. of KR 2020; 2020. To appear.
[10] Wallner JP, Niskanen A, Järvisalo M. Complexity Results and Algorithms for Extension
Enforcement in Abstract Argumentation. J Artif Intell Res. 2017;60:1–40.
[11] Niskanen A, Wallner JP, Järvisalo M. Optimal Status Enforcement in Abstract Argumen-
tation. In: Proc. of IJCAI 2016; 2016. p. 1216–1222.
Gning and Mailly / On the Impact of SAT Solvers on Argumentation Solvers 73
(a) EE-CO
(b) DC-CO
Figure 2. Solvers runtime for the complete semantics: Minisat in abscissa; Glucose in ordinate
[12] Niskanen A, Neugebauer D, Järvisalo 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, Järvisalo M. Controllability of Control Argumentation Frame-
works. 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] Eén N, Sörensson N. An Extensible SAT-solver. In: Proc. of SAT 2003; 2003. p. 502–518.
[17] Dvorák 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.