Lower Bound Techniques for QBF Expansion | Theory of Computing Systems Skip to main content
Springer Nature Link
Log in

Lower Bound Techniques for QBF Expansion

  • Published:
Theory of Computing Systems Aims and scope Submit manuscript

Abstract

We propose some general techniques for proving lower bounds in expansion-based QBF proof systems. We present them in a framework centred on natural properties of winning strategies in the ‘evaluation game’ interpretation of QBF semantics. As applications, we prove an exponential proof-size lower bound for a whole class of formula families, and demonstrate the power of our approach over existing methods by providing alternative short proofs of two known hardness results. We also use our technique to deduce an interesting result: in the absence of propositional hardness, formulas separating the two major QBF expansion systems must have unbounded quantifier alternations.

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

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (Japan)

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3

Similar content being viewed by others

Notes

  1. Proof system P1 simulates proof system P2 whenever P1-proofs and be transformed into P2-proofs with at most polynomial increase in proof size.

  2. This is our notation; in [30], the formulas are referred to as ‘(2)’.

  3. That such a clause and its subderivation remain is proved as part of Proposition 2. We note that this subderivation may include weakening steps – the addition of arbitrary literals to a clause – but such steps are easily erased from a refutation.

  4. In fact, the authors separated Q-Res from ∀Exp+Res; since IR-calcp-simulates Q-Res [9], the result stated in the text is an immediate corollary.

References

  1. Bacchus, F., Walsh, T. (eds.): International conference on theory and practice of satisfiability testing (SAT), Lecture notes in computer science, vol. 3569. Springer, Berlin (2005)

  2. Balabanov, V., Jiang, J.R., Janota, M., Widl, M.: Efficient extraction of QBF (counter)models from long-distance resolution proofs. In: Conference on artificial intelligence (AAAI), pp. 3694–3701 (2015)

  3. Balabanov, V., Widl, M., Jiang, J.R.: QBF resolution systems and their proof complexities. In: Sinz, C., Egly, U. (eds.) International conference on theory and applications of satisfiability testing (SAT), Lecture notes in computer science, vol. 8561, pp. 154–169. Springer (2014)

  4. Ben-Sasson, E., Wigderson, A.: Short proofs are narrow - resolution made simple. J. ACM 48(2), 149–169 (2001)

    Article  MathSciNet  Google Scholar 

  5. Benedetti, M., Mangassarian, H.: QBF-based formal verification: Experience and perspectives. Journal on Satisfiability Boolean Modeling and Computation (JSAT) 5(1–4), 133–191 (2008)

    Article  MathSciNet  Google Scholar 

  6. Beyersdorff, O., Blinkhorn, J.: Genuine lower bounds for QBF expansion. In: Niedermeier, R., Vallée, B. (eds.) International symposium on theoretical aspects of computer science (STACS), Leibniz international proceedings in informatics (LIPIcs), vol. 96, pp. 12:1–12:15. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2018)

  7. Beyersdorff, O., Blinkhorn, J., Hinde, L.: Size, cost, and capacity: A semantic technique for hard random qbfs. Logical Methods in Computer Science 15(1) (2019)

  8. Beyersdorff, O., Bonacina, I., Chew, L.: Lower bounds: From circuits to QBF proof systems. In: Sudan, M. (ed.) ACM conference on innovations in theoretical computer science (ITCS), pp. 249–260. ACM (2016)

  9. Beyersdorff, O., Chew, L., Janota, M.: On unification of QBF resolution-based calculi. In: Csuhaj-Varjú, E., Dietzfelbinger, M., Ésik, Z. (eds.) International symposium on mathematical foundations of computer science (MFCS), Lecture notes in computer science, vol. 8635, pp. 81–93. Springer (2014)

  10. Beyersdorff, O., Chew, L., Janota, M.: Proof complexity of resolution-based QBF calculi. In: Mayr, E.W., Ollinger, N. (eds.) International symposium on theoretical aspects of computer science (STACS), Leibniz international proceedings in informatics (LIPIcs), vol. 30, pp. 76–89. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2015)

  11. Beyersdorff, O., Chew, L., Mahajan, M., Shukla, A.: Feasible interpolation for QBF resolution calculi. Logical Methods in Computer Science 13 (2017)

  12. Beyersdorff, O., Chew, L., Mahajan, M., Shukla, A.: Are short proofs narrow? QBF resolution is not so simple. ACM Trans. Comput. Log. 19(1), 1:1–1:26 (2018)

    MathSciNet  MATH  Google Scholar 

  13. Beyersdorff, O., Chew, L., Sreenivasaiah, K.: A game characterisation of tree-like Q-resolution size. Journal of Computer and System Sciences. In press (2017)

  14. Beyersdorff, O., Galesi, N., Lauria, M.: A characterization of tree-like resolution size. Inf. Process. Lett. 113(18), 666–671 (2013)

    Article  MathSciNet  Google Scholar 

  15. Beyersdorff, O., Hinde, L., Pich, J.: Reasons for hardness in QBF proof systems. In: Conference on foundations of software technology and theoretical computer science (FSTTCS) (2017)

  16. Buss, S.R.: Towards NP-P via proof complexity and search. Ann. Pure Appl. Logic 163(7), 906–917 (2012)

    Article  MathSciNet  Google Scholar 

  17. Cashmore, M., Fox, M., Giunchiglia, E.: Partially grounded planning as quantified Boolean formula. In: Borrajo, D., Kambhampati, S., Oddi, A., Fratini, S. (eds.) International conference on automated planning and scheduling (ICAPS). AAAI (2013)

  18. Chen, H.: Proof complexity modulo the polynomial hierarchy: Understanding alternation as a source of hardness. ACM Trans. Comput. Theory 9(3), 15:1–15:20 (2017)

    MathSciNet  MATH  Google Scholar 

  19. Cook, S.A., Nguyen, P.: Logical foundations of proof complexity. Cambridge University Press, Cambridge (2010)

    Book  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  21. Craig, W.: Linear reasoning. A new form of the Herbrand-Gentzen Theorem. J. Symb. Log. 22(3), 250–268 (1957)

    Article  MathSciNet  Google Scholar 

  22. Creignou, N., Berre, D.L. (eds.): International conference on theory and practice of satisfiability testing (SAT), Lecture notes in computer science, vol. 9710. Springer, Berlin (2016)

  23. Dershowitz, N., Hanna, Z., Katz, J.: Space-efficient bounded model checking. In: Bacchus and Walsh [1], pp. 502–518

  24. Egly, U.: On stronger calculi for QBFs. In: Creignou and Berre [22], pp. 419–434

  25. Egly, U., Kronegger, M., Lonsing, F., Pfandler, A.: Conformant planning as a case study of incremental QBF solving. Ann. Math. Artif. Intell. 80(1), 21–45 (2017)

    Article  MathSciNet  Google Scholar 

  26. Egly, U., Lonsing, F., Widl, M.: Long-distance resolution: Proof generation and strategy extraction in search-based QBF solving. In: International conference on logic for programming, artificial intelligence and reasoning (LPAR), pp. 291–308 (2013)

  27. Giunchiglia, E., Marin, P., Narizzano, M.: Reasoning with 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. 761–780. IOS Press (2009)

  28. Giunchiglia, E., Narizzano, M., Tacchella, A.: QBF reasoning on real-world instances. In: International conference on theory and applications of satisfiability testing (SAT), online proceedings (2004)

  29. Janota, M., Klieber, W., Marques-Silva, J., Clarke, E.M.: Solving QBF with counterexample guided refinement. Artif. Intell. 234, 1–25 (2016)

    Article  MathSciNet  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  31. Jordan, C., Kaiser, L.: Experiments with reduction finding. In: Järvisalo, M., Gelder, A.V. (eds.) International conference on theory and applications of satisfiability testing (SAT), Lecture notes in computer science, vol. 7962, pp. 192–207. Springer (2013)

  32. 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 

  33. Kontchakov, R., Pulina, L., Sattler, U., Schneider, T., Selmer, P., Wolter, F., Zakharyaschev, M.: Minimal module extraction from DL-lite ontologies using QBF solvers. In: Boutilier, C. (ed.) International joint conference on artificial intelligence (IJCAI), pp. 836–841. AAAI Press (2009)

  34. Krajíček, J.: Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic. J. Symb. Log. 62(2), 457–486 (1997)

    Article  MathSciNet  Google Scholar 

  35. 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 

  36. Ling, A.C., Singh, D.P., Brown, S.D.: FPGA logic synthesis using quantified boolean satisfiability. In: Bacchus and Walsh [1], pp. 444–450

  37. Lonsing, F., Egly, U., Seidl, M.: Q-resolution with generalized axioms. In: Creignou and Berre [22], pp. 435–452

  38. Mangassarian, H., Veneris, A.G., Benedetti, M.: Robust QBF encodings for sequential circuits with applications to verification, debug, and test. IEEE Trans. Comput. 59(7), 981–994 (2010)

    Article  MathSciNet  Google Scholar 

  39. Mangassarian, H., Veneris, A.G., Safarpour, S., Benedetti, M., Smith, D.E.: A performance-driven QBF-based iterative logic array representation with applications to verification, debug and test. In: International conference on computer-aided design (ICCAD), pp. 240–245 (2007)

  40. Peitl, T., Slivovsky, F., Szeider, S.: Long distance Q-resolution with dependency schemes. In: Creignou and Berre [22], pp. 500–518

  41. Pudlák, P., Impagliazzo, R.: A lower bound for DLL algorithms for k-SAT (preliminary version). In: Shmoys, D.B. (ed.) Symposium on Discrete Algorithms, pp. 128–136. ACM/SIAM (2000)

  42. Rintanen, J.: Asymptotically optimal encodings of conformant planning in QBF. In: National conference on artificial intelligence (AAAI), pp. 1045–1050. AAAI Press (2007)

  43. Segerlind, N.: The complexity of propositional proofs. Bull. Symb. Log. 13(4), 417–481 (2007)

    Article  MathSciNet  Google Scholar 

  44. Staber, S., Bloem, R.: Fault localization and correction with QBF. In: Marques-Silva, J., Sakallah, K.A. (eds.) International conference on theory and applications of satisfiability testing (SAT), Lecture notes in computer science, vol. 4501, pp. 355–368. Springer (2007)

  45. Stockmeyer, L.J., Meyer, A.R.: Word problems requiring exponential time: Preliminary report. In: Aho, A.V., Borodin, A., Constable, R.L., Floyd, R.W., Harrison, M.A., Karp, R.M., Strong, H.R. (eds.) ACM symposium on theory of computing (STOC), pp. 1–9. ACM (1973)

Download references

Acknowledgments

We thank Meena Mahajan and Anil Shukla for helpful discussions on this work.

Author information

Authors and Affiliations

  1. Institut für Informatik, Friedrich Schiller Universität Jena, Jena, Germany

    Olaf Beyersdorff & Joshua Blinkhorn

Authors
  1. Olaf Beyersdorff
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Joshua Blinkhorn
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Joshua Blinkhorn.

Additional information

Publisher’s Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

This article is part of the Topical Collection on Special Issue on Theoretical Aspects of Computer Science (2018)

An extended abstract of this article appeared in the proceedings of the conference STACS’18 [6]. Research was supported by grants from the John Templeton Foundation (grant no. 60842), the Carl-Zeiss Foundation, and the EU (Marie Curie IRSES project CORCON).

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Beyersdorff, O., Blinkhorn, J. Lower Bound Techniques for QBF Expansion. Theory Comput Syst 64, 400–421 (2020). https://doi.org/10.1007/s00224-019-09940-0

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s00224-019-09940-0

Keywords

Search

Navigation