Skip to main content
SpringerLink
Log in

Q-Resolution with Generalized Axioms

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

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

Abstract

Q-resolution is a proof system for quantified Boolean formulas (QBFs) in prenex conjunctive normal form (PCNF) which underlies search-based QBF solvers with clause and cube learning (QCDCL). With the aim to derive and learn stronger clauses and cubes earlier in the search, we generalize the axioms of the Q-resolution calculus resulting in an exponentially more powerful proof system. The generalized axioms introduce an interface of Q-resolution to any other QBF proof system allowing for the direct combination of orthogonal solving techniques. We implemented a variant of the Q-resolution calculus with generalized axioms in the QBF solver DepQBF. As two case studies, we apply integrated SAT solving and resource-bounded QBF preprocessing during the search to heuristically detect potential axiom applications. Experiments with application benchmarks indicate a substantial performance improvement.

Supported by the Austrian Science Fund (FWF) under grants S11408-N23 and 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.

    Note that there are different variants of Q-resolution, e.g., long-distance resolution [34], QU-resolution [33], etc. [2, 5].

  2. 2.

    \(C'\) can also contain literals assigned by pure/unit literal detection, but as they are left to the maximal decision variable in the prefix, we treat them like decision variables.

  3. 3.

    In fact, a stronger result is proved in [30]: model-preserving manipulations of the matrix of a PCNF result in a PCNF having the same set of tree-like QBF models.

  4. 4.

    We refer to an appendix of this paper with additional results [24].

  5. 5.

    DepQBF is free software: http://lonsing.github.io/depqbf/.

  6. 6.

    http://qbf.satisfiability.org/gallery/.

  7. 7.

    The authors [26] provided us with an updated version which we used in our tests.

  8. 8.

    We refer to an appendix of this paper with additional tables [24].

References

  1. Ayari, A., Basin, D.A.: QUBOS: Deciding quantified boolean logic using propositional satisfiability solvers. In: Aagaard, M.D., O’Leary, J.W. (eds.) FMCAD 2002. LNCS, vol. 2517, pp. 187–201. Springer, Heidelberg (2002)

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

    Google Scholar 

  3. Benedetti, M., Mangassarian, H.: QBF-based formal verification: Experience and perspectives. JSAT 5(1–4), 133–191 (2008)

    MathSciNet  MATH  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, Part II. LNCS, vol. 8635, pp. 81–93. Springer, Heidelberg (2014)

    Google Scholar 

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

    Google Scholar 

  6. Biere, A.: Resolve and expand. In: H. Hoos, H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 59–70. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  7. Biere, A.: PicoSAT essentials. JSAT 4(2–4), 75–97 (2008)

    MATH  Google Scholar 

  8. Biere, A., Lonsing, F., Seidl, M.: Blocked clause elimination for QBF. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 101–115. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

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

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

    Article  MathSciNet  MATH  Google Scholar 

  11. Giunchiglia, E., Marin, P., Narizzano, M.: Reasoning with quantified boolean formulas. In: Biere, A., Heule, M., Van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. FAIA, vol. 185, pp. 761–780. IOS Press, Amsterdam (2009)

    Google Scholar 

  12. Giunchiglia, E., Narizzano, M., Tacchella, A.: Clause/term resolution and learning in the evaluation of quantified boolean formulas. JAIR 26, 371–416 (2006)

    MathSciNet  MATH  Google Scholar 

  13. Heule, M., Järvisalo, M., Lonsing, F., Seidl, M., Biere, A.: Clause elimination for SAT and QSAT. JAIR 53, 127–168 (2015)

    MathSciNet  MATH  Google Scholar 

  14. 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, vol. 8562, pp. 91–106. Springer, Heidelberg (2014)

    Google Scholar 

  15. Janota, M., Jordan, C., Klieber, W., Lonsing, F., Seidl, M., Van Gelder, A.: The QBF Gallery 2014: The QBF competition at the FLoC olympic games. JSAT 9, 187–206 (2015)

    Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  17. Janota, M., Marques-Silva, J.: Solving QBF by clause selection. In: IJCAI, pp. 325–331. AAAI Press (2015)

    Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

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

  20. Klieber, W., Sapra, S., Gao, S., Clarke, E.: A non-prenex, non-clausal QBF solver with game-state learning. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 128–142. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  21. Letz, R.: Lemma and model caching in decision procedures for quantified boolean formulas. In: Egly, U., Fermüller, C. (eds.) TABLEAUX 2002. LNCS (LNAI), vol. 2381, pp. 160–175. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  22. Lonsing, F., Bacchus, F., Biere, A., Egly, U., Seidl, M.: Enhancing search-based QBF solving by dynamic blocked clause elimination. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) LPAR-20 2015. LNCS, vol. 9450, pp. 418–433. Springer, Heidelberg (2015)

    Chapter  Google Scholar 

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

    Chapter  Google Scholar 

  24. Lonsing, F., Egly, U., Seidl, M.: Q-resolution with generalized axioms. CoRR abs/1604.05994, SAT 2016 proceedings version with appendix (2016). http://arxiv.org/abs/1604.05994

  25. Lonsing, F., Seidl, M., Van Gelder, A.: The QBF Gallery: Behind the scenes. Artif. Intell. 237, 92–114 (2016)

    Article  MathSciNet  MATH  Google Scholar 

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

    Google Scholar 

  27. Reimer, S., Pigorsch, F., Scholl, C., Becker, B.: Enhanced Integration of QBF Solving Techniques. In: Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), pp. 133–143. Verlag Dr. Kovac (2012)

    Google Scholar 

  28. Samer, M., Szeider, S.: Backdoor sets of quantified boolean formulas. JAR 42(1), 77–97 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  29. Samulowitz, H., Bacchus, F.: Using SAT in QBF. In: van Beek, P. (ed.) CP 2005. LNCS, vol. 3709, pp. 578–592. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  30. Samulowitz, H., Davies, J., Bacchus, F.: Preprocessing QBF. In: Benhamou, F. (ed.) CP 2006. LNCS, vol. 4204, pp. 514–529. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  31. Silva, J.P.M., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers. In: Biere, A., Heule, M., Van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. FAIA, vol. 185, pp. 131–153. IOS Press, Amsterdam (2009)

    Google Scholar 

  32. Tu, K.-H., Hsu, T.-C., Jiang, J.-H.R.: QELL: QBF reasoning with extended clause learning and levelized SAT solving. In: Heule, M., Weaver, S. (eds.) SAT 2015. LNCS, vol. 9340, pp. 343–359. Springer, Heidelberg (2015)

    Chapter  Google Scholar 

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

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

  35. Zhang, L., Malik, S.: Towards a symmetric treatment of satisfaction and conflicts in quantified boolean formula evaluation. In: Van Hentenryck, P. (ed.) CP 2002. LNCS, vol. 2470, pp. 200–215. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Knowledge-Based Systems Group, Vienna University of Technology, Vienna, Austria

    Florian Lonsing & Uwe Egly

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

    Martina Seidl

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

  3. Martina Seidl
    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. Aix-Marseille Université, Marseille, France

    Nadia Creignou

  2. Université d'Artois, Lens, France

    Daniel Le Berre

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Lonsing, F., Egly, U., Seidl, M. (2016). Q-Resolution with Generalized Axioms. In: Creignou, N., Le Berre, D. (eds) Theory and Applications of Satisfiability Testing – SAT 2016. SAT 2016. Lecture Notes in Computer Science(), vol 9710. Springer, Cham. https://doi.org/10.1007/978-3-319-40970-2_27

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-40970-2_27

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-40969-6

  • Online ISBN: 978-3-319-40970-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation