Skip to main content
SpringerLink
Log in

Hardness and Optimality in QBF Proof Systems Modulo NP

  • Conference paper
  • First Online:
Theory and Applications of Satisfiability Testing – SAT 2021 (SAT 2021)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 12831))

  • 1752 Accesses

Abstract

In this paper we show that extended Q-resolution is optimal among all QBF proof systems that allow strategy extraction modulo an NP oracle. In other words, for any QBF refutation system f where circuits witnessing the Herbrand functions can be extracted in polynomial time from f-refutations, f can be simulated by extended Q-resolution augmented with an NP oracle as described by Beyersdorff et al. We argue that using NP oracles and strategy extraction gives a natural framework to study QBF systems as they have relations to SAT calls and game instances, respectively, in QBF solving.

A weaker version of QBF extension variables also put forward by Jussila et al. does not have this optimality result, and we show that under an NP oracle there is no improvement of weak extended Q-Resolution compared to ordinary Q-Resolution.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 89.00
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 119.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Arora, S., Barak, B.: Computational Complexity - A Modern Approach. Cambridge University Press, Cambridge (2009)

    Google Scholar 

  2. Balabanov, V., Jiang, J.H.R.: Unified QBF certification and its applications. Formal Methods Syst. Des. 41(1), 45–65 (2012)

    Article  Google Scholar 

  3. Bellatoni, S., Pitassi, T., Urquhart, A.: Approximation of small-depth Frege proofs. SIAM J. Comput. 21, 1161–1179 (1992)

    Article  MathSciNet  Google Scholar 

  4. Beyersdorff, O., Blinkhorn, J., Hinde, L.: Size, cost, and capacity: a semantic technique for hard random QBFs. CoRR abs/1712.03626 (2017). http://arxiv.org/abs/1712.03626

  5. Beyersdorff, O., Bonacina, I., Chew, L., Pich, J.: Frege systems for quantified boolean logic. J. ACM 67(2), (2020). https://doi.org/10.1145/3381881

  6. Beyersdorff, O., Chew, L., Janota, M.: New resolution-based QBF calculi and their proof complexity. ACM Trans. Comput. Theory 11(4), 26:1–26:42 (2019). https://doi.org/10.1145/3352155

  7. Beyersdorff, O., Chew, L., Janota, M.: Extension variables in QBF resolution. In: Beyond, N.P.: Papers from the 2016 AAAI Workshop (2016). http://www.aaai.org/ocs/index.php/WS/AAAIW16/paper/view/12612

  8. Beyersdorff, O., Hinde, L., Pich, J.: Reasons for hardness in QBF proof systems. Electron. Colloquium Comput. Complexity (ECCC) 24, 44 (2017). https://eccc.weizmann.ac.il/report/2017/044

  9. Blinkhorn, J.L.: Quantified Boolean Formulas: Proof Complexity and Models of Solving. Ph.D. thesis, University of Leeds (2019)

    Google Scholar 

  10. Chen, H.: Proof complexity modulo the polynomial hierarchy: Understanding alternation as a source of hardness. In: ICALP, pp. 94:1–94:14 (2016)

    Google Scholar 

  11. Chew, L., Clymo, J.: How QBF expansion makes strategy extraction hard. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) IJCAR 2020. LNCS (LNAI), vol. 12166, pp. 66–82. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-51074-9_5

    Chapter  Google Scholar 

  12. Cook, S.A., Reckhow, R.A.: The relative efficiency of propositional proof systems. J. Symbolic Logic 44(1), 36–50 (1979)

    Article  MathSciNet  Google Scholar 

  13. Feldman, A., Kleer, J., Matei, I.: Design space exploration as quantified satisfaction (05 2019)

    Google Scholar 

  14. Furst, M.L., Saxe, J.B., Sipser, M.: Parity, circuits, and the polynomial-time hierarchy. Math. Syst. Theory 17(1), 13–27 (1984)

    Article  MathSciNet  Google Scholar 

  15. Goultiaeva, A., Van Gelder, A., Bacchus, F.: A uniform approach for generating proofs and strategies for both true and false QBF formulas. In: Walsh, T. (ed.) International Joint Conference on Artificial Intelligence IJCAI, pp. 546–553. IJCAI/AAAI (2011)

    Google Scholar 

  16. Haken, A.: The intractability of resolution. Theor. Comput. Sci. 39, 297–308 (1985)

    Article  MathSciNet  Google Scholar 

  17. Håstad, J.: One-way permutations in NC\(^0\). Inf. Process. Lett. 26(3), 153–155 (1987)

    Article  MathSciNet  Google Scholar 

  18. Heule, M., Seidl, M., Biere, A.: A unified proof system for QBF preprocessing. In: 7th International Joint Conference on Automated Reasoning (IJCAR), pp. 91–106 (2014)

    Google Scholar 

  19. Janota, M., Klieber, W., Marques-Silva, J., Clarke, E.: Solving QBF with counterexample guided refinement. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 114–128. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31612-8_10

    Chapter  Google Scholar 

  20. Janota, M., Marques-Silva, J.: Expansion-based QBF solving versus Q-resolution. Theor. Comput. Sci. 577, 25–42 (2015)

    Article  MathSciNet  Google Scholar 

  21. Jeřábek, E.: Dual weak pigeonhole principle, Boolean complexity, and derandomization. Ann. Pure Appl. Logic 129, 1–37 (2004)

    Article  MathSciNet  Google Scholar 

  22. Jussila, T., Biere, A., Sinz, C., Kröning, D., Wintersteiger, C.M.: A first step towards a unified proof checker for QBF. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 201–214. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-72788-0_21

    Chapter  Google Scholar 

  23. Kiesl, B., Heule, M.J.H., Seidl, M.: A little blocked literal goes a long way. In: Gaspers, S., Walsh, T. (eds.) SAT 2017. LNCS, vol. 10491, pp. 281–297. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66263-3_18

    Chapter  Google Scholar 

  24. Kiesl, B., Seidl, M.: QRAT polynomially simulates \(\forall \text{-Exp+Res }\). In: Janota, M., Lynce, I. (eds.) SAT 2019. LNCS, vol. 11628, pp. 193–202. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-24258-9_13

    Chapter  Google Scholar 

  25. Kleine Büning, H., Bubeck, U.: Theory of quantified Boolean formulas. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 735–760. IOS Press (2009)

    Google Scholar 

  26. Kleine Büning, H., Karpinski, M., Flögel, A.: Resolution for quantified Boolean formulas. Inf. Comput. 117(1), 12–18 (1995)

    Article  MathSciNet  Google Scholar 

  27. Krajíček, J.: Bounded Arithmetic, Propositional Logic, and Complexity Theory, Encyclopedia of Mathematics and Its Applications, vol. 60. Cambridge University Press, Cambridge (1995)

    MATH  Google Scholar 

  28. Lonsing, F.: Dependency Schemes and Search-Based QBF Solving: Theory and Practice. Ph.D. thesis, Informatik, Johannes Kepler University Linz (2012)

    Google Scholar 

  29. Lonsing, F., Biere, A.: DepQBF: a dependency-aware QBF solver. JSAT 7(2–3), 71–76 (2010)

    Google Scholar 

  30. Messner, J., Torán, J.: Optimal proof systems for propositional logic and complete sets. Technical Report, TR97-026, Electronic Colloquium on Computational Complexity, a revised version appears at STACS’98 (1997)

    Google Scholar 

  31. Papadimitriou, C.H.: Computational Complexity. Addison-Wesley, Boston (1994)

    Google Scholar 

  32. Slivovsky, F.: Structure in# SAT and QBF. Ph.D. thesis (2015)

    Google Scholar 

  33. Tseitin, G.S.: On the complexity of proof in prepositional calculus. Zapiski Nauchnykh Seminarov POMI 8, 234–259 (1968)

    MathSciNet  MATH  Google Scholar 

  34. Gelder, A.: Contributions to the theory of practical quantified Boolean formula solving. In: Milano, M. (ed.) CP 2012. LNCS, pp. 647–663. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-33558-7_47

    Chapter  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Technische Universität Wien, Vienna, Austria

    Leroy Chew

Authors
  1. Leroy Chew
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Leroy Chew .

Editor information

Editors and Affiliations

  1. Laboratoire MIS, University of Picardie Jules Verne, Amiens, France

    Chu-Min Li

  2. IIIA-CSIC, Spanish National Research Council (CSIC), Bellaterra, Barcelona, Spain

    Felip Manyà

Rights and permissions

Reprints and permissions

Copyright information

© 2021 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Chew, L. (2021). Hardness and Optimality in QBF Proof Systems Modulo NP. In: Li, CM., Manyà, F. (eds) Theory and Applications of Satisfiability Testing – SAT 2021. SAT 2021. Lecture Notes in Computer Science(), vol 12831. Springer, Cham. https://doi.org/10.1007/978-3-030-80223-3_8

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-80223-3_8

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-80222-6

  • Online ISBN: 978-3-030-80223-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation