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

艾森陽(yáng),宋振明,沈 雪

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

(西南交通大學(xué) 系統(tǒng)可信性自動(dòng)驗(yàn)證國(guó)家地方聯(lián)合工程實(shí)驗(yàn)室,成都 611756)

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

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

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

1 預(yù)備知識(shí)

1.1 相關(guān)定義

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

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

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

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

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

1.2 相關(guān)過(guò)程

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

BCP 過(guò)程也稱(chēng)為單元推導(dǎo).BCP 過(guò)程即是反復(fù)利用單元子句規(guī)則對(duì)子句集里的合取范式不斷地化簡(jiǎn),直到子句集中不再存在單元子句或者出現(xiàn)沖突子句為止.隨著搜索的不斷進(jìn)行,一個(gè)合取范式想要被滿(mǎn)足,則要求其所組成的子句都是可滿(mǎn)足的,所以通過(guò)單元規(guī)則會(huì)導(dǎo)致一些變量必須被賦值為真(子句中除了一個(gè)未賦值的變量外,其余變量都被賦值為0),通過(guò)單元規(guī)則導(dǎo)致的變量賦值被稱(chēng)之為蘊(yùn)涵[12,13].因?yàn)樽泳浼凶兞康奶N(yùn)涵關(guān)系,所以BCP 過(guò)程又可以通過(guò)蘊(yùn)涵圖直觀地表示出來(lái).

例1.若有子句集:

則可得到蘊(yùn)含圖,如圖1 所示.

圖1 蘊(yùn)涵圖

(2)學(xué)習(xí)子句形成過(guò)程

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

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

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

2.1 VSIDS 策略

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

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

(2)當(dāng)學(xué)習(xí)子句加入到子句集時(shí),該子句中所有的文字活性;

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

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

2.2 VSIDS 策略的有效變體

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

ACIDS(Average Conflict-Index Decision Score)[16],ACIDS 策略與EVSIDS 一樣,對(duì)每個(gè)變?cè)粎^(qū)分正負(fù)方向,只保留一個(gè)計(jì)數(shù)器.變?cè)钴S度累加方式為s′=(s+i)/2 ,式中i為沖突次數(shù).ACIDS 策略不僅給后來(lái)的涉及沖突的變量賦予更大的權(quán)重,而且隨著沖突次數(shù)的增加較早發(fā)生的沖突對(duì)搜索的影響呈指數(shù)下降.同時(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)先滿(mǎn)足學(xué)習(xí)子句來(lái)加速搜索過(guò)程,在很大程度提高了求解速度.

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

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

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

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

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

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

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

在步驟(2)的等式中:

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

?

4 實(shí)驗(yàn)分析

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

4.1 實(shí)驗(yàn)環(huán)境

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

4.2 實(shí)驗(yàn)方法

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

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

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

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

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

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

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

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

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

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

5 結(jié)論與展望

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

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