一句话：提出 QuickSampler，以少量 SAT 求解器调用高效生成大量满足约束的解，用于测试。
软件与硬件测试（如模糊测试和激励生成）常需生成大量满足给定约束的输入，但既要采样高效又要保证样本多样、分布合理十分困难。论文提出 QuickSampler：一种面向 SAT 约束解的采样算法，仅需少量求解器调用即可生成大量满足约束的样本，并以较高概率保证有效性。作者在大型真实基准上评估，结果表明 QuickSampler 生成唯一有效解的速度比现有先进采样工具快若干数量级，且实际分布相当接近均匀分布。
In software and hardware testing, generating multiple inputs which satisfy a given set of constraints is an important problem with applications in fuzz testing and stimulus generation. However, it is a challenge to perform the sampling efficiently, while generating a diverse set of inputs which satisfy the constraints. 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. We evaluate QuickSampler on large real-world benchmarks and show that it can produce unique valid solutions orders of magnitude faster than other state-of-the-art sampling tools, with a distribution which is reasonably close to uniform in practice.