Skip to main content
SpringerLink
Log in
Book cover

International Joint Conference on Automated Reasoning

IJCAR 2018: Automated Reasoning pp 161–177Cite as

\({\textsf {QRAT}}^{+}\): Generalizing QRAT by a More Powerful QBF Redundancy Property

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 10900))

Abstract

The \(\mathsf {QRAT} \) (quantified resolution asymmetric tautology) proof system simulates virtually all inference rules applied in state of the art quantified Boolean formula (QBF) reasoning tools. It consists of rules to rewrite a QBF by adding and deleting clauses and universal literals that have a certain redundancy property. To check for this redundancy property in \(\mathsf {QRAT} \), propositional unit propagation (UP) is applied to the quantifier free, i.e., propositional part of the QBF. We generalize the redundancy property in the \(\mathsf {QRAT} \) system by QBF specific UP (QUP). QUP extends UP by the universal reduction operation to eliminate universal literals from clauses. We apply QUP to an abstraction of the QBF where certain universal quantifiers are converted into existential ones. This way, we obtain a generalization of \(\mathsf {QRAT} \) we call \(\mathsf {QRAT}^{+} \). The redundancy property in \(\mathsf {QRAT}^{+} \) based on QUP is more powerful than the one in \(\mathsf {QRAT} \) based on UP. We report on proof theoretical improvements and experimental results to illustrate the benefits of \(\mathsf {QRAT}^{+} \) for QBF preprocessing.

Supported by the Austrian Science Fund (FWF) under grant S11409-N23.

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

Learn about institutional subscriptions

Notes

  1. 1.

    In general, clauses C are always (implicitly) interpreted under a quantifier prefix \(\varPi \).

  2. 2.

    Source code of : https://github.com/lonsing/qratpreplus.

  3. 3.

    We excluded the top-performing solver AIGSolve due to observed assertion failures.

References

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

  2. Beyersdorff, O., Chew, L., Janota, M.: Proof complexity of resolution-based QBF calculi. In: STACS. LIPIcs, vol. 30, pp. 76–89. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2015)

    Google Scholar 

  3. Biere, A.: Resolve and expand. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 59–70. Springer, Heidelberg (2005). https://doi.org/10.1007/11527695_5

    Chapter  MATH  Google Scholar 

  4. Faymonville, P., Finkbeiner, B., Rabe, M.N., Tentrup, L.: Encodings of bounded synthesis. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 354–370. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-54577-5_20

    Chapter  Google Scholar 

  5. Fazekas, K., Heule, M.J.H., Seidl, M., Biere, A.: Skolem function continuation for quantified Boolean formulas. In: Gabmeyer, S., Johnsen, E.B. (eds.) TAP 2017. LNCS, vol. 10375, pp. 129–138. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-61467-0_8

    Chapter  Google Scholar 

  6. Heule, M.J.H., Kiesl, B.: The potential of interference-based proof systems. In: ARCADE. EPiC Series in Computing, vol. 51, pp. 51–54. EasyChair (2017)

    Google Scholar 

  7. Heule, M.J.H., Kullmann, O.: The science of brute force. Commun. ACM 60(8), 70–79 (2017)

    Article  Google Scholar 

  8. Heule, M.J.H., 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 

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

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

    Article  MathSciNet  Google Scholar 

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

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

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

  14. Kiesl, B., Suda, M.: A unifying principle for clause elimination in first-order logic. In: de Moura, L. (ed.) CADE 2017. LNCS (LNAI), vol. 10395, pp. 274–290. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63046-5_17

    Chapter  Google Scholar 

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

  16. Lonsing, F., Biere, A.: Failed literal detection for QBF. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol. 6695, pp. 259–272. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-21581-0_21

    Chapter  Google Scholar 

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

  18. Lonsing, F., Egly, U.: \({\sf QRAT}^{+}\): Generalizing \({\sf QRAT}\) by a more powerful QBF redundancy property. CoRR abs/1804.02908 (2018). https://arxiv.org/abs/1804.02908, IJCAR 2018 proceedings version with appendix

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

  20. Rabe, M.N., Tentrup, L.: CAQE: A certifying QBF solver. In: FMCAD, pp. 136–143. IEEE (2015)

    Google Scholar 

  21. Samulowitz, H., Davies, J., Bacchus, F.: Preprocessing QBF. In: Benhamou, F. (ed.) CP 2006. LNCS, vol. 4204, pp. 514–529. Springer, Heidelberg (2006). https://doi.org/10.1007/11889205_37

    Chapter  Google Scholar 

  22. Van 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  Google Scholar 

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

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

  25. 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. Research Division of Knowledge Based Systems, Institute of Logic and Computation, TU Wien, Vienna, Austria

    Florian Lonsing & 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. Université de Lorraine, Vandoeuvre-lès-Nancy, France

    Didier Galmiche

  2. Baden-Wuerttemberg Cooperative State University, Stuttgart, Germany

    Stephan Schulz

  3. University of Trento, Trento, Italy

    Roberto Sebastiani

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG, part of Springer Nature

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Lonsing, F., Egly, U. (2018). \({\textsf {QRAT}}^{+}\): Generalizing QRAT by a More Powerful QBF Redundancy Property. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds) Automated Reasoning. IJCAR 2018. Lecture Notes in Computer Science(), vol 10900. Springer, Cham. https://doi.org/10.1007/978-3-319-94205-6_12

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-94205-6_12

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-94204-9

  • Online ISBN: 978-3-319-94205-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation