不可滿足子式研究

殷明浩，李欣

(東北師范大學計算機科學與信息技術學院，吉林長春130117)

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

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

1 相關定義

在計算機科學領域，不可滿足子式的研究最初源于SAT問題，首先介紹本文涉及的相關概念.

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

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

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

對于一個公式φ，φ是φ的一個不可滿足子式，當且僅當φ是不可滿足的，且φ?φ.

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

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

對于一個不可滿足的公式φ的一個不可滿足子式φ，那么φ是極小不可滿足子式，當且僅當?φ∈φ，使得φ是可滿足的.

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

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

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

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

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

當且僅當φ是不可滿足的，并且從φ中移出任何一個子句將導致公式變為可滿足，一個QBF公式φ被稱為極小不滿足，不可滿足子式的子式可以表示為MF(minimal false formulas).

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

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

定義8 SMT不可滿足子式.

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

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

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

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

由一個變量集合和一個約束集合組成.問題的一個狀態是由對一些或全部變量的一個賦值定義的完全賦值:每個變量都參與的賦值.問題的解是滿足所有約束的完全賦值，或更進一步，使目標函數最大化.

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

一個極小CSP不可滿足子式，其約束的有關子集是不可滿足的，并且其真子集是可滿足的.

2 不可滿足子式求解算法

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

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

2.1 極小不可滿足子式求解

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

2.1.1 基于沖突樹的搜索算法

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

2.1.2OMUS 與 ASMUS 算法

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

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

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

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

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

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

2.1.5 基于關聯賦值的算法

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

2.2 最小不可滿足子式求解

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

2.2.1 基于輔助變量的算法

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

2.2.2 分支限界算法

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

2.2.3 貪心遺傳算法

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

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

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

2.3.1 Lemma－lifting 方式

Cimatti等[15－16]提出了求解 SMT 不可滿足子式的算法—Lemma－lifting 方式.Lemma－lifting 方 式將SMT求解器與外部命題核提取器結合起來，通過一種直接的方式求解SMT.SMT求解器保存并返回在證明公式不可滿足性的過程中獲得的特定理論引理.外部命題核提取器隨后調用原始SMT問題和特定理論引理的布爾抽象.算法是基于以下2個重要的觀察:1)在搜索過程中，SMT求解器發現的特定理論引理是在T理論中考慮的有效子句，因此它們不影響T中一個公式的可滿足性;2)原始SMT公式與特定理論引理的合取是命題不可滿足的.因此，當外部命題核提取器找到原始SMT公式與特定理論引理的合取的一個核時，應當刪除其中的特定理論引理，獲得一個精簡的原始公式的子集.雖然在原理上很簡單，但是該方式的概念很有趣，本質上講，SMT求解器動態地將理論信息適當地轉化為布爾標準.而且，該方式還有以下優點:1)易于實現與升級.由于SMT求解器與布爾不可滿足子式提取算法是相互獨立的，因此能夠將最新的求解器或算法進行組合，從而提高SMT不可滿足子式的求解效率;2)尋找較小的不可滿足子式非常有效;3)內核提取不需要復雜的SMT推理.但是，該算法有如下缺點:1)需要額外的存儲空間用來保存SMT求解器產生的引理;2)無法保證最終求得的不可滿足子式是極小不可滿子式.

2.3.2 基于DPLL構架求解算法

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

2.3.3 基于否正蘊涵圖的求解算法

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

3 不可滿足子式的復雜性

研究不可滿足子式的復雜性，對不可滿足子式算法的提出和改進有重大意義.

3.1 不可滿足子式的子類

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

Unique－SAT≈pUnique－MU≤pDis－MU

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

式中:≤p表示多項式時間可約.A≈pB是A≤pB，B≤pA的縮寫.

3.2 不可滿足子式參數復雜性

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

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

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

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

4 總結與展望

不可滿足子式的研究給研究人員帶了多方面的挑戰，但是也給研究人員帶來多方面機會.不可滿足子式的研究出現了以下研究方面的熱點.

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

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

3)新領域中擴展:在形式驗證等實際應用中，QBF、CSP、SMT都比SAT表達力強.尤其SMT技術得到飛速發展，并且在驗證領域獲得很好的效果.研究SMT的極小不可滿足子式將是未來主要方向.

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

[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.