Efficient Sampling of SAT Solutions for Testing
We developed a new algorithm QuickSampler which requires a small number of solver calls to produce millions of samples which satisfy the constraints with high probability.
Instead of generating a single solution for the path constraint of a path prefix, one could generate multiple solutions to randomly test multiple paths having the same prefix. We call this approach constraint-based fuzzing.
Our goal is to efficiently generate lots of random satisfying assignments to SAT formulas, also known as SAT witnesses.
Random assignment => atomic mutations => combination =>
Very similar to generic mutations.