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

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

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

SMT

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

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

DPLL( T T T): DPLL Modulo Theories

这是现代SMT求解器的基础技术
将SMT问题分解为我呢吧可以高效求解的子问题：

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

布尔结构

布尔结构

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

这里 P i P_i Pi​是布尔变量
举例：
考虑以下公式：
F : g ( a ) = c ∧ ( f ( g ( a ) ) ≠ f ( c ) ∨ g ( a ) = d ) ∧ c ≠ d F:g(a)=cwedge (f(g(a))ne f(c)vee g(a)=d)wedge cne d F:g(a)=c∧(f(g(a))​=f(c)∨g(a)=d)∧c​=d
F F F的布尔抽象：
B ( F ) = B ( g ( a ) = c ) ∧ ( B ( f ( g ( a ) ) ≠ f ( c ) ) ∨ B ( g ( a ) = d ) ) ∧ B ( c ≠ d ) = P 1 ∧ ( ¬ P 2 ∨ P 3 ) ∧ ¬ P 4 B(F)=B(g(a)=c)wedge (B(f(g(a))ne f(c))vee B(g(a)=d))wedge B(cne d)=P_1 wedge (neg P_2vee P_3)wedge neg P_4 B(F)=B(g(a)=c)∧(B(f(g(a))​=f(c))∨B(g(a)=d))∧B(c​=d)=P1​∧(¬P2​∨P3​)∧¬P4​
我们也可以定义 B − 1 B^{-1} B−1，比如 B − 1 ( P 1 ∧ P 3 ∧ P 4 ) B^{-1}(P_1 wedge P_3 wedge P_4) B−1(P1​∧P3​∧P4​)就是 g ( a ) = c ∧ g ( a ) = d ∧ c = d g(a)=cwedge g(a)=dwedge c=d g(a)=c∧g(a)=d∧c=d

布尔抽象

为什么称为抽象？因为它实际上是一个过度简化
几个事实：

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

T T T与SAT求解器的结合

基本算法

1. 构造 F B : = B ( F ) F_B:=B(F) FB​:=B(F)
2. 如果 F B F_B FB​是 u n s a t unsat unsat，那么返回 u n s a t unsat unsat
3. 否则，获得一个 F B F_B FB​的赋值 α alpha α
4. 构造 C = ⋀ i = 1 n P i ↔ α ( P i ) C=bigwedge^n_{i=1} P_ileftrightarrow alpha (P_i) C=⋀i=1n​Pi​↔α(Pi​)
5. 将 B − 1 ( C ) B^{-1}(C) B−1(C)发送到 T T T-求解器
6. 如果 T T T-求解器判断为 s a t sat sat，那么返回 s a t sat sat
7. 否则，更新 F B : = F B ∧ ¬ C F_B :=F_Bwedge neg C FB​:=FB​∧¬C，重复以上步骤

最后一步更新的解释：

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

举例

判断以下公式的可满足性：
F : g ( a ) = c ∧ ( f ( g ( a ) ) ≠ f ( c ) ∨ g ( a ) = d ) ∧ c ≠ d F:g(a)=cwedge (f(g(a))ne f(c)vee g(a)=d)wedge cne d F:g(a)=c∧(f(g(a))​=f(c)∨g(a)=d)∧c​=d

