Skip to main content
SpringerLink
Log in

Contributions to the Theory of Practical Quantified Boolean Formula Solving

  • Conference paper
Principles and Practice of Constraint Programming (CP 2012)

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

Abstract

Recent solvers for quantified boolean formulas (QBFs) use a clause learning method based on a procedure proposed by Giunchiglia et al. (JAIR 2006), which avoids creating tautological clauses. The underlying proof system is Q-resolution. This paper shows an exponential worst case for the clause-learning procedure. This finding confirms empirical observations that some formulas take mysteriously long times to solve, compared to other apparently similar formulas.

Q-resolution is known to be refutation complete for QBF, but not all logically implied clauses can be derived with it. A stronger proof system called QU-resolution is introduced, and shown to be complete in this stronger sense. A new procedure called QPUP for clause learning without tautologies is also described.

A generalization of pure literals is introduced, called effectively depth-monotonic literals. In general, the variable-elimination resolution operation, as used by Quantor, sQueezeBF, and Bloqqer is unsound if the existential variable being eliminated is not at innermost scope. It is shown that variable-elimination resolution is sound for effectively depth-monotonic literals even when they are not at innermost scope.

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 84.99
Price excludes VAT (USA)
  • Available as 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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Anderson, R., Bledsoe, W.W.: A linear format for resolution with merging and a new technique for establishing completeness. JACM 17 (1970)

    Google Scholar 

  2. Balabanov, V., Jiang, J.-H.R.: Resolution Proofs and Skolem Functions in QBF Evaluation and Applications. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 149–164. Springer, Heidelberg (2011)

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

    Chapter  Google Scholar 

  4. Bubeck, U., Kleine Büning, H.: Bounded Universal Expansion for Preprocessing QBF. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 244–257. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  5. Bubeck, U.: Model-based Transformations for Quantified Boolean Formulas. PhD thesis, University of Paderborn (2010) (DISKI, 329, IOS Press; also at http://www.ub-net.de/bubeck-qbf-transformations-2010.pdf )

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

    Article  MathSciNet  MATH  Google Scholar 

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

  8. Goultiaeva, A., Bacchus, F.: Exploiting QBF duality on a circuit representation. In: AAAI (2010)

    Google Scholar 

  9. Goultiaeva, A., Iverson, V., Bacchus, F.: Beyond CNF: A Circuit-Based QBF Solver. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 412–426. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  10. Goultiaeva, A., Van Gelder, A., Bacchus, F.: A uniform approach for generating proofs and strategies for both true and false QBF formulas. In: Proc. IJCAI (2011)

    Google Scholar 

  11. Giunchiglia, E., Narizzano, M., Tacchella, A.: Learning for Quantified Boolean Logic Satisfiability. In: AAAI/IAAI, pp. 649–654 (2002)

    Google Scholar 

  12. Giunchiglia, E., Narizzano, M., Tacchella, A.: Monotone Literals and Learning in QBF Reasoning. In: Wallace, M. (ed.) CP 2004. LNCS, vol. 3258, pp. 260–273. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

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

    Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  15. Kleine Büning, H., Lettmann, T.: Propositional Logic: Deduction and Algorithms. Cambridge University Press (1999)

    Google Scholar 

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

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

    Google Scholar 

  18. Lonsing, F., Biere, A.: A Compact Representation for Syntactic Dependencies in QBFs. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 398–411. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

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

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

  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. Narizzano, M., Peschiera, C., Pulina, L., Tacchella, A.: Evaluating and certifying QBFs: A comparison of state-of-the-art tools. AI Commun. 22(4), 191–210 (2009)

    MathSciNet  MATH  Google Scholar 

  23. Van Gelder, A.: Improved Conflict-Clause Minimization Leads to Improved Propositional Proof Traces. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 141–146. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  24. Van Gelder, A.: Generalized Conflict-Clause Strengthening for Satisfiability Solvers. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol. 6695, pp. 329–342. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

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

  26. Van Gelder, A.: Producing and verifying extremely large propositional refutations: Have your cake and eat it too. AMAI (2012) (accepted subject to revisions)

    Google Scholar 

  27. Van Gelder, A., Wood, S.B., Lonsing, F.: Extended Failed-Literal Preprocessing for Quantified Boolean Formulas. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 86–99. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  28. Zhang, L., Malik, S.: Conflict driven learning in a quantified boolean satisfiability solver. In: Proc. ICCAD, pp. 442–449 (2002)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of California, Santa Cruz, USA

    Allen Van Gelder

Authors
  1. Allen Van Gelder
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. DEIS Universitá di Bologna, V.le Risorgimento, 2, 40136, Bologna, Italy

    Michela Milano

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Van Gelder, A. (2012). Contributions to the Theory of Practical Quantified Boolean Formula Solving. In: Milano, M. (eds) Principles and Practice of Constraint Programming. CP 2012. Lecture Notes in Computer Science, vol 7514. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-33558-7_47

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-33558-7_47

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-33557-0

  • Online ISBN: 978-3-642-33558-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation