Designing Samplers is Easy: The Boon of Testers
summary
A scalable grey-box tester called Barbarik tester uses conditional sampling to distinguish samplers without needing samples proportional to the solution count and rejects QuickSampler on 50/50 benchmarks while accepting UniGen; testing previously failed with only 1,000 naive samples. Using CryptoMiniSat options yields CMSGen (CryptoMiniSatGen), which passes Barbarik on held-out instances, runs faster than other heuristic samplers, and achieves 100% 2-wise coverage on 110 benchmarks after ~1,000 samples, though no proof explains why.
AI-written summary · about
chapters (14)
- 0:00Introduction
- 0:42Uniform sampling in Boolean formulas
- 3:17Sampler uniformity testing
- 6:51Conditional sampling model
- 10:29Theory versus sampler conditioning
- 13:47Testing samplers with Barbarik
- 15:13Designing better samplers
- 17:26Tuning CMSGen with Barbarik
- 18:30CMSGen performance
- 20:20Combinatorial testing application
- 21:43Functional synthesis application
- 23:17Observations and open questions
- 25:12Theoretical implications
- 26:20Q&A
related talks
22mWriting tests when the code is already there: Golden Master technique
21mBounded-Exhaustive Subspace Diversification for SMT Solver Testing
17mCode-Specify-Test-Debug-Prove: Flexibly Integrating Separation Logic Specification into(…)
16mSEMSAN: a Configurable Sanitizer for Detecting System-Level Semantic Bugs
17mA Difference World: High-performance, NVM-invariant, Software-only Intermittent...
01h 00mMeasure, Then Build
05mChoose proper container... automatically?
01h 09mThere's Treasure Everywhere