Skip to main content
SpringerLink
Log in
SpringerLink
Log in

QRATPre+: Effective QBF Preprocessing via Strong Redundancy Properties

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

Abstract

We present version 2.0 of QRATPre+, a preprocessor for quantified Boolean formulas (QBFs) based on the \(\mathsf {QRAT} \) proof system and its generalization \(\mathsf {QRAT}^{+} \). These systems rely on strong redundancy properties of clauses and universal literals. QRATPre+ is the first implementation of these redundancy properties in \(\mathsf {QRAT} \) and \(\mathsf {QRAT}^{+} \) used to simplify QBFs in preprocessing. It is written in C and features an API for easy integration in other QBF tools. We present implementation details and report on experimental results demonstrating that QRATPre+ improves upon the power of state-of-the-art preprocessors and solvers.

Part of this work was carried out while the first author was employed at the Institute of Logic and Computation, TU Wien, Austria. This work is supported by the Austrian Science Fund (FWF) under grant S11409-N23.

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 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.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/index_eval.php.

  2. 2.

    QRATPre+ is licensed under GPLv3: https://lonsing.github.io/qratpreplus/.

  3. 3.

    We refer to an online appendix [19] for results with combinations BQ and QH.

References

  1. Biere, A., Lonsing, F., Seidl, M.: Blocked clause elimination for QBF. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol. 6803, pp. 101–115. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22438-6_10

    Chapter  Google Scholar 

  2. Bloem, R., Braud-Santoni, N., Hadzic, V., Egly, U., Lonsing, F., Seidl, M.: Expansion-based QBF solving without recursion. In: FMCAD, pp. 1–10. IEEE (2018)

    Google Scholar 

  3. Cadoli, M., Giovanardi, A., Schaerf, M.: An algorithm to evaluate quantified boolean formulae. In: AAAI, pp. 262–267. AAAI Press/The MIT Press (1998)

    Google Scholar 

  4. Gent, I., Giunchiglia, E., Narizzano, M., Rowley, A., Tacchella, A.: Watched data structures for QBF solvers. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 25–36. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24605-3_3

    Chapter  Google Scholar 

  5. Giunchiglia, E., Narizzano, M., Tacchella, A.: Clause/term resolution and learning in the evaluation of quantified boolean formulas. JAIR 26, 371–416 (2006). https://doi.org/10.1613/jair.1959

    Article  MathSciNet  MATH  Google Scholar 

  6. Heule, M., Järvisalo, M., Lonsing, F., Seidl, M., Biere, A.: Clause elimination for SAT and QSAT. JAIR 53, 127–168 (2015). https://doi.org/10.1613/jair.4694

    Article  MathSciNet  MATH  Google Scholar 

  7. Heule, M., Seidl, M., Biere, A.: A unified proof system for QBF preprocessing. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS (LNAI), vol. 8562, pp. 91–106. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08587-6_7

    Chapter  Google Scholar 

  8. Heule, M.J.H., Seidl, M., Biere, A.: Blocked literals are universal. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 436–442. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-17524-9_33

    Chapter  Google Scholar 

  9. Heule, M., Seidl, M., Biere, A.: Solution validation and extraction for QBF preprocessing. J. Autom. Reasoning 58(1), 97–125 (2017)

    Article  MathSciNet  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  11. Järvisalo, M., Heule, M.J.H., Biere, A.: Inprocessing rules. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 355–370. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31365-3_28

    Chapter  Google Scholar 

  12. Kiesl, B., Seidl, M., Tompits, H., Biere, A.: Super-blocked clauses. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 45–61. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-40229-1_5

    Chapter  Google Scholar 

  13. Kiesl, B., Seidl, M., Tompits, H., Biere, A.: Blockedness in propositional logic: are you satisfied with your neighborhood? In: IJCAI, pp. 4884–4888 (2017). www.ijcai.org

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

    Article  MathSciNet  MATH  Google Scholar 

  15. Letz, R.: Lemma and model caching in decision procedures for quantified boolean formulas. In: Egly, U., Fermüller, C.G. (eds.) TABLEAUX 2002. LNCS (LNAI), vol. 2381, pp. 160–175. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45616-3_12

    Chapter  MATH  Google Scholar 

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

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

  18. Lonsing, F., Egly, U.: \({\sf QRAT}^+\): generalizing QRAT by a more powerful QBF redundancy property. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) IJCAR 2018. LNCS (LNAI), vol. 10900, pp. 161–177. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-94205-6_12

    Chapter  Google Scholar 

  19. Lonsing, F., Egly, U.: QRATPre+: effective QBF preprocessing via strong redundancy properties. CoRR abs/1904.12927 (2019). https://arxiv.org/abs/1904.12927. SAT 2019 proceedings version with appendix

  20. Lonsing, F., Seidl, M., Van Gelder, A.: The QBF gallery: behind the scenes. Artif. Intell. 237, 92–114 (2016)

    Article  MathSciNet  Google Scholar 

  21. Marin, P., Narizzano, M., Pulina, L., Tacchella, A., Giunchiglia, E.: Twelve years of QBF evaluations: QSAT Is PSPACE-hard and it shows. Fundam. Inform. 149(1–2), 133–158 (2016)

    Article  MathSciNet  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. Rabe, M.N., Tentrup, L.: CAQE: a certifying QBF solver. In: FMCAD, pp. 136–143. IEEE (2015)

    Google Scholar 

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

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

  26. Wimmer, R., Reimer, S., Marin, P., Becker, B.: HQSpre – an effective preprocessor for QBF and DQBF. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 373–390. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-54577-5_21

    Chapter  Google Scholar 

  27. Zhang, L., Malik, S.: Conflict driven learning in a quantified boolean satisfiability solver. In: ICCAD, pp. 442–449. ACM/IEEE Computer Society (2002)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computer Science Department, Stanford University, Stanford, CA, 94305, USA

    Florian Lonsing

  2. Institute of Logic and Computation, TU Wien, 1040, Vienna, Austria

    Uwe Egly

Authors
  1. Florian Lonsing
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Uwe Egly
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Florian Lonsing .

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

Lonsing, F., Egly, U. (2019). QRATPre+: Effective QBF Preprocessing via Strong Redundancy Properties. 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_14

Download citation

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

  • 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

Search

Navigation