Document Open Access Logo

Building Strategies into QBF Proofs

Authors Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan

PDF
Thumbnail PDF

File

LIPIcs.STACS.2019.14.pdf
  • Filesize: 0.55 MB
  • 18 pages

Document Identifiers

Author Details

Olaf Beyersdorff
  • Institut für Informatik, Friedrich-Schiller-Universität Jena, Germany
Joshua Blinkhorn
  • Institut für Informatik, Friedrich-Schiller-Universität Jena, Germany
Meena Mahajan
  • The Institute of Mathematical Sciences, HBNI, Chennai, India

Funding

Supported by the EU Marie Curie IRSES grant CORCON, and grant no. 60842 from the John Templeton Foundation.

Cite AsGet BibTex

Olaf Beyersdorff, Joshua Blinkhorn, and Meena Mahajan. Building Strategies into QBF Proofs. In 36th International Symposium on Theoretical Aspects of Computer Science (STACS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 126, pp. 14:1-14:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.STACS.2019.14

Abstract

Strategy extraction is of paramount importance for quantified Boolean formulas (QBF), both in solving and proof complexity. It extracts (counter)models for a QBF from a run of the solver resp. the proof of the QBF, thereby allowing to certify the solver’s answer resp. establish soundness of the system. So far in the QBF literature, strategy extraction has been algorithmically performed from proofs. Here we devise the first QBF system where (partial) strategies are built into the proof and are piecewise constructed by simple operations along with the derivation. This has several advantages: (1) lines of our calculus have a clear semantic meaning as they are accompanied by semantic objects; (2) partial strategies are represented succinctly (in contrast to some previous approaches); (3) our calculus has strategy extraction by design; and (4) the partial strategies allow new sound inference steps which are disallowed in previous central QBF calculi such as Q-Resolution and long-distance Q-Resolution. The last item (4) allows us to show an exponential separation between our new system and the previously studied reductionless long-distance resolution calculus, introduced to model QCDCL solving. Our approach also naturally lifts to dependency QBFs (DQBF), where it yields the first sound and complete CDCL-type calculus for DQBF, thus opening future avenues into DQBF CDCL solving.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
Keywords
  • QBF
  • DQBF
  • resolution
  • proof complexity

Metrics

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

References

  1. QBFEVAL homepage. http://www.qbflib.org/index_eval.php. Accessed: 2018-09-26.
  2. Valeriy Balabanov, Hui-Ju Katherine Chiang, and Jie-Hong R. Jiang. Henkin quantifiers and Boolean formulae: A certification perspective of DQBF. Theoretical Computer Science, 523:86-100, 2014. Google Scholar
  3. Valeriy Balabanov and Jie-Hong R. Jiang. Unified QBF Certification and its Applications. Formal Methods in System Design, 41(1):45-65, 2012. Google Scholar
  4. Valeriy Balabanov, Jie-Hong Roland Jiang, Mikolás̆ Janota, and Magdalena Widl. Efficient Extraction of QBF (Counter)models from Long-Distance Resolution Proofs. In Blai Bonet and Sven Koenig, editors, Conference on Artificial Intelligence (AAAI), pages 3694-3701. AAAI Press, 2015. Google Scholar
  5. Marco Benedetti and Hratch Mangassarian. QBF-based formal verification: Experience and perspectives. Journal on Satisfiability, Boolean Modeling and Computation (JSAT), 5(1-4):133-191, 2008. Google Scholar
  6. Olaf Beyerdorff, Joshua Blinkhorn, Leroy Chew, Renate Schmidt, and Martin Suda. Reinterpreting Dependency Schemes: Soundness Meets Incompleteness in DQBF. Journal of Automated Reasoning (in press), 2018. Google Scholar
  7. Olaf Beyersdorff and Joshua Blinkhorn. Dependency Schemes in QBF Calculi: Semantics and Soundness. In Michel Rueher, editor, Principles and Practice of Constraint Programming (CP), volume 9892 of Lecture Notes in Computer Science, pages 96-112. Springer, 2016. Google Scholar
  8. Olaf Beyersdorff, Joshua Blinkhorn, and Luke Hinde. Size, Cost and Capacity: A Semantic Technique for Hard Random QBFs. In Anna R. Karlin, editor, ACM Conference on Innovations in Theoretical Computer Science (ITCS), volume 94 of Leibniz International Proceedings in Informatics (LIPIcs), pages 9:1-9:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. Google Scholar
  9. Olaf Beyersdorff, Ilario Bonacina, and Leroy Chew. Lower Bounds: From Circuits to QBF Proof Systems. In Madhu Sudan, editor, ACM Conference on Innovations in Theoretical Computer Science (ITCS), pages 249-260. ACM, 2016. Google Scholar
  10. Olaf Beyersdorff, Leroy Chew, and Mikolás̆ Janota. On Unification of QBF Resolution-Based Calculi. In Erzsébet Csuhaj-Varjú, Martin Dietzfelbinger, and Zoltán Ésik, editors, International Symposium on Mathematical Foundations of Computer Science (MFCS), volume 8635 of Lecture Notes in Computer Science, pages 81-93. Springer, 2014. Google Scholar
  11. Olaf Beyersdorff, Leroy Chew, and Mikolás̆ Janota. Proof Complexity of Resolution-based QBF Calculi. In Ernst W. Mayr and Nicolas Ollinger, editors, International Symposium on Theoretical Aspects of Computer Science (STACS), volume 30 of Leibniz International Proceedings in Informatics (LIPIcs), pages 76-89. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. Google Scholar
  12. Olaf Beyersdorff, Leroy Chew, Renate A. Schmidt, and Martin Suda. Lifting QBF Resolution Calculi to DQBF. In Nadia Creignou and Daniel Le Berre, editors, International Conference on Theory and Applications of Satisfiability Testing (SAT), volume 9710 of Lecture Notes in Computer Science, pages 490-499. Springer, 2016. Google Scholar
  13. Nikolaj Bjørner, Mikolás Janota, and William Klieber. On Conflicts and Strategies in QBF. In Ansgar Fehnker, Annabelle McIver, Geoff Sutcliffe, and Andrei Voronkov, editors, International Conference on Logic for Programming, Artificial Intelligence and Reasoning - Short Presentations (LPAR), volume 35 of EPiC Series in Computing, pages 28-41. EasyChair, 2015. Google Scholar
  14. Samuel R. Buss. Towards NP-P via proof complexity and search. Annals of Pure and Applied Logic, 163(7):906-917, 2012. Google Scholar
  15. Michael Cashmore, Maria Fox, and Enrico Giunchiglia. Partially Grounded Planning as Quantified Boolean Formula. In Daniel Borrajo, Subbarao Kambhampati, Angelo Oddi, and Simone Fratini, editors, International Conference on Automated Planning and Scheduling (ICAPS). AAAI, 2013. Google Scholar
  16. Stephen A. Cook and Phuong Nguyen. Logical Foundations of Proof Complexity. Cambridge University Press, Cambridge, 2010. Google Scholar
  17. Stephen A. Cook and Robert A. Reckhow. The Relative Efficiency of Propositional Proof Systems. Journal of Symbolic Logic, 44(1):36-50, 1979. Google Scholar
  18. Uwe Egly, Martin Kronegger, Florian Lonsing, and Andreas Pfandler. Conformant planning as a case study of incremental QBF solving. Annals of Mathematics and Artificial Intelligence, 80(1):21-45, 2017. Google Scholar
  19. Uwe Egly, Florian Lonsing, and Magdalena Widl. Long-Distance Resolution: Proof Generation and Strategy Extraction in Search-Based QBF Solving. In Kenneth L. McMillan, Aart Middeldorp, and Andrei Voronkov, editors, International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), volume 8312 of Lecture Notes in Computer Science, pages 291-308. Springer, 2013. Google Scholar
  20. Peter Faymonville, Bernd Finkbeiner, Markus N. Rabe, and Leander Tentrup. Encodings of Bounded Synthesis. In Axel Legay and Tiziana Margaria, editors, International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 10205 of Lecture Notes in Computer Science, pages 354-370, 2017. Google Scholar
  21. Marijn J. H. Heule and Oliver Kullmann. The science of brute force. Communications of the ACM, 60(8):70-79, 2017. Google Scholar
  22. Hans Kleine Büning, Marek Karpinski, and Andreas Flögel. Resolution for Quantified Boolean Formulas. Information and Computation, 117(1):12-18, 1995. Google Scholar
  23. William Klieber, Samir Sapra, Sicun Gao, and Edmund M. Clarke. A Non-prenex, Non-clausal QBF Solver with Game-State Learning. In Ofer Strichman and Stefan Szeider, editors, Interenational Conference on Theory and Applications of Satisfiability Testing (SAT), volume 6175 of Lecture Notes in Computer Science, pages 128-142. Springer, 2010. Google Scholar
  24. Roman Kontchakov, Luca Pulina, Ulrike Sattler, Thomas Schneider, Petra Selmer, Frank Wolter, and Michael Zakharyaschev. Minimal Module Extraction from DL-Lite Ontologies Using QBF Solvers. In Craig Boutilier, editor, International Joint Conference on Artificial Intelligence (IJCAI), pages 836-841. AAAI Press, 2009. Google Scholar
  25. 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
  26. Andrew C. Ling, Deshanand P. Singh, and Stephen Dean Brown. FPGA logic synthesis using quantified boolean satisfiability. In Fahiem Bacchus and Toby Walsh, editors, International Conference on Theory and Applications of Satisfiability Testing (SAT), volume 3569 of Lecture Notes in Computer Science, pages 444-450. Springer, 2005. Google Scholar
  27. Hratch Mangassarian, Andreas G. Veneris, and Marco Benedetti. Robust QBF Encodings for Sequential Circuits with Applications to Verification, Debug, and Test. IEEE Transactions on Computers, 59(7):981-994, 2010. Google Scholar
  28. Joao Marques-Silva and Sharad Malik. Propositional SAT Solving. In Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors, Handbook of Model Checking, pages 247-275. Springer, 2018. Google Scholar
  29. Jakob Nordström. On the interplay between proof complexity and SAT solving. SIGLOG News, 2(3):19-44, 2015. Google Scholar
  30. Tomás Peitl, Friedrich Slivovsky, and Stefan Szeider. Long Distance Q-Resolution with Dependency Schemes. In Nadia Creignou and Daniel Le Berre, editors, International Conference on Theory and Applications of Satisfiability Testing (SAT), volume 9710 of Lecture Notes in Computer Science, pages 500-518. Springer, 2016. Google Scholar
  31. Tomás Peitl, Friedrich Slivovsky, and Stefan Szeider. Dependency Learning for QBF. In Serge Gaspers and Toby Walsh, editors, International Conference on Theory and Practice of Satisfiability Testing (SAT), volume 10491 of Lecture Notes in Computer Science, pages 298-313. Springer, 2017. Google Scholar
  32. Tomás Peitl, Friedrich Slivovsky, and Stefan Szeider. Polynomial-Time Validation of QCDCL Certificates. In Olaf Beyersdorff and Christoph M. Wintersteiger, editors, International Conference on Theory and Practice of Satisfiability Testing (SAT), volume 10929 of Lecture Notes in Computer Science, pages 253-269. Springer, 2018. Google Scholar
  33. Markus N. Rabe. A Resolution-Style Proof System for DQBF. In Serge Gaspers and Toby Walsh, editors, International Conference on Theory and Practice of Satisfiability Testing (SAT), volume 10491 of Lecture Notes in Computer Science, pages 314-325. Springer, 2017. Google Scholar
  34. Horst Samulowitz, Jessica Davies, and Fahiem Bacchus. Preprocessing QBF. In Frédéric Benhamou, editor, International Conference on Principles and Practice of Constraint Programming (CP), volume 4204 of Lecture Notes in Computer Science, pages 514-529. Springer, 2006. Google Scholar
  35. Christoph Scholl and Ralf Wimmer. Dependency Quantified Boolean Formulas: An Overview of Solution Methods and Applications - Extended Abstract. In Olaf Beyersdorff and Christoph M. Wintersteiger, editors, International Conference on Theory and Practice of Satisfiability Testing (SAT), volume 10929 of Lecture Notes in Computer Science, pages 3-16. Springer, 2018. Google Scholar
  36. João P. Marques Silva, Inês Lynce, and Sharad Malik. Conflict-Driven Clause Learning SAT Solvers. In Handbook of Satisfiability, pages 131-153. IOS Press, 2009. Google Scholar
  37. Martin Suda and Bernhard Gleiss. Local Soundness for QBF Calculi. In Olaf Beyersdorff and Christoph M. Wintersteiger, editors, International Conference on Theory and Practice of Satisfiability Testing (SAT), volume 10929 of Lecture Notes in Computer Science, pages 217-234. Springer, 2018. Google Scholar
  38. Moshe Y. Vardi. Boolean satisfiability: Theory and engineering. Communications of the ACM, 57(3):5, 2014. Google Scholar
  39. Lintao Zhang and Sharad Malik. Conflict driven learning in a quantified Boolean Satisfiability solver. In International Conference on Computer-aided Design (ICCAD), pages 442-449, 2002. 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