Constrained Sampling and Counting
summary
Describes an implementation that turns universal hashing plus XOR constraints into a practical sampler and counter: uses Crypt minisat to handle CNF+XOR, relies on 3‑wise universal hashing, and applies CDCL-era solver engineering. Claims almost-uniform sampling with tolerance epsilon=0.75 (experiment: 4 million samples on an instance with 16,000 solutions produced counts statistically indistinguishable from uniform). Scales to millions of variables for sampling and ~50,000 variables for approximate counting, outperforming prior tools by 2–3 orders on benchmarks.
AI-written summary · about
chapters (13)
- 0:00Introduction to AI logic
- 0:56History of SAT solving
- 4:48Modern SAT solver techniques
- 7:07Success and industrial impact
- 9:56Verification and test generation
- 14:15Uniform generation challenges
- 17:10New framework for sampling
- 20:35Universal hashing and cells
- 23:21Implementing hash functions
- 27:41Integrating SMT solvers
- 31:31Model counting applications
- 34:27Reflections on theory vs practice
- 38:37Audience Q&A
related talks
47mExploiting Combinatorial Structure in Constraint Programming: ...
37mFirst-Order Model Counting and Sampling
41mCounting Solutions to Random CNF Formulas
29mTesting Probability Distributions using Conditional Samples
29mPure Exploration Problems
01h 02mImportance Sampling in High Dimensions via Hashing
29mSampling Algorithms for Combinatorial Pure Exploration
43mPrivacy Amplification by Sampling in Practice