程序验证（七）：可满足性模理论(Satisfiability Modulo Theories) SMT Satisfiability Modulo Theories(SMT)是以下情况的公式的判定问题： 一些一阶理论的复合具有任意的布尔结构 DPLL( T T T): DPLL Modulo Theories 这是现代SMT求解器的基础技术 将SMT问题分解为我呢吧可以高效求解的子问题：