{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,29]],"date-time":"2025-11-29T08:03:00Z","timestamp":1764403380301,"version":"3.40.3"},"publisher-location":"Cham","reference-count":60,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031656262"},{"type":"electronic","value":"9783031656279"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,7,26]],"date-time":"2024-07-26T00:00:00Z","timestamp":1721952000000},"content-version":"vor","delay-in-days":207,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Approximate model counting is the task of approximating the number of solutions to an input Boolean formula. The state-of-the-art approximate model counter for formulas in conjunctive normal form\u00a0(CNF), <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\textsf{ApproxMC}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>ApproxMC<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>, provides a scalable means of obtaining model counts with <jats:italic>probably approximately correct<\/jats:italic> (PAC)-style guarantees. Nevertheless, the validity of <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\textsf{ApproxMC}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>ApproxMC<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>\u2019s approximation relies on a careful theoretical analysis of its randomized algorithm and the correctness of its highly optimized implementation, especially the latter\u2019s stateful interactions with an incremental CNF satisfiability solver capable of natively handling parity (XOR) constraints.<\/jats:p><jats:p>We present the first certification framework for approximate model counting with formally verified guarantees on the quality of its output approximation. Our approach combines: (i) a <jats:italic>static<\/jats:italic>, once-off, formal proof of the algorithm\u2019s PAC guarantee in the Isabelle\/HOL proof assistant; and (ii) <jats:italic>dynamic<\/jats:italic>, per-run, verification of <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\textsf{ApproxMC}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>ApproxMC<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>\u2019s calls to an external CNF-XOR solver using proof certificates. We detail our general approach to establish a rigorous connection between these two parts of the verification, including our blueprint for turning the formalized, randomized algorithm into a verified proof checker, and our design of proof certificates for both <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\textsf{ApproxMC}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>ApproxMC<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula> and its internal CNF-XOR solving steps. Experimentally, we show that certificate generation adds little overhead to an approximate counter implementation, and that our certificate checker is able to fully certify <jats:inline-formula><jats:alternatives><jats:tex-math>$$84.7\\%$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mn>84.7<\/mml:mn>\n                    <mml:mo>%<\/mml:mo>\n                  <\/mml:mrow>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula> of instances with generated certificates when given the same time and memory limits as the counter.<\/jats:p>","DOI":"10.1007\/978-3-031-65627-9_8","type":"book-chapter","created":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T19:01:31Z","timestamp":1721934091000},"page":"153-177","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Formally Certified Approximate Model Counting"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7033-2463","authenticated-orcid":false,"given":"Yong Kiam","family":"Tan","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8356-6637","authenticated-orcid":false,"given":"Jiong","family":"Yang","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7355-881X","authenticated-orcid":false,"given":"Mate","family":"Soos","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9504-4107","authenticated-orcid":false,"given":"Magnus O.","family":"Myreen","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9423-5270","authenticated-orcid":false,"given":"Kuldeep S.","family":"Meel","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,7,26]]},"reference":[{"key":"8_CR1","doi-asserted-by":"publisher","unstructured":"Abdulaziz, M., Mehlhorn, K., Nipkow, T.: Trustworthy graph algorithms (invited talk). In: Rossmanith, P., Heggernes, P., Katoen, J. (eds.) MFCS. LIPIcs, vol.\u00a0138, pp. 1:1\u20131:22. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2019). https:\/\/doi.org\/10.4230\/LIPICS.MFCS.2019.1","DOI":"10.4230\/LIPICS.MFCS.2019.1"},{"key":"8_CR2","unstructured":"ApproxMCCert and CertCheck tool repository. https:\/\/github.com\/meelgroup\/approxmc-cert"},{"key":"8_CR3","doi-asserted-by":"publisher","unstructured":"Baek, S., Carneiro, M., Heule, M.J.H.: A flexible proof format for SAT solver-elaborator communication. Log. Methods Comput. Sci. 18(2) (2022). https:\/\/doi.org\/10.46298\/LMCS-18(2:3)2022","DOI":"10.46298\/LMCS-18(2:3)2022"},{"issue":"2","key":"8_CR4","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/s10817-013-9284-7","volume":"52","author":"C Ballarin","year":"2014","unstructured":"Ballarin, C.: Locales: a module system for mathematical theories. J. Autom. Reason. 52(2), 123\u2013153 (2014). https:\/\/doi.org\/10.1007\/s10817-013-9284-7","journal-title":"J. Autom. Reason."},{"key":"8_CR5","doi-asserted-by":"publisher","unstructured":"Baluta, T., Shen, S., Shinde, S., Meel, K.S., Saxena, P.: Quantitative verification of neural networks and its security applications. In: Cavallaro, L., Kinder, J., Wang, X., Katz, J. (eds.) CCS, pp. 1249\u20131264. ACM (2019). https:\/\/doi.org\/10.1145\/3319535.3354245","DOI":"10.1145\/3319535.3354245"},{"issue":"3","key":"8_CR6","doi-asserted-by":"publisher","first-page":"485","DOI":"10.1007\/s10817-018-09502-y","volume":"64","author":"H Barbosa","year":"2020","unstructured":"Barbosa, H., Blanchette, J.C., Fleury, M., Fontaine, P.: Scalable fine-grained proofs for formula processing. J. Autom. Reason. 64(3), 485\u2013510 (2020). https:\/\/doi.org\/10.1007\/s10817-018-09502-y","journal-title":"J. Autom. Reason."},{"key":"8_CR7","doi-asserted-by":"publisher","unstructured":"Beyersdorff, O., Hoffmann, T., Spachmann, L.N.: Proof complexity of propositional model counting. In: Mahajan, M., Slivovsky, F. (eds.) SAT. LIPIcs, vol.\u00a0271, pp. 2:1\u20132:18. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2023). https:\/\/doi.org\/10.4230\/LIPICS.SAT.2023.2","DOI":"10.4230\/LIPICS.SAT.2023.2"},{"key":"8_CR8","unstructured":"Biere, A., Fazekas, K., Fleury, M., Heisinger, M.: CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT competition 2020. In: Balyo, T., Froleyks, N., Heule, M., Iser, M., J\u00e4rvisalo, M., Suda, M. (eds.) Proceedings\u00a0of SAT Competition 2020 \u2013 Solver and Benchmark Descriptions. Department of Computer Science Report Series B, vol. B-2020-1, pp. 51\u201353. University of Helsinki (2020)"},{"key":"8_CR9","doi-asserted-by":"publisher","unstructured":"Bryant, R.E.: TBUDDY: a proof-generating BDD package. In: Griggio, A., Rungta, N. (eds.) FMCAD, pp. 49\u201358. TU Wien Academic Press (2022).https:\/\/doi.org\/10.34727\/2022\/ISBN.978-3-85448-053-2_10","DOI":"10.34727\/2022\/ISBN.978-3-85448-053-2_10"},{"key":"8_CR10","doi-asserted-by":"publisher","unstructured":"Bryant, R.E., Nawrocki, W., Avigad, J., Heule, M.J.H.: Certified knowledge compilation with application to verified model counting. In: Mahajan, M., Slivovsky, F. (eds.) SAT. LIPIcs, vol.\u00a0271, pp. 6:1\u20136:20. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2023). https:\/\/doi.org\/10.4230\/LIPIcs.SAT.2023.6","DOI":"10.4230\/LIPIcs.SAT.2023.6"},{"key":"8_CR11","doi-asserted-by":"publisher","unstructured":"Chakraborty, S., Fremont, D.J., Meel, K.S., Seshia, S.A., Vardi, M.Y.: Distribution-aware sampling and weighted model counting for SAT. In: Brodley, C.E., Stone, P. (eds.) AAAI, pp. 1722\u20131730. AAAI Press (2014). https:\/\/doi.org\/10.1609\/AAAI.V28I1.8990","DOI":"10.1609\/AAAI.V28I1.8990"},{"key":"8_CR12","unstructured":"Chakraborty, S., Meel, K.S., Vardi, M.Y.: Algorithmic improvements in approximate counting for probabilistic inference: from linear to logarithmic SAT calls. In: Kambhampati, S. (ed.) IJCAI, pp. 3569\u20133576. IJCAI\/AAAI Press (2016). http:\/\/www.ijcai.org\/Abstract\/16\/503"},{"key":"8_CR13","doi-asserted-by":"publisher","unstructured":"Chakraborty, S., Meel, K.S., Vardi, M.Y.: Approximate model counting. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability - Second Edition, Frontiers in Artificial Intelligence and Applications, vol.\u00a0336, pp. 1015\u20131045. IOS Press (2021). https:\/\/doi.org\/10.3233\/FAIA201010","DOI":"10.3233\/FAIA201010"},{"key":"8_CR14","doi-asserted-by":"publisher","unstructured":"Due\u00f1as-Osorio, L., Meel, K.S., Paredes, R., Vardi, M.Y.: Counting-based reliability estimation for power-transmission grids. In: Singh, S., Markovitch, S. (eds.) AAAI, pp. 4488\u20134494. AAAI Press (2017). https:\/\/doi.org\/10.1609\/AAAI.V31I1.11178","DOI":"10.1609\/AAAI.V31I1.11178"},{"issue":"5","key":"8_CR15","doi-asserted-by":"publisher","first-page":"879","DOI":"10.1007\/s10817-020-09545-0","volume":"64","author":"M Eberl","year":"2020","unstructured":"Eberl, M., Haslbeck, M.W., Nipkow, T.: Verified analysis of random binary tree structures. J. Autom. Reason. 64(5), 879\u2013910 (2020). https:\/\/doi.org\/10.1007\/s10817-020-09545-0","journal-title":"J. Autom. Reason."},{"key":"8_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/978-3-662-46669-8_4","volume-title":"Programming Languages and Systems","author":"M Eberl","year":"2015","unstructured":"Eberl, M., H\u00f6lzl, J., Nipkow, T.: A verified compiler for probability density functions. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 80\u2013104. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46669-8_4"},{"key":"8_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502\u2013518. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24605-3_37"},{"key":"8_CR18","unstructured":"Ermon, S., Gomes, C.P., Sabharwal, A., Selman, B.: Taming the curse of dimensionality: discrete integration by hashing and optimization. In: ICML. PMLR, vol.\u00a028, pp. 334\u2013342. PMLR (2013). http:\/\/proceedings.mlr.press\/v28\/ermon13.html"},{"key":"8_CR19","doi-asserted-by":"publisher","unstructured":"Fichte, J.K., Hecher, M., Roland, V.: Proofs for propositional model counting. In: Meel, K.S., Strichman, O. (eds.) SAT. LIPIcs, vol.\u00a0236, pp. 30:1\u201330:24. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2022). https:\/\/doi.org\/10.4230\/LIPICS.SAT.2022.30","DOI":"10.4230\/LIPICS.SAT.2022.30"},{"key":"8_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/978-3-030-20652-9_10","volume-title":"NASA Formal Methods","author":"M Fleury","year":"2019","unstructured":"Fleury, M.: Optimizing a verified SAT solver. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2019. LNCS, vol. 11460, pp. 148\u2013165. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-20652-9_10"},{"key":"8_CR21","unstructured":"FRATxor and cakexlrup tool repository. https:\/\/github.com\/meelgroup\/frat-xor"},{"key":"8_CR22","doi-asserted-by":"publisher","unstructured":"Gittis, A., Vin, E., Fremont, D.J.: Randomized synthesis for diversity and cost constraints with control improvisation. In: Shoham, S., Vizel, Y. (eds.) CAV. LNCS, vol. 13372, pp. 526\u2013546. Springer, Heidelberg (2022). https:\/\/doi.org\/10.1007\/978-3-031-13188-2_26","DOI":"10.1007\/978-3-031-13188-2_26"},{"key":"8_CR23","doi-asserted-by":"publisher","unstructured":"Gocht, S., McCreesh, C., Myreen, M.O., Nordstr\u00f6m, J., Oertel, A., Tan, Y.K.: End-to-end verification for subgraph solving. In: Wooldridge, M.J., Dy, J.G., Natarajan, S. (eds.) AAAI, pp. 8038\u20138047. AAAI Press (2024). https:\/\/doi.org\/10.1609\/AAAI.V38I8.28642","DOI":"10.1609\/AAAI.V38I8.28642"},{"key":"8_CR24","doi-asserted-by":"publisher","unstructured":"Gocht, S., Nordstr\u00f6m, J.: Certifying parity reasoning efficiently using pseudo-Boolean proofs. In: AAAI, pp. 3768\u20133777. AAAI Press (2021). https:\/\/doi.org\/10.1609\/AAAI.V35I5.16494","DOI":"10.1609\/AAAI.V35I5.16494"},{"key":"8_CR25","doi-asserted-by":"crossref","unstructured":"Gomes, C.P., Sabharwal, A., Selman, B.: Near-uniform sampling of combinatorial spaces using XOR constraints. In: Sch\u00f6lkopf, B., Platt, J.C., Hofmann, T. (eds.) NIPS, pp. 481\u2013488. MIT Press (2006)","DOI":"10.7551\/mitpress\/7503.003.0065"},{"key":"8_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/978-3-030-53291-8_16","volume-title":"Computer Aided Verification","author":"K Gopinathan","year":"2020","unstructured":"Gopinathan, K., Sergey, I.: Certifying certainty and uncertainty in approximate membership query structures. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12225, pp. 279\u2013303. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_16"},{"key":"8_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/978-3-319-66107-0_18","volume-title":"Interactive Theorem Proving","author":"M Heule","year":"2017","unstructured":"Heule, M., Hunt, W., Kaufmann, M., Wetzler, N.: Efficient, verified checking of propositional proofs. In: Ayala-Rinc\u00f3n, M., Mu\u00f1oz, C.A. (eds.) ITP 2017. LNCS, vol. 10499, pp. 269\u2013284. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66107-0_18"},{"key":"8_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/978-3-319-22102-1_13","volume-title":"Interactive Theorem Proving","author":"J H\u00f6lzl","year":"2015","unstructured":"H\u00f6lzl, J., Lochbihler, A., Traytel, D.: A formalized hierarchy of probabilistic system types. In: Urban, C., Zhang, X. (eds.) ITP 2015. LNCS, vol. 9236, pp. 203\u2013220. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-22102-1_13"},{"key":"8_CR29","doi-asserted-by":"publisher","unstructured":"Hurd, J.: Formal verification of probabilistic algorithms. Technical Report. UCAM-CL-TR-566, University of Cambridge, Computer Laboratory (2003). https:\/\/doi.org\/10.48456\/tr-566","DOI":"10.48456\/tr-566"},{"key":"8_CR30","doi-asserted-by":"publisher","unstructured":"Kan, S., Lin, A.W., R\u00fcmmer, P., Schrader, M.: CertiStr: a certified string solver. In: Popescu, A., Zdancewic, S. (eds.) CPP, pp. 210\u2013224. ACM (2022) https:\/\/doi.org\/10.1145\/3497775.3503691","DOI":"10.1145\/3497775.3503691"},{"key":"8_CR31","doi-asserted-by":"publisher","unstructured":"Karayel, E.: Formalization of randomized approximation algorithms for frequency moments. In: Andronick, J., de\u00a0Moura, L. (eds.) ITP. LIPIcs, vol.\u00a0237, pp. 21:1\u201321:21. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2022). https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2022.21","DOI":"10.4230\/LIPIcs.ITP.2022.21"},{"key":"8_CR32","unstructured":"Karayel, E.: Formalization of randomized approximation algorithms for frequency moments. Archive of Formal Proofs (2022). https:\/\/isa-afp.org\/entries\/Frequency_Moments.html, Formal proof development"},{"key":"8_CR33","unstructured":"Karayel, E.: Median method. Archive of Formal Proofs (2022). https:\/\/isa-afp.org\/entries\/Median_Method.html, Formal proof development"},{"key":"8_CR34","unstructured":"Karayel, E.: Universal hash families. Archive of Formal Proofs (2022). https:\/\/isa-afp.org\/entries\/Universal_Hash_Families.html, Formal proof development"},{"key":"8_CR35","doi-asserted-by":"publisher","unstructured":"Kaufmann, D., Fleury, M., Biere, A.: The proof checkers Pacheck and Past\u00e8que for the practical algebraic calculus. In: FMCAD, pp. 264\u2013269. TU Wien Academic Press (2020).https:\/\/doi.org\/10.34727\/2020\/isbn.978-3-85448-042-6_34","DOI":"10.34727\/2020\/isbn.978-3-85448-042-6_34"},{"key":"8_CR36","doi-asserted-by":"publisher","unstructured":"Kumar, R., Myreen, M.O., Norrish, M., Owens, S.: CakeML: a verified implementation of ML. In: Jagannathan, S., Sewell, P. (eds.) POPL, pp. 179\u2013192. ACM (2014). https:\/\/doi.org\/10.1145\/2535838.2535841","DOI":"10.1145\/2535838.2535841"},{"issue":"3","key":"8_CR37","doi-asserted-by":"publisher","first-page":"513","DOI":"10.1007\/s10817-019-09525-z","volume":"64","author":"P Lammich","year":"2020","unstructured":"Lammich, P.: Efficient verified (UN)SAT certificate checking. J. Autom. Reason. 64(3), 513\u2013532 (2020). https:\/\/doi.org\/10.1007\/s10817-019-09525-z","journal-title":"J. Autom. Reason."},{"issue":"2","key":"8_CR38","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1016\/J.COSREV.2010.09.009","volume":"5","author":"RM McConnell","year":"2011","unstructured":"McConnell, R.M., Mehlhorn, K., N\u00e4her, S., Schweitzer, P.: Certifying algorithms. Comput. Sci. Rev. 5(2), 119\u2013161 (2011). https:\/\/doi.org\/10.1016\/J.COSREV.2010.09.009","journal-title":"Comput. Sci. Rev."},{"key":"8_CR39","doi-asserted-by":"publisher","unstructured":"Meel, K.S., Akshay, S.: Sparse hashing for scalable approximate model counting: theory and practice. In: Hermanns, H., Zhang, L., Kobayashi, N., Miller, D. (eds.) LICS, pp. 728\u2013741. ACM (2020). https:\/\/doi.org\/10.1145\/3373718.3394809","DOI":"10.1145\/3373718.3394809"},{"key":"8_CR40","doi-asserted-by":"publisher","unstructured":"Meel, K.S., Chakraborty, S., Akshay, S.: Auditable algorithms for approximate model counting. In: Wooldridge, M.J., Dy, J.G., Natarajan, S. (eds.) AAAI, pp. 10654\u201310661. AAAI Press (2024). https:\/\/doi.org\/10.1609\/AAAI.V38I9.28936","DOI":"10.1609\/AAAI.V38I9.28936"},{"key":"8_CR41","doi-asserted-by":"publisher","unstructured":"Meel, K.S., Soos, M.: Model counting and uniform sampling instances (2020). https:\/\/doi.org\/10.5281\/zenodo.3793090","DOI":"10.5281\/zenodo.3793090"},{"key":"8_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","year":"2002","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle\/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9"},{"issue":"3","key":"8_CR43","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/BF00248324","volume":"5","author":"LC Paulson","year":"1989","unstructured":"Paulson, L.C.: The foundation of a generic theorem prover. J. Autom. Reasoning 5(3), 363\u2013397 (1989). https:\/\/doi.org\/10.1007\/BF00248324","journal-title":"J. Autom. Reasoning"},{"key":"8_CR44","doi-asserted-by":"publisher","unstructured":"Pollitt, F., Fleury, M., Biere, A.: Faster LRAT checking than solving with CaDiCaL. In: Mahajan, M., Slivovsky, F. (eds.) SAT. LIPIcs, vol.\u00a0271, pp. 21:1\u201321:12. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2023). https:\/\/doi.org\/10.4230\/LIPICS.SAT.2023.21","DOI":"10.4230\/LIPICS.SAT.2023.21"},{"issue":"1\u20132","key":"8_CR45","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1016\/0004-3702(94)00092-1","volume":"82","author":"D Roth","year":"1996","unstructured":"Roth, D.: On the hardness of approximate reasoning. Artif. Intell. 82(1\u20132), 273\u2013302 (1996). https:\/\/doi.org\/10.1016\/0004-3702(94)00092-1","journal-title":"Artif. Intell."},{"key":"8_CR46","unstructured":"Sang, T., Beame, P., Kautz, H.A.: Performing Bayesian inference by weighted model counting. In: Veloso, M.M., Kambhampati, S. (eds.) AAAI, pp. 475\u2013482. AAAI Press\/The MIT Press (2005). http:\/\/www.aaai.org\/Library\/AAAI\/2005\/aaai05-075.php"},{"key":"8_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/978-3-030-81688-9_7","volume-title":"Computer Aided Verification","author":"X Shi","year":"2021","unstructured":"Shi, X., Fu, Y.-F., Liu, J., Tsai, M.-H., Wang, B.-Y., Yang, B.-Y.: CoqQFBV: a scalable certified SMT quantifier-free bit-vector solver. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12760, pp. 149\u2013171. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_7"},{"key":"8_CR48","doi-asserted-by":"publisher","unstructured":"Soos, M., Bryant, R.E.: Proof generation for CDCL solvers using Gauss-Jordan elimination. CoRR arxiv:2304.04292 (2023). https:\/\/doi.org\/10.48550\/ARXIV.2304.04292","DOI":"10.48550\/ARXIV.2304.04292"},{"key":"8_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1007\/978-3-030-53288-8_22","volume-title":"Computer Aided Verification","author":"M Soos","year":"2020","unstructured":"Soos, M., Gocht, S., Meel, K.S.: Tinted, detached, and lazy CNF-XOR solving and its applications to counting and sampling. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12224, pp. 463\u2013484. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53288-8_22"},{"key":"8_CR50","doi-asserted-by":"publisher","unstructured":"Soos, M., Meel, K.S.: BIRD: engineering an efficient CNF-XOR SAT solver and its applications to approximate model counting. In: AAAI, pp. 1592\u20131599. AAAI Press (2019). https:\/\/doi.org\/10.1609\/AAAI.V33I01.33011592","DOI":"10.1609\/AAAI.V33I01.33011592"},{"key":"8_CR51","doi-asserted-by":"publisher","unstructured":"Soos, M., Meel, K.S.: Arjun: An efficient independent support computation technique and its applications to counting and sampling. In: Mitra, T., Young, E.F.Y., Xiong, J. (eds.) ICCAD, pp. 71:1\u201371:9. ACM (2022). https:\/\/doi.org\/10.1145\/3508352.3549406","DOI":"10.1145\/3508352.3549406"},{"key":"8_CR52","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1007\/978-3-642-02777-2_24","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"M Soos","year":"2009","unstructured":"Soos, M., Nohl, K., Castelluccia, C.: Extending SAT solvers to cryptographic problems. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 244\u2013257. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02777-2_24"},{"issue":"2","key":"8_CR53","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/s10009-022-00690-y","volume":"25","author":"YK Tan","year":"2023","unstructured":"Tan, Y.K., Heule, M.J.H., Myreen, M.O.: Verified propagation redundancy and compositional UNSAT checking in CakeML. Int. J. Softw. Tools Technol. Transf. 25(2), 167\u2013184 (2023). https:\/\/doi.org\/10.1007\/s10009-022-00690-y","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"8_CR54","unstructured":"Tan, Y.K., Yang, J.: Approximate model counting. Archive of Formal Proofs (2024). https:\/\/isa-afp.org\/entries\/Approximate_Model_Counting.html, Formal proof development"},{"key":"8_CR55","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"452","DOI":"10.1007\/978-3-642-03359-9_31","volume-title":"Theorem Proving in Higher Order Logics","author":"R Thiemann","year":"2009","unstructured":"Thiemann, R., Sternagel, C.: Certification of termination proofs using CeTA. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 452\u2013468. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03359-9_31"},{"issue":"3","key":"8_CR56","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1137\/0208032","volume":"8","author":"LG Valiant","year":"1979","unstructured":"Valiant, L.G.: The complexity of enumeration and reliability problems. SIAM J. Comput. 8(3), 410\u2013421 (1979). https:\/\/doi.org\/10.1137\/0208032","journal-title":"SIAM J. Comput."},{"issue":"2","key":"8_CR57","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1145\/103135.103136","volume":"13","author":"MN Wegman","year":"1991","unstructured":"Wegman, M.N., Zadeck, F.K.: Constant propagation with conditional branches. ACM Trans. Program. Lang. Syst. 13(2), 181\u2013210 (1991). https:\/\/doi.org\/10.1145\/103135.103136","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"8_CR58","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"422","DOI":"10.1007\/978-3-319-09284-3_31","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"N Wetzler","year":"2014","unstructured":"Wetzler, N., Heule, M.J.H., Hunt, W.A.: DRAT-trim: efficient checking and trimming using expressive clausal proofs. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 422\u2013429. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-09284-3_31"},{"key":"8_CR59","doi-asserted-by":"publisher","unstructured":"Yang, J., Meel, K.S.: Engineering an efficient PB-XOR solver. In: Michel, L.D. (ed.) CP. LIPIcs, vol.\u00a0210, pp. 58:1\u201358:20. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2021https:\/\/doi.org\/10.4230\/LIPIcs.CP.2021.58","DOI":"10.4230\/LIPIcs.CP.2021.58"},{"key":"8_CR60","doi-asserted-by":"publisher","unstructured":"Yang, J., Meel, K.S.: Rounding meets approximate model counting. In: Enea, C., Lal, A. (eds.) CAV. LNCS, vol. 13965, pp. 132\u2013162. Springer, Heidelberg (2023). https:\/\/doi.org\/10.1007\/978-3-031-37703-7_7","DOI":"10.1007\/978-3-031-37703-7_7"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-65627-9_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T19:03:13Z","timestamp":1721934193000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-65627-9_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031656262","9783031656279"],"references-count":60,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-65627-9_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"26 July 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Montreal, QC","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 July 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 July 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"36","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}