Skip to main content
SpringerLink
Log in
Book cover

International Conference on Theory and Applications of Satisfiability Testing

SAT 2007: Theory and Applications of Satisfiability Testing – SAT 2007 pp 230–243Cite as

Backdoor Sets of Quantified Boolean Formulas

  • Conference paper

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

Abstract

We generalize the notion of backdoor sets from propositional formulas to quantified Boolean formulas in conjunctive normal form (QCNF). We develop parameterized algorithms that admit uniform polynomial time QCNF evaluation parameterized by the size of smallest strong backdoor sets. For our algorithms we develop a theory of variable dependency which is of independent interest. As a result, we obtain hierarchies of classes of tractable QCNF formulas with the classes of quantified Horn and quantified 2CNF formulas, respectively, at their first level, thus gradually generalizing these two prominent tractable classes. In contrast to known tractable classes based on bounded treewidth, the number of quantifier alternations of our classes is unbounded.

Research supported by the EPSRC project EP/E001394/1.

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Aspvall, B., Plass, M.F., Tarjan, R.E.: A linear-time algorithm for testing the truth of certain quantified Boolean formulas. Information Processing Letters 8(3), 121–123 (1979)

    Article  MathSciNet  MATH  Google Scholar 

  2. Benedetti, M.: Quantifier trees for QBFs. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 378–385. Springer, Heidelberg (2005)

    Google Scholar 

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

    Google Scholar 

  4. Downey, R.G., Fellows, M.R.: Parameterized Complexity. Springer, Heidelberg (1999)

    Google Scholar 

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

    Google Scholar 

  6. Flum, J., Grohe, M.: Parameterized Complexity Theory. Springer, Heidelberg (2006)

    Google Scholar 

  7. Hoffmann, J., Gomes, C., Selman, B.: Structure and problem hardness: Goal asymmetry and DPLL proofs in SAT-based planning. In: Proc. 16th Int. Conf. on Automated Planning and Scheduling (ICAPS’06), pp. 284–293. AAAI Press, Menlo Park (2006)

    Google Scholar 

  8. Interian, Y.: Backdoor sets for random 3-SAT. In: Proc. 6th Int. Conf. on Theory and Applications of Satisfiability Testing (SAT’03), Informal Proceedings, pp. 231–238 (2003)

    Google Scholar 

  9. Kilby, P., et al.: Backbones and backdoors in satisfiability. In: Proc. 20th National Conf. on Artificial Intelligence (AAAI’05), pp. 1368–1373. AAAI Press, Menlo Park (2005)

    Google Scholar 

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

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

    MATH  Google Scholar 

  12. Knuth, D.E.: Sorting by Exchanging. In: Knuth, D.E. (ed.) Sorting and Searching. The Art of Computer Programming, vol. 3, pp. 106–110. Addison-Wesley, Reading (1973)

    Google Scholar 

  13. Lynce, I., Marques-Silva, J.P.: Hidden structure in unsatisfiable random 3-SAT: An empirical study. In: Proc. 16th IEEE Int. Conf. on Tools with Artificial Intelligence (ICTAI’04), pp. 246–251. IEEE Computer Society Press, Los Alamitos (2004)

    Chapter  Google Scholar 

  14. Niedermeier, R.: Invitation to Fixed-Parameter Algorithms. Oxford University Press, Oxford (2006)

    MATH  Google Scholar 

  15. Nishimura, N., Ragde, P., Szeider, S.: Detecting backdoor sets with respect to Horn and binary clauses. In: Proc. 7th Int. Conf. on Theory and Applications of Satisfiability Testing (SAT’04), Informal Proceedings, pp. 96–103 (2004)

    Google Scholar 

  16. Nishimura, N., Ragde, P., Szeider, S.: Solving #SAT using vertex covers. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 396–409. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  17. Otwell, C., Remshagen, A., Truemper, K.: An effective QBF solver for planning problems. In: Proc. Int. Conf. on Modeling, Simulation and Visualization Methods and Int. Conf. on Algorithmic Mathematics and Computer Science (MSV/AMCS’04), pp. 311–316. CSREA Press (2004)

    Google Scholar 

  18. Pan, G., Vardi, M.Y.: Fixed-parameter hierarchies inside PSpace. In: Proc. 21st Annual IEEE Symposium on Logic in Computer Science (LICS’06), pp. 27–36. IEEE Computer Society Press, Los Alamitos (2006)

    Google Scholar 

  19. Papadimitriou, C.H.: Computational Complexity. Addison-Wesley, Reading (1994)

    MATH  Google Scholar 

  20. Rintanen, J.: Constructing conditional plans by a theorem-prover. Journal of Artificial Intelligence Research 10, 323–352 (1999)

    MATH  Google Scholar 

  21. Ruan, Y., Kautz, H.A., Horvitz, E.: The backdoor key: A path to understanding problem hardness. In: Proc. 19th National Conf. on Artificial Intelligence (AAAI’04), pp. 124–130. AAAI Press, Menlo Park (2004)

    Google Scholar 

  22. Sabharwal, A., et al.: QBF modeling: Exploiting player symmetry for simplicity and efficiency. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 382–395. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  23. Samulowitz, H., Bacchus, F.: Binary clause reasoning in QBF. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 353–367. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  24. Stockmeyer, L.J., Meyer, A.R.: Word problems requiring exponential time. In: Proc. 5th Annual ACM Symposium on Theory of Computing (STOC’73), pp. 1–9. ACM Press, New York (1973)

    Chapter  Google Scholar 

  25. Szeider, S.: Backdoor sets for DLL subsolvers. Journal of Automated Reasoning 35(1-3), 73–88 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  26. Szeider, S.: Generalizations of matched CNF formulas. Ann. Math. Artif. Intell. 43(1-4), 223–238 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  27. Williams, R., Gomes, C., Selman, B.: Backdoors to typical case complexity. In: Proc. 18th Int. Joint Conf. on Artificial Intelligence (IJCAI’03), pp. 1173–1178. Morgan Kaufmann, San Francisco (2003)

    Google Scholar 

  28. Williams, R., Gomes, C., Selman, B.: On the connections between backdoors, restarts, and heavy-tailedness in combinatorial search. In: Proc. 6th Int. Conf. on Theory and Applications of Satisfiability Testing (SAT’03), Informal Proceedings, pp. 222–230 (2003)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Durham University, UK

    Marko Samer & Stefan Szeider

Authors
  1. Marko Samer
    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

João Marques-Silva Karem A. Sakallah

Rights and permissions

Reprints and permissions

Copyright information

© 2007 Springer Berlin Heidelberg

About this paper

Cite this paper

Samer, M., Szeider, S. (2007). Backdoor Sets of Quantified Boolean Formulas. In: Marques-Silva, J., Sakallah, K.A. (eds) Theory and Applications of Satisfiability Testing – SAT 2007. SAT 2007. Lecture Notes in Computer Science, vol 4501. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-72788-0_23

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-72788-0_23

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-72787-3

  • Online ISBN: 978-3-540-72788-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation