Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

OuterCount: A First-Level Solution-Counter for Quantified Boolean Formulas

  • Conference paper
  • First Online:
Intelligent Computer Mathematics (CICM 2022)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 13467))

Included in the following conference series:

Abstract

Counting the solutions of symbolic encodings is an intriguing computational problem with many applications. In the field of propositional satisfiability (SAT) solving, for example, many algorithms and tools have emerged to tackle the counting problem. For quantified Boolean formulas (QBFs), an extension of SAT with quantifiers used to compactly encode and solve problems of formal verification, synthesis, planning, etc., practical solution counting has not been considered yet.

We present the first practical counting algorithm for top-level solutions. We prove soundness of our algorithm for true and false formulas and show how to implement it with recent QBF solving technology. Our evaluation of benchmarks from the recent QBF competition gives promising results for this difficult problem.

This work has been supported by the Austrian Science Fund (FWF) under projects W1255-N23 and P31571-N32, the LIT AI Lab funded by the State of Upper Austria.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    http://www.qbfeval.org.

  2. 2.

    http://fmv.jku.at/bloqqer.

References

  1. 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–137. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-24318-4_10

    Chapter  Google Scholar 

  2. 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–186. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-30557-6_14

    Chapter  Google Scholar 

  3. Baluta, T., Shen, S., Shinde, S., Meel, K.S., Saxena, P.: Quantitative verification of neural networks and its security applications. In: CCS, pp. 1249–1264. ACM (2019)

    Google Scholar 

  4. Bayardo Jr., R., Pehoushek, J.D.: Counting models using connected components. In: AAAI/IAAI, pp. 157–162. AAAI Press/The MIT Press (2000)

    Google Scholar 

  5. Becker, B., Ehlers, R., Lewis, M., Marin, P.: ALLQBF solving by computational learning. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, pp. 370–384. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-33386-6_29

    Chapter  Google Scholar 

  6. Bendík, J., Černá, I.: Replication-guided enumeration of minimal unsatisfiable subsets. In: Simonis, H. (ed.) CP 2020. LNCS, vol. 12333, pp. 37–54. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-58475-7_3

    Chapter  Google Scholar 

  7. Bendík, J., Cerna, I.: Rotation based MSS/MCS enumeration. In: LPAR. EPIC, vol. 73, pp. 120–137. EasyChair (2020)

    Google Scholar 

  8. 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–93. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-73721-8_4

    Chapter  Google Scholar 

  9. Birnbaum, E., Lozinskii, E.L.: The good old Davis-Putnam procedure helps counting models. J. Artif. Intell. Res. 10, 457–477 (1999)

    Article  MathSciNet  Google Scholar 

  10. 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–3576. IJCAI/AAAI Press (2016)

    Google Scholar 

  11. 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–1045. IOS Press (2021)

    Google Scholar 

  12. Diptarama, Yoshinaka, R., Shinohara, A.: QBF encoding of generalized tic-tac-toe. In: QBF@SAT. CEUR Workshop Proceedings, vol. 1719, pp. 14–26. CEUR-WS.org (2016)

    Google Scholar 

  13. Dubois, O.: Counting the number of solutions for instances of satisfiability. Theor. Comput. Sci. 81(1), 49–64 (1991)

    Article  MathSciNet  Google Scholar 

  14. 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–148. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-72200-7_13

    Chapter  Google Scholar 

  15. Giunchiglia, E., Narizzano, M., Tacchella, A.: Learning for quantified Boolean logic satisfiability. In: AAAI/IAAI, pp. 649–654. AAAI Press/The MIT Press (2002)

    Google Scholar 

  16. Gomes, C.P., Sabharwal, A., Selman, B.: Chapter 25. Model counting. In: Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 336, pp. 993–1014. IOS Press, Amsterdam, Netherlands (2021)

    Google Scholar 

  17. Hemaspaandra, L.A., Vollmer, H.: The satanic notations: counting classes beyond #P and other definitional adventures. SIGACT News 26(1), 2–13 (1995)

    Article  Google Scholar 

  18. Heule, M., Järvisalo, M., Lonsing, F., Seidl, M., Biere, A.: Clause elimination for SAT and QSAT. J. Artif. Intell. Res. 53, 127–168 (2015)

    Article  MathSciNet  Google Scholar 

  19. Hunter, A., Konieczny, S.: Measuring inconsistency through minimal inconsistent sets. In: KR, pp. 358–366. AAAI Press (2008)

    Google Scholar 

  20. 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–300. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-31980-1_19

    Chapter  MATH  Google Scholar 

  21. Ladner, R.E.: Polynomial space counting problems. SIAM J. Comput. 18(6), 1087–1097 (1989)

    Article  MathSciNet  Google Scholar 

  22. Letz, R.: Lemma and model caching in decision procedures for quantified Boolean formulas. In: Egly, U., Fermüller, C.G. (eds.) TABLEAUX 2002. LNCS (LNAI), vol. 2381, pp. 160–175. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45616-3_12

    Chapter  MATH  Google Scholar 

  23. Li, B., Hsiao, M.S., Sheng, S.: A novel SAT all-solutions solver for efficient preimage computation. In: DATE, pp. 272–279. IEEE Computer Society (2004)

    Google Scholar 

  24. 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–384. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63046-5_23

    Chapter  Google Scholar 

  25. McAreavey, K., Liu, W., Miller, P.: Computational approaches to finding and measuring inconsistency in arbitrary knowledge bases. Int. J. Approx. Reason. 55(8), 1659–1693 (2014)

    Article  MathSciNet  Google Scholar 

  26. Möhle, S., Biere, A.: Combining conflict-driven clause learning and chronological backtracking for propositional model counting. In: GCAI. EPIC, vol. 65, pp. 113–126. EasyChair (2019)

    Google Scholar 

  27. 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–101. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39611-3_13

    Chapter  Google Scholar 

  28. Narodytska, N., Bjørner, N., Marinescu, M.V., Sagiv, M.: Core-guided minimal correction set and core enumeration. In: IJCAI, pp. 1353–1361. ijcai.org (2018)

    Google Scholar 

  29. 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–278. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-24258-9_19

    Chapter  Google Scholar 

  30. Pan, G., Vardi, M.Y.: Symbolic decision procedures for QBF. In: Wallace, M. (ed.) CP 2004. LNCS, vol. 3258, pp. 453–467. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30201-8_34

    Chapter  Google Scholar 

  31. Plaisted, D.A., Greenbaum, S.: A structure-preserving clause form translation. J. Symb. Comput. 2(3), 293–304 (1986)

    Article  MathSciNet  Google Scholar 

  32. Pulina, L., Seidl, M.: The 2016 and 2017 QBF solvers evaluations (QBFEVAL’16 and QBFEVAL’17). Artif. Intell. 274, 224–248 (2019)

    Article  MathSciNet  Google Scholar 

  33. Sang, T., Beame, P., Kautz, H.A.: Performing Bayesian inference by weighted model counting. In: AAAI, pp. 475–482. AAAI Press/The MIT Press (2005)

    Google Scholar 

  34. Shukla, A., Biere, A., Pulina, L., Seidl, M.: A survey on applications of quantified Boolean formulas. In: ICTAI, pp. 78–84. IEEE (2019)

    Google Scholar 

  35. Stockmeyer, L.J., Meyer, A.R.: Word problems requiring exponential time: preliminary report. In: STOC, pp. 1–9. ACM (1973)

    Google Scholar 

  36. Thimm, M., Wallner, J.P.: On the complexity of inconsistency measurement. Artif. Intell. 275, 411–456 (2019)

    Article  MathSciNet  Google Scholar 

  37. 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–215. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-46135-3_14

    Chapter  Google Scholar 

  38. Zhou, Z., Qian, Z., Reiter, M.K., Zhang, Y.: Static evaluation of noninterference using approximate model counting. In: SP, pp. 514–528. IEEE Computer Society (2018)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute for Formal Models and Verification, JKU, Linz, Austria

    Ankit Shukla & Sibylle Möhle

  2. Institute for Algebra, JKU, Linz, Austria

    Manuel Kauers

  3. Institute for Symbolic Artificial Intelligence, JKU, Linz, Austria

    Martina Seidl

Authors
  1. Ankit Shukla
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Sibylle Möhle
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Manuel Kauers
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Martina Seidl
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Martina Seidl .

Editor information

Editors and Affiliations

  1. Imperial College London, London, UK

    Kevin Buzzard

  2. Johannes Kepler University Linz, Linz, Austria

    Temur Kutsia

Rights and permissions

Reprints and permissions

Copyright information

© 2022 The Author(s), under exclusive license to Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Shukla, A., Möhle, S., Kauers, M., Seidl, M. (2022). OuterCount: A First-Level Solution-Counter for Quantified Boolean Formulas. In: Buzzard, K., Kutsia, T. (eds) Intelligent Computer Mathematics. CICM 2022. Lecture Notes in Computer Science(), vol 13467. Springer, Cham. https://doi.org/10.1007/978-3-031-16681-5_19

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-16681-5_19

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-16680-8

  • Online ISBN: 978-3-031-16681-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation