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

Tattoo

发布日期: 2020-06-30 16:30:18 浏览量: 25
评分:
star star star star star star star star star star
*转载请注明来自write-bug.com

版权声明:本文为CSDN博主「swy_swy_swy」的原创文章,遵循CC 4.0 BY-SA版权协议,转载请附上原文出处链接及本声明。
原文链接:https://blog.csdn.net/swy_swy_swy/article/details/106675816

一、SMT

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

  • 一些一阶理论的复合

  • 具有任意的布尔结构

二、DPLL(T): DPLL Modulo Theories

这是现代SMT求解器的基础技术。

将SMT问题分解为可以高效求解的子问题:

  • 使用SAT求解技术来处理布尔结构(宏观)

  • 使用专门的理论求解器(theory solver)来判定背景理论的可满足性(微观)

三、布尔结构

通过TT-公式的语义,我们递归定义公式FF的布尔结构:

这里PiP_i是布尔变量。

举例:考虑以下公式

F:g(a)=c(f(g(a))f(c)g(a)=d)cdF:g(a)=c\wedge (f(g(a))\ne f(c)\vee g(a)=d)\wedge c\ne d

FF的布尔抽象:

B(F)=B(g(a)=c)(B(f(g(a))f(c))B(g(a)=d))B(cd)=P1(¬P2P3)¬P4B(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

我们也可以定义B1B^{-1},比如B1(P1P3P4)B^{-1}(P_1 \wedge P_3 \wedge P_4)就是g(a)=cg(a)=dc=dg(a)=c\wedge g(a)=d\wedge c=d

3.1 布尔抽象

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

  • 如果FFsatsat,那么B(F)B(F)总是satsat

  • 如果B(F)B(F)satsat,那么FF一定是satsat吗?不是

  • 如果FFunsatunsat,那么B(F)B(F)一定是unsatunsat吗?不是

  • 如果B(F)B(F)unsatunsat,那么FF呢?是

3.2 T与SAT求解器的结合

3.2.1 基本算法

  • 构造FB:=B(F)F_B:=B(F)

  • 如果FBF_Bunsatunsat,那么返回unsatunsat

  • 否则,获得一个FBF_B的赋值α\alpha

  • 构造C=i=1nPiα(Pi)C=\bigwedge^n_{i=1} P_i\leftrightarrow \alpha (P_i)

  • B1(C)B^{-1}(C)发送到TT-求解器

  • 如果TT-求解器判断为satsat,那么返回satsat

  • 否则,更新FB:=FB¬CF_B :=F_B\wedge \neg C,重复以上步骤

最后一步更新的解释:

  • 如果不更新,我们的FBF_B会得到同样的unsatunsat模型

  • 其中¬C\neg C叫做理论冲突子句(theory conflict clause)

  • 更新之后,可以防止求解器未来搜索同样的路径

3.2.2 举例

判断以下公式的可满足性:

F:g(a)=c(f(g(a))f(c)g(a)=d)cdF:g(a)=c\wedge (f(g(a))\ne f(c)\vee g(a)=d)\wedge c\ne d

构造布尔抽象:

B(F)=P1(¬P2P3)¬P4B(F)=P_1\wedge (\neg P_2\vee P_3)\wedge \neg P_4

找到一个satsat赋值(通过SAT求解器):

α={P11,P20,P31,P40}\alpha =\{P_1\mapsto 1,P_2\mapsto 0,P_3\mapsto 1,P_4\mapsto 0\}

构造C=P1¬P2P3¬P4C = P_1\wedge \neg P_2\wedge P_3\wedge \neg P_4

TT-求解器中搜索B1(C)B^{-1}(C)

g(a)=cf(g(a))f(c)g(a)=dcdg(a)=c\wedge f(g(a))\ne f(c)\wedge g(a)=d\wedge c\ne d

unsatunsat

更新FBF_B

P1(¬P2P3)¬P4(¬P1P2¬P3P4)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)

找到一个satsat赋值(通过SAT求解器):

α={P11,P21,P31,P40}\alpha =\{P_1\mapsto 1,P_2\mapsto 1,P_3\mapsto 1,P_4\mapsto 0\}

构造C=P1P2P3¬P4C=P_1\wedge P_2\wedge P_3\wedge \neg P_4

TT-求解器中搜索B1(C)B^{-1}(C)

g(a)=cf(g(a))=f(c)g(a)=dcdg(a)=c\wedge f(g(a))=f(c)\wedge g(a)=d\wedge c\ne d

unsatunsat

更新FBF_B

P1(¬P2P3)¬P4(¬P1P2¬P3P4)(¬P1¬P2¬P3P4)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)

找到一个赋值:

α={P11,P20,P30,P40}\alpha = \{P_1\mapsto 1,P_2\mapsto 0,P_3\mapsto 0,P_4\mapsto 0\}

构造C=P1¬P2¬P3¬P4C=P_1\wedge \neg P_2\wedge \neg P_3\wedge \neg P_4

TT-求解器中搜索B1(C)B^{-1}(C)

g(a)=cf(g(a))f(c)g(a)dcdg(a)=c\wedge f(g(a))\ne f(c)\wedge g(a)\ne d\wedge c\ne d

更新FBF_B

P1(¬P2P3)¬P4(¬P1P2¬P3P4)(¬P1¬P2¬P3P4)(¬P1P2P3P4)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)

注意,这个布尔抽象已经是unsatunsat了,所以我们说FFunsatunsat了。

3.2.3 另一个例子

考虑这样的TZT_Z-公式FF

F:0<xx<1wedge(x<2..x<99)F:0 < x\wedge x < 1wedge (x < 2\vee .. \vee x < 99)

布尔抽象:

P0P1(P2..P99)P_0\wedge P_1\wedge (P_2\vee .. \vee P_99)

一共有29812^{98}-1个可满足的赋值,但是没有一个满足FF。然而,我们每次只能添加一个冲突子句!所以我们需要改进。

四、真正的DPLL(TTT)

4.1 思路

  • 不要把SAT求解器看做一个黑箱

  • 当构造出赋值的时候,渐进的查询理论求解器

  • 在之前的例子中,添加{0<x,x<1}\lbrace 0<x,x<1 \rbrace后会立刻停止

4.2 举例

还是之前的例子:

  • 布尔抽象:B(F)=P1,¬P2,P3,¬P4B(F)={{P_1},{\neg P_2,P_3},{\neg P_4}}

  • DPLL从P1P_1¬P4\neg P_4开始

  • 此时,根据公理,我们有更多的逻辑传递:

g(a)=cf(g(a))=f(c)g(a)=c\Rightarrow f(g(a))=f(c)

g(a)=ccdg(a)dg(a)=c\wedge c\ne d\Rightarrow g(a)\ne d

判定¬P2\neg P_2P3P_3过于冗长,所以我们可以添加一些引理(theory lemmas):

P1P2P_1\to P_2

P1¬P4¬P3P_1\wedge \neg P_4\to \neg P_3

4.3 核(unsat core)

我们之前是把¬C\neg C添加到原式,一个不满足核(unsatisfiable core)CC^{*}是CCC的一个子集,满足:

  • CC^{*}依然是不可满足的

  • 删除CC^{*}的任何元素,都使它可满足

比如

F:0<xx<1x<2..x<99F:0 < x\wedge x < 1\wedge x < 2\wedge .. \wedge x < 99

不满足核是0<xx<10<x \wedge x<1,所以我们添加¬C\neg C^{*}而不是¬C\neg C

上传的附件

发送私信

人生最好的三个词:久别重逢,失而复得,虚惊一场

48
文章数
33
评论数
最近文章
eject