Skip to main content
SpringerLink
Log in

Exploiting Treewidth for Projected Model Counting and Its Limits

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

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

Abstract

In this paper, we introduce a novel algorithm to solve projected model counting (PMC). PMC asks to count solutions of a Boolean formula with respect to a given set of projected variables, where multiple solutions that are identical when restricted to the projected variables count as only one solution. Our algorithm exploits small treewidth of the primal graph of the input instance. It runs in time \({\mathcal O}(2^{2^{k+4}} n^2)\) where k is the treewidth and n is the input size of the instance. In other words, we obtain that the problem PMC is fixed-parameter tractable when parameterized by treewidth. Further, we take the exponential time hypothesis (ETH) into consideration and establish lower bounds of bounded treewidth algorithms for PMC, yielding asymptotically tight runtime bounds of our algorithm.

The work has been supported by the Austrian Science Fund (FWF), Grants Y698 and P26696, and the German Science Fund (DFG), Grant HO 1294/11-1. The first two authors are also affiliated with the University of Potsdam, Germany.

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.

    Actually, \(\mathbb {SAT}\) takes in addition as input PP-Tabs, which contains a mapping of nodes of the tree decomposition to tables, i.e., tables of the previous pass. Later, we use this for a second traversal to pass results () from the first traversal to the table algorithm \(\mathbb {PROJ} \) for projected model counting in the second traversal.

