Document Open Access Logo

Towards Uniform Certification in QBF

Authors Leroy Chew , Friedrich Slivovsky

PDF
Thumbnail PDF

File

LIPIcs.STACS.2022.22.pdf
  • Filesize: 0.9 MB
  • 23 pages

Document Identifiers

Author Details

Leroy Chew
  • TU Wien, Austria
Friedrich Slivovsky
  • TU Wien, Austria

Funding

This work was supported by the Vienna Science and Technology Fund (WWTF) under grant ICT19-060.

Cite AsGet BibTex

Leroy Chew and Friedrich Slivovsky. Towards Uniform Certification in QBF. In 39th International Symposium on Theoretical Aspects of Computer Science (STACS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 219, pp. 22:1-22:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.STACS.2022.22

Abstract

We pioneer a new technique that allows us to prove a multitude of previously open simulations in QBF proof complexity. In particular, we show that extended QBF Frege p-simulates clausal proof systems such as IR-Calculus, IRM-Calculus, Long-Distance Q-Resolution, and Merge Resolution. These results are obtained by taking a technique of Beyersdorff et al. (JACM 2020) that turns strategy extraction into simulation and combining it with new local strategy extraction arguments. This approach leads to simulations that are carried out mainly in propositional logic, with minimal use of the QBF rules. Our proofs therefore provide a new, largely propositional interpretation of the simulated systems. We argue that these results strengthen the case for uniform certification in QBF solving, since many QBF proof systems now fall into place underneath extended QBF Frege.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
Keywords
  • QBF
  • Proof Complexity
  • Verification
  • Frege
  • Extended Frege
  • Strategy Extraction

Metrics

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

Related Versions

References

  1. Sanjeev Arora and Boaz Barak. Computational Complexity: A Modern Approach. Cambridge University Press, 2009. Google Scholar
  2. Valeriy Balabanov and Jie-Hong R. Jiang. Unified QBF certification and its applications. Formal Methods in System Design, 41(1):45-65, 2012. URL: https://doi.org/10.1007/s10703-012-0152-6.
  3. Valeriy Balabanov, Magdalena Widl, and Jie-Hong R. Jiang. QBF resolution systems and their proof complexities. In SAT 2014, pages 154-169, 2014. Google Scholar
  4. Olaf Beyersdorff. On the correspondence between arithmetic theories and propositional proof systems - a survey. Mathematical Logic Quarterly, 55(2):116-137, 2009. Google Scholar
  5. Olaf Beyersdorff, Joshua Blinkhorn, and M. Mahajan. Building strategies into QBF proofs. In Electron. Colloquium Comput. Complex., 2018. Google Scholar
  6. Olaf Beyersdorff, Ilario Bonacina, Leroy Chew, and Jan Pich. Frege systems for quantified Boolean logic. J. ACM, 67(2), April 2020. Google Scholar
  7. Olaf Beyersdorff, Leroy Chew, and Mikolás Janota. New resolution-based QBF calculi and their proof complexity. ACM Trans. Comput. Theory, 11(4):26:1-26:42, 2019. URL: https://doi.org/10.1145/3352155.
  8. Olaf Beyersdorff, Leroy Chew, Meena Mahajan, and Anil Shukla. Understanding Cutting Planes for QBFs. In FSTTCS 2016, volume 65 of Leibniz International Proceedings in Informatics (LIPIcs), pages 40:1-40:15, 2016. Google Scholar
  9. Robert Brummayer, Florian Lonsing, and Armin Biere. Automated testing and debugging of SAT and QBF solvers. In SAT 2010, volume 6175 of Lecture Notes in Computer Science, pages 44-57. Springer, 2010. Google Scholar
  10. Sravanthi Chede and Anil Shukla. Does QRAT simulate IR-calc? QRAT simulation algorithm for ∀Exp+Res cannot be lifted to IR-calc. Electron. Colloquium Comput. Complex., page 104, 2021. Google Scholar
  11. Hubie Chen. Proof complexity modulo the polynomial hierarchy: Understanding alternation as a source of hardness. In ICALP 2016, pages 94:1-94:14, 2016. Google Scholar
  12. Leroy Chew. Hardness and optimality in QBF proof systems modulo NP. In SAT 2021, pages 98-115, Cham, 2021. Springer. Google Scholar
  13. Leroy Chew and Marijn Heule. Relating existing powerful proof systems for QBF. Electron. Colloquium Comput. Complex., 27:159, 2020. URL: https://eccc.weizmann.ac.il/report/2020/159.
  14. Stephen A. Cook and Robert A. Reckhow. The relative efficiency of propositional proof systems. The Journal of Symbolic Logic, 44(1):36-50, 1979. Google Scholar
  15. Luís Cruz-Filipe, Marijn J. H. Heule, Warren A. Hunt Jr., Matt Kaufmann, and Peter Schneider-Kamp. Efficient certified RAT verification. In CADE 2017, volume 10395 of Lecture Notes in Computer Science, pages 220-236. Springer, 2017. Google Scholar
  16. 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, LPAR 2013, pages 291-308. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-45221-5_21.
  17. Alexandra Goultiaeva, Allen Van Gelder, and Fahiem Bacchus. A uniform approach for generating proofs and strategies for both true and false QBF formulas. In Toby Walsh, editor, IJCAI 2011, pages 546-553. IJCAI/AAAI, 2011. URL: http://ijcai.org/papers11/Papers/IJCAI11-099.pdf.
  18. Marijn J. H. Heule, Martina Seidl, and Armin Biere. Solution validation and extraction for QBF preprocessing. J. Autom. Reason., 58(1):97-125, 2017. Google Scholar
  19. Mikolás Janota, William Klieber, João Marques-Silva, and Edmund M. Clarke. Solving QBF with counterexample guided refinement. Artif. Intell., 234:1-25, 2016. Google Scholar
  20. Mikolás Janota and João Marques-Silva. Solving QBF by clause selection. In IJCAI 2015, pages 325-331. AAAI Press, 2015. Google Scholar
  21. Mikoláš Janota and Joao Marques-Silva. Expansion-based QBF solving versus Q-resolution. Theor. Comput. Sci., 577:25-42, 2015. Google Scholar
  22. Toni Jussila, Armin Biere, Carsten Sinz, Daniel Kröning, and Christoph M. Wintersteiger. A first step towards a unified proof checker for QBF. In SAT 2007, pages 201-214, 2007. URL: https://doi.org/10.1007/978-3-540-72788-0_21.
  23. Benjamin Kiesl, Marijn J. H. Heule, and Martina Seidl. A little blocked literal goes a long way. In SAT 2017, volume 10491 of Lecture Notes in Computer Science, pages 281-297. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-66263-3_18.
  24. Benjamin Kiesl and Martina Seidl. QRAT polynomially simulates ∀Exp+Res. In SAT 2019, volume 11628 of Lecture Notes in Computer Science, pages 193-202. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-24258-9_13.
  25. 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.
  26. Jan Krajíček. Proof complexity, volume 170. Cambridge University Press, 2019. Google Scholar
  27. 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
  28. Jan Krajíček and Pavel Pudlák. Quantified propositional calculi and fragments of bounded arithmetic. Zeitschrift für mathematische Logik und Grundlagen der Mathematik, 36:29-46, 1990. Google Scholar
  29. Florian Lonsing and Armin Biere. Integrating dependency schemes in search-based QBF solvers. In SAT 2010, volume 6175 of Lecture Notes in Computer Science, pages 158-171. Springer, 2010. Google Scholar
  30. Tomás Peitl, Friedrich Slivovsky, and Stefan Szeider. Dependency learning for QBF. J. Artif. Intell. Res., 65:180-208, 2019. Google Scholar
  31. Tomás Peitl, Friedrich Slivovsky, and Stefan Szeider. Long-distance Q-Resolution with dependency schemes. J. Autom. Reason., 63(1):127-155, 2019. Google Scholar
  32. Markus N Rabe and Leander Tentrup. CAQE: A certifying QBF solver. In FMCAD 2015, pages 136-143. FMCAD Inc, 2015. Google Scholar
  33. Robert A. Reckhow. On the lengths of proofs in the propositional calculus. PhD thesis, University of Toronto, 1976. Google Scholar
  34. Matthias Schlaipfer, Friedrich Slivovsky, Georg Weissenbacher, and Florian Zuleger. Multi-linear strategy extraction for QBF expansion proofs via local soundness. In SAT 2020, volume 12178 of Lecture Notes in Computer Science, pages 429-446. Springer, 2020. Google Scholar
  35. Ankit Shukla, Armin Biere, Luca Pulina, and Martina Seidl. A survey on applications of quantified Boolean formulas. In ICTAI 2019, pages 78-84. IEEE, 2019. Google Scholar
  36. L. J. Stockmeyer and A. R. Meyer. Word problems requiring exponential time. Proc. 5th ACM Symposium on Theory of Computing, pages 1-9, 1973. Google Scholar
  37. Martin Suda and Bernhard Gleiss. Local soundness for QBF calculi. In SAT 2018, volume 10929 of Lecture Notes in Computer Science, pages 217-234. Springer, 2018. Google Scholar
  38. Allen Van Gelder. Contributions to the theory of practical quantified Boolean formula solving. In Principles and Practice of Constraint Programming, pages 647-663. Springer, 2012. Google Scholar
  39. Nathan Wetzler, Marijn Heule, and Warren A. Hunt Jr. DRAT-trim: Efficient checking and trimming using expressive clausal proofs. In SAT 2014, volume 8561 of Lecture Notes in Computer Science, pages 422-429. Springer, 2014. Google Scholar
  40. Lintao Zhang and Sharad Malik. Conflict driven learning in a quantified Boolean satisfiability solver. In ICCAD 2002, 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