Skip to main content
SpringerLink
Log in

Lower Bounds for QCDCL via Formula Gauge

  • 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

QCDCL is one of the main algorithmic paradigms for solving quantified Boolean formulas (QBF). We design a new technique to show lower bounds for the running time in QCDCL algorithms. For this we model QCDCL by concisely defined proof systems and identify a new width measure for formulas, which we call gauge. We show that for a large class of QBFs, large (e.g. linear) gauge implies exponential lower bounds for QCDCL proof size.

We illustrate our technique by computing the gauge for a number of sample QBFs, thereby providing new exponential lower bounds for QCDCL. Our technique is the first bespoke lower bound technique for QCDCL.

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

Similar content being viewed by others

Notes

  1. 1.

    The existential width of a clause is defined as the number of existential literals in this clause. The existential proof width is defined as the maximal existential width over all clauses in this proof.

References

  1. Balabanov, V., Jiang, J.H.R.: Unified QBF certification and its applications. Form. 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: Proceedings of Theory and Applications of Satisfiability Testing (SAT), pp. 154–169 (2014)

    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. Ben-Sasson, E., Wigderson, A.: Short proofs are narrow - resolution made simple. J. ACM 48(2), 149–169 (2001)

    Article  MathSciNet  Google Scholar 

  5. Beyersdorff, O., Blinkhorn, J., Hinde, L.: Size, cost, and capacity: a semantic technique for hard random QBFs. Logical Methods Comput. Sci 15(1), 13:1–13:39 (2019)

    Google Scholar 

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

    Google Scholar 

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

  8. Beyersdorff, O., Bonacina, I., Chew, L., Pich, J.: Frege systems for quantified Boolean logic. J. ACM 67(2), 1–36 (2020)

    Google Scholar 

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

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

    Google Scholar 

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

    Google Scholar 

  12. Beyersdorff, O., Chew, L., Sreenivasaiah, K.: A game characterisation of tree-like Q-resolution size. J. Comput. Syst. Sci. 104, 82–101 (2019)

    Article  MathSciNet  Google Scholar 

  13. Beyersdorff, O., Hinde, L., Pich, J.: Reasons for hardness in QBF proof systems. ACM Trans. Comput. Theor. 12(2), 1–27 (2020)

    Google Scholar 

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

  15. Clymo, J., Beyersdorff, O.: Relating size and width in variants of Q-resolution. Inf. Process. Lett. 138, 1–6 (2018)

    Article  MathSciNet  Google Scholar 

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

  17. Giunchiglia, E., Narizzano, M., Tacchella, A.: Clause/term resolution and learning in the evaluation of quantified Boolean formulas. J. Artif. Intell. Res. 26, 371–416 (2006)

    Article  MathSciNet  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

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

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

  22. Krajíček, J.: Proof complexity, Encyclopedia of Mathematics and Its Applications, vol. 170. Cambridge University Press (2019)

    Google Scholar 

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

    Google Scholar 

  24. Lonsing, F., Egly, U.: DepQBF 6.0: A search-based QBF solver beyond traditional QCDCL. In: Proceedings of International Conference on Automated Deduction (CADE), pp. 371–384 (2017)

    Google Scholar 

  25. Lonsing, F., Egly, U.: Evaluating QBF solvers: quantifier alternations matter. In: Hooker, J. (ed.) CP 2018. LNCS, vol. 11008, pp. 276–294. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-98334-9_19

    Chapter  Google Scholar 

  26. Lonsing, F., Egly, U., Seidl, M.: Q-resolution with generalized axioms. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 435–452. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-40970-2_27

    Chapter  Google Scholar 

  27. Marques Silva, J.P., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers. In: Handbook of Satisfiability. IOS Press (2009)

    Google Scholar 

  28. Peitl, T., Slivovsky, F., Szeider, S.: Dependency learning for QBF. J. Artif. Intell. Res. 65, 180–208 (2019)

    Article  MathSciNet  Google Scholar 

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

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

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

    Google Scholar 

  32. Vinyals, M.: Hard examples for common variable decision heuristics. In: Proceedings of the AAAI Conference on Artificial Intelligence (AAAI) (2020)

    Google Scholar 

  33. Zhang, L., Madigan, C.F., Moskewicz, M.W., Malik, S.: Efficient conflict driven learning in Boolean satisfiability solver. In: Proceedings of IEEE/ACM International Conference on Computer-Aided Design (ICCAD), pp. 279–285 (2001)

    Google Scholar 

  34. Zhang, L., Malik, S.: Conflict driven learning in a quantified Boolean satisfiability solver. In: Proceedings of IEEE/ACM International Conference on Computer-aided Design (ICCAD), pp. 442–449 (2002)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Friedrich Schiller University Jena, Jena, Germany

    Benjamin Böhm & Olaf Beyersdorff

Authors
  1. Benjamin Böhm
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Olaf Beyersdorff
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding authors

Correspondence to Benjamin Böhm or Olaf Beyersdorff .

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

Böhm, B., Beyersdorff, O. (2021). Lower Bounds for QCDCL via Formula Gauge. 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_5

Download citation

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

  • 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