基于重啟策略的學(xué)習(xí)子句優(yōu)化方法

李 壯, 劉 磊, 張桐搏, 呂 帥

(吉林大學(xué) 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院, 吉林 長(zhǎng)春 130012)

可滿(mǎn)足性問(wèn)題(SAT)是計(jì)算機(jī)領(lǐng)域的熱點(diǎn)問(wèn)題,許多學(xué)者在該問(wèn)題上作了大量研究,并在問(wèn)題求解效率方面取得了較大的突破,當(dāng)今SAT求解器已能夠解決很多現(xiàn)實(shí)問(wèn)題.隨著SAT求解技術(shù)的發(fā)展,子句學(xué)習(xí)技術(shù)進(jìn)入了蓬勃發(fā)展的階段[1].對(duì)于現(xiàn)實(shí)問(wèn)題,子句學(xué)習(xí)(clause learning)是DPLL求解中最重要的部分[2].

在實(shí)踐中,SAT的求解效率很大程度上取決于對(duì)已學(xué)習(xí)子句數(shù)據(jù)庫(kù)的管理策略.即發(fā)生沖突后,新子句添加到已學(xué)習(xí)的子句數(shù)據(jù)庫(kù)中,其增長(zhǎng)規(guī)模是呈指數(shù)增長(zhǎng)的.保留太多的學(xué)習(xí)子句會(huì)減緩單元傳播的速率,而刪除太多將會(huì)破壞學(xué)習(xí)的整體性[3].所以,優(yōu)化目標(biāo)在于清除掉已學(xué)習(xí)子句數(shù)據(jù)庫(kù)中被判定為在以后的搜索中無(wú)關(guān)的已學(xué)習(xí)子句.學(xué)習(xí)子句管理策略的效率,很大程度上取決于消除頻率和每次刪除的子句數(shù)量[4].

為了優(yōu)化已學(xué)習(xí)子句數(shù)據(jù)庫(kù),近幾年一些先進(jìn)的管理策略已被提出.首次提出質(zhì)量測(cè)量的是VSIDS啟發(fā)式,該優(yōu)化策略假設(shè)一個(gè)過(guò)去學(xué)習(xí)的子句在未來(lái)的求解過(guò)程中可能是有用的[5];Audemard等介紹了一個(gè)新的靜態(tài)措施,加入LBD子句這一概念,更加完善了對(duì)學(xué)習(xí)子句的預(yù)處理技術(shù)[3];Audemard等提出了一個(gè)基于動(dòng)態(tài)的凍結(jié)與激活學(xué)習(xí)子句的原則,即激活最相關(guān)的學(xué)習(xí)子句而凍結(jié)不相關(guān)的學(xué)習(xí)子句[6];Hamadi等提出規(guī)約策略SBR,保留文字?jǐn)?shù)小于等于k的子句,同時(shí)隨機(jī)刪除大于k的子句[7];Luo等提出了學(xué)習(xí)子句最小化的方法,該方法通過(guò)BCP刪除學(xué)習(xí)子句中的冗余文字,從而達(dá)到對(duì)學(xué)習(xí)子句質(zhì)量的優(yōu)化[4];Luo等基于Maple_LCM求解器的子句最小化方法,在Maple_CM求解器上擴(kuò)展到原始子句的預(yù)處理[8].對(duì)學(xué)習(xí)庫(kù)的優(yōu)化主要包括:優(yōu)化學(xué)習(xí)庫(kù)的時(shí)機(jī)、應(yīng)刪除哪些子句以及每次優(yōu)化應(yīng)保留多少子句.經(jīng)分析,優(yōu)化學(xué)習(xí)庫(kù)的時(shí)機(jī)對(duì)求解效率的影響并不大,多數(shù)研究人員將注意力集中在應(yīng)刪除哪些冗余子句,即注重了學(xué)習(xí)子句的質(zhì)量,保留更多有用的學(xué)習(xí)子句,而對(duì)應(yīng)保留學(xué)習(xí)庫(kù)中子句數(shù)量的工作甚少.

本文基于經(jīng)典的SAT求解器,提出了新的動(dòng)態(tài)管理學(xué)習(xí)子句數(shù)據(jù)庫(kù)的算法.在優(yōu)化的過(guò)程中,通過(guò)博弈論的思想,在階段重啟的過(guò)程中,通過(guò)程序中輸出的階段布爾約束傳播(Boolean constraint propagation，BCP)速率和平均BCP速率的對(duì)比,調(diào)整學(xué)習(xí)數(shù)據(jù)庫(kù)的增長(zhǎng)參數(shù),更大可能地靠近學(xué)習(xí)數(shù)據(jù)庫(kù)中子句存儲(chǔ)量的均衡點(diǎn),從而使學(xué)習(xí)庫(kù)的存儲(chǔ)量盡可能地達(dá)到Pareto最優(yōu).實(shí)驗(yàn)結(jié)果表明:新的優(yōu)化方法在隨機(jī)問(wèn)題上勝過(guò)傳統(tǒng)的優(yōu)化方法,在求解出相同的算例中,GTMiniSAT求解器的求解效率也遠(yuǎn)超過(guò)MiniSAT求解器.

1 CDCL和重啟策略

子句學(xué)習(xí)采用了強(qiáng)大的沖突分析技術(shù),其主要思想是在求解過(guò)程中發(fā)生沖突時(shí),分析沖突原因并推理出一些簡(jiǎn)潔地表達(dá)沖突原因的子句,這種已學(xué)習(xí)的子句用于在后面的搜索過(guò)程中避免發(fā)生同樣的沖突且減少搜索空間,更加快了求解的效率.

當(dāng)單元傳播過(guò)程中出現(xiàn)了一對(duì)互補(bǔ)文字時(shí),求解器判定子句集F中出現(xiàn)了一個(gè)沖突,這個(gè)沖突將驅(qū)動(dòng)子句學(xué)習(xí)機(jī)制,將沖突原因保存為一個(gè)新的子句C,并將它添加到原子句集中,以防止在接下來(lái)的搜索過(guò)程發(fā)生相同的沖突,這便是沖突驅(qū)動(dòng)子句學(xué)習(xí)(conflict-driven clause learning,CDCL)[2].

重啟發(fā)生在子句被學(xué)習(xí)之后,當(dāng)指派過(guò)程中發(fā)生了ε(ε>1)次沖突后,重啟策略被觸發(fā),求解器終止當(dāng)前搜索并返回到第0層,即重新求解該子句集[9].沖突上界會(huì)通過(guò)參數(shù)ε來(lái)決定.

2 基于博弈論的學(xué)習(xí)子句優(yōu)化方法

學(xué)習(xí)庫(kù)空間的占有主要體現(xiàn)在對(duì)學(xué)習(xí)庫(kù)增長(zhǎng)參數(shù)的控制.如何調(diào)整學(xué)習(xí)庫(kù)空間的分配,使之在優(yōu)化過(guò)程中無(wú)限接近學(xué)習(xí)庫(kù)的納什均衡點(diǎn),達(dá)到Pareto最優(yōu)狀態(tài),將是子句學(xué)習(xí)的關(guān)鍵.

2.1 博弈模型

求解效率是求解算法好壞的關(guān)鍵衡量指標(biāo).由于BCP時(shí)間占了總求解時(shí)間約90%以上[10],所以本文將求解時(shí)間等同于BCP時(shí)間.

求解效率是無(wú)法量化而又客觀存在的,但滿(mǎn)足:平均求解效率越高,平均BCP速率也越高.所以在本文中用平均BCP速率代替求解效率.

在一個(gè)SAT問(wèn)題求解過(guò)程中,存在著最基本的數(shù)學(xué)公式:

BCP總數(shù)=BCP速率×BCP時(shí)間.

(1)

在子句學(xué)習(xí)庫(kù)中,學(xué)習(xí)子句的多少?lài)?yán)重影響了BCP速率.因此,SAT求解過(guò)程對(duì)應(yīng)了博弈模型,其中:參與者對(duì)應(yīng)平均BCP速率和階段BCP速率;策略對(duì)應(yīng)學(xué)習(xí)庫(kù)的調(diào)整參數(shù)±0.01;利益對(duì)應(yīng)求解效率提高和BCP速率提高;信息對(duì)應(yīng)平均BCP速率和階段BCP速率.

綜上,博弈模型的支付矩陣如表1所示.

表1 學(xué)習(xí)子句數(shù)據(jù)庫(kù)的支付矩陣

2.2 博弈模型的分析

本文令重啟總數(shù)為N,每重啟S次記為一個(gè)階段,第i階段的BCP數(shù)量為si,相應(yīng)的第i階段的執(zhí)行時(shí)間為ti,則階段BCP速率vi=si/ti.

表2 學(xué)習(xí)子句數(shù)據(jù)庫(kù)的實(shí)際支付矩陣

這一過(guò)程是一個(gè)連續(xù)的博弈過(guò)程,其根本目的是在不斷地追求無(wú)限接近納什均衡點(diǎn),實(shí)現(xiàn)已學(xué)習(xí)子句庫(kù)的Pareto最優(yōu)分配.

2.3 基于博弈論的學(xué)習(xí)子句優(yōu)化算法

算法1是GTMiniSAT求解器的簡(jiǎn)要求解過(guò)程,其中包括了學(xué)習(xí)子句優(yōu)化的函數(shù).

算法1 DPLL with clause learning

輸入:CNF formulaF

輸出:A solutionPofFor UNSAT ifFis not satisfiable

1.BCP_num++

2.ifPassigns a value to every variable

3. return success

4.else

5.Pcontains a conflict

6. choose a conflict graphGto find clauseCunderPand add it toF

7. rollback variable or backjump

8. conflict_num++

9.ifconflict_num>ε

10. restart++

11.ifrestart%S==0

12. BCP_total+=BCP_num

13. speed_average=BCP_total/nowtime

14. speed_now=BCP_num/(nowtime-lasttime)

15.ifspeed_now>speed_average

16. learntsize_inc+=p

17.elseifspeed_now

18.iflearntsize_inc-p≥0.5

19. learntsize_inc-=p

20.restarts

在算法1中,第9行表明當(dāng)沖突數(shù)量達(dá)到了臨界值ε時(shí)重啟,第11行表明重啟次數(shù)達(dá)到S(實(shí)驗(yàn)表明55為最優(yōu)值)次時(shí),觸發(fā)重啟參數(shù)調(diào)整策略.第12～19行描述了控制增長(zhǎng)參數(shù)的過(guò)程.當(dāng)沖突數(shù)達(dá)到55次后,第12行統(tǒng)計(jì)從開(kāi)始求解截止到目前的BCP數(shù)量.第13～14行計(jì)算平均BCP速率和階段BCP速率.第15～19行通過(guò)對(duì)速率的比較,來(lái)調(diào)整增減參數(shù).當(dāng)階段BCP速率大于平均BCP速率時(shí),增長(zhǎng)參數(shù)提高;當(dāng)階段BCP速率小于平均BCP速率時(shí),增長(zhǎng)參數(shù)降低.第18行控制了下界,當(dāng)參數(shù)小于0.5時(shí),增減參數(shù)不變.

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

本文從2017年SAT比賽Agile組中隨機(jī)選取了200個(gè)測(cè)試用例,其規(guī)模為幾百個(gè)變量(1 000條子句)至180萬(wàn)變量(668萬(wàn)條子句)不等,CPU在求解器運(yùn)行時(shí)間至5 000 s時(shí)停止.其重啟參數(shù)默認(rèn)為50,增減參數(shù)默認(rèn)為0.1.實(shí)驗(yàn)環(huán)境:Arch Linux 16.04操作系統(tǒng),12核CPU,8GB RAM.

圖1橫坐標(biāo)代表MiniSAT求解器的運(yùn)行時(shí)間,縱坐標(biāo)代表GTMiniSAT求解器的運(yùn)行時(shí)間.所以,分布在斜線(xiàn)以下的點(diǎn)說(shuō)明這些算例在GTMiniSAT求解器上的求解效果較好;在斜線(xiàn)以上的點(diǎn)說(shuō)明這些算例在MiniSAT求解器上的求解效果較好.可以看出,GTMiniSAT求解器效率較明顯地優(yōu)于MiniSAT求解器.斜線(xiàn)以上的點(diǎn)多半離斜線(xiàn)較近,說(shuō)明這些算例在MiniSAT求解器的求解效果略?xún)?yōu)于GTMiniSAT求解器;而斜線(xiàn)以下的點(diǎn)有很大一部分離斜線(xiàn)較遠(yuǎn),說(shuō)明這一部分的算例在GTMiniSAT求解器的求解效果明顯優(yōu)于MiniSAT求解器.

為了更準(zhǔn)確地決定重啟的次數(shù)對(duì)GTMiniSAT求解器的影響,在上述200個(gè)算例中,多次嘗試了重啟1次,5次直到重啟65次,增減參數(shù)默認(rèn)為0.1,CPU在求解器運(yùn)行時(shí)間至5 000 s時(shí)停止.實(shí)驗(yàn)結(jié)果如表3所示.

表3 GTMiniSAT求解器重啟次數(shù)的測(cè)試

由表3可知,重啟次數(shù)固定在55次,平均求解時(shí)間最短,而且優(yōu)于MiniSAT求解器.而其他參數(shù)的數(shù)據(jù)表明求解的平均效率較低,且重啟55次時(shí)求解個(gè)數(shù)也是最多的.因此,在重啟55次后調(diào)整增減參數(shù)是最合理的.

在固定了重啟參數(shù)為55次之后,接下來(lái)需要對(duì)增減參數(shù)進(jìn)行測(cè)試.在上述算例中,嘗試增減0.01,0.02直至0.1.CPU在求解器運(yùn)行時(shí)間至 5 000 s 時(shí)停止.實(shí)驗(yàn)結(jié)果如表4所示.

由表4可知,增減參數(shù)為0.05和0.1的兩組求解效率比較高,而且優(yōu)于MiniSAT求解器.但兩者所處的距離較遠(yuǎn),中間出現(xiàn)了一系列的波動(dòng).出現(xiàn)的原因是否會(huì)受到重啟參數(shù)的影響,即重啟參數(shù)越大,所對(duì)應(yīng)的增減參數(shù)則越大,兩者是否成正比關(guān)系呢?為了證明這個(gè)想法,在以下實(shí)驗(yàn)中給出了更具體的證明,并且驗(yàn)證本文的GTMiniSAT求解器對(duì)于一般的工業(yè)問(wèn)題,也是優(yōu)于MiniSAT求解器的.

表4 GTMiniSAT求解器增減參數(shù)的測(cè)試

GTMiniSAT求解器主要針對(duì)規(guī)模較大的工業(yè)問(wèn)題有效,簡(jiǎn)單問(wèn)題的優(yōu)化效果并不明顯.所以,選擇了2017年SAT競(jìng)賽中Random組的300個(gè)算例,CPU在求解器運(yùn)行時(shí)間至5 000 s時(shí)停止.實(shí)驗(yàn)結(jié)果見(jiàn)表5.

表5 2017年SAT競(jìng)賽隨機(jī)組300算例

由表5可知,GTMiniSAT求解器所求出的兩組算例是相同的114個(gè),且包含在MiniSAT求解器所求出的124個(gè)算例中,平均求解時(shí)間也略高于MiniSAT求解器.(±0.1)-GTMiniSAT求解器所解出的114個(gè)算例中,有72個(gè)算例比MiniSAT求解器快,而(±0.05)-GTMiniSAT僅有50個(gè)算例優(yōu)于MiniSAT求解器.因此,選擇增減參數(shù)為0.1是最合理的.

雖然GTMiniSAT求解器平均求解時(shí)間并沒(méi)有勝過(guò)MiniSAT求解器,但是通過(guò)統(tǒng)計(jì)實(shí)驗(yàn)結(jié)果,在這72個(gè)算例中,MiniSAT求解器的平均求解時(shí)間為136.56 s,而GTMiniSAT求解器的平均求解時(shí)間為44.44 s.表6中統(tǒng)計(jì)了所有問(wèn)題的求解個(gè)數(shù)和平均求解時(shí)間,數(shù)據(jù)表明:GTMiniSAT求解器的效率遠(yuǎn)高于MiniSAT求解器,其求解效率提高了67.45%.

表6 GTMiniSAT和MiniSAT求解器的對(duì)比實(shí)驗(yàn)結(jié)果

為了驗(yàn)證GTMiniSAT求解器的有效性,再次對(duì)GTMiniSAT求解器和MiniSAT求解器在共同求解出的114個(gè)算例中做出數(shù)據(jù)統(tǒng)計(jì)，如表7所示.從表7可知,GTMiniSAT求解器的求解效率也遠(yuǎn)超過(guò)MiniSAT求解器,其求解效率提高了35.76%.

表7 GTMiniSAT和MiniSAT求解器的對(duì)比實(shí)驗(yàn) (共同求解算例)

4 結(jié) 語(yǔ)

本文首次將博弈論的思想應(yīng)用于經(jīng)典SAT求解中,通過(guò)重啟次數(shù)來(lái)調(diào)整學(xué)習(xí)庫(kù)的增長(zhǎng)參數(shù),將原有學(xué)習(xí)數(shù)據(jù)庫(kù)的靜態(tài)等比級(jí)數(shù)增長(zhǎng)改進(jìn)為動(dòng)態(tài)的變化,盡可能靠近學(xué)習(xí)數(shù)據(jù)庫(kù)中子句存儲(chǔ)量的均衡點(diǎn),從而使學(xué)習(xí)庫(kù)的存儲(chǔ)量盡可能達(dá)到Pareto最優(yōu).

GTMiniSAT還存在如下問(wèn)題有待解決:1)之所以改進(jìn)MiniSAT求解器,因?yàn)镸iniSAT是一款經(jīng)典的求解器,對(duì)于新方法的融入有更大的接受空間,下一步工作將考慮改進(jìn)Maple_CM等當(dāng)前最先進(jìn)的求解器.2)由于分析的角度不同,選擇的博弈模型也不同,本文中求解效率和BCP速率具有競(jìng)爭(zhēng)關(guān)系,而同時(shí)又擁有共同目標(biāo)——求解SAT問(wèn)題,即它們相互合作卻又彼此競(jìng)爭(zhēng).下一步工作將站在兩者共同的立場(chǎng)(即合作博弈),對(duì)它們的合作做出進(jìn)一步的博弈分析.