Research map / Learning theory and algorithms / Combinatorial and search optimization
Auditable Algorithms for Approximate Model Counting
Read the paperCheck 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.
Designs auditable deterministic approximate model counting algorithms whose certificates shrink from O(n^2 log^2 n) to O(n log n) variables by trading up to Sigma_3^P oracle calls in the counter.
Problem
Approximate model counting via deterministic algorithms needs certificates that a limited verifier can audit; existing Stockmeyer-style certificates require large audit queries (many variables), which hinders practical auditing.
Approach
Audit the Stockmeyer algorithm via a single Sigma_2^P query over n^2 log^2 n variables, then design counters using Sigma_3^P oracles (cells with bounded lower and upper solution counts, and a "holes" formula) so that certificates only need certifying True answers, reducing audit size to n log n variables.
Key results
- Stockmeyer's algorithm can be audited with one Sigma_2^P query over O(n^2 log^2 n) variables.
- EqualCellsCounter achieves audit complexity O(n^2) using O(n) Sigma_3^P oracle calls.
- The final algorithm (CountAuditor-based) achieves audit complexity O(n log n) with O(n log n) Sigma_3^P calls and a 16-factor approximation.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Replace the Stockmeyer counting-and-audit approach with EqualCellsCounter using equal-sized hash cells and a Σ3^P oracle | Deterministic approximate model counting · DAC (n-variable CNF) | audit complexity (variables): O(n^2 \log^2 n) -> O(n^2) | Helped |
| Use the holes certificate and copied formulas | Deterministic approximate model counting · DAC (n-variable CNF) | audit complexity (variables): O(n^2) -> O(n \log n) | Helped |
| Use a Σ3^P oracle with EqualCellsCounter rather than Stockmeyer's Σ2^P counting oracle | Deterministic approximate model counting · DAC (n-variable CNF) | oracle calls: O(n \log n) -> O(n) | Helped |
Surprising findings
- The count estimate can be computed from c_high alone, but certification needs c_low, and certifying c_high being minimal is unnecessary once c_high - c_low <= 7 is checked.
Limitations
- Results are purely theoretical; no implementation or empirical evaluation of audit cost.
- Counting algorithms become less efficient, requiring a Sigma_3^P oracle instead of Sigma_2^P.
Experimental setup
Metrics: audit complexity (number of variables in the auditing query) approximation factor number of oracle calls
Baselines: Stockmeyer's algorithm
Builds on: Stockmeyer's approximate counting algorithm Sipser hashing k-wise independent hash families
Closest papers by meaning
- Towards Real-Time Approximate Counting (AAAI 2025 · similarity 0.91)
- Engineering an Exact Pseudo-Boolean Model Counter (AAAI 2024 · similarity 0.87)
- Towards Projected and Incremental Pseudo-Boolean Model Counting (AAAI 2025 · similarity 0.87)
- An Approximate Skolem Function Counter (AAAI 2024 · similarity 0.84)
- Model Counting and Sampling via Semiring Extensions (AAAI 2024 · similarity 0.83)
- Solving Satisfiability Modulo Counting Exactly with Probabilistic Circuits (ICML 2025 · similarity 0.83)
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.