基于動(dòng)態(tài)獎(jiǎng)懲的分支策略的SAT完備算法

劉燕麗，徐振興，熊 丹

(1.武漢科技大學(xué) 理學(xué)院，武漢 430081； 2.華中科技大學(xué) 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，武漢 430074)

基于動(dòng)態(tài)獎(jiǎng)懲的分支策略的SAT完備算法

劉燕麗1,2*，徐振興2，熊 丹1

(1.武漢科技大學(xué) 理學(xué)院，武漢 430081； 2.華中科技大學(xué) 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，武漢 430074)

針對(duì)學(xué)習(xí)子句數(shù)量有限或相似度高導(dǎo)致歷史信息有限、搜索樹(shù)不平衡的問(wèn)題，提出了基于動(dòng)態(tài)獎(jiǎng)懲的分支策略。首先，對(duì)每次單子句傳播的變?cè)M(jìn)行懲罰，依據(jù)變?cè)欠癞a(chǎn)生沖突和產(chǎn)生沖突的間隔，確立不同的懲罰函數(shù);其次，在學(xué)習(xí)階段，利用學(xué)習(xí)子句確定對(duì)構(gòu)造沖突有益的變?cè)蔷€性增加它們的活躍度;最后，選擇活躍度最大的變?cè)鳛樾路种ё冊(cè)Ｔ趃lucose3.0算法基礎(chǔ)上，完成了改進(jìn)的動(dòng)態(tài)獎(jiǎng)懲算法——AP7。實(shí)驗(yàn)結(jié)果表明，相比glucose3.0算法，AP7算法的剪枝率提高了14.2%～29.3%，少數(shù)算例剪枝率的提高可達(dá)51%，且改進(jìn)后的AP7算法相比glucose3.0算法，運(yùn)行時(shí)間縮短了7%以上。所提分支策略可以有效降低搜索樹(shù)規(guī)模，使搜索樹(shù)更加平衡，減少計(jì)算時(shí)間。

NP完全問(wèn)題；可滿足性問(wèn)題；沖突驅(qū)動(dòng)子句學(xué)習(xí)；完備算法；分支策略

0 引言

可滿足性問(wèn)題(SATisfiability problem, SAT)是計(jì)算機(jī)科學(xué)領(lǐng)域經(jīng)典的NP問(wèn)題(Non-deterministic Polynomial Complete problem, NPC)，在計(jì)算機(jī)科學(xué)理論中占有非常重要的地位?，F(xiàn)實(shí)世界的問(wèn)題大多數(shù)都是NP問(wèn)題，即不確定性問(wèn)題。比如，超大規(guī)模集成電路測(cè)試、資源配置、網(wǎng)絡(luò)的搜索、數(shù)據(jù)挖掘、城市交通等，解決這些工業(yè)問(wèn)題的SAT技術(shù)推動(dòng)了人工智能的重要發(fā)展。

目前，絕大多數(shù)SAT完備算法是基于深度遍歷二叉樹(shù)的DPLL(Davis Putnam Logemann Loveland)[1]算法。2001年Moskewicz等[2]提出的沖突驅(qū)動(dòng)子句學(xué)習(xí)(Conflict Driven Clause Learning, CDCL)，使得SAT求解效率有了標(biāo)志性的進(jìn)步，在合理時(shí)間內(nèi)，求解規(guī)模從數(shù)百個(gè)變?cè)?，擴(kuò)大到數(shù)萬(wàn)個(gè)變?cè)?。后續(xù)提出的SAT完備算法的主要方法和改進(jìn)[3-4]均基于沖突驅(qū)動(dòng)子句學(xué)習(xí)技術(shù)。比如，非時(shí)間序列回溯(Non-chronological Backtracking, NCB)[5]，該策略分析沖突的產(chǎn)生原因，記錄優(yōu)化的學(xué)習(xí)子句，并在回溯后，優(yōu)先滿足學(xué)習(xí)子句，以避免再次陷入相同沖突。文字塊距離(Literal Block Distance, LBD)[6]是統(tǒng)計(jì)學(xué)習(xí)子句中不同分支層的變?cè)獢?shù)，是一個(gè)動(dòng)態(tài)變化值。子句庫(kù)始終保留二元學(xué)習(xí)子句或LBD值小的學(xué)習(xí)子句。該策略既避免了因?qū)W習(xí)子句劇增而內(nèi)存崩潰的危險(xiǎn)，又保留了質(zhì)量高的變?cè)s束條件，是有效的子句刪除策略。

變?cè)?dú)立衰減 (Variables State Independent Decaying Sum, VSIDS)[7]分支策略強(qiáng)化了沖突學(xué)習(xí)對(duì)搜索的影響。一旦變?cè)诋a(chǎn)生學(xué)習(xí)子句的過(guò)程中出現(xiàn)，那么該變?cè)幕钴S度將非線性增加。近幾年的SAT競(jìng)賽數(shù)據(jù)顯示變?cè)?dú)立衰減策略或者其變種是較為高效的分支策略。動(dòng)態(tài)重啟(Dynamic Restart, DR)[8]是當(dāng)算法較長(zhǎng)時(shí)間不能找到?jīng)_突時(shí)，程序撤銷之前的搜索動(dòng)作，重新開(kāi)始遍歷二叉樹(shù)。因?yàn)樾滤阉魇窃诤袑W(xué)習(xí)子句的子句庫(kù)中進(jìn)行，學(xué)習(xí)子句代表了之前的搜索信息，所以重啟并不是推翻之前的搜索。目前，工業(yè)算例的規(guī)?？蛇_(dá)百萬(wàn)個(gè)變?cè)獢?shù)，千萬(wàn)個(gè)子句數(shù)。因?yàn)閱?wèn)題的復(fù)雜度高，量化這些策略在搜索過(guò)程中的作用，以及它們之間的相互影響，是非常困難的事情。

本文針對(duì)在搜索空間為2n(n是變?cè)獢?shù))的二叉樹(shù)中，由于學(xué)習(xí)子句數(shù)量有限，或?qū)W習(xí)子句相似度高而導(dǎo)致搜索樹(shù)層次過(guò)深、計(jì)算效率低的問(wèn)題，提出了雙階段評(píng)分的新分支策略。即對(duì)于搜索階段傳播的變?cè)羝鋵?duì)構(gòu)造沖突作用小，則給予適當(dāng)?shù)膽土P；對(duì)于學(xué)習(xí)階段中構(gòu)建沖突的變?cè)o予獎(jiǎng)勵(lì)，通過(guò)較為全面地評(píng)估變?cè)獙?duì)搜索的影響，以達(dá)到更快地發(fā)現(xiàn)沖突，提高剪枝率的目標(biāo)。計(jì)算了SAT國(guó)際競(jìng)賽的工業(yè)組算例，實(shí)驗(yàn)結(jié)果表明新變?cè)x擇策略可有效地調(diào)整搜索樹(shù)的高度，縮短運(yùn)算時(shí)間。

1 可滿足性問(wèn)題的求解

文獻(xiàn)[9]給出了可滿足性問(wèn)題的相關(guān)術(shù)語(yǔ)的定義。

1.1 相關(guān)術(shù)語(yǔ)

定義2 子句集。子句是V上若干文字的析取，記為c。子句集是由若干子句構(gòu)成的集合，記為C。子句長(zhǎng)度是子句所含文字的個(gè)數(shù)，記為|c|。特別地，長(zhǎng)度為1的子句稱為單子句。長(zhǎng)度為0的子句稱為空子句，記為δ。

定義3 子句滿足。若子句滿足當(dāng)且僅當(dāng)子句中至少有1個(gè)文字為true。因不含有任何文字，所以空子句永遠(yuǎn)不滿足。若子句不滿足當(dāng)且僅當(dāng)子句中所有文字均為false，該子句又稱為沖突子句，記為□。

定義4 合取范式。 合取范式(Conjunctive Normal Formula, CNF)是由若干V上的子句合取構(gòu)成的命題公式，記為F。

定義5 真值指派。 真值指派是命題變?cè)猇′→{1,0}的映射，V′?V，記為A。當(dāng)V′=V時(shí)，A是完整真值指派；否則，稱之為部分真值指派。

定義6 沖突集。 對(duì)任意一組V上的真值指派，若子句集C中至少含有1個(gè)不滿足子句，則稱C為沖突集，記為Φ。若兩個(gè)沖突集的交為空，則稱它們是相互獨(dú)立的。

定義7 SAT問(wèn)題。 對(duì)于命題變?cè)蟅和子句集C，判定是否存在一組關(guān)于V的真值指派使得C中所有子句滿足。

1.2 SAT問(wèn)題的完備算法

目前，DPLL是絕大多數(shù)SAT完備算法的主流程的控制程序。算法從根節(jié)點(diǎn)開(kāi)始深度遍歷二叉樹(shù)，當(dāng)遇到?jīng)_突的真值指派時(shí)，算法回溯。若算法找到一組真值指派，使得每個(gè)子句滿足，那么程序終止，返回“可滿足”。若遍歷完完整的二叉樹(shù)后，未找到一組真值指派使得所有子句滿足，那么程序終止，返回“不可滿足”。DPLL算法詳見(jiàn)文獻(xiàn)[1]。

1)測(cè)試沖突的單子句傳播。

單子句傳播(Unit Propagation)[9-10]可以幫助SAT算法推導(dǎo)出真值指派的沖突，減少搜索空間。算法1是單子句傳播的具體過(guò)程。

算法1 UnitPropagate(F)。

輸入 合取范式F；

輸出 若有沖突，返回沖突子句，否則返回NoConflict。

1)

F′←F

2)

do {

3)

取UnitQue中單子句cj，滿足cj的文字l；

4)

形如l∨li…∨lk的子句已滿足，從F′中移除；

5)

6)

if (lm∨ls…∨lt為單子句)

7)

lm∨ls…∨lt入U(xiǎn)nitQue隊(duì)列；

8)

else if (lm∨ls…∨lt為空子句)

9)

returncn；

10)

}while(UnitQue不為空)

11)

return NoConflict

圖1 F的邏輯蘊(yùn)含圖Fig. 1 Logical implication graph of F

2)學(xué)習(xí)子句的產(chǎn)生。

當(dāng)搜索到?jīng)_突后，SAT算法進(jìn)入分析沖突的原因，產(chǎn)生學(xué)習(xí)子句的學(xué)習(xí)階段。圖2顯示了由沖突子句出發(fā)，通過(guò)消解規(guī)則，逐一產(chǎn)生學(xué)習(xí)子句的過(guò)程。消解規(guī)則是若兩個(gè)子句中包含有相反文字，則將這對(duì)文字刪除，剩余文字通過(guò)析取構(gòu)成新的子句。消解規(guī)則不改變合取范式的滿足性。

圖2 學(xué)習(xí)子句的產(chǎn)生過(guò)程Fig. 2 Generation process of learning clauses

2 基于動(dòng)態(tài)獎(jiǎng)懲分支策略的SAT算法

DPLL+子句學(xué)習(xí)是SAT完備算法的基礎(chǔ)。為了減少搜索樹(shù)的節(jié)點(diǎn)數(shù)，提高算法的效率，分支策略將選擇對(duì)搜索樹(shù)規(guī)模影響大的變?cè)?/p>

2.1 基于學(xué)習(xí)過(guò)程的變?cè)呗?/h3>

如變?cè)?dú)立衰減策略或其變種，這類基于學(xué)習(xí)過(guò)程的分支策略是在產(chǎn)生學(xué)習(xí)子句的學(xué)習(xí)階段，對(duì)參與消解操作的所有子句包含的變?cè)?，增大其活躍度。算法始終選擇當(dāng)前活躍度最大的變?cè)鳛樾碌姆种c(diǎn)。如例1會(huì)增加變?cè)獂5、x9、x11、x23、x2、x15的活躍度。變?cè)獏⑴c構(gòu)造沖突越多，其活躍度越大。在后續(xù)搜索中選擇活躍度大的變?cè)?，易找到之前發(fā)現(xiàn)過(guò)的沖突，有利于減少搜索路徑。

我們發(fā)現(xiàn)僅基于學(xué)習(xí)過(guò)程的分支策略對(duì)減小搜索樹(shù)規(guī)模并不總是有效的。某些情況下，相似的學(xué)習(xí)過(guò)程導(dǎo)致學(xué)習(xí)子句相似度高。學(xué)習(xí)子句代表的搜索的歷史信息比較集中，回溯后或重啟后，基于學(xué)習(xí)過(guò)程的變?cè)呗詴?huì)僅有少量變?cè)梢詢?yōu)先選擇。搜索沒(méi)有足夠的歷史信息指引方向，會(huì)隨機(jī)去選擇變?cè)鳛樾碌姆种Ч?jié)點(diǎn)，這會(huì)導(dǎo)致搜索樹(shù)層次過(guò)深，算法陷入困境。目前，絕大多數(shù)SAT求解器采用動(dòng)態(tài)重啟逃脫這種困境。因?yàn)樽泳鋷?kù)保存了表述沖突關(guān)系的學(xué)習(xí)子句，所以重啟后的搜索與沒(méi)有學(xué)習(xí)信息的原始搜索不同。通過(guò)優(yōu)先選擇沖突關(guān)系多的變?cè)?，新搜索可能?huì)找到?jīng)_突。但是動(dòng)態(tài)重啟只能緩和算法遇到的問(wèn)題，并未改變變?cè)幕钴S度，程序可能會(huì)又陷入到某一子樹(shù)的過(guò)度搜索中。

2.2 基于學(xué)習(xí)與搜索雙階段的分支策略

為了減少搜索樹(shù)規(guī)模，使搜索樹(shù)更加平衡，全面地評(píng)估變?cè)獙?duì)搜索的作用，使得越容易構(gòu)造沖突的變?cè)浇咏鼧?shù)根，增大搜索優(yōu)先找到?jīng)_突的概率是基于動(dòng)態(tài)獎(jiǎng)懲分支策略的獎(jiǎng)懲算法——AP7(Award and Punishment 7)的主要改進(jìn)思路。

SAT完備算法包括2個(gè)主要過(guò)程：一是搜索過(guò)程，即單子句傳播，發(fā)現(xiàn)沖突的操作；二是學(xué)習(xí)過(guò)程，即產(chǎn)生學(xué)習(xí)子句，增加沖突變?cè)幕钴S度，確定回溯層次。AP7算法對(duì)以上兩個(gè)過(guò)程中的變?cè)M(jìn)行全面的評(píng)估。在搜索階段，降低較長(zhǎng)時(shí)間內(nèi)未找到?jīng)_突的變?cè)幕钴S度，在學(xué)習(xí)階段，提高對(duì)構(gòu)造沖突有益的變?cè)幕钴S度，并優(yōu)先選擇當(dāng)前活躍度最大的變?cè)鳛榉种ё冊(cè)?。算法流程如圖3所示。

算法2是AP7的偽代碼。算法中penalty是讓變?cè)钴S度隨著傳播而衰減的獨(dú)立參數(shù)；numCC是沖突數(shù)，初始值為0；penaltyV是存儲(chǔ)待懲罰變?cè)臄?shù)組；dl是搜索樹(shù)的層數(shù)；lastC[x]是存放變?cè)獂的最近一次出現(xiàn)的沖突；Act是記錄變?cè)獂活躍度的數(shù)組；ΦL是學(xué)習(xí)子句L對(duì)應(yīng)的沖突集，Variable(ΦL)是沖突集中出現(xiàn)的所有變?cè)募?；V是輸入算例的變?cè)?；BranchV是分支變?cè)?；max函數(shù)返回活躍度最大的變?cè)?；bl是SAT算法產(chǎn)生沖突后的回溯層次；AP7采用非時(shí)間序列回溯的方法；cancel函數(shù)是算法回溯到指定的層次。

圖3 AP7算法流程Fig. 3 AP7 algorithm flowchart

算法2 AP7(F)。

輸入 合取范式F；

輸出F是否滿足，滿足返回“SAT”，不滿足返回“UNSAT”。

1)

penalty=0.6;numCC=0;penaltyV.clear();

2)

for(;;)

3)

UnitPropagate(F)且將傳播的變?cè)獂壓入penaltyV中；

4)

forxt∈penaltyVdo

//搜索階段的懲罰

5)

if UnitPropagate(F)==沖突 then

6)

ifpenalty<0.98 then

7)

penalty=penalty+10-7;

8)

end if

9)

Act[xt]=Act[xt]*penalty+(1-penalty)/(numCC-

lastC[xt]);

10)

else

11)

Act[xt]=Act[xt]*penalty;

12)

end if

13)

end for

//結(jié)束懲罰計(jì)算

14)

penaltyV.clear();

15)

if UnitPropagate(F)==沖突 then

//找到?jīng)_突

16)

ifdl==0 then

17)

return "UNSAT";

18)

end if

19)

numCC++;

20)

FUIP方式產(chǎn)生學(xué)習(xí)子句L,并返回回溯層次bl；

21)

forxi∈Variable(ΦL) do

//學(xué)習(xí)階段的獎(jiǎng)勵(lì)

22)

lastC[xi]=numCC;

23)

Act[xi]=Act[xi]+(1/0.9)numCC

24)

ifAct[xi] >1E100 then

25)

forxi∈Vdo

26)

Act[xi]*=1E-100;

//作平滑

27)

end for

28)

end if

29)

end for

//學(xué)習(xí)階段獎(jiǎng)勵(lì)結(jié)束

30)

cancel(bl);

31)

翻轉(zhuǎn)學(xué)習(xí)子句L中未滿足的文字；

32)

else

//未找到?jīng)_突

33)

BranchV=max(Act[xk]);xk∈V

34)

if 所有變?cè)加辛苏嬷抵概?then

35)

return "SAT";

36)

end if

37)

dl++;

38)

BranchV壓入penaltyV;

39)

end if

40)

end for

AP7首先作單子句傳播，將單子句傳播中所有變?cè)獕喝雙enaltyV中，如果這些變?cè)恼嬷抵概芍g沒(méi)有沖突，那么將它們的活躍度降低至60%～98%；如果這些變?cè)g有沖突那么除了適當(dāng)?shù)慕o予懲罰之外，還給予少量的獎(jiǎng)勵(lì)。以上是傳播階段變?cè)幕钴S度計(jì)算。

如果單子句傳播發(fā)現(xiàn)了沖突，且當(dāng)前搜索層次是第0層，那么SAT問(wèn)題無(wú)解，返回“UNSAT”；如果當(dāng)前層次不是第0層，則AP7對(duì)沖突進(jìn)行分析，采用FUIP方式產(chǎn)生學(xué)習(xí)子句，確定回溯層次bl。在學(xué)習(xí)子句對(duì)應(yīng)的沖突集中出現(xiàn)的變?cè)?，其活躍度會(huì)得到大小為(1/0.9)numCC的獎(jiǎng)勵(lì)。AP7對(duì)構(gòu)造沖突的變?cè)M(jìn)行獎(jiǎng)勵(lì)后，開(kāi)始回溯，撤銷第bl+1層到當(dāng)前層傳播的變?cè)?。因?yàn)榛厮莺蟮膶W(xué)習(xí)子句是單子句，所以滿足學(xué)習(xí)子句，進(jìn)入到新的一輪單子句傳播。

如果單子句傳播未發(fā)現(xiàn)沖突，則AP7選擇活躍度最大且未賦值的變?cè)鳛榉种ё冊(cè)?。分支層次增?，分支變?cè)獕喝雙enaltyV中。AP7開(kāi)始新的一輪單子句傳播。如果所有變?cè)哂泻侠淼恼嬷抵概?，沒(méi)有未賦值的變?cè)敲碅P7找到了問(wèn)題的解，算法返回“SAT”。

學(xué)習(xí)階段對(duì)變?cè)莫?jiǎng)勵(lì)值不是固定值，該值隨著搜索層次的加深，獎(jiǎng)勵(lì)值越大。為了防止活躍度值的溢出，當(dāng)某個(gè)變?cè)幕钴S度大于閾值1E100時(shí)，變?cè)幕钴S度整體地平滑下降。搜索階段實(shí)施懲罰時(shí)需注意以下幾個(gè)問(wèn)題：1)降低活躍度的penalty不是一個(gè)固定值。算法找到越多的沖突，活躍度降低得越少。這是因?yàn)樽罱业降臎_突很大概率上質(zhì)量會(huì)比之前的沖突要好。2)當(dāng)搜索找到?jīng)_突時(shí)，增加了一個(gè)變量1/(numCC-lastC[xt])。若某個(gè)變?cè)欢螘r(shí)間之后，再次找到了沖突，那么它與長(zhǎng)時(shí)間未有沖突的變?cè)啾龋钴S度應(yīng)該高一些。3)當(dāng)搜索沒(méi)有找到?jīng)_突時(shí)，直接大幅度降低變?cè)幕钴S度。雖然這種方式比較野蠻，但是對(duì)于復(fù)雜的問(wèn)題，它是有效的。

3 新分支策略的評(píng)估

3.1 實(shí)驗(yàn)環(huán)境和設(shè)置

為了準(zhǔn)確評(píng)估新分支策略在求解工業(yè)問(wèn)題上的作用，實(shí)驗(yàn)對(duì)比了新算法AP7和glucose3.0。兩者僅分支策略不同，AP7采用的是基于獎(jiǎng)懲的新策略，而glucose3.0是基于學(xué)習(xí)過(guò)程的變?cè)?dú)立衰減分支策略。在SAT競(jìng)賽的工業(yè)組中，glucose算法及其變種[12]有重要的地位。glucose2.3算法是2013年競(jìng)賽的工業(yè)組冠軍，獲得2014年—2016年工業(yè)組前三名的算法均是以glucose3.0為基礎(chǔ)的；同時(shí)，glucose被SAT組委會(huì)用于確定算例的難度等級(jí)。

實(shí)驗(yàn)的機(jī)器配置采用Intel E5 2.7 GHz處理器、32 GB內(nèi)存、Centos 6.3服務(wù)器版本的操作系統(tǒng)。在相同的機(jī)器上，AP7算法和glucose3.0算法求解2016年SAT Competition (http://www.satcompetition.org) 公布的工業(yè)算例集。這些算例來(lái)自軟件測(cè)試、調(diào)度、硬件電路測(cè)試、網(wǎng)絡(luò)安全、加密算法等實(shí)際問(wèn)題。根據(jù)算例的解的滿足性，這些算例被分為可滿足算例集和不可滿足算例集。實(shí)驗(yàn)采用SAT競(jìng)賽的限定時(shí)間，每個(gè)算例的運(yùn)算不超過(guò)5 000 s，若超出，該算例結(jié)果記為unsolved。

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

首先給出glucose3.0和AP7算法在相同機(jī)器上計(jì)算相同算例的時(shí)間結(jié)果。glucose3.0和AP7算法計(jì)算加密安全哈希算法(Secure Hash Algorithm, SHA)、矩形裝配、交通規(guī)劃等工業(yè)問(wèn)題的運(yùn)算時(shí)間如表1所示。表1中算例的變?cè)獢?shù)是13 408～521 147，子句數(shù)是308 391～13 378 009。表1顯示，在27個(gè)算例中AP7算法有22個(gè)算例運(yùn)行時(shí)間少于glucose3.0，AP7算法相比glucose3.0計(jì)算可滿足算例的運(yùn)行總時(shí)間縮短了31.66%。

表1 不同算法可滿足算例的運(yùn)行時(shí)間對(duì)比 sTab. 1 Running time comparison of SAT examples for different algorithms s

glucose3.0和AP7算法計(jì)算硬件電路優(yōu)化、電子控制等工業(yè)問(wèn)題的運(yùn)算時(shí)間對(duì)比如表2所示。表2中算例的變?cè)獢?shù)是3 295～89 315，子句數(shù)是13 079～5 584 002。 glucose3.0在5 000 s限定時(shí)間內(nèi)，未求解出表2的第1個(gè)算例smtlib-qfbv-aigs-ext_con_032_008_0256-tseitin，該算例在競(jìng)賽網(wǎng)站公布的最好成績(jī)是Lingeling(druplig)算法的1.432 s。根據(jù)表2中AP7和glcuose3.0均計(jì)算出結(jié)果的21個(gè)算例，有17個(gè)算例AP7算法運(yùn)算時(shí)間少于glucose3.0，AP7算法的運(yùn)行總時(shí)間比glucose3.0縮短了37.13%。

表2 不同算法不可滿足算例的運(yùn)行時(shí)間對(duì)比 sTab.2 Running time comparison of UNSAT examples for different algorithms s

3.3 實(shí)驗(yàn)結(jié)果分析

分支數(shù)是SAT完備算法效率的核心參數(shù)。當(dāng)搜索樹(shù)分支減少，搜索空間減小，SAT完備算法的運(yùn)算時(shí)間才會(huì)降低。

glucose3.0和AP7計(jì)算的部分算例的分支數(shù)以及降低比如表3所示。降低比=(glucose3.0分支數(shù)-AP7分支數(shù))/(glucose3.0分支數(shù))。

表3 不同算法算例的分支數(shù)對(duì)比Tab. 3 Branch number comparison for different algorithms and examples

從表3可以看出，除1個(gè)算例外，改進(jìn)后的AP7相比glucose3.0可降低分支數(shù)為14.2%～56.5%。通過(guò)表3實(shí)驗(yàn)數(shù)據(jù)可知基于獎(jiǎng)懲的分支策略相比僅增加變?cè)钴S度的分支策略可以有效地減小搜索樹(shù)規(guī)模。

為了進(jìn)一步觀察動(dòng)態(tài)獎(jiǎng)懲策略對(duì)搜索沖突的影響，每增長(zhǎng)1萬(wàn)個(gè)沖突時(shí)，算法輸出重啟的次數(shù)。圖4～5 對(duì)比了兩個(gè)算法計(jì)算相同算例時(shí)，相同沖突數(shù)下所需的重啟次數(shù)。glucose3.0計(jì)算002- 80- 12.cnf重啟了103 921次，找到13 841 064次沖突；AP7則重啟了67 927次，找到10 633 140次沖突。圖4顯示在0～10 633 140次沖突時(shí)，兩個(gè)算法相應(yīng)的重啟次數(shù)。AP7和glucose3.0采用相同的重啟策略。在0～105萬(wàn)次沖突搜索中，glucose3.0比AP7重啟次數(shù)少；在105萬(wàn)～1 384萬(wàn)次沖突中，AP7重啟次數(shù)少于glucose3.0。實(shí)驗(yàn)結(jié)果表明AP7算法綜合地評(píng)定變?cè)谒阉髦械淖饔茫捎行У販p少較長(zhǎng)時(shí)間找不到?jīng)_突的情況，從而減少了重啟次數(shù)。

圖4 可滿足002- 80- 12.cnf的重啟次數(shù)和沖突數(shù)的對(duì)比Fig. 4 Comparison of conflicts and restarts of SAT 002- 80- 12.cnf

glucose3.0計(jì)算不可滿足算例6s168-opt.cnf的沖突數(shù)是2 063 558，重啟次數(shù)是4 758；AP7計(jì)算該算例的沖突數(shù)是1 084 645，重啟次數(shù)是2 059。圖5顯示了6s168-opt.cnf在0～120萬(wàn)次沖突范圍內(nèi)兩個(gè)算法的重啟次數(shù)的對(duì)比。從圖5可以看出，產(chǎn)生相同個(gè)數(shù)的沖突時(shí)，AP7的重啟次數(shù)遠(yuǎn)低于glucose3.0算法的重啟次數(shù)。因此，基于獎(jiǎng)懲的分支策略AP7對(duì)于不可滿足的工業(yè)問(wèn)題，也可以有效地減少搜索樹(shù)層次，從而減少重啟次數(shù)。

圖5 不可滿足6s168-opt.cnf的沖突數(shù)和重啟數(shù)的對(duì)比Fig. 5 Comparison of conflicts and restarts of UNSAT 6s168-opt.cnf

從學(xué)習(xí)子句質(zhì)量進(jìn)一步分析新分支策略的作用。SAT完備算法每次找到1個(gè)沖突，產(chǎn)生1個(gè)學(xué)習(xí)子句。每個(gè)學(xué)習(xí)子句會(huì)計(jì)算其相應(yīng)的LBD值，LBD值為2的學(xué)習(xí)子句是指產(chǎn)生沖突的原因子句分布在搜索樹(shù)的2個(gè)層次。因?yàn)長(zhǎng)BD值為2的學(xué)習(xí)子句描述了關(guān)系更為緊密的沖突變?cè)g的關(guān)系，所以質(zhì)量高的這類學(xué)習(xí)子句一直保留在子句庫(kù)中，不會(huì)被刪除。表4列出了glucose3.0和AP7算法正確求解的算例的重啟次數(shù)，LBD_2學(xué)習(xí)子句數(shù)以及LBD_2學(xué)習(xí)子句數(shù)與重啟次數(shù)的比例。若LBD_2學(xué)習(xí)子句數(shù)與重啟次數(shù)的比例越大，說(shuō)明重啟后被選擇的搜索變?cè)P(guān)系更加緊密，導(dǎo)致找到?jīng)_突后學(xué)習(xí)子句的LBD值下降。表4顯示在重啟次數(shù)較小時(shí)(重啟次數(shù)<150)glucose3.0算法重啟的平均學(xué)習(xí)質(zhì)量較高，但是求解復(fù)雜的問(wèn)題(重啟次數(shù)>150)AP7算法的平均學(xué)習(xí)質(zhì)量較高。這表明綜合評(píng)定變?cè)梢援a(chǎn)生更多高質(zhì)量學(xué)習(xí)子句。

表4 不同算例的重啟次數(shù)、LBD_2子句數(shù)的對(duì)比Tab. 4 Comparison of number of restarts and LBD_2 clauses for different examples

4 結(jié)語(yǔ)

工業(yè)問(wèn)題規(guī)模大，求解難度高。學(xué)習(xí)子句數(shù)量少或質(zhì)量不高對(duì)搜索的指導(dǎo)意義有限，使搜索易陷入到層次過(guò)高，不平衡的困境中。為了縮短求解問(wèn)題的時(shí)間，算法需要盡可能地選擇對(duì)尋找沖突更有利的變?cè)?，以使得搜索?shù)更加平衡?；趧?dòng)態(tài)獎(jiǎng)懲的分支策略綜合地評(píng)估了變?cè)獙?duì)傳播和學(xué)習(xí)兩個(gè)主要過(guò)程的影響，建立懲罰函數(shù)。相比傳統(tǒng)、單一的獎(jiǎng)勵(lì)變?cè)u(píng)估策略，動(dòng)態(tài)獎(jiǎng)懲的分支策略通過(guò)調(diào)整更關(guān)鍵的變?cè)拷?jié)點(diǎn)，從而有效地降低重啟次數(shù)，提高了學(xué)習(xí)子句質(zhì)量，減小搜索樹(shù)的規(guī)模。分支變?cè)呗缘母淖兪沟盟阉鳂?shù)更加緊湊，將會(huì)影響子句刪除的標(biāo)準(zhǔn)，后續(xù)將對(duì)學(xué)習(xí)子句的刪除作新的探索。

References)

[1] DAVIS M, LOGEMANN G, LOVELAND D. A machine program for theorem proving [J]. Communications of the ACM, 1962, 5(7): 394-397.

[2] MOSKEWICZ M W, MADIGAN C F, ZHAO Y, et al. Chaff: engineering an efficient sat solver [C]// Proceedings of the 38th Annual Design Automation Conference. New York: ACM, 2001: 530-535.

[4] KOSHIMURA M, ZHANG T, FUJITA H, et al. QMaxSAT: a partial Max-SAT solver system description [J]. Journal on Satisfiability, Boolean Modeling and Computation, 2012, 8(1/2): 95-100.

[5] ZHANG L T, MADIGAN C F, MOSKEWICZ M H, et al. Efficient conflict driven learning in a boolean satisfiability solver [C]// ICCAD 2001: Proceedings of the 2001 IEEE/ACM International Conference on Computer-Aided Design. Piscataway, NJ: IEEE, 2001: 279-285.

[6] LIU Y L, LI C M, HE K, et al. Breaking cycle structure to improve lower bound for Max-SAT [C]// FAW 2016: Proceeding of the 11th International Workshop on Frontiers in Algorithmics, LNCS 9711. Berlin: Springer, 2016: 111-124.

[7] AUDEMARD G, SIMON L. Predicting learnt clauses quality in modern SAT solvers [C]// IJCAI 2009: Proceeding of the 2009 International Joint Conference on Artificial Intelligence. San Francisco, CA: Morgan Kaufmann, 2009: 399-404.

[8] AUDEMARD G, LAGNIEZ J M, SIMON L. Improving glucose for incremental SAT solving with assumption: application to MUS extraction [C]// SAT 2013: Proceedings of the 16th International Conference on Theory and Applications of Satisfiability Testing. Berlin: Springer, 2013: 309-317.

[9] DE KLERK E. Aspects of Semidefinite Programming [M]. Berlin: Springer, 2002: 211-228.

[10] 劉燕麗,李初民,何琨.基于優(yōu)化沖突集提高下界的MaxSAT完備算法[J].計(jì)算機(jī)學(xué)報(bào),2013,36(10):2087-2095.(LIU Y L, LI C M, HE K. Improved lower bounds in MAXSAT complete algorithm based optimizing inconsistent set [J]. Chinese Journal of Computers, 2013, 36(10): 2087-2095.)

[11] 劉燕麗,黃飛,張婷.基于環(huán)型擴(kuò)展推理規(guī)則的MaxSAT完備算法[J].南京大學(xué)學(xué)報(bào)(自然科學(xué)版),2015,51(4):762-771.(LIU Y L, HUANG F, ZHANG T. MaxSAT complete algorithm based cycle extended inference rules [J]. Journal of Nanjing University (Natural Sciences), 2015, 51(4): 762-771.)

[12] AUDEMARD G, SIMON L. Lazy clause exchange policy for parallel SAT solvers [C]// SAT 2014: Proceedings of the 2014 17th International Conference on Theory and Applications of Satisfiability Testing, LNCS 8561. Berlin: Springer, 2014: 197-205.

This work is partially supported by the Science and Technology Project of Hubei Provincial Education Department (B2016015).

LIUYanli, born in 1980, M. S., lecturer. Her research interests include algorithm design of NP problem, algorithm optimization.

XUZhenxing, born in 1990, Ph. D. candidate. His research interests include approximate solution of NP problem, algorithm optimization.

XIONGDan, born in 1979, M. S., lecturer. Her research interests include mathematical statistics, system identification.

ExactSATalgorithmbasedondynamicbranchingstrategyofawardandpunishment

LIU Yanli1,2*, XU Zhenxing2, XIONG Dan1

(1.CollegeofScience,WuhanUniversityofScienceandTechnology,WuhanHubei430081,China;2.SchoolofComputerScienceandTechnology,HuazhongUniversityofScienceandTechnology,WuhanHebei430074,China)

The limited number and high similarity of learning clauses lead to limited historical information and imbalanced search tree. In order to solve the problems, a dynamic branching strategy of award and punishment was proposed. Firstly, the variables of every unit propagation were punished. Different penalty functions were established according to whether the variable generated a conflict and the conflict interval. Then, in the learning phase, the positive variables for the conflict were found according to the learning clauses, and their activities were nonlinearly increased. Finally, the variable with the maximum activity was chosen as the new branching variable. On the basis of the glucose3.0 algorithm, an improved dynamic algorithm of award and punishment named Award and Punishment 7 (AP7) was completed. The experimental results show that, compared with the glucose3.0 algorithm, the rate of cutting branches of AP7 algorithm is improved by 14.2%-29.3%, and that of a few examples is improved up to 51%. The running time of the improved AP7 algorithm is shortened more than 7% compared with the glucose3.0 algorithm. The branching strategy can efficiently reduce the size of search tree, make the search tree more balanced and reduce the computation time.

Non-deterministic Polynomial Complete problem (NPC); SATisfiability problem (SAT); conflict driven clause learning; exact algorithm; branching strategy

2017- 06- 07;

2017- 08- 03。

湖北省教育廳科學(xué)研究計(jì)劃項(xiàng)目(B2016015)。

劉燕麗(1980—)，女，河南西平人，講師，碩士，CCF會(huì)員，主要研究方向： NP問(wèn)題的算法設(shè)計(jì)、算法優(yōu)化； 徐振興(1990—)，男，湖北鄂州人，博士研究生，主要研究方向：NP問(wèn)題的近似求解、算法優(yōu)化； 熊丹(1979—)，女，湖北天門人，講師，碩士，主要研究方向：數(shù)理統(tǒng)計(jì)、系統(tǒng)辨識(shí)。

1001- 9081(2017)12- 3487- 06

10.11772/j.issn.1001- 9081.2017.12.3487

(*通信作者電子郵箱yanlil2008@163.com)

TP301.6

A