References

  1. Abiteboul, S., Hull, R., Vianu, V.: Foundations of Databases: The Logical Level, 1st edn. Addison-Wesley, Boston (1995)

    Google Scholar 

  2. Abramson, B., Brown, J., Edwards, W., Murphy, A., Winkler, R.L.: Hailfinder: a Bayesian system for forecasting severe weather. Int. J. Forecast. 12(1), 57–71 (1996)

    Article  Google Scholar 

  3. Aziz, R.A., Chu, G., Muise, C., Stuckey, P.: \(\#\exists \)SAT: projected model counting. In: Heule, M., Weaver, S. (eds.) SAT 2015. LNCS, vol. 9340, pp. 121–137. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-24318-4_10

    Chapter  Google Scholar 

  4. Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press, Amsterdam (2009)

    Google Scholar 

  5. Bodlaender, H.L.: A linear-time algorithm for finding tree-decompositions of small treewidth. SIAM J. Comput. 25(6), 1305–1317 (1996)

    Article  MathSciNet  Google Scholar 

  6. Bodlaender, H.L., Kloks, T.: Efficient and constructive algorithms for the pathwidth and treewidth of graphs. J. Algorithms 21(2), 358–402 (1996)

    Article  MathSciNet  Google Scholar 

  7. Bodlaender, H.L., Koster, A.M.C.A.: Combinatorial optimization on graphs of bounded treewidth. Comput. J. 51(3), 255–269 (2008)

    Article  Google Scholar 

  8. Bondy, J.A., Murty, U.S.R.: Graph theory, Graduate Texts in Mathematics, vol. 244. Springer Verlag, New York (2008)

    MATH  Google Scholar 

  9. Chakraborty, S., Meel, K.S., Vardi, M.Y.: Improving approximate counting for probabilistic inference: from linear to logarithmic SAT solver calls. In: Kambhampati, S. (ed.) Proceedings of 25th International Joint Conference on Artificial Intelligence (IJCAI 2016), pp. 3569–3576. The AAAI Press, New York City, July 2016

    Google Scholar 

  10. Charwat, G., Woltran, S.: Dynamic programming-based QBF solving. In: Lonsing, F., Seidl, M. (eds.) Proceedings of the 4th International Workshop on Quantified Boolean Formulas (QBF 2016), vol. 1719, pp. 27–40. CEUR Workshop Proceedings (CEUR-WS.org) (2016). Co-located with 19th International Conference on Theory and Applications of Satisfiability Testing (SAT 2016)

    Google Scholar 

  11. Choi, A., Van den Broeck, G., Darwiche, A.: Tractable learning for structured probability spaces: a case study in learning preference distributions. In: Yang, Q. (ed.) Proceedings of 24th International Joint Conference on Artificial Intelligence (IJCAI 2015). The AAAI Press (2015)

    Google Scholar 

  12. Cygan, M., Fomin, F.V., Kowalik, Ł., Lokshtanov, D., Marx, D., Pilipczuk, M., Pilipczuk, M., Saurabh, S.: Parameterized Algorithms. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21275-3

    Book  MATH  Google Scholar 

  13. Diestel, R.: Graph Theory. Graduate Texts in Mathematics, vol. 173, 4th edn. Springer, Heidelberg (2012)

    MATH  Google Scholar 

  14. Domshlak, C., Hoffmann, J.: Probabilistic planning via heuristic forward search and weighted model counting. J. Artif. Intell. Res. 30, 565–620 (2007)

    MathSciNet  MATH  Google Scholar 

  15. Downey, R.G., Fellows, M.R.: Fundamentals of Parameterized Complexity. TCS. Springer, London (2013). https://doi.org/10.1007/978-1-4471-5559-1

    Book  MATH  Google Scholar 

  16. Dueñas-Osorio, L., Meel, K.S., Paredes, R., Vardi, M.Y.: Counting-based reliability estimation for power-transmission grids. In: Singh, S.P., Markovitch, S. (eds.) Proceedings of the Thirty-First AAAI Conference on Artificial Intelligence (AAAI 2017), pp. 4488–4494. The AAAI Press, February 2017

    Google Scholar 

  17. Durand, A., Hermann, M., Kolaitis, P.G.: Subtractive reductions and complete problems for counting complexity classes. Theor. Comput. Sci. 340(3), 496–513 (2005)

    Article  MathSciNet  Google Scholar 

  18. Fichte, J.K., Hecher, M., Morak, M., Woltran, S.: Answer set solving with bounded treewidth revisited. In: Balduccini, M., Janhunen, T. (eds.) LPNMR 2017. LNCS (LNAI), vol. 10377, pp. 132–145. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-61660-5_13

    Chapter  Google Scholar 

  19. Fichte, J.K., Hecher, M., Morak, M., Woltran, S.: DynASP2.5: dynamic programming on tree decompositions in action. In: Lokshtanov, D., Nishimura, N. (eds.) Proceedings of the 12th International Symposium on Parameterized and Exact Computation (IPEC 2017). Dagstuhl Publishing (2017)

    Google Scholar 

  20. Flum, J., Grohe, M.: Parameterized Complexity Theory. TTCS, vol. XIV. Springer, Berlin (2006). https://doi.org/10.1007/3-540-29953-X

    Book  MATH  Google Scholar 

  21. Gebser, M., Schaub, T., Thiele, S., Veber, P.: Detecting inconsistencies in large biological networks with answer set programming. Theory Pract. Log. Program. 11(2–3), 323–360 (2011)

    Article  MathSciNet  Google Scholar 

  22. Gebser, M., Kaufmann, B., Schaub, T.: Solution enumeration for projected boolean search problems. In: van Hoeve, W.-J., Hooker, J.N. (eds.) CPAIOR 2009. LNCS, vol. 5547, pp. 71–86. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-01929-6_7

    Chapter  MATH  Google Scholar 

  23. Ginsberg, M.L., Parkes, A.J., Roy, A.: Supermodels and robustness. In: Rich, C., Mostow, J. (eds.) Proceedings of the 15th National Conference on Artificial Intelligence and 10th Innovative Applications of Artificial Intelligence Conference (AAAI/IAAI 1998), pp. 334–339. The AAAI Press, Madison, July 1998

    Google Scholar 

  24. Gomes, C.P., Sabharwal, A., Selman, B.: Chapter 20: model counting. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 633–654. IOS Press, Amsterdam (2009)

    Google Scholar 

  25. Graham, R.L., Grötschel, M., Lovász, L.: Handbook of Combinatorics, vol. I. Elsevier Science Publishers, North-Holland (1995)

    MATH  Google Scholar 

  26. Harvey, D., van der Hoeven, J., Lecerf, G.: Even faster integer multiplication. J. Complex. 36, 1–30 (2016)

    Article  MathSciNet  Google Scholar 

  27. Hemaspaandra, L.A., Vollmer, H.: The satanic notations: Counting classes beyond #P and other definitional adventures. SIGACT News 26(1), 2–13 (1995)

    Article  Google Scholar 

  28. Impagliazzo, R., Paturi, R., Zane, F.: Which problems have strongly exponential complexity? J. Comput. Syst. Sci. 63(4), 512–530 (2001)

    Article  MathSciNet  Google Scholar 

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

    MATH  Google Scholar 

  30. Knuth, D.E.: How fast can we multiply? In: The Art of Computer Programming, Seminumerical Algorithms, 3 edn., vol. 2, chap. 4.3.3, pp. 294–318. Addison-Wesley (1998)

    Google Scholar 

  31. Lagniez, J.M., Marquis, P.: An improved decision-DNNF compiler. In: Sierra, C. (ed.) Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence (IJCAI 2017). The AAAI Press (2017)

    Google Scholar 

  32. Lampis, M., Mitsou, V.: Treewidth with a quantifier alternation revisited. In: Lokshtanov, D., Nishimura, N. (eds.) Proceedings of the 12th International Symposium on Parameterized and Exact Computation (IPEC 2017). Dagstuhl Publishing (2017)

    Google Scholar 

  33. Manning, C.D., Raghavan, P., Schütze, H.: Introduction to Information Retrieval. Cambridge University Press, Cambridge (2008)

    Book  Google Scholar 

  34. Niedermeier, R.: Invitation to Fixed-Parameter Algorithms. Oxford Lecture Series in Mathematics and its Applications, vol. 31. Oxford University Press, New York (2006)

    Book  Google Scholar 

  35. Papadimitriou, C.H.: Computational Complexity. Addison-Wesley, Boston (1994)

    MATH  Google Scholar 

  36. Pichler, R., Rümmele, S., Woltran, S.: Counting and enumeration problems with bounded treewidth. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 387–404. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-17511-4_22

    Chapter  MATH  Google Scholar 

  37. Pourret, O., Naim, P., Bruce, M.: Bayesian Networks - A Practical Guide to Applications. Wiley, Hoboken (2008)

    MATH  Google Scholar 

  38. Roth, D.: On the hardness of approximate reasoning. Artif. Intell. 82(1–2), 273–302 (1996)

    Article  MathSciNet  Google Scholar 

  39. Sæther, S.H., Telle, J.A., Vatshelle, M.: Solving #SAT and MAXSAT by dynamic programming. J. Artif. Intell. Res. 54, 59–82 (2015)

    MathSciNet  MATH  Google Scholar 

  40. Sahami, M., Dumais, S., Heckerman, D., Horvitz, E.: A Bayesian approach to filtering junk e-mail. In: Joachims, T. (ed.) Proceedings of the AAAI-98 Workshop on Learning for Text Categorization, vol. 62, pp. 98–105 (1998)

    Google Scholar 

  41. Samer, M., Szeider, S.: Algorithms for propositional model counting. J. Discret. Algorithms 8(1), 50–64 (2010)

    Article  MathSciNet  Google Scholar 

  42. Sang, T., Beame, P., Kautz, H.: Performing Bayesian inference by weighted model counting. In: Veloso, M.M., Kambhampati, S. (eds.) Proceedings of the 29th National Conference on Artificial Intelligence (AAAI 2005). The AAAI Press (2005)

    Google Scholar 

  43. Valiant, L.: The complexity of enumeration and reliability problems. SIAM J. Comput. 8(3), 410–421 (1979)

    Article  MathSciNet  Google Scholar 

  44. Wilder, R.L.: Introduction to the Foundations of Mathematics, 2nd edn. Wiley, New York (1965)

    MATH  Google Scholar 

  45. Xue, Y., Choi, A., Darwiche, A.: Basing decisions on sentences in decision diagrams. In: Hoffmann, J., Selman, B. (eds.) Proceedings of the 26th AAAI Conference on Artificial Intelligence (AAAI 2012). The AAAI Press (2012)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute of Logic and Computation, TU Wien, Vienna, Austria

    Johannes K. Fichte, Markus Hecher, Michael Morak & Stefan Woltran

Authors
  1. Johannes K. Fichte
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Markus Hecher
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Michael Morak
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Stefan Woltran
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding authors

Correspondence to Johannes K. Fichte , Markus Hecher , Michael Morak or Stefan Woltran .

Editor information

Editors and Affiliations

  1. Friedrich Schiller University Jena, Jena, Germany

    Olaf Beyersdorff

  2. Microsoft Research Ltd., Cambridge, United Kingdom

    Christoph M. Wintersteiger

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG, part of Springer Nature

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Fichte, J.K., Hecher, M., Morak, M., Woltran, S. (2018). Exploiting Treewidth for Projected Model Counting and Its Limits. In: Beyersdorff, O., Wintersteiger, C. (eds) Theory and Applications of Satisfiability Testing – SAT 2018. SAT 2018. Lecture Notes in Computer Science(), vol 10929. Springer, Cham. https://doi.org/10.1007/978-3-319-94144-8_11

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-94144-8_11

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-94143-1

  • Online ISBN: 978-3-319-94144-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation