# Constrained Sampling and Counting: Universal Hashing Meets SAT Solving

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

## Key facts

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

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

- [Softened Symbol Grounding for Neuro-symbolic Systems](https://mlsanity.com/paper/2403.00323/) (2024)
- [Rounding Meets Approximate Model Counting](https://mlsanity.com/paper/2305.09247/) (2023)
- [Projected Model Counting: Beyond Independent Support](https://mlsanity.com/paper/2110.09171/) (2021)
- [Exploiting complex pattern features for interactive pattern mining](https://mlsanity.com/paper/2204.04242/) (2022)
- [SMT(LIA) Sampling with High Diversity](https://mlsanity.com/paper/2503.04782/) (2025)
- [Systematic Parameter Decision in Approximate Model Counting](https://mlsanity.com/paper/2504.05874/) (2025)

## Abstract (arXiv)

Constrained sampling and counting are two fundamental problems in artificial intelligence with a diverse range of applications, spanning probabilistic reasoning and planning to constrained-random verification. While the theory of these problems was thoroughly investigated in the 1980s, prior work either did not scale to industrial size instances or gave up correctness guarantees to achieve scalability. Recently, we proposed a novel approach that combines universal hashing and SAT solving and scales to formulas with hundreds of thousands of variables without giving up correctness guarantees. This paper provides an overview of the key ingredients of the approach and discusses challenges that need to be overcome to handle larger real-world instances.