XChy's Blog

For life

0%

SMT-可满足性模理论

Posted on In

SMT Solver

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

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

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

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

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

Eager Method

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

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

    \[ P_{A=c} \wedge P_{B=c} \rightarrow P_{A=B} \]

    \[ P_{A=B} \wedge P_{B=c} \rightarrow P\_{A=c} \]

    \[ \cdots \]

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

Lazy Method

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

  • SAT Solver 将其看成 \(A \wedge (\neg B \vee C) \wedge 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 方法的优点与问题： img1

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

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

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

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

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

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

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

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

令\(e_0 = f(x), e_1 = e_0 + e_0, e_2 = 1, e_3 = 2, e_4 = 2x, e_5 = x + 1, e_6 = 2a\) ，对 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 = 2x\] \[e_5 = x + 1\] \[e_6 = 2a\] \[2x = 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 \rightarrow f(e_1) = f(e_3) \rightarrow e_6 = a\]

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

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

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

对于非凸包

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

Application

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

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

Reference

北大软件分析