Skip to main content
SpringerLink
Log in

QBFFam: A Tool for Generating QBF Families from Proof Complexity

  • 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))

Abstract

We present QBFFam, a tool for the generation of formula families originating from the field of proof complexity. Such formula families are used to investigate the strength of proof systems and to show how they relate to each other in terms of simulations and separations. Furthermore, these proof systems underlie the reasoning power of QBF solvers. With our tool, it is possible to generate informative and scalable benchmarks that help to analyse the behavior of solvers. As we will see in this paper, runtime behavior predicted by proof complexity is indeed reflected by recent solver implementations.

This work has been supported by the Austrian Science Fund (FWF) under project W1255-N23, the LIT AI Lab funded by the State of Upper Austria, and a grant by the Carl Zeiss Foundation.

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

Notes

  1. 1.

    http://www.qbflib.org/qdimacs.html.

  2. 2.

    However, formulas hard for QRes-LD such as LQParity are hard for QCDCL (with arbitrary heuristics) from a theory point of view.

  3. 3.

    http://www.qbfeval.org.

References

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

    Article  Google Scholar 

  2. Balabanov, V., Widl, M., Jiang, J.-H.R.: QBF resolution systems and their proof complexities. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 154–169. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-09284-3_12

    Chapter  MATH  Google Scholar 

  3. Beame, P., Kautz, H.A., Sabharwal, A.: Towards understanding and harnessing the potential of clause learning. J. Artif. Intell. Res. (JAIR) 22, 319–351 (2004)

    Article  MathSciNet  Google Scholar 

  4. Beyersdorff, O., Blinkhorn, J.: Dynamic QBF dependencies in reduction and expansion. ACM Trans. Comput. Log. 21(2), 8:1–8:27 (2020)

    Google Scholar 

  5. Beyersdorff, O., Blinkhorn, J.: A simple proof of QBF hardness. Inf. Process. Lett. 168, 106093 (2021)

    Google Scholar 

  6. Beyersdorff, O., Blinkhorn, J., Hinde, L.: Size, cost, and capacity: A semantic technique for hard random QBFS. Log. Methods Comput. Sci. 15(1), 13:1–13:39 (2019)

    Google Scholar 

  7. Beyersdorff, O., Blinkhorn, J., Mahajan, M.: Hardness characterisations and size-width lower bounds for QBF resolution. In: Proceedings ACM/IEEE Symposium on Logic in Computer Science (LICS), pp. 209–223. ACM (2020)

    Google Scholar 

  8. Beyersdorff, O., Blinkhorn, J., Mahajan, M.: Building strategies into QBF proofs. J. Autom. Reasoning 65(1), 125–154 (2021)

    Article  MathSciNet  Google Scholar 

  9. Beyersdorff, O., Böhm, B.: Understanding the relative strength of QBF CDCL solvers and QBF resolution. In: Proceedings of Innovations in Theoretical Computer Science (ITCS), pp. 12:1–12:20 (2021)

    Google Scholar 

  10. Beyersdorff, O., Chew, L., Janota, M.: New resolution-based QBF calculi and their proof complexity. ACM Trans. Comput. Theor. 11(4), 26:1–26:42 (2019)

    Google Scholar 

  11. Beyersdorff, O., Chew, L., Mahajan, M., Shukla, A.: Feasible interpolation for QBF resolution calculi. Logical Methods Comput. Sci. 13(2), 1–20 (2017)

    Google Scholar 

  12. Beyersdorff, O., Janota, M., Lonsing, F., Seidl, M.: Quantified Boolean formulas. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, 2nd edn. IOS press, Frontiers in Artificial Intelligence and Applications (2021)

    Google Scholar 

  13. Blinkhorn, J., Beyersdorff, O.: Proof complexity of QBF symmetry recomputation. In: Janota, M., Lynce, I. (eds.) SAT 2019. LNCS, vol. 11628, pp. 36–52. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-24258-9_3

    Chapter  MATH  Google Scholar 

  14. Brummayer, R., Lonsing, F., Biere, A.: Automated testing and debugging of SAT and QBF solvers. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 44–57. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14186-7_6

    Chapter  MATH  Google Scholar 

  15. Chen, H., Interian, Y.: A model for generating random quantified boolean formulas. In: Proc. of the 19th International Joint Conferences on Artificial Intelligence (IJCAI 2005), pp. 66–71. Professional Book Center (2005)

    Google Scholar 

  16. Chew, L.: QBF proof complexity. Ph.D. thesis, University of Leeds, Leeds (2017)

    Google Scholar 

  17. Creignou, N., Daudé, H., Egly, U., Rossignol, R.: New results on the phase transition for random quantified Boolean formulas. In: Kleine Büning, H., Zhao, X. (eds.) SAT 2008. LNCS, vol. 4996, pp. 34–47. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-79719-7_5

    Chapter  Google Scholar 

  18. Creignou, N., Egly, U., Seidl, M.: A framework for the specification of random SAT and QSAT formulas. In: Brucker, A.D., Julliand, J. (eds.) TAP 2012. LNCS, vol. 7305, pp. 163–168. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-30473-6_14

    Chapter  Google Scholar 

  19. Egly, U., Lonsing, F., Widl, M.: Long-distance resolution: proof generation and strategy extraction in search-based QBF solving. In: Proceedings of Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), pp. 291–308 (2013)

    Google Scholar 

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

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

    Article  MathSciNet  Google Scholar 

  22. Håstad, J.: Computational Limitations of Small Depth Circuits. MIT Press, Cambridge (1987)

    Google Scholar 

  23. Janota, M.: On Q-resolution and CDCL QBF solving. In: Proceedings of International Conference on Theory and Applications of Satisfiability Testing (SAT), pp. 402–418 (2016)

    Google Scholar 

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

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

    Article  MathSciNet  Google Scholar 

  26. Kauers, M., Seidl, M.: Short proofs for some symmetric quantified Boolean formulas. Inf. Process. Lett. 140, 4–7 (2018)

    Article  MathSciNet  Google Scholar 

  27. Kauers, M., Seidl, M.: Symmetries of quantified Boolean formulas. In: Beyersdorff, O., Wintersteiger, C.M. (eds.) SAT 2018. LNCS, vol. 10929, pp. 199–216. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-94144-8_13

    Chapter  MATH  Google Scholar 

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

  29. Lauria, M., Elffers, J., Nordström, J., Vinyals, M.: CNFgen: a generator of crafted benchmarks. In: Gaspers, S., Walsh, T. (eds.) SAT 2017. LNCS, vol. 10491, pp. 464–473. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66263-3_30

    Chapter  MATH  Google Scholar 

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

    Google Scholar 

  31. Lonsing, F., Egly, U.: DepQBF 6.0: a search-based QBF solver beyond traditional QCDCL. In: de Moura, L. (ed.) CADE 2017. LNCS (LNAI), vol. 10395, pp. 371–384. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63046-5_23

    Chapter  Google Scholar 

  32. Peitl, T., Slivovsky, F., Szeider, S.: Qute in the QBF evaluation 2018. J. Satisf. Boolean Model. Comput. 11(1), 261–272 (2019)

    MathSciNet  Google Scholar 

  33. Pipatsrisawat, K., Darwiche, A.: On the power of clause-learning SAT solvers as resolution engines. Artif. Intell. 175(2), 512–525 (2011)

    Article  MathSciNet  Google Scholar 

  34. Pulina, L., Seidl, M.: The 2016 and 2017 QBF solvers evaluations (qbfeval’16 and qbfeval’17). Artif. Intell. 274, 224–248 (2019)

    Article  MathSciNet  Google Scholar 

  35. Shukla, A., Biere, A., Pulina, L., Seidl, M.: A survey on applications of quantified boolean formulas. In: Proceedings of the the 31st IEEE International Conferences on Tools with Artificial Intelligence, (ICTAI 2019), pp. 78–84. IEEE (2019)

    Google Scholar 

  36. Tentrup, L.: CAQE and quabs: Abstraction based QBF solvers. J. Satisf. Boolean Model. Comput. 11(1), 155–210 (2019)

    MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Friedrich Schiller University Jena, Jena, Germany

    Olaf Beyersdorff

  2. University of Sassari, Sassari, Italy

    Luca Pulina

  3. Johannes Kepler University Linz, Linz, Austria

    Martina Seidl & Ankit Shukla

Authors
  1. Olaf Beyersdorff
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Luca Pulina
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Martina Seidl
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Ankit Shukla
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Ankit Shukla .

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

Beyersdorff, O., Pulina, L., Seidl, M., Shukla, A. (2021). QBFFam: A Tool for Generating QBF Families from Proof Complexity. 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_3

Download citation

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

  • 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