基于不可滿足原因的最小糾正集求解*

胡瀟灑，張?jiān)綆X，李建文，蒲戈光，張 敏

(華東師范大學(xué)計(jì)算機(jī)科學(xué)與軟件工程學(xué)院，上海 200062)

1 引言

最小糾正集MCS(Minimal Correction Subset)是約束的集合。對于一個(gè)約束求解問題，MCS是其約束的子集。在布爾可滿足性判定問題中，MCS是原公式的子集。與計(jì)算不可滿足公式的最大不可滿足的核MUC(Maximal UNSAT Core)類似，計(jì)算不可滿足公式的MCS也是 NP-難問題[1]。MCS和MUC互為擊中集(Hitting Set)問題[2]，因此可以通過計(jì)算MCS找到不可滿足公式的MUC[3,4]。MCS還可以用于求解MaxSAT問題，通過多次計(jì)算MCS得到最大可滿足子集SS(Maximal Satisfiable Subset)的集合，進(jìn)而找到MaxSAT。對于可滿足的公式，MCS也能夠幫助其計(jì)算最大(小)的可滿足解[5]。

在實(shí)際問題中，MCS也有著相應(yīng)的應(yīng)用[6,7]。由于MCS具有識(shí)別不可滿足約束的最小原因的功能，能夠幫助自動(dòng)分析軟硬件設(shè)計(jì)中的故障，通過計(jì)算MCS能夠得到可能的出錯(cuò)原因，進(jìn)而根據(jù)實(shí)際情況對軟硬件故障進(jìn)行修復(fù)[8 - 12]。由于軟硬件系統(tǒng)通常較為復(fù)雜，擁有很大的狀態(tài)空間，模型檢查工作通常轉(zhuǎn)換為軟硬件系統(tǒng)內(nèi)的可達(dá)性分析。通過使用MCS 計(jì)算兩個(gè)狀態(tài)之間不可達(dá)的原因，能夠引導(dǎo)可達(dá)性分析問題中下一個(gè)狀態(tài)的選取，對軟硬件系統(tǒng)進(jìn)行剪枝，實(shí)現(xiàn)加速模型檢查的效果。MCS也可以用于實(shí)際的配置優(yōu)化問題中，當(dāng)用戶給出的要求過于嚴(yán)格時(shí)，無法計(jì)算出一個(gè)完全符合要求的配置方案，通過計(jì)算MCS能夠給出一個(gè)次優(yōu)的配置方案，以盡量滿足用戶所提出的配置要求。用戶根據(jù)MCS給出的配置方案，可以調(diào)整配置要求，最終找到一個(gè)用戶滿意且可行的配置方案。

本文提出了不可滿足子句中的沖突算法CUC(Conflict in Unsatisfiable Clauses)，一種基于不可滿足原因計(jì)算MCS的方法。CUC首先根據(jù)初始賦值，將公式分為可滿足的子公式集合S和不可滿足的子公式集合U。然后通過提取U中所出現(xiàn)的文字L(U)，并對L(U)進(jìn)行分組，迭代判斷L(U)中是否有文字可以加入到S中。當(dāng)發(fā)現(xiàn)可加入的文字后，將所有出現(xiàn)該文字的子句從U中刪除，并加入到S中。直到U中沒有任何可加入S中的文字，當(dāng)前的U子句集合即為MCS。

在CUC中，通過對L(U)進(jìn)行分組，加速了L(U)的處理過程。對于一組文字g?L(U)，若g不能加入到S中，SAT(boolean SATisfiability)求解器將返回其不能加入(不可滿足)的原因。通過對不可滿足原因的分析，能夠得到關(guān)鍵文字信息，進(jìn)而加速M(fèi)CS求解過程。

與其他求解MCS的工作相比，本文采用組合判定的方法，在可滿足性求解搜索之前預(yù)先規(guī)定了一組文字的賦值，降低了可滿足性求解所需要的時(shí)間。實(shí)驗(yàn)表明，與目前性能優(yōu)秀的基于文字的提取LBX(Literal-Based eXtractor)[1]工具相比,CUC平均多求解65個(gè)(5%)公式，且求解效率比LBX快2.5倍。在4種不同的初始化策略中，CUC比LBX最多多求解出9%(113個(gè))公式。

本文第2節(jié)給出文中所用到的定義和符號(hào)；第3節(jié)介紹所提出的CUC算法和 4種不同的初始化策略，并簡單介紹本文根據(jù)已有算法所實(shí)現(xiàn)的LBX工具；第4節(jié)介紹CUC 與LBX的實(shí)驗(yàn)比較結(jié)果，并分析CUC占優(yōu)勢的原因；第5節(jié)對全文進(jìn)行總結(jié)，并指出可能存在的問題。

2 預(yù)備知識(shí)

定義1(布爾變量) 布爾變量集合X={x1,…,xr}，文字是布爾變量xj(j=1,…,r)或者是布爾變量的否定xj。xj稱為正文字，xj稱為負(fù)文字。

定義2(布爾子句) 布爾子句由一組文字的析取組成，對于一個(gè)布爾子句φ=x1∨x2∨x3，我們稱x1,x2,x3出現(xiàn)在φ中，即x1,x2,x3∈φ。

定義3(布爾公式) 布爾公式由布爾子句合取組成，對于一個(gè)布爾公式F=φ1∧φ2∧φ3，我們稱φ1,φ2,φ3出現(xiàn)在F中，即φ1,φ2,φ3∈F。

為了講解方便，我們使用變量、子句、公式代替布爾變量、布爾子句、布爾公式。給定一個(gè)公式F，我們使用cls(F)表示公式中出現(xiàn)的所有子句集合，用var(F)表示公式中出現(xiàn)的所有變量集合，用lit(F)表示公式中出現(xiàn)的所有文字集合。對于一個(gè)給定子句φ，我們使用var(φ)表示子句中出現(xiàn)的所有變量集合，用lit(φ)表示子句中出現(xiàn)的所有文字集合。對于所有集合Z，我們用|Z|表示集合的長度，即集合中元素的個(gè)數(shù)。

定義4(賦值) 對于變量集合X={x1,…,xr}，賦值是一個(gè)映射μ:X→{0,1},當(dāng)μ(xi)=1時(shí)，i=1,…,r,μ(xi)=0。當(dāng)μ(xi)=1時(shí)，μ(xi)=0。

通過計(jì)算公式F中每個(gè)變量的賦值，根據(jù)布爾公式中∧和∨的計(jì)算規(guī)則，能夠得出F的整體賦值。給定一個(gè)賦值μ，若F在μ的賦值情況下真值為1，則F可以被μ滿足，μ是F的一個(gè)解。若F在μ的賦值情況下真值為0，則F不可以被μ滿足。若F不存在一個(gè)解，則F不可滿足。

定義5(MCS) 對于不可滿足公式F，MCS?F,是F的一個(gè)子集，且FMCS可滿足，對于MCS中任一子句φ，F(xiàn)MCS∪{φ}不可滿足。本文所研究的問題即為不可滿足公式的MCS求解問題。

一個(gè)不可滿足公式F如下:

F=(x1∨x2∨x3)∧(x1∨x2)∧x1∧x3∧(x4∨x5∨x6)∧(x4∨x5)∧x4∧x6

其中,變量集合為X={x1,x2,x3,x4,x5,x6}，子句集合C={c1=(x2∨x2∨x3),c2=(x1∨x2),c3=x1,c4=x3,c5=(x4∨x5∨x6),c6=(x4∨x5),c7=x4,c8=x6}。則子句集合C={c3,c7}為公式F的MCS，從F中移除C后，剩余集合：FC=(x1∨x2∨x3)∧(x1∨x2)∧x3∧(x4∨x5∨x6)∧(x4∨x5)∧x6可滿足，且(x1∨x2∨x3)∧(x1∨x2)∧x3∧(x4∨x5∨x6)∧(x4∨x5)∧x6∧x1和(x1∨x2∨x3)∧(x1∨x2)∧x3∧(x4∨x5∨x6)∧(x4∨x5)∧x6∧x4均不可滿足。

3 基于不可滿足原因的最小糾正集求解方法

本文所提出的算法思想如下：對不可滿足公式進(jìn)行分組，使用不可滿足原因，迭代分析公式中當(dāng)前不可滿足的部分能否被其他賦值滿足，進(jìn)而找到最小不可滿足的部分，即為當(dāng)前公式的MCS。我們通過一個(gè)簡單例子說明CUC的工作流程。

對于一個(gè)不可滿足公式：

F=(x1∨x2)∧(x1∨x2)∧(x1∨x2)∧(x1∨x2)∧(x3∨x4)

首先使用初始化賦值μ(x1)=1,μ(x2)=1,μ(x3)=0,μ(x4)=0將F分為可以被μ滿足的子集S和不可以被μ滿足的子集U兩個(gè)部分，其中

S={(x1∨x2),(x1∨x1),(x1∨x1)}

U={(x1∨x2),(x3∨x4)}

CUC計(jì)算U中的所有文字lit(U)，并對lit(U)進(jìn)行分組。lit(U)={x1,x2,x3,x4}。CUC將lit(U)分為組，每組包含個(gè)文字。在當(dāng)前例子中，lit(U)被分為兩組，每組包含兩個(gè)文字。第一組為{x1,x2}，第二組為{x3,x4}。

CUC通過SAT求解器判斷是否存在一個(gè)新的解μ′，使得分組中每個(gè)文字在μ′中的賦值為1。對于第一組，CUC通過求解S∧x1∧x2判斷是否存在一個(gè)新的解μ′，μ′滿足S，且μ′(x1)=1,μ′(x2)=1。由于不存在這樣一個(gè)新的μ′ ，SAT求解器返回不可滿足的原因{x1,x2}。CUC將刪除不可滿足原因中的第一個(gè)文字，判斷剩余的文字所組成的單元子句能否加入到S中。在這個(gè)例子中，S∧x1和S∧x2均不可滿足，不存在一個(gè)新的解μ′，U中沒有新的子句可以加入到S中。在完成第一組文字分組的判定之后，CUC繼續(xù)處理剩余的文字分組，在當(dāng)前的例子中，S∧x3∧x4可滿足，存在一個(gè)新的{x3,x4}所組成的單元子句可以加入到S中，U中所有包含x3或x4的子句可以加入到S中，CUC將{x3∨x4}加入到S中。此時(shí)，U中所有的文字均已處理，MCS求解完成，求得的MCS為{(x1∨x2)}。

計(jì)算MCS(CUC算法)流程描述如下：

算法1計(jì)算MCS

輸入:不可滿足公式F;

輸出:最小修正子集MCS。

1: (S,U) ←initialAssignment(F);

2: (L,B,Lc) ← (L(U),?,?)

3: whileL≠ ? do

4:Lc ←removeLiterals(L,m);

5: (sat,μ,conflcit) ←SAT(S∪B∪Lc);

6: ifsatthen

7: (S,U) ←updateSatClauses(μ,S,U);

8: else

9:dealConflict(S,conflict,Lc);

10: returnMCS=FU

算法1中，F(xiàn)是不可滿足的公式，S和U是F的子集，S∪U=F；L是U中文字的集合;B是CUC在求解過程中找到的關(guān)鍵文字集合;Lc是L的子集，表示當(dāng)前正在處理的文字分組。

算法1的詳細(xì)過程如下:

第1行給定不可滿足公式F，使用initialAssignment方法將F分為子公式集合S和U兩部分。

第2行將所有出現(xiàn)在U中的文字放入L中，B和Lc初始化為空集。

第3行根據(jù)U中的文字集合L，開始循環(huán)計(jì)算U中可以加入到S中的子句。在循環(huán)過程中，不斷從L中移除已經(jīng)訪問過的文字，直到L變?yōu)榭占?。循環(huán)的終止條件是U中所有的文字都已標(biāo)記為已訪問。

第5行求解公式S′:=S∪B∪Lc的可滿足性，返回結(jié)果為三元組(sat,μ,conflict)。若S′可滿足，sat為true，μ為S′的一個(gè)解，conflict為空集；否則sat為false，μ為空集，conflict為S′ 不可滿足的原因。

第6、7行當(dāng)sat為 true時(shí)，調(diào)用updateSatClauses方法將U中的子句加入到S中。

第8、9行當(dāng)sat為 false，即S′不可滿足時(shí)，根據(jù)得到的conflict使用dealConflict繼續(xù)求解當(dāng)前文字分組中能夠加入到S中的單元子句，進(jìn)而計(jì)算能夠加入到S中的子句。

第10行最終的MCS為F和S的差集。

CUC設(shè)計(jì)并實(shí)現(xiàn)了4種不同的initialAssignment方法，分別為:

(1) 全0(-0)初始化策略:將所有的正文字賦值為0，負(fù)文字相應(yīng)地賦值為1。

(2) 全1(-1)初始化策略:將所有的正文字賦值為1，負(fù)文字相應(yīng)地賦值為0。

(3) 隨機(jī)初始化(-random)策略:隨機(jī)決定所有正文字的賦值，負(fù)文字相應(yīng)地取反賦值。

(4) 最大出現(xiàn)次數(shù)(-max)初始化策略:計(jì)算其相應(yīng)正負(fù)文字的出現(xiàn)次數(shù)，將出現(xiàn)次數(shù)較多的文字賦值為1。比如，在公式F中，若文字a的出現(xiàn)次數(shù)為10次，文字a的出現(xiàn)次數(shù)為5次，則a的賦值為1，a的賦值為0。

在removeLiterals方法中，CUC從L中順序選取m個(gè)文字，并將其加入到Lc中形成當(dāng)前正在處理的文字分組。由于CUC保證一個(gè)分組結(jié)束之后才會(huì)開始計(jì)算下一個(gè)分組，因此從L中直接移除這m個(gè)文字，并將其標(biāo)記為已訪問。

在updateClauses方法中，CUC根據(jù)得到的解μ將U中的子句加入到S中。對于所有U中的子句，若其所包含的文字中至少有一個(gè)文字在μ中的賦值為1，則當(dāng)前子句可以加入到S中。即對于?φ∈U,φ可以加入到S中，當(dāng)且僅當(dāng)?a∈φ,μ(a)=1。當(dāng)子句φ加入到S中后，CUC將φ從U中移除。

當(dāng)算法1中第5行的可滿足性求解結(jié)果為不可滿足時(shí)，CUC根據(jù)當(dāng)前分組及其所返回的原因繼續(xù)計(jì)算MCS，其算法偽代碼如算法2所示。

算法2CUC不可滿足原因處理算法dealConflict(S,conflict,L)

輸入:可滿足子公式S，不可滿足的原因conflict，文字分組Lc;

輸出:文字分組Lc中的文字是否均完成處理。

1:(len,vlen)←(|L|,0);

2:if |conflict| == 1 then

3:B←B∪{conflict};

4:vlen++;

5:whilelen≠vlendo

6:a=conflict[0];

7: (sat,μ,conflict′)←SAT(S∪B∪a);

8: ifsatthen

9: (S,U) ←updateSatClauses(μ,S,U)

10: else

11:B←B∪(a)

12: (sat,μ,conflcit′)←SAT(S∪B∪(conflicta}))

13: ifsatthen

14: (S,U)←updateSatClauses(μ,S,U)

15: break

16: else

17:dealConflict(S,conflict′,conflicta}))

18:vlen=vlen+|conflict|;

19:return true

算法2中，len為當(dāng)前文字分組Lc的長度，vlen為當(dāng)前分組中已完成處理的文字個(gè)數(shù)。

算法2的詳細(xì)過程如下:

第1行l(wèi)en初始化為當(dāng)前輸入的文字集合的長度，vlen初始化為0。

第2～4行當(dāng)前輸入的不可滿足原因conflict長度為1時(shí)，將原因中唯一的文字的反加入到關(guān)鍵文字集合B中，將已完成處理的文字個(gè)數(shù)加1。

第5行當(dāng)Lc中還存在未處理的文字，len≠vlen時(shí)，且len≠ 1，循環(huán)處理Lc中剩余的未處理文字，直到所有文字均已完成處理。

第6～11行取出當(dāng)前不可滿足原因集合中的第1個(gè)文字a，判斷單元子句a能否加入到S中。若單元子句a可以加入到S中，則根據(jù)第9行中得到的解μ更新S；若單元子句a不能加入到S中，則執(zhí)行第11行，將文字a的反加入到關(guān)鍵文字集合中。

第12行使用移除了第1個(gè)文字a后的不可滿足原因conflict計(jì)算能夠加入到S中的子句，若存在能夠加入到S中的子句，則執(zhí)行第14行更新S；若仍然不存在能夠加入到S中的子句，則根據(jù)第12行返回的新的不可滿足原因遞歸執(zhí)行dealConflict方法，處理新的不可滿足原因，繼續(xù)計(jì)算能夠加入到S中的子句。

4 實(shí)驗(yàn)結(jié)果

實(shí)驗(yàn)結(jié)果顯示，CUC整體性能比LBX好。綜合4種策略，CUC平均計(jì)算出1 249個(gè)公式，LBX平均計(jì)算出1 184個(gè)公式，CUC比LBX平均多計(jì)算出5%的公式。在LBX與CUC均能夠解出的公式中，LBX的平均計(jì)算時(shí)間為0.44 s，CUC的平均計(jì)算時(shí)間為0.18 s，比LBX快了2.5倍。

4.1 實(shí)驗(yàn)環(huán)境與數(shù)據(jù)集設(shè)置

本文使用Minisat 2.2[5]作為可滿足性求解器，使用C++語言設(shè)計(jì)并開發(fā)了CUC工具，用于計(jì)算不可滿足的布爾公式的最小糾正子集。工具的下載鏈接為http:∥lab301.cn/blog/?page_ id=168&lang=en。

實(shí)驗(yàn)的運(yùn)行服務(wù)器為Intel i7處理器，運(yùn)行內(nèi)存限制為4 GB，ijcai13-bench中的公式運(yùn)行時(shí)間限制為30 s，maxsat14-bench中的公式運(yùn)行時(shí)間限制為180 s。由于maxsat14-bench中的公式求解更加困難，我們在實(shí)驗(yàn)中為其設(shè)置了比ijcai13-bench中公式更長的運(yùn)行時(shí)間限制。

通過查閱參考文獻(xiàn)[1,14]中的實(shí)驗(yàn)部分發(fā)現(xiàn),LBX[1]是目前求解效率最高的MCS求解工具。我們選用LBX作為比較的工具，但由于LBX不提供開源代碼，因此本文按照LBX文中的描述，重新實(shí)現(xiàn)了LBX的工具。

LBX算法同樣根據(jù)初始賦值將不可滿足公式F分為可滿足子集S和不可被滿足子集U兩個(gè)部分。LBX通過逐個(gè)判斷U中文字能否加入到S中的方法，找出U中所有可以加入到S中的子句，進(jìn)而求出F的MCS。

我們嚴(yán)格按照參考文獻(xiàn)[1]中算法1對LBX求解算法的描述實(shí)現(xiàn)了LBX。由于參考文獻(xiàn)[1]中沒有詳細(xì)說明LBX中的初始化策略，我們使用與CUC中相同的4種初始化策略，實(shí)現(xiàn)了 LBX的4種不同的初始化策略，即LBX-1、LBX-0、LBX-random和LBX-max。

本文選用的測試數(shù)據(jù)集包括：ijcai13-bench[1],共1 642個(gè)，其所包含的公式均為合取公式;maxsat14-bench,共105個(gè)[1]，選取了2014年MaxSAT比賽中公式規(guī)模小于30M的公式。

4.2 初始化策略分析

圖1給出了CUC與LBX在4種不同初始化策略下能夠求解出的公式個(gè)數(shù)情況。通過比較發(fā)現(xiàn)，除了LBX-random 初始策略外，CUC的求解個(gè)數(shù)均多于LBX的求解個(gè)數(shù)。而由于LBX-random初始策略具有隨機(jī)性，因此其數(shù)據(jù)對性能的反應(yīng)具有偏差。

Figure 1 Number of instances whose MCS can be solved by the two algorithms under four strategies圖1 兩種算法在4種不同策略下可以求解出MCS的實(shí)例數(shù)量

表1給出了在ijcai13-bench 數(shù)據(jù)集中，LBX與CUC能夠同時(shí)求解出的公式個(gè)數(shù)，及相應(yīng)的求解時(shí)間和平均求解時(shí)間。結(jié)果表明CUC在不同策略下的性能均要優(yōu)于LBX，平均求解效率是LBX的2.5倍。在4種不同的初始化策略下，求解同樣的公式，CUC所需的總時(shí)間均小于LBX所需總時(shí)間。值得注意的是，雖然CUC-random的求解時(shí)間與LBX-random 的求解時(shí)間相差最大，但由于LBX-random能夠求解出的公式數(shù)量較少，且多數(shù)為簡單公式，因此該組時(shí)間差距最大。

Table 1 Analysis of the formulas which can be solved by both CUC and LBX表1 CUC與LBX均可求解的公式分析結(jié)果

圖2展示了LBX和CUC在不同策略和不同時(shí)間內(nèi)求解出的公式個(gè)數(shù)的變化。在1 642個(gè)公式中，存在部分公式使用LBX和CUC計(jì)算MCS的平均求解時(shí)間小于0.01 s。為了使圖表更加清晰，圖2中僅選擇了LBX和CUC的平均時(shí)間大于0.01 s的公式進(jìn)行分析。CUC-max、CUC-1、CUC-0可求解公式的個(gè)數(shù)均大于LBX的相應(yīng)策略。

上述實(shí)驗(yàn)結(jié)果表明，CUC在CUC-1、CUC-0初始化策略下，求解公式個(gè)數(shù)均多于 LBX的，總求解時(shí)間和平均求解時(shí)間均小于LBX的求解時(shí)間。依據(jù)圖2展示的LBX和CUC在-max策略下不同時(shí)間求解出的公式個(gè)數(shù)的變化，在相同時(shí)間下，CUC求解出的公式個(gè)數(shù)均大于LBX的，換言之求解出相同個(gè)數(shù)公式的情況下，CUC效率高于LBX，如表3所示，其平均求解時(shí)間比LBX快2.5倍。最為重要的是，CUC可以求解出LBX無法在規(guī)定時(shí)間內(nèi)求解出的公式，這表明 CUC的平均性能優(yōu)于LBX。分析CUC求解數(shù)據(jù)情況可知，CUC-0與CUC-max的性能優(yōu)于其他兩種策略。CUC-max能夠比CUC-0多求解出46個(gè)公式。在520 s時(shí)，CUC-max求解個(gè)數(shù)比 CUC-0多了9個(gè)，時(shí)間超過520 s，CUC-max可以求解出在規(guī)定時(shí)間內(nèi)CUC-0無法求出的公式，占總公式2%。由此可知，CUC-max性能優(yōu)于CUC-0，在4種不同的初始化策略中最優(yōu)。而分析LBX求解數(shù)據(jù)情況也可以發(fā)現(xiàn)，LBX-max能夠求解出的公式個(gè)數(shù)在LBX的4種策略中最多，其求解公式數(shù)量僅次于CUC-max的。因此，在4種初始化策略中，-max初始化策略的性能最優(yōu)。這是因?yàn)?max初始化策略通過不停地選擇未賦值文字出現(xiàn)次數(shù)最多的文字，能夠使得初始化賦值盡量滿足更多的子句。在后續(xù)的計(jì)算過程中，僅有較少的未滿足子句需要使用CUC或LBX方法進(jìn)行判定，節(jié)省了判定過程中調(diào)用可滿足性求解器的次數(shù)，加快了LBX和CUC的求解效率，縮短了求解時(shí)間。

Figure 2 Running times for ijcai13-bench instances圖2 ijcai13-bench運(yùn)行時(shí)間圖

圖3展示了CUC-max與LBX-max在不同時(shí)間內(nèi)求解出的公式個(gè)數(shù)的變化。CUC-max的求解個(gè)數(shù)優(yōu)于LBX-max的。由于選取的公式在規(guī)定的時(shí)間內(nèi)求解出MCS較為困難，CUC與LBX均只能求解出較少的公式，CUC-max能夠求解出10個(gè)公式， LBX-max能夠求解出5個(gè)公式，所有LBX-max能夠求解出的公式，均可以由CUC-max求解得出。

Figure 3 Running times for MaxSAT instances圖3 MaxSAT運(yùn)行時(shí)間圖

5 相關(guān)工作

MCS計(jì)算問題作為一種研究不可滿足約束的主要方法，從1987年開始就引起了研究學(xué)者的關(guān)注，并應(yīng)用于基于可滿足性分析的模型故障分析之中[12]。MCS求解方法主要分為迭代求解公式可滿足性的方法和根據(jù)初始化賦值構(gòu)建最大可滿足公式的方法兩類。

迭代求解公式可滿足性方法主要包括線性搜索方法[15]、松弛文字方法[16]和FASTDIAG方法[17]。

Bailey等人[15]使用線性搜索方法求解公式F的MCS集合C。線性搜索算法從MCS的定義出發(fā)，每次選擇一個(gè)子句c∈F，并將c從F中移除，判定Fc的可滿足性，若Fc可滿足，則完成了對C的計(jì)算，若Fc不可滿足，則繼續(xù)選擇另一個(gè)子句c′，并判定Fc∪c′的可滿足性。線性搜索算法通過不斷地從原公式F中刪除子句的方法，能夠找到一個(gè)子句集合M，使得FM可滿足，且對于M中的任一子句m，F(xiàn)M∪m均不可滿足。M就是原公式F的MCS集合。對于同等的布爾約束公式，當(dāng)公式不可滿足時(shí)其可滿足性評價(jià)判定時(shí)間較長，線性搜索算法中的大部分需要判定可滿足性的公式均為不可滿足公式，因此線性搜索的平均搜索時(shí)間較長。

Liffiton等人[16]提出了使用最大可滿足子集計(jì)算MCS的方法。為了避免多次判定不可滿足公式的可滿足性，節(jié)省判定時(shí)間，最大可滿足子集方法為原公式中每個(gè)子句增加了一個(gè)松弛文字l，所生成的新公式為F′，c′一定存在一個(gè)解μ，μ中所有的松弛文字均被賦值為1，則F′一定是可滿足的。最大可滿足子集方法不斷搜索新的解，并希望在新的解中賦值為1的松弛文字個(gè)數(shù)不斷減少。當(dāng)不存在能夠?qū)①x值從1改為0的松弛文字時(shí)，最大可滿足子集方法結(jié)束搜索，最終的MCS是那些松弛文字賦值為1的子句組成的集合。

Felfernig等人[17]提出了FASTDIAG算法，使用分而治之的思想計(jì)算MCS。FASTDIAG算法遞歸地分析原公式F不可滿足的原因。FASTDIAG算法將F逐層分解為子公式，每層兩個(gè)子公式均由上層的子公式一分為二而來。通過將不可滿足的原因分解到兩個(gè)子公式中，逐層分析出原公式的最小不可滿足原因MCS。

在通過初始化賦值構(gòu)建最大可滿足公式的MCS求解方法中，為了避免判定公式不可滿足所需的大量時(shí)間，MCS提取算法在調(diào)用求解器之前，先生成初始化賦值μ，根據(jù)μ將原公式F分為能夠被μ滿足的子集S和不能被μ滿足的子集U，該類方法主要有D子句算法CLD(Clause D)[18]、分區(qū)算法CMP(Computational Method for Partitioning)[4]和LBX方法[1]。

Marques-Silva等人[18]提出了CLD算法。CLD算法根據(jù)初始化賦值，將原公式分為子公式集合S和U兩個(gè)部分，子公式集合S能夠被初始化賦值滿足，子公式集合U不能夠被初始化賦值滿足。CLD算法統(tǒng)計(jì)所有出現(xiàn)在子公式集合U中的文字Lit(U)，并將這些文字析取連接，生成一個(gè)新的子句clauseD，即clauseD=∨l,l∈Lit(U)。將子句ClauseD合取加入到子公式集合S中，判定S∧clauseD的可滿足性。若S∧clauseD可滿足，則根據(jù)所得到的解更新S和U；若不可滿足，則說明當(dāng)前的U即為MCS。

Grégoire等人[4]提出的CMP算法也使用初始化賦值將原公式劃分為可滿足子公式集合S及其補(bǔ)集U。CMP算法利用MCS和MUC計(jì)算互為擊中集問題的性質(zhì)，通過計(jì)算變遷子句(Transition Clause)來計(jì)算MCS。假設(shè)一個(gè)不可滿足的公式F存在多個(gè)不可滿足的最小核(MUC)，即F中存在多組由于互相沖突導(dǎo)致無法同時(shí)可滿足的子句集合。為了消除沖突，找到可滿足子公式，需要解決每個(gè)MUC的沖突。根據(jù)MUC的性質(zhì)，從MUC 子句集合中任意移除一條子句即可解決該MUC的沖突。因此，從每個(gè)MUC中移除一條子句即可使得到的子公式可滿足，所移除的所有子句組成了MCS。CMP提出了一種從MUC中找到一條子句的方法，進(jìn)而能夠計(jì)算MCS。需要注意的是，計(jì)算MUC的時(shí)間開銷較大，因此CMP沒有選擇通過計(jì)算得到所有的MUC。CMP首先從U中選擇一條子句c，計(jì)算S∧Uc的可滿足性，若公式可滿足，則根據(jù)所得到的解更新子公式集合S和U，并將c放入MCS集合中，c是CMP找到的一個(gè)能夠解決相應(yīng)MUC沖突的變遷子句。若公式不可滿足，則將c從U中移除，之后重新選擇一條子句c′，重復(fù)上述步驟。已經(jīng)放入 MCS中的子句c不會(huì)再次出現(xiàn)在子公式集合S和U中，當(dāng)存在一個(gè)賦值，其計(jì)算出的子公式集合U為空集時(shí)，CMP算法結(jié)束，返回計(jì)算得到的MCS。

Mencia等人[1]提出的LBX算法首先根據(jù)初始化賦值將原公式劃分為可滿足子公式集合S及其補(bǔ)集U。之后，LBX算法調(diào)用CLD算法計(jì)算所有出現(xiàn)在子公式集合U中的文字，與CLD算法不同的是，LBX算法將U中出現(xiàn)的文字構(gòu)建為單元子句，逐個(gè)地加入到S中。LBX算法每次選取一個(gè)構(gòu)建的單元子句c，判定是否可滿足，若可滿足，則根據(jù)求得的解更新S和U，若不可滿足，繼續(xù)選擇下一個(gè)單元子句c進(jìn)行判定。已判定過的單元子句不會(huì)重復(fù)判定，當(dāng)所有的單元子句均判定結(jié)束后，LBX算法結(jié)束，最終得到的U即為 MCS。與CUC算法相比，CLD算法將出現(xiàn)在子公式集合U中的文字組成一個(gè)新的子句，容易導(dǎo)致新生成的子句過長，影響可滿足性求解器的求解效率。在CMP的運(yùn)行過程中，對不可滿足公式的判定次數(shù)明顯多于對可滿足公式的判定次數(shù)，算法整體的可滿足性判定效率因此降低。LBX算法對每個(gè)出現(xiàn)在子公式集合U中的文字均調(diào)用一次可滿足性求解判定其是否出現(xiàn)在MCS 中，對可滿足性求解的利用效率較低。

6 結(jié)束語

本文提出了一種基于不可滿足計(jì)算MCS的CUC算法和工具。CUC通過分析不可滿足的原因，改進(jìn)LBX求解MCS的算法，減少了調(diào)用SAT求解器的次數(shù)，最終加速了求解過程。與LBX比較，CUC能夠通過一次可滿足性求解確定多個(gè)文字是否出現(xiàn)在最終的MCS中，而LBX中的一次可滿足性求解只能確定一個(gè)文字是否出現(xiàn)在最終的MCS中。通過與已有LBX的實(shí)驗(yàn)比較發(fā)現(xiàn)，CUC能夠使用更少的求解時(shí)間求解出更多的公式?？傮w而言，與LBX工具相比，CUC在求解MCS時(shí)更具有優(yōu)勢，特別在初始賦值使用-max策略時(shí)，CUC的優(yōu)勢更為顯著，對于CUC和LBX同時(shí)可以解出的公式，CUC平均求解時(shí)間比LBX快2.5倍。

[1] Mencia C,Previti A,Marques-Silva J.Literal-based MCS extraction[C]∥Proc of the 24th International Joint Conference on Artificial Intelligence, 2015:1973-1979.

[2] Reiter R.A theory of diagnosis from first principles[J].Artificial Intelligence,1987,32(1):57-95.

[3] Liffiton M H,Previti A,Malik A,et al.Fast,flexible MUS enumeration[J].Constraints,2016,21(2):223-250.

[4] Grégoire E,Lagniez J M,Mazure B.An experimentally efficient method for (MSS,CoMSS) partitioning[C]∥Proc of AAAI,2014:2666-2673.

[5] Kavvadias D J, Sideri M,Stavropoulos E C.Generating all maximal models of a Boolean expression[J].Information Processing Letters,2000,74(3-4):157-162.

[6] Xu Dao-yun. Applications of minimal unsatisfiable formulas to polynomially reduction for formulas[J].Journal of Software,2006,17(5):1204-1212.(in Chinese)

[7] Yin Ming-hao, Lin Hai,Sun Ji-gui. Solving #SAT using extension rules[J].Journal of Software,2009,20(7):1714-1725.(in Chinese)

[8] Koitz R,Wotawa F.SAT-based abductive diagnosis[C]∥Proc of the 26th Internatinal Workshop on Principles of Diagnosis,2015:167-176.

[9] Walter R, Felfernig A, Küchlin W.Constraint-based and SAT-based diagnosis of automotive configuration problems[J].Journal of Intelligent Information Systems,2017,49(1):87-118.

[10] Arif M F, Mencía C,Ignatiev A,et al.BEACON:An efficient SAT-based tool for debugging εL ontologies[C]∥Proc of International Conference on Theory and Applications of Satisfiability Testing,2016:521-530.

[11] Arif M F, Mencía C,Marques-Silva J.Efficient axiom pinpointing with EL2MCS[C]∥Proc of Joint German/Austrian Conference on Artificial Intelligence (Künstliche Intelligenz),2015:225-233.

[12] Bekkouche M,Collavizza H,Rueher M.LocFaults:A new flow-driven and constraint-based error localization approach[C]∥Proc of the 30th Annual ACM Symposium on Applied Computing,2015:1773-1780.

[13] Eén N,S?rensson N.An extensible SAT-solver[C]∥Proc of International Conference on Theory and Applications of Satisfiability Testing,2003:502-518.

[14] Mencía C,Ignatiev A,Previti A,et al.MCS extraction with sublinear oracle queries[C]∥Proc of International Conference on Theory and Applications of Satisfiability Testing,2016:342-360.

[15] Bailey J,Stuckey P.Discovery of minimal unsatisfiable subsets of constraints using hitting set dualization[C]∥Proc of the 7th International Symposium on Practical Aspects of Declarative Languages,2005:174-186.

[16] Liffiton M H,Sakallah K A.Algorithms for computing minimal unsatisfiable subsets of constraints[J].Journal of Automated Reasoning,2008,40(1):1-33.

[17] Felfernig A,Schubert M,Zehentner C.An efficient diagnosis algorithm for inconsistent constraint sets[J].AI EDAM,2012,26(1):53-62.

[18] Marques-Silva J,Heras F,Janota M,et al.On computing minimal correction subsets[C]∥Proc of the 23rd International Joint Conference on Artificial Intelligence, 2013:615-622.

附中文參考文獻(xiàn)：

[6] 許道云.極小不可滿足公式在多項(xiàng)式歸約中的應(yīng)用[J].軟件學(xué)報(bào),2006,17(5):1204-1212.

[7] 殷明浩,林海,孫吉貴.一種基于擴(kuò)展規(guī)則的#SAT求解系統(tǒng)[J].軟件學(xué)報(bào),2009,20(7):1714-1725.