{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T07:37:48Z","timestamp":1648539468592},"reference-count":33,"publisher":"Cambridge University Press (CUP)","issue":"4","license":[{"start":{"date-parts":[[2015,12,17]],"date-time":"2015-12-17T00:00:00Z","timestamp":1450310400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theory and Practice of Logic Programming"],"published-print":{"date-parts":[[2016,7]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Answer set programming is a declarative programming paradigm oriented towards difficult combinatorial search problems. A fundamental task in answer set programming is to compute stable models, i.e., solutions of logic programs. Answer set solvers are the programs that perform this task. The problem of deciding whether a disjunctive program has a stable model is \u03a3<jats:sup><jats:italic>P<\/jats:italic><\/jats:sup><jats:sub>2<\/jats:sub>-complete. The high complexity of reasoning within disjunctive logic programming is responsible for few solvers capable of dealing with such programs, namely <jats:sc>dlv<\/jats:sc>, <jats:sc>gnt<\/jats:sc>, <jats:sc>cmodels<\/jats:sc>, <jats:sc>clasp<\/jats:sc> and <jats:sc>wasp<\/jats:sc>. In this paper, we show that transition systems introduced by Nieuwenhuis, Oliveras, and Tinelli to model and analyze satisfiability solvers can be adapted for disjunctive answer set solvers. Transition systems give a unifying perspective and bring clarity in the description and comparison of solvers. They can be effectively used for analyzing, comparing and proving correctness of search algorithms as well as inspiring new ideas in the design of disjunctive answer set solvers. In this light, we introduce a general template, which accounts for major techniques implemented in disjunctive solvers. We then illustrate how this general template captures solvers <jats:sc>dlv<\/jats:sc>, <jats:sc>gnt<\/jats:sc>, and <jats:sc>cmodels<\/jats:sc>. We also show how this framework provides a convenient tool for designing new solving algorithms by means of combinations of techniques employed in different solvers.<\/jats:p>","DOI":"10.1017\/s1471068415000411","type":"journal-article","created":{"date-parts":[[2015,12,17]],"date-time":"2015-12-17T09:59:38Z","timestamp":1450346378000},"page":"465-497","source":"Crossref","is-referenced-by-count":2,"title":["Disjunctive answer set solvers via templates"],"prefix":"10.1017","volume":"16","author":[{"given":"REMI","family":"BROCHENIN","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"MARCO","family":"MARATEA","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"YULIYA","family":"LIERLER","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2015,12,17]]},"reference":[{"key":"S1471068415000411_ref22","unstructured":"Lierler Y. 2010. SAT-Based Answer Set Programming. Ph.D. thesis, University of Texas at Austin."},{"key":"S1471068415000411_ref27","doi-asserted-by":"publisher","DOI":"10.1023\/A:1018930122475"},{"key":"S1471068415000411_ref23","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068410000578"},{"key":"S1471068415000411_ref16","doi-asserted-by":"publisher","DOI":"10.1145\/1119439.1119440"},{"key":"S1471068415000411_ref31","doi-asserted-by":"publisher","DOI":"10.1016\/S0004-3702(02)00187-X"},{"key":"S1471068415000411_ref15","first-page":"37","volume-title":"Proc. of the 21st International Conference on Logic Programming (ICLP 2005)","author":"Giunchiglia","year":"2005"},{"key":"S1471068415000411_ref9","unstructured":"Gebser M. , Kaufmann B. and Schaub T. 2013. Advanced conflict-driven disjunctive answer set solving. In Proc. of the 23rd International Joint Conference on Artificial Intelligence (IJCAI 2013), F. Rossi , Ed. IJCAI\/AAAI."},{"key":"S1471068415000411_ref19","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1997.2630"},{"key":"S1471068415000411_ref29","doi-asserted-by":"publisher","DOI":"10.1007\/s10472-008-9090-9"},{"key":"S1471068415000411_ref18","doi-asserted-by":"publisher","DOI":"10.1145\/1149114.1149117"},{"key":"S1471068415000411_ref21","first-page":"377","volume-title":"Proc. of the 24th International Conference on Logic Programming (ICLP 2008)","author":"Lierler","year":"2008"},{"key":"S1471068415000411_ref12","first-page":"1070","volume-title":"Proc. of the 5th International Conference and Symposium on Logic Programming (ICLP\/SLP 1988)","author":"Gelfond","year":"1988"},{"key":"S1471068415000411_ref8","unstructured":"Faber W. 2002. Enhancing Efficiency and Expressiveness in Answer Set Programming Systems. Ph.D. thesis, Vienna University of Technology."},{"key":"S1471068415000411_ref3","unstructured":"Brochenin R. , Lierler Y. and Maratea M. 2014. Abstract disjunctive answer set solvers. In Proc. of the 21st European Conference on Artificial Intelligence (ECAI 2014). Frontiers in Artificial Intelligence and Applications, vol. 263. IOS, Amsterdam, 165\u2013170."},{"key":"S1471068415000411_ref32","first-page":"305","volume-title":"Proc. of the 1st International Workshop on Practical Aspects of Declarative Languages (PADL 1999)","author":"Soininen","year":"1999"},{"key":"S1471068415000411_ref14","doi-asserted-by":"publisher","DOI":"10.1007\/s10472-009-9113-1"},{"key":"S1471068415000411_ref4","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-007-9082-1"},{"key":"S1471068415000411_ref11","first-page":"15","article-title":"Tableau calculi for logic programs under answer set semantics","volume":"14","author":"Gebser","year":"2013","journal-title":"ACM Transaction on Computational Logic"},{"key":"S1471068415000411_ref25","first-page":"23","volume-title":"Proc. of the 16th International Conference on Logic Programming (ICLP 1999)","author":"Lifschitz","year":"1999"},{"key":"S1471068415000411_ref1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40564-8_6"},{"key":"S1471068415000411_ref6","first-page":"266","volume-title":"Proc. of the 1993 International Logic Programming Symposium (ILPS)","author":"Eiter","year":"1993"},{"key":"S1471068415000411_ref17","doi-asserted-by":"publisher","DOI":"10.1016\/S0004-3702(03)00078-X"},{"key":"S1471068415000411_ref20","doi-asserted-by":"publisher","DOI":"10.1007\/11546207_44"},{"key":"S1471068415000411_ref7","doi-asserted-by":"publisher","DOI":"10.1145\/261124.261126"},{"key":"S1471068415000411_ref30","doi-asserted-by":"publisher","DOI":"10.1017\/S147106841100007X"},{"key":"S1471068415000411_ref33","first-page":"267","volume-title":"Proc. of the 6th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR 2001)","author":"Syrj\u00e4nen","year":"2001"},{"key":"S1471068415000411_ref10","first-page":"11","volume-title":"Proc. of the 22nd International Conference on Logic Programming (ICLP 2006)","author":"Gebser","year":"2006"},{"key":"S1471068415000411_ref5","doi-asserted-by":"publisher","DOI":"10.1145\/368273.368557"},{"key":"S1471068415000411_ref2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511543357"},{"key":"S1471068415000411_ref28","doi-asserted-by":"publisher","DOI":"10.1145\/1217856.1217859"},{"key":"S1471068415000411_ref26","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-60085-2_17"},{"key":"S1471068415000411_ref24","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068411000214"},{"key":"S1471068415000411_ref13","doi-asserted-by":"publisher","DOI":"10.1007\/BF03037169"}],"container-title":["Theory and Practice of Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S1471068415000411","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,19]],"date-time":"2019-04-19T01:54:49Z","timestamp":1555638889000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1471068415000411\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,12,17]]},"references-count":33,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2016,7]]}},"alternative-id":["S1471068415000411"],"URL":"https:\/\/doi.org\/10.1017\/s1471068415000411","relation":{},"ISSN":["1471-0684","1475-3081"],"issn-type":[{"value":"1471-0684","type":"print"},{"value":"1475-3081","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,12,17]]}}}