{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,19]],"date-time":"2026-02-19T08:14:25Z","timestamp":1771488865612,"version":"3.50.1"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031377020","type":"print"},{"value":"9783031377037","type":"electronic"}],"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,7,18]],"date-time":"2023-07-18T00:00:00Z","timestamp":1689638400000},"content-version":"vor","delay-in-days":198,"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>The problem of model counting, also known as <jats:inline-formula><jats:tex-math>$$\\#\\textsf{SAT}$$<\/jats:tex-math><\/jats:inline-formula>, is to compute the number of models or satisfying assignments of a given Boolean formula <jats:italic>F<\/jats:italic>. 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 <jats:inline-formula><jats:tex-math>$$(\\varepsilon , \\delta )$$<\/jats:tex-math><\/jats:inline-formula>-guarantees: i.e., the count returned is within a <jats:inline-formula><jats:tex-math>$$(1+\\varepsilon )$$<\/jats:tex-math><\/jats:inline-formula>-factor of the exact count with confidence at least <jats:inline-formula><jats:tex-math>$$1-\\delta $$<\/jats:tex-math><\/jats:inline-formula>. While hashing-based techniques attain reasonable scalability for large enough values of <jats:inline-formula><jats:tex-math>$$\\delta $$<\/jats:tex-math><\/jats:inline-formula>, their scalability is severely impacted for smaller values of <jats:inline-formula><jats:tex-math>$$\\delta $$<\/jats:tex-math><\/jats:inline-formula>, thereby preventing their adoption in application domains that require estimates with high confidence.<\/jats:p><jats:p>The primary contribution of this paper is to address the Achilles heel of hashing-based techniques: we propose a novel approach based on <jats:italic>rounding<\/jats:italic> that allows us to achieve a significant reduction in runtime for smaller values of <jats:inline-formula><jats:tex-math>$$\\delta $$<\/jats:tex-math><\/jats:inline-formula>. The resulting counter, called <jats:inline-formula><jats:tex-math>$$\\textsf{ApproxMC6}$$<\/jats:tex-math><\/jats:inline-formula> (The resulting tool <jats:inline-formula><jats:tex-math>$$\\textsf{ApproxMC6}$$<\/jats:tex-math><\/jats:inline-formula> is available open-source at <jats:ext-link xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" ext-link-type=\"uri\" xlink:href=\"https:\/\/github.com\/meelgroup\/approxmc\">https:\/\/github.com\/meelgroup\/approxmc<\/jats:ext-link>), achieves a substantial runtime performance improvement over the current state-of-the-art counter, <jats:inline-formula><jats:tex-math>$$\\textsf{ApproxMC}$$<\/jats:tex-math><\/jats:inline-formula>. In particular, our extensive evaluation over a benchmark suite consisting of 1890 instances shows <jats:inline-formula><jats:tex-math>$$\\textsf{ApproxMC6}$$<\/jats:tex-math><\/jats:inline-formula> solves 204 more instances than <jats:inline-formula><jats:tex-math>$$\\textsf{ApproxMC}$$<\/jats:tex-math><\/jats:inline-formula>, and achieves a <jats:inline-formula><jats:tex-math>$$4\\times $$<\/jats:tex-math><\/jats:inline-formula> speedup over <jats:inline-formula><jats:tex-math>$$\\textsf{ApproxMC}$$<\/jats:tex-math><\/jats:inline-formula>.<\/jats:p>","DOI":"10.1007\/978-3-031-37703-7_7","type":"book-chapter","created":{"date-parts":[[2023,7,17]],"date-time":"2023-07-17T17:02:15Z","timestamp":1689613335000},"page":"132-162","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Rounding Meets Approximate Model Counting"],"prefix":"10.1007","author":[{"given":"Jiong","family":"Yang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kuldeep S.","family":"Meel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,7,18]]},"reference":[{"key":"7_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R., et al.: Syntax-guided synthesis. In: Proceedings of FMCAD (2013)","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"7_CR2","doi-asserted-by":"crossref","unstructured":"Baluta, T., Shen, S., Shine, S., Meel, K.S., Saxena, P.: Quantitative verification of neural networks and its security applications. In: Proceedings of CCS (2019)","DOI":"10.1145\/3319535.3354245"},{"key":"7_CR3","unstructured":"Beck, G., Zinkus, M., Green, M.: Automating the development of chosen ciphertext attacks. In: Proceedings of USENIX Security (2020)"},{"key":"7_CR4","doi-asserted-by":"crossref","unstructured":"Carter, J.L., Wegman, M.N.: Universal classes of hash functions. J. Comput. Syst. Sci. (1977)","DOI":"10.1145\/800105.803400"},{"key":"7_CR5","doi-asserted-by":"crossref","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: Proceedings of AAAI (2014)","DOI":"10.1609\/aaai.v28i1.8990"},{"key":"7_CR6","doi-asserted-by":"crossref","unstructured":"Chakraborty, S., Meel, K.S., Mistry, R., Vardi, M.Y.: Approximate probabilistic inference via word-level counting. In: Proceedings of AAAI (2016)","DOI":"10.1609\/aaai.v30i1.10416"},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"Chakraborty, S., Meel, K.S., Vardi, M.Y.: A scalable approximate model counter. In: Proceedings of CP (2013)","DOI":"10.1007\/978-3-642-40627-0_18"},{"key":"7_CR8","unstructured":"Chakraborty, S., Meel, K.S., Vardi, M.Y.: Algorithmic improvements in approximate counting for probabilistic inference: from linear to logarithmic SAT calls. In: Proceedings of IJCAI (2016)"},{"key":"7_CR9","doi-asserted-by":"crossref","unstructured":"Duenas-Osorio, L., Meel, K.S., Paredes, R., Vardi, M.Y.: Counting-based reliability estimation for power-transmission grids. In: Proceedings of AAAI (2017)","DOI":"10.1609\/aaai.v31i1.11178"},{"key":"7_CR10","unstructured":"Ermon, S., Gomes, C.P., Sabharwal, A., Selman, B.: Embed and project: discrete sampling with universal hashing. In: Proceedings of NeurIPS (2013)"},{"key":"7_CR11","unstructured":"Ermon, S., Gomes, C.P., Sabharwal, A., Selman, B.: Taming the curse of dimensionality: discrete integration by hashing and optimization. In: Proceedings of ICML (2013)"},{"key":"7_CR12","doi-asserted-by":"crossref","unstructured":"Fichte, J.K., Hecher, M., Hamiti, F.: The model counting competition 2020. ACM J. Exp. Algorithmics (2021)","DOI":"10.1145\/3459080"},{"key":"7_CR13","doi-asserted-by":"crossref","unstructured":"Gittis, A., Vin, E., Fremont, D.J.: Randomized synthesis for diversity and cost constraints with control improvisation. In: Proceedings of CAV (2022)","DOI":"10.1007\/978-3-031-13188-2_26"},{"key":"7_CR14","unstructured":"Gomes, C.P., Sabharwal, A., Selman, B.: Model counting: a new strategy for obtaining good bounds. In: Proceedings of AAAI (2006)"},{"key":"7_CR15","unstructured":"Hecher, M., Fichte, J.K.: Model counting competition 2021 (2021). https:\/\/www.mccompetition.org\/2021\/mc_description"},{"key":"7_CR16","unstructured":"Hecher, M., Fichte, J.K.: Model counting competition 2022 (2022). https:\/\/mccompetition.org\/2022\/mc_description"},{"key":"7_CR17","doi-asserted-by":"crossref","unstructured":"Ivrii, A., Malik, S., Meel, K.S., Vardi, M.Y.: On computing minimal independent support and its applications to sampling and counting. Constraints (2016)","DOI":"10.1007\/s10601-015-9204-z"},{"key":"7_CR18","doi-asserted-by":"crossref","unstructured":"Meel, K.S., Akshay, S.: Sparse hashing for scalable approximate model counting: theory and practice. In: Proceedings of LICS (2020)","DOI":"10.1145\/3373718.3394809"},{"key":"7_CR19","unstructured":"Meel, K.S., et al.: Constrained sampling and counting: universal hashing meets sat solving. In: Proceedings of Workshop on Beyond NP(BNP) (2016)"},{"key":"7_CR20","unstructured":"Roth, D.: On the hardness of approximate reasoning. Artif. Intell. (1996)"},{"key":"7_CR21","unstructured":"Sang, T., Bearne, P., Kautz, H.: Performing Bayesian inference by weighted model counting. In: Proceedings of AAAI (2005)"},{"key":"7_CR22","doi-asserted-by":"crossref","unstructured":"Soos, M., Gocht, S., Meel, K.S.: Tinted, detached, and lazy CNF-XOR solving and its applications to counting and sampling. In: Proceedings of CAV (2020)","DOI":"10.1007\/978-3-030-53288-8_22"},{"key":"7_CR23","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: Proceedings of AAAI (2019)","DOI":"10.1609\/aaai.v33i01.33011592"},{"key":"7_CR24","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: Proceedings of ICCAD (2022)","DOI":"10.1145\/3508352.3549406"},{"key":"7_CR25","doi-asserted-by":"crossref","unstructured":"Stockmeyer, L.: The complexity of approximate counting. In: Proceedings of STOC (1983)","DOI":"10.1145\/800061.808740"},{"key":"7_CR26","doi-asserted-by":"crossref","unstructured":"Teuber, S., Weigl, A.: Quantifying software reliability via model-counting. In: Proceedings of QEST (2021)","DOI":"10.1007\/978-3-030-85172-9_4"},{"key":"7_CR27","doi-asserted-by":"crossref","unstructured":"Toda, S.: On the computational power of PP and (+)P. In: Proceedings of FOCS (1989)","DOI":"10.1109\/SFCS.1989.63527"},{"key":"7_CR28","doi-asserted-by":"crossref","unstructured":"Valiant, L.G.: The complexity of enumeration and reliability problems. SIAM J. Comput. (1979)","DOI":"10.1137\/0208032"},{"key":"7_CR29","doi-asserted-by":"crossref","unstructured":"Yang, J., Chakraborty, S., Meel, K.S.: Projected model counting: beyond independent support. In: Proceedings of ATVA (2022)","DOI":"10.1007\/978-3-031-19992-9_11"},{"key":"7_CR30","unstructured":"Yang, J., Meel, K.S.: Engineering an efficient PB-XOR solver. In: Proceedings of CP (2021)"}],"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-37703-7_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,26]],"date-time":"2023-08-26T11:03:20Z","timestamp":1693047800000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-37703-7_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031377020","9783031377037"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-37703-7_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"18 July 2023","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":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","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":"17 July 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 July 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"35","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.i-cav.org\/2023\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"hotcrp","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"261","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"67","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"26% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}