# Dynamic Blocked Clause Elimination for Projected Model Counting

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 3 of its 27 references that are in the map.
- First posted on arXiv 12 Aug 2024.

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

- [Projected Model Counting](https://mlsanity.com/paper/1507.07648/) (2015)
- [Blocked Clauses in First-Order Logic](https://mlsanity.com/paper/1702.00847/) (2017)
- [Solving Projected Model Counting by Utilizing Treewidth and its Limits](https://mlsanity.com/paper/2305.19212/) (2023)

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

- [Quantifying Sensitivity for Tree Ensembles: A symbolic and compositional approach](https://mlsanity.com/paper/2605.13830/) (2026)

## Abstract (arXiv)

In this paper, we explore the application of blocked clause elimination for projected model counting. This is the problem of determining the number of models ||exists X.Sigma|| of a propositional formula Sigma after eliminating a given set X of variables existentially. Although blocked clause elimination is a well-known technique for SAT solving, its direct application to model counting is challenging as in general it changes the number of models. However, we demonstrate, by focusing on projected variables during the blocked clause search, that blocked clause elimination can be leveraged while preserving the correct model count. To take advantage of blocked clause elimination in an efficient way during model counting, a novel data structure and associated algorithms are introduced. Our proposed approach is implemented in the model counter d4. Our experiments demonstrate the computational benefits of our new method of blocked clause elimination for projected model counting.