{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,12]],"date-time":"2025-03-12T04:23:18Z","timestamp":1741753398783,"version":"3.38.0"},"reference-count":96,"publisher":"SAGE Publications","issue":"2","license":[{"start":{"date-parts":[[2024,5,25]],"date-time":"2024-05-25T00:00:00Z","timestamp":1716595200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/journals.sagepub.com\/page\/policies\/text-and-data-mining-license"}],"content-domain":{"domain":["journals.sagepub.com"],"crossmark-restriction":true},"short-container-title":["Intelligenza Artificiale: The international journal of the AIxIA"],"published-print":{"date-parts":[[2024,10,9]]},"abstract":"<jats:p> Answer Set Programming (ASP) is a declarative language oriented towards solving complex combinatorial problems. In fact, ASP has been successfully used to address problems in various academic and industrial domains. The success of ASP can be attributed to its concise syntax, intuitive semantics, and the availability of several efficient solvers based on the Conflict-Driven Clause Learning (CDCL) algorithm. This paper details the design and implementation of contemporary CDCL solvers, emphasizing both algorithmic descriptions and their effective and efficientimplementation. <\/jats:p>","DOI":"10.3233\/ia-240019","type":"journal-article","created":{"date-parts":[[2024,5,28]],"date-time":"2024-05-28T17:39:57Z","timestamp":1716917997000},"page":"239-259","update-policy":"https:\/\/doi.org\/10.1177\/sage-journals-update-policy","source":"Crossref","is-referenced-by-count":0,"title":["Design and implementation of modern CDCL ASP solvers"],"prefix":"10.1177","volume":"18","author":[{"given":"Carmine","family":"Dodaro","sequence":"first","affiliation":[{"name":"Department of Mathematics and Computer Science, University of Calabria, Via P. Bucci, cubo 30B, Rende (CS), Italy"}]}],"member":"179","published-online":{"date-parts":[[2024,5,25]]},"reference":[{"key":"ref001","unstructured":"AlvianoM., DodaroC., Completion of disjunctive logic programs. In Proc. of IJCAI, (2016), pp. 886\u2013892. IJCAI\/AAAI Press. URL http:\/\/www.ijcai.org\/Abstract\/16\/130."},{"key":"ref002","doi-asserted-by":"publisher","DOI":"10.1017\/S147106841600020X"},{"key":"ref003","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40564-8_6"},{"key":"ref004","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-03524-6_1"},{"key":"ref005","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-23264-5_5"},{"key":"ref006","unstructured":"AlvianoM., DodaroC., RiccaF., A maxsat algorithm using cardinality constraints of bounded size. In Proc. of IJCAI, (2015), pp. 2677\u20132683. AAAI Press. URL http:\/\/ijcai.org\/Abstract\/15\/379."},{"key":"ref007","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-61660-5_19"},{"key":"ref008","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068418000133"},{"key":"ref009","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-20528-7_18"},{"key":"ref010","doi-asserted-by":"publisher","DOI":"10.1093\/LOGCOM\/EXV061"},{"key":"ref011","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068422000047"},{"key":"ref012","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ICLP.2012.211"},{"key":"ref013","unstructured":"AudemardG., SimonL., Predicting learnt clauses quality in modern SAT solvers. In Proc. of IJCAI, (2009), pp. 399\u2013404. URL http:\/\/ijcai.org\/Proceedings\/09\/Papers\/074.pdf."},{"key":"ref014","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33558-7_11"},{"key":"ref015","doi-asserted-by":"publisher","DOI":"10.1016\/J.PARCO.2005.03.004"},{"key":"ref016","unstructured":"Baral.C. Knowledge Representation, Reasoning and Declarative Problem Solving. Cambridge University Press, 2010. ISBN 978-0-521-14775-0."},{"key":"ref017","doi-asserted-by":"publisher","DOI":"10.1007\/BF01530761"},{"key":"ref018","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-24318-4_29"},{"key":"ref019","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40564-8_19"},{"key":"ref020","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-11558-0_12"},{"key":"ref021","doi-asserted-by":"publisher","DOI":"10.1145\/2043174.2043195"},{"key":"ref022","doi-asserted-by":"publisher","DOI":"10.1109\/69.877512"},{"key":"ref023","doi-asserted-by":"publisher","DOI":"10.3233\/IA-170104"},{"key":"ref024","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068418000546"},{"key":"ref025","doi-asserted-by":"publisher","DOI":"10.3233\/SAT190064"},{"key":"ref026","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4684-3384-5_11"},{"key":"ref027","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068417000254"},{"key":"ref028","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068419000231"},{"key":"ref029","doi-asserted-by":"publisher","DOI":"10.3233\/FI-2009-180"},{"key":"ref030","doi-asserted-by":"publisher","DOI":"10.1145\/321033.321034"},{"key":"ref031","doi-asserted-by":"publisher","DOI":"10.1145\/368273.368557"},{"key":"ref032","doi-asserted-by":"publisher","DOI":"10.1007\/S10601-010-9095-Y"},{"key":"ref033","unstructured":"DodaroC., AlvianoM., FaberW., LeoneN., RiccaF., SirianniM., The birth of a WASP: preliminary report on a new ASP solver. In Proc. of CILC, volume 810 of CEUR Workshop Proceedings, (2011), pp. 99\u2013113. CEURWS. org. URLhttps:\/\/ceur-ws.org\/Vol-810\/paper-l06.pdf."},{"key":"ref034","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-15707-3_12"},{"key":"ref035","doi-asserted-by":"publisher","DOI":"10.3233\/FAIA230316"},{"key":"ref036","unstructured":"DovierA., FormisanoA., PontelliE., VellaF., Parallel execution of the ASP computation - an investigation on gpus. In Proc. of ICLP Technical Communications, volume 1433 ofCEURWorkshop Proceedings. CEUR-WS.org, 2015. URL https:\/\/ceur-ws.org\/Vol-1433\/tc_11.pdf."},{"key":"ref037","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-28228-2_3"},{"key":"ref038","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63516-3_7"},{"key":"ref039","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-46714-2_1"},{"key":"ref040","unstructured":"DrescherC., GebserM., GroteT., KaufmannB., K\u00f6nigA., OstrowskiM., SchaubT., Conflict-driven disjunctive answer set solving. In Proc. of KR, (2008), pp. 422\u2013432. AAAI Press. URLhttp:\/\/www.aaai.org\/Library\/KR\/2008\/kr08-041.php."},{"key":"ref041","doi-asserted-by":"publisher","DOI":"10.1007\/11499107_5"},{"key":"ref042","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"ref043","doi-asserted-by":"publisher","DOI":"10.1145\/261124.261126"},{"key":"ref044","doi-asserted-by":"publisher","DOI":"10.1609\/AIMAG.V37I3.2678"},{"key":"ref045","doi-asserted-by":"publisher","DOI":"10.1145\/1970398.1970401"},{"key":"ref046","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068403001923"},{"key":"ref047","unstructured":"Raphael FinkelA., Victor MarekW., MooreN., TruszczynskiM., Computing stable models in parallel. In Proc. of ASP Workshop, 2001. URLhttp:\/\/www.cs.nmsu.edu\/%7Etson\/ASP2001\/18.ps."},{"key":"ref048","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-72200-7_23"},{"key":"ref049","doi-asserted-by":"publisher","DOI":"10.3233\/978-1-58603-891-5-15"},{"key":"ref050","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02846-5_23"},{"key":"ref051","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04238-6_50"},{"key":"ref052","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20895-9_42"},{"key":"ref053","doi-asserted-by":"publisher","DOI":"10.1016\/J.ARTINT.2012.04.001"},{"key":"ref054","unstructured":"GebserM., KaufmannB., SchaubT., Advanced conflict-driven disjunctive answer set solving. In Proc. of IJCAI, (2013), pp. 912\u2013918. IJCAI\/AAAI. URL http:\/\/www.aaai.org\/ocs\/index.php\/IJCAI\/IJCAI13\/paper\/view\/6835."},{"key":"ref055","doi-asserted-by":"publisher","DOI":"10.3233\/978-1-61499-419-0-351"},{"key":"ref056","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-23264-5_31"},{"key":"ref057","doi-asserted-by":"publisher","DOI":"10.24963\/IJCAI.2018\/769"},{"key":"ref058","unstructured":"GelfondM., LifschitzV., The stable model semantics for logic programming. In Proc. of Logic Programming, (1988), pp. 1070\u20131080. MIT Press."},{"key":"ref059","doi-asserted-by":"publisher","DOI":"10.1007\/BF03037169"},{"key":"ref060","doi-asserted-by":"publisher","DOI":"10.1007\/S10845-017-1333-3"},{"key":"ref061","doi-asserted-by":"publisher","DOI":"10.1007\/11853886_43"},{"key":"ref062","unstructured":"GiunchigliaE., LierlerY., MarateaM., Satbased answer set programming. In Proc. of the Nineteenth National Conference on Artificial Intelligence, Sixteenth Conference on Innovative Applications of Artificial Intelligence, (2004), pp. 61\u201366. AAAI Press \/ The MIT Press. URL http:\/\/www.aaai.org\/Library\/AAAI\/2004\/aaai04-010.php."},{"key":"ref063","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068414000210"},{"key":"ref064","doi-asserted-by":"publisher","DOI":"10.3166\/JANCL.16.35-86"},{"key":"ref065","doi-asserted-by":"publisher","DOI":"10.1007\/S13218-018-0529-9"},{"key":"ref066","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24609-1_29"},{"key":"ref067","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04238-6_14"},{"key":"ref068","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068421000508"},{"key":"ref069","doi-asserted-by":"publisher","DOI":"10.1609\/AIMAG.V37I3.2672"},{"key":"ref070","doi-asserted-by":"publisher","DOI":"10.1016\/S0004-3702(03)00078-X"},{"key":"ref071","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04238-6_52"},{"key":"ref072","doi-asserted-by":"publisher","DOI":"10.1006\/INCO.1997.2630"},{"key":"ref073","doi-asserted-by":"publisher","DOI":"10.1145\/1149114.1149117"},{"key":"ref074","unstructured":"LierlerY., MarateaM., Computing answer sets of a logic program via-enumeration of SAT certificates. In Proc. of Answer Set Programming, Advances in Theory and Implementation, volume 78 of CEUR Workshop Proceedings. CEURWS.org, 2003. URLhttps:\/\/ceur-ws.org\/Vol-78\/asp03-final-lierler.pdf."},{"key":"ref075","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24609-1_32"},{"key":"ref076","doi-asserted-by":"publisher","DOI":"10.1016\/J.ARTINT.2004.04.004"},{"key":"ref077","unstructured":"LiuG., JanhunenT., Niemel\u00e4I., Answer set programming via mixed integer programming. In Proc. of KR. AAAI Press, 2012. URLhttp:\/\/www.aaai.org\/ocs\/index.php\/KR\/KR12\/paper\/view\/4516."},{"key":"ref078","doi-asserted-by":"publisher","DOI":"10.1007\/11546207_37"},{"key":"ref079","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(93)90029-9"},{"key":"ref080","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068413000094"},{"key":"ref081","doi-asserted-by":"publisher","DOI":"10.1093\/LOGCOM\/EXT068"},{"key":"ref082","doi-asserted-by":"publisher","DOI":"10.1609\/AAAI.V36I5.20527"},{"key":"ref083","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10428-7_41"},{"key":"ref084","doi-asserted-by":"publisher","DOI":"10.1145\/378239.379017"},{"key":"ref085","doi-asserted-by":"publisher","DOI":"10.1145\/1217856.1217859"},{"key":"ref086","unstructured":"PerriS., RiccaF., SirianniM., Towards a fullyparallel DLV system. In Proc. of RCRA, volume 616 of CEUR Workshop Proceedings. CEUR-WS.org, 2010. URL https:\/\/ceur-ws.org\/Vol-616\/paper09.pdf."},{"key":"ref087","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-41524-1_16"},{"issue":"2","key":"ref088","first-page":"155","volume":"19","author":"Ricca F.","year":"2006","journal-title":"AI Commun"},{"key":"ref089","doi-asserted-by":"publisher","DOI":"10.1016\/S0065-2458(08)60520-3"},{"key":"ref090","doi-asserted-by":"publisher","DOI":"10.1109\/12.769433"},{"key":"ref091","doi-asserted-by":"publisher","DOI":"10.1016\/S0004-3702(02)00187-X"},{"key":"ref092","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24609-1_26"},{"key":"ref093","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-61660-5_17"},{"key":"ref094","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.325.25"},{"key":"ref095","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24605-3_22"},{"key":"ref096","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2001.968634"}],"container-title":["Intelligenza Artificiale: The international journal of the AIxIA"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.3233\/IA-240019","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/full-xml\/10.3233\/IA-240019","content-type":"application\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.3233\/IA-240019","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,11]],"date-time":"2025-03-11T06:51:50Z","timestamp":1741675910000},"score":1,"resource":{"primary":{"URL":"https:\/\/journals.sagepub.com\/doi\/10.3233\/IA-240019"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,5,25]]},"references-count":96,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2024,10,9]]}},"alternative-id":["10.3233\/IA-240019"],"URL":"https:\/\/doi.org\/10.3233\/ia-240019","relation":{},"ISSN":["1724-8035","2211-0097"],"issn-type":[{"type":"print","value":"1724-8035"},{"type":"electronic","value":"2211-0097"}],"subject":[],"published":{"date-parts":[[2024,5,25]]}}}