SAT问题求解讲解

1、SAT问题研究小结预备知识：1.基于模型诊断的基本概念介绍：首先我们介绍基于模型诊断的主要思想和框架结构:Fig. I Main idea of model-based diagnosis图1应于模型珍断的主要理想基本定义：(1)诊断系统：一个诊断系统符号化定义即为一个三元组(SD,COMPS,OBS),其中SD为系统描述，是一 阶谓词公式集合；COMPS是系统的组成部件集合，是一个有限常量集合，而OBS是一个观 测集合，是一阶谓词公式的有限集合。简而言之就是把一个相关的系统抽象成符号化的几个 部分，然后把系统模型化，根据逻辑关系和相关的硬件结构抽象成模型，根据模型推理出系 统正常的输出，而往

2、往在实际系统中得到的观测和预期的结果不符，此时便需要诊断出哪些 元件可能出现故障，出现故障的原因，并找到故障元件并解决，其中最主要的是故障元件集 合的找出即：诊断集合。(2)我们把一个元件不正常工作符号化表示即为：AB(c):abnormal,AB(c)为真当且仅当 c 反常，其中 cc COMPS。(3)基于一致性诊断：设组件集合Ae COMPS，称A为关于(SD,COMPS,OBS)的一个基于一致性诊断，如果 SD U OBS U AB(c)|c e COMPS A)是可满足的。(4)极小诊断集：称一个关于(SD,COMPS,OBS)的一个基于一致性诊断A是极小的(MCBD),if不存在A

3、的 任何真子集也是关于(SD,COMPS,OBS)的一个基于一致性诊断。(5)由此我们可以知道：要想判断一个诊断集合是否是基于一致性诊断，只需要判断在这 个诊断集合中的组件都是反常的(是故障的)，然后剩下的组件工作正常工作和系统的相关描 述以及系统在这种情况下系统的观测是否逻辑上可以解释的。(6)命题可满足性问题(propositional Satisfiability Problem,SAT是人工智能里的一个分支，它 是完全NP问题，并且人工智能中很多的NP问题都可以转化成SAT问题，然后求解，相应 的基于模型诊断问题(MBD)问题也可转化为SAT问题，然后求解。(7)集成组合电路可以转化C

4、NF例如与门电路：其可转化为（一 +。）（一+ b）（c + +丁），其转化过程如下: c c a b如果与门工作正常的情况下：则有：c = a其可转化为（一 +。）（一+ b）（c + +丁），其转化过程如下: c c a b如果与门工作正常的情况下：则有：c = a ba b=cc oa bc fa ba bf c(c Ta b a b( +a b)(a b ) +化简转化即为:(G+ )(b+ b a + b + c )同理其它组合电路门转化为CNF如下:与门或门与非门非门或非门同或门异或门选择器a 、/c(c+a)(c+bXc + a+b)(c + a)(c + bXc + a +b)

5、(c + a)(c -l- b)(c + a + b)(a + b)(a + b)(c + a)(c + b Xc + a + b)(c + a+ bXc + a+b) (c + a+bXc+a + b)(c+W 4+b) (S-+ff+bX+a+b)(x+l+fXx+T+ fXx+w+ 手 X+评+ C一般的组合电路如下图:其对应的CNF如下：0 + b + cf)(a + b + cf)(a + b + c)(af + b + c)(a + d)(b + d)(a,+ b + d)(a + e)(b + e)(a + b + e)(d + f)(e +1+ f)(c + f + g)(c

6、+ f + g)(c + f + g)(c + F + g)(g)2.SAT问题定义可满足问题的一些基本定义，表示如下：定义2.1文字(literal):对于变量集合X=x1,x2,x3,.,xn,文字li是变量xi或者否定-xi。定义2.2子句(clause):子句Ci是文字li的析取。二1132 33 34. 3m .定义 2.3.合取范式(conjunctive normal form,CNF):CNF F是子句的合取， F = C1 c C2 c C3.c Cr.定义 2.4 赋值(assignment):v:X f 0,u,1,对于变量集合x1,x2,x3,x4,.,xn:完全赋值(

7、complete assignment):v(x) 0,1,对于所有的 x X;(2)部分赋值(partial assignment):v(x) 0,u,1,其中u是自由变量，其取值范围为： 0uUB)rti i.irn UH ；选择分支变元上1if (MaxsmtHm=0)VUH)UB = MaxsatE(s = 0) *if (Maxsatz( = IXIjB)UE =Max5atz(T= I)；return UB.下界的保守估计：对下界进行估计时，算法需要保证CNF的等价性，在MAXSATz算法中， 下界值得估计工作主要包含两个部分，UP检测和失败文字检测两个方法1)UP检测是依次对合取

8、范式F中的单子句进行单子句传播，以便找到由该单子句传播导致 的冲突集。这部分主要运用了以下6个规则。利用下面这六条规则进行进一步推理产生空子 句，从而得到冲突集和极小冲突集。规则 L 设 F = Vi2 vX Vx2 VV 加 UP,那么 B = gVV.UF& 等价口幻.当子句长度为2时，（力V1,工1V必等价于 4产生了 一个单子句.规则1可以简化CNF范 式，产生寻找冲突集的单子句.规则2. 设F1=翼吊，那么K = 口与F】 等价出规则2表示无论.总赋值为真还是假，I都会产 生一个空子句.规则3. 设F； = I4,后飞理小小 U尸，那么 F尸口V七 U F与尸1等价叫规则4. 设居=

9、父灸1 /久一京2 /心工V 心，心；U F,那么 F = _!/春 + 12vH n-1 V 工 UF与P等价叫规则3、规则1表示的是链式结构的冲突集，它 需要耗费多个二元子句和两个单子句.规则 5. 设 F1 X , 1 V J-2 t i7 I V 3 J X 2 V .z 3 UF那么?产旧石丫/口勺小丫口丫土一声与 Fi等价叫规则6. 设F| = 重，元i V比 ? V/，-3 V k-2 /i V比方一1, 时t V /、k-i V U F ，那么 Fe = （ l , M 1 V 卫 2 +工2 V 至 3 3 1 至2至 V 工,土一丫心-iVi/ur与F等价,.2）单子句排序

10、：效率高的分支限界算法要求有好的分支变元选择策略和有效的冲突集检测方法，本文采用的 是将变元的正负文字在一元子句集，二元子句集和三元子句集中出现次数之和作为该变元的 分数，即：Score（x） = |C| 1 （x）+8*|C| 2 （x）+|C| 3 （x）+|C| 1 （又）+|C| 2 （又）+|C| 3 （x）3）进一步失败文字检测：进一步失败文字检测是在变元xi为真或为假，不能都产生空子句时，继续向前一步检测的方法.其原理下图所示.进一步失败文字检测原理如图表示在进行失败文字检测时，令xi=1进行up可以产生空子句,xi=0进行up未产 生空子句，失败文字检测寻找冲突集不成功.Maxsatz2013在由xi=0赋值简化后的中，继续 检测变元xj，若xj=0和xj=1进行up均产生了空子句，则从xi出发到3个空子句路径上出现 的子句，构成的集合是一个冲突集，下界加1.进一步失败文字因搜索空间大，所以计算成本高 且找到的冲突集规模大.但实验显示进一步失败文字检测仍有助于提高算法下界缩短运行时 间.该函数表述如下：过程2. Furrher failed literal detectionfwr