Document Open Access Logo

On Proof Systems for #QBF (Short Paper)

Authors Sravanthi Chede , Leroy Chew , Vaibhav Krishan , Anil Shukla

PDF

File

Thumbnail PDF
PDF
LIPIcs.SAT.2026.32.pdf
  • Filesize: 0.86 MB
  • 12 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
Keywords
  • QBF
  • Model Counting
  • Proof Systems
  • #QBF

Metrics

Abstract

For a quantified Boolean formula (QBF), the problem of computing the number of winning strategies is known as the #QBF problem. This problem is considered harder than the analogous #SAT problem. Recently, important proof systems for QBFs and #SAT have been studied. By extending the ideas from both fields, we show that it is possible to design proof systems for #QBF. Such proof systems are important not only for advancing the theory of #QBF but also for certifying and designing better #QBF solvers, an area that is still in its early stages.
In this paper, we explore #QBF proof systems to count the number of Skolem functions. In addition to a naive system, we study #QBF systems based on the ∀-expansion rule of QBFs. We observe that these systems have inherent structural weaknesses that lead to lower bounds. As an alternative, we propose a #QBF proof system that we call Q-MICE, which consists of sound inference rules for computing and certifying the #QBF solution, similar to the line-based #SAT proof system MICE. To demonstrate the strength of Q-MICE, we present various upper bounds, such as the quantified version of the propositional XOR-PAIRS formula, which are known to be hard for MICE. Consequently, we also separate Q-MICE from ∀-expansion based #QBF proof systems.

Cite As Get BibTex

Sravanthi Chede, Leroy Chew, Vaibhav Krishan, and Anil Shukla. On Proof Systems for #QBF (Short Paper). In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 32:1-32:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.SAT.2026.32

Author Details

Sravanthi Chede
  • The Institute of Mathematical Sciences (A CI of Homi Bhabha National Institute), Chennai, India
Leroy Chew
  • Czech Technical University in Prague, Czech Republic
Vaibhav Krishan
  • The Institute of Mathematical Sciences (A CI of Homi Bhabha National Institute), Chennai, India
Anil Shukla
  • Indian Institute of Technology Ropar, Rupnagar, India

Funding

  • Chede, Sravanthi: Supported by the ANRF J C Bose fellowship no. JCB/2023/000006.
  • Chew, Leroy: This project is supported by the European Union under the project ROBOPROX (reg. no. CZ.02.01.01/00/22_008/0004590) and by the Czech Science Foundation project 24-12759S.

Acknowledgements

We thank the anonymous reviewers for their detailed and helpful suggestions.

