Approximate Model Counting

Concept

Approximate model counting is the problem of estimating the number of satisfying assignments of a Boolean formula, often a CNF formula, with formal accuracy and confidence guarantees. It is motivated by the #P-completeness of exact model counting and is commonly implemented with hashing-based methods that use random XOR constraints and SAT solving. ApproxMC is described as the state-of-the-art CNF approximate counter with PAC-style guarantees, and recent work has introduced a formal certification framework for its outputs. Approximate model counting is also closely connected to almost-uniform SAT witness generation and is used by tools such as UniGen to set hashing parameters.

First seen 7/17/2026

Last seen 9/7/2026

Evidence 10 chunks

Wiki v2

WIKI

Approximate Model Counting

Approximate model counting is the task of approximating the number of satisfying assignments (models) of a Boolean formula. In the CNF setting, approximate counters typically aim to return estimates with probably approximately correct (PAC)-style guarantees on accuracy and confidence. The problem is important because exact model counting is #P-complete, and it has applications including Quantitative Information Flow.

Core approach: hashing with XOR constraints

READ FULL ARTICLE →

NEIGHBORHOOD

6 nodes · 7 edges

graph · Approximate Model Counting · depth=1

RELATIONSHIPS

6 connections

UniGen ← uses 100% 4e

UniGen invokes an approximate model counter to estimate |RF| for choosing the hash parameter m.

PAWS ← uses 93% 2e

PAWS uses an approximate model counter to estimate |RF| for choosing hash parameter m.

ApproxMC ← uses 95% 2e

ApproxMC is a scalable approximate model counter.

ApproxMC ← implements 100% 1e

ApproxMC is an approximate model counter used within UniGen.

UniGen ← uses 95% 1e

UniGen exploits the connection between approximate counting and almost-uniform sampling.

On Parallel Scalable Uniform SAT Witness Generation ← uses 85% 1e

The paper addresses approximate model counting as a related application of SAT witness sampling.

LINKED ENTITIES

3 links

UniGen USES Extracted graph relationship

On Parallel Scalable Uniform SAT Witness Generation USES Extracted graph relationship

ApproxMC USES Extracted graph relationship

CITATIONS

8 sources

8 citations — click to expand

[1] Approximate model counting is the task of approximating the number of solutions to a Boolean formula; exact model counting is #P-complete; approximate counters provide formal confidence and accuracy guarantees; applications include Quantitative Information Flow. Approximate Model Counting, Sparse XOR Constraints and Minimum Distance

[2] A common approximate-counting approach uses random XOR constraints together with SAT solving, and sparse XOR constraints relate correctness bounds to the minimum Hamming distance between models. Approximate Model Counting, Sparse XOR Constraints and Minimum Distance

[3] ApproxMC is the state-of-the-art approximate model counter for CNF formulas and provides scalable PAC-style guarantees. Formally Certified Approximate Model Counting

[4] ApproxMC's guarantees depend on both the theoretical analysis of its randomized algorithm and the correctness of its implementation, especially its interaction with an incremental CNF-XOR SAT solver. Formally Certified Approximate Model Counting

[5] A formal certification framework combines a once-off Isabelle/HOL proof of the PAC guarantee with per-run certificate checking of ApproxMC's external CNF-XOR solver calls, and reports 84.7% full certification under matched resource limits. Formally Certified Approximate Model Counting

[6] Almost-uniform generation is polynomially inter-reducible with approximate model counting. On Parallel Scalable Uniform SAT Witness Generation

[7] UniGen provides stronger guarantees of uniformity by exploiting a deep connection between approximate counting and almost-uniform sampling. On Parallel Scalable Uniform SAT Witness Generation

[8] In UniGen, an approximate model counter is used to estimate |R_F| within a specified tolerance and confidence, and that estimate is used to choose a small range of candidate values of the hashing parameter m. Balancing Scalability and Uniformity in SAT Witness Generator