• 构造布尔抽象： B ( F ) = P 1 ∧ ( ¬ P 2 ∨ P 3 ) ∧ ¬ P 4 B(F)=P_1wedge (neg P_2vee P_3)wedge neg P_4 B(F)=P1​∧(¬P2​∨P3​)∧¬P4​
• 找到一个 s a t sat sat赋值（通过SAT求解器）： α = { P 1 ↦ 1 , P 2 ↦ 0 , P 3 ↦ 1 , P 4 ↦ 0 } alpha ={P_1mapsto 1,P_2mapsto 0,P_3mapsto 1,P_4mapsto 0} α={P1​↦1,P2​↦0,P3​↦1,P4​↦0}
• 构造 C = P 1 ∧ ¬ P 2 ∧ P 3 ∧ ¬ P 4 C = P_1wedge neg P_2wedge P_3wedge neg P_4 C=P1​∧¬P2​∧P3​∧¬P4​
• 在 T T T-求解器中搜索 B − 1 ( C ) B^{-1}(C) B−1(C): g ( a ) = c ∧ f ( g ( a ) ) ≠ f ( c ) ∧ g ( a ) = d ∧ c ≠ d g(a)=cwedge f(g(a))ne f(c)wedge g(a)=dwedge cne d g(a)=c∧f(g(a))​=f(c)∧g(a)=d∧c​=d u n s a t unsat unsat
• 更新 F B F_B FB​: P 1 ∧ ( ¬ P 2 ∨ P 3 ) ∧ ¬ P 4 ∧ ( ¬ P 1 ∨ P 2 ∨ ¬ P 3 ∨ P 4 ) P_1wedge (neg P_2vee P_3)wedge neg P_4wedge (neg P_1vee P_2veeneg P_3 vee P_4) P1​∧(¬P2​∨P3​)∧¬P4​∧(¬P1​∨P2​∨¬P3​∨P4​)
• 找到一个 s a t sat sat赋值（通过SAT求解器）： α = { P 1 ↦ 1 , P 2 ↦ 1 , P 3 ↦ 1 , P 4 ↦ 0 } alpha ={P_1mapsto 1,P_2mapsto 1,P_3mapsto 1,P_4mapsto 0} α={P1​↦1,P2​↦1,P3​↦1,P4​↦0}
• 构造 C = P 1 ∧ P 2 ∧ P 3 ∧ ¬ P 4 C=P_1wedge P_2wedge P_3wedge neg P_4 C=P1​∧P2​∧P3​∧¬P4​
• 在 T T T-求解器中搜索 B − 1 ( C ) B^{-1}(C) B−1(C): g ( a ) = c ∧ f ( g ( a ) ) = f ( c ) ∧ g ( a ) = d ∧ c ≠ d g(a)=cwedge f(g(a))=f(c)wedge g(a)=dwedge cne d g(a)=c∧f(g(a))=f(c)∧g(a)=d∧c​=d u n s a t unsat unsat
• 更新 F B F_B FB​: P 1 ∧ ( ¬ P 2 ∨ P 3 ) ∧ ¬ P 4 ∧ ( ¬ P 1 ∨ P 2 ∨ ¬ P 3 ∨ P 4 ) ∧ ( ¬ P 1 ∨ ¬ P 2 ∨ ¬ P 3 ∨ P 4 ) P_1wedge (neg P_2vee P_3)wedge neg P_4wedge (neg P_1vee P_2veeneg P_3vee P_4)wedge (neg P_1veeneg P_2veeneg P_3vee P_4) P1​∧(¬P2​∨P3​)∧¬P4​∧(¬P1​∨P2​∨¬P3​∨P4​)∧(¬P1​∨¬P2​∨¬P3​∨P4​)
• 找到一个赋值： α = { P 1 ↦ 1 , P 2 ↦ 0 , P 3 ↦ 0 , P 4 ↦ 0 } alpha = {P_1mapsto 1,P_2mapsto 0,P_3mapsto 0,P_4mapsto 0} α={P1​↦1,P2​↦0,P3​↦0,P4​↦0}
• 构造 C = P 1 ∧ ¬ P 2 ∧ ¬ P 3 ∧ ¬ P 4 C=P_1wedge neg P_2wedge neg P_3wedge neg P_4 C=P1​∧¬P2​∧¬P3​∧¬P4​
• 在 T T T-求解器中搜索 B − 1 ( C ) B^{-1}(C) B−1(C): g ( a ) = c ∧ f ( g ( a ) ) ≠ f ( c ) ∧ g ( a ) ≠ d ∧ c ≠ d g(a)=cwedge f(g(a))ne f(c)wedge g(a)ne dwedge cne d g(a)=c∧f(g(a))​=f(c)∧g(a)​=d∧c​=d
• 更新 F B F_B FB​: P 1 ∧ ( ¬ P 2 ∨ P 3 ) ∧ ¬ P 4 ∧ ( ¬ P 1 ∨ P 2 ∨ ¬ P 3 ∨ P 4 ) ∧ ( ¬ P 1 ∨ ¬ P 2 ∨ ¬ P 3 ∨ P 4 ) ∧ ( ¬ P 1 ∨ P 2 ∨ P 3 ∨ P 4 ) P_1wedge (neg P_2vee P_3)wedge neg P_4wedge (neg P_1vee P_2veeneg P_3vee P_4)wedge (neg P_1veeneg P_2vee neg P_3vee P_4)wedge (neg P_1vee P_2vee P_3vee P_4) P1​∧(¬P2​∨P3​)∧¬P4​∧(¬P1​∨P2​∨¬P3​∨P4​)∧(¬P1​∨¬P2​∨¬P3​∨P4​)∧(¬P1​∨P2​∨P3​∨P4​)
• 注意，这个布尔抽象已经是 u n s a t unsat unsat了，所以我们说 F F F是 u n s a t unsat unsat了。

另一个例子

考虑这样的 T Z T_Z TZ​-公式 F F F:
F : 0 < x ∧ x < 1 w e d g e ( x < 2 ∨ ⋯ ∨ x < 99 ) F:0<xwedge x<1wedge (x<2veedotsvee x<99) F:0<x∧x<1wedge(x<2∨⋯∨x<99)
布尔抽象：
P 0 ∧ P 1 ∧ ( P 2 ∨ ⋯ ∨ P 9 9 ) P_0wedge P_1wedge (P_2veedotsvee P_99) P0​∧P1​∧(P2​∨⋯∨P9​9)
一共有 2 98 − 1 2^{98}-1 298−1个可满足的赋值，但是没有一个满足 F F F。然而，我们每次只能添加一个冲突子句！所以我们需要改进。

真正的DPLL( T T T)

思路：

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

举例

还是之前的例子

• 布尔抽象： B ( F ) = { { P 1 } , { ¬ P 2 , P 3 } , { ¬ P 4 } } B(F)={{P_1},{neg P_2,P_3},{neg P_4}} B(F)={{P1​},{¬P2​,P3​},{¬P4​}}
• DPLL从 P 1 P_1 P1​， ¬ P 4 neg P_4 ¬P4​开始
• 此时，根据公理，我们有更多的逻辑传递： g ( a ) = c ⇒ f ( g ( a ) ) = f ( c ) g(a)=cRightarrow f(g(a))=f(c) g(a)=c⇒f(g(a))=f(c) g ( a ) = c ∧ c ≠ d ⇒ g ( a ) ≠ d g(a)=cwedge cne dRightarrow g(a)ne d g(a)=c∧c​=d⇒g(a)​=d
• 判定 ¬ P 2 neg P_2 ¬P2​与 P 3 P_3 P3​过于冗长，所以我们可以添加一些引理(theory lemmas): P 1 → P 2 P_1to P_2 P1​→P2​ P 1 ∧ ¬ P 4 → ¬ P 3 P_1wedge neg P_4to neg P_3 P1​∧¬P4​→¬P3​

核(unsat core)

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

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