Source-linked AI summary
A Scalable Approximate Model Counter
Supratik Chakraborty, Kuldeep S. Meel, Moshe Y. Vardi
TL;DR
Exact #SAT counting is difficult, and prior approximate counting implementations did not provide scalable tolerance and confidence guarantees for CNF formulas. The paper presents ApproxMC, a hashing-based counter that uses repeated SAT-solver calls, and reports scalable, accurate results on large formulas. Its main scope boundary is that related almost-uniform-generation approaches lacked practical scalability, while one analysis also assumes an integer log2(pivot).
Problem
Prior approximate model counting was largely theoretical or limited to DNF, while CNF tools lacked both tolerance and confidence guarantees at practical scale.
Method
ApproxMC randomly hashes CNF models into small cells, uses bounded SAT calls to estimate cell sizes, and aggregates repeated estimates.
Results
ApproxMC stayed within the specified tolerance on all 95 benchmarks with exact Cachet counts, with L1 relative error 0.033 and approximately 4% practical error.
Takeaways & Limitations
ApproxMC provides a scalable CNF approximate counter for instances beyond exact counters while retaining explicit tolerance and confidence guarantees.
Takeaways & Limitations
The analysis assumes log2(pivot) is an integer, with removal of this restriction requiring constant-factor probability scaling; a theoretical analysis of leap-frogging is deferred.
Abstract
from arXiv · showhide
Propositional model counting} (#SAT), i.e., counting the number of satisfying assignments of a propositional formula, is a problem of significant theoretical and practical interest. Due to the inherent complexity of the problem, approximate model counting, which counts the number of satisfying assignments to within given tolerance and confidence level, was proposed as a practical alternative to exact model counting. Yet, approximate model counting has been studied essentially only theoretically. The only reported implementation of approximate model counting, due to Karp and Luby, worked only for DNF formulas. A few existing tools for CNF formulas are bounding model counters; they can handle realistic problem sizes, but fall short of providing counts within given tolerance and confidence, and, thus, are not approximate model counters. We present here a novel algorithm, as well as a reference implementation, that is the first scalable approximate model counter for CNF formulas. The algorithm works by issuing a polynomial number of calls to a SAT solver. Our tool, ApproxMC, scales to formulas with tens of thousands of variables. Careful experimental comparisons show that ApproxMC reports, with high confidence, bounds that are close to the exact count, and also succeeds in reporting bounds with small tolerance and high confidence in cases that are too large for computing exact model counts.
1 Introduction
#SAT counts satisfying assignments and is important in probabilistic reasoning and other applications, but its complexity motivates approximate counting. Before this work, scalable approximate counters were unavailable for CNF formulas despite the value of tolerance and confidence guarantees.
- #SAT counts the satisfying assignments of a propositional formula and is #P-complete.
- Approximate counts can suffice when exact counts are unnecessary or impractical because of #SAT's inherent complexity.
- (ε, δ) counters guarantee a count within [(1 + ε)^-1#F, (1 + ε)#F] with probability at least 1 −δ.ε is the tolerance, while 1 −δ is the confidence.
- Bounding tolerance and confidence is valuable for applications such as probabilistic inference, but prior implementations did not provide scalable CNF guarantees.Karp and Luby's implemented approximate counter applied to DNF formulas, while existing CNF tools were bounding counters.
- ApproxMC is presented as the first scalable (ε, δ) counter for CNF formulas, using randomized polynomial-time SAT-oracle calls and experiments on formulas with tens of thousands of variables.
2 Notation and Preliminaries
The preliminaries formalize model counting through NP relations and introduce the hash-function framework used to partition satisfying assignments into cells. These definitions establish #SAT as counting the models associated with a CNF relation.
- An NP relation is polynomial-time decidable with polynomially bounded witnesses, and its models for x form the set R_x.
- The counting problem for a relation asks for |R_x|; when the relation connects CNF formulas to satisfying assignments, it is #SAT.
- r-wise independent hash functions map {0, 1}^n to {0, 1}^m and provide the randomized partitioning framework used in the paper.
- For a fixed hash function, the sets R_x,h,α partition R_x into cells, each having expected size |R_x|/2^m.
- The specific Hxor(n, m, 3) family randomly selects bits and combines them with xor to obtain hash functions.
3 Related Work
Prior work connected approximate counting with almost-uniform generation but lacked a scalable generator suitable for CNF formulas. ApproxMC instead uses hashing insights from UniWit directly, without treating the generator as a black box.
- Approximate counting and almost-uniform generation are polynomially inter-reducible for self-reducible NP relations such as SAT.
- The JVV approach requires an almost-uniform generator whose model-generation probabilities differ by at most a factor in O(ε^2).
- Existing generators either provide the required probability guarantee but scale poorly, or scale well without providing it for CNF formulas with thousands of variables.
- The paper designs a scalable (ε, δ) counter using UniWit's insights without using the near-uniform generator as a black box.
- The shared hashing strategy uses low-independence linear functions and reduces target cell sizes to a constant.
4 Algorithm
ApproxMC repeatedly hashes a formula's model space into cells, searches for a nonempty cell below an ε-dependent threshold, scales that cell's size, and returns the median of repeated estimates. SAT-based bounded counting supplies the cell checks, while leap-frogging improves repeated invocations in practice.
- ApproxMC uses 3-wise independent Hxor hashing to partition models into cells and increases the number of cells until a randomly selected cell is nonempty and small.
- ApproxMC sets pivot from ε, sets t from δ, invokes ApproxMCCore t times, and returns the median of non-⊥ estimates.
- ApproxMCCore returns an ε-approximate estimate by scaling the size of a selected small cell by the number of generated cells, or reports ⊥ when no suitable cell is found.
- BoundedSAT checks conjunctions of CNF clauses and xor constraints, with CryptoMiniSAT used as the back-end SAT solver.
- Leap-frogging reuses earlier stopping information across ApproxMCCore invocations and produces significant practical time savings, although its theoretical analysis is deferred.
5 Analysis of ApproxMC
The analysis establishes that ApproxMC’s core and repeated procedures return multiplicative approximations with high confidence, while requiring only polynomial time relative to a SAT oracle.
- Core guarantees: ApproxMCCore returns a non-⊥ result at an appropriate iteration with probability at least 1 −e−3/2 when |RF | > pivot.The proof uses hash-induced 3-wise independent indicator variables and concentration bounds.
- Core guarantees: An ApproxMCCore invocation returning c satisfies (1 + ε)−1 · |RF | ≤c ≤(1 + ε) · |RF | with the analyzed success probability.The argument combines the suitable-iteration event with the bound on the hashed cell count.
- Confidence amplification: ApproxMC raises confidence to at least 1 −δ by invoking ApproxMCCore O(log2(1/δ)) times and taking the median of non-⊥ counts.The error analysis bounds the probability that too many returned values are ⊥ or outside the target interval.
- Confidence amplification: ApproxMC returns a count c satisfying (1 + ε)−1 · |RF | ≤c ≤(1 + ε) · |RF | with probability at least 1 −δ.This is the paper’s overall correctness guarantee for the specified tolerance and confidence parameters.
- Complexity: Given a SAT oracle, ApproxMC runs in time polynomial in log2(1/δ), |F| and 1/ε relative to that oracle.ApproxMCCore makes O(|F|) BoundedSAT calls, each reducible to at most pivot + 1 SAT-oracle calls, with pivot + 1 in O(1/ε2).
6 Experimental Methodology
The evaluation uses diverse practical and theoretical model-counting benchmarks, controlled computing conditions, and comparisons with exact and bounding counters.
- Benchmarks: The benchmark suite spans grid networks, plan recognition, DQMR networks, Langford sequences, circuit synthesis, random k-CNF and logistics problems.The experiments were designed to cover practical domains as well as theoretically interesting instances.
- Experimental setup: Experiments ran on single cluster nodes with two quad-core Intel Xeon processors and 4GB of memory, using 2500-second BoundedSAT and 20-hour ApproxMC timeouts.Multiple experiments could run in parallel across the high-performance cluster.
- Implementation: The implementation used leap-frogging to estimate initial loop values and a precomputed table to tighten the iteration count t.The tighter iteration count was based on requiring η(t, t/2, 0.4) ≤δ.
- Exact-counter comparison: ApproxMC was compared with the exact counter Cachet using ε = 0.75 and δ = 0.1 on benchmarks where Cachet did not time out.Approximation quality was checked against a factor of 1.75 and also measured using relative L1 error.
- Bounding-counter comparison: Because bounding counters provide no tolerance guarantees, comparisons with them focused on the sizes of their output intervals.The study used MBound, Hybrid-MBound, SampleCount, BPCount and MiniCount, with fixed confidence settings and 20-hour limits.
7 Results
ApproxMC remained useful on increasingly difficult CNF benchmarks, delivering specified-guarantee bounds beyond the reach of exact counters and producing tighter approximations than existing bounding counters.
- Performance comparison: ApproxMC continued returning bounds with specified tolerance and confidence after Cachet timed out on increasingly difficult and larger problems, though it also timed out on the very largest instances.The benchmarks were ordered by increasing ApproxMC running time.
- Practical scope: The experiments identify a large class of practical problems beyond exact counters where ApproxMC still obtains (ε, δ)-style guarantees in reasonable time.The authors recommend trying Cachet first, then ApproxMC, and finally weaker-guarantee bounding counters if ApproxMC also times out.
- Count quality: ApproxMC stayed within the specified tolerance for all 95 benchmarks on which Cachet reported exact counts.Figure 2 shows a 37-benchmark subset; the x-axis orders benchmarks by increasing model count.
- Count quality: ApproxMC achieved approximately 4% practical error, compared with a 75% theoretical guarantee for ε = 0.75.The reported L1 norm of relative error across the 95 exact-count benchmarks was 0.033.
- Comparison with bounding counters: ApproxMC produced consistently smaller intervals than existing bounding counters, improving MiniCount upper bounds significantly and SampleCount and MBound lower bounds to a lesser extent.Smaller intervals with comparable confidence represent better approximations.
8 Conclusion and Future Work
ApproxMC is presented as the first practical (ε, δ) approximate counter for CNF formulas at the scale of tens of thousands of variables, with smaller practical error than its theoretical guarantee. The authors identify extending the approach to probabilistic inference and SMT model counting as future work.
- Conclusion: ApproxMC is presented as the first (ε, δ) approximate counter for CNF formulas that scales in practice to tens of thousands of variables.The conclusion states that it provides small theoretical tolerance and much smaller practical error with high confidence.
- Future work: The authors propose extending the paper's ideas to probabilistic inference and counting models of SMT constraints.These extensions are identified as directions for future research.