SATvsSMT

SAT

SAT（Boolean Satisfiability Problem）是计算机科学中第一个被证明为 NP 完全的问题：给定一个布尔公式，判断是否存在一组变量赋值使公式为真。SAT 求解器是 SMT 求解器的核心引擎，也是符号执行、模型检验、形式化验证等技术的底层基础。

SMT

SMT（Satisfiability Modulo Theories）是在 SAT（布尔可满足性）基础上扩展了算术、位向量、数组等理论的自动化约束求解框架。在二进制安全领域，SMT 求解器（如 Z3）被广泛用于符号执行、反混淆、漏洞自动发现和 CTF 解题——将程序行为建模为数学约束，让求解器自动找出满足特定条件的输入。

SAT

• 第一个被证明为 NP 完全的问题（Cook-Levin 定理）
• SMT 求解器的核心引擎
• 现代 SAT 求解器可处理数百万变量的实际问题

SMT

• 在 SAT 基础上扩展算术/位向量等理论的约束求解
• 二进制逆向和漏洞挖掘的核心引擎
• Z3 是最广泛使用的 SMT 求解器

SAT

判断给定布尔公式是否存在使其为真的变量赋值的判定问题，是计算复杂性理论中第一个 NP 完全问题

SMT

在布尔可满足性（SAT）基础上扩展了算术、位向量、数组等一阶逻辑理论的自动化约束求解框架

SAT

• SMT 求解器的底层引擎（bit-blasting 后归约为 SAT）
• 硬件电路等价性验证
• 模型检验中的状态空间搜索
• 密码学中的约束求解攻击

SMT

• 符号执行中判断程序路径可达性
• 自动生成触发漏洞的 PoC 输入
• CTF 逆向题自动求解校验逻辑
• 去除代码混淆/简化表达式

SAT

SAT 问题的输入通常是 CNF（合取范式）形式的布尔公式：多个子句的 AND，每个子句是若干文字的 OR。例如 (x₁ ∨ ¬x₂) ∧ (x₂ ∨ x₃) ∧ (¬x₁ ∨ ¬x₃)。虽然 SAT 理论上是 NP 完全的（最坏情况指数时间），但现代 SAT 求解器（如 MiniSat、CaDiCaL）通过 DPLL/CDCL 算法和大量启发式优化，在实际问题上表现极好，能处理工业级规模的实例。在二进制安全中，SMT 求解器内部将位向量/算术约束最终编码（bit-blasting）为 SAT 问题交给 SAT 引擎求解。

SMT

SMT 的核心思想是将程序逻辑转化为数学公式：将变量、运算、分支条件表达为约束，然后问求解器「是否存在一组输入使这些约束同时成立」。在二进制安全中的典型应用：1) 符号执行（Symbolic Execution）——用符号变量代替具体输入跟踪程序执行，在每个分支处收集约束，用 SMT 求解判断路径可达性；2) 反混淆——将混淆后的表达式简化为等价的简单形式；3) 漏洞自动发现——构造使程序触发缓冲区溢出/整数溢出等条件的输入；4) CTF 逆向题——自动求解复杂的校验逻辑找出正确 flag。常用工具：Z3（微软）、angr（符号执行框架）、Triton（动态二进制分析）。