SAT 与 SMT：一句话区分

• SAT：命题逻辑公式是否可满足（变量 ∈ {0,1}）。
• SMT：在 SAT 之上叠加理论（位向量、数组、线性算术……），更贴近硬件断言。

硬件模型检测与等价性检查里，位向量 SMT 几乎是默认语言。

← 返回 Notes