# Projected Model Counting

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

## Key facts

- Cited by 6 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 28 Jul 2015.

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

- [Engineering an Exact Pseudo-Boolean Model Counter](https://mlsanity.com/paper/2312.12341/) (2023)
- [Solving Projected Model Counting by Utilizing Treewidth and its Limits](https://mlsanity.com/paper/2305.19212/) (2023)
- [Dynamic Blocked Clause Elimination for Projected Model Counting](https://mlsanity.com/paper/2408.06199/) (2024)
- [QuantifyML: How Good is my Machine Learning Model?](https://mlsanity.com/paper/2110.12588/) (2021)
- [Entailment vs. Verification for Partial-assignment Satisfiability and Enumeration](https://mlsanity.com/paper/2503.01536/) (2025)
- [Counting Answer Sets of Disjunctive Answer Set Programs](https://mlsanity.com/paper/2507.11655/) (2025)

## Abstract (arXiv)

Model counting is the task of computing the number of assignments to variables V that satisfy a given propositional theory F. Model counting is an essential tool in probabilistic reasoning. In this paper, we introduce the problem of model counting projected on a subset P of original variables that we call 'priority' variables. The task is to compute the number of assignments to P such that there exists an extension to 'non-priority' variables VP that satisfies F. Projected model counting arises when some parts of the model are irrelevant to the counts, in particular when we require additional variables to model the problem we are counting in SAT. We discuss three different approaches to projected model counting (two of which are novel), and compare their performance on different benchmark problems. To appear in 18th International Conference on Theory and Applications of Satisfiability Testing, September 24-27, 2015, Austin, Texas, USA