程序验证(二):SAT问题

Tattoo

发布日期: 2020-06-29 10:51:21 浏览量: 131
评分:
star star star star star star star star star star_border
*转载请注明来自write-bug.com

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

注意:原文中有部分公式书写错误,本文转载的时候,修正了这部分错误!

一、概念:Satisfiability Problem

SAT问题:给定一个命题公式FF,决定是否存在一个解释II使得IFI\models F

3SAT问题是首个被确定的NP完全问题。

大多数重要逻辑问题可以归约为SAT:

  • 永真性

  • 蕴含

  • 等价性

SAT求解能力的发展关键:将搜索与推理结合以提高效率。

二、CNF详解

SAT求解器的输入一般是CNF,这里为便于讨论,引入关于CNF的集合表示。

2.1 集合表示

一个公式(formula)可以视为子句(clause)的集合:

可以表示为:

同样,子句可以视为文字(literal)的集合:

可以表示为:

一些通用的表示方法:

Ci{PF}C_i\left \lbrace P\mapsto F \right \rbrace:在子句CiC_i中使用FF替代PP

Ci[P]C_i\left [ P \right ]:变量PP在子句CiC_i中是不取非的,也就是 Ci={..,P,..}C_i = \lbrace .. , P , .. \rbrace

Ci[¬P]C_i[\neg P]:变量PPCiC_i中是取非的,也就是Ci={..,¬P,..}C_i = \lbrace .. , \neg P , .. \rbrace

在这种符号体系下,会有以下命题成立(有点绕,需要多看几遍):

FF表示公式,CC表示子句,基于CNF公式的集合表示,有:

2.2 归结(resolution)

只有一条规则:

给定两个具有相同变量PP,但是对于PP取非情况不同的两个子句,那么:

  • 如果PP为真,那么C2C_2中的其它文字必然为真

  • 如果PP为假,那么C1C_1中的其它文字必然为假

因此,可以在两个子句中都移除PP,也就是归结。

C1{P}C2{¬P}C_1\{P\mapsto \bot\}\vee C_2\{\neg P\mapsto\bot\}

叫做归结式(resolvent)。这个归结式可以作为一个合取子句加入到原公式,这样得到的新公式与原公式等价。

而如果:

C1{p}C2{¬P}==C_1\{p\mapsto \bot\}\vee C_2\{\neg P\mapsto\bot\}=\bot\vee\bot=\bot

那么C1C2C_1\wedge C_2是不可满足的。任何包括 {C1,C2} \lbrace C_1,C_2 \rbrace 在内的CNF都是不可满足的。

举例

ABCA\vee B\vee C¬ABD\neg A\vee B\vee D的归结子句是BCDB\vee C\vee D

三、归结法求解SAT

3.1 归结算法

  • FF^{\prime} 是所有归结式的集合

  • 每一轮迭代,更新FF以包含以产生的归结式

  • 每一轮迭代,计算所有可能的归结式

  • 在更新后的FF上重复归结过程

  • 终止条件:

    • 出现\bot归结式

    • 无法再更新FF(此时所有的可归结的子句都已经被归结了)

举例

(PQ)(PR)(QR)¬R(P\vee Q)\wedge (P\to R)\wedge (Q\to R)\wedge \neg R

3.2 归结算法的评价

解决较大规模问题的效率低下。

四、基于搜索的方法

大致思路:从一个空的解释(interpretation)出发,每次扩展一个变量的取值。

4.1 部分解释

如果II是一个部分解释,文字\ell可以为true,false,undeftrue, false, undef

  • truetrue(satisfied):II\models \ell

  • falsefalse(conflicting):II \nvDash \ell

  • undefundefvar()Ivar(\ell)\notin I

给定一个子句CC和解释II

  • CC is truetrue under II iff ICI\models C

  • CC is falsefalse under II iff ICI \nvDash C

  • CC is unitunit under II iff C=C,IC,C=C^{\prime} \vee \ell, I \nvDash C^{\prime}, \ell is undefundef

  • Otherwise it is undefundef

  1. 说明:
  2. iff: if and only if,当且仅当
  3. unit: 单元,一个新引入的概念

