Skip to main content
SpringerLink
Log in

Solving #SAT Using Vertex Covers

  • Conference paper
Theory and Applications of Satisfiability Testing - SAT 2006 (SAT 2006)

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

Abstract

We propose an exact algorithm for counting the models of propositional formulas in conjunctive normal form (CNF). Our algorithm is based on the detection of strong backdoor sets of bounded size; each instantiation of the variables of a strong backdoor set puts the given formula into a class of formulas for which models can be counted in polynomial time. For the backdoor set detection we utilize an efficient vertex cover algorithm applied to a certain “obstruction graph” that we associate with the given formula. This approach gives rise to a new hardness index for formulas, the clustering-width. Our algorithm runs in uniform polynomial time on formulas with bounded clustering-width.

It is known that the number of models of formulas with bounded clique-width, bounded treewidth, or bounded branchwidth can be computed in polynomial time; these graph parameters are applied to formulas via certain (hyper)graphs associated with formulas. We show that clustering-width and the other parameters mentioned are incomparable: there are formulas with bounded clustering-width and arbitrarily large clique-width, treewidth, and branchwidth. Conversely, there are formulas with arbitrarily large clustering-width and bounded clique-width, treewidth, and branchwidth.

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. Bacchus, F., Dalmao, S., Pitassi, T.: Algorithms and complexity results for #SAT and Bayesian Inference. In: 44th Annual IEEE Symposium on Foundations of Computer Science (FOCS 2003), pp. 340–351 (2003)

    Google Scholar 

  2. Bodlaender, H.L.: A partial k-arboretum of graphs with bounded treewidth. Theoret. Comput. Sci. 209(1-2), 1–45 (1998)

    Article  MATH  MathSciNet  Google Scholar 

  3. Chen, J., Kanj, I.A., Xia, G.: Simplicity is beauty: Improved upper bounds for vertex cover. Technical Report TR05-008, DePaul University, Chicago IL (2005)

    Google Scholar 

  4. Courcelle, B., Makowsky, J.A., Rotics, U.: Linear time solvable optimization problems on graphs of bounded clique-width. Theory Comput. Syst. 33(2), 125–150 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  5. Courcelle, B., Makowsky, J.A., Rotics, U.: On the fixed parameter complexity of graph enumeration problems definable in monadic second-order logic. Discr. Appl. Math. 108(1-2), 23–52 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  6. Courcelle, B., Olariu, S.: Upper bounds to the clique width of graphs. Discr. Appl. Math. 101(1-3), 77–114 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  7. Downey, R.G., Fellows, M.R.: Parameterized Complexity. In: Monographs in Computer Science, Springer, Heidelberg (1999)

    Google Scholar 

  8. Fischer, E., Makowsky, J.A., Ravve, E.R.: Counting truth assignments of formulas of bounded tree-width or clique-width. Discr. Appl. Math. (to appear)

    Google Scholar 

  9. Flum, J., Grohe, M.: The parameterized complexity of counting problems. SIAM J. Comput. 33(4), 892–922 (2004)

    Article  MATH  MathSciNet  Google Scholar 

  10. Golumbic, M.C., Rotics, U.: On the clique-width of some perfect graph classes. WG 1999 11(3), 423–443 (2000), Selected papers from the Workshop on Graph-Theoretical Aspects of Computer Science (WG 1999), Part 1 (Ascona)

    Google Scholar 

  11. Gramm, J., Guo, J., Hüffner, F., Niedermeier, R.: Graph-modeled data clustering: fixed-parameter algorithms for clique generation. Theory Comput. Syst. 38(4), 373–392 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  12. Gottlob, G., Scarcello, F., Sideri, M.: Fixed-parameter complexity in AI and nonmonotonic reasoning. Artificial Intelligence 138(1-2), 55–86 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  13. Gottlob, G., Szeider, S.: Fixed-parameter algorithms for artificial intelligence, constraint satisfaction, and database problems (April 2006) (submitted)

    Google Scholar 

  14. Interian, Y.: Backdoor sets for random 3-SAT. In: Informal Proceedings of SAT 2003, pp. 231–238 (2003)

    Google Scholar 

  15. Iwama, K.: CNF-satisfiability test by counting and polynomial average time. SIAM J. Comput. 18(2), 385–391 (1989)

    Article  MATH  MathSciNet  Google Scholar 

  16. Kilby, P., Slaney, J.K., Thiébaux, S., Walsh, T.: Backbones and backdoors in satisfiability. In: Proceedings, The Twentieth National Conference on Artificial Intelligence and the Seventeenth Innovative Applications of Artificial Intelligence Conference (AAAI 2005), pp. 1368–1373 (2005)

    Google Scholar 

  17. Kleine Büning, H., Zhao, X.: Satisfiable formulas closed under replacement. In: Proceedings for the Workshop on Theory and Applications of Satisfiability. Electronic Notes in Discrete Mathematics, vol. 9, Elsevier Science Publishers, North-Holland (2001)

    Google Scholar 

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

    Chapter  Google Scholar 

  19. Niedermeier, R.: Invitation to Fixed-Parameter Algorithms. In: Oxford Lecture Series in Mathematics and Its Applications, Oxford University Press, Oxford (2006)

    Google Scholar 

  20. Nishimura, N., Ragde, P., Szeider, S.: Detecting backdoor sets with respect to Horn and binary clauses. In: Informal Proceedings of SAT 2004, pp. 96–103 (2004)

    Google Scholar 

  21. Oum, S., Seymour, P.: Approximating clique-width and branch-width. J. Combin. Theory, Ser. B (to appear)

    Google Scholar 

  22. Robertson, N., Seymour, P.D.: Graph minors. X. Obstructions to tree-decomposition. J. Combin. Theory Ser. B 52(2), 153–190 (1991)

    Article  MATH  MathSciNet  Google Scholar 

  23. Roth, D.: On the hardness of approximate reasoning. Artificial Intelligence 82(1-2), 273–302 (1996)

    Article  MathSciNet  Google Scholar 

  24. Ruan, Y., Kautz, H.A., Horvitz, E.: The backdoor key: A path to understanding problem hardness. In: Proceedings of the 19th National Conference on Artificial Intelligence, 16th Conference on Innovative Applications of Artificial Intelligence, pp. 124–130. AAAI Press / The MIT Press (2004)

    Google Scholar 

  25. Szeider, S.: On fixed-parameter tractable parameterizations of SAT. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 188–202. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  26. Szeider, S.: Backdoor sets for DLL subsolvers. Journal of Automated Reasoning (in press, 2005)

    Google Scholar 

  27. Valiant, L.G.: The complexity of computing the permanent. Theoret. Comput. Sci. 8(2), 189–201 (1979)

    Article  MATH  MathSciNet  Google Scholar 

  28. Williams, R., Gomes, C., Selman, B.: On the connections between backdoors, restarts, and heavy-tailedness in combinatorial search. In: Informal Proceedings of SAT 2003, pp. 222–230 (2003)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Computer Science, University of Waterloo, Waterloo, Ontario, N2L 3G1, Canada

    Naomi Nishimura & Prabhakar Ragde

  2. Department of Computer Science, Durham University, Durham, DH1 3LE, United Kingdom

    Stefan Szeider

Authors
  1. Naomi Nishimura
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Prabhakar Ragde
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Stefan Szeider
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Institute for Formal Models and Verification, Johannes Kepler University, Linz, Austria

    Armin Biere

  2. Department of Computer Science, Cornell University, 14853, Ithaca, NY, U.S.A.

    Carla P. Gomes

Rights and permissions

Reprints and permissions

Copyright information

© 2006 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Nishimura, N., Ragde, P., Szeider, S. (2006). Solving #SAT Using Vertex Covers. In: Biere, A., Gomes, C.P. (eds) Theory and Applications of Satisfiability Testing - SAT 2006. SAT 2006. Lecture Notes in Computer Science, vol 4121. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11814948_36

Download citation

  • DOI: https://doi.org/10.1007/11814948_36

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-37206-6

  • Online ISBN: 978-3-540-37207-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation