SAT for Argumentation

1. Introduction

The study of computational models of argumentation is a vibrant research area in artificial intelligence [ 1 ]. Among the proposed computational models of argumentation, considerable progress has been recently made in developing automated reasoning techniques for abstract argumentation frameworks (AFs) [ 2 ]. Various systems have been recently implemented for reasoning over AFs [ 3 ], further incentivized by the ICCMA series of international competitions on computational models of argumentation [ 4,5 ], focusing on AF reasoning tasks such as credulous and skeptical reasoning of the acceptance of arguments, and extension enumeration.

AF reasoning tasks can be represented in a natural way as Boolean combinations of logical constraints via developing propositional (Boolean satisfiability, SAT) encodings [ 6 ]. As witnessed by the results of the ICCMA competitions, SAT-based approaches based on (potentially iterative) invocations of SAT solvers on propositional encodings currently form a central computational approach to reasoning over argumentation frameworks, complementing and being very competitive when compared to specialized algorithms developed for AF reasoning. Indeed, the state-of-the-art SAT solver technology readily available today offers the core NP decision engines employed in many of the current state-of-the-art argumentation reasoning systems focusing on AF reasoning problems [ 7,8,9,10,11,12,13 ].

The use of SAT solvers is not restricted to problem domains in NP. SAT solvers allow for solving hard decision problems presumably well beyond NP via harnessing instantiations of the general SAT-based counterexample-guided abstraction refinement (CEGAR) approach [ 14 ], based on iterative and incremental applications of SAT solvers, solving a sequence of abstractions and ruling out non-solutions through counterexamplebased refinements to the abstraction towards finding one or more solutions to the actual problem instance at hand. As complexity-theoretically very challenging problems are abundant in AF reasoning—various types of decision and optimization problems under different AF semantics exhibiting completeness for different levels of the polynomial hierarchy—developing CEGAR-type SAT-based procedures for AF reasoning tasks is an intuitive choice. Furthermore, there are further connections between AF semantics and iterative SAT procedures; computing the ideal extension essentially corresponds to computing the backbone of the propositional formula encoding the admissible sets of a given AF [ 15,16 ], which gives promise of developing new backbone algorithms particularly suited for argumentation instances [ 17 ].

Going beyond the problems focused on in the ICCMA competitions, SAT-based algorithms have also been developed problems related to AF dynamics, dealing with e.g. adjusting (or revising) a given AF to support new knowledge represented as extensions the AF should support [ 18,19,20 ] or synthesizing a semantically best AF structure to represent a given set of extensions [ 21 ]. The study of AF dynamics gives rise to optimization problems, inviting the employment of Boolean optimization solvers such as maximum satisfiability (MaxSAT) solvers, the optimization counterpart of SAT—relying again heavily on SAT solvers. Furthermore, some AF semantics which yield polynomialtime static reasoning problems turn into NP-hard optimization problems when considering AF dynamics; for example, extension enforcement [ 22,23,24 ] under grounded semantics requires non-trivial SAT encodings [ 25 ].

Beyond abstract argumentation, the SAT-based techniques developed for AF reasoning have been shown to be applicable also for reasoning about acceptance and enumeration of extensions in structured argumentation formalisms. Especially in the context of assumption-based argumentation (ABA) [ 26,27,28 ], a translation-based approach consisting of mapping the structured reasoning task first to the AF level and then employing variants of AF reasoning techniques has recently been shown to provide a complementary approach to native algorithms for ABA reasoning [ 29 ].

The development of SAT-based procedures for AF reasoning, and extensions of AFs such as abstract dialectic frameworks (ADFs) [ 30 ], poses interesting research challenges. Understanding the complexity of AF reasoning tasks with respect to different parameterizations (AF semantics, reasoning modes, and other problem-specific parameters) is essential for understanding what type of SAT-based approaches may be suitable. From encodings and procedures to implementation, the choice of the SAT and MaxSAT solvers can have a noticeable impact on scalability and efficiency. The incremental APIs offered by some of the central SAT solvers also play a key role in implementing CEGAR-style iterative approaches. The use of MaxSAT solvers in CEGAR has been less studied, and poses more challenges, e.g. in terms of incrementality. All in all, developing further understanding on the best-suited ways of employing SAT solvers for reasoning over computational models of argumentation holds great potential for pushing and extending further the current state of the art in computational approaches for argumentation.

Acknowledgements

The author is financially supported by Academy of Finland (grants 276412 and 312662).

References

[1] T. Bench-Capon and P. Dunne , “Argumentation in artificial intelligence,” Artif. Intell., vol. 171 , no. 10 - 15 , pp. 619 - 641 , 2007 .

[2] P. Dung , “ On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games ,” Artif. Intell., vol. 77 , no. 2 , pp. 321 - 358 , 1995 .

[3] G. Charwat , W. Dvora´k, S. A. Gaggl , J. P. Wallner , and S. Woltran , “ Methods for solving reasoning problems in abstract argumentation - A survey,” Artif . Intell., vol. 220 , pp. 28 - 63 , 2015 .

[4] M. Thimm , S. Villata , F. Cerutti , N. Oren , H. Strass , and M. Vallati , “ Summary report of the first international competition on computational models of argumentation,” AI Mag. , vol. 37 , no. 1 , p. 102 , 2016 .

[5] M. Thimm and S. Villata , “ The first international competition on computational models of argumentation: Results and analysis ,” Artif. Intell., vol. 252 , pp. 267 - 294 , 2017 .

[6] P. Besnard and S. Doutre , “ Checking the acceptability of a set of arguments,” in Proc. NMR , pp. 59 - 64 , 2004 .

[7] F. Cerutti , P. E. Dunne , M. Giacomin , and M. Vallati , “ Computing preferred extensions in abstract argumentation: A SAT-based approach ,” in TAFA 2013 Revised Selected Papers , vol. 8306 of LNCS, pp. 176 - 193 , 2014 .

[8] F. Cerutti , M. Giacomin , and M. Vallati , “ ArgSemSAT: Solving argumentation problems using SAT,” in Proc. COMMA , vol. 266 of FAIA, pp. 455 - 456 , 2014 .

[9] W. Dvorˇa´k, M. Ja¨rvisalo , J. Wallner, and S. Woltran , “ Complexity-sensitive decision procedures for abstract argumentation ,” Artif. Intell., vol. 206 , pp. 53 - 78 , 2014 .

[10] J. Lagniez , E. Lonca, and J. Mailly , “ Coquiaas: A constraint-based quick abstract argumentation solver,” in Proc. ICTAI , pp. 928 - 935 , IEEE Computer Society, 2015 .

[11] F. Cerutti , M. Vallati , and M. Giacomin , “ An efficient java-based solver for abstract argumentation frameworks: jargsemsat,” Int. J. Artif . Intell. Tools , vol. 26 , no. 2 , pp. 1 - 26 , 2017 .

[12] M. Alviano , “ The pyglaf argumentation reasoner,” in Technical Communications of ICLP 2017 , vol. 58 of OASICS, pp. 2 : 1 - 2 : 3 , Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik , 2018 .

[13] F. Pu , G. Luo, and Z. Jiang , “ Encoding argumentation semantics by boolean algebra,” IEICE Transactions , vol. 100-D, no. 4 , pp. 838 - 848 , 2017 .

[14] E. M. Clarke , A. Gupta , and O. Strichman , “ SAT-based counterexample-guided abstraction refinement,” IEEE T-CAD , vol. 23 , no. 7 , pp. 1113 - 1123 , 2004 .

[15] P. E. Dunne , W. Dvora´k, and S. Woltran, “ Parametric properties of ideal semantics , ” Artificial Intelligence , vol. 202 , pp. 1 - 28 , 2013 .

[16] J. P. Wallner , G. Weissenbacher, and S. Woltran , “ Advanced SAT techniques for abstract argumentation ,” in Proc. CLIMA , vol. 8143 of LNCS, pp. 138 - 154 , Springer, 2013 .

[17] A. Previti and M. Ja¨rvisalo, “A preference-based approach to backbone computation with application to argumentation,” in Proc. SAC , pp. 896 - 902 , ACM, 2018 .

[18] A. Niskanen , J. Wallner , and M. Ja¨rvisalo, “Optimal status enforcement in abstract argumentation,” in Proc. IJCAI , pp. 1216 - 1222 , AAAI Press, 2016 .

[19] J. P. Wallner , A. Niskanen , and M. Ja¨rvisalo, “Complexity results and algorithms for extension enforcement in abstract argumentation , ” J. Artif. Intell. Res. , vol. 60 , pp. 1 - 40 , 2017 .

[20] T. Lehtonen , A. Niskanen , and M. Ja¨rvisalo, “SAT-based approaches to adjusting, repairing, and computing largest extensions of argumentation frameworks,” in Proc. COMMA , FAIA, IOS Press, 2018 .

[21] A. Niskanen , J. Wallner , and M. Ja¨rvisalo, “Synthesizing argumentation frameworks from examples,” in Proc. ECAI , vol. 285 of FAIA, pp. 551 - 559 , IOS Press, 2016 .

[22] R. Baumann , “ What does it take to enforce an argument? Minimal change in abstract argumentation,” in Proc. ECAI , vol. 242 of FAIA, pp. 127 - 132 , 2012 .

[23] P. Bisquert , C. Cayrol , F. D. de Saint-Cyr, and M. Lagasquie-Schiex , “ Enforcement in argumentation is a kind of update , ” in Proc. SUM , vol. 8078 of LNCS, pp. 30 - 43 , Springer, 2013 .

[24] S. Coste-Marquis , S. Konieczny , J. Mailly , and P. Marquis , “ Extension enforcement in abstract argumentation as an optimization problem,” in Proc. IJCAI , pp. 2876 - 2882 , AAAI Press, 2015 .

[25] A. Niskanen , J. P. Wallner , and M. Ja¨rvisalo, “Extension enforcement under grounded semantics in abstract argumentation,” in Proc. KR , AAAI Press, 2018 .

[26] A. Bondarenko , P. M. Dung , R. A. Kowalski , and F. Toni , “ An abstract, argumentation-theoretic approach to default reasoning,” Artif . Intell., vol. 93 , pp. 63 - 101 , 1997 .

[27] P. M. Dung , R. A. Kowalski , and F. Toni , “ Assumption-based argumentation,” in Argumentation in Artificial Intelligence (I. Rahwan and G. R. Simari , eds.), pp. 25 - 44 , Springer, 2009 .

[28] F. Toni , “ A tutorial on assumption-based argumentation , ” Argument & Computation , vol. 5 , no. 1 , pp. 89 - 117 , 2014 .

[29] T. Lehtonen , J. P. Wallner , and M. Ja¨rvisalo, “From structured to abstract argumentation: Assumptionbased acceptance via AF reasoning,” in Proc. ECSQARU , vol. 10369 of LNCS, pp. 57 - 68 , Springer, 2017 .

[30] T. Linsbichler , M. Maratea , A. Niskanen , J. P. Wallner , and S. Woltran , “ Novel algorithms for abstract dialectical frameworks based on complexity analysis of subclasses and SAT solving,” in Proc. IJCAI , pp. 1905 - 1911 , ijcai.org, 2018 .