Skip to main content
SpringerLink
Log in

ProCount: Weighted Projected Model Counting with Graded Project-Join Trees

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

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

Abstract

Recent work in weighted model counting proposed a unifying framework for dynamic-programming algorithms. The core of this framework is a project-join tree: an execution plan that specifies how Boolean variables are eliminated. We adapt this framework to compute exact literal-weighted projected model counts of propositional formulas in conjunctive normal form. Our key conceptual contribution is to define gradedness on project-join trees, a novel condition requiring irrelevant variables to be eliminated before relevant variables. We prove that building graded project-join trees can be reduced to building standard project-join trees and that graded project-join trees can be used to compute projected model counts. The resulting tool ProCount is competitive with the state-of-the-art tools \(\texttt {D4}_{\texttt {P}}\), projMC, and reSSAT, achieving the shortest solving time on 131 benchmarks of 390 benchmarks solved by at least one tool, from 849 benchmarks in total.

Work supported in part by NSF grants CCF-1704883, DMS-1547433, IIS-1527668, and IIS-1830549, DoD MURI grant N00014-20-1-2787, and an award from the Maryland Procurement Office.

Authors sorted alphabetically by surnames.

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 89.00
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 119.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.

    nestHDB is an unweighted tool, but the benchmarks in Sect. 5 are weighted. Moreover, the cluster used in Sect. 5 does not support database management systems.

References

  1. Abo Khamis, M., Ngo, H.Q., Rudra, A.: FAQ: questions asked frequently. In: PODS, pp. 13–28 (2016)

    Google Scholar 

  2. Abseher, M., Musliu, N., Woltran, S.: htd-a free, open-source framework for (customized) tree decompositions and beyond. In: CPAIOR, pp. 376–386 (2017). https://doi.org/10.1007/978-3-319-59776-8_30

  3. Aguirre, A.S.M., Vardi, M.: Random 3-SAT and BDDs: the plot thickens further. In: CP, pp. 121–136 (2001). https://doi.org/10.1007/3-540-45578-7_9

  4. Aziz, R.A., Chu, G., Muise, C., Stuckey, P.: Projected model counting. In: SAT, pp. 121–137 (2015)

    Google Scholar 

  5. Bacchus, F., Dalmao, S., Pitassi, T.: Solving #SAT and Bayesian inference with backtracking search. JAIR 34, 391–442 (2009). https://doi.org/10.1613/jair.2648

    Article  MathSciNet  MATH  Google Scholar 

  6. Bahar, R.I., et al.: Algebraic decision diagrams and their applications. Form. Method Syst. Des. 10(2–3), 171–206 (1997). https://doi.org/10.1023/A:1008699807402

    Article  Google Scholar 

  7. Bellman, R.: Dynamic programming. Science 153(3731), 34–37 (1966). https://doi.org/10.1126/science.153.3731.34

    Article  MATH  Google Scholar 

  8. Bouquet, F.: Gestion de la dynamicité et énumération d’impliquants premiers: une approche fondée sur les Diagrammes de Décision Binaire. Ph.D. thesis, Aix-Marseille 1 (1999). https://www.theses.fr/1999AIX11011

  9. Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE TC 100(8), 677–691 (1986). https://doi.org/10.1109/TC.1986.1676819

    Article  MATH  Google Scholar 

  10. Charwat, G., Woltran, S.: BDD-based dynamic programming on tree decompositions. Technical report, Technische Universität Wien, Institut für Informationssysteme (2016). https://dbai.tuwien.ac.at/research/report/dbai-tr-2016-95.pdf

  11. Dalmau, V., Kolaitis, P.G., Vardi, M.Y.: Constraint satisfaction, bounded treewidth, and finite-variable logics. In: CP, pp. 310–326 (2002). https://doi.org/10.1007/3-540-46135-3_21

  12. Darwiche, A.: New advances in compiling CNF to decomposable negation normal form. In: ECAI, pp. 318–322 (2004). https://dl.acm.org/doi/10.5555/3000001.3000069

  13. Dechter, R.: Bucket elimination: a unifying framework for reasoning. AIJ 113(1–2), 41–85 (1999). https://doi.org/10.1016/S0004-3702(99)00059-4

    Article  MathSciNet  MATH  Google Scholar 

  14. Dechter, R.: Constraint Processing. Morgan Kaufmann (2003). https://doi.org/10.1016/B978-1-55860-890-0.X5000-2

  15. van Dijk, T., van de Pol, J.: Sylvan: multi-core decision diagrams. In: TACAS, pp. 677–691 (2015). https://doi.org/10.1007/978-3-662-46681-0_60

  16. Dudek, J.M., Dueñas-Osorio, L., Vardi, M.Y.: Efficient contraction of large tensor networks for weighted model counting through graph decompositions (2019). arXiv preprint arXiv:1908.04381

  17. Dudek, J.M., Phan, V.H.N., Vardi, M.Y.: DPMC: weighted model counting by dynamic programming on project-join trees. In: CP, pp. 211–230 (2020). arxiv.org/abs/2008.08748

  18. Dudek, J.M., Phan, V.H., Vardi, M.Y.: ADDMC: weighted model counting with algebraic decision diagrams. AAAI 34, 1468–1476 (2020). https://doi.org/10.1609/aaai.v34i02.5505

    Article  Google Scholar 

  19. Dudek, J.M., Vardi, M.Y.: Parallel weighted model counting with tensor networks. In: MCW (2020). https://mccompetition.org/assets/files/2020/MCW_2020_paper_1.pdf

  20. Duenas-Osorio, L., Meel, K.S., Paredes, R., Vardi, M.Y.: Counting-based reliability estimation for power-transmission grids. In: AAAI. pp. 4488–4494 (2017)

    Google Scholar 

  21. Ermon, S., Gomes, C., Sabharwal, A., Selman, B.: Taming the curse of dimensionality: discrete integration by hashing and optimization. In: ICML, pp. 334–342 (2013)

    Google Scholar 

  22. Fichte, J.K., Hecher, M.: Counting with bounded treewidth: meta algorithm and runtime guarantees. In: NMR, pp. 9–18 (2020)

    Google Scholar 

  23. Fichte, J.K., Hecher, M., Hamiti, F.: The Model Counting Competition 2020 (2020). arXiv preprint arXiv:2012.01323

  24. Fichte, J.K., Hecher, M., Morak, M., Woltran, S.: Exploiting treewidth for projected model counting and its limits. In: SAT, pp. 165–184 (2018)

    Google Scholar 

  25. Fichte, J.K., Hecher, M., Thier, P., Woltran, S.: Exploiting database management systems and treewidth for counting. In: PADL, pp. 151–167 (2020). https://doi.org/10.1007/978-3-030-39197-3_10

  26. Fremont, D.J., Rabe, M.N., Seshia, S.A.: Maximum model counting. In: AAAI, pp. 3885–3892 (2017)

    Google Scholar 

  27. Gupta, R., Sharma, S., Roy, S., Meel, K.S.: WAPS: weighted and projected sampling. In: TACAS, pp. 59–76 (2019)

    Google Scholar 

  28. Hamann, M., Strasser, B.: Graph bisection with pareto optimization. JEA 23, 1–34 (2018)

    MathSciNet  MATH  Google Scholar 

  29. Hecher, M., Thier, P., Woltran, S.: Taming high treewidth with abstraction, nested dynamic programming, and database technology. In: SAT, pp. 343–360 (2020)

    Google Scholar 

  30. Impagliazzo, R., Paturi, R., Zane, F.: Which problems have strongly exponential complexity? JCSS 63(4), 512–530 (2001)

    MathSciNet  MATH  Google Scholar 

  31. Jégou, P., Kanso, H., Terrioux, C.: Improving exact solution counting for decomposition methods. In: ICTAI, pp. 327–334 (2016). https://doi.org/10.1109/ICTAI.2016.0057

  32. Jerrum, M.R., Valiant, L.G., Vazirani, V.V.: Random generation of combinatorial structures from a uniform distribution. Theor. Comput. Sci. 43, 169–188 (1986)

    Article  MathSciNet  Google Scholar 

  33. Kelly, C., Sarkhel, S., Venugopal, D.: Adaptive Rao-Blackwellisation in Gibbs sampling for probabilistic graphical models. In: AISTATS, pp. 2907–2915 (2019)

    Google Scholar 

  34. Klebanov, V., Manthey, N., Muise, C.: SAT-based analysis and quantification of information flow in programs. In: QEST, pp. 177–192 (2013). https://doi.org/10.1007/978-3-642-40196-1_16

  35. Koster, A.M., Bodlaender, H.L., Van Hoesel, S.P.: Treewidth: computational experiments. Electron. Notes Disc. Math. 8, 54–57 (2001). https://doi.org/10.1016/S1571-0653(05)80078-2

    Article  MathSciNet  MATH  Google Scholar 

  36. Lagniez, J.M., Marquis, P.: An improved decision-DNNF compiler. In: IJCAI, pp. 667–673 (2017). https://doi.org/10.24963/ijcai.2017/93

  37. Lagniez, J.M., Marquis, P.: A recursive algorithm for projected model counting. AAAI 33, 1536–1543 (2019)

    Article  Google Scholar 

  38. Lee, N.Z., Wang, Y.S., Jiang, J.H.R.: Solving stochastic Boolean satisfiability under random-exist quantification. In: IJCAI, pp. 688–694 (2017)

    Google Scholar 

  39. Lloyd, J.W.: Foundations of Logic Programming. Springer, Cham (2012). https://doi.org/10.1007/978-3-642-96826-6

    Book  Google Scholar 

  40. Maua, D.D., de Campos, C.P., Cozman, F.G.: The complexity of MAP inference in Bayesian networks specified through logical languages. In: IJCAI, pp. 889–895 (2015)

    Google Scholar 

  41. McMahan, B.J., Pan, G., Porter, P., Vardi, M.Y.: Projection pushing revisited. In: EDBT, pp. 441–458 (2004). https://doi.org/10.1007/978-3-540-24741-8_26

  42. Möhle, S., Biere, A.: Dualizing projected model counting. In: ICTAI, pp. 702–709 (2018)

    Google Scholar 

  43. Murphy, K.P.: Machine Learning: A Probabilistic Perspective. MIT press, Cambridge (2012)

    MATH  Google Scholar 

  44. Oztok, U., Darwiche, A.: A top-down compiler for sentential decision diagrams. In: IJCAI, pp. 3141–3148 (2015). https://dl.acm.org/doi/10.5555/2832581.2832687

  45. Pan, G., Vardi, M.Y.: Symbolic techniques in satisfiability solving. J. Autom. Reas. 35(1–3), 25–50 (2005). https://doi.org/10.1007/s10817-005-9009-7

    Article  MathSciNet  MATH  Google Scholar 

  46. Park, J.D., Darwiche, A.: Complexity results and approximation strategies for MAP explanations. JAIR 21, 101–133 (2004)

    Article  MathSciNet  Google Scholar 

  47. Pearl, J.: Bayesian networks: a model cf self-activated memory for evidential reasoning. In: Proceedings of the 7th Conference of the Cognitive Science Society, University of California, Irvine, CA, USA, pp. 15–17 (1985)

    Google Scholar 

  48. Robertson, N., Seymour, P.D.: Graph minors. X. Obstructions to tree-decomposition. J. Comb. Theory B 52(2), 153–190 (1991). https://doi.org/10.1016/0095-8956(91)90061-N

  49. Samer, M., Szeider, S.: Algorithms for propositional model counting. J. Disc. Algor. 8(1), 50–64 (2010). https://doi.org/10.1007/978-3-540-75560-9_35

    Article  MathSciNet  MATH  Google Scholar 

  50. Sang, T., Bacchus, F., Beame, P., Kautz, H.A., Pitassi, T.: Combining component caching and clause learning for effective model counting. SAT 4, 20–28 (2004). http://www.satisfiability.org/SAT04/accepted/65.html

  51. Sharma, S., Roy, S., Soos, M., Meel, K.S.: GANAK: a scalable probabilistic exact model counter. In: IJCAI, pp. 1169–1176 (2019)

    Google Scholar 

  52. Soos, M., Meel, K.S.: BIRD: engineering an efficient CNF-XOR SAT solver and its applications to approximate model counting. AAAI 33, 1592–1599 (2019)

    Article  Google Scholar 

  53. Soos, M., Nohl, K., Castelluccia, C.: Extending SAT solvers to cryptographic problems. In: SAT, pp. 244–257 (2009)

    Google Scholar 

  54. Stearns, R.E., Hunt, H.B., III.: Exploiting structure in quantified formulas. J. Algor. 43(2), 220–263 (2002)

    Article  MathSciNet  Google Scholar 

  55. Stonebraker, M., Rowe, L.A.: The design of Postgres. ACM Sigmod Rec. 15(2), 340–355 (1986)

    Article  Google Scholar 

  56. Tabajara, L.M., Vardi, M.Y.: Factored Boolean functional synthesis. In: FMCAD, pp. 124–131 (2017). https://dl.acm.org/doi/10.5555/3168451.3168480

  57. Tamaki, H.: Positive-instance-driven dynamic programming for treewidth. J. Comb. Optim. 37(4), 1283–1311 (2019). https://doi.org/10.1007/s10878-018-0353-z

    Article  MathSciNet  MATH  Google Scholar 

  58. Tarjan, R.E., Yannakakis, M.: Simple linear-time algorithms to test chordality of graphs, test acyclicity of hypergraphs, and selectively reduce acyclic hypergraphs. SICOMP 13(3), 566–579 (1984). https://doi.org/10.1137/0213035

    Article  MathSciNet  MATH  Google Scholar 

  59. Uribe, T.E., Stickel, M.E.: Ordered binary decision diagrams and the Davis-Putnam procedure. In: CCL, pp. 34–49 (1994). https://doi.org/10.1007/BFb0016843

  60. Wetzler, N., Heule, M.J.H., Hunt, W.A.: DRAT-trim: efficient checking and trimming using expressive clausal proofs. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 422–429. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-09284-3_31

    Chapter  MATH  Google Scholar 

  61. Xu, L., Hutter, F., Hoos, H.H., Leyton-Brown, K.: SATzilla: portfolio-based algorithm selection for SAT. JAIR 32, 565–606 (2008)

    Article  Google Scholar 

  62. Xue, Y., Li, Z., Ermon, S., Gomes, C.P., Selman, B.: Solving marginal MAP problems with NP oracles and parity constraints. In: NIPS, pp. 1127–1135 (2016)

    Google Scholar 

  63. Zawadzki, E.P., Platzer, A., Gordon, G.J.: A generalization of SAT and #SAT for robust policy evaluation. In: IJCAI, pp. 2583–2589 (2013)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Rice University, Houston, TX, USA

    Jeffrey M. Dudek, Vu H. N. Phan & Moshe Y. Vardi

Authors
  1. Jeffrey M. Dudek
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Vu H. N. Phan
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Moshe Y. Vardi
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Vu H. N. Phan .

Editor information

Editors and Affiliations

  1. Laboratoire MIS, University of Picardie Jules Verne, Amiens, France

    Chu-Min Li

  2. IIIA-CSIC, Spanish National Research Council (CSIC), Bellaterra, Barcelona, Spain

    Felip Manyà

Rights and permissions

Reprints and permissions

Copyright information

© 2021 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Dudek, J.M., Phan, V.H.N., Vardi, M.Y. (2021). ProCount: Weighted Projected Model Counting with Graded Project-Join Trees. In: Li, CM., Manyà, F. (eds) Theory and Applications of Satisfiability Testing – SAT 2021. SAT 2021. Lecture Notes in Computer Science(), vol 12831. Springer, Cham. https://doi.org/10.1007/978-3-030-80223-3_11

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-80223-3_11

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-80222-6

  • Online ISBN: 978-3-030-80223-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation