殷明浩，李欣

(東北師范大學(xué)計(jì)算機(jī)科學(xué)與信息技術(shù)學(xué)院，吉林長(zhǎng)春130117)

可滿足性問題(satisfiability problem，SAT)是當(dāng)前人們研究得最多的約束可滿足性問題，也是當(dāng)今計(jì)算機(jī)科學(xué)和人工智能研究的核心問題.在實(shí)際應(yīng)用領(lǐng)域中的很多問題，例如等價(jià)性檢查、大規(guī)模集成電路的自動(dòng)布線、自動(dòng)測(cè)試向量生成、硬件與軟件的屬性驗(yàn)證等都可轉(zhuǎn)化為約束可滿足問題，即能夠歸約為一階邏輯公式或命題邏輯.然而，僅僅判斷命題邏輯的可滿足性是無法滿足實(shí)際要求的.當(dāng)公式不可滿足時(shí)，為了查找不可滿足的原因，往往要?jiǎng)h除無關(guān)子句進(jìn)而提取不可滿足子式.目前，研究人員對(duì)不可滿足子式的算法研究和相應(yīng)計(jì)算的復(fù)雜性表現(xiàn)出了極大興趣.尋找最小不可滿足子式的決策問題是問題[1]，尋找一個(gè)極小不可滿足子式是Dp－complete問題.目前有很多算法是關(guān)于極小[2－11]和最小不可滿足子式[12－14]的提取，這些提取不可滿足子式的算法主要應(yīng)用于形式驗(yàn)證領(lǐng)域.極小不可滿足子式可以更好地解釋不可滿足的根源所在，最小不可滿足子式可以精確地定位錯(cuò)誤原因，但是其求解難度極大.隨著SMT(satisfiability modulo theories)技術(shù)的不斷發(fā)展，它開始逐漸取代SAT.相對(duì)于SAT，SMT具有更好的抽象能力，更接近于高層設(shè)計(jì)，極具發(fā)展?jié)摿?它使用字級(jí)建模，不必像SAT那樣將問題轉(zhuǎn)化為位級(jí)處理，從而減少了空間和時(shí)間的開銷.SMT可以看作是SAT問題的一個(gè)擴(kuò)展，它極大地補(bǔ)充了SAT的不足之處.求解其極小不可滿足子式算法也極具實(shí)際意義.SMT技術(shù)是近幾年發(fā)展起來的，目前提取SMT中極小不可滿足子式的算法比較少.Cimatti[15－16]提出了一個(gè)新穎的方式lemma－Lift來提取 SMT極小不可滿足子式;張建民[17]提出了基于DPLL(T)的深度優(yōu)先搜索的極小SMT不可滿足子式求解算法 DFS－MUSE和寬度優(yōu)先搜索的極小SMT不可滿足子式的求解算法BFSMUSE.2010年，他又提出了基于沖突分析與否證蘊(yùn)含的極小 SMT不可滿足子式求解算法 CARIMUSE[18]，該算法的效果明顯好于 DFS－MUSE 算法，性能隨著時(shí)間復(fù)雜度的增加更加明顯.

研究不可滿足子式的復(fù)雜性對(duì)不可滿足子式求解算法也極具重大意義.H.K.Büning 和趙希順[19]對(duì)不可滿足的子類進(jìn)行了研究，介紹了各子類的特性，并在文獻(xiàn)中對(duì)子類的復(fù)雜性進(jìn)行了證明[20].H.Fleischne[21]、S.Szeide[22]將固定參數(shù)的概念與極小不可滿足子式中固定差值概念相關(guān)聯(lián)，證明了固定參數(shù)的極小不可滿足子式的計(jì)算復(fù)雜性.帶量詞的布爾公式QBF作SAT公式的自然擴(kuò)展具有緊湊的空間結(jié)構(gòu)以及更強(qiáng)大、更直觀的表達(dá)能力，對(duì)QBF中極小不可滿足子式的研究有利于探索新的QBF算法.趙希順[23]證明了QBF中，對(duì)QCNF公式固定差值為1的極小不可滿足子式可以在多項(xiàng)式時(shí)間內(nèi)有解.

1 相關(guān)定義

在計(jì)算機(jī)科學(xué)領(lǐng)域，不可滿足子式的研究最初源于SAT問題，首先介紹本文涉及的相關(guān)概念.

定義1 命題可滿足性問題.

給定一個(gè)CNF表達(dá)式F和一個(gè)變量集合{V=x1，x2，x3}.如果變量集合V中的一組賦值使得表達(dá)式F的值為真，那么稱表達(dá)式F是可滿足的;否則，表達(dá)式F為不可滿足.

定義2 不可滿足子式/不可滿足核(US/UC).

對(duì)于一個(gè)公式φ，φ是φ的一個(gè)不可滿足子式，當(dāng)且僅當(dāng)φ是不可滿足的，且φ?φ.

顯然，對(duì)于同一個(gè)問題實(shí)例，可能存在不同的不可滿足子式，每個(gè)不可滿足子式的子句數(shù)也可能不同.其中一些不可滿足子式可能是其他不可滿足子式的子集.在最壞情況下，不可滿足子式就是原始公式本身.

定義3 極小不可滿足子式.

對(duì)于一個(gè)不可滿足的公式φ的一個(gè)不可滿足子式φ，那么φ是極小不可滿足子式，當(dāng)且僅當(dāng)?φ∈φ，使得φ是可滿足的.

定義4 最小不可滿足子式.

給出一個(gè)不可滿足的公式φ以及φ的所有不可滿足子式構(gòu)成的集合 {φ1，φ2，…，φn}，如果 φk∈{φ1，φ2，…，φn}是最小不可滿子式，當(dāng)且僅當(dāng)使 得

定義5 量化布爾公式－QBF問題.

一個(gè) QCNF公式 φ=Q1x1Q2x2…Qnxnφ，其中Qi∈{?，?}，φ是一個(gè)CNF公式，用矩陣形式表達(dá) φ.x1，x2，…，xn分別被 Q1，Q2，…，Qn量化.有時(shí)，可以簡(jiǎn)寫為φ=Qφ.

定義6 QBF極小不可滿足子式(MF).

當(dāng)且僅當(dāng)φ是不可滿足的，并且從φ中移出任何一個(gè)子句將導(dǎo)致公式變?yōu)榭蓾M足，一個(gè)QBF公式φ被稱為極小不滿足，不可滿足子式的子式可以表示為MF(minimal false formulas).

定義7 可滿足性模理論(SMT).

SMT是SAT的一種擴(kuò)展，其命題不僅包括布爾公式，還包括其他特定理論中的一階邏輯約束，如整數(shù)與實(shí)數(shù)算術(shù)類型、位向量、遞歸及數(shù)據(jù)類型等.

定義8 SMT不可滿足子式.

給出一個(gè)不可滿足的無量詞一階邏輯公式φ，當(dāng)且僅當(dāng)φ是不可滿足的，并且φ?φ，φ是公式φ的一個(gè)SMT不可滿足子式.

定義9 極小SMT不可滿足子式.

給出不可滿足的無量詞一階邏輯公式φ，及其一個(gè)不可滿足子式φ，那么φ是極小SMT不可滿足子式，當(dāng)且僅當(dāng)?φ∈φ，使得φ是可滿足的.

定義10 約束可滿足問題(CSP).

由一個(gè)變量集合和一個(gè)約束集合組成.問題的一個(gè)狀態(tài)是由對(duì)一些或全部變量的一個(gè)賦值定義的完全賦值:每個(gè)變量都參與的賦值.問題的解是滿足所有約束的完全賦值，或更進(jìn)一步，使目標(biāo)函數(shù)最大化.

定義11 極小CSP不可滿足子式.

一個(gè)極小CSP不可滿足子式，其約束的有關(guān)子集是不可滿足的，并且其真子集是可滿足的.

2 不可滿足子式求解算法

按照問題的解決方式，求解布爾不可滿足子式的方法可劃分為基于DPLL搜索[2，4－6，12－14]與 局 部 搜索[7－11].通常來說 ，基于 DPLL 搜索方法能夠找到問題的精確解，但其面臨的主要挑戰(zhàn)是計(jì)算時(shí)間隨問題規(guī)模的增大呈指數(shù)級(jí)增長(zhǎng).而局部啟發(fā)式搜索盡管有時(shí)無法給出精確解，但其運(yùn)算速度快，求解效率高.

根據(jù)不可滿足子式的大小可以分為2類:1)極小不可滿足子式的提取算法[2－11];2)最小不可滿足子式的提取算法[12－14].相對(duì)而言，最小不可滿足子式的求解難度更大，算法的復(fù)雜度也更高.

2.1 極小不可滿足子式求解

當(dāng)前主流的不可滿足子式提取算法關(guān)于極小不可滿足子式的提取.形式驗(yàn)證與人工智能規(guī)劃問題均可轉(zhuǎn)為可滿足性問題，一組可滿足的賦值代表了一種可行方案;反之，說明原問題存在錯(cuò)誤，尋找不可滿足子式可以精確地對(duì)問題進(jìn)行定位.

2.1.1 基于沖突樹的搜索算法

Han和Lee[24]提出了一個(gè)獲得所有極小不可滿足子式的算法.該方法的思想是有序遍歷集合S的所有子集.它由2部分組成:1)用CS－tree(沖突樹)的不同結(jié)點(diǎn)表示集合S的不同子集，并且沒有哪2個(gè)結(jié)點(diǎn)表示相同的子集.CS－tree定義了子集間的遍歷順序，因此保證了同一子集不被重復(fù)搜索.為了實(shí)現(xiàn)這個(gè)目標(biāo)，一個(gè)結(jié)點(diǎn)由集合D和集合P 2部分組成，表示為D∪P.集合D的元素一定要出現(xiàn)在所有后續(xù)子集中，而集合P的元素不需要.如果一個(gè)結(jié)點(diǎn)有|P|個(gè)孩子，它由逐個(gè)消減集合P約束，并加入到集合D中獲得.函數(shù)all subsets(D，P，φ)遍歷CS－tree的所有結(jié)點(diǎn)，返回D∪X(X?P).當(dāng)?shù)L問一個(gè)根結(jié)點(diǎn)時(shí)，每次迭代以深度優(yōu)先方式遍歷CS－tree，并且每次內(nèi)部調(diào)用all subsets()函數(shù)訪問這個(gè)孩子結(jié)點(diǎn)的后代.2)利用CS－tree探測(cè)所有極小不可滿足子式.算法以深度優(yōu)先方式遍歷樹，測(cè)試每個(gè)結(jié)點(diǎn)的標(biāo)志D∪P，判斷其可滿足性.如果結(jié)點(diǎn)可滿足，那么就不必訪問它的孩子節(jié)點(diǎn).否則，繼續(xù)尋找孩子節(jié)點(diǎn)來尋找不可滿足子式.如果遍歷所有孩子結(jié)點(diǎn)沒有發(fā)現(xiàn)子集A使得A?D.那么集合D就是極小不可滿足集合.文獻(xiàn)[2]在以上基本算法中加入了預(yù)處理，利用約束獨(dú)立性、利用始終滿足的子句、蘊(yùn)涵、廉價(jià)求解器、增量式求解器、無視約束等策略.其中，使用增量式求解器極大地改進(jìn)了算法，它減少了對(duì)算法規(guī)則的依賴性，能夠快速地發(fā)現(xiàn)可滿足子集.

2.1.2OMUS 與 ASMUS 算法

文獻(xiàn)[14]中，é.Grégoire提出了基于啟發(fā)式局部搜索算法OMUS.OMUS算法是通過計(jì)算關(guān)鍵子句分值來獲得一個(gè)極小不可滿足子式的啟發(fā)式算法.算法主要分為2部分:1)在局部算法中根據(jù)子句布爾值為假的頻度計(jì)算子句的分值，移除確定不可能出現(xiàn)在不可滿足子式中的子句.具體來說，對(duì)于一個(gè)不可滿足子式，如果在局部搜索時(shí)終未能找到它的一個(gè)賦值模型，那么將移除子式中分值最低的子句.獲得的子公式將被記錄在堆棧中.2)檢查最后一個(gè)未能賦值的子式是否可滿足，如果子公式是不可滿足的，那么它就是不可滿足子式的近似解.否則，重復(fù)檢查棧頂子句超集的不可滿足性，直到一個(gè)集合被證明是不可滿足的.該過程將獲得一個(gè)近似的極小不可滿足子式.然后，調(diào)用一個(gè)精細(xì)調(diào)節(jié)(fine tunes)過程，OMUS算法最終獲得一個(gè)不可滿足子式.

é.Grégoire在文獻(xiàn)[8]中提出了 ASMUS算法.ASMUS以O(shè)MUS為基礎(chǔ)，可以近似求解所有不可滿足子式的集合.MAX－SAT可以提供極小的不可滿足子式數(shù)量.MAX－SAT解中的剩余不可滿足子句一定盡可能多地屬于那些不可滿足子式的交集.那么對(duì)于每個(gè)子句，記錄最小的子句數(shù).在探測(cè)到一個(gè)不可滿足子式后，把不可滿足子式中分值最高的子句刪除掉.很顯然，ASMUS是不完全的.

2.1.3 基于消解反駁的局部搜索算法

局部搜索是一種求解優(yōu)化問題的算法，算法從解空間的一個(gè)點(diǎn)出發(fā)，每一步從當(dāng)前候選解移動(dòng)到一個(gè)鄰居候選解，去尋找較好的候選解，候選解的質(zhì)量是由一個(gè)評(píng)估函數(shù)來界定的.局部搜索算法在處理規(guī)模較大的問題時(shí)，其收斂速度快，求解效率高.上文提到的OMUS與ASMUS實(shí)質(zhì)上是啟發(fā)式局部搜索與計(jì)數(shù)的組合.消解是判定SAT問題的基本方法之一.一個(gè)公式經(jīng)過一系列的消解步驟最終產(chǎn)生空子句，則公式是不可滿足的.文獻(xiàn)[9－11]中采用局部搜索方法作為解空間的搜索策略.算法在搜索過程中建立證明公式不可滿足性的消解序列，并從其中提取不可滿足子式.算法描述如下:算法啟發(fā)式或隨機(jī)地選擇2個(gè)子句進(jìn)行消解，最終得到一個(gè)消解序列或達(dá)到最大迭代次數(shù).搜索過程融合了一些基于啟發(fā)式的SAT推理技術(shù)，包括二元子句消解、等價(jià)約簡(jiǎn)和單元子句傳播.算法首先尋找公式中是否存在單元子句，如果存在，則在公式上進(jìn)行單元子句傳播，并進(jìn)一步判斷能否產(chǎn)生空子句;如果存在二元子句，則執(zhí)行二元子句消解與等價(jià)性約簡(jiǎn)，啟發(fā)式地選擇消解子句.若2類子句都不存在，則隨機(jī)選取2個(gè)子句進(jìn)行消解.最后采用一個(gè)遞歸函數(shù)從空子句開始回溯，逐步遍歷整個(gè)消解序列，提取布爾不可滿足子式.

2.1.4 基于最大可滿足性的求解算法

目前，有很多研究人員利用極大可滿足性和極小不可滿足性之間的二元關(guān)系提取極小不可滿足子式.Bailey和Stuckey在文獻(xiàn)[25]中已經(jīng)闡述了這種關(guān)系.基于最大可滿足性的 CAMUS[4]，Digger[13]能夠提取極小不可滿足子式;貪心遺傳算法和蟻群算法[14]能夠提取最小不可滿足子式.文獻(xiàn)[26]中提出了一種在CSP中提取極小不可滿足子式的混合算法.該算法也是基于最大可滿足性求解極小不可滿足子式.求解CSP極小不可滿足子式的算法一般分為直接算法和間接算法.間接算法利用極小不可滿足子式和極小修正集(MCS)之間的關(guān)系.算法主要是尋找一個(gè)完全的極小修正集，然后從中提取極小不可滿足子式.另一方面，直接算法通過產(chǎn)生子集和測(cè)試其可滿足性直接地在CSPs約束的子集空間搜索不可滿足子式.混合算法融合了直接和間接方法.混合算法像間接算法那樣不再計(jì)算全部的極小修正集，而是尋找極小修正集中較小的子集.這就是所謂的“主干”集合，即極小修正子集發(fā)現(xiàn)的不可消減的碰集.每個(gè)主干集表示不可滿足子式的一個(gè)簇.通過直接方法搜索主干的超級(jí)空間，這些主干集隨后逐個(gè)被擴(kuò)展為完全的不可滿足子式.實(shí)驗(yàn)表明，基于最大可滿足性的混合算法比單純直接算法或間接算法效率高很多.混合算法通過在每步中搜索一個(gè)較小的空間提高效率.

2.1.5 基于關(guān)聯(lián)賦值的算法

文獻(xiàn)[27]中算法提出了關(guān)聯(lián)賦值的概念，將賦值與子句聯(lián)系起來.關(guān)聯(lián)賦值的概念來自于布勞威爾不動(dòng)點(diǎn)近似算法在可滿足性問題方面的應(yīng)用.它將子句視為實(shí)體，也就是一個(gè)有序的賦值集合，并且從可能的賦值中選擇一個(gè)賦值與其關(guān)聯(lián).這些賦值形成一個(gè)完整的序列，在序列中優(yōu)先選擇所有可滿足賦值，再選擇所有不可滿足賦值.當(dāng)達(dá)到帕累托最優(yōu)后，有可能找到這些子句的一個(gè)子集來表示不可滿足性.在帕累托最優(yōu)中，所有子句已經(jīng)選擇了一個(gè)惟一的不滿足自己的賦值.帕累托最優(yōu)證明了子句的選擇權(quán)與不可滿足公式之間的沖突.當(dāng)子句證明了公式的不可滿足性后，利用文獻(xiàn)[27]中的理論去實(shí)現(xiàn)算法，尋找一個(gè)不可滿足子式.然而這種算法的效率并不高，文獻(xiàn)[12]中提出了一個(gè)簡(jiǎn)單有效的極小不可滿足子式抽取算法MiniUnsat.MiniUnsat中包含了一個(gè)高效率SAT求解器MiniSat 2.0.為了進(jìn)一步提高效率，在MiniSat的分支選擇中加入了啟發(fā)式策略.當(dāng)每個(gè)變量決策時(shí)，MiniSat的分支默認(rèn)選擇賦值為負(fù)值的一支.在算法的第1輪中，并不發(fā)生任何變化.第1輪之后，每個(gè)尚未刪除的子句都在前1輪中有了一個(gè)關(guān)聯(lián)賦值.除了新的關(guān)鍵子句移動(dòng)到這個(gè)賦值的前面，隨后的子句仍將保持同樣的順序.程序因此確定了變量的分支方向，這將引導(dǎo)求解器按著以前關(guān)聯(lián)賦值的方向?qū)ふ倚碌馁x值.

2.2 最小不可滿足子式求解

不可滿足子式反應(yīng)了問題的存在.最小不可滿足子式比極小不可滿足子式更能精確地定位錯(cuò)誤.研究最小不可滿足算法，也是研究人員的最終目的.目前關(guān)于最小不可滿足子式的提取研究還相對(duì)較少.

2.2.1 基于輔助變量的算法

算法 AMUSE[3]和文獻(xiàn)[12]中算法通過引入一組輔助變量求解不可滿足子式.AMUSE是對(duì)一個(gè)基于DPLL構(gòu)架的SAT求解器的擴(kuò)展.它不再尋找一個(gè)可滿足的真值賦值而是尋找其中蘊(yùn)含的不可滿足子式.為此引入了一組輔助變量，通過自底向上的方式搜索不可滿足樹的空間:從一個(gè)空子句開始，逐步添加子句，直到獲得一個(gè)不可滿足子式.為了改善搜索效率，其中使用了沖突子句學(xué)習(xí)優(yōu)化策略.但是AMUSE算法無法保證獲得極小不可滿足子式，尤其隨著問題規(guī)模的擴(kuò)大，效率會(huì)明顯下降.文獻(xiàn)[6]中提出了一個(gè)獲得最小不可滿足子式的模型:是由子句ωi與選擇變量si構(gòu)成.選擇變量si決定是否選擇子句ωi.對(duì)每個(gè)S中變量賦值，產(chǎn)生的子式可能是滿足的，也可能是不滿足的.對(duì)于不可滿足的子式，S中有多少變量賦值為1，就意味著有多少子句包含在不可滿足子式里.那么最小不可滿足子式就是S集合中賦值為1的、數(shù)量最少的子公式.通?？梢允褂酶咝У那蠼馄鱽韺?shí)現(xiàn)這個(gè)模型.公式中變量被組織成2個(gè)互斥的集合:變量集合S和變量集合X.首先決策變量S，然后決策變量X.因此每次變量S賦值，都定義了一個(gè)潛在的子式.如果對(duì)于一個(gè)賦值，所有的子句都滿足，那么回溯到最近未決策的變量S.否則，每次回溯要先改變X賦值，再改變S賦值，直到?jīng)]有變量X的賦值可以改變，則S中賦值為1最少的，就是最小不可滿足子式.

2.2.2 分支限界算法

文獻(xiàn)中[13]中 CAMUS－min和 Digger都是基于分支限界的算法.CAMUS－min算法是 CAMUS的改進(jìn)，它比CAMUS多了分支限界過程.CAMUS利用極大可滿足性和極小不可滿足性之間的二元關(guān)系提取極小不可滿足子式，一般分為2步:1)獲得公式中有所極大可滿足子式的補(bǔ)集;2)通過在遞歸樹中尋找補(bǔ)集的極小碰集來提取極小不可滿足子式.CAMUS－min與CAMUS不同之處在第2步，不直接尋找極小碰集，而在遞歸中增加了分支限界功能來減小樹的搜空間，產(chǎn)生最小的碰集.CAMUS－min中，一個(gè)貪婪的啟發(fā)式策略MIS－quick為算法提供下界，如果遞歸樹所包含的不可滿足子式?jīng)]有當(dāng)前不可滿足子式小，CAMUS－min刪除遞歸樹中的這些分支，因此運(yùn)行時(shí)間大幅減少，并且最后的不可滿足子式一定是最小不可滿足子式.Digger使用一個(gè)遞歸的分支限界樹來獲得最小不可滿足子式.樹中的每個(gè)結(jié)點(diǎn)都是原始公式的一個(gè)子集，并且上下界由子集中的最小不可滿足子式限定.因此算法在根結(jié)點(diǎn)處啟動(dòng)遞歸調(diào)用.Digger不同于標(biāo)準(zhǔn)的分支限界樹，不光遍歷葉子結(jié)點(diǎn)，也遍歷包括根結(jié)點(diǎn)的所有結(jié)點(diǎn).對(duì)于每個(gè)結(jié)點(diǎn)，算法利用不相交的極小修正集，啟發(fā)式選擇子句的一個(gè)樣本集，這不同于CAMUS－min中尋找全部極小修正集.實(shí)質(zhì)上，Digger利用不相交的極小修正集關(guān)系將一個(gè)問題分解為更容易處理的子公式，同時(shí)在搜索最小不可滿足子式過程中提供了一個(gè)非常有效的下界.

2.2.3 貪心遺傳算法

貪心遺傳算法[14]可以視為貪心算法與遺傳算法的混合算法.貪心算法是指在對(duì)問題求解時(shí)，總是做出在當(dāng)前看來是最好的選擇.也就是說，不從整體最優(yōu)上加以考慮，它所做出的僅是在某種意義上的局部最優(yōu)解.遺傳算法(genetic algorithm)是一類借鑒生物界的進(jìn)化規(guī)律演化而來的隨機(jī)化搜索方法.它由美國(guó)的J.Holland教授于1975年首先提出，其主要特點(diǎn)是直接對(duì)結(jié)構(gòu)對(duì)象進(jìn)行操作，不存在求導(dǎo)和函數(shù)連續(xù)性的限定;具有內(nèi)在的隱并行性和更好的全局尋優(yōu)能力;采用概率化的尋優(yōu)方法，能自動(dòng)獲取和指導(dǎo)優(yōu)化的搜索空間，自適應(yīng)地調(diào)整搜索方向，不需要確定規(guī)則.遺傳算法是全局進(jìn)化方法，可以避免進(jìn)入局部最優(yōu)，但是在初期缺乏充分有效啟發(fā)信息的情況下局部收斂速度較慢，并且對(duì)初始種群十分依賴.所以將貪心算法與遺傳算法有效地結(jié)合起來，保留了2種算法的優(yōu)點(diǎn)，極大地避免了2種算法的不足.貪心遺傳算法的基本策略是:首先采用貪心算法快速計(jì)算不可滿足子式的近似最優(yōu)解，為遺傳算法構(gòu)造一個(gè)較優(yōu)的初始種群，縮減其搜索空間，而后利用遺傳算法的全局性反復(fù)精化近似解，從而得到更小的不可滿足子式.實(shí)驗(yàn)結(jié)果表明，在運(yùn)算效率以及單位時(shí)間內(nèi)刪除的短句數(shù)方面，顯著高于分支限界算法，而貪心遺傳算法無論在運(yùn)行時(shí)間還是不可滿足子式的大小上都優(yōu)于蟻群算法.

2.3 SMT中不可滿足子式求解算法

隨著SMT技術(shù)的不斷發(fā)展，它開始逐漸取代SAT.SMT具有更好的抽象能力，更接近于高層設(shè)計(jì)，極其具有發(fā)展?jié)摿?它使用字級(jí)建模，不必像SAT中將問題轉(zhuǎn)化為位級(jí)處理，從而減少了空間和時(shí)間的開銷.SMT可以看做是SAT問題的一個(gè)擴(kuò)展，它極大地補(bǔ)充了SAT的不足之處.求解其極小不可滿足子式算法也是非常具有實(shí)際意義的.SMT技術(shù)是近幾年發(fā)展起來的，目前提取SMT中極小不可滿足子式的算法比較少.

2.3.1 Lemma－lifting 方式

Cimatti等[15－16]提出了求解 SMT 不可滿足子式的算法—Lemma－lifting 方式.Lemma－lifting 方 式將SMT求解器與外部命題核提取器結(jié)合起來，通過一種直接的方式求解SMT.SMT求解器保存并返回在證明公式不可滿足性的過程中獲得的特定理論引理.外部命題核提取器隨后調(diào)用原始SMT問題和特定理論引理的布爾抽象.算法是基于以下2個(gè)重要的觀察:1)在搜索過程中，SMT求解器發(fā)現(xiàn)的特定理論引理是在T理論中考慮的有效子句，因此它們不影響T中一個(gè)公式的可滿足性;2)原始SMT公式與特定理論引理的合取是命題不可滿足的.因此，當(dāng)外部命題核提取器找到原始SMT公式與特定理論引理的合取的一個(gè)核時(shí)，應(yīng)當(dāng)刪除其中的特定理論引理，獲得一個(gè)精簡(jiǎn)的原始公式的子集.雖然在原理上很簡(jiǎn)單，但是該方式的概念很有趣，本質(zhì)上講，SMT求解器動(dòng)態(tài)地將理論信息適當(dāng)?shù)剞D(zhuǎn)化為布爾標(biāo)準(zhǔn).而且，該方式還有以下優(yōu)點(diǎn):1)易于實(shí)現(xiàn)與升級(jí).由于SMT求解器與布爾不可滿足子式提取算法是相互獨(dú)立的，因此能夠?qū)⒆钚碌那蠼馄骰蛩惴ㄟM(jìn)行組合，從而提高SMT不可滿足子式的求解效率;2)尋找較小的不可滿足子式非常有效;3)內(nèi)核提取不需要復(fù)雜的SMT推理.但是，該算法有如下缺點(diǎn):1)需要額外的存儲(chǔ)空間用來保存SMT求解器產(chǎn)生的引理;2)無法保證最終求得的不可滿足子式是極小不可滿子式.

2.3.2 基于DPLL構(gòu)架求解算法

DPLL是一種基于回溯的算法，在成熟運(yùn)用于SAT求解器后，基于DPLL(T)的SMT求解技術(shù)也得到飛速發(fā)展.DPLL(T)由布爾引擎DPLL(X)與特定的理論求解器 T－slover組成.文獻(xiàn)[16－17]就是基于DPLL(T)構(gòu)架求解不可滿足子式.文獻(xiàn)[17]提出了深度優(yōu)先方式的極小不可滿足子式算法(DFS－MUSE)和深度優(yōu)先方式的極小不可滿足子式算法(BFS－MUSE).這2個(gè)算法從不可滿足子式中刪除任意一個(gè)子句，然后測(cè)試其余子句構(gòu)成公式的可滿足性，從而判斷是否為極小不可滿足子式;而不必測(cè)試不可滿足子式所有的真子式，將復(fù)雜度從指數(shù)降為線性.算法中也融合了剪枝技術(shù)、沖突子句學(xué)習(xí)技術(shù)用于剔除不必要的冗余不可滿足性測(cè)試，從而縮小了搜索空間，提高了搜索效率.算法中也融合了動(dòng)態(tài)排序技術(shù)，降低了剛測(cè)試過子句的優(yōu)先級(jí)，避免重復(fù)測(cè)試.DFS－MUSE的一個(gè)重要特點(diǎn)是:當(dāng)選擇搜索樹中不同的分支，會(huì)得到不同的極小SMT不可滿足子式.BFS－MUSE 與 DFS－MUSE 的區(qū)別在于搜索策略不同.BFS－MUSE是以寬度優(yōu)先的方式對(duì)搜索樹進(jìn)行遍歷，首先考慮同樣大小的子式的可滿足性，然后再考慮較小的子式.DFS－MUSE是以深度優(yōu)先的方式對(duì)搜索樹進(jìn)行遍歷，先對(duì)當(dāng)前子樹內(nèi)子式的可滿足性測(cè)試，找出最小的子式，然后再測(cè)試其他子樹的可滿足性.

2.3.3 基于否正蘊(yùn)涵圖的求解算法

文獻(xiàn)[18]中提出了基于否正蘊(yùn)涵與沖突分析提取SMT中極小不可滿足子式的算法CARI－MUSE.否證蘊(yùn)含圖是指對(duì)一個(gè)不可滿足的SMT子式及其子句蘊(yùn)含圖，從該蘊(yùn)含圖的每個(gè)子句出發(fā)，至少存在一條路徑可以達(dá)到空子句.否證蘊(yùn)含圖與不可滿足子式存在以下密切關(guān)系:對(duì)于不可滿足公式F的一個(gè)消解反駁R和R對(duì)應(yīng)的否證蘊(yùn)含圖G，那么G中逆向可達(dá)結(jié)點(diǎn)集合與公式F的交集就是F的一個(gè)不可滿足子式.CARI－MUSE算法以上述結(jié)論為依據(jù)，利用SMT求解器記錄在證明公式不可滿足性的過程中產(chǎn)生的消解反駁序列，并將其轉(zhuǎn)化為否證蘊(yùn)含圖，提取出不可滿足子式.為了進(jìn)一步獲得極小不可滿足子式，依次刪除蘊(yùn)含圖中原始子句及其相關(guān)的沖突短句，調(diào)用SMT求解器來判斷否證蘊(yùn)涵圖的剩余子公式(結(jié)點(diǎn))的可滿足性，以確定該子句是否為不可滿足的原因;如果剩余子公式是可滿足的，說明公式已經(jīng)是極小不可滿足子式;否則，從否證蘊(yùn)含圖中刪除該子句及其沖突短句，形成更小的否證蘊(yùn)含圖;算法迭代的遍歷否證蘊(yùn)含圖中所有原始子句，最后得到極小SMT不可滿足子式.為了提高搜索效率，算法中集成了蘊(yùn)含圖剪枝技術(shù)，減小了算法的搜索空間.實(shí)驗(yàn)結(jié)果表明，CARI－MUSE算法的效率明顯高于求解極小不可滿足子式的深度優(yōu)先搜索算法DFS－MUSE;并且隨著公式復(fù)雜度的增加，性能優(yōu)勢(shì)更加明顯.

3 不可滿足子式的復(fù)雜性

研究不可滿足子式的復(fù)雜性，對(duì)不可滿足子式算法的提出和改進(jìn)有重大意義.

3.1 不可滿足子式的子類

研究人員對(duì)不可滿足子式的子類感興趣有以下原因:1)有利于發(fā)展新的可滿足性算法，例如，對(duì)極小不可滿足子式結(jié)構(gòu)的深入了解，可能會(huì)改進(jìn)DP算法;2)可能有助于求解難度大的公式.例如利用差值特性產(chǎn)生新的多項(xiàng)式時(shí)間可解的公式類[28];3)不可滿足子式的決策問題是Dp－complete，但是不可滿足子式的一些子類的復(fù)雜性可能相對(duì)容易.Bü NING H K 和趙希順[19－20]將不可滿足子式進(jìn)行分類研究，并討論了這些子類的復(fù)雜性.MARG－MU類是指，如果一個(gè)極小不可滿足子式是臨界類，那么移除任意一個(gè)文字事件，將導(dǎo)致公式成為非極小不可滿足子式.也就是說 MARG－MU類中沒有多余文字.MAX－MU類由最大的極小不可滿足子式構(gòu)成，即公式中再加入一個(gè)文字將不再是極小不可滿足子式.Unique－SAT指公式在移除任意一個(gè)子句后，只有一個(gè)可滿足的真值分配.帶有這種性質(zhì)的極小不可滿足子式，就是 Unique－MU 類.Almost－Unique－MU 類，是Unique－MU較小的改進(jìn)，即至多有一個(gè)子句f∈F，使得F－{f}有多于一個(gè)可滿足的真值分配.Dis－MU類指一個(gè)極小不可滿足子式F可以分裂為2個(gè)獨(dú)立的公式G與H，且公式G與H中不再包含互補(bǔ)文字.目前一些證據(jù)[29]表明 Unique－SAT 不是 Dpcomplete的，那么 Unique－MU也不太可能是 Dpcomplete.Almost－Unique－MU 要比 Unique－MU 復(fù)雜，因?yàn)槲闹凶C明了它是 Dp－complete.但是未能找到Dis－MU 歸約到 Unique－SAT 方法.文獻(xiàn)[20]中證明了以下層次結(jié)構(gòu):

Unique－SAT≈pUnique－MU≤pDis－MU

MU≈pMARG－MU≤pMAX－MU≈pAlmost－U－nique－MU

式中:≤p表示多項(xiàng)式時(shí)間可約.A≈pB是A≤pB，B≤pA的縮寫.

3.2 不可滿足子式參數(shù)復(fù)雜性

Downey和Fellows提出了一種解決NP難問題的新的研究方法，即很多難解和無法判定的問題通過引入?yún)?shù)可以得到時(shí)間復(fù)雜度為O(f(k)·nα)的固定參數(shù)可解(FTP)方法.極小不可滿足子式也可以參數(shù)化，通常用MU(k)(k≥1)表示固定差值為k的極小不可滿足子式.參數(shù)k是子句數(shù)減去變量數(shù)的差值.文獻(xiàn)[21]中提出了一個(gè)多項(xiàng)式時(shí)間算法來判斷一個(gè)公式是否屬于MU(k).因?yàn)槠涫褂昧恕氨闅v全部k個(gè)子集”的策略，所以算法非常依賴參數(shù)k.H.Fleischne等利用雙邊圖匹配的某些相應(yīng)賦值限制尋找一個(gè)可滿足的真值賦值.算法的時(shí)間復(fù)雜度為nO(k)，精確上界O(ln k+1/2).(l為公式長(zhǎng)度，n為公式的變量數(shù)).S.Szeide[22]提出了一個(gè)算法，并得到一個(gè)新的結(jié)果.算法產(chǎn)生于SAT問題的固定參數(shù)可解問題:對(duì)于一個(gè)CNF公式F，如果其子集中子句個(gè)數(shù)超過變量個(gè)數(shù)最多 k個(gè)，那么可以在O(2kn3)時(shí)間內(nèi)判斷公式F的可滿足性.參數(shù)k就是F的最大差值，可以用圖匹配算法有效計(jì)算.最后，基于以上結(jié)論，利用圖論中的最大差值和q－expanding雙邊圖[30]計(jì)算出改進(jìn)的結(jié)果為O(2kn4).

3.3 QBF中的極小不可滿足子式

近年來，SAT技術(shù)已經(jīng)成功應(yīng)用在限界模型檢驗(yàn)(bounded model checking，BMC)并推廣到限界的模型檢驗(yàn).但是直接將基于SAT的BMC推廣到非限界的模型檢驗(yàn)的方法不能克服軟件規(guī)模增大導(dǎo)致的狀態(tài)空間爆炸問題，即模型檢驗(yàn)過程中軟件規(guī)模的增大可能導(dǎo)致命題邏輯公式的長(zhǎng)度呈指數(shù)倍的增長(zhǎng).帶量詞的布爾公式QBF作為SAT公式的自然擴(kuò)展具有緊湊的空間結(jié)構(gòu)和更強(qiáng)大、更直觀的表達(dá)能力.

趙希順等[23]對(duì) QBF中的極小不可滿足問題(minimal falsity，MF)進(jìn)行了研究.對(duì)不可滿足的子式研究，有可能產(chǎn)生新的QBF求解算法.QBF的最小不可滿足公式QCNF指的是該公式不可滿足但其任一真子公式均可滿足.一個(gè)QCNF公式的差值不同于命題公式的差值，其差值是子句數(shù)和存在量詞之間的差值.對(duì)QCNF公式固定差值為1的極小不可滿足子式可表示為MF(1).文獻(xiàn)[23]中得出重要結(jié)論:對(duì)QCNF公式固定差值為1的極小不可滿足子式可以在多項(xiàng)式時(shí)間有解.這個(gè)證明依賴于公式MU(1)的結(jié)構(gòu).對(duì)于MF(k)(k≥2)是否存在多項(xiàng)式時(shí)間可解，仍然是開放的.

4 總結(jié)與展望

不可滿足子式的研究給研究人員帶了多方面的挑戰(zhàn)，但是也給研究人員帶來多方面機(jī)會(huì).不可滿足子式的研究出現(xiàn)了以下研究方面的熱點(diǎn).

1)使用符號(hào)化技術(shù)，如BDD技術(shù)能夠緊湊地表示公式，是緩解內(nèi)存瓶頸的關(guān)鍵技術(shù).文獻(xiàn)[31]借助于BDD判斷公式是不可滿足的并且其全部子公式是滿足的，從而證明公式是極小不可滿足子式.

2)混合求解算法:每種求解策略有其自身優(yōu)點(diǎn)和缺點(diǎn).混合求解有利于發(fā)揮各自算法的優(yōu)勢(shì)，避免其缺點(diǎn)，盡可能提高算法的效率.例如文獻(xiàn)[26]中提出了一種在CSP中提取極小不可滿足子式的混合算法，這是直接算法和間接算法的混合.文獻(xiàn)[14]求解最小不可滿足子式可以視為貪心算法與遺傳算法的混合算法.

3)新領(lǐng)域中擴(kuò)展:在形式驗(yàn)證等實(shí)際應(yīng)用中，QBF、CSP、SMT都比SAT表達(dá)力強(qiáng).尤其SMT技術(shù)得到飛速發(fā)展，并且在驗(yàn)證領(lǐng)域獲得很好的效果.研究SMT的極小不可滿足子式將是未來主要方向.

4)參數(shù)復(fù)雜性:將固定差值的極小不可滿足子式轉(zhuǎn)化為固定參數(shù)問題，并且求解其計(jì)算復(fù)雜性.但是，對(duì)于QBF中，MF(k)(k＞1)是否可以在多項(xiàng)式時(shí)間內(nèi)判定，依然是開放的.

[1]GUPTA A.Learning abstractions for model checking[D].Pittsburgh:Carnegie Mellon University，2006:1－180.

[2]De La BANDA M G，STUCKEY P J，WAZNY J.Finding all minimal unsatisfiable subsets[C]//Proceedings of the 5th ACM SIGPLAN International Conference on Principles and Practice of Declaritive Programming.New York，USA，2003:32－43.

[3]OH Y，MNEIMNEH M N，ANDRAUS Z S.AMUSE:a minimally unsatisfiable subformula extractor[C]//Proceedings of the 41st Annual Design Automation Conference.New York，USA，2004:518－523.

[4]LIFFITON M，SAKALLAH K.On finding all minimally unsatisfiable subformulas[C]//Theory and Applications of Satisfiability Testing.St.Andrews，Scotland，2005:173－186.

[5]MARQUES－SILVA J，LYNCE I.On improving MUS extraction algorithms[M]//Lecture Notes in Computer Science，Heidelberg:Springer，2011，6695:159－173.

[6]Van MAAREN H，WIERINGA S.Finding guaranteed MUSes fast[M].Heidelberg:Springer，2008:291－304.

[7]GRéGOIRE é，MAZURE B，PIETTE C.Extracting MUSes[C]//Proceedings of the 17th European Conference on Artificial Intelligence 2006.Riva del Garda，Italy，2006:387－391.

[8]GRéGOIRE é，MAZURE B，PIETTE C.Local－search extraction of MUSes[J].Constrain，2007，12(3):325－344.

[9]ZHANG J，SHEN S，LI S.Finding unsatisfiable subformulas with stochastic method[M].Heidelberg:Springer，2007，4881:385－394.

[10]ZHANG J，SHEN S，LI S.A heuristic local search algorithm for unsatisfiable cores extraction[M].Heidelberg:Springer，2007，4707:649－659.

[11]ZHANG J，SHEN S，LI S.Tracking unsatisfiable subformulas from reduced refutation proof[J].Journal of Software，2009，4(1):42－49.

[12]LYNCE I，MARQUES－SILVA J P.On computing minimum unsatisfiable cores[C]//International Symposium on Theo－ry and Applications of Satisfiability Testing.Vancouver，Canada，2004:305－310.

[13]LIFFITON M，MNEIMNEH M，LYNCE I，et al.A branch and bound algorithm for extracting smallest minimal unsatisfiable subformulas[J].Constraints，2009，14(4):415－442.

[14]ZHANG Jianmin，SHEN Shengyu，LI Sikun.Algorithms for deriving minimum unsatisfiable Boolean subformulae[J].Acta Electronica Sinica，2009，37(5):993－999.

[15]CIMATTI A，GRIGGIO A，SEBASTIANI R.A simple and flexible way of computing small unsatisfiable cores in SAT modulo theories[M].Heidelberg:Springer，2007，4501:334－339.

[16]CIMATTI A，GRIGGIO A，SEBASTIANI R.Computing small unsatisfiable cores in satisfiability modulo theories[J].Journal of Artificial Intelligence Research，2011，40:701－728.

[17]ZHANG Jianmin，SHEN Shengyu，ZHANG Jun，et al.Extracting minimal unsatisfiable subformulas in satisfiability modulo theories[J].Computer Science and Information Systems，2011，8:693－710.

[18]ZHANG Jianmin，SHEN Shengyu，LI Sikun.An algorithm for extracting minimal unsatisfiable subformulae in first－order logic based on refutation implication[J].Chinese Journal of Conputers，2010，33(3):415－426.

[19]Bü NING H K，ZHAO X.On the structure of some classes of minimal unsatisfiable formulas[J].Discrete Applied Mathematics，2003，130(2):185－207.

[20]Bü NING H K，ZHAO X.The complexity of some subclasses of minimal unsatisable formulas[J].Journal on Satisfiability Boolean Modeling and Computation，2007，3:1－17.

[21]FLEISCHNER H，KULLMANN O，SZEIDER S.Polynomial－time recognition of minimal unsatisable formulas with fxed clause－variable difference[J].Theoretical Computer Science，2002，289(1):503－516.

[22]SZEIDER S.Minimal unsatisable formulas with bounded clause－variable difference are fixed－parameter tractable[M].Heidelberg:Springer，2003:548－558.

[23]Bü NING H，ZHAO X.Minimal false quantified Boolean formulas[M].Heidelberg:Springer，2006:339－352.

[24]HAN B，LEE S J.Deriving minimal conflict sets by CS－trees with mark set in diagnosis from first principles[J].IEEE Transactions on Systems，Man，and Cybernetics，1999，29(2):281－286.

[25]BAILEY J，STUCKEY P J.Discovery of minimal unsatisfiable subsets of constraints using hitting set dualization[M].Heidelberg:Springer，2005:174－186.

[26]SHAH I.A hybrid algorithm for finding minimal unsatisfiable subsets in over－constrained CSPs[J].International Journal of Intelligent Systems，2011，26(11):1023－1048.

[27]Van MAAREN H.Pivoting algorithms based on Boolean vector labeling[J].Acta Mathematica Vietnamica，1997，22(1):183－198.

[28]DAVYDOV G，DAVYDOVA I，BüNING H K.An efficient algorithm for the minimal unsatisfiability problem for a subclass of CNF[J].Annals of Mathematics and Artificial Intelligence，1998，23:229－245.

[29]TORAN J.Complexity classes defined by counting quantifiers[J].Journal of the ACM，1991，38(3):753－774.

[30]LOVASZ L，PLUMMER M D.Matching theory[M].Amsterdam:North－Holland Publishing，1986:29.

[31]HUANG J P.MUP:a minimally unsatisfiability prover[C]//Proceedings of the 10th Asia and South Pacific Design Automation Conference.Shanghai， China， 2005:432－437.