SMT-可满足性模理论

SMT Solver

继上篇有关 SAT 的介绍，我们接着展开看看 SMT - Satisfiability Modulo Theories。 SAT 是基于布尔逻辑回答某个命题的可满足性，如 $x \lor y$ 。但现实中有各种其他的理论，如实数理论等： $a < c \lor a > b$ ，那我们怎么判断这种公式的可满足性呢？

这里我们就提出了可满足性模理论 Satisfiability Modulo Theories：

给定一组理论，根据给定逻辑，求在该组理论解释下公式的可满足性
现有理论通常针对一阶理论，即公理都是一阶的

比如 EUF(Equality with Uninterpreted Functions): $a = b \to f (a) = f (b)$
$a = b \leftrightarrow f (a) = f (b)$
以及等价关系的性质。

再比如线性方程组，算数求解之类的理论。

Eager Method

我们可以将 SMT 问题编码为 SAT 问题，如:

$f (a) = f (c) \land f (b) \neq c \land a \neq b$ , 我们把 $f (a)$ 替换为 $A$ , $f (b)$ 替换为 $B$ ，原式就变为了 $A = C \land B \neq c \land a \neq b$ ，然后根据 EUF 理论的传递性，我们得到一堆的 SAT 可解的命题：

$P_{A = c} \land P_{B = c} \to P_{A = B}$

$P_{A = B} \land P_{B = c} \to P_A = c$

$\dots$

从这个例子就可以知道，Eager 方法有许多问题，再摘自北大软件分析 PPT:

Lazy Method

把 Theory Solver 当作输出 SAT/UNSAT 的黑盒，那么我们可以先把命题看成 SAT 命题，然后有流程：对于一个类似 $f (a) = b \land (g (b) \neq c \lor g (c) = d) \land k (d) = a$ 的公式，

SAT Solver 将其看成 $A \land (\neg B \lor C) \land D$
SAT Solver 返回 SAT 并赋值 ${A = 1, B = 1, C = 1}$
然后把 $A, \neg B, C$ 对应的公式组给到 Theory Solver
Theory Solver 返回 SAT/UNSAT
- SAT，继续让 SAT Solver 赋值，直到赋值 complete 为止
- UNSAT，表示 SAT 达到了 Conflict，加新约束到子句集中，若加入后不可满足了，那么宣告整个命题 UNSAT

Lazy 方法的优点与问题：

怎么解决这个问题呢? 我们只需要给 Theory Solver 加接口就行了，这个就是DPLL(T)算法了（懒得再写了，如北大 PPT 所示）：注意，这里的冲突项的前驱和 SAT 那篇文章里求合适分割是一样的。

混合多个理论 -- Nelson-Oppen 方法

本质和 SAT 与其他理论的结合一样，通过变形让同一个文字(Literal)变为不同的文字，然后让不同的理论处理不同的文字，最后再结合不同 Theory Solver 的结果，也就是让不同理论之间通过接口属性交换信息。但通常我们不能遍历所有的接口属性（通常是无限多的）。

注: 接口属性指的是两种理论都包含的命题集合

$D P L L (T)$ 算法可以处理混合的多个理论，但前提是他们没有共享变量，共享变量的情况该怎么处理呢？

Nelson-Oppen 方法解决了这一问题，但他有一定的限定范围：

两个理论除等号外没有公共函数或者谓词
理论在某种无限域上成立
理论是凸的：
- 这里引入一个凸理论(Convex Theory)，一个理论是凸的当其满足: 其对于每个变量自由的公式 $F$ ，若 $F \to ⋁_{i = 1}^{n} u_{i} = v_{i}$ 则 $F \to u_{i} = v_{i} for some i \in {1, \dots, n}$ 可以举个反例，对于 $F : 1 \leq z \land z \leq 2 \land u = 1 \land v = 2$ 那么 $F \to z = u \lor z = v$
  但是无法推出 $F \to z = u$ 或 $F \to z = v$
  对于凸理论，我们只需要考虑变量之间的等价关系，这些关系则是有限的。

基于以上限制，对于混合多个理论的命题，我们只需要沿着 AST 自底向上将其他理论的子树用变量替代即可, 对于以下例子，假设我们有 EUC 和线性方程组两个理论求解器： $f (f (x) + f (x)) = 2 a$ $f (1) = 1$ $f (2) = a$ $2 x = x + 1$

令 $e_{0} = f (x), e_{1} = e_{0} + e_{0}, e_{2} = 1, e_{3} = 2, e_{4} = 2 x, e_{5} = x + 1, e_{6} = 2 a$ ，对 EUC 我们有:

$e_{0} = f (x)$ $f (e_{1}) = e_{6}$ $f (e_{2}) = e_{2}$ $f (e_{3}) = a$ $e_{4} = e_{5}$

在线性方程组理论中我们有：

$e_{1} = e_{0} + e_{0}$ $e_{2} = 1$ $e_{3} = 2$ $e_{4} = 2 x$ $e_{5} = x + 1$ $e_{6} = 2 a$ $2 x = x + 1$

故我们有共享变量 $V = {x, e_{0}, e_{1}, e_{2}, e_{3}, e_{4}, e_{5}, e_{6}}$

线性方程组理论解得： $x = 1, e_{4} = 2, e_{5} = 2$

接口属性经过 EUC 处理，再次求解得：

$x = e_{2} = 1, e_{0} = f (x) = f (e_{2}) = 1, e_{4} = e_{5} = e_{3} = 2$

线性方程组求解得:

$e_{1} = e_{0} + e_{0} = 2$

EUC 继而求到:

$e_{3} = e_{1} = 2 \to f (e_{1}) = f (e_{3}) \to e_{6} = a$

最后线性方程组求解 $e_{6} = 2 a = a$ 得到 $a = 0$ 还是要注意：沿着 AST 自底向上将其他理论的子树用变量替代，而非所有子树都要用变量代替。

把例子扔了，我们只剩下一个简单的流程：遍历 $V$ 中的变量对 $x, y$ ，然后求解 $F \land x \neq y$ ，如果 UNSAT 说明 $x = y$ 成立

具体理论通常有高效的实现方式

对于非凸包

任何时候遇到一个等价关系的析取式，依次尝试每个等价关系, 如果任意一个得出 SAT，即整体 SAT, 如果全部 UNSAT，即整体 UNSAT。

Application

Z3 是一个基于 SMT 理论的求解器

Alive2 基于 Z3 完成了 LLVM-IR 的程序验证/refinement 关系验证的工作

Reference

北大软件分析