{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T16:56:11Z","timestamp":1762448171429,"version":"build-2065373602"},"reference-count":31,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2025,7,11]],"date-time":"2025-07-11T00:00:00Z","timestamp":1752192000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,7,11]],"date-time":"2025-07-11T00:00:00Z","timestamp":1752192000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100001381","name":"National Research Foundation Singapore","doi-asserted-by":"publisher","award":["NRF-NRFFAI1-2019-0004","NRF-NRFFAI1-2019-0004"],"award-info":[{"award-number":["NRF-NRFFAI1-2019-0004","NRF-NRFFAI1-2019-0004"]}],"id":[{"id":"10.13039\/501100001381","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001459","name":"Ministry of Education - Singapore","doi-asserted-by":"publisher","award":["MOE-T2EP20121-0011","MOE-T2EP20121-0011"],"award-info":[{"award-number":["MOE-T2EP20121-0011","MOE-T2EP20121-0011"]}],"id":[{"id":"10.13039\/501100001459","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2025,11]]},"abstract":"Abstract<\/jats:title>\n \n The problem of model counting, also known as\n \n \n $$\\#\\textsf{SAT}$$<\/jats:tex-math>\n \n \n #<\/mml:mo>\n SAT<\/mml:mi>\n <\/mml:mrow>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>\n , is to compute the number of models or satisfying assignments of a given Boolean formula\n F<\/jats:italic>\n . Model counting is a fundamental problem in computer science with a wide range of applications. In recent years, there has been a growing interest in using hashing-based techniques for approximate model counting that provide\n \n \n $$(\\varepsilon , \\delta )$$<\/jats:tex-math>\n \n \n (<\/mml:mo>\n \u03b5<\/mml:mi>\n ,<\/mml:mo>\n \u03b4<\/mml:mi>\n )<\/mml:mo>\n <\/mml:mrow>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>\n -guarantees: i.e., the count returned is within a\n \n \n $$(1+\\varepsilon )$$<\/jats:tex-math>\n \n \n (<\/mml:mo>\n 1<\/mml:mn>\n +<\/mml:mo>\n \u03b5<\/mml:mi>\n )<\/mml:mo>\n <\/mml:mrow>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>\n -factor of the exact count with confidence at least\n \n \n $$1-\\delta$$<\/jats:tex-math>\n \n \n 1<\/mml:mn>\n -<\/mml:mo>\n \u03b4<\/mml:mi>\n <\/mml:mrow>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>\n . While hashing-based techniques attain reasonable scalability for large enough values of\n \n \n $$\\delta$$<\/jats:tex-math>\n \n \u03b4<\/mml:mi>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>\n , their scalability is severely impacted for smaller values of\n \n \n $$\\delta$$<\/jats:tex-math>\n \n \u03b4<\/mml:mi>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>\n , thereby preventing their adoption in application domains that require estimates with high confidence. The primary contribution of this paper is to address the Achilles heel of hashing-based techniques: we propose a novel approach based on\n rounding<\/jats:italic>\n that allows us to achieve a significant reduction in runtime for smaller values of\n \n \n $$\\delta$$<\/jats:tex-math>\n \n \u03b4<\/mml:mi>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>\n . The resulting counter, called\n \n \n $$\\textsf{ApproxMC6}$$<\/jats:tex-math>\n \n \n ApproxMC<\/mml:mi>\n 6<\/mml:mn>\n <\/mml:mrow>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>\n , achieves a substantial runtime performance improvement over the current state-of-the-art counter,\n \n \n $$\\textsf{ApproxMC}$$<\/jats:tex-math>\n \n ApproxMC<\/mml:mi>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>\n . In particular, our extensive evaluation over a benchmark suite consisting of 1890 instances shows\n \n \n $$\\textsf{ApproxMC6}$$<\/jats:tex-math>\n \n \n ApproxMC<\/mml:mi>\n 6<\/mml:mn>\n <\/mml:mrow>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>\n solves 204 more instances than\n \n \n $$\\textsf{ApproxMC}$$<\/jats:tex-math>\n \n ApproxMC<\/mml:mi>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>\n , and achieves a\n \n \n $$4\\times$$<\/jats:tex-math>\n \n \n 4<\/mml:mn>\n \u00d7<\/mml:mo>\n <\/mml:mrow>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>\n speedup over\n \n \n $$\\textsf{ApproxMC}$$<\/jats:tex-math>\n \n ApproxMC<\/mml:mi>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>\n .\n <\/jats:p>","DOI":"10.1007\/s10703-025-00481-6","type":"journal-article","created":{"date-parts":[[2025,7,11]],"date-time":"2025-07-11T19:26:06Z","timestamp":1752261966000},"page":"189-221","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Rounding meets approximate model counting"],"prefix":"10.1007","volume":"67","author":[{"given":"Jiong","family":"Yang","sequence":"first","affiliation":[]},{"given":"Kuldeep S.","family":"Meel","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,7,11]]},"reference":[{"key":"481_CR1","doi-asserted-by":"crossref","unstructured":"Alur R, Bodik R, Juniwal G, et\u00a0al (2013) Syntax-guided synthesis. In: Proc of FMCAD","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"481_CR2","doi-asserted-by":"crossref","unstructured":"Baluta T, Shen S, Shine S, et\u00a0al (2019) Quantitative verification of neural networks and its security applications. In: Proc of CCS","DOI":"10.1145\/3319535.3354245"},{"key":"481_CR3","unstructured":"Beck G, Zinkus M, Green M (2020) Automating the development of chosen ciphertext attacks. In: Proc. of USENIX Security"},{"key":"481_CR4","doi-asserted-by":"crossref","unstructured":"Carter JL, Wegman MN (1977) Universal classes of hash functions. J Comput Syst Sci","DOI":"10.1145\/800105.803400"},{"key":"481_CR5","doi-asserted-by":"crossref","unstructured":"Chakraborty S, Meel KS, Vardi MY (2013) A scalable approximate model counter. In: Proc of CP","DOI":"10.1007\/978-3-642-40627-0_18"},{"key":"481_CR6","doi-asserted-by":"crossref","unstructured":"Chakraborty S, Fremont DJ, Meel KS, et\u00a0al (2014) Distribution-aware sampling and weighted model counting for SAT. In: Proc of AAAI","DOI":"10.1609\/aaai.v28i1.8990"},{"key":"481_CR7","doi-asserted-by":"crossref","unstructured":"Chakraborty S, Meel KS, Mistry R, et\u00a0al (2016a) Approximate probabilistic inference via word-level counting. In: Proc of AAAI","DOI":"10.1609\/aaai.v30i1.10416"},{"key":"481_CR8","unstructured":"Chakraborty S, Meel KS, Vardi MY (2016b) Algorithmic improvements in approximate counting for probabilistic inference: From linear to logarithmic SAT calls. In: Proc of IJCAI"},{"key":"481_CR9","doi-asserted-by":"crossref","unstructured":"Duenas-Osorio L, Meel KS, Paredes R, et\u00a0al (2017) Counting-based reliability estimation for power-transmission grids. In: Proc of AAAI","DOI":"10.1609\/aaai.v31i1.11178"},{"key":"481_CR10","unstructured":"Ermon S, Gomes CP, Sabharwal A, et\u00a0al (2013a) Embed and project: Discrete sampling with universal hashing. In: Proc of NeurIPS"},{"key":"481_CR11","unstructured":"Ermon S, Gomes CP, Sabharwal A, et\u00a0al (2013b) Taming the curse of dimensionality: Discrete integration by hashing and optimization. In: Proc of ICML"},{"key":"481_CR12","doi-asserted-by":"crossref","unstructured":"Fichte JK, Hecher M, Hamiti F (2021) The model counting competition 2020. ACM J Exp Algorithmics","DOI":"10.1145\/3459080"},{"key":"481_CR13","doi-asserted-by":"crossref","unstructured":"Gittis A, Vin E, Fremont DJ (2022) Randomized synthesis for diversity and cost constraints with control improvisation. In: Proc of CAV","DOI":"10.1007\/978-3-031-13188-2_26"},{"key":"481_CR14","unstructured":"Gomes CP, Sabharwal A, Selman B (2006) Model counting: A new strategy for obtaining good bounds. In: Proc of AAAI"},{"key":"481_CR15","unstructured":"Hecher M, Fichte JK (2021) Model counting competition 2021. https:\/\/mccompetition.org\/2021\/mc_description"},{"key":"481_CR16","unstructured":"Hecher M, Fichte JK (2022) Model counting competition 2022. https:\/\/mccompetition.org\/2022\/mc_description"},{"key":"481_CR17","doi-asserted-by":"crossref","unstructured":"Ivrii A, Malik S, Meel KS, et\u00a0al (2016) On computing minimal independent support and its applications to sampling and counting. Constraints","DOI":"10.1007\/s10601-015-9204-z"},{"key":"481_CR18","doi-asserted-by":"crossref","unstructured":"Meel KS, Akshay S (2020) Sparse hashing for scalable approximate model counting: Theory and practice. In: Proc of LICS","DOI":"10.1145\/3373718.3394809"},{"key":"481_CR19","unstructured":"Meel KS, Vardi MY, Chakraborty S, et\u00a0al (2016) Constrained sampling and counting: Universal hashing meets sat solving. In: Proc of Workshop on Beyond NP(BNP)"},{"key":"481_CR20","doi-asserted-by":"crossref","unstructured":"Roth D (1996) On the hardness of approximate reasoning. Artificial Intelligence","DOI":"10.1016\/0004-3702(94)00092-1"},{"key":"481_CR21","unstructured":"Sang T, Bearne P, Kautz H (2005) Performing Bayesian inference by weighted model counting. In: Proc of AAAI"},{"key":"481_CR22","doi-asserted-by":"crossref","unstructured":"Soos M, Meel KS (2019) Bird: Engineering an efficient CNF-XOR sat solver and its applications to approximate model counting. In: Proc of AAAI","DOI":"10.1609\/aaai.v33i01.33011592"},{"key":"481_CR23","doi-asserted-by":"crossref","unstructured":"Soos M, Meel KS (2022) Arjun: An efficient independent support computation technique and its applications to counting and sampling. In: Proc of ICCAD","DOI":"10.1145\/3508352.3549406"},{"key":"481_CR24","doi-asserted-by":"crossref","unstructured":"Soos M, Gocht S, Meel KS (2020) Tinted, detached, and lazy cnf-xor solving and its applications to counting and sampling. In: Proc of CAV","DOI":"10.1007\/978-3-030-53288-8_22"},{"key":"481_CR25","doi-asserted-by":"crossref","unstructured":"Stockmeyer L (1983) The complexity of approximate counting. In: Proc of STOC","DOI":"10.1145\/800061.808740"},{"key":"481_CR26","doi-asserted-by":"crossref","unstructured":"Teuber S, Weigl A (2021) Quantifying software reliability via model-counting. In: Proc of QEST","DOI":"10.1007\/978-3-030-85172-9_4"},{"key":"481_CR27","doi-asserted-by":"crossref","unstructured":"Toda S (1989) On the computational power of pp and (+)p. In: Proc of FOCS","DOI":"10.1109\/SFCS.1989.63527"},{"key":"481_CR28","doi-asserted-by":"crossref","unstructured":"Valiant LG (1979) The complexity of enumeration and reliability problems. SIAM J Comput","DOI":"10.1137\/0208032"},{"key":"481_CR29","unstructured":"Yang J, Meel KS (2021) Engineering an efficient pb-xor solver. In: Proc of CP"},{"key":"481_CR30","doi-asserted-by":"crossref","unstructured":"Yang J, Meel KS (2023) Rounding meets approximate model counting. In: Proc of CAV","DOI":"10.1007\/978-3-031-37703-7_7"},{"key":"481_CR31","doi-asserted-by":"crossref","unstructured":"Yang J, Chakraborty S, Meel KS (2022) Projected model counting: Beyond independent support. In: Proc of ATVA","DOI":"10.1007\/978-3-031-19992-9_11"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-025-00481-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-025-00481-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-025-00481-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T16:54:08Z","timestamp":1762448048000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-025-00481-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,7,11]]},"references-count":31,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2025,11]]}},"alternative-id":["481"],"URL":"https:\/\/doi.org\/10.1007\/s10703-025-00481-6","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2025,7,11]]},"assertion":[{"value":"15 March 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"12 May 2025","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"11 July 2025","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"}}]}}