References

  1. Cook S. A. and Reckhow A. R. The relative efficiency of propositional proof systems. Journal of Symbolic Logic, 44(1):36-50, 1977. Google Scholar
  2. Sanjeev Arora and Boaz Barak. Computational Complexity - A Modern Approach. Cambridge University Press, 2009. Google Scholar
  3. Olaf Beyersdorff and Joshua Blinkhorn. Genuine lower bounds for QBF expansion. In Rolf Niedermeier and Brigitte Vallée, editors, 35th Symposium on Theoretical Aspects of Computer Science, STACS 2018, Caen, France, February 28 - March 3, 2018, LIPIcs, pages 12:1-12:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.STACS.2018.12.
  4. Olaf Beyersdorff, Ilario Bonacina, Leroy Chew, and Ján Pich. Frege systems for Quantified Boolean Logic. J. ACM, 67(2):9:1-9:36, 2020. URL: https://doi.org/10.1145/3381881.
  5. Olaf Beyersdorff, Tim Hoffmann, and Luc Nicolas Spachmann. Proof complexity of propositional model counting. J. Satisf. Boolean Model. Comput., 15(1):27-59, 2024. URL: https://doi.org/10.3233/SAT-231507.
  6. Randal E. Bryant, Wojciech Nawrocki, Jeremy Avigad, and Marijn J. H. Heule. Certified knowledge compilation with application to formally verified model counting. J. Artif. Intell. Res., 82, 2025. URL: https://doi.org/10.1613/JAIR.1.15958.
  7. Florent Capelli. Knowledge compilation languages as proof systems. In Mikoláš Janota and Inês Lynce, editors, Theory and Applications of Satisfiability Testing - SAT 2019 - 22nd International Conference, SAT 2019, Lisbon, Portugal, July 9-12, 2019, Proceedings, Lecture Notes in Computer Science, pages 90-99. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-24258-9_6.
  8. Florent Capelli, Jean-Marie Lagniez, Andreas Plank, and Martina Seidl. A top-down tree model counter for quantified boolean formulas. In Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence, IJCAI 2024, Jeju, South Korea, August 3-9, 2024, pages 1853-1861. ijcai.org, 2024. URL: https://www.ijcai.org/proceedings/2024/205.
  9. Sravanthi Chede, Leroy Chew, and Anil Shukla. Circuits, proofs and propositional model counting. In Siddharth Barman and Slawomir Lasota, editors, 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2024, Gandhinagar, Gujarat, India, December 16-18, 2024, LIPIcs, pages 18:1-18:23. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2024.18.
  10. Johannes Klaus Fichte, Markus Hecher, and Valentin Roland. Proofs for propositional model counting. In Kuldeep S. Meel and Ofer Strichman, editors, 25th International Conference on Theory and Applications of Satisfiability Testing, SAT 2022, Haifa, Israel, August 2-5, 2022, LIPIcs, pages 30:1-30:24. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.SAT.2022.30.
  11. Aysegül Ihsan and Nurettin Dogan. Improved affine encryption algorithm for color images using LFSR and XOR encryption. Multim. Tools Appl., 82(5):7621-7637, 2023. URL: https://doi.org/10.1007/S11042-022-13727-W.
  12. Mikoláš Janota and João Marques-Silva. Expansion-based QBF solving versus Q-resolution. Theor. Comput. Sci., 577:25-42, 2015. URL: https://doi.org/10.1016/j.tcs.2015.01.048.
  13. Richard E. Ladner. Polynomial space counting problems. SIAM J. Comput., 18(6):1087-1097, 1989. URL: https://doi.org/10.1137/0218073.
  14. Andreas Plank, Sibylle Möhle, and Martina Seidl. Counting QBF solutions at level two. Constraints An Int. J., 29(1-2):22-39, 2024. URL: https://doi.org/10.1007/S10601-024-09369-4.
  15. Arijit Shaw, Brendan Juba, and Kuldeep S. Meel. An approximate skolem function counter. In Michael J. Wooldridge, Jennifer G. Dy, and Sriraam Natarajan, editors, Thirty-Eighth AAAI Conference on Artificial Intelligence, AAAI 2024, Thirty-Sixth Conference on Innovative Applications of Artificial Intelligence, IAAI 2024, Fourteenth Symposium on Educational Advances in Artificial Intelligence, EAAI 2014, February 20-27, 2024, Vancouver, Canada, pages 8108-8116. AAAI Press, 2024. URL: https://doi.org/10.1609/AAAI.V38I8.28650.
  16. Ankit Shukla, Sibylle Möhle, Manuel Kauers, and Martina Seidl. Outercount: A first-level solution-counter for quantified boolean formulas. In Kevin Buzzard and Temur Kutsia, editors, Intelligent Computer Mathematics - 15th International Conference, CICM 2022, Tbilisi, Georgia, September 19-23, 2022, Proceedings, Lecture Notes in Computer Science, pages 272-284. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-16681-5_19.
  17. G. S. Tseitin. On the complexity of derivations in propositional calculus. In A. O. Slisenko, editor, Studies in Mathematics and Mathematical Logic, Part II, pages 115-125. Springer, 1970. Translated from Russian: Zapiski Nauchnykh Seminarov LOMI 8 (1968), pp. 234–259. Google Scholar
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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