基于變量混合特征的分支啟發(fā)式策略①

艾森陽,宋振明,沈 雪

(西南交通大學 數(shù)學學院,成都 611756)

(西南交通大學 系統(tǒng)可信性自動驗證國家地方聯(lián)合工程實驗室,成都 611756)

可滿足性問題(SATisfiability problem,SAT 問題)是判斷一個以合取范式(Conjunctive Normal Form,CNF)形式給出的命題邏輯公式,在多項式時間內(nèi)是否存在一組真值賦值,使得該公式為真.可滿足SAT 問題,是世界上第一個被證明的NP-Complete 問題[1].同時SAT 問題被廣泛地應用在人工智能、密碼系統(tǒng)、計算機科學等實際領域,因此當前尋找求解SAT 問題的有效算法以提升SAT 求解技術的健壯性和綜合性能極其重要.近年來很多學者對SAT 問題進行了廣泛深入的研究,目前的SAT 算法大致可以分為兩大類:完備性算法和不完備算法.完備性算法采取窮舉和回溯思想,它的優(yōu)點是能保證找到對應SAT 問題的解,在無解的情況下能給出完備證明,但不適用于求解大規(guī)模的SAT 問題.不完備算法基于局部搜索思想,在處理可滿足的大規(guī)模隨機類問題時,往往能比確定性算法更快得到一個解,但絕大多數(shù)隨機搜索算法不能判斷SAT 實例是不滿足的.

本文主要介紹完備性算法,目前流行的完備性算法幾乎都是基于DPLL[2]算法衍生而來,CDCL(Conflict-Driven Clause Learning,CDCL)[3]算法是在DPLL 算法的基礎上添加了高效的啟發(fā)式分支策略[4]、沖突分析與子句學習機制[5,6]以及周期性重啟[7]等技術,使得完備算法處理可解決的SAT 問題越來越多.近年來發(fā)展出很多沖突驅(qū)動型的CDCL 求解器,如Chaff[8]、Zchaff[9]、Minisat[10]、Glucose[11]等,這些求解器已經(jīng)在大規(guī)模實際領域的問題中得到廣泛應用.

本文結(jié)構(gòu)如下:第1 節(jié)介紹SAT 問題的相關知識;第2 節(jié)介紹了幾種分支啟發(fā)式策略;第3 節(jié)引出新的決策啟發(fā)式及其具體算法;第4 節(jié)對比測試與實驗分析;最后總結(jié)全文.

1 預備知識

1.1 相關定義

定義1[12].變量集合.用X表示命題變量的集合,用x1,x2,x3,···,xn代表任意的命題,稱為命題變量,簡稱變量,則X=x1,x2,x3,···,xn用 |X|表 示集合X中含有命題變量的個數(shù).

定義2[12].賦值.從變量集合X到真假值集合{0,1}的函數(shù)叫做真值賦值,簡稱賦值.即v(x):X→{0,1}.如果v(xi)=1,則稱xi在賦值下取真值,否則為取假值.若只有部分變量具有真假值,稱為部分賦值;若全部變量具有真假值,稱為完全賦值.

定義3[12].文字.對任意的變量xi(i=1,2,···,n),xi和 ?xi叫做變量的文字,其中叫做xi正 文字,?xi叫做負文字.

定義4[12].子句.若干個文字的析取(或,∨)稱之為子句,用字母C表示,即C=l1∨l2∨···∨ln,|C|表示子句C中文字的個數(shù).在同一個子句中,文字是不同的.特別地,單個文字也是子句,稱為單元子句,沒有文字的子句稱為空子句.

定義5[12].合取范式.一些子句的合取(與,∧)稱之為合取范式,F(X)=C1∧C2∧···∧Cm,其通式表達為

1.2 相關過程

(1)布爾約束傳播過程(Boolean Constraint Propagation,BCP)

BCP 過程也稱為單元推導.BCP 過程即是反復利用單元子句規(guī)則對子句集里的合取范式不斷地化簡,直到子句集中不再存在單元子句或者出現(xiàn)沖突子句為止.隨著搜索的不斷進行,一個合取范式想要被滿足,則要求其所組成的子句都是可滿足的,所以通過單元規(guī)則會導致一些變量必須被賦值為真(子句中除了一個未賦值的變量外,其余變量都被賦值為0),通過單元規(guī)則導致的變量賦值被稱之為蘊涵[12,13].因為子句集中變量的蘊涵關系,所以BCP 過程又可以通過蘊涵圖直觀地表示出來.

例1.若有子句集:

則可得到蘊含圖,如圖1 所示.

圖1 蘊涵圖

(2)學習子句形成過程

若布爾傳播過程中產(chǎn)生沖突,則求解器進入沖突分析過程,沖突分析結(jié)束后將會產(chǎn)生一個學習子句.經(jīng)證明認為,在沖突分析過程中根據(jù)第一唯一蘊含點(First Unit Implication Point,First-UIP)學習得到的子句是最有效的[14].根據(jù)First-UIP 切割方法,通常把蘊含圖被分為兩個部分:沖突側(cè)和原因側(cè).如圖1 所示,包含沖突節(jié)點的一側(cè)為沖突側(cè),另一側(cè)為原因側(cè).First-UIP 切割線周圍包含了構(gòu)成此次沖突的所有原因,學習子句是這些參與沖突分析的子句通過消解規(guī)則產(chǎn)生.圖1 中參與沖突分析的子句集 φ={C4,C7,C9},生成的學習子句為 ?x6∨x10∨x11.通過學習子句知在任何時候x10和x11被 賦值為0,文字x6必須賦值為0,即求解器不會進入x6=1的搜索空間,避免了進入相同的沖突.

2 現(xiàn)有分支啟發(fā)策略

Chaff 算法表明整個搜索過程中布爾約束傳播占用大部分時間,一個好的分支策略可以快速找到?jīng)Q策變量,減少沖突次數(shù),加速BCP 過程,因此好的分支決策對提高整個SAT 求解器的運行效率意義重大.

2.1 VSIDS 策略

VSIDS(Variable State Independent Decaying Sum)分支變量啟發(fā)式策略,該策略由Moskewic 等于2001 年提出[8].相比早期的分支啟發(fā)式,VSIDS 分支變量啟發(fā)式策略很好地結(jié)合了沖突分析過程.

(1)每一個變量的正、負文字都分配一個計數(shù)器s,并且初始值設置為0;

(2)當學習子句加入到子句集時,該子句中所有的文字活性;

(3)每次分支決策時選擇計數(shù)器分值最高未賦值的文字進行賦值,在有多個相等計數(shù)器的情況下,隨機選擇一個文字進行賦值;

(4)所有文字的得分周期性地除以一個常數(shù).

2.2 VSIDS 策略的有效變體

近年來,隨著SAT 問題研究的深入,VSIDS 算法得到了不斷的改進.NVSIDS(Normalized VSIDS)策略是由Armin 等于2008 年提出[15].該策略為每個變量設置一個計數(shù)器,其中涉及沖突的變量以s′=f·s+(1-f)更新得分,f為衰減因子;未涉及沖突的變量其活性仍被“重新計分”s′=f·s.即在每次沖突中NVSIDS 策略需要更新所有變量的得分.EVSIDS(Exponential VSIDS)策略則是其更有效的實現(xiàn),最初由MiniSAT 的作者提出[10],EVSID 策略僅對涉及沖突的變量通過添加指數(shù)增量的方式來更新變量的得分s′=s+(1/f)i,其中f為衰減因子,i表示沖突次數(shù),未涉及沖突的變量得分不變,由證明得EVSIDS 策略與NVSIDS 策略得分線性相關.

ACIDS(Average Conflict-Index Decision Score)[16],ACIDS 策略與EVSIDS 一樣,對每個變元不區(qū)分正負方向,只保留一個計數(shù)器.變元活躍度累加方式為s′=(s+i)/2 ,式中i為沖突次數(shù).ACIDS 策略不僅給后來的涉及沖突的變量賦予更大的權(quán)重,而且隨著沖突次數(shù)的增加較早發(fā)生的沖突對搜索的影響呈指數(shù)下降.同時ACIDS 中變量的得分僅受沖突次數(shù)i的限制,因此,ACIDS 策略比EVSIDS 策略更加平滑.

除了上述兩種分支策略,目前還發(fā)展出一些其他高效的VSIDS 的變體策略,2016 年Liang JH 等提出的了CHB(Conflict History Based Branching Heuristic)策略[17]及同年提出的LRB(Learning Rate Branching)策略[18]等.這些啟發(fā)式分支策略都是盡可能優(yōu)先滿足學習子句來加速搜索過程,在很大程度提高了求解速度.

3 基于變量混合特征分支策略

上述啟發(fā)式策略有兩方面的優(yōu)勢:(1)僅對參與沖突分析的子句所包含的變量,即參與沖突分析的變量進行活性更新.如圖1 的實例,變量x4,x6,x10,x11,x13的活性值會被更新,即變量參與沖突越多,活躍度越大,相應地活性值也就越高;(2)滿足學習子句優(yōu)先原則,變量活躍度的增加方式與沖突次數(shù)i有關,隨著沖突的發(fā)生,越往后發(fā)生的沖突,活躍度增加的越大.

我們發(fā)現(xiàn)基于沖突分析的活性增長方式并不是完善的,因為對每個參與沖突分析的變量,其活躍度的增量是一致的,沒有根據(jù)變量的所攜帶的一些特性來區(qū)分變量的重要性,而在實際求解階段變量所攜帶的信息是多方面的,如:(1)變量的決策層,在非時序性回溯階段,我們認為當回溯到較低的決策層時,搜素過程對二叉樹的剪枝能力越強;(2)變量最近一次參與沖突分析時的總沖突次數(shù),變量參與沖突分析的沖突差(當前沖突次數(shù)-變量最近一次參與沖突分析時的總沖突次數(shù))越小,我們認為該變量最近越活躍,可以適當給予更高的活性.

針對此問題,本文提出了一種基于變量特性的有效混合策略稱為混合特征分支策略(Mixed Feature Branching Strategy,MFBS),此策略不僅加入了變量最近一次參與沖突分析的總沖突次數(shù),還考慮了參與沖突分析變量所在的原因子句的文字塊距離(Literal Block Distance,LBD).LBD 值指子句中變量所在的不同決策層數(shù)目,Audemard 等證明具有較小LBD 值的子句比具有較高LBD 值的子句更有用[17].實際上LBD 較小,則表明子句需要單位傳播中的決策數(shù)量更少,子句中的變量分布相對更集中,更有利于布爾傳播過程.綜上,我們分析了影響變量決策的兩個因素,為了平衡沖突次數(shù)與LBD 對分支決策影響程度的大小,我們設置調(diào)節(jié)因子來適當?shù)仄胶夥治?本文的策略具體表述如下:

(1)為每個變量設置一個計數(shù)器,初始為0;

(2)對于參與沖突分析的變量,活躍度增長方式為s′=s+Hyb(v)·Inc;

(3)每次分之決策時,挑選計數(shù)器分值最大的為賦值的變量,作為下一個決策變量.若多變量值相同,則隨機挑選一個文字賦值.

在步驟(2)的等式中:

其中,α為調(diào)節(jié)因子,lastcon flict為變量最近一次參與沖突分析的總沖突次數(shù),nconflicts為當前沖突次數(shù).Inc為活性增長因子,初始值取1,每次沖突更新Inc/Decay,Decay是一個(0,1)區(qū)間的實數(shù),在Minisat中,Decay=0.95 .由Hyb(v)的定義值,頻繁參與沖突分析的變量其活性增長速度比長時間未參與沖突分析的變量快,且具有較小的子句LBD 的變量更有優(yōu)勢.基于此我們可以生成MFBS 的偽代碼,在算法1 中第7 行,本文用MFBS 策略代替了原版分支策略,即當變量出現(xiàn)在沖突分析中,變量的活性以新的策略更新.每次進行分支時,總是選擇活性值最大的變量作為下一個分支變量,如算法1 所示.

?

4 實驗分析

Glucose 作為國際先進的求解器,近些年部分優(yōu)秀的求解器都是在此基礎上的改進,2009 年Glucose 3.0 獲得SAT Main Track 組競賽冠軍,2017 年其并行版本求解器Syrup 獲得冠軍等,本文則選取最新的Glucose4.1 求解器為基礎,把MFBS 分支策略嵌入Glucose4.1 生成Glucose4.1+MFBS 版本,下一步將兩版本進行實驗對比分析.

4.1 實驗環(huán)境

本文選取的實驗機器配置為Windows 64 位操作系統(tǒng),Intel(R)Core(TM)i3-3240 CPU 3.40 GHz 8 GB內(nèi)存.

4.2 實驗方法

兩個版本的求解器都在4.1 的實驗配置下,分別對2017 年SAT 競賽Main Track 組實進行測試.2017年實例總體可分為兩大類:g2 和mp1,本文首先在每類中隨機選取一個小類別共(108 個),其中包括:g2-T(40)、g2-test(2)、g2-UGG(3)、g2-UR(2)、g2-UTI(2)和mp1 構(gòu)成第1 步的測試例.實驗第2 步選取第1 步表現(xiàn)較好的求解器,對2017 年SAT 競賽的350 個實例,進行綜合測試.兩個過程中每個實例均限時3600 s,若超時未解決自動終止.

4.3 實驗結(jié)果分析

本文首先在理論上提出的兩個特征因素,但對于每個特征因素的對分支決策的影響還需要進一步通過實驗說明.因此為了綜合評估MFBS 算法的求解性能,充分探究各個特征因素對分支的影響,本次實驗首先對調(diào)節(jié)因子 α設置了3 個參數(shù),實驗中α 取值分別為α={0.4,0.5,0.6,0.7}.表1 則為Glucose4.1+MFBS 的4 個版本與Glucose4.1 原版的對比,在不可滿足問題上Glucose4.1+MFBS 4 個版本與原版求解器實力相當,在可滿足性問題上Glucose4.1+MFBS 4 個版本中有2 個版本較優(yōu)于原版求解器,0.5 版本求解效果最好,相對于Glucose4.1 求解實例增加了9.4%.

圖2 表示不同版本的4 個求解器與原策略對108 個實例求解時間對比.黑色實心三角代表原版求解器,圖中曲線上每個點代表一個實例,曲線越靠近x 軸,則表明曲線所代表的求解器求解時間越少,求解個數(shù)越多.從圖中可以看出是4 個版本中有3 個版本的求解時間均優(yōu)于原版求解器,其中α =0.5和 α =0.6最有求解優(yōu)勢,求解時間明顯小于原版.

表1 Glucose 與Glucose4.1+MFBS 求解個數(shù)對比(108 個)

圖2 Glucose 與Glucose_4.1+MFBS 的求解性能對比

為了更深一步探究求解器的性能,以下的實驗,將針對本文第一步測試的較優(yōu)的兩個求解器:α =0.5和α=0.6進行更深入的測試.實驗選取2017 年剩余的實例242 個(共350 個)進行測試,實驗結(jié)果如表2 所示,可以看出,α =0.5的版本在求解不可滿足性問題的能力要弱于可滿足性問題,α =0.6版本表現(xiàn)相對比較穩(wěn)定,對于不可滿足實例和原版求解器求解能力相當.但兩個改進版本求解實例總個數(shù)均多于原版,說明MFBS策略對于求解可滿足性問題具有一定的優(yōu)勢,整體在求解能力上有所提高,同時也進一步說明本文所提出的兩個影響因子對分支決策,有一定的促進作用,且LBD 值相比沖突次數(shù)對分支決策影響更大.

表2 Glucose 與Glucose4.1+MFBS 求解個數(shù)對比(350 個)

圖3 列出了兩個版本的求解器與原版求解器的求解個數(shù)與求解時間的關系,實心三角代表原版,空心圖形代表MFBS 版本.因MFBS 策略傾向于求解可滿足性問題,所以針對2017 年350 個實例的總體求解時間表現(xiàn)有所減弱.可以看出前一段實例3 個求解器求解時間高度重合,在中間部分原版求解器的求解性能要高于本文提出的兩個版本,但在求解較難問題時,本文的兩個版本又表現(xiàn)出優(yōu)于原版的性能,尤其對于多求解出來的實例,每個實例用時接近于3600,因此也會增加總體的平均求解時間.

圖3 Glucose4.1 與Glucose4.1+MFBS(α )求解性能對比

5 結(jié)論與展望

因求解實際的SAT 問題的多樣性和復雜性,使SAT 問題求解難度提高.本文所提出的混合啟發(fā)式策略,不僅考慮了變量在參與沖突分析的次數(shù),還加入了變量所在沖突子句的LBD 值,相比傳統(tǒng)單一的啟發(fā)式策略,具有一定的優(yōu)勢,測試結(jié)果表明混合策略在一定程度上要優(yōu)于原始策略.

后續(xù)將對混合啟發(fā)式策略進一步測試,從中探究不同實驗參數(shù)對整體求解性能的影響,發(fā)現(xiàn)不同因素之間的聯(lián)系,進而更好地提高求解器的求解性能.