[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to main content
Springer Nature Link
Log in

QRAT Polynomially Simulates \(\forall \text {-Exp+Res}\)

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

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

  • 1308 Accesses

  • 3 Citations

Abstract

The proof system \(\forall \text {-Exp+Res}\) formally captures expansion-based solving of quantified Boolean formulas (QBFs) whereas the \(\mathsf {QRAT}\) proof system captures QBF preprocessing. From previous work it is known that certain families of formulas have short proofs in \(\mathsf {QRAT}\) but not in \(\forall \text {-Exp+Res}\). However, it was not known if the two proof systems were incomparable (i.e., if there also existed QBFs with short \(\forall \text {-Exp+Res}\) proofs but without short \(\mathsf {QRAT}\) proofs), or if \(\mathsf {QRAT}\) polynomially simulates \(\forall \text {-Exp+Res}\). We close this gap of the QBF-proof-complexity landscape by presenting a polynomial simulation of \(\forall \text {-Exp+Res}\) in \(\mathsf {QRAT}\). Our simulation shows how definition introduction combined with extended-universal reduction can mimic the concept of universal expansion.

This work has been supported by the Austrian Science Fund (FWF) projects W1255-N23 and S11408-N23 and the LIT AI Lab funded by the State of Upper Austria.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
£29.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

eBook
GBP 13.99
Price includes VAT (United Kingdom)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
GBP 44.99
Price includes VAT (United Kingdom)
  • 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

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

    Google Scholar 

  4. Beyersdorff, O., Chew, L., Janota, M.: On unification of QBF resolution-based calculi. In: Csuhaj-Varjú, E., Dietzfelbinger, M., Ésik, Z. (eds.) MFCS 2014. LNCS, vol. 8635, pp. 81–93. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-662-44465-8_8

    Chapter  MATH  Google Scholar 

  5. Beyersdorff, O., Chew, L., Janota, M.: Proof complexity of resolution-based QBF calculi. In: Proceedings of the 32nd International Symposium on Theoretical Aspects of Computer Science (STACS 2015). LIPIcs, vol. 30, pp. 76–89. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2015)

    Google Scholar 

  6. Beyersdorff, O., Chew, L., Mahajan, M., Shukla, A.: Are short proofs narrow? QBF resolution is not simple. In: Proceedings of the 33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016). LIPIcs, vol. 47, pp. 15:1–15:14. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2016)

    Google Scholar 

  7. Bloem, R., Braud-Santoni, N., Hadzic, V., Egly, U., Lonsing, F., Seidl, M.: Expansion-based QBF solving without recursion. In: Proceedings of the International Conference on Formal Methods in Computer Aided Design (FMCAD 2018), pp. 1–10. IEEE (2018)

    Google Scholar 

  8. Chen, H.: Proof complexity modulo the polynomial hierarchy: understanding alternation as a source of hardness. In: Proceedings of the 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). LIPIcs, vol. 55, pp. 94:1–94:14. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2016)

    Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  10. Egly, U.: On stronger calculi for QBFs. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 419–434. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-40970-2_26

    Chapter  Google Scholar 

  11. 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). https://doi.org/10.1007/978-3-642-23786-7_59

    Chapter  Google Scholar 

  12. Heule, M.J.H., Seidl, M., Biere, A.: Solution validation and extraction for QBF preprocessing. J. Autom. Reasoning 58(1), 1–29 (2016)

    MathSciNet  MATH  Google Scholar 

  13. Janota, M.: On Q-resolution and CDCL QBF solving. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 402–418. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-40970-2_25

    Chapter  MATH  Google Scholar 

  14. Janota, M., Grigore, R., Marques-Silva, J.: On QBF proofs and preprocessing. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR 2013. LNCS, vol. 8312, pp. 473–489. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-45221-5_32

    Chapter  MATH  Google Scholar 

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

  16. Janota, M., Marques-Silva, J.: On propositional QBF expansions and Q-resolution. In: Järvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 67–82. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39071-5_7

    Chapter  MATH  Google Scholar 

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

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

  19. Kiesl, B., Rebola-Pardo, A., Heule, M.J.H.: Extended resolution simulates DRAT. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) IJCAR 2018. LNCS (LNAI), vol. 10900, pp. 516–531. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-94205-6_34

    Chapter  Google Scholar 

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

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

  22. Peitl, T., Slivovsky, F., Szeider, S.: Dependency learning for QBF. In: Gaspers, S., Walsh, T. (eds.) SAT 2017. LNCS, vol. 10491, pp. 298–313. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66263-3_19

    Chapter  Google Scholar 

  23. Slivovsky, F., Szeider, S.: Variable dependencies and Q-resolution. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 269–284. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-09284-3_21

    Chapter  MATH  Google Scholar 

  24. Slivovsky, F., Szeider, S.: Soundness of Q-resolution with dependency schemes. Theor. Comput. Sci. 612, 83–101 (2016)

    Article  MathSciNet  Google Scholar 

  25. Tentrup, L.: On expansion and resolution in CEGAR based QBF solving. In: Majumdar, R., Kunčak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 475–494. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63390-9_25

    Chapter  Google Scholar 

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

  27. Wetzler, N., Heule, M.J.H., Hunt, W.A.: DRAT-trim: efficient checking and trimming using expressive clausal proofs. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 422–429. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-09284-3_31

    Chapter  MATH  Google Scholar 

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

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute of Logic and Computation, TU Wien, Vienna, Austria

    Benjamin Kiesl

  2. CISPA Helmholtz Center for Information Security, Saarbrücken, Germany

    Benjamin Kiesl

  3. Institute for Formal Models and Verification, JKU Linz, Linz, Austria

    Martina Seidl

Authors
  1. Benjamin Kiesl
    View author publications

    Search author on:PubMed Google Scholar

  2. Martina Seidl
    View author publications

    Search author on:PubMed Google Scholar

Corresponding author

Correspondence to Benjamin Kiesl .

Editor information

Editors and Affiliations

  1. University of Lisbon, Lisbon, Portugal

    Mikoláš Janota

  2. University of Lisbon, Lisbon, Portugal

    Inês Lynce

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Kiesl, B., Seidl, M. (2019). QRAT Polynomially Simulates \(\forall \text {-Exp+Res}\). In: Janota, M., Lynce, I. (eds) Theory and Applications of Satisfiability Testing – SAT 2019. SAT 2019. Lecture Notes in Computer Science(), vol 11628. Springer, Cham. https://doi.org/10.1007/978-3-030-24258-9_13

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-24258-9_13

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-24257-2

  • Online ISBN: 978-3-030-24258-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics