Document Open Access Logo

Definition-Based Dependency Schemes

Authors David Kattermann , Clemens Hofstadler , Martina Seidl

PDF

File

Thumbnail PDF
PDF
LIPIcs.SAT.2026.22.pdf
  • Filesize: 0.82 MB
  • 18 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
Keywords
  • Quantified Boolean formulas
  • Dependency schemes
  • Proof calculi

Metrics

Abstract

A variable in a quantified Boolean formula (QBFs) is defined, if its value is uniquely determined by some other variables. Such definitions are widely exploited in various techniques for QBF solving. In this work, we formalize the concept of using definitions for reducing variable dependencies by introducing a novel dependency scheme and investigate its proof-theoretic impact. 
Our analysis shows that a definition-based dependency scheme is able to detect independencies other established dependency schemes cannot and that this can lead to exponentially shorter refutations. We further demonstrate that our scheme can be combined with any other scheme and that such a combined use can exponentially outperform using either scheme alone. Moreover, we study the dynamic application of our definition-based dependency scheme, which leads to another exponential speedup compared to the static application. Finally, we analyze the computational complexity of our dependency scheme and introduce a family of tractable variants.

Cite As Get BibTex

David Kattermann, Clemens Hofstadler, and Martina Seidl. Definition-Based Dependency Schemes. In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 22:1-22:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.SAT.2026.22

Author Details

David Kattermann
  • Institute for Symbolic AI, Johannes Kepler Universität Linz, Austria
Clemens Hofstadler
  • Institute for Symbolic AI, Johannes Kepler Universität Linz, Austria
Martina Seidl
  • Institute for Symbolic AI, Johannes Kepler Universität Linz, Austria

Funding

This work is supported by the LIT AI Lab funded by the State of Upper Austria and by the Austrian Science Fund (FWF) [10.55776/COE12].

References

  1. Olaf Beyersdorff. Proof complexity of quantified Boolean logic-a survey. Mathematics for Computation (M4C), pages 353-391, 2022. URL: https://doi.org/10.1142/9789811245220_0015.
  2. Olaf Beyersdorff and Joshua Blinkhorn. Dependency Schemes in QBF Calculi: Semantics and Soundness. In Principles and Practice of Constraint Programming, volume 9892, pages 96-112, 2016. URL: https://doi.org/10.1007/978-3-319-44953-1_7.
  3. Olaf Beyersdorff and Joshua Blinkhorn. Dynamic QBF Dependencies in Reduction and Expansion. ACM Transactions on Computational Logic, 21(2):1-27, 2020. URL: https://doi.org/10.1145/3355995.
  4. Olaf Beyersdorff, Joshua Blinkhorn, Leroy Chew, Renate Schmidt, and Martin Suda. Reinterpreting Dependency Schemes: Soundness Meets Incompleteness in DQBF. Journal of Automated Reasoning, 63(3):597-623, 2019. URL: https://doi.org/10.1007/s10817-018-9482-4.
  5. Olaf Beyersdorff, Joshua Blinkhorn, and Luke Hinde. Size, Cost, and Capacity: A Semantic Technique for Hard Random QBFs. Logical Methods in Computer Science, Volume 15, Issue 1:4141, 2019. URL: https://doi.org/10.23638/LMCS-15(1:13)2019.
  6. Olaf Beyersdorff, Joshua Blinkhorn, and Tomáš Peitl. Strong (D)QBF Dependency Schemes via Implication-free Resolution Paths. ACM Transactions on Computation Theory, 16(4):1-25, 2024. URL: https://doi.org/10.1145/3689345.
  7. Olaf Beyersdorff and Benjamin Böhm. Understanding the relative strength of QBF CDCL solvers and QBF resolution. Logical Methods in Computer Science, 19(2), 2023. URL: https://doi.org/10.46298/LMCS-19(2:2)2023.
  8. Olaf Beyersdorff, Leroy Chew, and Mikolás Janota. Proof Complexity of Resolution-based QBF Calculi. LIPIcs STACS 2015, 30:76-89, 2015. URL: https://doi.org/10.4230/LIPIcs.STACS.2015.76.
  9. Olaf Beyersdorff, Leroy Chew, Renate Schmidt, and Martin Suda. Lifting QBF resolution calculi to DQBF. In International Conference on Theory and Applications of Satisfiability Testing, pages 490-499. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-40970-2_30.
  10. Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors. Handbook of Satisfiability - Second Edition, volume 336 of Frontiers in Artificial Intelligence and Applications. IOS Press, 2021. URL: https://doi.org/10.3233/FAIA336.
  11. Joshua Blinkhorn and Olaf Beyersdorff. Shortening QBF proofs with dependency schemes. In International Conference on Theory and Applications of Satisfiability Testing, pages 263-280. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-66263-3_17.
  12. Joshua Lewis Blinkhorn. Quantified Boolean formulas: Proof complexity and models of solving. PhD thesis, University of Leeds, 2019. URL: https://etheses.whiterose.ac.uk/id/eprint/26508/.
  13. Leroy Chew and Tomás Peitl. Strong (D)QBF Dependency Schemes via Pure Universal Resolution Paths. Electronic Colloquium on Computational Complexity, TR25-149, 2025. URL: https://eccc.weizmann.ac.il/report/2025/149.
  14. Abhimanyu Choudhury and Meena Mahajan. Dependency Schemes in CDCL-based QBF Solving: A Proof-Theoretic Study. Journal of Automated Reasoning, 68(3):16, 2024. URL: https://doi.org/10.1007/s10817-024-09707-4.
  15. Zhaohui Fu and Sharad Malik. Extracting Logic Circuit Structure from Conjunctive Normal Form Descriptions. In 20th International Conference on VLSI Design held jointly with 6th International Conference on Embedded Systems (VLSID'07), pages 37-42, 2007. URL: https://doi.org/10.1109/VLSID.2007.81.
  16. Markus Iser. Recognition and Exploitation of Gate Structure in SAT Solving. PhD thesis, Karlsruher Institut für Technologie (KIT), 2020. URL: https://doi.org/10.5445/IR/1000118523.
  17. Mikoláš Janota and Joao Marques-Silva. Expansion-based QBF solving versus Q-resolution. Theoretical Computer Science, 577:25-42, 2015. URL: https://doi.org/10.1016/j.tcs.2015.01.048.
  18. Hans Kleine Büning, Marek Karpinski, and Andreas Flögel. Resolution for quantified Boolean formulas. Information and computation, 117(1):12-18, 1995. URL: https://doi.org/10.1006/inco.1995.1025.
  19. Jean-Marie Lagniez, Emmanuel Lonca, and Pierre Marquis. Improving Model Counting by Leveraging Definability. In Proceedings of the 25th International Joint Conference on Artificial Intelligence, pages 751-757. IJCAI/AAAI Press, 2016. URL: http://www.ijcai.org/Abstract/16/112.
  20. Florian Lonsing. Dependency Schemes and Search-Based QBF Solving: Theory and Practice. PhD thesis, Johannes Kepler University Linz, 2012. Google Scholar
  21. Florian Lonsing and Armin Biere. DepQBF: A Dependency-Aware QBF Solver. Journal of Satisfiability, Boolean Modeling and Computation, 7(2-3):71-76, 2010. URL: https://doi.org/10.3233/SAT190077.
  22. Alessandro Padoa. Essai d'une théorie algébrique des nombres entiers, précédé d’une introduction logique à une theorie déductive quelconque. In Bibliothèque du Congrès international de philosophie, volume 3, pages 309-365, 1901. Google Scholar
  23. Tomáš Peitl, Friedrich Slivovsky, and Stefan Szeider. Combining resolution-path dependencies with dependency learning. In International Conference on Theory and Applications of Satisfiability Testing, pages 306-318. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-24258-9_22.
  24. Tomáš Peitl, Friedrich Slivovsky, and Stefan Szeider. Dependency learning for QBF. Journal of Artificial Intelligence Research, 65:181-208, 2019. URL: https://doi.org/10.1613/JAIR.1.11529.
  25. Tomáš Peitl, Friedrich Slivovsky, and Stefan Szeider. Long-Distance Q-Resolution with Dependency Schemes. Journal of Automated Reasoning, 63(1):127-155, 2019. URL: https://doi.org/10.1007/s10817-018-9467-3.
  26. Joseph Reeves, Marijn Heule, and Randal Bryant. Moving definition variables in quantified Boolean formulas. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 462-479. Springer, 2022. URL: https://doi.org/10.1007/978-3-030-99524-9_26.
  27. Franz-Xaver Reichl, Friedrich Slivovsky, and Stefan Szeider. Certified DQBF solving by definition extraction. In International Conference on Theory and Applications of Satisfiability Testing, pages 499-517. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-80223-3_34.
  28. Marko Samer and Stefan Szeider. Backdoor sets of quantified Boolean formulas. Journal of Automated Reasoning, 42(1):77-97, 2009. URL: https://doi.org/10.1007/s10817-008-9114-5.
  29. Ankit Shukla, Armin Biere, Luca Pulina, and Martina Seidl. A survey on applications of quantified Boolean formulas. In 2019 IEEE 31st International Conference on Tools with Artificial Intelligence (ICTAI), pages 78-84. IEEE, 2019. URL: https://doi.org/10.1109/ICTAI.2019.00020.
  30. Friedrich Slivovsky. Interpolation-based semantic gate extraction and its applications to qbf preprocessing. In International Conference on Computer Aided Verification, pages 508-528. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-53288-8_24.
  31. Friedrich Slivovsky and Stefan Szeider. Computing resolution-path dependencies in linear time. In International Conference on Theory and Applications of Satisfiability Testing, pages 58-71. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-31612-8_6.
  32. 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.
  33. Grigori S Tseitin. On the complexity of derivation in propositional calculus. In Automation of reasoning 2: Classical papers on computational logic 1967-1970, pages 466-483. Springer, 1983. URL: https://doi.org/10.1007/978-3-642-81955-1_28.
  34. Allen Van Gelder. Contributions to the theory of practical quantified boolean formula solving. In International Conference on Principles and Practice of Constraint Programming, pages 647-663. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-33558-7_47.
  35. Ralf Wimmer, Christoph Scholl, and Bernd Becker. The (D)QBF Preprocessor HQSpre - Underlying Theory and Its Implementation. Journal on Satisfiability, Boolean Modeling and Computation, 11(1):3-52, 2019. URL: https://doi.org/10.3233/SAT190115.
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