基于雙模型的MUS求解方法

歐陽丹彤 高 菡 田乃予 劉 夢 張立明

1(吉林大學(xué)軟件學(xué)院 長春 130012)2(吉林大學(xué)計算機(jī)科學(xué)與技術(shù)學(xué)院 長春 130012)3(符號計算與知識工程教育部重點(diǎn)實(shí)驗(yàn)室(吉林大學(xué))長春 130012)(ouyangdantong@163.com)

命題可滿足問題(propositional satisfiability problem,SAT)是人工智能領(lǐng)域中的研究熱點(diǎn)[1-5],極小不可滿足子集(minimal unsatisfiable subset,MUS)和極小修正子集(minimal correction set,MCS)是SAT問題的擴(kuò)展問題.在現(xiàn)實(shí)中許多重要問題可以編碼為MUS問題進(jìn)行求解,MUS的主要應(yīng)用包括本體中不一致性檢測問題[6-7]、關(guān)系規(guī)范調(diào)試問題[8-9]、過度約束的時序分析問題[10]、描述邏輯中的公理精確定位問題[11]、硬件模型驗(yàn)證問題[12]和基于模型的診斷[13]等問題.如何高效求解MUS問題對人工智能的很多領(lǐng)域都有深遠(yuǎn)意義.

近年來,極小不可滿足子集求解問題受到國內(nèi)外學(xué)者廣泛關(guān)注.早在2005年Bailey等人[14]提出DAA方法,根據(jù)MUS與MCS互為極小碰集的對偶性來提高M(jìn)US枚舉效率,首先利用Grow(依次向上遍歷真超集)子過程根據(jù)1個可滿足的節(jié)點(diǎn)求得極大可滿足子集(maximal satisfiable subset,MSS),對其得到的補(bǔ)集MCS求極小碰集來得到1個MUS,不斷迭代此方法來得到多個MUS.2005年及2008年,Liffiton等人[10,15]在DAA方法的基礎(chǔ)上提出了CAMUS方法對MUS進(jìn)行完備求解,CAMUS方法先計算給定問題的所有MSS,再由MSS求得對應(yīng)的所有MCS,最后根據(jù)對偶性求解出全部MUS.值得注意的是,此方法在較難的問題中可能得不到解.2011年Belov等人[16]提出遞歸模型翻轉(zhuǎn)方法來提升MUS枚舉效率,先由給定的不可滿足問題得到1個MCS,利用模型翻轉(zhuǎn)得到1組MCS,直至得到所有MCS,之后根據(jù)對偶性求得所有的MUS，此方法由于要多次調(diào)用碰集算法，故求解MUS較為耗時.2013年Liffiton等人[17]提出結(jié)合哈斯圖求解MUS的方法,對于哈斯圖Map中的任意一個未被探索的節(jié)點(diǎn),利用Grow或Shrink(依次向下遍歷真子集)子過程求解得到1個MSS或MUS.同時在2013年P(guān)reviti等人[18]提出部分MUS枚舉方法,稱為eMUS方法,此方法先計算極大模型對應(yīng)的可滿足性,如可滿足則得到MSS,繼而求得其補(bǔ)集MCS,再求極小碰集得到MUS;若不可滿足則直接用MUS提取器求解MUS.2016年Liffiton等人[19]結(jié)合eMUS方法對MARCO方法進(jìn)行了改進(jìn),給出極大化模型的MARCO-M方法,此方法針對隨機(jī)選擇節(jié)點(diǎn)進(jìn)行求解的缺點(diǎn),在哈斯圖的未求解空間中利用啟發(fā)式策略優(yōu)先選擇極大節(jié)點(diǎn)進(jìn)行求解,進(jìn)而較快地求解得到MUS.為了加快MARCO-M方法求解效率，2016年Zhao等人[20]實(shí)現(xiàn)了MARCO-M方法的多種子并行化求解方法,使得MARCO-M方法求解效率有較大提高,但并行化求解方法并沒有降低分解后子問題的求解復(fù)雜度.隨著MUS求解方法的不斷改進(jìn),許多學(xué)者開始研究如何結(jié)合MUS求解技術(shù)對MCS求解方法進(jìn)行優(yōu)化.2018年Narodytska等人[21]在Belov等人[16]遞歸模型翻轉(zhuǎn)求解MUS方法的基礎(chǔ)上給出高效的MCS求解方法,先根據(jù)求解得到的1個MUS求出對應(yīng)的MCS,然后結(jié)合遞歸模型翻轉(zhuǎn)得到其對應(yīng)的1組MCS,重復(fù)迭代上述2步直至得到所有的MCS.

對于MARCO-M方法,它使用1個框架來描述和可視化不可滿足性分析方法,就不可滿足的約束系統(tǒng)以哈斯圖的形式可視化冪集圖以及遍歷操作.在MARCO-M方法對其之前工作中隨機(jī)模型進(jìn)行改進(jìn)后新提出的極大化模型而言,該模型是利用了在時間上產(chǎn)生類似于最先進(jìn)的單-MUS方法的第1個輸出,這使得在較早期產(chǎn)生解時它是高效的.基于它自上而下的遍歷方式,若是實(shí)例中MUS解個數(shù)很少或都集中在冪集圖下半部時,它將在求得首個MUS之后效果不再顯著,甚至變差,這是由它自身模型的單一性導(dǎo)致的.

本文在充分分析MARCO-M方法的基礎(chǔ)上,對其極大化模型進(jìn)行改進(jìn),給出雙模型遍歷方法MARCO-MAM方法,對于極大化模型以犧牲MSS求解而只專注于MUS求解的遍歷方式,提出了利用MSS求解輔助MUS求解的新想法,并以此增強(qiáng)MARCO-M方法在難以處理實(shí)例問題中的穩(wěn)健性.

1 預(yù)備知識

本節(jié)首先介紹SAT問題的相關(guān)定義,然后介紹其擴(kuò)展問題MUS和MCS的相關(guān)概念,并在最后介紹了MUS和MCS之間的對偶關(guān)系.

1.1 SAT問題

SAT問題又稱布爾可滿足性問題,是一種簡單布爾類型的約束可滿足判定問題,即判定1個給定的命題公式是否可滿足.在命題邏輯的定義中,析取用符號∨表示,合取用符號∧表示.下面給出其相關(guān)形式化定義.

定義1.文字[22].給定m個布爾變量x1,x2,…,xm,文字Qi是變量xi或xi的否定(﹁xi).

定義2.子句[22].給定n個互不相同的文字Q1,Q2,…,Qn,子句Ci是文字的析?。篞1∨Q2∨…∨Qn.

定義3.合取范式(CNF)[22].形式如C1∧C2∧…∧Cr的由多個不同子句的合取所組成的公式稱為合取范式(CNF).

定義4.SAT問題[22].SAT問題通常是指合取范式CNF的可滿足問題,即判定是否存在使得合取公式C1∧C2∧…∧Cr的真值為真的1組變量的賦值.

對于1個給定的合取范式Φ,SAT問題即判斷是否存在1組賦值使得公式Φ的值為真：若存在,則稱公式Φ是可滿足的;否則,是不可滿足的.

1.2 MUS和MCS

本節(jié)介紹SAT的擴(kuò)展問題MUS,MSS,MCS問題,并介紹3者之間的互補(bǔ)及對偶的關(guān)系.

定義5.MUS[19].稱M為不可滿足問題Φ的1個MUS,若M?Φ,M不可滿足,且?c∈M:M{c}可滿足.

定義6.MSS[19].稱M為不可滿足問題Φ的1個MSS,若M?Φ,M可滿足,且?c∈ΦM:M∪{c}不可滿足.

定義7.MCS[19].稱M為不可滿足問題Φ的1個MCS,若M?Φ,ΦM可滿足,且?S∈M:ΦS不可滿足.

從定義6和定義7的關(guān)系可以得出,MSS與MCS互為補(bǔ)集.不可滿足問題Φ的任何一個MSS都對應(yīng)1個MCS,反之亦然.實(shí)例的任何MCS都是該實(shí)例的MUS集合的極小碰集,并且任何MUS都是MCS的極小碰集[21],即對偶性.下面給出1個實(shí)例來介紹MUS,MSS,MCS三者之間的關(guān)系.

例1.Φ={s1:(α),s2:(﹁α),s3:(﹁α∨β),s4:(﹁β)},其中,不可滿足問題Φ的所有MUS為{s1,s2},{s1,s3,s4},根據(jù)其對偶性關(guān)系對所有MUS求極小碰集得到所有MCS為{s1},{s2,s4},{s2,s3},又由MCS與MSS的互補(bǔ)關(guān)系可以得到所有的MSS為{s2,s3,s4},{s1,s3},{s1,s4}.

2 MARCO-M方法

為了求解給定不可滿足問題的所有MUS,則需要判定不可滿足問題每一個子集的可滿足性,此過程實(shí)際上是枚舉集合對應(yīng)其冪集的過程.MARCO-M方法中利用哈斯圖枚舉,下面先介紹哈斯圖.對于給定集合S={1,2,3,4},設(shè)它的冪集為P(S),則S的哈斯圖冪集可視化如圖1所示:

Fig.1 Example of Hasse diagram圖1 哈斯圖示例

MARCO-M方法基本思想：在求解不可滿足問題的所有MUS的過程中,利用哈斯圖對求解過程進(jìn)行模擬.即要求解所有的MUS,只需要遍歷哈斯圖上的所有節(jié)點(diǎn),對每個節(jié)點(diǎn)進(jìn)行相應(yīng)的判定就可以得到最后的解.如果當(dāng)前判定的節(jié)點(diǎn)是可滿足的,則向上判定其超集的可滿足性,直到某個超集節(jié)點(diǎn)是不可滿足,則此過程中最后一個可滿足的節(jié)點(diǎn)為MSS,并對MSS對應(yīng)的所有子集節(jié)點(diǎn)進(jìn)行阻塞,不再訪問求解此空間;如果當(dāng)前判定的節(jié)點(diǎn)是不可滿足的,則向下判定其子集的可滿足性,直到某個子集節(jié)點(diǎn)是可滿足的,則此過程中最后一個不可滿足的節(jié)點(diǎn)為MUS,并對MUS對應(yīng)的所有超集節(jié)點(diǎn)進(jìn)行阻塞,不再訪問求解此空間.最后得到所有MUS和MSS.

上面介紹了MARCO-M方法用到的哈斯圖和其求解的基本思想,下面介紹MARCO-M方法的偽代碼.

算法1.MARCO-M.

輸入:不可滿足的約束系統(tǒng)C;

輸出:C中的極小不可滿足集合ΨMUS、極大可滿足集合ΨMSS.

①ΨMUS←?;

②ΨMSS←?;

③nvars←|C|;

④Map←BoolFormula(nvars);

⑤ While(Map是可滿足的)

⑥Seed←GetUepM(Map);

⑦ If(SAT(Seed))

/*極大化模型得到的Seed就是1個MSS*/

⑧ΨMSS←ΨMSS∪Seed;

⑨Map←Map∩BlockDown(Seed);

⑩ Else

算法1中行①②初始化MUS及MSS的解集集合,行③④初始化Map即哈斯圖,讀取文件中的約束加入Map,在Map可滿足時(行⑤),說明Map中至少還有1個節(jié)點(diǎn)沒有被遍歷,則繼續(xù)遍歷,將未遍歷節(jié)點(diǎn)中的極大節(jié)點(diǎn)作為下一次遍歷的目標(biāo)節(jié)點(diǎn)也就是種子Seed,每得到1個Seed,就判斷它的可滿足性.若可滿足(行⑦),因?yàn)樗菢O大的,故直接得到1個MSS,將它加入ΨMSS解集(行⑧)并向下阻塞所有子集(行⑨);若不可滿足(行⑩),則向下Shrink成1個MUS,將它加入ΨMUS解集(行)并向上阻塞其所有超集(行).極大化模型選取極大種子的目的在于選取的Seed越大它就越可能是不可滿足的,且若Seed是可滿足,則它直接就是MSS解,省去了Grow的子過程.下面介紹MARCO-MAM方法,并以1個實(shí)例運(yùn)行過程來說明MARCO-MAM方法對MARCO-M方法的改進(jìn).

3 MARCO-MAM方法

第2節(jié)介紹了MARCO-M方法的基本思想,它在算法1中提出了針對求解所有MUS的極大化模型.MARCO-MAM方法是在此基礎(chǔ)上提出的雙模型交替求解方法,避免了MARCO-M方法單一極大化模型求解MUS時未有效利用其他優(yōu)化技術(shù)對求解空間進(jìn)行剪枝的不足.下面給出MARCO-MAM方法使用的雙模型交替求解方法,最后再給出1個實(shí)例對2種方法進(jìn)行說明.

MARCO-MAM方法思想：本方法交替求解MUS解及MSS解,利用MSS求解時對應(yīng)的剪枝來減小MUS搜索的空間,進(jìn)而提高M(jìn)US求解效率,同時也提高M(jìn)SS求解效率.MARCO-MAM方法在求解中仍然使用哈斯圖對求解過程進(jìn)行模擬.雙模型交替即為使用極大化模型-中間模型交替來遍歷哈斯圖,已知極大化模型是針對求解MUS的,我們提出中間模型用來針對求解MSS,因此使用雙模型會得到MUS,MSS交替的解.在求解MUS及MSS的過程中我們?nèi)哉{(diào)用Shrink及Grow子過程,并在每一次得到1個解后對Map進(jìn)行阻塞以標(biāo)記已探索空間,直到得到所有的MUS,MSS.下面給出MARCO-MAM方法的偽代碼.

算法2.MARCO-MAM.

輸入:不可滿足的約束系統(tǒng)C;

輸出:C中的極小不可滿足集合ΨMUS、極大可滿足集合ΨMSS.

①ΨMUS←?;

②ΨMSS←?;

③nvars←|C|;

④Map←BoolFormula(nvars);

⑤ While (Map是可滿足的)

⑥Seed[]←GetUepM(Map);

/*極大化模型得到的Seed_Max*/

⑦ If (SAT(Seed[0]))

⑧s←Grow(Seed);

⑨ΨMSS←ΨMSS∪s;

⑩Map←Map∩BlockDown(s);

算法2相對與MARCO-M方法的改進(jìn)主要體現(xiàn)在遍歷方式及模型的選取上.首先根據(jù)極大化模型選取Seed列表中的第1個Seed(行⑥).行⑦中,當(dāng)Seed可滿足時,若Seed由極大化模型得到,則直接作為MSS解,若Seed由中間模型得到,則調(diào)用Grow得到1個MSS(行⑧);當(dāng)Seed不可滿足時,根據(jù)極大化模型得到1個中間模型加入到Seed列表中(行),作為下一個Seed.在每得到1個解后刪除當(dāng)前Seed(行).下面給出1個實(shí)例對這2種方法進(jìn)行對比.

例2.對于待求解問題Φ={s1:(α),s2:(﹁α),s3:(﹁α∨β),s4:(﹁β)},其對應(yīng)的哈斯圖如圖1所示.MARCO-M方法執(zhí)行實(shí)例為:從Map=?開始執(zhí)行,當(dāng)前實(shí)例的可滿足性需進(jìn)行判定,GetUepM()在首次執(zhí)行時會選擇P(Φ)中的全集即{s1,s2,s3,s4}作為Seed,即為極大模型.其執(zhí)行過程為:

步驟1.

選取{s1,s2,s3,s4}為Seed;

SAT({s1,s2,s3,s4})→False(不可滿足的);

Shrink({s1,s2,s3,s4})→{s1,s2};

ΨMUS:{s1,s2};

ΨMSS:?;

Map∧(﹁x1∨﹁x2);

可滿足集合:?;

不可滿足集合:{s1,s2,s3,s4},{s1,s2,s3},{s1,s2,s4},{s1,s2}.

步驟2.

選取{s1,s3,s4}為Seed;

SAT({s1,s3,s4})→False(不可滿足的);

Shrink({s1,s3,s4})→{s1,s3,s4};

ΨMUS:{s1,s2},{s1,s3,s4};

ΨMSS:?;

Map∧(﹁x1∨﹁x3∨﹁x4);

可滿足集合:?;

不可滿足集合:{s1,s2,s3,s4},{s1,s2,s3},{s1,s2,s4},{s1,s2},{s1,s3,s4}.

步驟3.

選取{s2,s3,s4}為Seed;

SAT({s2,s3,s4})→True(可滿足的);

Grow({s2,s3,s4})→{s2,s3,s4};

ΨMUS:{s1,s2},{s1,s3,s4};

ΨMSS:{s2,s3,s4};

Map∧(x1);

可滿足集合:{s2,s3,s4},{s2,s3},{s2,s4},{s3,s4},{s2},{s3},{s4},{?};

不可滿足集合:{s1,s2,s3,s4},{s1,s2,s3},{s1,s2,s4},{s1,s2},{s1,s3,s4}.

步驟4.

選取{s1,s3}為Seed;

SAT({s1,s3})→True(可滿足的);

Grow({s1,s3})→{s1,s3};

ΨMUS:{s1,s2},{s1,s3,s4};

ΨMSS:{s2,s3,s4},{s1,s3};

Map∧(x2∨x4);

可滿足集合:{s2,s3,s4},{s2,s3},{s2,s4},{s3,s4},{s2},{s3},{s4},{?},{s1,s3},{s1};

不可滿足集合:{s1,s2,s3,s4},{s1,s2,s3},{s1,s2,s4},{s1,s2},{s1,s3,s4}.

步驟5.

選取{s1,s4}為Seed;

SAT({s1,s4})→True(可滿足的);

Grow({s1,s4})→{s1,s4};

ΨMUS:{s1,s2},{s1,s3,s4};

ΨMSS:{s2,s3,s4},{s1,s3},{s1,s4};

Map∧(x2∨x3);

可滿足集合:{s2,s3,s4},{s2,s3},{s2,s4},{s3,s4},{s2},{s3},{s4},{?},{s1,s3},{s1},{s1,s4};

不可滿足集合:{s1,s2,s3,s4},{s1,s2,s3},{s1,s2,s4},{s1,s2},{s1,s3,s4}.

MARCO-M方法僅針對MUS做了改進(jìn),在快速求出MUS時,不能兼顧以同樣的速度求出MSS,忽視了MSS對于哈斯圖遍歷求解MUS的輔助剪枝作用,且每次只能標(biāo)記1次Map,模型較單一.下面給出MARCO-MAM方法在上述相同實(shí)例上的求解過程,以說明對MARCO-M方法的優(yōu)化改進(jìn)之處,MARCO-MAM方法的執(zhí)行過程為:

步驟1.

選取{s1,s2,s3,s4}為Seed_Max;

SAT({s1,s2,s3,s4})→False(不可滿足的);

選取{s1,s3}為Seed_Mid;

SAT({s1,s3})→True(可滿足的);

Shrink({s1,s2,s3,s4})→{s1,s2};

Grow({s1,s3})→{s1,s3};

ΨMUS:{s1,s2};

ΨMSS:{s1,s3};

Map∧(﹁x1∨﹁x2)∧(x2∨x4);

可滿足集合:{s1,s3},{s1},{s3},{?};

不可滿足集合:{s1,s2,s3,s4},{s1,s2,s3},{s1,s2,s4},{s1,s2}.

步驟2.

選取{s1,s3,s4}為Seed_Max;

SAT({s1,s3,s4})→False(不可滿足的);

選取{s1,s4}為Seed_Mid;

SAT({s1,s4})→True(可滿足的);

Shrink({s1,s3,s4})→{s1,s3,s4});

Grow({s1,s4})→{s1,s4};

ΨMUS:{s1,s2},{s1,s3,s4};

ΨMSS:({s1,s3},{s1,s4});

Map∧(﹁x1∨﹁x3∨﹁x4)∧(x2∨x3);

可滿足集合:{s1,s3},{s1},{s3},{?},{s1,s4},{s4};

不可滿足集合:{s1,s2,s3,s4},{s1,s2,s3},{s1,s2,s4},{s1,s2},{s1,s3,s4}.

步驟3.

選取{s2,s3,s4}為Seed_Max;

SAT({s2,s3,s4})→True(可滿足的);

選取{s2,s4}為Seed_Mid;

{s2,s4}在本步驟Seed_Max中已經(jīng)被遍歷過，不再判斷其可滿足性;

Grow{s2,s3,s4})→{s2,s3,s4});

ΨMUS:{s1,s2},{s1,s3,s4};

ΨMSS:{s1,s3},{s1,s4},{s2,s3,s4};

Map∧(x1);

可滿足集合:{s1,s3},{s1},{s3},{?},{s1,s4},{s4},{s2,s3,s4},{s2,s3},{s2,s4},{s3,s4},{s2};

不可滿足集合:{s1,s2,s3,s4},{s1,s2,s3},{s1,s2,s4},{s1,s2},{s1,s3,s4}.

由例2可以看出,MARCO-MAM方法每次獲取雙模型后會求得2個解,標(biāo)記Map兩次.在MARCO-M方法中只標(biāo)記1次,這也使得MARCO-M方法需要5步完成全部的遍歷,而MARCO-MAM方法則將步驟減少為3步.MARCO-MAM方法在節(jié)省生成Seed的求解器調(diào)用的同時,也利用求解得到的MSS對Map進(jìn)行剪枝,使問題在縮減后的求解空間上進(jìn)行求解,進(jìn)而節(jié)省總求解時間.

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

本節(jié)將對MARCO-MAM方法與MARCO-M方法進(jìn)行比較,并給出2種方法在同樣測試用例下的實(shí)驗(yàn)結(jié)果.實(shí)驗(yàn)平臺為：64位Ubantu 16.04.3 LTS系統(tǒng),Intel?CoreTMi5-3470 CPU@3.20 GHz×4.MARCO-MAM方法使用的編程語言為Python,調(diào)用C++編寫的MUS提取器MUSer2以及MiniSat,其中我們使用到的MiniSat是未經(jīng)修改的MiniSat求解器[18],本次實(shí)驗(yàn)測試用例選用MARCO-M方法[20]所用的標(biāo)準(zhǔn)測試用例見http://www.cril.univ-artois.fr/SAT11/.

表1中列1為測試用例名稱,測試選取的求解限定時間分別為2 h,4 h,6 h,8 h,10 h,12 h;列2是MARCO-M方法在各限定求解時間內(nèi)得到MUS的個數(shù);列3是MARCO-MAM方法在各限定求解時間內(nèi)得到MUS的個數(shù);為直觀表達(dá)求解效果更優(yōu)的方法，對表1中MARCO-M方法與MARCO-MAM方法求解得到的MUS較多的個數(shù)用黑體表示(相同個數(shù)未做標(biāo)記).從表1中可以看到MARCO-MAM方法在限定時間內(nèi)大多數(shù)實(shí)例求得解的個數(shù)都優(yōu)于MARCO-M方法.

Table 1 Comparison of Enumerating MUS Numbers Between MARCO-MAM Method and MARCO-M Method Under Different Execution Time Limits表1 MARCO-MAM方法與MARCO-M方法在不同執(zhí)行時間限制下枚舉MUS個數(shù)的比較

Continued (Table 1)

Note:The data of the unadded unit in the table is the number of MUS solutions,and the time for limiting execution is 2 h,4 h,6 h,8 h,10 h,12 h.Data in bold represent more solutions obtained by this method than the other method.

Fig.3 The difference in number of MUS enumeration between MARCO-MAM method and MARCO-M method at different execution times圖3 MARCO-MAM方法與MARCO-M方法在不同執(zhí)行時間下枚舉MUS的數(shù)量差

圖2和圖3給出了MARCO -M方法與MARCO -MAM方法在不同時間下求解MUS數(shù)量的差值,其中差值是MARCO-MAM方法求解MUS個數(shù)減去MARCO-M方法求解的MUS數(shù)量.在圖3中,差值大于0的數(shù)據(jù)點(diǎn)為MARCO-MAM方法更優(yōu),差值小于0的數(shù)據(jù)點(diǎn)為MARCO-M方法更優(yōu).

在圖2中絕大多數(shù)點(diǎn)都在坐標(biāo)軸上方即表示MARCO-MAM方法求解出的MUS數(shù)量更多,還有一些點(diǎn)在0刻度線上下浮動,即為與MARCO-M方法相差較小的數(shù)據(jù)點(diǎn).

在坐標(biāo)軸下方少量的點(diǎn)表示有極少情況下MARCO-MAM方法求解MUS數(shù)量是少于MARCO-M方法的,這是由于MARCO-MAM方法一部分時間花費(fèi)在求解中間模型MSS上,即在同一時刻MUS個數(shù)少于MARCO-M方法.

Fig.2 The difference in number of MUS enumeration between MARCO-MAM method and MARCO-M method圖2 MARCO-MAM方法與MARCO-M方法枚舉MUS的數(shù)量差

圖3給出了時間限定分別在1 h,6 h,12 h求解到的MUS數(shù)量差作為表中數(shù)據(jù)點(diǎn).從圖3(a)中可以看出,在1 h以內(nèi),2種方法效率差別不大,MARCO-MAM方法要稍優(yōu)于MARCO-M方法;在圖3(b)中,6 h以內(nèi)求解得到的MUS數(shù)量差較大,在圖3(c)中,12 h的時間限制下,MARCO-MAM方法要比MARCO-M方法得到的MUS解數(shù)量多近120個解.

MARCO-MAM方法使得MUS的求解越來越快,這得益于MSS的輔助求解及返回2個Seed的模型求解方式,這種方式減少了近一半的因得到Seed模型而調(diào)用求解器的次數(shù),進(jìn)而節(jié)省了求解時間.

5 結(jié)束語

在對MARCO-M方法深入研究的基礎(chǔ)上,針對MARCO-M方法單一極大化模型求解MUS時未有效利用其他優(yōu)化技術(shù)對求解空間進(jìn)行剪枝的不足,給出基于雙模型的MARCO-MAM方法求解MUS.對于MARCO-M方法每次調(diào)用求解器只能得到單一模型的問題,MARCO-MAM方法采用了雙模型交替的方式,使得求解器返回1個極大化模型及1個中間模型.對中間模型進(jìn)行求解得到MSS時,利用MSS對應(yīng)的阻塞空間來對MUS搜索空間進(jìn)行剪枝,進(jìn)而提高M(jìn)US求解效率;如果中間模型進(jìn)行求解得到MUS時,則減少了MARCO-M方法中MUS的不可滿足迭代求解次數(shù).實(shí)驗(yàn)結(jié)果表明,在剛開始求解時由于MARCO-MAM一部分時間花費(fèi)在利用中間模型求解MSS上,此時MUS個數(shù)可能會少于MARCO-M方法,但隨著求得MSS對應(yīng)的空間逐漸對MUS搜索空間進(jìn)行剪枝和減少M(fèi)US求解時不可滿足迭代求解次數(shù),MARCO-MAM方法求解效率越來越高,尤其在大規(guī)模問題或較大搜索空間時MARCO-MAM方法效率提高更為明顯.