{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,17]],"date-time":"2026-08-17T15:17:16Z","timestamp":1786979836206,"version":"build-2736575974"},"reference-count":42,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2026,6,25]],"date-time":"2026-06-25T00:00:00Z","timestamp":1782345600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,6,25]],"date-time":"2026-06-25T00:00:00Z","timestamp":1782345600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"funder":[{"DOI":"10.13039\/501100000038","name":"Natural Sciences and Engineering Research Council of Canada","doi-asserted-by":"publisher","award":["RGPIN-2024-05956"],"award-info":[{"award-number":["RGPIN-2024-05956"]}],"id":[{"id":"10.13039\/501100000038","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001381","name":"National Research Foundation Singapore","doi-asserted-by":"publisher","award":["NRF-NRFFAI1- 2019-0004"],"award-info":[{"award-number":["NRF-NRFFAI1- 2019-0004"]}],"id":[{"id":"10.13039\/501100001381","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2026,9]]},"DOI":"10.1007\/s00236-026-00535-0","type":"journal-article","created":{"date-parts":[[2026,6,25]],"date-time":"2026-06-25T11:29:29Z","timestamp":1782386969000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["CSB: A Counting and Sampling tool for Bit-vectors"],"prefix":"10.1007","volume":"63","author":[{"given":"Arijit","family":"Shaw","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Kuldeep S.","family":"Meel","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,6,25]]},"reference":[{"key":"535_CR1","doi-asserted-by":"crossref","unstructured":"Barbosa, H., Barrett, C., Brain, M., Kremer, G., Lachnitt, H., Mann, M., Mohamed, A., Mohamed, M., Niemetz, A., N\u00f6tzli, A., et\u00a0al.: cvc5: a versatile and industrial-strength smt solver. In: Proc. of TACAS (2022)","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"535_CR2","unstructured":"Barrett, C., Stump, A., Tinelli, C.: The smt-lib standard: version 2.0. In: Proc. of SMT Workshop, (2010)"},{"key":"535_CR3","doi-asserted-by":"crossref","unstructured":"Barrett, C., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Handbook of Satisfiability, (2021)","DOI":"10.3233\/FAIA201017"},{"key":"535_CR4","unstructured":"Beck, G., Zinkus, M., Green, M.: Automating the development of chosen ciphertext attacks. In: Proc. of USENIX Security, (2020)"},{"key":"535_CR5","doi-asserted-by":"crossref","unstructured":"Brummayer, R., Biere, A.: Boolector: An efficient SMT solver for bit-vectors and arrays. In: Proc. of TACAS, (2009)","DOI":"10.1007\/978-3-642-00768-2_16"},{"key":"535_CR6","unstructured":"Chakraborty, S., Meel, K.S., Vardi, M.Y.: Algorithmic improvements in approximate counting for probabilistic inference: from linear to logarithmic SAT calls. In: Proc. of IJCAI, (2016)"},{"key":"535_CR7","doi-asserted-by":"crossref","unstructured":"Chakraborty, S., Meel, K.S.: On testing of uniform samplers. In: Proc. of AAAI, (2019)","DOI":"10.1609\/aaai.v33i01.33017777"},{"key":"535_CR8","doi-asserted-by":"crossref","unstructured":"Chakraborty, S., Meel, K.S., Vardi, M.Y.: A scalable approximate model counter. In: Proc. of CP, (2013)","DOI":"10.1007\/978-3-642-40627-0_18"},{"key":"535_CR9","doi-asserted-by":"crossref","unstructured":"Chakraborty, S., Fremont, D.J., Meel, K.S., Seshia, S.A., Vardi, M.Y.: On parallel scalable uniform sat witness generation. In: Proc. of TACAS, (2015)","DOI":"10.1007\/978-3-662-46681-0_25"},{"key":"535_CR10","doi-asserted-by":"crossref","unstructured":"Chakraborty, S., Meel, K., Mistry, R., Vardi, M.: Approximate probabilistic inference via word-level counting. In: Proc. of AAAI, (2016)","DOI":"10.1609\/aaai.v30i1.10416"},{"key":"535_CR11","doi-asserted-by":"crossref","unstructured":"Chistikov, D., Dimitrova, R., Majumdar, R.: Approximate counting in SMT and value estimation for probabilistic programs. In: Proc. of TACAS, (2015)","DOI":"10.1007\/978-3-662-46681-0_26"},{"key":"535_CR12","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The mathsat5 SMT solver. In: Proc. of TACAS, (2013)","DOI":"10.1007\/978-3-642-36742-7_7"},{"key":"535_CR13","unstructured":"Dutra, R., Bachrach, J., Sen, K.: Smtsampler: efficient stimulus generation from complex smt constraints. In: Proc. of ICCAD, (2018)"},{"key":"535_CR14","doi-asserted-by":"crossref","unstructured":"Dutra, R., Bachrach, J., Sen, K.: Guidedsampler: coverage-guided sampling of smt solutions. In: Proc. of FMCAD, (2019)","DOI":"10.23919\/FMCAD.2019.8894251"},{"key":"535_CR15","unstructured":"E\u00e9n, N., Mishchenko, A., S\u00f6rensson, N.: Applying logic synthesis for speeding up SAT. In: Proc. of SAT, (2007)"},{"key":"535_CR16","doi-asserted-by":"publisher","DOI":"10.1145\/3459080","volume-title":"The model counting competition 2020","author":"JK Fichte","year":"2021","unstructured":"Fichte, J.K., Hecher, M., Hamiti, F.: The model counting competition 2020. J. Exp, Algorithmics (JEA) (2021)"},{"key":"535_CR17","doi-asserted-by":"publisher","unstructured":"Fichte, J., Hecher, M., Shaw, A.: Model Counting Competition 2024: Submitted Solvers. https:\/\/doi.org\/10.5281\/zenodo.14249109","DOI":"10.5281\/zenodo.14249109"},{"key":"535_CR18","unstructured":"Fichte, J., Hecher, M., Shaw, A.: Model counting competition data format (version 1.1) (2024)"},{"key":"535_CR19","unstructured":"Ganesh, V., Dill, D.L.: A decision procedure for bit-vectors and arrays. In: International Conference on Computer Aided Verification, Springer (2007)"},{"key":"535_CR20","doi-asserted-by":"crossref","unstructured":"Girol, G., Farinier, B., Bardin, S.: Not all bugs are created equal, but robust reachability can tell the difference. In: Proc. of CAV, (2021)","DOI":"10.1007\/978-3-030-81685-8_32"},{"key":"535_CR21","unstructured":"Golia, P., Soos, M., Chakraborty, S., Meel, K.S.: Designing samplers is easy: the boon of testers. In: Proc. of FMCAD, (2021)"},{"key":"535_CR22","unstructured":"Hecher, M., Fichte, J.K., Shaw, A.: Model Counting Competition 2025: Description. Model Counting Competition. https:\/\/mccompetition.org\/2025\/mc_description.html. Accessed 15 Dec 2025"},{"key":"535_CR23","doi-asserted-by":"crossref","unstructured":"Jha, S., Limaye, R., Seshia, S.A.: Beaver: engineering an efficient smt solver for bit-vector arithmetic. In: Proc. of CAV, (2009)","DOI":"10.1007\/978-3-642-02658-4_53"},{"key":"535_CR24","doi-asserted-by":"crossref","unstructured":"Kim, S., McCamant, S.: Bit-vector model counting using statistical estimation. In: Proc. of TACAS (2018)","DOI":"10.1007\/978-3-319-89960-2_8"},{"key":"535_CR25","unstructured":"Kim, S., McCamant, S.: Structural bit-vector model counting. In: SMT (2020)"},{"key":"535_CR26","unstructured":"Korhonen, T., J\u00e4rvisalo, M.: Integrating tree decompositions into decision heuristics of propositional model counters. In: Proc. of CP, (2021)"},{"key":"535_CR27","doi-asserted-by":"crossref","unstructured":"Kroening, D., Strichman, O.: Decision Procedures (2016)","DOI":"10.1007\/978-3-662-50497-0"},{"key":"535_CR28","doi-asserted-by":"crossref","unstructured":"Lagniez, J.-M., Marquis, P.: An improved decision-dnnf compiler. In: Proc. of IJCAI, (2017)","DOI":"10.24963\/ijcai.2017\/93"},{"key":"535_CR29","unstructured":"Lagniez, J.-M., Lonca, E., Marquis, P.: Improving model counting by leveraging definability. In: Proc. of IJCAI, (2016)"},{"key":"535_CR30","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2019.103229","volume-title":"Definability for model counting","author":"J-M Lagniez","year":"2020","unstructured":"Lagniez, J.-M., Lonca, E., Marquis, P.: Definability for model counting. Artif, Intell (2020)"},{"key":"535_CR31","unstructured":"Meel, K.S., Pote, Y.P., Chakraborty, S.: On testing of samplers. In: Proc. of NeurIPS, (2020)"},{"key":"535_CR32","doi-asserted-by":"crossref","unstructured":"Niemetz, A., Preiner, M.: Bitwuzla. In: Proc. of CAV, (2023)","DOI":"10.1007\/978-3-031-37703-7_1"},{"key":"535_CR33","doi-asserted-by":"crossref","unstructured":"Peled, M.I., Rothenberg, B.-C., Itzhaky, S.: Smt sampling via model-guided approximation. In: Proc. of FM, (2023)","DOI":"10.1007\/978-3-031-27481-7_6"},{"key":"535_CR34","doi-asserted-by":"crossref","unstructured":"Sharma, S., Roy, S., Soos, M., Meel, K.S.: Ganak: a scalable probabilistic exact model counter. In: Proc. of IJCAI, (2019)","DOI":"10.24963\/ijcai.2019\/163"},{"key":"535_CR35","doi-asserted-by":"crossref","unstructured":"Shaw, A., Meel, K.S.: Model counting in the wild. In: Proc. of KR, (2024)","DOI":"10.24963\/kr.2024\/71"},{"key":"535_CR36","doi-asserted-by":"crossref","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: International Conference on Computer Aided Verification, pp. 149\u2013171. Springer (2021)","DOI":"10.1007\/978-3-030-81688-9_7"},{"key":"535_CR37","doi-asserted-by":"crossref","unstructured":"Soos, M., Meel, K.S.: BIRD: engineering an efficient CNF-XOR SAT solver and its applications to approximate model counting. In: Proc. of AAAI, (2019)","DOI":"10.1609\/aaai.v33i01.33011592"},{"key":"535_CR38","doi-asserted-by":"crossref","unstructured":"Soos, M., Meel, K.S.: Arjun: an efficient independent support computation technique and its applications to counting and sampling. In: Proc. of ICCAD, (2022)","DOI":"10.1145\/3508352.3549406"},{"key":"535_CR39","doi-asserted-by":"crossref","unstructured":"Soos, M., Meel, K.S.: Engineering an efficient preprocessor for model counting. In: Proceedings of the 61st ACM\/IEEE Design Automation Conference, pp. 1\u20136. (2024)","DOI":"10.1145\/3649329.3658489"},{"key":"535_CR40","doi-asserted-by":"crossref","unstructured":"Soos, M., Meel, K.S.: Engineering an efficient probabilistic exact model counter. In: International Conference on Computer Aided Verification, pp. 72\u201391. Springer (2025)","DOI":"10.1007\/978-3-031-98682-6_5"},{"key":"535_CR41","doi-asserted-by":"crossref","unstructured":"Teuber, S., Weigl, A.: Quantifying software reliability via model-counting. In: Proc. of Quantitative Evaluation of Systems, (2021)","DOI":"10.1007\/978-3-030-85172-9_4"},{"key":"535_CR42","doi-asserted-by":"crossref","unstructured":"Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Automation of Reasoning, , Berlin (1983)","DOI":"10.1007\/978-3-642-81955-1_28"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-026-00535-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00236-026-00535-0","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-026-00535-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,25]],"date-time":"2026-06-25T11:30:20Z","timestamp":1782387020000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s00236-026-00535-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,6,25]]},"references-count":42,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2026,9]]}},"alternative-id":["535"],"URL":"https:\/\/doi.org\/10.1007\/s00236-026-00535-0","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,6,25]]},"assertion":[{"value":"2 December 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"14 May 2026","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"25 June 2026","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare no conflict of interest.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}}],"article-number":"23"}}