# DPMC: Weighted Model Counting by Dynamic Programming on Project-Join Trees

arXiv: https://arxiv.org/abs/2008.08748 · HTML: https://mlsanity.com/paper/2008.08748/

## Key facts

- Cited by 6 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 20 Aug 2020.

## Built on by (most cited first, 6 of 6)

- [Treewidth-aware Reductions of Normal ASP to SAT -- Is Normal ASP Harder than SAT after All?](https://mlsanity.com/paper/2210.03553/) (2022)
- [DPMS: An ADD-Based Symbolic Approach for Generalized MaxSAT Solving](https://mlsanity.com/paper/2205.03747/) (2022)
- [Engineering an Exact Pseudo-Boolean Model Counter](https://mlsanity.com/paper/2312.12341/) (2023)
- [DPO: Dynamic-Programming Optimization on Hybrid Constraints](https://mlsanity.com/paper/2205.08632/) (2022)
- [DPER: Dynamic Programming for Exist-Random Stochastic SAT](https://mlsanity.com/paper/2205.09826/) (2022)
- [Attn-JGNN: Attention Enhanced Join-Graph Neural Networks](https://mlsanity.com/paper/2510.15583/) (2025)

## Abstract (arXiv)

We propose a unifying dynamic-programming framework to compute exact literal-weighted model counts of formulas in conjunctive normal form. At the center of our framework are project-join trees, which specify efficient project-join orders to apply additive projections (variable eliminations) and joins (clause multiplications). In this framework, model counting is performed in two phases. First, the planning phase constructs a project-join tree from a formula. Second, the execution phase computes the model count of the formula, employing dynamic programming as guided by the project-join tree. We empirically evaluate various methods for the planning phase and compare constraint-satisfaction heuristics with tree-decomposition tools. We also investigate the performance of different data structures for the execution phase and compare algebraic decision diagrams with tensors. We show that our dynamic-programming model-counting framework DPMC is competitive with the state-of-the-art exact weighted model counters cachet, c2d, d4, and miniC2D.