# Projected Model Counting: Beyond Independent Support

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

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 12 of its 41 references that are in the map.
- First posted on arXiv 18 Oct 2021.

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

- [Quantitative Verification of Neural Networks And its Security Applications](https://mlsanity.com/paper/1906.10395/) (2019)
- [The Model Counting Competition 2020](https://mlsanity.com/paper/2012.01323/) (2020)
- [A Scalable Approximate Model Counter](https://mlsanity.com/paper/1306.5726/) (2013)
- [Taming the Curse of Dimensionality: Discrete Integration by Hashing and Optimization](https://mlsanity.com/paper/1302.6677/) (2013)
- [Manthan: A Data Driven Approach for Boolean Function Synthesis](https://mlsanity.com/paper/2005.06922/) (2020)
- [A Scalable and Nearly Uniform Generator of SAT Witnesses](https://mlsanity.com/paper/1304.1584/) (2013)
- [Partition Function Estimation: A Quantitative Study](https://mlsanity.com/paper/2105.11132/) (2021)
- [Sparse Hashing for Scalable Approximate Model Counting: Theory and Practice](https://mlsanity.com/paper/2004.14692/) (2020)
- [Constrained Sampling and Counting: Universal Hashing Meets SAT Solving](https://mlsanity.com/paper/1512.06633/) (2015)
- [Balancing Scalability and Uniformity in SAT Witness Generator](https://mlsanity.com/paper/1403.6246/) (2014)
- [Probabilistic Model Counting with Short XORs](https://mlsanity.com/paper/1707.09467/) (2017)
- [Towards Parallel Boolean Functional Synthesis](https://mlsanity.com/paper/1703.01440/) (2017)

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

- [Rounding Meets Approximate Model Counting](https://mlsanity.com/paper/2305.09247/) (2023)
- [Systematic Parameter Decision in Approximate Model Counting](https://mlsanity.com/paper/2504.05874/) (2025)

## Abstract (arXiv)

The past decade has witnessed a surge of interest in practical techniques for projected model counting. Despite significant advancements, however, performance scaling remains the Achilles' heel of this field. A key idea used in modern counters is to count models projected on an independent support that is often a small subset of the projection set, i.e. original set of variables on which we wanted to project. While this idea has been effective in scaling performance, the question of whether it can benefit to count models projected on variables beyond the projection set, has not been explored. In this paper, we study this question and show that contrary to intuition, it can be beneficial to project on variables beyond the projection set. In applications such as verification of binarized neural networks, quantification of information flow, reliability of power grids etc., a good upper bound of the projected model count often suffices. We show that in several such cases, we can identify a set of variables, called upper bound support (UBS), that is not necessarily a subset of the projection set, and yet counting models projected on UBS guarantees an upper bound of the true projected model count. Theoretically, a UBS can be exponentially smaller than the smallest independent support. Our experiments show that even otherwise, UBS-based projected counting can be more efficient than independent support-based projected counting, while yielding bounds of very high quality. Based on extensive experiments, we find that UBS-based projected counting can solve many problem instances that are beyond the reach of a state-of-the-art independent support-based projected model counter.