# Sparse Hashing for Scalable Approximate Model Counting: Theory and Practice

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

## Key facts

- Cited by 7 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 30 Apr 2020.

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

- [Arjun: An Efficient Independent Support Computation Technique and its Applications to Counting and Sampling](https://mlsanity.com/paper/2110.09026/) (2021)
- [Partition Function Estimation: A Quantitative Study](https://mlsanity.com/paper/2105.11132/) (2021)
- [Rounding Meets Approximate Model Counting](https://mlsanity.com/paper/2305.09247/) (2023)
- [Locally-Minimal Probabilistic Explanations](https://mlsanity.com/paper/2312.11831/) (2023)
- [Projected Model Counting: Beyond Independent Support](https://mlsanity.com/paper/2110.09171/) (2021)
- [Formally Certified Approximate Model Counting](https://mlsanity.com/paper/2406.11414/) (2024)
- [Systematic Parameter Decision in Approximate Model Counting](https://mlsanity.com/paper/2504.05874/) (2025)

## Abstract (arXiv)

Given a CNF formula F on n variables, the problem of model counting or #SAT is to compute the number of satisfying assignments of F . Model counting is a fundamental but hard problem in computer science with varied applications. Recent years have witnessed a surge of effort towards developing efficient algorithmic techniques that combine the classical 2-universal hashing with the remarkable progress in SAT solving over the past decade. These techniques augment the CNF formula F with random XOR constraints and invoke an NP oracle repeatedly on the resultant CNF-XOR formulas. In practice, calls to the NP oracle calls are replaced a SAT solver whose runtime performance is adversely affected by size of XOR constraints. The standard construction of 2-universal hash functions chooses every variable with probability p = 1/2 leading to XOR constraints of size n/2 in expectation. Consequently, the challenge is to design sparse hash functions where variables can be chosen with smaller probability and lead to smaller sized XOR constraints. In this paper, we address this challenge from theoretical and practical perspectives. First, we formalize a relaxation of universal hashing, called concentrated hashing and establish a novel and beautiful connection between concentration measures of these hash functions and isoperimetric inequalities on boolean hypercubes. This allows us to obtain (log m) tight bounds on variance and dispersion index and show that p = O( log(m)/m ) suffices for design of sparse hash functions from {0, 1}^n to {0, 1}^m. We then use sparse hash functions belonging to this concentrated hash family to develop new approximate counting algorithms. A comprehensive experimental evaluation of our algorithm on 1893 benchmarks demonstrates that usage of sparse hash functions can lead to significant speedups.