SAT Counting and Sampling -- From Theory to Practice
summary
Moshe Vardi reviews methods for counting and sampling satisfying assignments of Boolean formulas, focusing on practical implementations of theoretical algorithms. The talk covers approximate counting techniques and sampling methods tied to SAT, likely discussing algorithmic approaches that bridge complexity-theoretic results and usable tools for SAT counting and sampling.
AI-written summary · about
chapters (20)
- 0:00Start
- 0:51Boolean Satisfiability
- 2:44Algorithmic Boolean Reasoning: Early History
- 8:23Applications of SAT Solving in SW Engineering
- 10:53Dynamic Verification
- 12:04Motivating Example: HW FP Divider
- 12:26Test Generation
- 14:16Random Solutions
- 15:02Constrained Sampling Applications
- 15:58Constrained Sampling - Prior Approaches. I
- 18:56Almost Uniform Generation of Solutions
- 20:01Uniformity vs Almost Uniformity
- 21:44The Base Idea
- 23:23Strong Universality
- 25:35XOR-Based 3. Universal Hashing
- 26:55SMT: Satisfiability Modulo Theory
- 31:48Constrained Counting
- 32:16Approximate Counting
- 34:19ApproxMC Performance: Accuracy
- 36:25Reflection on P vs. NP