{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,4]],"date-time":"2026-06-04T05:26:21Z","timestamp":1780550781391,"version":"3.54.1"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783031166808","type":"print"},{"value":"9783031166815","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-031-16681-5_19","type":"book-chapter","created":{"date-parts":[[2022,9,16]],"date-time":"2022-09-16T03:41:24Z","timestamp":1663299684000},"page":"272-284","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["OuterCount: A First-Level Solution-Counter for\u00a0Quantified Boolean Formulas"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1038-3602","authenticated-orcid":false,"given":"Ankit","family":"Shukla","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7883-7749","authenticated-orcid":false,"given":"Sibylle","family":"M\u00f6hle","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8641-6661","authenticated-orcid":false,"given":"Manuel","family":"Kauers","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3267-4494","authenticated-orcid":false,"given":"Martina","family":"Seidl","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2022,9,17]]},"reference":[{"key":"19_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/978-3-319-24318-4_10","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2015","author":"RA Aziz","year":"2015","unstructured":"Aziz, R.A., Chu, G., Muise, C., Stuckey, P.: $$\\#\\exists $$SAT: projected model counting. In: Heule, M., Weaver, S. (eds.) SAT 2015. LNCS, vol. 9340, pp. 121\u2013137. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-24318-4_10"},{"key":"19_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-540-30557-6_14","volume-title":"Practical Aspects of Declarative Languages","author":"J Bailey","year":"2005","unstructured":"Bailey, J., Stuckey, P.J.: Discovery of minimal unsatisfiable subsets of constraints using hitting set dualization. In: Hermenegildo, M.V., Cabeza, D. (eds.) PADL 2005. LNCS, vol. 3350, pp. 174\u2013186. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-30557-6_14"},{"key":"19_CR3","doi-asserted-by":"crossref","unstructured":"Baluta, T., Shen, S., Shinde, S., Meel, K.S., Saxena, P.: Quantitative verification of neural networks and its security applications. In: CCS, pp. 1249\u20131264. ACM (2019)","DOI":"10.1145\/3319535.3354245"},{"key":"19_CR4","unstructured":"Bayardo Jr., R., Pehoushek, J.D.: Counting models using connected components. In: AAAI\/IAAI, pp. 157\u2013162. AAAI Press\/The MIT Press (2000)"},{"key":"19_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"370","DOI":"10.1007\/978-3-642-33386-6_29","volume-title":"Automated Technology for Verification and Analysis","author":"B Becker","year":"2012","unstructured":"Becker, B., Ehlers, R., Lewis, M., Marin, P.: ALLQBF solving by computational learning. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, pp. 370\u2013384. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33386-6_29"},{"key":"19_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/978-3-030-58475-7_3","volume-title":"Principles and Practice of Constraint Programming","author":"J Bend\u00edk","year":"2020","unstructured":"Bend\u00edk, J., \u010cern\u00e1, I.: Replication-guided enumeration of minimal unsatisfiable subsets. In: Simonis, H. (ed.) CP 2020. LNCS, vol. 12333, pp. 37\u201354. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-58475-7_3"},{"key":"19_CR7","doi-asserted-by":"crossref","unstructured":"Bend\u00edk, J., Cerna, I.: Rotation based MSS\/MCS enumeration. In: LPAR. EPIC, vol. 73, pp. 120\u2013137. EasyChair (2020)","DOI":"10.29007\/8btb"},{"key":"19_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/978-3-319-73721-8_4","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"F Biondi","year":"2018","unstructured":"Biondi, F., Enescu, M.A., Heuser, A., Legay, A., Meel, K.S., Quilbeuf, J.: Scalable approximation of quantitative information flow in programs. In: VMCAI 2018. LNCS, vol. 10747, pp. 71\u201393. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-73721-8_4"},{"key":"19_CR9","doi-asserted-by":"publisher","first-page":"457","DOI":"10.1613\/jair.601","volume":"10","author":"E Birnbaum","year":"1999","unstructured":"Birnbaum, E., Lozinskii, E.L.: The good old Davis-Putnam procedure helps counting models. J. Artif. Intell. Res. 10, 457\u2013477 (1999)","journal-title":"J. Artif. Intell. Res."},{"key":"19_CR10","unstructured":"Chakraborty, S., Meel, K.S., Vardi, M.Y.: Algorithmic improvements in approximate counting for probabilistic inference: From linear to logarithmic SAT calls. In: IJCAI, pp. 3569\u20133576. IJCAI\/AAAI Press (2016)"},{"key":"19_CR11","doi-asserted-by":"crossref","unstructured":"Chakraborty, S., Meel, K.S., Vardi, M.Y.: Chapter 26. Approximate model counting. In: Handbook of satisfiability, frontiers in artificial intelligence and applications, vol. 336, pp. 1015\u20131045. IOS Press (2021)","DOI":"10.3233\/FAIA201010"},{"key":"19_CR12","unstructured":"Diptarama, Yoshinaka, R., Shinohara, A.: QBF encoding of generalized tic-tac-toe. In: QBF@SAT. CEUR Workshop Proceedings, vol. 1719, pp. 14\u201326. CEUR-WS.org (2016)"},{"issue":"1","key":"19_CR13","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1016\/0304-3975(91)90315-S","volume":"81","author":"O Dubois","year":"1991","unstructured":"Dubois, O.: Counting the number of solutions for instances of satisfiability. Theor. Comput. Sci. 81(1), 49\u201364 (1991)","journal-title":"Theor. Comput. Sci."},{"key":"19_CR14","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"136","DOI":"10.1007\/978-3-540-72200-7_13","volume-title":"Logic Programming and Nonmonotonic Reasoning","author":"M Gebser","year":"2007","unstructured":"Gebser, M., Kaufmann, B., Neumann, A., Schaub, T.: Conflict-driven answer set enumeration. In: Baral, C., Brewka, G., Schlipf, J. (eds.) LPNMR 2007. LNCS (LNAI), vol. 4483, pp. 136\u2013148. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-72200-7_13"},{"key":"19_CR15","unstructured":"Giunchiglia, E., Narizzano, M., Tacchella, A.: Learning for quantified Boolean logic satisfiability. In: AAAI\/IAAI, pp. 649\u2013654. AAAI Press\/The MIT Press (2002)"},{"key":"19_CR16","doi-asserted-by":"crossref","unstructured":"Gomes, C.P., Sabharwal, A., Selman, B.: Chapter 25. Model counting. In: Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol.\u00a0336, pp. 993\u20131014. IOS Press, Amsterdam, Netherlands (2021)","DOI":"10.3233\/FAIA201009"},{"issue":"1","key":"19_CR17","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1145\/203610.203611","volume":"26","author":"LA Hemaspaandra","year":"1995","unstructured":"Hemaspaandra, L.A., Vollmer, H.: The satanic notations: counting classes beyond #P and other definitional adventures. SIGACT News 26(1), 2\u201313 (1995)","journal-title":"SIGACT News"},{"key":"19_CR18","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1613\/jair.4694","volume":"53","author":"M Heule","year":"2015","unstructured":"Heule, M., J\u00e4rvisalo, M., Lonsing, F., Seidl, M., Biere, A.: Clause elimination for SAT and QSAT. J. Artif. Intell. Res. 53, 127\u2013168 (2015)","journal-title":"J. Artif. Intell. Res."},{"key":"19_CR19","unstructured":"Hunter, A., Konieczny, S.: Measuring inconsistency through minimal inconsistent sets. In: KR, pp. 358\u2013366. AAAI Press (2008)"},{"key":"19_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/978-3-540-31980-1_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"HS Jin","year":"2005","unstructured":"Jin, H.S., Han, H.J., Somenzi, F.: Efficient conflict analysis for finding all satisfying assignments of a Boolean circuit. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 287\u2013300. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-31980-1_19"},{"issue":"6","key":"19_CR21","doi-asserted-by":"publisher","first-page":"1087","DOI":"10.1137\/0218073","volume":"18","author":"RE Ladner","year":"1989","unstructured":"Ladner, R.E.: Polynomial space counting problems. SIAM J. Comput. 18(6), 1087\u20131097 (1989)","journal-title":"SIAM J. Comput."},{"key":"19_CR22","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/3-540-45616-3_12","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"R Letz","year":"2002","unstructured":"Letz, R.: Lemma and model caching in decision procedures for quantified Boolean formulas. In: Egly, U., Ferm\u00fcller, C.G. (eds.) TABLEAUX 2002. LNCS (LNAI), vol. 2381, pp. 160\u2013175. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45616-3_12"},{"key":"19_CR23","unstructured":"Li, B., Hsiao, M.S., Sheng, S.: A novel SAT all-solutions solver for efficient preimage computation. In: DATE, pp. 272\u2013279. IEEE Computer Society (2004)"},{"key":"19_CR24","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1007\/978-3-319-63046-5_23","volume-title":"Automated Deduction \u2013 CADE 26","author":"F Lonsing","year":"2017","unstructured":"Lonsing, F., Egly, U.: DepQBF 6.0: a search-based qbf solver beyond traditional QCDCL. In: de Moura, L. (ed.) CADE 2017. LNCS (LNAI), vol. 10395, pp. 371\u2013384. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63046-5_23"},{"issue":"8","key":"19_CR25","doi-asserted-by":"publisher","first-page":"1659","DOI":"10.1016\/j.ijar.2014.06.003","volume":"55","author":"K McAreavey","year":"2014","unstructured":"McAreavey, K., Liu, W., Miller, P.: Computational approaches to finding and measuring inconsistency in arbitrary knowledge bases. Int. J. Approx. Reason. 55(8), 1659\u20131693 (2014)","journal-title":"Int. J. Approx. Reason."},{"key":"19_CR26","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, vol. 65, pp. 113\u2013126. EasyChair (2019)","DOI":"10.29007\/vgg4"},{"key":"19_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1007\/978-3-642-39611-3_13","volume-title":"Hardware and Software: Verification and Testing","author":"A Morgado","year":"2013","unstructured":"Morgado, A., Liffiton, M., Marques-Silva, J.: MaxSAT-based MCS enumeration. In: Biere, A., Nahir, A., Vos, T. (eds.) HVC 2012. LNCS, vol. 7857, pp. 86\u2013101. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39611-3_13"},{"key":"19_CR28","doi-asserted-by":"crossref","unstructured":"Narodytska, N., Bj\u00f8rner, N., Marinescu, M.V., Sagiv, M.: Core-guided minimal correction set and core enumeration. In: IJCAI, pp. 1353\u20131361. ijcai.org (2018)","DOI":"10.24963\/ijcai.2018\/188"},{"key":"19_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/978-3-030-24258-9_19","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2019","author":"N Narodytska","year":"2019","unstructured":"Narodytska, N., Shrotri, A., Meel, K.S., Ignatiev, A., Marques-Silva, J.: Assessing heuristic machine learning explanations with model counting. In: Janota, M., Lynce, I. (eds.) SAT 2019. LNCS, vol. 11628, pp. 267\u2013278. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-24258-9_19"},{"key":"19_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1007\/978-3-540-30201-8_34","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2004","author":"G Pan","year":"2004","unstructured":"Pan, G., Vardi, M.Y.: Symbolic decision procedures for QBF. In: Wallace, M. (ed.) CP 2004. LNCS, vol. 3258, pp. 453\u2013467. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30201-8_34"},{"issue":"3","key":"19_CR31","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1016\/S0747-7171(86)80028-1","volume":"2","author":"DA Plaisted","year":"1986","unstructured":"Plaisted, D.A., Greenbaum, S.: A structure-preserving clause form translation. J. Symb. Comput. 2(3), 293\u2013304 (1986)","journal-title":"J. Symb. Comput."},{"key":"19_CR32","doi-asserted-by":"publisher","first-page":"224","DOI":"10.1016\/j.artint.2019.04.002","volume":"274","author":"L Pulina","year":"2019","unstructured":"Pulina, L., Seidl, M.: The 2016 and 2017 QBF solvers evaluations (QBFEVAL\u201916 and QBFEVAL\u201917). Artif. Intell. 274, 224\u2013248 (2019)","journal-title":"Artif. Intell."},{"key":"19_CR33","unstructured":"Sang, T., Beame, P., Kautz, H.A.: Performing Bayesian inference by weighted model counting. In: AAAI, pp. 475\u2013482. AAAI Press\/The MIT Press (2005)"},{"key":"19_CR34","doi-asserted-by":"crossref","unstructured":"Shukla, A., Biere, A., Pulina, L., Seidl, M.: A survey on applications of quantified Boolean formulas. In: ICTAI, pp. 78\u201384. IEEE (2019)","DOI":"10.1109\/ICTAI.2019.00020"},{"key":"19_CR35","doi-asserted-by":"crossref","unstructured":"Stockmeyer, L.J., Meyer, A.R.: Word problems requiring exponential time: preliminary report. In: STOC, pp. 1\u20139. ACM (1973)","DOI":"10.1145\/800125.804029"},{"key":"19_CR36","doi-asserted-by":"publisher","first-page":"411","DOI":"10.1016\/j.artint.2019.07.001","volume":"275","author":"M Thimm","year":"2019","unstructured":"Thimm, M., Wallner, J.P.: On the complexity of inconsistency measurement. Artif. Intell. 275, 411\u2013456 (2019)","journal-title":"Artif. Intell."},{"key":"19_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/3-540-46135-3_14","volume-title":"Principles and Practice of Constraint Programming - CP 2002","author":"L Zhang","year":"2002","unstructured":"Zhang, L., Malik, S.: Towards a symmetric treatment of satisfaction and conflicts in quantified Boolean formula evaluation. In: Van Hentenryck, P. (ed.) CP 2002. LNCS, vol. 2470, pp. 200\u2013215. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-46135-3_14"},{"key":"19_CR38","doi-asserted-by":"crossref","unstructured":"Zhou, Z., Qian, Z., Reiter, M.K., Zhang, Y.: Static evaluation of noninterference using approximate model counting. In: SP, pp. 514\u2013528. IEEE Computer Society (2018)","DOI":"10.1109\/SP.2018.00052"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-16681-5_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,3]],"date-time":"2024-10-03T23:43:55Z","timestamp":1727999035000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-16681-5_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031166808","9783031166815"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-16681-5_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"17 September 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CICM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Intelligent Computer Mathematics","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Tbilisi","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Georgia","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19 September 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 September 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"mkm2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/cicm-conference.org\/2022\/cicm.php","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"37","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":"17","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":"4","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":"46% - 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":"2.95","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":"3.9","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)"}}]}}