Source-linked AI summary
Distribution-Aware Sampling and Weighted Model Counting for SAT
Supratik Chakraborty, Daniel J. Fremont, Kuldeep S. Meel, Sanjit A. Seshia, Moshe Y. Vardi
TL;DR
Weighted model counting and distribution-aware sampling are hard problems for which prior guaranteed methods can depend on expensive MAP oracles and structured weight representations. This paper replaces those requirements with black-box assignment weights and an NP-oracle, obtaining practical approximate algorithms with strong guarantees under mild tilt assumptions and improved efficiency when weights are factored.
Problem
Weighted model counting and distribution-aware sampling need scalable approximate methods because exact solutions are hard, while prior guaranteed approaches may rely on expensive MAP oracles and structured weight representations.
Method
The paper adapts hashing-based counting and sampling algorithms to use a black-box weight function and an NP-oracle, with a white-box partitioning approach for large tilt.
Results
The algorithms provide strong theoretical guarantees, WeightMC stayed within tolerance in all reported experiments with L1 relative error 0.036, and WeightGen scaled to formulas with thousands of variables.
Takeaways & Limitations
Weighted counting and sampling can avoid MAP queries while retaining theoretical guarantees, and known factored weight functions can relax tilt-related efficiency constraints.
Takeaways & Limitations
The black-box algorithms become impractical when the weight-function tilt is large, while the white-box alternative requires a known polynomial-time computable weight function and specialized pseudo-Boolean solving support.
Abstract
from arXiv · showhide
Given a CNF formula and a weight for each assignment of values to variables, two natural problems are weighted model counting and distribution-aware sampling of satisfying assignments. Both problems have a wide variety of important applications. Due to the inherent complexity of the exact versions of the problems, interest has focused on solving them approximately. Prior work in this area scaled only to small problems in practice, or failed to provide strong theoretical guarantees, or employed a computationally-expensive maximum a posteriori probability (MAP) oracle that assumes prior knowledge of a factored representation of the weight distribution. We present a novel approach that works with a black-box oracle for weights of assignments and requires only an {\NP}-oracle (in practice, a SAT-solver) to solve both the counting and sampling problems. Our approach works under mild assumptions on the distribution of weights of satisfying assignments, provides strong theoretical guarantees, and scales to problems involving several thousand variables. We also show that the assumptions can be significantly relaxed while improving computational efficiency if a factored representation of the weights is known.
1 Introduction
Weighted model counting sums assignment weights satisfying constraints, while weighted sampling draws satisfying assignments proportionally to their weights. Because exact solutions are hard, the paper targets approximate methods that avoid MAP oracles and specialized weight representations.
- Weighted model counting computes the cumulative weight of satisfying assignments, while weighted sampling selects satisfying assignments with probability proportional to weight.Both problems support applications including machine learning, probabilistic reasoning, statistics, planning, combinatorics, and constrained random verification.
- Exact weighted model counting is #P-hard, and efficient weighted sampling would imply an FPRAS for #P-complete inference problems.These complexity results motivate approximate algorithms for both tasks.
- Prior work motivates methods that avoid computationally expensive MAP oracles and assumptions about a specific representation of the weight distribution.The paper frames this as the central design question for approximate counting and sampling.
- The proposed algorithms adapt hashing-based unweighted counting and sampling methods to weighted assignments using only a SAT solver and a black-box weight function.The approach works under mild assumptions on weight distributions and uses small tilt for practical performance.
2 Notation and Preliminaries
The paper formalizes CNF witnesses, supports, weight functions, approximation guarantees, and hash-function machinery for weighted counting and sampling. Its main algorithms treat weights as a black box, with tilt controlling efficiency and a white-box case enabling improvements.
- CNF notation and supports: A satisfying assignment, or witness, makes a CNF formula true; an independent support determines all remaining variables in every satisfying assignment.A formula may have multiple independent supports, and every superset of an independent support is also independent.
- Weight functions: The weight function maps each assignment σ to a value w(σ) in (0, 1], and the weight of a set is the sum of its assignment weights.The main algorithms do not assume that assignment weights factor over variable subsets.
- Weight functions: The tilt ρ = wmax/wmin measures the ratio between maximum and minimum satisfying-assignment weights, and the algorithms require an upper bound r on it.A tight bound improves algorithmic efficiency, while MAP is defined using wmax.
- Hashing machinery: The method uses k-wise independent hash functions, including Hxor(n, m, 3), to partition assignments into hashed cells.The Hxor family is generated by randomly choosing binary coefficients and is 3-independent.
- Approximation guarantees: An approximate weighted model counter returns v within multiplicative tolerance ε of w(RF) with confidence at least 1 − δ.The guarantee is expressed as w(RF)/(1 + ε) ≤ v ≤ (1 + ε)w(RF).
- Approximation guarantees: A weighted-uniform generator samples each witness y with probability w(y)/w(RF), while an almost generator may occasionally fail with probability at most δ.The exact weighted-uniform requirement is relaxed only by allowing bounded failure.
3 Related Work
Related work exposes a tension between strong guarantees and scalable performance in weighted counting and sampling. MAP-oracle-based methods provide guarantees but can be difficult to scale, motivating the paper’s SAT-oracle approach.
- Prior approaches: Existing approaches divide broadly into exact or strongly guaranteed methods that scale poorly, heuristic methods that scale well without strong guarantees, and MAP-based bridge methods.Exact methods enumerate solutions or compile formulas, while heuristic methods include variational and sampling-based techniques.
- MAP-based methods: MAP-based algorithms use random parity constraints and repeated MAP queries to obtain provable approximate counting and sampling.Their guarantees depend on solving MAP queries efficiently.
- MAP-based methods: MAP is substantially harder than CNF satisfiability, and random parity constraints often violate the structural properties that make graphical-model MAP solving efficient.This combination makes scalability challenging for prior weighted counting and sampling algorithms.
- MAP-based methods: Later MAP-based work reduced average parity-constraint size but retained the MAP-oracle paradigm and used experimental relaxations without guaranteed approximation factors.Obtaining the optimal MAP value was considered likely to take significantly longer and was not attempted.
- Connection to prior hashing methods: The paper’s algorithms are closely related to hashing-based unweighted model counting and near-uniform sampling algorithms that also use parity constraints.The contribution adapts this algorithmic lineage to weighted assignments.
4 Algorithm
The paper adapts hashing-based approximate counting and sampling to weighted assignments using a black-box weight function, SAT access, and a bounded tilt assumption. WeightMC estimates weighted model counts, while WeightGen produces approximately weighted-uniform satisfying assignments with explicit guarantees and polynomial oracle-relative runtime.
- Core approach: WeightMC and WeightGen adapt ApproxMC and UniWit by partitioning satisfying assignments into cells with roughly controlled weight.Both algorithms use random XOR constraints and weighted satisfiability procedures to operate on weighted rather than unweighted assignments.
- Core approach: MAP-oracle access is avoided because the maximum satisfying-assignment weight is estimated online without additional performance cost.This removes the need for a factored representation of the weight distribution in the core algorithms.
- Core approach: The algorithms require only a black-box weight function, an NP-oracle such as SAT, an independent support, and an upper bound on tilt.BoundedWeightSAT collects satisfying assignments until their scaled total weight exceeds a pivot and updates the observed weight bound.
- Guarantees: WeightMC returns an approximate weighted count within multiplicative tolerance ε with confidence at least 1 − δ, and runs in polynomial time relative to SAT.The runtime is polynomial in log2(1/δ), the tilt bound r, formula size, and 1/ε.
- Guarantees: WeightGen outputs satisfying assignments with probability bounded by (1 + ε)w(y) and succeeds with probability at least 0.62.Its runtime is polynomial in the tilt bound, formula size, and 1/ε relative to a SAT oracle.
5 Experimental Results
Experiments evaluate the implementations across practical and theoretical CNF benchmarks, comparing runtimes, count accuracy, and sampling behavior. The results show scalable performance on formulas with thousands of variables and empirical accuracy better than the theoretical guarantees.
- Experimental setup: The benchmark suite covers grid networks, plan recognition, bounded circuit checking, SMT-LIB instances, and parity-constrained circuits.Experiments used a high-performance cluster with per-invocation and overall timeouts for the main procedures.
- Runtime: WeightMC was significantly faster than SDD on all benchmarks with more than 1,000 variables, although SDD was generally superior on smaller problems.Table 1 reports runtimes for WeightMC, SDD, and WeightGen in seconds.
- Counting accuracy: All WeightMC counts lay within the tolerance of exact SDD counts, with an overall L1 norm of relative error of 0.036.The observed accuracy was substantially better than the theoretical guarantee stated in Theorem 3.
- Tilt sensitivity: WeightMC runtime increased roughly linearly with the tilt bound r, matching the theoretical dependence described in Theorem 2.Runtimes were normalized so that each benchmark took one time unit at r = 1, with averages over five runs.
- Sampling performance: WeightGen scales to formulas with thousands of variables when generating samples after the weighted model count has already been computed.The reported per-sample runtime averages over many runs and reuses the count computed earlier in the procedure.
- Sampling accuracy: For case110 with 16,384 solutions, WeightGen and the Ideal Sampler produced almost perfectly matching witness-frequency distributions.The comparison used N = 6 × 10^5 samples, and the close match also held for other benchmarks.
6 White-Box Weight Functions
The white-box approach partitions satisfying assignments into regions with bounded tilt, enabling weighted model counting with logarithmic dependence on the global tilt bound. It requires a known polynomial-time-computable weight function and introduces practical solver-efficiency constraints.
- Partitioning: PartitionedWeightMC divides satisfying assignments into regions whose tilt is at most 2.The regions are defined by successive weight intervals using bounds L and H.
- Algorithm: The algorithm sums WeightMC estimates over weight-constrained regions using the procedure shown in its pseudocode.Each region is added as a weight constraint to the CNF, counted, and accumulated into the final result.
- Guarantees: Theorem 6 gives polynomial runtime in |F|, 1/ε, log(1/δ), and log r = log(H/L) with access to an NP oracle.This replaces linear dependence on the tilt bound with logarithmic dependence.
- Guarantees: Reducing tilt dependence from linear to logarithmic can preserve polynomial runtime when literal-weight bounds on tilt are exponential in n.This is particularly relevant when assignment weights are products of literal weights.
- Implementation: Practical efficiency depends critically on implementing the pseudo-Boolean weight constraints, especially alongside XOR handling.The paper identifies specialized pseudo-Boolean solvers with efficient XOR support as a direction for future work.
7 Conclusion
The paper removes MAP-oracle dependence by providing black-box weighting algorithms using only an NP oracle, while also offering a white-box alternative with improved tilt dependence. The black-box approach has strong guarantees and is efficient for small tilt values; the alternative requires a factored weighting model and a pseudo-Boolean solver.
- Black-box approach: The black-box algorithms solve weighted counting and sampling using only assignment weights and an NP oracle, retaining strong theoretical guarantees.Their practical efficiency is stated for small tilt values.
- White-box approach: The alternative approach improves efficiency for tilt values but requires a white-box weighting model and access to a pseudo-Boolean solver.The paper notes that this approach remains to be empirically evaluated with suitable solvers.
- Evaluation: Experimental results demonstrate the effectiveness of the black-box approach in practice.
APPENDIX
The appendix establishes that WeightMC can use an independent support instead of the full variable support without changing the relevant probabilistic behavior. The proof reduces the independent-support case to the full-support case through Boolean representations and hash-function distributions.
- Independent-support reduction: An independent support S permits dependent variables to be represented by Boolean functions whose support is S.The appendix formalizes this representation through Lemma 1.
- Independent-support reduction: WeightMC depends directly on the support subset only when choosing hash functions and constructing the bounded-weight solution set.All subsequent algorithmic steps depend only on the resulting set Y.
- Notation: The appendix assumes X = {x1, …, xn}, S = {x1, …, xk}, and D = X \ S when analyzing the strict independent-support case.
- Independent-support reduction: Lemma 2 states that hashing over an independent support produces the same distribution for Y as hashing over the full support X.This allows the remainder of the proof to assume S = X.
- Hashing: The proof uses uniformly random XOR hash functions with independently selected coefficients and 3-wise independence.The hash-function properties support the distributional equivalence and later concentration analysis.
- Concentration: A concentration lemma bounds deviations of sums of r-wise independent variables confined to [0, 1].The stated condition requires 2 ≤ r ≤ 3 and a lower bound on the expectation μ.
A Analysis of WeightMC
The analysis proves that WeightMC achieves a multiplicative approximation with confidence at least 1 − δ and runs in polynomial time relative to a SAT oracle. Its guarantees follow from hashing-based concentration, bounded-core success, repetition, and median aggregation.
- Core analysis: WeightMC uses m = log2 W(RF) − log2(pivot+1) to index the hashing level analyzed by the core procedure.The exposition assumes m is an integer, with the paper stating that removing this assumption changes probabilities only by a constant factor.
- Core analysis: 3-wise hashing yields an approximate weighted cell estimate within a factor of 1 + ε with probability at least 1 − e^-3/2.The estimate is expressed as (1 + ε)^−1 · W(RF) ≤ 2^iW(RF,h,α) ≤ (1 + ε) · W(RF).
- Core analysis: When W(RF) > pivot, WeightMCCore returns a non-⊥ result at an appropriate iteration with probability at least 1 − e^-3/2.
- Amplification: Each WeightMCCore invocation returns a valid multiplicative estimate with probability greater than 0.6.The bound is (1 − e^-3/2)^2 > 0.6.
- Amplification: The failure probability is bounded by δ using t = ⌈35 log2(3/δ)⌉ repetitions and a binomial-tail argument.The analysis derives Pr[Err] ≤ 3·(0.98)^t ≤ δ.
- Amplification: Repeating the core procedure and taking the median yields a final estimate within the factor-1 + ε interval with probability at least 1 − δ.The theorem states the bound for ε ∈ (0, 1] and δ ∈ (0, 1].
- Runtime: With access to a SAT oracle, WeightMC runs in time polynomial in log2(1/δ), r, |F|, and 1/ε relative to that oracle.The runtime analysis counts bounded-weight SAT calls within the core procedure.
B Analysis of WeightGen
The analysis establishes that WeightGen produces approximately weighted-uniform witnesses with constant success probability, under ε > 1.71, and runs efficiently relative to a SAT oracle.
- Counter estimate: The approximate weighted counter supplies an estimate with tolerance 0.8 and confidence 0.8 for the total satisfying weight.This estimate is used to determine the scale parameter governing WeightGen’s hashing and sampling loop.
- Lower bound: The proof lower-bounds the probability that a fixed witness is selected by combining 3-wise independent hashing with bounded-weight sampling.For each hash bucket, the analysis derives a lower bound on the probability that the witness is output at the relevant level.
- Success probability: WeightGen succeeds, meaning it does not return ⊥, with probability at least 0.62.The success analysis uses the probability of selecting an appropriate hashing level and a lower bound of 1 − e^-3/2 on the relevant hashing event.
- Runtime: With access to a SAT oracle, WeightGen runs in time polynomial in r, |F|, and 1/ε relative to that oracle.The runtime is bounded by a constant number of BoundedWeightSAT calls and one WeightMC call.
C Analysis of Partitioned WeightMC
PartitionedWeightMC decomposes the formula into weight ranges, estimates each range with WeightMC, and combines the estimates into a global count with controlled confidence.
- Confidence: The combined estimate inherits the requested confidence through per-range estimates whose failure probabilities sum to at most δ.The proof uses (1 − δ′)^N ≥ 1 − δ for N partitioned ranges.
- Partitioning: PartitionedWeightMC partitions satisfying assignments into ranges G_m defined by H/2^m < w(X) ≤ H/2^(m−1).Each range is passed to WeightMC separately.
- Runtime: With an NP oracle, PartitionedWeightMC runs in time polynomial in |F|, 1/ε, log(1/δ), and log r = log(H/L).The algorithm makes O(log r) calls to WeightMC, with confidence allocation δ′ = δ/N.