程序验证（七）：可满足性模理论(Satisfiability Modulo Theories)

大家好，我是讯享网，很高兴认识大家。

程序验证（七）：可满足性模理论(Satisfiability Modulo Theories)

SMT

Satisfiability Modulo Theories(SMT)是以下情况的公式的判定问题：

一些一阶理论的复合
具有任意的布尔结构

DPLL( $T$ ): DPLL Modulo Theories

使用SAT求解技术来处理布尔结构（宏观）
使用专门的理论求解器(theory solver)来判定背景理论的可满足性（微观）

布尔结构

通过 $T$ -公式的语义，我们递归定义公式 $F$ 的布尔结构：

原式	布尔结构定义
$B(\ell_T)$	$P_i$
$B(\neg F)$	$\neg B(F)$
$B(F_1\wedge F_2)$	$B(F_1)\wedge B(F_2)$
$B(F_1\vee F_2)$	$B(F_1)\vee B(F_2)$
$B(F_1 \to F_2)$	$B(F_1)\to B(F_2)$
$B(F_1\leftrightarrow F_2)$	$B(F_1) \leftrightarrow B(F_2)$

这里 $P_i$ 是布尔变量
举例：
考虑以下公式：
$F:g(a)=c\wedge (f(g(a))\ne f(c)\vee g(a)=d)\wedge c\ne d$
$F$ 的布尔抽象：
$B(F)=B(g(a)=c)\wedge (B(f(g(a))\ne f(c))\vee B(g(a)=d))\wedge B(c\ne d)=P_1 \wedge (\neg P_2\vee P_3)\wedge \neg P_4$
我们也可以定义 $B^{-1}$ ，比如 $B^{-1}(P_1 \wedge P_3 \wedge P_4)$ 就是 $g(a)=c\wedge g(a)=d\wedge c=d$

布尔抽象

如果 $F$ 是 $s a t$ ，那么 $B (F)$ 总是 $s a t$
如果 $B (F)$ 是 $s a t$ ，那么 $F$ 一定是 $s a t$ 吗？不是，如： $KaTeX parse error: Undefined control sequence: \wedgef at position 22: … x\wedge x\le 2\̲w̲e̲d̲g̲e̲f̲(x)\ne f(1)\wed…$
如果 $F$ 是 $u n s a t$ ，那么 $B (F)$ 一定是 $u n s a t$ 吗？不是，举例同上。
如果 $B (F)$ 是 $u n s a t$ ，那么 $F$ 呢？是。

$T$ 与SAT求解器的结合

基本算法

构造 $F_B:=B(F)$
如果 $F_B$ 是 $u n s a t$ ，那么返回 $u n s a t$
否则，获得一个 $F_B$ 的赋值 $\alpha$
构造 $C=\bigwedge^n_{i=1} P_i\leftrightarrow \alpha (P_i)$
将 $B^{-1}(C)$ 发送到 $T$ -求解器
如果 $T$ -求解器判断为 $s a t$ ，那么返回 $s a t$
否则，更新 $F_B :=F_B\wedge \neg C$ ，重复以上步骤

最后一步更新的解释：

讯享网

如果不更新，我们的 $F_B$ 会得到同样的 $u n s a t$ 模型
$\neg C$ 叫做理论冲突子句(theory conflict clause)
更新之后，可以防止求解器未来搜索同样的路径

举例

判断以下公式的可满足性：
$F:g(a)=c\wedge (f(g(a))\ne f(c)\vee g(a)=d)\wedge c\ne d$

构造布尔抽象： $B(F)=P_1\wedge (\neg P_2\vee P_3)\wedge \neg P_4$
找到一个 $s a t$ 赋值（通过SAT求解器）： $\alpha =\{P_1\mapsto 1,P_2\mapsto 0,P_3\mapsto 1,P_4\mapsto 0\}$
构造 $P_1\wedge \neg P_2\wedge P_3\wedge \neg P_4$
在 $T$ -求解器中搜索 $B^{-1}(C)$ : $g(a)=c\wedge f(g(a))\ne f(c)\wedge g(a)=d\wedge c\ne d$ $u n s a t$
更新 $F_B$ : $P_1\wedge (\neg P_2\vee P_3)\wedge \neg P_4\wedge (\neg P_1\vee P_2\vee\neg P_3 \vee P_4)$
找到一个 $s a t$ 赋值（通过SAT求解器）： $\alpha =\{P_1\mapsto 1,P_2\mapsto 1,P_3\mapsto 1,P_4\mapsto 0\}$
构造 $C=P_1\wedge P_2\wedge P_3\wedge \neg P_4$
在 $T$ -求解器中搜索 $B^{-1}(C)$ : $g(a)=c\wedge f(g(a))=f(c)\wedge g(a)=d\wedge c\ne d$ $u n s a t$
更新 $F_B$ : $P_1\wedge (\neg P_2\vee P_3)\wedge \neg P_4\wedge (\neg P_1\vee P_2\vee\neg P_3\vee P_4)\wedge (\neg P_1\vee\neg P_2\vee\neg P_3\vee P_4)$
找到一个赋值： $\alpha = \{P_1\mapsto 1,P_2\mapsto 0,P_3\mapsto 0,P_4\mapsto 0\}$
构造 $C=P_1\wedge \neg P_2\wedge \neg P_3\wedge \neg P_4$
在 $T$ -求解器中搜索 $B^{-1}(C)$ : $g(a)=c\wedge f(g(a))\ne f(c)\wedge g(a)\ne d\wedge c\ne d$
更新 $F_B$ : $P_1\wedge (\neg P_2\vee P_3)\wedge \neg P_4\wedge (\neg P_1\vee P_2\vee\neg P_3\vee P_4)\wedge (\neg P_1\vee\neg P_2\vee \neg P_3\vee P_4)\wedge (\neg P_1\vee P_2\vee P_3\vee P_4)$
注意，这个布尔抽象已经是 $u n s a t$ 了，所以我们说 $F$ 是 $u n s a t$ 了。

另一个例子

考虑这样的 $T_Z$ -公式 $F$ :
$F:0<x\wedge x<1wedge (x<2\vee\dots\vee x<99)$
布尔抽象：
$P_0\wedge P_1\wedge (P_2\vee\dots\vee P_99)$
一共有 $2^{98}-1$ 个可满足的赋值，但是没有一个满足 $F$ 。然而，我们每次只能添加一个冲突子句！所以我们需要改进。

真正的DPLL( $T$ )

思路：

不要把SAT求解器看做一个黑箱
当构造出赋值的时候，渐进的查询理论求解器
在之前的例子中，添加 ${0<x,x<1\}$ 后会立刻停止

举例

还是之前的例子

布尔抽象： $B(F)=\{\{P_1\},\{\neg P_2,P_3\},\{\neg P_4\}\}$
DPLL从 $P_1$ ， $\neg P_4$ 开始
此时，根据公理，我们有更多的逻辑传递： $g(a)=c\Rightarrow f(g(a))=f(c)$ $g(a)=c\wedge c\ne d\Rightarrow g(a)\ne d$
判定 $\neg P_2$ 与 $P_3$ 过于冗长，所以我们可以添加一些引理(theory lemmas): $P_1\to P_2$ $P_1\wedge \neg P_4\to \neg P_3$

核(unsat core)

我们之前是把 $\neg C$ 添加到原式
一个不满足核(unsatisfiable core) $C^{*}$ 是 $C$ 的一个子集，满足：

$C^{*}$ 依然是不可满足的
删除 $C^{*}$ 的任何元素，都使它可满足
比如， $F:0<x\wedge x<1\wedge x<2\wedge \dots\wedge x<99$ 的不满足核是 $0<x\wedge x<1$ ，所以我们添加 $\neg C^{*}$ 而不是 $\neg C$

程序验证（七）：可满足性模理论(Satisfiability Modulo Theories)