Research map / Learning theory and algorithms / Combinatorial and search optimization
An Approximate Skolem Function Counter
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.
Proposes SkolemFC, the first approximate counter for Skolem functions of a Boolean specification, reducing the log-count to linearly many approximate model counting calls and almost-uniform sampling calls.
Problem
Counting Skolem functions (functions from inputs to outputs satisfying a Boolean specification F(X,Y)) is #P-hard and unlikely to admit an FPRAS, and finding even one Skolem function is hard; existing model counting techniques do not scale to it.
Approach
Expresses the Skolem function count as a product over input assignments of per-input solution counts, and estimates the log-count by stopping-rule sampling of inputs with at least two outputs (drawn via a self-composed formula G = F(X,Y) ∧ F(X,Y') ∧ Y≠Y') and approximate model counting, without enumerating any Skolem function.
Key results
- SkolemFC solved 375 of 609 instances versus 8 for the exact-counting baseline BASE and 0 for QC.
- On 158 SyGuS instances compared against QC, average relative error was 0.005 (max 0.035), far below the theoretical tolerance of 0.8.
- The algorithm makes O~(m/eps^2 ln(2/delta)) SAT oracle calls, where m is the number of output variables.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Use SKLMC instead of the exact-counting Baseline | Skolem function counting · Efficiency benchmarks (609 instances) | instances solved: 8 -> 375 | Helped |
| Use SKLMC instead of QC | Skolem function counting · Efficiency benchmarks (609 instances) | instances solved: none -> 375 | Helped |
| Use SKLMC estimates compared with QC counts | SKLMC · Correctness benchmarks (158 SyGuS instances) | average relative error: 0.8 -> 0.005 | Helped |
Surprising findings
- Observed error (average 0.5%) is far below the theoretical guarantee, which is loose at epsilon=0.8.
- BASE required up to about 10^230 counter calls on some instances, showing enumeration-based approaches are infeasible.
Limitations
- Guarantee relies on approximate counter and sampler oracles, so practical accuracy depends on their behavior.
- Accuracy validated against QC only on 158 small SyGuS instances with m<=8 due to lack of other ground truth.
- Targets CNF specifications; generalization to richer function classes such as SMT uninterpreted functions is left open.
Experimental setup
Datasets: QBF Evaluation 2017 Prenex-2QBF QBF Evaluation 2018 Prenex-2QBF Boolean function synthesis benchmarks (disjunctive, arithmetic, factorization) SyGuS instances
Benchmarks: 609 Boolean function synthesis instances 158 SyGuS instances for accuracy
Metrics: number of instances solved runtime counter calls relative error of log count
Baselines: BASE (exact model counting with AllSAT enumeration) QC (QBF level-2 solution counter) Manthan2 Manthan
Builds on: Stopping Rule algorithm ApproxMC UniGen Manthan
Closest papers by meaning
- Engineering an Exact Pseudo-Boolean Model Counter (AAAI 2024 · similarity 0.88)
- Approximate Probabilistic Inference via Word-Level Counting (AAAI 2016 · similarity 0.88)
- Towards Projected and Incremental Pseudo-Boolean Model Counting (AAAI 2025 · similarity 0.86)
- Towards Real-Time Approximate Counting (AAAI 2025 · similarity 0.86)
- Model Counting and Sampling via Semiring Extensions (AAAI 2024 · similarity 0.84)
- Auditable Algorithms for Approximate Model Counting (AAAI 2024 · similarity 0.84)
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.