基于近期文字極性分配的學(xué)習(xí)子句評估算法

馮心妍,吳貫鋒,張丁榮,王恪銘

(1.西南交通大學(xué)信息科學(xué)與技術(shù)學(xué)院,四川 成都 611756; 2.西南交通大學(xué)系統(tǒng)可信性自動(dòng)驗(yàn)證國家地方聯(lián)合工程實(shí)驗(yàn)室,四川 成都 611756; 3.西南交通大學(xué)數(shù)學(xué)學(xué)院,四川 成都 611756;4.西南交通大學(xué)計(jì)算機(jī)與人工智能學(xué)院,四川 成都 611756)

1 引言

布爾可滿足性問題(Boolean Satisfiability Problem),簡稱SAT問題,是邏輯學(xué)中的一個(gè)基本問題,也是理論計(jì)算機(jī)科學(xué)和人工智能研究中的核心問題。SAT問題是第一個(gè)被證明的NP完全問題NPC(Nondeterministic Polynomial Complete problem)[1]。在過去的幾十年中,SAT問題在工程技術(shù)、軍事、工商管理、交通運(yùn)輸及自然科學(xué)研究領(lǐng)域得到了廣泛的應(yīng)用。從人工智能規(guī)劃到密碼學(xué),現(xiàn)代SAT求解器已經(jīng)被證明了能夠處理包含數(shù)百萬個(gè)變量和子句的龐大公式,因此致力于尋找求解SAT問題的快速而有效的算法,對理論研究和許多應(yīng)用領(lǐng)域都具有極其重要的意義[2]。

現(xiàn)代基于沖突驅(qū)動(dòng)子句學(xué)習(xí)算法CDCL(Conflict Driven Clause Learning)的SAT求解器已成功地用于解決各種工業(yè)實(shí)際問題,并且隨著多核處理器的廣泛應(yīng)用,越來越多的并行求解器也得到發(fā)展[3]。在這種情況下,SAT求解器的進(jìn)步歸功于核心組件的不斷改進(jìn)和各個(gè)功能模塊的有效結(jié)合,包括:變量與分支的選擇和決策、沖突分析、內(nèi)存管理和重新啟動(dòng)等。

SAT求解器在求解工業(yè)級(jí)規(guī)模的問題時(shí),往往會(huì)通過沖突分析產(chǎn)生指數(shù)級(jí)別的學(xué)習(xí)子句,但保留過多的子句會(huì)過度消耗內(nèi)存資源,增加執(zhí)行單元傳播過程的時(shí)間,大大減緩了求解速度。因此,SAT求解器運(yùn)行過程中往往會(huì)刪除大部分學(xué)習(xí)子句,僅保留部分對求解過程有益的子句,從而維護(hù)一個(gè)多項(xiàng)式大小的學(xué)習(xí)子句數(shù)據(jù)庫[4]。

目前主流的基于CDCL的SAT求解器都是通過刪除被認(rèn)為與下一次搜索無關(guān)的子句來動(dòng)態(tài)地減少學(xué)習(xí)子句數(shù)據(jù)庫。其中,最具有里程碑意義的MiniSAT求解器采用了變量狀態(tài)獨(dú)立衰減和VSIDS(Variable State Independent Decaying Sum)評估策略[5]。但是,這種方式在求解的初期無法正確評估子句的活躍程度,可能會(huì)造成誤刪部分未被使用的子句,也可能出現(xiàn)部分無用的學(xué)習(xí)子句由于反復(fù)碰撞而造成的持續(xù)被保留的現(xiàn)象。在此基礎(chǔ)上,基于文字塊距離LBD(Literals Blocks Distance)的評估策略在Glucose求解器中被提出并得到廣泛應(yīng)用[6],針對求解器中子句評估策略現(xiàn)存的缺陷而進(jìn)行改進(jìn),Glucose使用LBD的靜態(tài)度量方式來量化學(xué)習(xí)子句的質(zhì)量。

在現(xiàn)代SAT求解器的發(fā)展過程中,也出現(xiàn)了很多使用混合算法進(jìn)行子句評估的策略,從而避免單個(gè)評估指標(biāo)可能造成的缺陷。在MapleComsSPS求解器中提出了新的學(xué)習(xí)比率分支決策算法LRB(Learning Ratio Branching)[7,8],同時(shí)結(jié)合了VSIDS和LBD算法進(jìn)行子句質(zhì)量評估,即在求解的前2 500 s采用LBD評估方式對子句進(jìn)行周期性刪除,之后再采用VSIDS的策略評估學(xué)習(xí)子句。在LingeLing求解器中也采用了VSIDS與LBD混合的評估策略[9],通過分析學(xué)習(xí)子句的LBD值分布情況,在LBD值分布不均時(shí)切換為VSIDS評估方式。

基于VSIDS和LBD的評估方式都存在評估指標(biāo)單一的問題,在周期性刪除子句時(shí)可能會(huì)誤刪一些對求解過程有用的子句,從而導(dǎo)致反復(fù)地推導(dǎo)求解。在并行SAT求解中,目前存在的策略和啟發(fā)式算法還未能充分發(fā)揮學(xué)習(xí)子句在并行節(jié)點(diǎn)間的剪枝能力,且并行程序設(shè)計(jì)中存在任務(wù)劃分、負(fù)載均衡和數(shù)據(jù)一致性等難題,并行節(jié)點(diǎn)間如何有效地動(dòng)態(tài)選擇共享的信息還有待深入研究。

吳貫鋒等人[10,11]通過分析學(xué)習(xí)子句出現(xiàn)的頻率,進(jìn)一步將學(xué)習(xí)子句頻率與LBD算法相結(jié)合,以此作為一種新型混合子句評估方式。該混合算法不僅反映了沖突分析中學(xué)習(xí)子句的分布情況,也充分利用了文字信息。大量實(shí)驗(yàn)結(jié)果表明,這種混合算法在SAT求解器的串行和并行版本中都比LBD評估算法具有優(yōu)勢,且能進(jìn)一步增加求解問題的數(shù)量。

進(jìn)度節(jié)省(Progress Saving)是由Pipatsrisawat等人[12]提出的一種基于字面極性的啟發(fā)式方法,通過為每個(gè)變量動(dòng)態(tài)保存最后使用的極性,從而達(dá)到防止求解器多次求解相同的可滿足子公式的目的。Shaw等[13]在進(jìn)度節(jié)省的基礎(chǔ)上提出了一種新的類似于VSIDS的啟發(fā)式策略,稱為文字狀態(tài)獨(dú)立衰減和LSIDS(Literal State Independent Decay Sum),即捕獲分配給變量的最近極性加權(quán)趨勢和相應(yīng)的文字活動(dòng),作為非時(shí)間序列回溯的相位選擇啟發(fā)式,其研究結(jié)果也論證了子句中文字活動(dòng)的趨勢與近期極性分配的相關(guān)性。

因此,在求解器中,識(shí)別高質(zhì)量的學(xué)習(xí)子句,提出新的有效的學(xué)習(xí)子句評估算法,對SAT求解器的進(jìn)一步提升與改進(jìn)能起到關(guān)鍵的作用。本文通過研究求解器中的文字活動(dòng)趨勢與近期極性分配情況之間的關(guān)系,將其量化為一種評估學(xué)習(xí)子句有用性的指標(biāo),通過改進(jìn)求解器在周期性刪除策略中的評估方式,驗(yàn)證這種新的子句評估策略的有效性,并將其應(yīng)用在串行和并行求解器上,以提高SAT求解器的效率。

2 相關(guān)工作

2.1 SAT基礎(chǔ)知識(shí)

在布爾可滿足性問題中,文字(Literal)是指命題變量v或它的否定形式v[14]。如果布爾公式F表示子句集的合取(∧),且其中每一個(gè)子句都由文字集的析取(∨)構(gòu)成,則F被稱為合取范式CNF(Conjunctive Normal Form)。公式F的真值賦值定義如式(1)所示:

V→{True,False}

(1)

其中,V是F的變量集。F中每個(gè)變量映射到真值True或False后,F取值0或1。如果F=1,則稱F可滿足分配或存在解。SAT問題旨在尋求是否存在F的可滿足分配。若給定公式F為可滿足,則SAT求解器返回其可滿足分配作為問題的解,否則給出不滿足證明。

Figure 1 Process of SAT solver solution圖1 SAT求解器求解過程

CDCL算法是在DPLL(Davis Putnam Logemann Loveland)算法的基礎(chǔ)上改進(jìn)而來的,并且用于幾乎所有的現(xiàn)代SAT求解器。CDCL針對DPLL算法中存在的缺陷,進(jìn)行了學(xué)習(xí)沖突子句和非時(shí)間回溯的改進(jìn)。其關(guān)鍵組件如圖1所示,包含:布爾約束傳播、分支變量決策、子句沖突學(xué)習(xí)、重新啟動(dòng)和子句數(shù)據(jù)庫周期性刪除等[15]。

CDCL算法由算法1所示。

算法1CDCL算法

輸入：CNF公式F。

輸出：SAT或UNSAT。

1Δ=?;//Δ:學(xué)習(xí)子句數(shù)據(jù)庫

2While(true)do{

3if(!propagate())then{

4if((c=analyzeConflict())==?)then

returnUNSAT;

5Δ=Δ∪{c};

6if(timeToRestart())then

backtrack to level 0;

7else

8 backtrack to the assertion level ofc;

9 }

10else{

11if((l=decide())==null)then

returnSAT;

12 assertlin a new decision level;

13if(timeToReduce())then

clean(?);

14 }

15 }

在CDCL算法主循環(huán)的每一步,都會(huì)先執(zhí)行單元傳播propagate()[16,17]。如果發(fā)生沖突,則通過沖突分析analyzeConflict()函數(shù)導(dǎo)出一個(gè)新的斷言子句,若導(dǎo)出的子句為空集,則該公式被返回UNSAT,即公式F不可滿足(第4行)。否則將導(dǎo)出的子句添加到學(xué)習(xí)子句數(shù)據(jù)庫Δ中(第5行)。如果循環(huán)過程中不需要重啟,則回跳到學(xué)習(xí)子句的斷言級(jí)別(第8行),否則它將回跳到搜索的初始級(jí)別(第6行)。如果在執(zhí)行單元傳播下產(chǎn)生空子句時(shí),算法將選擇一個(gè)新的文字作為決策文字。如果該決策文字存在,則在新的決策級(jí)別中進(jìn)行斷言(第12行),反之求解器則找到公式的可滿足模型(第11行)。

當(dāng)學(xué)習(xí)子句數(shù)據(jù)庫需Δ要被縮減時(shí),則執(zhí)行timeToReduce()函數(shù)(第13行)。由于保留過多的學(xué)習(xí)子句會(huì)放緩單元傳播過程,增加求解器遍歷子句的時(shí)間,而刪除太多學(xué)習(xí)子句則會(huì)破壞整體學(xué)習(xí)的結(jié)果對求解的有用性,因此該組件對CDCL求解器的性能至關(guān)重要。

綜合分析,識(shí)別與證明學(xué)習(xí)子句質(zhì)量的好壞仍然是一個(gè)重要的挑戰(zhàn)。第一個(gè)子句質(zhì)量度量的方式是在基于活躍度的VSIDS啟發(fā)式成功后提出的,這種刪除策略假定過去有用的子句將來也可能是有用的。更準(zhǔn)確地說,如果學(xué)習(xí)子句頻繁地參與最近的沖突,則認(rèn)為它與證明學(xué)習(xí)子句的質(zhì)量好壞更加相關(guān)。之后Glucose使用一種稱為LBD的更準(zhǔn)確的度量方式來估計(jì)學(xué)習(xí)子句的質(zhì)量[18],從而提出了比以往更好的子句管理策略。

2.2 已有的學(xué)習(xí)子句評估算法

基于LBD的學(xué)習(xí)子句評估算法[5]:學(xué)習(xí)子句的LBD值表示該子句中包含的不同決策級(jí)別的數(shù)量,即子句中變量所在不同決策層次的個(gè)數(shù)。LBD的值是一個(gè)正整數(shù),如果LBD(c)=k,則學(xué)習(xí)子句c包含k個(gè)傳播模塊,每個(gè)塊都在相同的分支中傳播。具有較低LBD值的學(xué)習(xí)子句往往具有更高的質(zhì)量,LBD值為2的學(xué)習(xí)子句被稱為glue子句,這些子句有可能在部分賦值下快速傳播真值,并且被認(rèn)為是質(zhì)量最好的學(xué)習(xí)子句?；贚BD的評估算法在幾乎所有CDCL類的SAT求解器中用于學(xué)習(xí)子句質(zhì)量度量。子句的LBD值在求解過程中隨著時(shí)間的推移而變化,并且每次完全分配子句時(shí)都需要重新計(jì)算。

VSIDS評估算法[6]:VSIDS評估算法在MiniSAT和現(xiàn)有大多數(shù)CDCL求解器中使用,其步驟描述如下:

(1)每個(gè)文字都附有一個(gè)計(jì)算活躍度的變量,每發(fā)生一次沖突,所生成學(xué)習(xí)子句中的所有文字的活躍度增加1,該過程稱為碰撞(Bumping)。

(2)在發(fā)生沖突后,系統(tǒng)中所有文字的活躍度會(huì)被乘以一個(gè)小于1的常數(shù),從而隨著時(shí)間的推移使文字的活躍度衰減。該算法利用文字的活躍性,在選擇變量的過程中優(yōu)先考慮與沖突更相關(guān)的文字。

3 基于近期文字極性分配的子句評估算法改進(jìn)

3.1 基于近期文字極性分配評估學(xué)習(xí)子句的有用性

變量決策模塊是SAT求解器中的核心組件之一,其中包含了決策變量和決策級(jí)別。求解過程中,變量決策模塊從一組未分配的變量中選取一個(gè)決策變量v,并為該決策變量v分配一個(gè)真值[12]。在SAT求解器的求解過程中,除了引導(dǎo)學(xué)習(xí)子句外,求解器還尋求撤銷當(dāng)前部分分配的子句,該過程稱為回溯。為此,在沖突分析子程序中計(jì)算回溯級(jí)別dl,接下來求解器會(huì)刪除所有決策級(jí)別大于dl的變量的賦值。

在目前普遍使用的VSIDS啟發(fā)式文字活躍度評估方法中,選擇下一個(gè)決策變量時(shí)通常要考慮文字的字面極性。在一般情況下,每次分配決策文字變量時(shí),都會(huì)定義并使用默認(rèn)的極性。但是,在SAT求解器求解過程中存在的重新啟動(dòng)和回溯過程可能會(huì)導(dǎo)致求解重復(fù)的子公式,因此,進(jìn)度節(jié)省方法的提出有效地避免了求解器多次求解相同的可滿足子公式,且該啟發(fā)式方法在現(xiàn)代SAT求解器中被廣泛使用。

為了進(jìn)一步研究近期文字極性的分配與學(xué)習(xí)子句有用性之間的相關(guān)性,本文以2種最先進(jìn)的CDCL求解器Glucose 4.1和lstech_maple為基準(zhǔn)進(jìn)行分析。Glucose 4.1的出現(xiàn)使得LBD評估算法在現(xiàn)代求解中被廣泛使用,并多次在SAT Competition中獲獎(jiǎng)。MapleLCMDistChronoBT-DL求解器在2019年的SAT Competition的主軌道中取得了第1名,且其搜索方式在后來的發(fā)展過程中得到了改進(jìn),改進(jìn)后的lstech_maple求解器在2021年的SAT Competition中取得了第2名[1]。

基于CDCL的SAT求解器利用進(jìn)度節(jié)省的概念,旨在將給定變量v的極性動(dòng)態(tài)地存儲(chǔ)在polarity[x]中,且該極性是通過最近一次決策或傳播分配給子句所得到的。因此,在研究過程中以polarity[x]作為所捕獲的文字近期極性分配的信息。并且利用該存儲(chǔ)信息與當(dāng)前子句的極性分配進(jìn)行邏輯與的操作,再與決策變量v的極性取交集,以此利用近期文字極性分配情況推斷學(xué)習(xí)子句與未來搜索之間的相關(guān)性。

定義1使用LitPol(Literal Polarity)衡量近期文字極性分配與學(xué)習(xí)子句有用性之間的關(guān)系,其計(jì)算如式(2)所示:

LitPol(c)=|polarity[v]∩(polarity[c[i]]∧

sign(c[i]))|,i∈[0,c.size())

(2)

其中,polarity[v]表示決策變量v的極性分配情況,polarity[c[i]]表示在決策和傳播過程中存儲(chǔ)的子句c中第i+1個(gè)文字的極性信息,sign(c[i])表示子句中第i個(gè)文字的極性符號(hào)。

LitPol的值是一個(gè)正整數(shù),是一種基于進(jìn)度節(jié)省的質(zhì)量度量,LitPol值等于當(dāng)前學(xué)習(xí)子句中的文字極性分配與近期變量極性分配相同的文字?jǐn)?shù)量。如果LitPol值很小,表示該子句可能是經(jīng)過沖突分析后導(dǎo)出的學(xué)習(xí)子句,并且與當(dāng)前決策變量極性的集合交集很小,因此推斷具有較小Litpol值的子句在后續(xù)的搜索和求解過程中是更有用的。LitPol度量是高度動(dòng)態(tài)的,由于保存的文字極性集polarity[v]在搜索過程中會(huì)發(fā)生變化,因此給定子句的LitPol值也會(huì)發(fā)生變化。

以CDCL求解器為基準(zhǔn)進(jìn)行分析,在其求解過程中加入計(jì)算學(xué)習(xí)子句LitPol值的功能,并將其應(yīng)用在子句的周期性刪除中。每次調(diào)用周期性刪除reduceDB()函數(shù)時(shí),先計(jì)算當(dāng)前所有學(xué)習(xí)子句的LitPol值,并按照子句周期性刪除策略的原則刪除一半的學(xué)習(xí)子句。

在保留原有利用LBD作為評估指標(biāo)的策略中,選取了2021年SAT Competition中的3個(gè)競賽實(shí)例(20-100-lambda100-65_sat.cnf,crafted_n10_d6_c4_num15.cnf和bv-term-small-rw_1492.smt2.cnf)進(jìn)行觀察。通過對比調(diào)用reduceDB()函數(shù)前后的學(xué)習(xí)子句的LitPol值,觀察發(fā)現(xiàn),具有較小LitPol值的學(xué)習(xí)子句被保留了下來。

Figure 2 LitPol of the learnt clauses before and after periodic reduce under the LBD evaluation strategy圖2 LBD評估策略下執(zhí)行周期性 刪除前后的學(xué)習(xí)子句的LitPol

首先在LBD評估策略下,對比分析執(zhí)行周期性刪除前后學(xué)習(xí)子句LitPol值的頻次分布情況。通過計(jì)算得出,LitPol的取值在0～255,圖2a和圖2c曲線服從重尾分布。本文為了突出顯示,截?cái)嗔撕罄m(xù)線條重疊部分,僅保留LitPol值在前100的頻次分布。

實(shí)驗(yàn)結(jié)果表明,LitPol值小于25的學(xué)習(xí)子句在整個(gè)數(shù)據(jù)庫中所占的比例較大。并在執(zhí)行reduceDB()后,LitPol值小于25的學(xué)習(xí)子句基本被保留,LitPol值較大的學(xué)習(xí)子句則基本被刪除。

因此,推斷具有較小LitPol值的學(xué)習(xí)子句是與未來搜索更相關(guān)的,能夠在一定程度上縮小搜索空間;相反,具有較大LitPol值的子句在當(dāng)前搜索空間可能不太有用,且與后續(xù)的求解過程無關(guān)。

3.2 基于LitPol的學(xué)習(xí)子句評估算法

通過分析學(xué)習(xí)子句的LitPol值在執(zhí)行周期性刪除前后的分布情況,本文選擇保留LitPol值較小的學(xué)習(xí)子句,并以此作為子句評估的標(biāo)準(zhǔn),即在求解器的周期性刪除模塊中利用LitPol的評估方法對學(xué)習(xí)子句的質(zhì)量進(jìn)行評估。

基于LBD的評估算法已經(jīng)被廣泛地證明了其有效性,因此應(yīng)保留LBD算法在沖突分析方面評估的優(yōu)勢,即在每次發(fā)生沖突調(diào)用沖突分析analyzeConflict()函數(shù)時(shí),利用LBD判斷是否需要將子句標(biāo)記為“可以被刪除”。而利用LitPol的評估策略主要用于評估學(xué)習(xí)子句的有用性,將該度量方法集成到周期性刪除中作為判斷條件,為釋放學(xué)習(xí)子句占用的內(nèi)存提供依據(jù),具體過程如算法2所示。

算法2LitPol評估算法

Step1調(diào)用LitPol值計(jì)算函數(shù),計(jì)算學(xué)習(xí)子句中文字極性與近期變量極性賦值情況相同的文字?jǐn)?shù)量。

Step2執(zhí)行刪除條件判斷:對于任意一個(gè)學(xué)習(xí)子句,如果其LitPol值大于閾值,且子句長度大于2,且在單文字子句傳播過程中未使用,則刪除該學(xué)習(xí)子句,否則標(biāo)記該學(xué)習(xí)子句,并在下一次循環(huán)中刪除。

圖3為在同一實(shí)驗(yàn)環(huán)境下的對比結(jié)果。實(shí)驗(yàn)中隨機(jī)選取了5個(gè)CNF測試?yán)募鳛閷?shí)驗(yàn)樣本,這5個(gè)CNF測試文件的平均文字?jǐn)?shù)為153 142,平均子句數(shù)為2 723 495。對3.1節(jié)中ReduceDB執(zhí)行前后的子句LitPol值的分布情況進(jìn)行分析,LitPol值較小的子句在周期性刪除策略執(zhí)行后被保留下來,因此在LitPol評估策略中,本文選擇設(shè)置較小的LitPol閾值來保留對求解過程有用的學(xué)習(xí)子句。

Figure 3 Setting different LitPol thresholds as the clause deletion strategy and performance comparison of solving CNF files under the LBD clause evaluation strategy圖3 設(shè)置不同的LitPol閾值作為子句刪除策略 與LBD子句評估策略下求解CNF文件的表現(xiàn)對比

實(shí)驗(yàn)過程中對同一測試示例設(shè)置10種不同的LitPol閾值,分別為3,4,5,10,15,10,25,30,40和50,并統(tǒng)計(jì)求解過程中執(zhí)行ReduceDB的次數(shù)和求解所用時(shí)長,最終得出一個(gè)平均的結(jié)果并將其與LBD評估策略下的求解表現(xiàn)進(jìn)行對比。從實(shí)驗(yàn)結(jié)果可以看出,當(dāng)LitPol值作為子句刪除的閾值時(shí),Litpol值設(shè)置得較小能夠在求解過程中減少ReduceDB的執(zhí)行次數(shù),一定程度上起到了節(jié)省進(jìn)度的作用,且該算法應(yīng)用上述策略時(shí)的求解速度優(yōu)于使用LBD值作為子句評估策略時(shí)的求解速度。

實(shí)驗(yàn)結(jié)果表明,在這種基于進(jìn)度節(jié)省的利用近期文字極分配性的評估策略中,通過使用LitPol值作為判斷是否刪除學(xué)習(xí)子句的條件,可以保留合適的學(xué)習(xí)子句,從而有效地節(jié)省求解進(jìn)度,提高求解速度。

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

本次實(shí)驗(yàn)的實(shí)驗(yàn)環(huán)境為:Windows 10 x64, Intel?CoreTMi7-7700 CPU主頻為4.2 GHz,內(nèi)存為32 GB。

2021年SAT競賽為主軌道和并行軌道提供了相同的400個(gè)測試實(shí)例,其中139個(gè)SAT,139個(gè)UNSAT,122個(gè)UNKNOWN。而在Main Track ALL中獲得第一名的典型CDCL求解器Kissat_MAB在規(guī)定時(shí)間內(nèi)求解出了296個(gè)測試實(shí)例,剩余104個(gè)測試實(shí)例則超時(shí)未被求解。

為了以合理的時(shí)間成本進(jìn)行測試,本次實(shí)驗(yàn)選取了Kissat_MAB中求解速度排名前200的測試實(shí)例進(jìn)行測試,該選取標(biāo)準(zhǔn)與CNF文件的子句規(guī)模大小無關(guān),求解時(shí)長限時(shí)4 000 s,所有的測試結(jié)果均在同一軟硬件環(huán)境下得出。前述的實(shí)驗(yàn)分析結(jié)果表明,LitPol的閾值設(shè)置得較小,所得實(shí)驗(yàn)結(jié)果效果更好,因此本次實(shí)驗(yàn)中LitPol值的閾值取4,該閾值是根據(jù)實(shí)驗(yàn)獲取的經(jīng)驗(yàn)值所設(shè)置。將LitPol評估算法應(yīng)用在Glucose、Glucose-Syrup和lstech_maple中,并行求解器默認(rèn)使用4個(gè)線程。

Table 1 Results comparison of Glucose serial solution 表1 Glucose串行求解結(jié)果對比

表1中,使用了LitPol作為子句周期性刪除策略的求解器為Glucose-LitPol,在求解個(gè)數(shù)上Glucose-LitPol比Glucose整體多了2個(gè),可滿足問題求解個(gè)數(shù)減少了1個(gè),不可滿足問題求解個(gè)數(shù)增加了3個(gè),求解平均時(shí)間比Glucose的縮短了34.74 s。

另一方面,采用了LitPol作為子句周期性刪除策略的并行求解器為Syrup-LitPol。如表2所示,與原始的求解器相比,求解總數(shù)相同,求解時(shí)間縮短了13.72 s。

Table 2 Results comparison of Glucose-Syrup parallel solution 表2 Glucose-Syrup并行求解結(jié)果對比

上述實(shí)驗(yàn)結(jié)果表明,將這種利用近期文字極性分配趨勢的子句評估策略應(yīng)用在目前主流的CDCL串行和并行求解器上,能夠有效地提高求解器的求解效率,增加求解個(gè)數(shù)的同時(shí)還能夠?qū)蝹€(gè)CNF文件的平均求解時(shí)間縮短13～34 s。

為了進(jìn)一步驗(yàn)證利用LitPol作為學(xué)習(xí)子句評估條件的有效性,選取lstech_maple求解器進(jìn)行進(jìn)一步測試。

表3中,使用了LitPol作為子句周期性刪除策略的求解器為lstech-LitPol。lstech-LitPol在求解問題個(gè)數(shù)上比lstech_maple整體多了2個(gè),其中可滿足問題和不可滿足問題各增加了1個(gè),求解平均時(shí)間比lstech_maple縮短了13.79 s。

Table 3 Results comparison of lstech_maple solution 表3 lstech_maple求解結(jié)果對比

對表3中l(wèi)stech_maple和lstech-LitPol求解器的求解時(shí)長進(jìn)行分析:對于lstech_maple求解耗時(shí)較長的問題,lstech-LitPol能夠有效地加快其求解速度,并求解出了部分lstech_maple在4 000 s內(nèi)未能解決的問題。具體對比如圖4所示,其中未得出解的文件求解時(shí)長標(biāo)為8 000 s。國際競賽中常用的懲罰平均運(yùn)行時(shí)長PAR-2(Penalized Average Runtime-2)是一種用于評估求解器性能的指標(biāo),其運(yùn)算方式是對求解器的求解時(shí)長進(jìn)行求和,并將超時(shí)未得出結(jié)果的問題的求解時(shí)長乘2進(jìn)行懲罰,最后相加得到指標(biāo)評估數(shù)據(jù)。通過使用PAR-2對上述2種求解器的性能進(jìn)行評估,可知lstech- LitPol具有更好的求解性能。

Figure 4 Duration comparison of solving CNF files圖4 求解CNF文件時(shí)長對比

5 結(jié)束語

通過一系列的實(shí)驗(yàn)分析可以得出,利用相位保存和近期文字極性分配情況對學(xué)習(xí)子句的質(zhì)量進(jìn)行評估的方式,可以在每次刪除數(shù)據(jù)庫中一半的學(xué)習(xí)子句時(shí)能有效地保留對求解過程有用的學(xué)習(xí)子句,從而達(dá)到節(jié)省求解進(jìn)度的目的。

實(shí)驗(yàn)結(jié)果表明,上述策略能夠在一定程度上達(dá)到且超越原有求解器的效果,并進(jìn)一步提高串行和并行SAT求解器的求解速度,提高SAT求解器的整體求解效率。

不足之處在于評估學(xué)習(xí)子句時(shí)閾值的選擇。不同的求解實(shí)例有不同的最佳臨界標(biāo)準(zhǔn),在動(dòng)態(tài)地計(jì)算閾值時(shí)需要盡量減小額外的計(jì)算開銷。另外,在并行求解器子句共享模塊中還需要更好地應(yīng)用改進(jìn)的子句評估策略,實(shí)現(xiàn)不同線程間信息的有效共享,更高效地保留對求解過程有用的學(xué)習(xí)子句。

后續(xù)研究中計(jì)劃進(jìn)一步將相位保存和近期文字極性的分配情況與求解器的其他關(guān)鍵模塊更好地結(jié)合,并結(jié)合SAT求解實(shí)例的特性實(shí)現(xiàn)更精確的分析,實(shí)現(xiàn)改進(jìn)求解效率的目的。