# Fast Converging Anytime Model Counting

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

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 6 of its 50 references that are in the map.
- First posted on arXiv 19 Dec 2022.

## Builds on (most cited first, 6 of 6)

- [Quantitative Verification of Neural Networks And its Security Applications](https://mlsanity.com/paper/1906.10395/) (2019)
- [A Scalable Approximate Model Counter](https://mlsanity.com/paper/1306.5726/) (2013)
- [Arjun: An Efficient Independent Support Computation Technique and its Applications to Counting and Sampling](https://mlsanity.com/paper/2110.09026/) (2021)
- [Approximate Knowledge Compilation by Online Collapsed Importance Sampling](https://mlsanity.com/paper/1805.12565/) (2018)
- [AND/OR Multi-Valued Decision Diagrams (AOMDDs) for Graphical Models](https://mlsanity.com/paper/1401.3448/) (2014)
- [CCDD: A Tractable Representation for Model Counting and Uniform Sampling](https://mlsanity.com/paper/2202.10025/) (2022)

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

- [PBCounter: Weighted Model Counting on Pseudo-Boolean Formulas](https://mlsanity.com/paper/2312.15877/) (2023)
- [Attn-JGNN: Attention Enhanced Join-Graph Neural Networks](https://mlsanity.com/paper/2510.15583/) (2025)

## Abstract (arXiv)

Model counting is a fundamental problem which has been influential in many applications, from artificial intelligence to formal verification. Due to the intrinsic hardness of model counting, approximate techniques have been developed to solve real-world instances of model counting. This paper designs a new anytime approach called PartialKC for approximate model counting. The idea is a form of partial knowledge compilation to provide an unbiased estimate of the model count which can converge to the exact count. Our empirical analysis demonstrates that PartialKC achieves significant scalability and accuracy over prior state-of-the-art approximate counters, including satss and STS. Interestingly, the empirical results show that PartialKC reaches convergence for many instances and therefore provides exact model counting performance comparable to state-of-the-art exact counters.