Research map / Learning theory and algorithms / Combinatorial and search optimization

Towards Real-Time Approximate Counting

AAAI 2025 · Learning theory and algorithms › Combinatorial and search optimization · approach: SAT and model counting solvers

Read the paper Check your idea against 108,967 papers

AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.

placeholder

Problem

Approximate model counting with (ε, δ) guarantees needs hundreds of SAT calls per query, which is too slow for applications making thousands of counting queries under tight time limits.

Approach

Replace ApproxMC's threshold-based cell enumeration (thresh = Θ(1/ε²) SAT calls per cell check) with a galloping search over hash prefix lengths that checks only one SAT call per step, using a Markov and Cantelli-based analysis with constants α, β to correct the estimate for the large-ε regime (ε > 1), giving a short one-page proof.

Key results

ApproxMC7 solved 1,072 of 2,247 instances vs 801 for ApproxMC6 (271 more) with a 2.1x geometric-mean speedup at ε=13, δ=0.2.
On a 101-instance chosen ciphertext attack case study, ApproxMC7 achieved a 7x speedup over ApproxMC6.
Theoretically, ApproxMC7 uses 17 SAT calls vs 336 for ApproxMC on an instance with ε=13, and 6% of 698 estimates (vs guaranteed 20%) fell outside the (ε, δ) range.

Measured effects reported in the paper

What was changed	Where	Measured	Effect
use ApproxMC7 instead of ApproxMC6	approximate model counting · 2,247 instances	instances solved: 801 -> 1072	Helped
use ApproxMC7 instead of ApproxMC6	approximate model counting · 2,247 instances	PAR-2 score: 139 -> 115	Helped
use ApproxMC7 instead of ApproxMC6	approximate model counting · Instances solved by both counters	geometric mean speedup: 2.1×	Helped
use ApproxMC7 instead of ApproxMC6	chosen ciphertext attack counting · Chosen ciphertext attack instances (101 instances)	speedup: 7×	Helped
replace ApproxMC6 with ApproxMC7	ApproxMC7 · Sampled instances	SAT calls: 334 -> 15; 331 -> 16; 226 -> 10	Helped
use ApproxMC7 estimates	ApproxMC7 · 698 instances solved by Ganak and ApproxMC7	outlier rate: 6%	Helped
use ApproxMC7 instead of ApproxMC6	approximate model counting · All instances in Figure 4	runtime	Helped

Surprising findings

The observed geometric-mean error (1.59) is far below the guaranteed tolerance ε=13, indicating the bound is conservative in practice.
Neural network benchmarks showed significant slowdown when using the Arjun pre-processor, so it was not applied to them.

Limitations

Guarantees and advantages apply only to the large-tolerance regime (ε > 1); the paper does not target small ε.
Evaluation uses a 100-second time limit on a single core with 4GB memory, so benefits at other budgets are not characterized.
Only the 2-universal hashing setting is studied; projected counting is evaluated empirically but not analyzed.

Experimental setup

Datasets: 2,247 model counting benchmark instances (Yang, Pote, and Meel 2024) chosen ciphertext attack CNF instances (Beck, Zinkus, and Green 2020)

Benchmarks: 2,247 model counting instances from MCC 2020-2022, neural network verification, program synthesis, and related domains 101 chosen ciphertext attack CNF instances

Metrics: instances solved PAR-2 score geometric mean speedup number of SAT calls fraction of estimates outside the (ε, δ) range observed multiplicative error

Baselines: ApproxMC6

Builds on: ApproxMC ApproxMC6 LogSATSearch Stockmeyer's hashing-based counting

Closest papers by meaning

Auditable Algorithms for Approximate Model Counting (AAAI 2024 · similarity 0.91)
Towards Projected and Incremental Pseudo-Boolean Model Counting (AAAI 2025 · similarity 0.89)
Engineering an Exact Pseudo-Boolean Model Counter (AAAI 2024 · similarity 0.89)
An Approximate Skolem Function Counter (AAAI 2024 · similarity 0.86)
Solving Satisfiability Modulo Counting Exactly with Probabilistic Circuits (ICML 2025 · similarity 0.85)
Model Counting and Sampling via Semiring Extensions (AAAI 2024 · similarity 0.85)

Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.

Open scime draft