Document Open Access Logo

Enumerative Level-2 Solution Counting for Quantified Boolean Formulas (Short Paper)

Authors Andreas Plank , Sibylle Möhle , Martina Seidl

PDF
Thumbnail PDF

File

LIPIcs.CP.2023.49.pdf
  • Filesize: 0.74 MB
  • 10 pages

Document Identifiers

Author Details

Andreas Plank
  • Institute for Symbolic Artificial Intelligence, JKU Linz, Austria
Sibylle Möhle
  • Max Planck Institute for Informatics, Saarbrücken, Germany
Martina Seidl
  • Institute for Symbolic Artificial Intelligence, JKU Linz, Austria

Funding

This work has been supported by the LIT AI Lab funded by the State of Upper Austria.

Cite AsGet BibTex

Andreas Plank, Sibylle Möhle, and Martina Seidl. Enumerative Level-2 Solution Counting for Quantified Boolean Formulas (Short Paper). In 29th International Conference on Principles and Practice of Constraint Programming (CP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 280, pp. 49:1-49:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.CP.2023.49

Abstract

We lift the problem of enumerative solution counting to quantified Boolean formulas (QBFs) at the second level. In contrast to the well-explored model counting problem for SAT (#SAT), where models are simply assignments to the Boolean variables of a formula, we are now dealing with tree (counter-)models reflecting the dependencies between the variables of the first and the second quantifier block. It turns out that enumerative counting on the second level does not give the complete model count. We present the - to the best of our knowledge - first approach of counting tree (counter-)models together with a counting tool that exploits state-of-the-art QBF technology. We provide several kinds of benchmarks for testing our implementation and illustrate in several case studies that solution counting provides valuable insights into QBF encodings.

Subject Classification

ACM Subject Classification
  • Theory of computation → Automated reasoning
Keywords
  • QBF
  • Second-Level Model Counting

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Teodora Baluta, Shiqi Shen, Shweta Shinde, Kuldeep S. Meel, and Prateek Saxena. Quantitative verification of neural networks and its security applications. In Proc. of the 2019 ACM SIGSAC Conf. on Computer and Communications Security, pages 1249-1264. ACM, 2019. Google Scholar
  2. Michael Bauland, Elmar Böhler, Nadia Creignou, Steffen Reith, Henning Schnoor, and Heribert Vollmer. Quantified constraints: The complexity of decision and counting for bounded alternation. Electron. Colloquium Comput. Complex., TR05-024, 2005. Google Scholar
  3. Olaf Beyersdorff, Janota Mikolás, Florian Lonsing, and Martina Seidl. Quantified Boolean Formulas. In Handbook of Satisfiability, volume 336, pages 1177-1221. IOS Press, 2021. Google Scholar
  4. Armin Biere. CaDiCaL, Lingeling, Plingeling, Treengeling and YalSAT Entering the SAT Competition 2018. In Proc. of SAT Competition 2018 - Solver and Benchmark Descriptions, volume B-2018-1 of Department of Computer Science Series of Publications B, pages 13-14. University of Helsinki, 2018. Google Scholar
  5. Fabrizio Biondi, Michael A. Enescu, Annelie Heuser, Axel Legay, Kuldeep S. Meel, and Jean Quilbeuf. Scalable approximation of quantitative information flow in programs. In Proc. of Int. Conf. on Verification, Model Checking, and Abstract Interpretation, volume 10747 of LNCS, pages 71-93. Springer, 2018. Google Scholar
  6. Elazar Birnbaum and Eliezer L. Lozinskii. The good old Davis-Putnam procedure helps counting models. J. Artif. Intell. Res., 10:457-477, 1999. Google Scholar
  7. Supratik Chakraborty, Kuldeep S. Meel, and Moshe Y. Vardi. Algorithmic improvements in approximate counting for probabilistic inference: From linear to logarithmic SAT calls. In Proc. of Int. Joint Conf. on Artificial Intelligence, pages 3569-3576. IJCAI/AAAI Press, 2016. Google Scholar
  8. Olivier Dubois. Counting the number of solutions for instances of satisfiability. Theor. Comput. Sci., 81(1):49-64, 1991. Google Scholar
  9. Carla P. Gomes, Ashish Sabharwal, and Bart Selman. Model counting. In Handbook of Satisfiability, pages 993-1014. IOS Press, 2021. Google Scholar
  10. Lane A. Hemaspaandra and Heribert Vollmer. The satanic notations: counting classes beyond #P and other definitional adventures. SIGACT News, 26(1):2-13, 1995. Google Scholar
  11. Hans Kleine Büning and Theodor Lettmann. Propositional logic - deduction and algorithms. Cambridge University Press, 1999. Google Scholar
  12. Elias Kuiter, Sebastian Krieter, Chico Sundermann, Thomas Thüm, and Gunter Saake. Tseitin or Not Tseitin? The Impact of CNF Transformations on Feature-Model Analyses. In Proc. of the 37th IEEE/ACM Int. Conf. on Automated Software Engineering. ACM, 2023. Google Scholar
  13. Richard E. Ladner. Polynomial space counting problems. SIAM J. Comput., 18(6):1087-1097, 1989. Google Scholar
  14. Massimo Lauria, Jan Elffers, Jakob Nordström, and Marc Vinyals. CNFgen: A Generator of Crafted Benchmarks. In Proc. of the 20th Int. Conf. on Theory and Applications of Satisfiability Testing, volume 10491 of LNCS, pages 464-473. Springer, 2017. Google Scholar
  15. Florian Lonsing and Uwe Egly. DepQBF 6.0: A search-based QBF solver beyond traditional QCDCL. In Proc. of the 26th Conf. on Automated Deduction, volume 10395 of LNCS, pages 371-384. Springer, 2017. Google Scholar
  16. Nina Narodytska, Aditya A. Shrotri, Kuldeep S. Meel, Alexey Ignatiev, and João Marques-Silva. Assessing heuristic machine learning explanations with model counting. In Proc. of the Int. Conf. on Theory and Applications of Satisfiability Testing, volume 11628 of LNCS, pages 267-278. Springer, 2019. Google Scholar
  17. Aina Niemetz, Mathias Preiner, Martina Seidl, and Armin Biere. Resolution-based certificate extraction for QBF - (tool presentation). In Proc. of the 15th Int. Conference on Theory and Applications of Satisfiability Testing, volume 7317 of LNCS, pages 430-435. Springer, 2012. Google Scholar
  18. Luca Pulina and Martina Seidl. The 2016 and 2017 QBF solvers evaluations (QBFEVAL'16 and QBFEVAL'17). Artif. Intell., 274:224-248, 2019. Google Scholar
  19. Tian Sang, Paul Beame, and Henry A. Kautz. Performing Bayesian inference by weighted model counting. In Proc. of the 20th Nat. Conf. on Artificial Intelligence, pages 475-482. AAAI Press / The MIT Press, 2005. Google Scholar
  20. Shubham Sharma, Subhajit Roy, Mate Soos, and Kuldeep S. Meel. Ganak: A scalable probabilistic exact model counter. In Proc.of Int. Joint Conf. on Artificial Intelligence, pages 1169-1176. Int. Joint Conf. on Artificial Intelligence Organization, 2019. Google Scholar
  21. Ankit Shukla, Armin Biere, Luca Pulina, and Martina Seidl. A survey on applications of quantified Boolean formulas. In Proc. of the Int. Conf. on Tools with Artificial Intelligence, pages 78-84. IEEE, 2019. Google Scholar
  22. Ankit Shukla, Sibylle Möhle, Manuel Kauers, and Martina Seidl. Outercount: A first-level solution-counter for quantified boolean formulas. In Proc. of the 15th Int. Conf on Intelligent Computer Mathematics, volume 13467 of LNCS, pages 272-284. Springer, 2022. Google Scholar
  23. G. S. Tseitin. On the Complexity of Derivation in Propositional Calculus, pages 466-483. Springer, 1983. Google Scholar
  24. Ziqiao Zhou, Zhiyun Qian, Michael K. Reiter, and Yinqian Zhang. Static evaluation of noninterference using approximate model counting. In Proc. of IEEE Symposium on Security and Privacy, pages 514-528. IEEE Computer Society, 2018. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact