Cav

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.

uniformity

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.