Skip to main content
SpringerLink
Log in

Computing Resolution-Path Dependencies in Linear Time ,

  • Conference paper
Theory and Applications of Satisfiability Testing – SAT 2012 (SAT 2012)

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

Abstract

The alternation of existential and universal quantifiers in a quantified boolean formula (QBF) generates dependencies among variables that must be respected when evaluating the formula. Dependency schemes provide a general framework for representing such dependencies. Since it is generally intractable to determine dependencies exactly, a set of potential dependencies is computed instead, which may include false positives. Among the schemes proposed so far, resolution path dependencies introduce the fewest spurious dependencies. In this work, we describe an algorithm that detects resolution-path dependencies in linear time, resolving a problem posed by Van Gelder (CP 2011).

Research supported by the European Research Council (ERC), project COMPLEX REASON 239962, and WWTF grant WWTF016.

Dedicated to the memory of Marko Samer.

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Ayari, A., Basin, D.: 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. Biere, A.: Resolve and Expand. In: Hoos, H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 59–70. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

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

  4. Egly, U., Tompits, H., Woltran, S.: On quantifier shifting for quantified Boolean formulas. In: Proc. SAT 2002 Workshop on Theory and Applications of Quantified Boolean Formulas. Informal Proceedings, pp. 48–61 (2002)

    Google Scholar 

  5. 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, vol. 185, pp. 761–780. IOS Press (2009)

    Google Scholar 

  6. Kleine Büning, H., Bubeck, U.: Theory of quantified boolean formulas. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, ch. 23, pp. 735–760. IOS Press (2009)

    Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  8. Kleine Büning, H., Lettman, T.: Propositional logic: deduction and algorithms. Cambridge University Press, Cambridge (1999)

    MATH  Google Scholar 

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

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

  11. Samer, M.: Variable Dependencies of Quantified CSPs. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 512–527. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  12. Samer, M., Szeider, S.: Backdoor sets of quantified Boolean formulas. Journal of Automated Reasoning 42(1), 77–97 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  13. Stockmeyer, L.J.: The polynomial-time hierarchy. Theoretical Computer Science 3(1), 1–22 (1976)

    Article  MathSciNet  Google Scholar 

  14. Stockmeyer, L.J., Meyer, A.R.: Word problems requiring exponential time. In: Proc. Theory of Computing, pp. 1–9. ACM (1973)

    Google Scholar 

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

Download references

Author information

Authors and Affiliations

  1. Institute of Information Systems, Vienna University of Technology, A-1040, Vienna, Austria

    Friedrich Slivovsky & Stefan Szeider

Authors
  1. Friedrich Slivovsky
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Stefan Szeider
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Center for Information Technology, Fondazione Bruno Kessler, via Sommarive 18, Povo, 38123, Trento, Italy

    Alessandro Cimatti

  2. Department of Information Engineering and Computer Science, University of Trento, via Sommarive 14, Povo, 38123, Trento, Italy

    Roberto Sebastiani

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Slivovsky, F., Szeider, S. (2012). Computing Resolution-Path Dependencies in Linear Time ,. In: Cimatti, A., Sebastiani, R. (eds) Theory and Applications of Satisfiability Testing – SAT 2012. SAT 2012. Lecture Notes in Computer Science, vol 7317. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-31612-8_6

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-31612-8_6

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-31611-1

  • Online ISBN: 978-3-642-31612-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation