Skip to main content
SpringerLink
Log in
Book cover

International Conference on Principles and Practice of Constraint Programming

CP 2016: Principles and Practice of Constraint Programming pp 96–112Cite as

Dependency Schemes in QBF Calculi: Semantics and Soundness

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 9892))

Abstract

We study the parametrisation of QBF resolution calculi by dependency schemes. One of the main problems in this area is to understand for which dependency schemes the resulting calculi are sound. Towards this end we propose a semantic framework for variable independence based on ‘exhibition’ by QBF models, and use it to express a property of dependency schemes called full exhibition that is known to be sufficient for soundness in Q-resolution. Introducing a generalised form of the long-distance resolution rule, we propose a complete parametrisation of classical long-distance Q-resolution, and show that full exhibition remains sufficient for soundness. We demonstrate that our approach applies to the current research frontiers by proving that the reflexive resolution path dependency scheme is fully exhibited.

This is a preview of subscription content, 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   84.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   109.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

Learn about institutional subscriptions

Notes

  1. 1.

    The term ‘dependency scheme’ was first introduced to denote a subset of proto-dependency schemes with a more technical definition [18]; for consistency with the literature we will use ‘proto-dependency scheme’ in technical portions of this paper.

  2. 2.

    Full exhibition is treated equivalently, as a property of models.

  3. 3.

    We can prove what we need to from the definition of such functions; we need not represent them explicitly as circuits as in [2].

References

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

    Article  MATH  Google Scholar 

  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)

    Google Scholar 

  3. 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, Heidelberg (2014)

    Google Scholar 

  4. Beyersdorff, O., Bonacina, I., Chew, L.: Lower bounds: from circuits to QBF proof systems. In: Proceedings of the ACM Conference on Innovations in Theoretical Computer Science (ITCS 2016), pp. 249–260. ACM (2016)

    Google Scholar 

  5. Beyersdorff, O., Chew, L., Janota, M.: On unification of QBF resolution-based calculi. In: Csuhaj-Varjú, E., Dietzfelbinger, M., Ésik, Z. (eds.) MFCS 2014, Part II. LNCS, vol. 8635, pp. 81–93. Springer, Heidelberg (2014)

    Google Scholar 

  6. Beyersdorff, O., Chew, L., Janota, M.: Proof complexity of resolution-based QBF calculi. In: International Symposium on Theoretical Aspects of Computer Science (STACS). Leibniz International Proceedings in Informatics (LIPIcs), vol. 30, pp. 76–89 (2015)

    Google Scholar 

  7. Beyersdorff, O., Chew, L., Mahajan, M., Shukla, A.: Feasible interpolation for QBF resolution calculi. In: Halldórsson, M.M., Iwama, K., Kobayashi, N., Speckmann, B. (eds.) ICALP 2015. LNCS, vol. 9134, pp. 180–192. Springer, Heidelberg (2015)

    Google Scholar 

  8. Beyersdorff, O., Chew, L., Mahajan, M., Shukla, A.: Are short proofs narrow? QBF resolution is not simple. In: Proceedings of the Symposium on Theoretical Aspects of Computer Science (STACS 2016) (2016)

    Google Scholar 

  9. Lonsing, F., Biere, A.: Integrating dependency schemes in search-based QBF solvers. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 158–171. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  10. Bubeck, U.: Model-based Transformations for Quantified Boolean Formulas. Ph.D. thesis (2010)

    Google Scholar 

  11. Egly, U.: On sequent systems and resolution for QBFs. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 100–113. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  12. Egly, U., Lonsing, F., Widl, M.: Long-distance resolution: proof generation and strategy extraction in search-based QBF solving. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR-19 2013. LNCS, vol. 8312, pp. 291–308. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

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

    Google Scholar 

  16. Lonsing, F., Egly, U.: Incrementally computing minimal unsatisfiable cores of QBFs via a clause group solver API. In: Heule, M., et al. (eds.) SAT 2015. LNCS, vol. 9340, pp. 191–198. Springer, Heidelberg (2015). doi:10.1007/978-3-319-24318-4_14

    Chapter  Google Scholar 

  17. Samer, M.: Variable dependencies of quantified CSPs. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 512–527. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  18. Samer, M., Szeider, S.: Backdoor sets of quantified boolean formulas. J. Autom. Reasoning 42(1), 77–97 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  19. Samulowitz, H., Bacchus, F.: Using SAT in QBF. In: International Conference on Principles and Practice of Constraint Programming (CP), pp. 578–592 (2005)

    Google Scholar 

  20. Slivovsky, F.: Structure in #SAT and QBF. Ph.D. thesis, Vienna University of Technology (2015)

    Google Scholar 

  21. Slivovsky, F., Szeider, S.: Soundness of Q-resolution with dependency schemes. TCS 612, 83–101 (2016)

    Article  MathSciNet  MATH  Google Scholar 

  22. Stockmeyer, L.J., Meyer, A.R.: Word problems requiring exponential time: preliminary report. In: Annual Symposium on Theory of Computing, pp. 1–9. ACM (1973)

    Google Scholar 

  23. Van Gelder, A.: Variable independence and resolution paths for quantified boolean formulas. In: Lee, J. (ed.) CP 2011. LNCS, vol. 6876, pp. 789–803. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  24. Van Gelder, A.: Contributions to the theory of practical quantified boolean formula solving. In: Milano, M. (ed.) CP 2012. LNCS, vol. 7514, pp. 647–663. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  25. Zhang, L., Malik, S.: Conflict driven learning in a quantified boolean satisfiability solver. In: International Conference on Computer-aided Design (ICCAD), pp. 442–449 (2002)

    Google Scholar 

Download references

Acknowledgments

This research was supported by grant no. 48138 from the John Templeton Foundation and EPSRC grant EP/L024233/1.

Author information

Authors and Affiliations

  1. School of Computing, University of Leeds, Leeds, UK

    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 .

Editor information

Editors and Affiliations

  1. University of Nice Sophia Antipolis , Sophia Antipolis, France

    Michel Rueher

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Beyersdorff, O., Blinkhorn, J. (2016). Dependency Schemes in QBF Calculi: Semantics and Soundness. In: Rueher, M. (eds) Principles and Practice of Constraint Programming. CP 2016. Lecture Notes in Computer Science(), vol 9892. Springer, Cham. https://doi.org/10.1007/978-3-319-44953-1_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-44953-1_7

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-44952-4

  • Online ISBN: 978-3-319-44953-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation