{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,30]],"date-time":"2025-12-30T23:37:46Z","timestamp":1767137866842,"version":"build-2238731810"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783031157066","type":"print"},{"value":"9783031157073","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Answer set programming (ASP) is a declarative programming paradigm where the solutions of a search problem are captured by the answer sets of a logic program describing its solutions. Besides native algorithms implemented as answer-set solvers, the computation of answer sets can be realized (i) by translating the logic program into propositional logic or its extensions and (ii) by finding satisfying assignments with appropriate solvers. In this work, we recall the graph-based extension of propositional logic, viz.\u00a0SAT modulo graphs, and the case of acyclicity constraint which keeps a digraph associated with each truth assignment acyclic. This particular extension lends itself very well for answer set computation, e.g., using extended SAT solvers, such as\n                    <jats:sc>GraphSAT<\/jats:sc>\n                    , as back-end solvers. The goal of this work, however, is to translate away the acyclicity extension altogether using a vertex elimination technique, giving rise to a translation from ASP into propositional clauses only. We use non-tight benchmarks and a state-of-the-art SAT solver,\n                    <jats:sc>Kissat<\/jats:sc>\n                    , to illustrate that performance obtained in this way can be competitive against\n                    <jats:sc>GraphSAT<\/jats:sc>\n                    and native ASP solvers such as\n                    <jats:sc>Clasp<\/jats:sc>\n                    and\n                    <jats:sc>Wasp<\/jats:sc>\n                    .\n                  <\/jats:p>","DOI":"10.1007\/978-3-031-15707-3_16","type":"book-chapter","created":{"date-parts":[[2022,8,26]],"date-time":"2022-08-26T07:02:47Z","timestamp":1661497367000},"page":"203-216","update-policy":"https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Efficient Computation of\u00a0Answer Sets via\u00a0SAT Modulo Acyclicity and\u00a0Vertex Elimination"],"prefix":"10.1007","author":[{"given":"Masood","family":"Feyzbakhsh Rankooh","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/2.zoppoz.workers.dev:443\/https\/orcid.org\/0000-0002-2029-7708","authenticated-orcid":false,"given":"Tomi","family":"Janhunen","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,8,29]]},"reference":[{"key":"16_CR1","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1007\/978-3-319-23264-5_5","volume-title":"Logic Programming and Nonmonotonic Reasoning","author":"M Alviano","year":"2015","unstructured":"Alviano, M., Dodaro, C., Leone, N., Ricca, F.: Advances in WASP. In: Calimeri, F., Ianni, G., Truszczynski, M. (eds.) LPNMR 2015. LNCS (LNAI), vol. 9345, pp. 40\u201354. Springer, Cham (2015). https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1007\/978-3-319-23264-5_5"},{"key":"16_CR2","unstructured":"Biere, A., Fazekas, K., Fleury, M., Heisinger, M.: CaDiCal, Kissat, Paracooba, Plingeling and Treengeling entering the SAT Competition 2020. In: SAT Competition 2020, pp. 50\u201354 (2020)"},{"key":"16_CR3","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/978-3-319-11558-0_12","volume-title":"Logics in Artificial Intelligence","author":"J Bomanson","year":"2014","unstructured":"Bomanson, J., Gebser, M., Janhunen, T.: Improving the normalization of weight rules in answer set programs. In: Ferm\u00e9, E., Leite, J. (eds.) JELIA 2014. LNCS (LNAI), vol. 8761, pp. 166\u2013180. Springer, Cham (2014). https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1007\/978-3-319-11558-0_12"},{"issue":"1","key":"16_CR4","doi-asserted-by":"publisher","first-page":"63","DOI":"10.3233\/FI-2016-1398","volume":"147","author":"J Bomanson","year":"2016","unstructured":"Bomanson, J., Gebser, M., Janhunen, T., Kaufmann, B., Schaub, T.: Answer set programming modulo acyclicity. Fundam. Informaticae 147(1), 63\u201391 (2016)","journal-title":"Fundam. Informaticae"},{"issue":"4","key":"16_CR5","doi-asserted-by":"publisher","first-page":"33:1","DOI":"10.1145\/3412854","volume":"21","author":"J Bomanson","year":"2020","unstructured":"Bomanson, J., Janhunen, T., Niemel\u00e4, I.: Applying visible strong equivalence in answer-set program transformations. ACM Trans. Comput. Log. 21(4), 33:1-33:41 (2020)","journal-title":"ACM Trans. Comput. Log."},{"issue":"12","key":"16_CR6","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1145\/2043174.2043195","volume":"54","author":"G Brewka","year":"2011","unstructured":"Brewka, G., Eiter, T., Truszczynski, M.: Answer set programming at a glance. Commun. ACM 54(12), 92\u2013103 (2011)","journal-title":"Commun. ACM"},{"key":"16_CR7","doi-asserted-by":"crossref","unstructured":"Clark, K.: Negation as failure. In: Gallaire, H., Minker, J. (eds.) Logic and Data Bases, pp. 293\u2013322. Plenum Press (1978)","DOI":"10.1007\/978-1-4684-3384-5_11"},{"key":"16_CR8","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/978-3-319-11558-0_10","volume-title":"Logics in Artificial Intelligence","author":"M Gebser","year":"2014","unstructured":"Gebser, M., Janhunen, T., Rintanen, J.: SAT modulo graphs: acyclicity. In: Ferm\u00e9, E., Leite, J. (eds.) JELIA 2014. LNCS (LNAI), vol. 8761, pp. 137\u2013151. Springer, Cham (2014). https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1007\/978-3-319-11558-0_10"},{"key":"16_CR9","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/978-3-319-11558-0_10","volume-title":"Logics in Artificial Intelligence","author":"M Gebser","year":"2014","unstructured":"Gebser, M., Janhunen, T., Rintanen, J.: SAT modulo graphs: acyclicity. In: Ferm\u00e9, E., Leite, J. (eds.) JELIA 2014. LNCS (LNAI), vol. 8761, pp. 137\u2013151. Springer, Cham (2014). https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1007\/978-3-319-11558-0_10"},{"issue":"4","key":"16_CR10","doi-asserted-by":"publisher","first-page":"923","DOI":"10.1093\/logcom\/exv063","volume":"30","author":"M Gebser","year":"2020","unstructured":"Gebser, M., Janhunen, T., Rintanen, J.: Declarative encodings of acyclicity properties. J. Log. Comput. 30(4), 923\u2013952 (2020)","journal-title":"J. Log. Comput."},{"key":"16_CR11","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"368","DOI":"10.1007\/978-3-319-23264-5_31","volume-title":"Logic Programming and Nonmonotonic Reasoning","author":"M Gebser","year":"2015","unstructured":"Gebser, M., Kaminski, R., Kaufmann, B., Romero, J., Schaub, T.: Progress in clasp Series 3. In: Calimeri, F., Ianni, G., Truszczynski, M. (eds.) LPNMR 2015. LNCS (LNAI), vol. 9345, pp. 368\u2013383. Springer, Cham (2015). https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1007\/978-3-319-23264-5_31"},{"issue":"2","key":"16_CR12","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1017\/S1471068419000061","volume":"20","author":"M Gebser","year":"2020","unstructured":"Gebser, M., Maratea, M., Ricca, F.: The seventh answer set programming competition: design and results. Theory Pract. Log. Program. 20(2), 176\u2013204 (2020)","journal-title":"Theory Pract. Log. Program."},{"issue":"1\u20132","key":"16_CR13","doi-asserted-by":"publisher","first-page":"35","DOI":"10.3166\/jancl.16.35-86","volume":"16","author":"T Janhunen","year":"2006","unstructured":"Janhunen, T.: Some (in)translatability results for normal logic programs and propositional theories. J. Appl. Non Class. Logics 16(1\u20132), 35\u201386 (2006)","journal-title":"J. Appl. Non Class. Logics"},{"issue":"2\u20133","key":"16_CR14","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/s13218-018-0529-9","volume":"32","author":"T Janhunen","year":"2018","unstructured":"Janhunen, T.: Cross-translating answer set programs using the ASPTOOLS collection. K\u00fcnstliche Intell. 32(2\u20133), 183\u2013184 (2018)","journal-title":"K\u00fcnstliche Intell."},{"issue":"3","key":"16_CR15","first-page":"13","volume":"37","author":"T Janhunen","year":"2016","unstructured":"Janhunen, T., Niemel\u00e4, I.: The answer set programming paradigm. AI Mag. 37(3), 13\u201324 (2016)","journal-title":"AI Mag."},{"key":"16_CR16","unstructured":"Lifschitz, V.: What is answer set programming? In: AAAI 2008, pp. 1594\u20131597 (2008)"},{"key":"16_CR17","unstructured":"Lin, F., Zhao, J.: On tight logic programs and yet another translation from normal logic programs to propositional logic. In: IJCAI 2003, pp. 853\u2013858 (2003)"},{"key":"16_CR18","unstructured":"Lin, F., Zhao, Y.: ASSAT: computing answer sets of a logic program by SAT solvers. In: AAAI 2002, pp. 112\u2013118 (2002)"},{"issue":"3\u20134","key":"16_CR19","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1023\/A:1018930122475","volume":"25","author":"I Niemel\u00e4","year":"1999","unstructured":"Niemel\u00e4, I.: Logic programs with stable model semantics as a constraint programming paradigm. Ann. Math. Artif. Intell. 25(3\u20134), 241\u2013273 (1999)","journal-title":"Ann. Math. Artif. Intell."},{"key":"16_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/11513988_33","volume-title":"Computer Aided Verification","author":"R Nieuwenhuis","year":"2005","unstructured":"Nieuwenhuis, R., Oliveras, A.: DPLL(T) with exhaustive theory propagation and its application to difference logic. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 321\u2013334. Springer, Heidelberg (2005). https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1007\/11513988_33"},{"key":"16_CR21","doi-asserted-by":"crossref","unstructured":"Rankooh, M.F., Rintanen, J.: Propositional encodings of acyclicity and reachability by using vertex elimination. In: AAAI 2022 (2022, to appear)","DOI":"10.1609\/aaai.v36i5.20530"},{"key":"16_CR22","doi-asserted-by":"crossref","unstructured":"Rose, D.J., Tarjan, R.E.: Algorithmic aspects of vertex elimination. In: Proceedings of the 7th Annual ACM Symposium on Theory of Computing, pp. 245\u2013254 (1975)","DOI":"10.1145\/800116.803775"},{"issue":"1\u20132","key":"16_CR23","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1016\/S0004-3702(02)00187-X","volume":"138","author":"P Simons","year":"2002","unstructured":"Simons, P., Niemel\u00e4, I., Soininen, T.: Extending and implementing the stable model semantics. Artif. Intell. 138(1\u20132), 181\u2013234 (2002)","journal-title":"Artif. Intell."},{"key":"16_CR24","first-page":"234","volume":"8","author":"G Tseitin","year":"1968","unstructured":"Tseitin, G.: On the complexity of derivation in the propositional calculus. Zapiski Nauchnykh Seminarov LOMI 8, 234\u2013259 (1968)","journal-title":"Zapiski Nauchnykh Seminarov LOMI"}],"updated-by":[{"DOI":"10.1007\/978-3-031-15707-3_40","type":"correction","label":"Correction","source":"publisher","updated":{"date-parts":[[2022,8,29]],"date-time":"2022-08-29T00:00:00Z","timestamp":1661731200000}}],"container-title":["Lecture Notes in Computer Science","Logic Programming and Nonmonotonic Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-15707-3_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,11,25]],"date-time":"2022-11-25T16:35:48Z","timestamp":1669394148000},"score":1,"resource":{"primary":{"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/link.springer.com\/10.1007\/978-3-031-15707-3_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031157066","9783031157073"],"references-count":24,"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1007\/978-3-031-15707-3_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"29 August 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"29 August 2022","order":2,"name":"change_date","label":"Change Date","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"Correction","order":3,"name":"change_type","label":"Change Type","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"Chapters [\u201cStatistical Statements in Probabilistic Logic Programming\u201c and \u201cEfficient Computation of Answer Sets via SAT Modulo Acyclicity and Vertex Elimination\u201d] were previously published non-open access. They have now been changed to open access under a CC BY 4.0 license and the copyright holder updated to \u2018The Author(s)\u2019. The book has also been updated with these changes.","order":4,"name":"change_details","label":"Change Details","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"LPNMR","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Logic Programming and Nonmonotonic Reasoning","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Genoa","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 September 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 September 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"lpnmr2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/2.zoppoz.workers.dev:443\/https\/lpnmr2022.dibris.unige.it\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"easychair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"57","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"34","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"60% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}