Document Open Access Logo

Proof Systems for QBF Synthesis: Extracting Skolem and Herbrand Functions

Authors S. Akshay , Olaf Beyersdorff , Supratik Chakraborty , Lea Kasche , Meena Mahajan , Luc Nicolas Spachmann

PDF

File

Thumbnail PDF
PDF
LIPIcs.SAT.2026.3.pdf
  • Filesize: 0.94 MB
  • 20 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
Keywords
  • Quantified Boolean Formulas
  • Skolem and Herbrand functions
  • Automated synthesis
  • Knowledge compilation
  • Proof systems and complexity

Metrics

Abstract

Strategy extraction in QBF proof systems usually attempts to extract winning strategies from valid proofs. However, an alternative (and arguably more powerful) view is to extract Skolem/Herbrand functions, or equivalently synthesis of the game values at all intermediate points. In this paper, we investigate the existence and properties of such proof systems from which one can extract Skolem and Herbrand functions. We propose such a proof system for QBF, which we show is sound and complete, and from which extraction of Skolem/Herbrand functions can be performed, and game values computed, in polynomial time. We also show that this system is optimal among all proof systems that allow efficient extraction of Skolem/Herbrand functions. We provide conditional lower bound results for our new proof system and compare it to several existing/standard proof systems for QBF that have been studied in the literature, showing interesting orthogonality results. Finally, we provide a compilation algorithm that takes an arbitrary QBF and synthesizes a proof in our system, from which Skolem and Herbrand functions can be easily computed.

Cite As Get BibTex

S. Akshay, Olaf Beyersdorff, Supratik Chakraborty, Lea Kasche, Meena Mahajan, and Luc Nicolas Spachmann. Proof Systems for QBF Synthesis: Extracting Skolem and Herbrand Functions. In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 3:1-3:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.SAT.2026.3

Author Details

S. Akshay
  • Indian Institute of Technology Bombay, India
Olaf Beyersdorff
  • Friedrich Schiller University Jena, Germany
Supratik Chakraborty
  • Indian Institute of Technology Bombay, India
Lea Kasche
  • Friedrich Schiller University Jena, Germany
Meena Mahajan
  • The Institute of Mathematical Sciences, Chennai, India
  • Homi Bhabha National Institute, Training School Complex, Anushaktinagar, Mumbai, India
Luc Nicolas Spachmann
  • Friedrich Schiller University Jena, Germany

Funding

  • Beyersdorff, Olaf: Carl-Zeiss Foundation and DFG grant BE 4209/3-2.
  • Kasche, Lea: Carl-Zeiss Foundation.
  • Mahajan, Meena: Supported in part from the ANRF J C Bose fellowship JCB/2023/000006.

References

  1. S. Akshay and Supratik Chakraborty. Synthesizing Skolem functions: A view from theory and practice. In Sundar Sarukkai and Mihir Chakraborty, editors, Handbook of Logical Thought in India, pages 1-36. Springer India, New Delhi, 2020. URL: https://doi.org/10.1007/978-81-322-1812-8_51-1.
  2. S. Akshay, Supratik Chakraborty, Shubham Goel, Sumith Kulal, and Shetal Shah. Boolean functional synthesis: hardness and practical algorithms. Formal Methods Syst. Des., 57(1):53-86, 2021. URL: https://doi.org/10.1007/s10703-020-00352-2.
  3. S. Akshay, Supratik Chakraborty, and Sahil Jain. Counterexample guided knowledge compilation for Boolean functional synthesis. In Constantin Enea and Akash Lal, editors, Computer Aided Verification - 35th International Conference, CAV 2023, Paris, France, July 17-22, 2023, Proceedings, Part I, volume 13964 of Lecture Notes in Computer Science, pages 367-389. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-37706-8_19.
  4. S. Akshay, Supratik Chakraborty, Ajith K. John, and Shetal Shah. Towards parallel Boolean functional synthesis. In TACAS 2017 Proceedings, Part I, pages 337-353, 2017. URL: https://doi.org/10.1007/978-3-662-54577-5_19.
  5. Sanjeev Arora and Boaz Barak. Computational Complexity - A Modern Approach. Cambridge University Press, 2009. URL: http://www.cambridge.org/catalogue/catalogue.asp?isbn=9780521424264.
  6. Valeriy Balabanov and Jie-Hong R. Jiang. Unified QBF certification and its applications. Form. Methods Syst. Des., 41(1):45-65, 2012. URL: https://doi.org/10.1007/S10703-012-0152-6.
  7. Valeriy Balabanov, Jie-Hong Roland Jiang, Mikolas Janota, and Magdalena Widl. Efficient extraction of QBF (counter)models from long-distance resolution proofs. In Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence, pages 3694-3701, 2015. URL: https://doi.org/10.1609/AAAI.V29I1.9750.
  8. Olaf Beyersdorff. Proof complexity of quantified Boolean logic - a survey. In Marco Benini, Olaf Beyersdorff, Michael Rathjen, and Peter Schuster, editors, Mathematics for Computation (M4C), pages 353-391. World Scientific, Singapore, 2022. Google Scholar
  9. Olaf Beyersdorff, Joshua Blinkhorn, and Luke Hinde. Size, cost, and capacity: A semantic technique for hard random QBFs. Logical Methods in Computer Science, 15(1), 2019. URL: https://doi.org/10.23638/LMCS-15(1:13)2019.
  10. Olaf Beyersdorff, Joshua Blinkhorn, and Meena Mahajan. Building strategies into QBF proofs. J. Autom. Reason., 65(1):125-154, 2021. URL: https://doi.org/10.1007/s10817-020-09560-1.
  11. Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan, and Tomás Peitl. Hardness characterisations and size-width lower bounds for QBF resolution. ACM Transactions on Computational Logic, 2022. Google Scholar
  12. Olaf Beyersdorff, Joshua Blinkhorn, and Tomás Peitl. Strong (D)QBF dependency schemes via tautology-free resolution paths. In Theory and Applications of Satisfiability Testing (SAT), pages 394-411. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-51825-7_28.
  13. Olaf Beyersdorff and Benjamin Böhm. Understanding the relative strength of QBF CDCL solvers and QBF resolution. Log. Methods Comput. Sci., 19(2), 2023. URL: https://doi.org/10.46298/LMCS-19(2:2)2023.
  14. Olaf Beyersdorff, Ilario Bonacina, and Leroy Chew. Lower bounds: From circuits to QBF proof systems. In Proc. ACM Conference on Innovations in Theoretical Computer Science (ITCS'16), pages 249-260. ACM, 2016. URL: https://doi.org/10.1145/2840728.2840740.
  15. Olaf Beyersdorff, Ilario Bonacina, Leroy Chew, and Jan Pich. Frege systems for quantified Boolean logic. J. ACM, 67(2):9:1-9:36, 2020. URL: https://doi.org/10.1145/3381881.
  16. Olaf Beyersdorff, Ilario Bonacina, Kaspar Kasche, Meena Mahajan, and Luc Nicolas Spachmann. Semi-algebraic proof systems for QBF. In Jeremias Berg and Jakob Nordström, editors, 28th International Conference on Theory and Applications of Satisfiability Testing, SAT 2025, Glasgow, Scotland, August 12-15, 2025, LIPIcs, pages 5:1-5:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. URL: https://doi.org/10.4230/LIPIcs.SAT.2025.5.
  17. Olaf Beyersdorff, Leroy Chew, and Mikolás Janota. New resolution-based QBF calculi and their proof complexity. ACM Transactions on Computation Theory, 11(4):26:1-26:42, 2019. URL: https://doi.org/10.1145/3352155.
  18. Olaf Beyersdorff, Leroy Chew, and Mikoláš Janota. On unification of QBF resolution-based calculi. In Proc. 39th Symposium on Mathematical Foundations of Computer Science, volume 8635 of Lecture Notes in Computer Science, pages 81-93, 2014. URL: https://doi.org/10.1007/978-3-662-44465-8_8.
  19. Olaf Beyersdorff, Luke Hinde, and Ján Pich. Reasons for hardness in QBF proof systems. ACM Transactions on Computation Theory, 12(2):10:1-10:27, 2020. URL: https://doi.org/10.1145/3378665.
  20. Olaf Beyersdorff, Mikolás Janota, Florian Lonsing, and Martina Seidl. Quantified Boolean formulas. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, pages 1177-1221. IOS Press, 2021. URL: https://doi.org/10.3233/FAIA201015.
  21. Olaf Beyersdorff, Luca Pulina, Martina Seidl, and Ankit Shukla. QBFFam: A tool for generating QBF families from proof complexity. In Chu-Min Li and Felip Manyà, editors, Theory and Applications of Satisfiability Testing (SAT), volume 12831 of Lecture Notes in Computer Science, pages 21-29. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-80223-3_3.
  22. Joshua Blinkhorn. Quantified Boolean Formulas: Proof Complexity and Models of Solving. PhD thesis, University of Leeds, Leeds, 2019. Google Scholar
  23. Benjamin Böhm and Olaf Beyersdorff. QCDCL vs QBF resolution: Further insights. J. Artif. Intell. Res., 81:741-769, 2024. URL: https://doi.org/10.1613/JAIR.1.15522.
  24. Benjamin Böhm, Tomás Peitl, and Olaf Beyersdorff. QCDCL with cube learning or pure literal elimination - what is best? Artif. Intell., 336:104194, 2024. URL: https://doi.org/10.1016/J.ARTINT.2024.104194.
  25. Supratik Chakraborty, Dror Fried, Lucas M. Tabajara, and Moshe Y. Vardi. Functional synthesis via input-output separation. Formal Methods Syst. Des., 60(2):228-258, 2022. URL: https://doi.org/10.1007/S10703-023-00410-5.
  26. Chen C. Chang and H. Jerome Keisler. Model theory, Third Edition, volume 73 of Studies in logic and the foundations of mathematics. North-Holland, 1992. Google Scholar
  27. Leroy Chew. Hardness and optimality in QBF proof systems modulo NP. In Chu-Min Li and Felip Manyà, editors, Theory and Applications of Satisfiability Testing - SAT 2021 - 24th International Conference, Barcelona, Spain, July 5-9, 2021, Proceedings, volume 12831 of Lecture Notes in Computer Science, pages 98-115. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-80223-3_8.
  28. Leroy Chew and Marijn J. H. Heule. Relating existing powerful proof systems for QBF. In Kuldeep S. Meel and Ofer Strichman, editors, 25th International Conference on Theory and Applications of Satisfiability Testing (SAT), volume 236 of LIPIcs, pages 10:1-10:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.SAT.2022.10.
  29. Stephen A. Cook and Robert A. Reckhow. The relative efficiency of propositional proof systems. The Journal of Symbolic Logic, 44(1):36-50, 1979. URL: https://doi.org/10.2307/2273702.
  30. Uwe Egly, Florian Lonsing, and Magdalena Widl. Long-distance resolution: Proof generation and strategy extraction in search-based QBF solving. In Proc. Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), pages 291-308, 2013. URL: https://doi.org/10.1007/978-3-642-45221-5_21.
  31. Dror Fried, Lucas M. Tabajara, and Moshe Y. Vardi. Bdd-based Boolean functional synthesis. In Swarat Chaudhuri and Azadeh Farzan, editors, Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part II, volume 9780 of Lecture Notes in Computer Science, pages 402-421. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-41540-6_22.
  32. Priyanka Golia, Subhajit Roy, and Kuldeep S. Meel. Manthan: A data-driven approach for boolean function synthesis. Computer Aided Verification, 12225:611-633, 2020. URL: https://doi.org/10.1007/978-3-030-53291-8_31.
  33. Priyanka Golia, Friedrich Slivovsky, Subhajit Roy, and Kuldeep S. Meel. Engineering an efficient boolean functional synthesis engine. In IEEE/ACM International Conference On Computer Aided Design, ICCAD 2021, Munich, Germany, November 1-4, 2021, pages 1-9. IEEE, 2021. URL: https://doi.org/10.1109/ICCAD51958.2021.9643583.
  34. Mikolás Janota. On Q-Resolution and CDCL QBF solving. In Proc. International Conference on Theory and Applications of Satisfiability Testing (SAT), pages 402-418, 2016. URL: https://doi.org/10.1007/978-3-319-40970-2_25.
  35. Mikolás Janota and Joao 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.
  36. Emil Jeřábek. Weak pigeonhole principle, and randomized computation. PhD thesis, Faculty of Mathematics and Physics, Charles University, Prague, 2005. Google Scholar
  37. J.-H. R. Jiang and V Balabanov. Resolution proofs and Skolem functions in QBF evaluation and applications. In Proc. of CAV, pages 149-164. Springer, 2011. Google Scholar
  38. A. John, S. Shah, S. Chakraborty, A. Trivedi, and S. Akshay. Skolem functions for factored formulas. In FMCAD, pages 73-80, 2015. Google Scholar
  39. Manuel Kauers and Martina Seidl. Short proofs for some symmetric quantified Boolean formulas. Inf. Process. Lett., 140:4-7, 2018. URL: https://doi.org/10.1016/J.IPL.2018.07.009.
  40. Hans Kleine Büning, Marek Karpinski, and Andreas Flögel. Resolution for quantified Boolean formulas. Inf. Comput., 117(1):12-18, 1995. URL: https://doi.org/10.1006/INCO.1995.1025.
  41. Jan Krajíček. Bounded Arithmetic, Propositional Logic, and Complexity Theory, volume 60 of Encyclopedia of Mathematics and Its Applications. Cambridge University Press, Cambridge, 1995. Google Scholar
  42. Martina Seidl Marijn Heule and Armin Biere. Efficient Extraction of Skolem Functions from QRAT Proofs. In Formal Methods in Computer-Aided Design, FMCAD 2014, Lausanne, Switzerland, October 21-24, 2014, pages 107-114, 2014. URL: https://doi.org/10.1109/FMCAD.2014.6987602.
  43. Alexander Nadel and Yogev Shalmon. Enumerating all boolean matches. In Jeremias Berg and Jakob Nordström, editors, 28th International Conference on Theory and Applications of Satisfiability Testing, SAT 2025, Glasgow, Scotland, August 12-15, 2025, volume 341 of LIPIcs, pages 22:1-22:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. URL: https://doi.org/10.4230/LIPIcs.SAT.2025.22.
  44. Tomás Peitl, Friedrich Slivovsky, and Stefan Szeider. Long-distance Q-resolution with dependency schemes. J. Autom. Reasoning, 63(1):127-155, 2019. URL: https://doi.org/10.1007/S10817-018-9467-3.
  45. Tomás Peitl, Friedrich Slivovsky, and Stefan Szeider. Proof complexity of fragments of long-distance Q-resolution. In Mikolás Janota and Inês Lynce, editors, Theory and Applications of Satisfiability Testing - SAT 2019 - 22nd International Conference, SAT, Proceedings, volume 11628 of Lecture Notes in Computer Science, pages 319-335. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-24258-9_23.
  46. Tomáš Peitl. QBF encodings of chess problems. Technical Report AC-TR-18-013, Algorithms and Complexity Group, TU Wien, 2018. URL: http://www.ac.tuwien.ac.at/files/tr/ac-tr-18-013.pdf.
  47. Markus N. Rabe and Sanjit A. Seshia. Incremental determinization. In Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings, pages 375-392, 2016. URL: https://doi.org/10.1007/978-3-319-40970-2_23.
  48. Ankit Shukla, Armin Biere, Luca Pulina, and Martina Seidl. A survey on applications of quantified Boolean formulas. In Proc. IEEE International Conference on Tools with Artificial Intelligence (ICTAI), pages 78-84, 2019. URL: https://doi.org/10.1109/ICTAI.2019.00020.
  49. Friedrich Slivovsky. Quantified CDCL with universal resolution. In Kuldeep S. Meel and Ofer Strichman, editors, 25th International Conference on Theory and Applications of Satisfiability Testing (SAT), volume 236 of LIPIcs, pages 24:1-24:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.SAT.2022.24.
  50. Friedrich Slivovsky and Stefan Szeider. Soundness of Q-resolution with dependency schemes. Theoretical Computer Science, 612:83-101, 2016. URL: https://doi.org/10.1016/J.TCS.2015.10.020.
  51. Allen Van Gelder. Contributions to the theory of practical quantified Boolean formula solving. In Proc. Principles and Practice of Constraint Programming (CP), pages 647-663, 2012. URL: https://doi.org/10.1007/978-3-642-33558-7_47.
  52. Heribert Vollmer. Introduction to Circuit Complexity - A Uniform Approach. Texts in Theoretical Computer Science. Springer Verlag, Berlin Heidelberg, 1999. 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