SAT問題求解講解

1、SAT問題研究小結(jié)預(yù)備知識：1.基于模型診斷的基本概念介紹：首先我們介紹基于模型診斷的主要思想和框架結(jié)構(gòu):Fig. I Main idea of model-based diagnosis圖1應(yīng)于模型珍斷的主要理想基本定義：(1)診斷系統(tǒng)：一個(gè)診斷系統(tǒng)符號化定義即為一個(gè)三元組(SD,COMPS,OBS),其中SD為系統(tǒng)描述，是一 階謂詞公式集合；COMPS是系統(tǒng)的組成部件集合，是一個(gè)有限常量集合，而OBS是一個(gè)觀 測集合，是一階謂詞公式的有限集合。簡而言之就是把一個(gè)相關(guān)的系統(tǒng)抽象成符號化的幾個(gè) 部分，然后把系統(tǒng)模型化，根據(jù)邏輯關(guān)系和相關(guān)的硬件結(jié)構(gòu)抽象成模型，根據(jù)模型推理出系 統(tǒng)正常的輸出，而往

2、往在實(shí)際系統(tǒng)中得到的觀測和預(yù)期的結(jié)果不符，此時(shí)便需要診斷出哪些 元件可能出現(xiàn)故障，出現(xiàn)故障的原因，并找到故障元件并解決，其中最主要的是故障元件集 合的找出即：診斷集合。(2)我們把一個(gè)元件不正常工作符號化表示即為：AB(c):abnormal,AB(c)為真當(dāng)且僅當(dāng) c 反常，其中 cc COMPS。(3)基于一致性診斷：設(shè)組件集合Ae COMPS，稱A為關(guān)于(SD,COMPS,OBS)的一個(gè)基于一致性診斷，如果 SD U OBS U AB(c)|c e COMPS A)是可滿足的。(4)極小診斷集：稱一個(gè)關(guān)于(SD,COMPS,OBS)的一個(gè)基于一致性診斷A是極小的(MCBD),if不存在A

3、的 任何真子集也是關(guān)于(SD,COMPS,OBS)的一個(gè)基于一致性診斷。(5)由此我們可以知道：要想判斷一個(gè)診斷集合是否是基于一致性診斷，只需要判斷在這 個(gè)診斷集合中的組件都是反常的(是故障的)，然后剩下的組件工作正常工作和系統(tǒng)的相關(guān)描 述以及系統(tǒng)在這種情況下系統(tǒng)的觀測是否邏輯上可以解釋的。(6)命題可滿足性問題(propositional Satisfiability Problem,SAT是人工智能里的一個(gè)分支，它 是完全NP問題，并且人工智能中很多的NP問題都可以轉(zhuǎn)化成SAT問題，然后求解，相應(yīng) 的基于模型診斷問題(MBD)問題也可轉(zhuǎn)化為SAT問題，然后求解。(7)集成組合電路可以轉(zhuǎn)化C

4、NF例如與門電路：其可轉(zhuǎn)化為（一 +。）（一+ b）（c + +丁），其轉(zhuǎn)化過程如下: c c a b如果與門工作正常的情況下：則有：c = a其可轉(zhuǎn)化為（一 +。）（一+ b）（c + +丁），其轉(zhuǎn)化過程如下: c c a b如果與門工作正常的情況下：則有：c = a ba b=cc oa bc fa ba bf c(c Ta b a b( +a b)(a b ) +化簡轉(zhuǎn)化即為:(G+ )(b+ b a + b + c )同理其它組合電路門轉(zhuǎn)化為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一般的組合電路如下圖:其對應(yīng)的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.下界的保守估計(jì)：對下界進(jìn)行估計(jì)時(shí)，算法需要保證CNF的等價(jià)性，在MAXSATz算法中， 下界值得估計(jì)工作主要包含兩個(gè)部分，UP檢測和失敗文字檢測兩個(gè)方法1)UP檢測是依次對合取

8、范式F中的單子句進(jìn)行單子句傳播，以便找到由該單子句傳播導(dǎo)致 的沖突集。這部分主要運(yùn)用了以下6個(gè)規(guī)則。利用下面這六條規(guī)則進(jìn)行進(jìn)一步推理產(chǎn)生空子 句，從而得到?jīng)_突集和極小沖突集。規(guī)則 L 設(shè) F = Vi2 vX Vx2 VV 加 UP,那么 B = gVV.UF& 等價(jià)口幻.當(dāng)子句長度為2時(shí)，（力V1,工1V必等價(jià)于 4產(chǎn)生了 一個(gè)單子句.規(guī)則1可以簡化CNF范 式，產(chǎn)生尋找沖突集的單子句.規(guī)則2. 設(shè)F1=翼吊，那么K = 口與F】 等價(jià)出規(guī)則2表示無論.總賦值為真還是假，I都會產(chǎn) 生一個(gè)空子句.規(guī)則3. 設(shè)F； = I4,后飛理小小 U尸，那么 F尸口V七 U F與尸1等價(jià)叫規(guī)則4. 設(shè)居=

9、父灸1 /久一京2 /心工V 心，心；U F,那么 F = _!/春 + 12vH n-1 V 工 UF與P等價(jià)叫規(guī)則3、規(guī)則1表示的是鏈?zhǔn)浇Y(jié)構(gòu)的沖突集，它 需要耗費(fèi)多個(gè)二元子句和兩個(gè)單子句.規(guī)則 5. 設(shè) F1 X , 1 V J-2 t i7 I V 3 J X 2 V .z 3 UF那么?產(chǎn)舊石丫/口勺小丫口丫土一聲與 Fi等價(jià)叫規(guī)則6. 設(shè)F| = 重，元i V比 ? V/，-3 V k-2 /i V比方一1, 時(shí)t V /、k-i V U F ，那么 Fe = （ l , M 1 V 衛(wèi) 2 +工2 V 至 3 3 1 至2至 V 工,土一丫心-iVi/ur與F等價(jià),.2）單子句排序

10、：效率高的分支限界算法要求有好的分支變元選擇策略和有效的沖突集檢測方法，本文采用的 是將變元的正負(fù)文字在一元子句集，二元子句集和三元子句集中出現(xiàn)次數(shù)之和作為該變元的 分?jǐn)?shù)，即：Score（x） = |C| 1 （x）+8*|C| 2 （x）+|C| 3 （x）+|C| 1 （又）+|C| 2 （又）+|C| 3 （x）3）進(jìn)一步失敗文字檢測：進(jìn)一步失敗文字檢測是在變元xi為真或?yàn)榧?，不能都產(chǎn)生空子句時(shí)，繼續(xù)向前一步檢測的方法.其原理下圖所示.進(jìn)一步失敗文字檢測原理如圖表示在進(jìn)行失敗文字檢測時(shí)，令xi=1進(jìn)行up可以產(chǎn)生空子句,xi=0進(jìn)行up未產(chǎn) 生空子句，失敗文字檢測尋找沖突集不成功.Maxsatz2013在由xi=0賦值簡化后的中，繼續(xù) 檢測變元xj，若xj=0和xj=1進(jìn)行up均產(chǎn)生了空子句，則從xi出發(fā)到3個(gè)空子句路徑上出現(xiàn) 的子句，構(gòu)成的集合是一個(gè)沖突集，下界加1.進(jìn)一步失敗文字因搜索空間大，所以計(jì)算成本高 且找到的沖突集規(guī)模大.但實(shí)驗(yàn)顯示進(jìn)一步失敗文字檢測仍有助于提高算法下界縮短運(yùn)行時(shí) 間.該函數(shù)表述如下：過程2. Furrher failed literal detectionfwr