本文主要是介绍程序验证(七):可满足性模理论(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的布尔结构:
原式 | 布尔结构定义 |
---|---|
B ( ℓ T ) B(\ell_T) B(ℓT) | P i P_i Pi |
B ( ¬ F ) B(\neg F) B(¬F) | ¬ B ( F ) \neg B(F) ¬B(F) |
B ( F 1 ∧ F 2 ) B(F_1\wedge F_2) B(F1∧F2) | B ( F 1 ) ∧ B ( F 2 ) B(F_1)\wedge B(F_2) B(F1)∧B(F2) |
B ( F 1 ∨ F 2 ) B(F_1\vee F_2) B(F1∨F2) | B ( F 1 ) ∨ B ( F 2 ) B(F_1)\vee B(F_2) B(F1)∨B(F2) |
B ( F 1 → F 2 ) B(F_1 \to F_2) B(F1→F2) | B ( F 1 ) → B ( F 2 ) B(F_1)\to B(F_2) B(F1)→B(F2) |
B ( F 1 ↔ F 2 ) B(F_1\leftrightarrow F_2) B(F1↔F2) | B ( F 1 ) ↔ B ( F 2 ) B(F_1) \leftrightarrow B(F_2) B(F1)↔B(F2) |
这里 P i P_i Pi是布尔变量
举例:
考虑以下公式:
F : g ( a ) = c ∧ ( f ( g ( a ) ) ≠ f ( c ) ∨ g ( a ) = d ) ∧ c ≠ d F:g(a)=c\wedge (f(g(a))\ne f(c)\vee g(a)=d)\wedge c\ne 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(c\ne d)=P_1 \wedge (\neg P_2\vee 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)=c\wedge g(a)=d\wedge 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: … x\wedge x\le 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求解器的结合
基本算法
- 构造 F B : = B ( F ) F_B:=B(F) FB:=B(F)
- 如果 F B F_B FB是 u n s a t unsat unsat,那么返回 u n s a t unsat unsat
- 否则,获得一个 F B F_B FB的赋值 α \alpha α
- 构造 C = ⋀ i = 1 n P i ↔ α ( P i ) C=\bigwedge^n_{i=1} P_i\leftrightarrow \alpha (P_i) C=⋀i=1nPi↔α(Pi)
- 将 B − 1 ( C ) B^{-1}(C) B−1(C)发送到 T T T-求解器
- 如果 T T T-求解器判断为 s a t sat sat,那么返回 s a t sat sat
- 否则,更新 F B : = F B ∧ ¬ C F_B :=F_B\wedge \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)=c\wedge (f(g(a))\ne f(c)\vee g(a)=d)\wedge c\ne 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_1\wedge (\neg P_2\vee 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_1\mapsto 1,P_2\mapsto 0,P_3\mapsto 1,P_4\mapsto 0\} α={P1↦1,P2↦0,P3↦1,P4↦0}
- 构造 C = P 1 ∧ ¬ P 2 ∧ P 3 ∧ ¬ P 4 C = P_1\wedge \neg P_2\wedge P_3\wedge \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)=c\wedge f(g(a))\ne f(c)\wedge g(a)=d\wedge c\ne 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\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) 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_1\mapsto 1,P_2\mapsto 1,P_3\mapsto 1,P_4\mapsto 0\} α={P1↦1,P2↦1,P3↦1,P4↦0}
- 构造 C = P 1 ∧ P 2 ∧ P 3 ∧ ¬ P 4 C=P_1\wedge P_2\wedge P_3\wedge \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)=c\wedge f(g(a))=f(c)\wedge g(a)=d\wedge c\ne 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_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) 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_1\mapsto 1,P_2\mapsto 0,P_3\mapsto 0,P_4\mapsto 0\} α={P1↦1,P2↦0,P3↦0,P4↦0}
- 构造 C = P 1 ∧ ¬ P 2 ∧ ¬ P 3 ∧ ¬ P 4 C=P_1\wedge \neg P_2\wedge \neg P_3\wedge \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)=c\wedge f(g(a))\ne f(c)\wedge g(a)\ne d\wedge c\ne 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_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) 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<x\wedge x<1wedge (x<2\vee\dots\vee x<99) F:0<x∧x<1wedge(x<2∨⋯∨x<99)
布尔抽象:
P 0 ∧ P 1 ∧ ( P 2 ∨ ⋯ ∨ P 9 9 ) P_0\wedge P_1\wedge (P_2\vee\dots\vee P_99) P0∧P1∧(P2∨⋯∨P99)
一共有 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)=c\Rightarrow f(g(a))=f(c) g(a)=c⇒f(g(a))=f(c) g ( a ) = c ∧ c ≠ d ⇒ g ( a ) ≠ d g(a)=c\wedge c\ne d\Rightarrow 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_1\to P_2 P1→P2 P 1 ∧ ¬ P 4 → ¬ P 3 P_1\wedge \neg P_4\to \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<x\wedge x<1\wedge x<2\wedge \dots\wedge x<99 F:0<x∧x<1∧x<2∧⋯∧x<99的不满足核是 0 < x ∧ x < 1 0<x\wedge x<1 0<x∧x<1,所以我们添加 ¬ C ∗ \neg C^{*} ¬C∗而不是 ¬ C \neg C ¬C
这篇关于程序验证(七):可满足性模理论(Satisfiability Modulo Theories)的文章就介绍到这儿,希望我们推荐的文章对编程师们有所帮助!