举例

I={P11,P20,P41}I= \lbrace P_1\mapsto 1,P_2\mapsto 0,P_4\mapsto 1 \rbrace,那么有:

  • 1.P1P3¬P4P_1\vee P_3\vee\neg P_4 is truetrue

  • 2.¬P1P2\neg P_1\vee P_2 is falsefalse

  • 3.¬P1¬P4P3\neg P_1\vee\neg P_4 \vee P_3 is unitunit

  • 4.¬P1P3P5\neg P_1\vee P_3 \vee P_5 is undefundef

4.2 搜索程序:一个状态机

每一个状态都记录了部分解释与当前的公式,状态之间的转化由转化规则决定。程序的状态包括:

  • 1.satsat

  • 2.unsatunsat

  • 3.[I]F[I]\Vert F,这里的[I][I]是一个解释,FF是一个CNF

    • 初始状态:[Φ]F[\Phi]\Vert F

    • 结束状态:sat,unsatsat, unsat

    • 中间状态:

      • (1) [Φ]F1[\Phi]\Vert F_1, CC:解释为空,F=F1CF=F_1\wedge C

      • (2) [I1,P¯,I2]F[I_1,\bar{P},I_2]\Vert F:解释先置为I1I_1,然后P0P\mapsto 0,然后解释为I2I_2

4.3 搜索规则

通俗的说,就是深度优先搜索。在某些算法中优化了回退策略。

判定规则(Decision Rule)

回退规则(Backtrack Rule)

可满足规则(Sat Rule)

不可满足规则(Unsat Rule)

以上 4 条规则足以构建一个基本的 sat 求解器。

单元传播规则(Unit Propagation Rule)

条件是

4.4 高级回退&子句学习

基础的回退规则比较“笨”:

  • 它总是回退到最近确定的解释

  • 它不保留子句冲突的信息

引入回跳规则(BackJump Rule):

这里ClC\to l就叫做冲突子句,我们只要避免冲突子句就可以进一步寻找解。

那么,如何找到冲突子句呢?

构造一个蕴含图(implication graph) G=(V,E)G=(V,E)

  • 其中VV对于解释II中每一个判定文字都有一个节点,用这个文字的值和它的判定等级来标记(说白了就是这个文字是你所判定的第几个文字)

  • 对于每个子句C=1..nC=\ell_1\vee .. \vee\ell_n \vee \ell,其中1,..,n\ell_1, .. ,\ell_n被赋值为假,首先为\ell添加一个节点,它的判定等级就是它进入到II的顺序,然后添加边(i,)(\ell_i, \ell)EE,其中1in1\le i\le n

  • 添加一个冲突节点Λ\Lambda。对于所有标记为PP¬P\neg P的冲突变元,在EE中添加从这些节点到Λ\Lambda的边

  • 将每条边都标记上导致这个蕴含关系的子句

例如:

冲突图:只有一个冲突变元,且所有节点都具有通往Λ\Lambda的路径的蕴含图。

例如:

获得冲突子句,考虑一个冲突图GG

  • GG中切一刀,使得:

    • 所有的判定节点在一侧(“原因”)
    • 至少一个冲突文字在另一侧(“结果”)
  • 在“原因”一侧中,选出所有与被切割的边相连的节点KK

  • KK中的节点即为冲突的原因

  • 相应的文字的非生成了冲突子句

例如:

图中¬P5¬P2\neg P_5\vee\neg P_2¬P5P6\neg P_5\vee P_6可以作为冲突子句。

4.5 DPLL & CDCL

CDCL即为(Conflict-Driven Clause Learning),是目前SAT求解器主要采用的方法。

上传的附件

发送私信

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

93
文章数
34
评论数
最近文章
eject