一句话：提出近似求解器 FUZZY-SAT，用模糊测试技术判定符号公式可满足性，作为混合模糊测试中 SMT 求解的替代与补充。
软件测试中模糊测试、符号执行与混合模糊测试广泛结合，SMT 求解器被用于推理分析中收集的符号表达式。本文研究能否将模糊测试领域的技术用于判断符号公式是否可满足，从而为 concolic 与 hybrid fuzzing 引擎提供经典 SMT 求解之外的可行替代。作者设计了近似求解器 FUZZY-SAT，并针对混合模糊器生成的查询，与 Z3 等最新求解器进行比较。结果表明，FUZZY-SAT 既具有竞争力，又与现有最先进求解器形成互补。
Recent years have witnessed a wide array of results in software testing, exploring different approaches and methodologies ranging from fuzzers to symbolic engines, with a full spectrum of instances in between such as concolic execution and hybrid fuzzing. A key ingredient of many of these tools is Satisfiability Modulo Theories (SMT) solvers, which are used to reason over symbolic expressions collected during the analysis. In this paper, we investigate whether techniques borrowed from the fuzzing domain can be applied to check whether symbolic formulas are satisfiable in the context of concolic and hybrid fuzzing engines, providing a viable alternative to classic SMT solving techniques. We devise a new approximate solver, FUZZY-SAT, and show that it is both competitive with and complementary to state-of-the-art solvers such as Z3 with respect to handling queries generated by hybrid fuzzers.