{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,11]],"date-time":"2026-01-11T20:34:38Z","timestamp":1768163678480,"version":"3.49.0"},"reference-count":24,"publisher":"Cambridge University Press (CUP)","issue":"4","license":[{"start":{"date-parts":[[2023,7,5]],"date-time":"2023-07-05T00:00:00Z","timestamp":1688515200000},"content-version":"unspecified","delay-in-days":4,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["Theory and Practice of Logic Programming"],"published-print":{"date-parts":[[2023,7]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Answer Set Programming with Quantifiers ASP(Q) extends Answer Set Programming (ASP) to allow for declarative and modular modeling of problems from the entire polynomial hierarchy. The first implementation of ASP(Q), called QASP, was based on a translation to Quantified Boolean Formulae (QBF) with the aim of exploiting the well-developed and mature QBF-solving technology. However, the implementation of the QBF encoding employed in qasp is very general and might produce formulas that are hard to evaluate for existing QBF solvers because of the large number of symbols and subclauses. In this paper, we present a new implementation that builds on the ideas of QASP and features both a more efficient encoding procedure and new optimized encodings of ASP(Q) programs in QBF. The new encodings produce smaller formulas (in terms of the number of quantifiers, variables, and clauses) and result in a more efficient evaluation process. An algorithm selection strategy automatically combines several QBF-solving back-ends to further increase performance. An experimental analysis, conducted on known benchmarks, shows that the new system outperforms QASP.<\/jats:p>","DOI":"10.1017\/s1471068423000121","type":"journal-article","created":{"date-parts":[[2023,7,5]],"date-time":"2023-07-05T04:22:46Z","timestamp":1688530966000},"page":"948-964","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":5,"title":["An Efficient Solver for ASP(Q)"],"prefix":"10.1017","volume":"23","author":[{"given":"WOLFGANG","family":"FABER","sequence":"first","affiliation":[]},{"given":"GIUSEPPE","family":"MAZZOTTA","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8218-3178","authenticated-orcid":false,"given":"FRANCESCO","family":"RICCA","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2023,7,5]]},"reference":[{"key":"S1471068423000121_ref22","first-page":"841","article-title":"A multi-engine approach to answer-set programming","volume":"6","author":"Maratea","year":"2014","journal-title":"TPLP 14"},{"key":"S1471068423000121_ref24","first-page":"620","article-title":"The well-founded semantics for general logic programs","volume":"3","author":"Van Gelder","year":"1991","journal-title":"J. ACM 38"},{"key":"S1471068423000121_ref23","doi-asserted-by":"crossref","first-page":"224","DOI":"10.1016\/j.artint.2019.04.002","article-title":"The 2016 and 2017 QBF solvers evaluations (qbfeval\u201916 and qbfeval\u201917)","author":"Pulina","year":"2019","journal-title":"Artif. Intell. 274"},{"key":"S1471068423000121_ref4","doi-asserted-by":"crossref","DOI":"10.1016\/j.artint.2019.103185","article-title":"New models for generating hard random boolean formulas and disjunctive logic programs","volume":"279","author":"Amendola","year":"2020","journal-title":"Artif. Intell."},{"key":"S1471068423000121_ref6","doi-asserted-by":"crossref","first-page":"92","DOI":"10.1145\/2043174.2043195","article-title":"Answer set programming at a glance","volume":"12","author":"Brewka","year":"2011","journal-title":"Commun. ACM 54"},{"key":"S1471068423000121_ref8","doi-asserted-by":"crossref","first-page":"374","DOI":"10.1145\/502807.502810","article-title":"Complexity and expressive power of logic programming","volume":"3","author":"Dantsin","year":"2001","journal-title":"ACM Comput. Surv. 33"},{"key":"S1471068423000121_ref13","first-page":"663","article-title":"Planning with incomplete information in quantified answer set programming","volume":"5","author":"Fandinno","year":"2021","journal-title":"TPLP 21"},{"key":"S1471068423000121_ref16","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1613\/jair.5373","article-title":"The sixth answer set programming competition","volume":"60","author":"Gebser","year":"2017","journal-title":"J. Artif. Intell. Res."},{"key":"S1471068423000121_ref20","doi-asserted-by":"crossref","unstructured":"Janhunen, T. 2022. Implementing stable-unstable semantics with ASPTOOLS and clingo. In PADL 2022, Proceedings. LNCS, vol. 13165. Springer, 135\u2013153.","DOI":"10.1007\/978-3-030-94479-7_9"},{"key":"S1471068423000121_ref10","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1609\/aimag.v37i3.2678","article-title":"Applications of answer set programming","volume":"3","author":"Erdem","year":"2016","journal-title":"AI Magazine 37"},{"key":"S1471068423000121_ref14","doi-asserted-by":"crossref","unstructured":"Gebser, M. , Kaminski, R. , K\u00f6nig, A. and Schaub, T. 2011. Advances in gringo series 3. In LPNMR 2011. Proceedings. LNCS, vol. 6645. Springer, 345\u2013351.","DOI":"10.1007\/978-3-642-20895-9_39"},{"key":"S1471068423000121_ref3","first-page":"705","article-title":"Beyond NP: quantifying over answer sets","volume":"19","author":"Amendola","year":"2019","journal-title":"TPLP"},{"key":"S1471068423000121_ref5","first-page":"570","article-title":"Stable-unstable semantics: Beyond NP with normal logic programs","volume":"5\u20136","author":"Bogaerts","year":"2016","journal-title":"TPLP 16"},{"key":"S1471068423000121_ref11","unstructured":"Faber, W. and Morak, M. 2022. Evaluating epistemic logic programs via answer set programming with quantifiers. In HYDRA\/RCRA@LPNMR. CEUR WS, vol. 3281, 78\u201389."},{"key":"S1471068423000121_ref15","doi-asserted-by":"crossref","unstructured":"Gebser, M. , Leone, N. , Maratea, M. , Perri, S. , Ricca, F. and Schaub, T. 2018. Evaluation techniques and systems for answer set programming: a survey. In Proceedings of IJCAI 2018. ijcai.org, 5450\u20135456.","DOI":"10.24963\/ijcai.2018\/769"},{"key":"S1471068423000121_ref19","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1007\/s13218-018-0529-9","article-title":"Cross-translating answer set programs using the ASPTOOLS collection","volume":"32","author":"Janhunen","year":"2018","journal-title":"K\u00fcnstliche Intell."},{"key":"S1471068423000121_ref9","doi-asserted-by":"crossref","first-page":"289","DOI":"10.1007\/BF01536399","article-title":"On the computational cost of disjunctive logic programming: Propositional case","volume":"3\u20134","author":"Eiter","year":"1995","journal-title":"Ann. Math. Artif. Intell. 15,"},{"key":"S1471068423000121_ref1","doi-asserted-by":"crossref","unstructured":"Amendola, G. , Cuteri, B. , Ricca, F. and Truszczynski, M. 2022. Solving problems in the PH with ASP(Q). In Proceedings of LPNMR. LNCS, vol. 13416. Springer, 373\u2013386.","DOI":"10.1007\/978-3-031-15707-3_29"},{"key":"S1471068423000121_ref7","first-page":"205","article-title":"Efficiently coupling the I-DLV grounder with ASP solvers","volume":"2","author":"Calimeri","year":"2020","journal-title":"TPLP 20"},{"key":"S1471068423000121_ref2","doi-asserted-by":"crossref","first-page":"103519","DOI":"10.1016\/j.artint.2021.103519","article-title":"Paracoherent answer set computation","volume":"299","author":"Amendola","year":"2021","journal-title":"Artif. Intell."},{"key":"S1471068423000121_ref12","doi-asserted-by":"crossref","unstructured":"Faber, W. , Morak, M. and Chrpa, L. 2022. Determining action reversibility in STRIPS using asp with quantifiers. In PADL. LNCS, vol. 13165. Springer, 42\u201356.","DOI":"10.1007\/978-3-030-94479-7_4"},{"key":"S1471068423000121_ref17","doi-asserted-by":"crossref","first-page":"365","DOI":"10.1007\/BF03037169","article-title":"Classical negation in logic programs and disjunctive databases","volume":"9","author":"Gelfond","year":"1991","journal-title":"New Gener. Comput."},{"key":"S1471068423000121_ref21","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1016\/S0004-3702(02)00186-8","article-title":"Answer set programming and plan generation","volume":"1\u20132","author":"Lifschitz","year":"2002","journal-title":"Artif. Intell. 138"},{"key":"S1471068423000121_ref18","unstructured":"Janhunen, T. 2004. Representing normal programs with clauses. In Proceedings of ECAI\u20192004., R. L. de M\u00e1ntaras and L. Saitta, Eds. IOS Press, 358\u2013362."}],"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\/S1471068423000121","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,27]],"date-time":"2024-02-27T09:38:40Z","timestamp":1709026720000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1471068423000121\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,7]]},"references-count":24,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2023,7]]}},"alternative-id":["S1471068423000121"],"URL":"https:\/\/doi.org\/10.1017\/s1471068423000121","relation":{},"ISSN":["1471-0684","1475-3081"],"issn-type":[{"value":"1471-0684","type":"print"},{"value":"1475-3081","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,7]]},"assertion":[{"value":"\u00a9 The Author(s), 2023. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (http:\/\/creativecommons.org\/licenses\/by\/4.0\/), which permits unrestricted re-use, distribution and reproduction, provided the original article is properly cited.","name":"license","label":"License","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}