{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,2]],"date-time":"2025-11-02T17:01:33Z","timestamp":1762102893512,"version":"3.40.3"},"publisher-location":"Cham","reference-count":49,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031433689"},{"type":"electronic","value":"9783031433696"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T00:00:00Z","timestamp":1694563200000},"content-version":"vor","delay-in-days":255,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We present<jats:sc>Abstract CNF2dDNNF<\/jats:sc>, a calculus describing an approach for compiling a formula in conjunctive normal form (CNF) into deterministic negation normal form (d-DNNF). It combines component-based reasoning with a model enumeration approach based on conflict-driven clause learning (CDCL) with chronological backtracking. Its properties, such as soundness and termination, carry over to implementations which can be modeled by it. We provide a correctness proof and a detailed example. The main conceptual differences to currently available tools targeting d-DNNF compilation are discussed and future research directions presented. The aim of this work is to lay the theoretical foundation for a novel method for d-DNNF compilation. To the best of our knowledge, our approach is the first knowledge compilation method using CDCL with chronological backtracking.<\/jats:p>","DOI":"10.1007\/978-3-031-43369-6_11","type":"book-chapter","created":{"date-parts":[[2023,9,14]],"date-time":"2023-09-14T14:32:18Z","timestamp":1694701938000},"page":"195-213","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["An Abstract CNF-to-d-DNNF Compiler Based on\u00a0Chronological CDCL"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7883-7749","authenticated-orcid":false,"given":"Sibylle","family":"M\u00f6hle","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,9,13]]},"reference":[{"key":"11_CR1","unstructured":"Bacchus, F., Dalmao, S., Pitassi, T.: DPLL with caching: a new algorithm for #SAT and Bayesian inference. Electron. Colloquium Comput. Complex. TR03-003 (2003)"},{"key":"11_CR2","unstructured":"Barrett, A.: From hybrid systems to universal plans via domain compilation. In: ICAPS, pp. 44\u201351. AAAI (2004)"},{"key":"11_CR3","unstructured":"Barrett, A.: Model compilation for real-time planning and diagnosis with feedback. In: IJCAI, pp. 1195\u20131200. Professional Book Center (2005)"},{"key":"11_CR4","unstructured":"Bayardo Jr., R., Pehoushek, J.: Counting models using connected components. In: AAAI\/IAAI, pp. 157\u2013162. AAAI Press\/The MIT Press (2000)"},{"issue":"4","key":"11_CR5","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1007\/s00224-013-9447-2","volume":"53","author":"A Bernasconi","year":"2013","unstructured":"Bernasconi, A., Ciriani, V., Luccio, F., Pagli, L.: Compact DSOP and partial DSOP forms. Theory Comput. Syst. 53(4), 583\u2013608 (2013)","journal-title":"Theory Comput. Syst."},{"issue":"1\u20134","key":"11_CR6","first-page":"201","volume":"2","author":"A Biere","year":"2006","unstructured":"Biere, A., Sinz, C.: Decomposing SAT problems into connected components. J. Satisf. Boolean Model. Comput. 2(1\u20134), 201\u2013208 (2006)","journal-title":"J. Satisf. Boolean Model. Comput."},{"issue":"5","key":"11_CR7","doi-asserted-by":"publisher","first-page":"799","DOI":"10.1007\/s00224-019-09960-w","volume":"64","author":"B Bollig","year":"2020","unstructured":"Bollig, B., Buttkus, M.: On limitations of structured (deterministic) DNNFs. Theory Comput. Syst. 64(5), 799\u2013825 (2020)","journal-title":"Theory Comput. Syst."},{"issue":"2","key":"11_CR8","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/s00224-020-10003-y","volume":"65","author":"B Bollig","year":"2021","unstructured":"Bollig, B., Farenholtz, M.: On the relation between structured d-DNNFs and SDDs. Theory Comput. Syst. 65(2), 274\u2013295 (2021)","journal-title":"Theory Comput. Syst."},{"key":"11_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/978-3-319-24318-4_15","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2015","author":"S Bova","year":"2015","unstructured":"Bova, S., Capelli, F., Mengel, S., Slivovsky, F.: On compiling CNFs into structured deterministic DNNFs. In: Heule, M., Weaver, S. (eds.) SAT 2015. LNCS, vol. 9340, pp. 199\u2013214. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-24318-4_15"},{"key":"11_CR10","unstructured":"Bova, S., Capelli, F., Mengel, S., Slivovsky, F.: Knowledge compilation meets communication complexity. In: IJCAI, pp. 1008\u20131014. IJCAI\/AAAI Press (2016)"},{"key":"11_CR11","doi-asserted-by":"publisher","unstructured":"Burchard, J., Schubert, T., Becker, B.: Laissez-faire caching for parallel $$\\#$$SAT solving. In: Heule, M., Weaver, S. (eds.) SAT 2015. LNCS, vol. 9340, pp. 46\u201361. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-24318-4_5","DOI":"10.1007\/978-3-319-24318-4_5"},{"key":"11_CR12","doi-asserted-by":"crossref","unstructured":"Burchard, J., Schubert, T., Becker, B.: Distributed parallel $$\\#$$SAT solving. In: CLUSTER, pp. 326\u2013335. IEEE Computer Society (2016)","DOI":"10.1109\/CLUSTER.2016.20"},{"issue":"3\u20134","key":"11_CR13","first-page":"137","volume":"10","author":"M Cadoli","year":"1997","unstructured":"Cadoli, M., Donini, F.M.: A survey on knowledge compilation. AI Commun. 10(3\u20134), 137\u2013150 (1997)","journal-title":"AI Commun."},{"key":"11_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/11814948_9","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"M Chavira","year":"2006","unstructured":"Chavira, M., Darwiche, A.: Encoding CNFs to empower component analysis. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 61\u201374. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11814948_9"},{"issue":"1\u20132","key":"11_CR15","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1016\/j.ijar.2005.10.001","volume":"42","author":"M Chavira","year":"2006","unstructured":"Chavira, M., Darwiche, A., Jaeger, M.: Compiling relational Bayesian networks for exact inference. Int. J. Approx. Reason. 42(1\u20132), 4\u201320 (2006)","journal-title":"Int. J. Approx. Reason."},{"issue":"1\u20133","key":"11_CR16","first-page":"99","volume":"6","author":"G Chu","year":"2009","unstructured":"Chu, G., Harwood, A., Stuckey, P.J.: Cache conscious data structures for Boolean satisfiability solvers. J. Satisf. Boolean Model. Comput. 6(1\u20133), 99\u2013120 (2009)","journal-title":"J. Satisf. Boolean Model. Comput."},{"key":"11_CR17","unstructured":"Darwiche, A.: Compiling knowledge into decomposable negation normal form. In: IJCAI, pp. 284\u2013289. Morgan Kaufmann (1999)"},{"issue":"4","key":"11_CR18","doi-asserted-by":"publisher","first-page":"608","DOI":"10.1145\/502090.502091","volume":"48","author":"A Darwiche","year":"2001","unstructured":"Darwiche, A.: Decomposable negation normal norm. J. ACM 48(4), 608\u2013647 (2001)","journal-title":"J. ACM"},{"issue":"1\u20132","key":"11_CR19","doi-asserted-by":"publisher","first-page":"11","DOI":"10.3166\/jancl.11.11-34","volume":"11","author":"A Darwiche","year":"2001","unstructured":"Darwiche, A.: On the tractable counting of theory models and its application to truth maintenance and belief revision. J. Appl. Non Class. Logics 11(1\u20132), 11\u201334 (2001)","journal-title":"J. Appl. Non Class. Logics"},{"key":"11_CR20","unstructured":"Darwiche, A.: New advances in compiling CNF into decomposable negation normal form. In: ECAI, pp. 328\u2013332. IOS Press (2004)"},{"key":"11_CR21","unstructured":"Darwiche, A.: SDD: a new canonical representation of propositional knowledge bases. In: IJCAI, pp. 819\u2013826. IJCAI\/AAAI (2011)"},{"key":"11_CR22","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1613\/jair.989","volume":"17","author":"A Darwiche","year":"2002","unstructured":"Darwiche, A., Marquis, P.: A knowledge compilation map. J. Artif. Intell. Res. 17, 229\u2013264 (2002)","journal-title":"J. Artif. Intell. Res."},{"issue":"7","key":"11_CR23","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.W.: A machine program for theorem-proving. Commun. ACM 5(7), 394\u2013397 (1962)","journal-title":"Commun. ACM"},{"issue":"3","key":"11_CR24","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7(3), 201\u2013215 (1960)","journal-title":"J. ACM"},{"key":"11_CR25","unstructured":"Fargier, H., Mengin, J.: A knowledge compilation map for conditional preference statements-based languages. In: AAMAS, pp. 492\u2013500. ACM (2021)"},{"key":"11_CR26","unstructured":"Huang, J., Darwiche, A.: DPLL with a trace: From SAT to knowledge compilation. In: IJCAI, pp. 156\u2013162. Professional Book Center (2005)"},{"key":"11_CR27","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1613\/jair.2097","volume":"29","author":"J Huang","year":"2007","unstructured":"Huang, J., Darwiche, A.: The language of search. J. Artif. Intell. Res. 29, 191\u2013219 (2007)","journal-title":"J. Artif. Intell. Res."},{"key":"11_CR28","doi-asserted-by":"crossref","unstructured":"Huang, X., Izza, Y., Ignatiev, A., Cooper, M.C., Asher, N., Marques-Silva, J.: Tractable explanations for d-DNNF classifiers. In: AAAI, pp. 5719\u20135728. AAAI Press (2022)","DOI":"10.1609\/aaai.v36i5.20514"},{"key":"11_CR29","unstructured":"Koriche, F., Lagniez, J., Marquis, P., Thomas, S.: Knowledge compilation for model counting: affine decision trees. In: IJCAI, pp. 947\u2013953. IJCAI\/AAAI (2013)"},{"key":"11_CR30","doi-asserted-by":"crossref","unstructured":"Lagniez, J., Marquis, P.: An improved Decision-DNNF compiler. In: IJCAI, pp. 667\u2013673. ijcai.org (2017)","DOI":"10.24963\/ijcai.2017\/93"},{"key":"11_CR31","doi-asserted-by":"crossref","unstructured":"Lagniez, J., Marquis, P., Szczepanski, N.: DMC: a distributed model counter. In: IJCAI, pp. 1331\u20131338. ijcai.org (2018)","DOI":"10.24963\/ijcai.2018\/185"},{"key":"11_CR32","doi-asserted-by":"crossref","unstructured":"M\u00f6hle, S., Biere, A.: Dualizing projected model counting. In: ICTAI, pp. 702\u2013709. IEEE (2018)","DOI":"10.1109\/ICTAI.2018.00111"},{"key":"11_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/978-3-030-24258-9_18","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2019","author":"S M\u00f6hle","year":"2019","unstructured":"M\u00f6hle, S., Biere, A.: Backing backtracking. In: Janota, M., Lynce, I. (eds.) SAT 2019. LNCS, vol. 11628, pp. 250\u2013266. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-24258-9_18"},{"key":"11_CR34","doi-asserted-by":"crossref","unstructured":"M\u00f6hle, S., Biere, A.: Combining conflict-driven clause learning and chronological backtracking for propositional model counting. In: GCAI. EPiC Series in Computing, vol. 65, pp. 113\u2013126. EasyChair (2019)","DOI":"10.29007\/vgg4"},{"key":"11_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1007\/978-3-030-51825-7_5","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2020","author":"S M\u00f6hle","year":"2020","unstructured":"M\u00f6hle, S., Sebastiani, R., Biere, A.: Four flavors of entailment. In: Pulina, L., Seidl, M. (eds.) SAT 2020. LNCS, vol. 12178, pp. 62\u201371. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-51825-7_5"},{"key":"11_CR36","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: DAC, pp. 530\u2013535. ACM (2001)","DOI":"10.1145\/378239.379017"},{"key":"11_CR37","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1007\/978-3-642-30353-1_36","volume-title":"Advances in Artificial Intelligence","author":"C Muise","year":"2012","unstructured":"Muise, C., McIlraith, S.A., Beck, J.C., Hsu, E.I.: Dsharp: fast d-DNNF compilation with sharpSAT. In: Kosseim, L., Inkpen, D. (eds.) AI 2012. LNCS (LNAI), vol. 7310, pp. 356\u2013361. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-30353-1_36"},{"key":"11_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/978-3-319-94144-8_7","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2018","author":"A Nadel","year":"2018","unstructured":"Nadel, A., Ryvchin, V.: Chronological backtracking. In: Beyersdorff, O., Wintersteiger, C.M. (eds.) SAT 2018. LNCS, vol. 10929, pp. 111\u2013121. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-94144-8_7"},{"key":"11_CR39","unstructured":"Palacios, H., Bonet, B., Darwiche, A., Geffner, H.: Pruning conformant plans by counting models on compiled d-DNNF representations. In: ICAPS, pp. 141\u2013150. AAAI (2005)"},{"key":"11_CR40","unstructured":"Pipatsrisawat, K., Darwiche, A.: A new d-DNNF-based bound computation algorithm for functional E-MAJSAT. In: IJCAI, pp. 590\u2013595 (2009)"},{"key":"11_CR41","unstructured":"Sang, T., Bacchus, F., Beame, P., Kautz, H.A., Pitassi, T.: Combining component caching and clause learning for effective model counting. In: SAT (2004)"},{"key":"11_CR42","doi-asserted-by":"crossref","unstructured":"Sharma, S., Roy, S., Soos, M., Meel, K.S.: GANAK: a scalable probabilistic exact model counter. In: IJCAI, pp. 1169\u20131176. ijcai.org (2019)","DOI":"10.24963\/ijcai.2019\/163"},{"key":"11_CR43","unstructured":"Siddiqi, S.A., Huang, J.: Probabilistic sequential diagnosis by compilation. In: ISAIM (2008)"},{"key":"11_CR44","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J.M., Sakallah, K.A.: GRASP - a new search algorithm for satisfiability. In: ICCAD, pp. 220\u2013227. IEEE Computer Society\/ACM (1996)","DOI":"10.1109\/ICCAD.1996.569607"},{"key":"11_CR45","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J.M., Sakallah, K.A.: GRASP: a search algorithm for propositional satisfiability. IEEE Trans. Comput. 48(5), 506\u2013521 (1999)","DOI":"10.1109\/12.769433"},{"key":"11_CR46","unstructured":"Spallitta, G., Sebastiani, R., Biere, A.: Enumerating disjoint partial models without blocking clauses. CoRR abs\/2306.00461 (2023)"},{"key":"11_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"424","DOI":"10.1007\/11814948_38","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"M Thurley","year":"2006","unstructured":"Thurley, M.: sharpSAT \u2013 counting models with advanced component caching and implicit BCP. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 424\u2013429. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11814948_38"},{"issue":"1","key":"11_CR48","doi-asserted-by":"publisher","first-page":"56","DOI":"10.1007\/s10601-018-9297-2","volume":"24","author":"D de U\u00f1a","year":"2019","unstructured":"de U\u00f1a, D., Gange, G., Schachte, P., Stuckey, P.J.: Compiling CP subproblems to MDDs and d-DNNFs. Constraints An Int. J. 24(1), 56\u201393 (2019)","journal-title":"Constraints An Int. J."},{"key":"11_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/978-3-540-24605-3_22","volume-title":"Theory and Applications of Satisfiability Testing","author":"L Zhang","year":"2004","unstructured":"Zhang, L., Malik, S.: Cache performance of SAT solvers: a case study for efficient implementation of algorithms. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 287\u2013298. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24605-3_22"}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-43369-6_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,28]],"date-time":"2024-10-28T02:21:34Z","timestamp":1730082094000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-43369-6_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031433689","9783031433696"],"references-count":49,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-43369-6_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"13 September 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FroCoS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Frontiers of Combining Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Prague","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Czech Republic","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 September 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 September 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"frocos2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/frocos2023.github.io\/index.html","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}