基于近期文字極性分配的學習子句評估算法

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

(1.西南交通大學信息科學與技術學院,四川 成都 611756; 2.西南交通大學系統可信性自動驗證國家地方聯合工程實驗室,四川 成都 611756; 3.西南交通大學數學學院,四川 成都 611756;4.西南交通大學計算機與人工智能學院,四川 成都 611756)

1 引言

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

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

SAT求解器在求解工業級規模的問題時,往往會通過沖突分析產生指數級別的學習子句,但保留過多的子句會過度消耗內存資源,增加執行單元傳播過程的時間,大大減緩了求解速度。因此,SAT求解器運行過程中往往會刪除大部分學習子句,僅保留部分對求解過程有益的子句,從而維護一個多項式大小的學習子句數據庫[4]。

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

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

基于VSIDS和LBD的評估方式都存在評估指標單一的問題,在周期性刪除子句時可能會誤刪一些對求解過程有用的子句,從而導致反復地推導求解。在并行SAT求解中,目前存在的策略和啟發式算法還未能充分發揮學習子句在并行節點間的剪枝能力,且并行程序設計中存在任務劃分、負載均衡和數據一致性等難題,并行節點間如何有效地動態選擇共享的信息還有待深入研究。

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

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

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

2 相關工作

2.1 SAT基礎知識

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

V→{True,False}

(1)

其中,V是F的變量集。F中每個變量映射到真值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)算法的基礎上改進而來的,并且用于幾乎所有的現代SAT求解器。CDCL針對DPLL算法中存在的缺陷,進行了學習沖突子句和非時間回溯的改進。其關鍵組件如圖1所示,包含:布爾約束傳播、分支變量決策、子句沖突學習、重新啟動和子句數據庫周期性刪除等[15]。

CDCL算法由算法1所示。

算法1CDCL算法

輸入：CNF公式F。

輸出：SAT或UNSAT。

1Δ=?;//Δ:學習子句數據庫

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

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

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

2.2 已有的學習子句評估算法

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

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

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

(2)在發生沖突后,系統中所有文字的活躍度會被乘以一個小于1的常數,從而隨著時間的推移使文字的活躍度衰減。該算法利用文字的活躍性,在選擇變量的過程中優先考慮與沖突更相關的文字。

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

3.1 基于近期文字極性分配評估學習子句的有用性

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

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

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

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

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

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

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

(2)

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

LitPol的值是一個正整數,是一種基于進度節省的質量度量,LitPol值等于當前學習子句中的文字極性分配與近期變量極性分配相同的文字數量。如果LitPol值很小,表示該子句可能是經過沖突分析后導出的學習子句,并且與當前決策變量極性的集合交集很小,因此推斷具有較小Litpol值的子句在后續的搜索和求解過程中是更有用的。LitPol度量是高度動態的,由于保存的文字極性集polarity[v]在搜索過程中會發生變化,因此給定子句的LitPol值也會發生變化。

以CDCL求解器為基準進行分析,在其求解過程中加入計算學習子句LitPol值的功能,并將其應用在子句的周期性刪除中。每次調用周期性刪除reduceDB()函數時,先計算當前所有學習子句的LitPol值,并按照子句周期性刪除策略的原則刪除一半的學習子句。

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

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

首先在LBD評估策略下,對比分析執行周期性刪除前后學習子句LitPol值的頻次分布情況。通過計算得出,LitPol的取值在0～255,圖2a和圖2c曲線服從重尾分布。本文為了突出顯示,截斷了后續線條重疊部分,僅保留LitPol值在前100的頻次分布。

實驗結果表明,LitPol值小于25的學習子句在整個數據庫中所占的比例較大。并在執行reduceDB()后,LitPol值小于25的學習子句基本被保留,LitPol值較大的學習子句則基本被刪除。

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

3.2 基于LitPol的學習子句評估算法

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

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

算法2LitPol評估算法

Step1調用LitPol值計算函數,計算學習子句中文字極性與近期變量極性賦值情況相同的文字數量。

Step2執行刪除條件判斷:對于任意一個學習子句,如果其LitPol值大于閾值,且子句長度大于2,且在單文字子句傳播過程中未使用,則刪除該學習子句,否則標記該學習子句,并在下一次循環中刪除。

圖3為在同一實驗環境下的對比結果。實驗中隨機選取了5個CNF測試例文件作為實驗樣本,這5個CNF測試文件的平均文字數為153 142,平均子句數為2 723 495。對3.1節中ReduceDB執行前后的子句LitPol值的分布情況進行分析,LitPol值較小的子句在周期性刪除策略執行后被保留下來,因此在LitPol評估策略中,本文選擇設置較小的LitPol閾值來保留對求解過程有用的學習子句。

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 設置不同的LitPol閾值作為子句刪除策略 與LBD子句評估策略下求解CNF文件的表現對比

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

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

4 實驗與結果分析

本次實驗的實驗環境為:Windows 10 x64, Intel?CoreTMi7-7700 CPU主頻為4.2 GHz,內存為32 GB。

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

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

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

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

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

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

上述實驗結果表明,將這種利用近期文字極性分配趨勢的子句評估策略應用在目前主流的CDCL串行和并行求解器上,能夠有效地提高求解器的求解效率,增加求解個數的同時還能夠將單個CNF文件的平均求解時間縮短13～34 s。

為了進一步驗證利用LitPol作為學習子句評估條件的有效性,選取lstech_maple求解器進行進一步測試。

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

Table 3 Results comparison of lstech_maple solution 表3 lstech_maple求解結果對比

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

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

5 結束語

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

實驗結果表明,上述策略能夠在一定程度上達到且超越原有求解器的效果,并進一步提高串行和并行SAT求解器的求解速度,提高SAT求解器的整體求解效率。

不足之處在于評估學習子句時閾值的選擇。不同的求解實例有不同的最佳臨界標準,在動態地計算閾值時需要盡量減小額外的計算開銷。另外,在并行求解器子句共享模塊中還需要更好地應用改進的子句評估策略,實現不同線程間信息的有效共享,更高效地保留對求解過程有用的學習子句。

后續研究中計劃進一步將相位保存和近期文字極性的分配情況與求解器的其他關鍵模塊更好地結合,并結合SAT求解實例的特性實現更精確的分析,實現改進求解效率的目的。