Hostname: page-component-586b7cd67f-t7fkt Total loading time: 0 Render date: 2024-11-24T03:36:52.511Z Has data issue: false hasContentIssue false

Exploiting Database Management Systems and Treewidth for Counting

Published online by Cambridge University Press:  12 March 2021

JOHANNES K. FICHTE
Affiliation:
UC Berkeley, Berkeley, CA, USA (e-mail: [email protected])
MARKUS HECHER
Affiliation:
TU Wien, Vienna, Austria (e-mails: [email protected], [email protected], [email protected])
PATRICK THIER
Affiliation:
TU Wien, Vienna, Austria (e-mails: [email protected], [email protected], [email protected])
STEFAN WOLTRAN
Affiliation:
TU Wien, Vienna, Austria (e-mails: [email protected], [email protected], [email protected])

Abstract

Bounded treewidth is one of the most cited combinatorial invariants in the literature. It was also applied for solving several counting problems efficiently. A canonical counting problem is #Sat, which asks to count the satisfying assignments of a Boolean formula. Recent work shows that benchmarking instances for #Sat often have reasonably small treewidth. This paper deals with counting problems for instances of small treewidth. We introduce a general framework to solve counting questions based on state-of-the-art database management systems (DBMSs). Our framework takes explicitly advantage of small treewidth by solving instances using dynamic programming (DP) on tree decompositions (TD). Therefore, we implement the concept of DP into a DBMS (PostgreSQL), since DP algorithms are already often given in terms of table manipulations in theory. This allows for elegant specifications of DP algorithms and the use of SQL to manipulate records and tables, which gives us a natural approach to bring DP algorithms into practice. To the best of our knowledge, we present the first approach to employ a DBMS for algorithms on TDs. A key advantage of our approach is that DBMSs naturally allow for dealing with huge tables with a limited amount of main memory (RAM).

Type
Rapid Communication
Copyright
© The Author(s), 2021. Published by Cambridge University Press

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

Footnotes

*

This is an extended version of a paper (Fichte et al. 2020) that appeared in the Proceedings of the 22nd International Symposium on Practical Aspects of Declarative Languages (PADL’20).

References

Abseher, M., Musliu, N. and Woltran, S. 2017. htd – a free, open-source framework for (customized) TDPs and beyond. In Proceedings of the 14th International Conference on Integration of AI and OR Techniques in Constraint Programming (CPAIOR’17), D. S. Lombardi, Ed. Lecture Notes in Computer Science, vol. 10335. Springer Verlag, Padua, Italy, 376386.Google Scholar
Bacchus, F., Dalmao, S. and Pitassi, T. 2003. Algorithms and complexity results for #SAT and Bayesian inference. In Proceedings of the 44th Annual IEEE Symposium on Foundations of Computer Science (FOCS’03), Chekuri, C. S. and Micciancio, D., Eds. IEEE Computer Society, Cambridge, MA, USA, 340–351.Google Scholar
Bannach, M. and Berndt, S. 2019. Practical access to dynamic programming on tree decompositions. Algorithms 12, 8, 172.CrossRefGoogle Scholar
Bliem, B., Charwat, G., Hecher, M. and Woltran, S. 2016. D-flat2: Subset minimization in dynamic programming on tree decompositions made easy. Fundamentals of Informatics 147, 1, 2761.CrossRefGoogle Scholar
Bodlaender, H. and Koster, A. 2008. Combinatorial optimization on graphs of bounded treewidth. The Computer Journal 51, 3, 255269.Google Scholar
Bodlaender, H. L. 1988. Dynamic programming on graphs with bounded treewidth. In Automata, Languages and Programming, Lepistö, T. and Salomaa, A., Eds. Springer, Berlin, Heidelberg, 105118.CrossRefGoogle Scholar
Bomanson, J., Gebser, M., Janhunen, T., Kaufmann, B. and Schaub, T. 2016. Answer set programming modulo acyclicity. Fundamentals of Informatics 147, 1, 6391.CrossRefGoogle Scholar
Burchard, J., Schubert, T. and Becker, B. 2015. Laissez-faire caching for parallel #SAT solving. In SAT’15, Heule, M. and Weaver, S., Eds. Lecture Notes in Computer Science, vol. 9340. Springer Verlag, Austin, TX, USA, 4661.Google Scholar
Burchard, J., Schubert, T. and Becker, B. 2016. Distributed parallel #SAT solving. In Proceedings of the 2016 IEEE International Conference on Cluster Computing (CLUSTER’16), de Supinski, B. R., Ed. IEEE Computer Society, Taipei, Taiwan, 326335.CrossRefGoogle Scholar
Chakraborty, S., Fremont, D. J., Meel, K. S., Seshia, S. A. and Vardi, M. Y. 2014. Distribution-aware sampling and weighted model counting for SAT. In Proceedings of the 28th Conference on Artificial Intelligence (AAAI’14), C. E. Brodley and P. Stone, Eds. The AAAI Press, Québec City, QC, Canada, 17221730.Google Scholar
Chakraborty, S., Meel, K. S. and Vardi, M. Y. 2016. Improving approximate counting for probabilistic inference: From linear to logarithmic SAT solver calls. In Proceedings of the 25th International Joint Conference on Artificial Intelligence (IJCAI’16), Kambhampati, S., Ed. The, AAAI Press, New York City, NY, USA, 35693576.Google Scholar
Charwat, G. and Woltran, S. 2019. Expansion-based QBF solving on tree decompositions. Fundamentals of Informatics 167, 1–2, 5992.CrossRefGoogle Scholar
Choi, A., Van den Broeck, G. and Darwiche, A. 2015. Tractable learning for structured probability spaces: A case study in learning preference distributions. In Proceedings of the 24th International Joint Conference on Artificial Intelligence (IJCAI’15), Yang, Q., Ed. The AAAI Press, Buenos Aires, Argentina, 28612868.Google Scholar
Clark, K. L. 1977. Negation as failure. In Logic and Data Bases. Advances in Data Base Theory. Plemum Press, New York, 293322.Google Scholar
Codd, E. F. 1970. A relational model of data for large shared data banks. Communications of the ACM 13, 6, 377387.CrossRefGoogle Scholar
Cygan, M., Fomin, F. V., Kowalik, Ł., Lokshtanov, D., Dániel Marx, M. P., Pilipczuk, M. and Saurabh, S. 2015. Parameterized Algorithms. Springer Verlag, Cham, Heidelberg, New York, Dordrecht, London.CrossRefGoogle Scholar
Darwiche, A. 2004. New advances in compiling CNF to decomposable negation normal form. In Proceedings of the 16th European Conference on Artificial Intelligence (ECAI’04), López De Mántaras, R. and Saitta, L., Eds. IOS Press, Valencia, Spain, 318322.Google Scholar
Darwiche, A. 2011. SDD: A new canonical representation of propositional knowledge bases. In Proceedings of the 22nd International Joint Conference on Artificial Intelligence (IJCAI’11), T. Walsh, Ed. AAAI Press/IJCAI, Barcelona, Catalonia, Spain, 819826.Google Scholar
Dechter, R. 1999. Bucket elimination: A unifying framework for reasoning. Artificial Intelligence 113, 1, 4185.CrossRefGoogle Scholar
Dell, H., Komusiewicz, C., Talmon, N. and Weller, M. 2018. The PACE 2017 parameterized algorithms and computational experiments challenge: The second iteration. In IPEC 2017, Lokshtanov, D. and Nishimura, N., Eds. Leibniz International Proceedings in Informatics (LIPIcs), vol. 89. Dagstuhl Publishing, Vienna, Austria, 30:1–30:12.Google Scholar
Diestel, R. 2012. Graph Theory, 4th ed. Graduate Texts in Mathematics, vol. 173. Springer Verlag, Heidelberg.Google Scholar
Domshlak, C. and Hoffmann, J. 2007. Probabilistic planning via heuristic forward search and weighted model counting. Journal of Artificial Intelligence Research 30, 156.CrossRefGoogle Scholar
Doubilet, P., Rota, G.-C. and Stanley, R. 1972. On the foundations of combinatorial theory. vi. the idea of generating function. In Berkeley Symposium on Mathematical Statistics and Probability, Cam, L. M. L., Neyman, J. and Scott, E. L., Eds. University of California Press, Berkeley, CA, USA, 2: 267318.Google Scholar
Dudek, J. M., Phan, V. H. N. and Vardi, M. Y. 2020. DPMC: Weighted model counting by dynamic programming on project-join trees. In Proceedings of the 26th International Conference on Principles and Practice of Constraint Programming (CP’20), H. Simonis, Ed. Lecture Notes in Computer Science, vol. 12333. Springer Verlag, Cham, 211230.CrossRefGoogle Scholar
Dueñas-Osorio, L., Meel, K. S., Paredes, R. and Vardi, M. Y. 2017. Counting-based reliability estimation for power-transmission grids. In Proceedings of the 31st AAAI Conference on Artificial Intelligence (AAAI’17), Singh, S. P. and Markovitch, S., Eds. The AAAI Press, San Francisco, CA, USA, 44884494.Google Scholar
Durand, A. and Mengel, S. 2015. Structural tractability of counting of solutions to conjunctive queries. Theoretical Computer Science 57, 4, 12021249.Google Scholar
Dzulfikar, M. A., Fichte, J. K. and Hecher, M. 2019. The PACE 2019 parameterized algorithms and computational experiments challenge: The fourth iteration (invited paper). In Proceedings of the 14th International Symposium on Parameterized and Exact Computation (IPEC’19), Jansen, B. M. P. and Telle, J. A., Eds. Leibniz International Proceedings in Informatics (LIPIcs), vol. 148. Dagstuhl Publishing, Munich, Germany, 25:1–25:23.Google Scholar
Elmasri, R. and Navathe, S. B. 2016. Fundamentals of Database Systems, 7th ed. Pearson.Google Scholar
Ermon, S., Gomes, C. P. and Selman, B. 2012. Uniform solution sampling using a constraint solver as an oracle. In Proceedings of the 28th Conference on Uncertainty in Artificial Intelligence (UAI’12), de Freitas, N. and Murphy, K., Eds. AUAI Press, Catalina Island, CA, USA, 255264.Google Scholar
Fichte, J. K., Hecher, M. and Hamiti, F. 2020. The model counting competition 2020. CoRR abs/2012.01323, 1–25.Google Scholar
Fichte, J. K., Hecher, M. and Meier, A. 2019. Counting complexity for reasoning in abstract argumentation. In Proceedings of the 33rd AAAI Conference on Artificial Intelligence (AAAI’19), P. V. Hentenryck and Z.-H. Zhou, Eds. The AAAI Press, Honolulu, Hawaii, USA, 28272834.Google Scholar
Fichte, J. K., Hecher, M. and Meier, A. in press. Counting complexity for reasoning in abstract argumentation. In Proceedings of the 35rd AAAI Conference on Artificial Intelligence (AAAI’21), K. Leyton-Brown and Mausam, Eds. The AAAI Press, Vancouver, Canada.Google Scholar
Fichte, J. K., Hecher, M., Morak, M. and Woltran, S. 2018. Exploiting treewidth for projected model counting and its limits. In Proceedings of the 21st International Conference on Theory and Applications of Satisfiability Testing (SAT’18), Beyersdorff, O. and Wintersteiger, C. M., Eds. Lecture Notes in Computer Science, vol. 10929. Springer Verlag, Oxford, UK, 165184. Held as Part of the Federated Logic Conference, FloC’18.Google Scholar
Fichte, J. K., Hecher, M. and Pfandler, A. 2020. Lower bounds for QBFs of bounded treewidth. In Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS’20), N. Kobayashi, Ed. Association for Computing Machinery, New York, Saarbrücken, Germany, 410424.CrossRefGoogle Scholar
Fichte, J. K., Hecher, M. and Schindler, I. 2018. Default logic and bounded treewidth. In Proceedings of the 12th International Conference on Language and Automata Theory and Applications (LATA’18), Klein, S. T. and Martn-Vide, C., Eds. Lecture Notes in Computer Science. Springer Verlag, Ramat Gan, Israel.Google Scholar
Fichte, J. K., Hecher, M. and Szeider, S. 2020. Breaking symmetries with rootclique and lextopsort. In Proceedings of the 26th International Conference on Principles and Practice of Constraint Programming (CP’20), H. Simonis, Ed. Lecture Notes in Computer Science, vol. 12333. Springer Verlag, Louvain-la-Neuve, Belgium, 286303.CrossRefGoogle Scholar
Fichte, J. K., Hecher, M., Thier, P. and Woltran, S. 2020. Exploiting database management systems and treewidth for counting. In Proceedings of the 22nd International Symposium on Practical Aspects of Declarative Languages (PADL’20), Komendantskaya, E. and Liu, Y. A., Eds. Lecture Notes in Computer Science, vol. 12007. Springer Verlag, New Orleans, LA, USA, 151167.CrossRefGoogle Scholar
Fichte, J. K., Hecher, M., Woltran, S. and Zisser, M. 2018a. A Benchmark Collection of #SAT Instances and Tree Decompositions (Benchmark Set). URL: https://doi.org/10.5281/zenodo.1299752.CrossRefGoogle Scholar
Fichte, J. K., Hecher, M., Woltran, S. and Zisser, M. 2018b. Weighted model counting on the GPU by exploiting small treewidth. In Proceedings of the 26th Annual European Symposium on Algorithms (ESA’18), Azar, Y., Bast, H. and Herman, G., Eds. Leibniz International Proceedings in Informatics (LIPIcs), vol. 112. Dagstuhl Publishing, Helsinki, Finland, 28:1–28:16.Google Scholar
Fichte, J. K., Hecher, M. and Zisser, M. 2019. An improved GPU-based SAT model counter. In Proceedings of the 25th International Conference on Principles and Practice of Constraint Programming (CP’19), Schiex, T. and de Givry, S., Eds. Springer Verlag, Stamford, CT, USA, 491509.Google Scholar
Fichte, J. K., Manthey, N., Stecklina, J. and Schidler, A. 2020. Towards faster reasoners by using transparent huge pages. In Proceedings of the 26th International Conference on Principles and Practice of Constraint Programming (CP’20), Simonis, H., Ed. Lecture Notes in Computer Science, vol. 12333. Springer Verlag, Louvain-la-Neuve, Belgium, 304322.CrossRefGoogle Scholar
Gabriel, E., Fagg, G. E., Bosilca, G., Angskun, T., Dongarra, J. J., Squyres, J. M., Sahay, V., Kambadur, P., Barrett, B., Lumsdaine, A., Castain, R. H., Daniel, D. J., Graham, R. L. and Woodall, T. S. 2004. Open MPI: Goals, concept, and design of a next generation MPI implementation. In Proceedings of the 11th European PVM/MPI Users’ Group Meeting, Kranzlmüller, D., Kacsuk, P. and Dongarra, J. J., Eds. Lecture Notes in Computer Science, vol. 3241. Springer Verlag, Budapest, Hungary, 97–104.Google Scholar
Garcia-Molina, H., Ullman, J. D. and Widom, J. 2009. Database Systems: the Complete Book, 2nd ed. Pearson Prentice Hall, Upper Saddle River, New Jersey.Google Scholar
Gomes, C. P., Sabharwal, A. and Selman, B. 2009. Chapter 20: Model counting. In Handbook of Satisfiability, A. Biere, M. Heule, H. van Maaren and T. Walsh, Eds. Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press, Amsterdam, Netherlands, 633–654.Google Scholar
Gottlob, G., Pichler, R. and Wei, F. 2006. Bounded treewidth as a key to tractability of knowledge representation and reasoning. In Proceedings of the 21st National Conference on Artificial Intelligence (AAAI’06), J. A. Hendler, Ed. The, AAAI Press, Boston, MA, USA, 250–256.Google Scholar
Gottlob, G., Pichler, R. and Wei, F. 2007. Efficient datalog abduction through bounded treewidth. In Proceedings of the 22nd AAAI Conference on Artificial Intelligence (AAAI’07), Holte, R. C. and Howe, A., Eds. The AAAI Press, Vancouver, BC, Canada, 16261631.Google Scholar
Gottlob, G. and Szeider, S. 2007. Fixed-parameter algorithms for artificial intelligence, constraint satisfaction and database problems. The Computer Journal 51, 3 (09), 303325.CrossRefGoogle Scholar
Grohe, M. 2007. The complexity of homomorphism and constraint satisfaction problems seen from the other side. Journal of the ACM 54, 1, 1:1–1:24.Google Scholar
Hecher, M., Morak, M. and Woltran, S. 2020. Structural decompositions of epistemic logic programs. In Proceedings of the 34th AAAI Conference on Artificial Intelligence (AAAI’20), V. Conitzer and F. Sha, Eds. The AAAI Press, New York City, NY, USA, 2830–2837.Google Scholar
Hecher, M., Thier, P. and Woltran, S. 2020. Taming high treewidth with abstraction, nested dynamic programming, and database technology. In Proceedings of the 23rd International Conference on Theory and Applications of Satisfiability Testing (SAT’20), Pulina, L. and Seidl, M., Eds. Lecture Notes in Computer Science, vol. 12178. Springer Verlag, Alghero, Italy, 343–360.Google Scholar
Janhunen, T. 2006. Some (in)translatability results for normal logic programs and propositional theories. Journal of Applied Non-Classical Logics 16, 1–2, 3586.CrossRefGoogle Scholar
Jégou, P. and Terrioux, C. 2014. Tree-decompositions with connected clusters for solving constraint networks. In Proceedings of the 20th International Conference on Principles and Practice of Constraint Programming (CP’14), B. O’Sullivan, Ed. Lecture Notes in Computer Science, vol. 8656. Springer Verlag, Lyon, France, 407–423.Google Scholar
Khamis, M. A., Ngo, H. Q. and Rudra, A. 2016. FAQ: Questions asked frequently. In Proceedings of the 35th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems (PODS’16), T. Milo and W. Tan, Eds. Association for Computing Machinery, New York, San Francisco, CA, USA, 13–28.Google Scholar
Kiljan, K. and Pilipczuk, M. 2018. Experimental evaluation of parameterized algorithms for feedback vertex set. In Proceedings of the 17th International Symposium on Experimental Algorithms (SEA’18), G. D’Angelo, Ed. Leibniz International Proceedings in Informatics (LIPIcs), vol. 103. Dagstuhl Publishing, Dagstuhl, Germany, 12:1–12:12.Google Scholar
Kleine Büning, H. and Lettman, T. 1999. Propositional Logic: Deduction and Algorithms. Cambridge University Press, Cambridge, New York, NY, USA.Google Scholar
Kloks, T. 1994. Treewidth. Computations and Approximations. Lecture Notes in Computer Science, vol. 842. Springer Verlag, Berlin, Heidelber.Google Scholar
Koriche, F., Lagniez, J.-M., Marquis, P. and Thomas, S. 2013. Knowledge compilation for model counting: Affine decision trees. In Proceedings of the 23rd International Joint Conference on Artificial Intelligence (IJCAI’13), Rossi, F. and Thrun, S., Eds. The AAAI Press, Beijing, China.Google Scholar
Lagniez, J. and Marquis, P. 2014. Preprocessing for propositional model counting. In Proceedings of the 28th AAAI Conference on Artificial Intelligence (AAAI’14), C. E. Brodley and P. Stone, Eds. The AAAI Press, Québec City, QC, Canada, 2688–2694.Google Scholar
Lagniez, J.-M. and Marquis, P. 2017. An improved decision-DDNF compiler. In Proceedings of the 26th International Joint Conference on Artificial Intelligence (IJCAI’17), C. Sierra, Ed. The AAAI Press, Melbourne, VIC, Australia, 667–673.Google Scholar
Lagniez, J.-M., Marquis, P. and Szczepanski, N. 2018. DMC: A distributed model counter. In Proceedings of the 27th International Joint Conference on Artificial Intelligence (IJCAI’18), J. Lang, Ed. The AAAI Press, Stockholm, Sweden, 1331–1338.Google Scholar
Langer, A., Reidl, F., Rossmanith, P. and Sikdar, S. 2012. Evaluation of an MSO-solver. In Proceedings of the Meeting on Algorithm Engineering & Expermiments (ALENEX’12), Bader, D. A. and Mutzel, P., Eds. Society for Industrial and Applied Mathematics (SIAM), Miyako, Kyoto, Japan, 55–63.Google Scholar
Liu, J., Zhong, W. and Jiao, L. 2006. Comments on “the 1993 DIMACS graph coloring challenge” and “energy function-based approaches to graph coloring”. IEEE Transactions on Neural Networks 17, 2, 533.Google Scholar
Muise, C. J., McIlraith, S. A., Beck, J. C. and Hsu, E. I. 2012. Dsharp: Fast d-DNNF compilation with sharpSAT. In Proceedings of the 25th Canadian Conference on Artificial Intelligence (AI’17), Kosseim, L. and Inkpen, D., Eds. Lecture Notes in Computer Science, vol. 7310. Springer Verlag, Toronto, ON, Canada, 356–361.Google Scholar
Oztok, U. and Darwiche, A. 2015. A top-down compiler for sentential decision diagrams. In Proceedings of the 24th International Joint Conference on Artificial Intelligence (IJCAI’15), Yang, Q. and Wooldridge, M., Eds. The AAAI Press, Buenos Aires, Argentina, 3141–3148.Google Scholar
Pan, G. and Vardi, M. Y. 2006. Fixed-parameter hierarchies inside PSPACE. In Proceedings of the 21st Annual IEEE Symposium on Logic in Computer Science (LICS’06), R. Alur, Ed. IEEE Computer Society, Seattle, WA, USA, 27–36.Google Scholar
PostgreSQL Global Development Group. 2020. PostgreSQL documentation 12. URL: https://www.postgresql.org/docs/12/queries-with.html.Google Scholar
Roth, D. 1996. On the hardness of approximate reasoning. Artificial Intelligence 82, 1–2, 273302.CrossRefGoogle Scholar
Samer, M. and Szeider, S. 2010. Algorithms for propositional model counting. Journal of Discrete Algorithms 8, 1, 5064.CrossRefGoogle Scholar
Sang, T., Bacchus, F., Beame, P., Kautz, H. and Pitassi, T. 2004. Combining component caching and clause learning for effective model counting. In Proceedings of the 7th International Conference on Theory and Applications of Satisfiability Testing (SAT’04), Hoos, H. H. and Mitchell, D. G., Eds. Springer Verlag, Vancouver, BC, Canada, 19.Google Scholar
Sang, T., Beame, P. and Kautz, H. 2005. Performing Bayesian inference by weighted model counting. In Proceedings of the 20th National Conference on Artificial Intelligence (AAAI’05), Veloso, M. M. and Kambhampati, S., Eds. The AAAI Press, Pittsburgh, Pennsylvania, USA, 475481.Google Scholar
Sharma, S., Roy, S., Soos, M. and Meel, K. S. 2019. GANAK: A scalable probabilistic exact model counter. In Proceedings of the 28th International Joint Conference on Artificial Intelligence (IJCAI’19), S. Kraus, Ed. ijcai.org, Macao, China, 11691176.Google Scholar
Strasser, B. 2017. Computing tree decompositions with flowcutter: PACE 2017 submission. CoRR abs/1709.08949, 19.Google Scholar
Thurley, M. 2006. sharpSAT – counting models with advanced component caching and implicit BCP. In Proceedings of the 9th International Conference on International Conference on Theory and Applications of Satisfiability Testing (SAT’06), Biere, A. and Gomes, C. P., Eds. Lecture Notes in Computer Science, vol. 4121. Springer Verlag, Seattle, WA, USA, 424–429.Google Scholar
Toda, S. 1991. PP is as hard as the polynomial-time hierarchy. SIAM Journal on Computing 20, 5, 865877.CrossRefGoogle Scholar
Toda, T. and Soh, T. 2015. Implementing efficient all solutions SAT solvers. ACM Journal of Experimental Algorithmics 21, 1.12. Special Issue SEA 2014.Google Scholar
Ullman, J. D. 1989. Principles of Database and Knowledge-Base Systems, Volume II. Computer Science Press, New York, NY, USA.Google Scholar
Xue, Y., Choi, A. and Darwiche, A. 2012. Basing decisions on sentences in decision diagrams. In Proceedings of the 26th AAAI Conference on Artificial Intelligence (AAAI’12), Hoffmann, J. and Selman, B., Eds. The AAAI Press, Toronto, ON, Canada, 842–849.Google Scholar