基于演繹長(zhǎng)度的學(xué)習(xí)子句刪除策略

常文靜，徐 揚(yáng)，吳貫鋒

CHANG Wenjing1，3,XU Yang2，3,WU Guanfeng1，3

1.西南交通大學(xué) 信息科學(xué)與技術(shù)學(xué)院，成都 610036

2.西南交通大學(xué) 數(shù)學(xué)學(xué)院，成都 610036

3.系統(tǒng)可信性自動(dòng)驗(yàn)證國(guó)家地方聯(lián)合工程實(shí)驗(yàn)室，成都 610036

1.School of Information Science and Technology,Southwest Jiaotong University,Chengdu 610036,China

2.School of Mathematics,Southwest Jiaotong University,Chengdu 610036,China

3.National-Local Joint Engineering Laboratory of System Credibility Automatic Verification,Chengdu 610036,China

1 引言

布爾可滿足問(wèn)題（Boolean Satisfiability Problem，SAT問(wèn)題）是首個(gè)被證明是NP完全的問(wèn)題[1]，具有十分重要的理論意義。布爾變量x可以被賦值為true（1）或false（0），由一個(gè)或多個(gè)變量的析取組成一個(gè)子句，若子句中至少存在一個(gè)變量賦值為1，則該子句是可滿足的。由一個(gè)或多個(gè)子句的合取構(gòu)成合取范式（Conjunction Normal Form，CNF），SAT問(wèn)題一般可轉(zhuǎn)化成CNF表示。判定SAT問(wèn)題的滿足性是指若存在一組變量賦值{x1,x2,…,xN}（N為子句集F中的變量個(gè)數(shù)），使得子句集F中所有的子句都是可滿足的，則子句集F是可滿足的，或者給出證明，對(duì)于變量的任何賦值，子句集F都是不可滿足的。近年來(lái)，SAT問(wèn)題的判定技術(shù)也應(yīng)用在實(shí)際領(lǐng)域中，如人工智能規(guī)劃（AI Planning）、定理證明、軟件及硬件驗(yàn)證、集成電路設(shè)計(jì)與驗(yàn)證等。求解SAT問(wèn)題的算法主要分為兩類：完備算法和不完備算法。盡管不完備算法可快速求解，卻不能證明問(wèn)題是不可滿足的。完備算法不僅能在問(wèn)題的屬性是可滿足時(shí)給出問(wèn)題的解，而且在問(wèn)題無(wú)解時(shí)可以給出一個(gè)完備的證明，證明此問(wèn)題是不可滿足的?，F(xiàn)實(shí)生活中許多實(shí)際應(yīng)用問(wèn)題需要證明問(wèn)題的無(wú)解，因此本文主要介紹完備算法的相關(guān)內(nèi)容。

當(dāng)前主流的SAT完備求解算法幾乎都是基于DPLL（Davis Putnam Longmann Loveland）算法[2]衍生而來(lái)，DPLL算法主要利用單文字規(guī)則、純文字規(guī)則和分裂規(guī)則，通過(guò)深度優(yōu)先搜索二叉樹(shù)，求解子句集，但是由于SAT問(wèn)題的特殊性，導(dǎo)致DPLL算法在最壞情況下具有以問(wèn)題規(guī)模為指數(shù)的時(shí)間復(fù)雜性。因此，許多研究學(xué)者提出了改進(jìn)算法。其中，沖突驅(qū)動(dòng)子句學(xué)習(xí)（Conflict Driven Clause Learning，CDCL）算法[3]在DPLL算法基礎(chǔ)框架上，主要在以下方面做出改進(jìn)：變量決策[4-7]，沖突分析與子句學(xué)習(xí)[3]，重啟[8]和數(shù)據(jù)結(jié)構(gòu)[7，9]。

CDCL算法的主要思想是：當(dāng)基于深度二叉樹(shù)搜索時(shí)發(fā)生沖突，分析出沖突產(chǎn)生的原因，導(dǎo)致沖突產(chǎn)生的子句就會(huì)被記錄下來(lái)，稱為學(xué)習(xí)子句。每次沖突時(shí)，相應(yīng)地產(chǎn)生一個(gè)學(xué)習(xí)子句，由于實(shí)際應(yīng)用問(wèn)題的規(guī)模較大，其沖突次數(shù)達(dá)到百萬(wàn)次，學(xué)習(xí)子句的數(shù)目會(huì)隨著沖突數(shù)目的增加而不斷增大，在最壞情況下這種增長(zhǎng)速度是變量規(guī)模的指數(shù)級(jí)。學(xué)習(xí)子句數(shù)目的增加影響B(tài)CP的效率，并最終導(dǎo)致可用內(nèi)存耗盡。Silva和Sakallah[3]曾證明，大量的已學(xué)習(xí)子句對(duì)于減小搜索樹(shù)的空間并不是特別有用，有時(shí)只會(huì)對(duì)搜索過(guò)程帶來(lái)額外的開(kāi)銷。因此現(xiàn)今的許多SAT求解器都添加了學(xué)習(xí)子句的刪除功能，提高BCP的效率以及避免出現(xiàn)內(nèi)存爆炸問(wèn)題。

Silva和Sakallah設(shè)計(jì)的求解器GRASP[3]中提出一種基于大小邊界（size-bounded）的學(xué)習(xí)子句刪除策略：一旦學(xué)習(xí)子句中文字個(gè)數(shù)超過(guò)設(shè)定的整數(shù)k時(shí)，則刪除這些子句。Bayardo和Schrag在求解器RelSAT[10]中提出一種基于相關(guān)性邊界（relevance-bounded）的學(xué)習(xí)子句刪除策略：當(dāng)學(xué)習(xí)子句中未被賦值文字的個(gè)數(shù)超過(guò)設(shè)定的閾值i時(shí)，則刪除這些學(xué)習(xí)子句。求解器Chaff[7]中采用一種“懶散”的學(xué)習(xí)子句刪除策略，學(xué)習(xí)子句添加到子句數(shù)據(jù)庫(kù)，當(dāng)此學(xué)習(xí)子句中未被賦值的文字個(gè)數(shù)首次大于n個(gè)時(shí)（n一般取值范圍為100～200），此學(xué)習(xí)子句被標(biāo)記為需要“刪除”的狀態(tài)，在之后的內(nèi)存清理過(guò)程中統(tǒng)一被刪除。求解器BerkMin[11]的設(shè)計(jì)者認(rèn)為最新得到的學(xué)習(xí)子句具有較大的價(jià)值，因?yàn)樾枰馁M(fèi)更多的時(shí)間來(lái)推導(dǎo)出最新得到的學(xué)習(xí)子句。BerkMin中不僅考慮學(xué)習(xí)子句生成的先后順序，即將學(xué)習(xí)子句存儲(chǔ)在隊(duì)列中（先進(jìn)先出），刪除隊(duì)列中前1/16的學(xué)習(xí)子句（但是不包含那些文字個(gè)數(shù)小于8的學(xué)習(xí)子句）；而且考慮學(xué)習(xí)子句的長(zhǎng)度大小，當(dāng)隊(duì)列中后15/16的學(xué)習(xí)子句的文字個(gè)數(shù)大于42時(shí)，也會(huì)被刪除。求解器Minisat[12]中為每個(gè)學(xué)習(xí)子句設(shè)置活躍值activity，當(dāng)子句與沖突有關(guān)時(shí)（包括學(xué)習(xí)子句），增加其活躍值，認(rèn)為活躍值小于其設(shè)定的邊界值k的子句是不相關(guān)的，需要被刪除。Glucose求解器[13]中使用一種新的評(píng)價(jià)學(xué)習(xí)子句的策略——文字塊距離（Literals Blocks Distance，LBD），即子句中所有文字所在的不同的決策層個(gè)數(shù)。認(rèn)為越小LBD值的子句的相關(guān)性越高，其價(jià)值越大，因此對(duì)學(xué)習(xí)子句按照LBD值的大小從大到小排序，刪除一半的學(xué)習(xí)子句（但不包括LBD值為2的子句）?，F(xiàn)有的大多數(shù)SAT求解器中也使用此子句策略，如Lingeling[14]求解器中動(dòng)態(tài)地選擇LBD和activity兩種評(píng)估學(xué)習(xí)子句質(zhì)量的標(biāo)準(zhǔn)，如果學(xué)習(xí)子句的LBD值過(guò)大或過(guò)小，選擇activity評(píng)估標(biāo)準(zhǔn)；求解器MapleCOMSPS[15]中綜合使用LBD和activity兩種評(píng)估標(biāo)準(zhǔn)，只保留LBD值小于6的學(xué)習(xí)子句，其余子句按照activity評(píng)估。文獻(xiàn)[16]建立一個(gè)基于過(guò)程保存的相關(guān)函數(shù)，此函數(shù)在搜索的某階段動(dòng)態(tài)地激活或者凍結(jié)子句。文獻(xiàn)[17]提出一種基于回退層次（BackTracking Level，BTL）的方法，計(jì)算學(xué)習(xí)子句中不同的BTL大小，實(shí)驗(yàn)發(fā)現(xiàn)當(dāng)BTL小于3時(shí)學(xué)習(xí)子句在布爾約束傳播中使用頻率高于其他子句，因此認(rèn)為對(duì)求解過(guò)程具有更大的相關(guān)度，刪除那些相關(guān)度小的子句。文獻(xiàn)[18]認(rèn)為學(xué)習(xí)子句的長(zhǎng)度對(duì)求解過(guò)程有著重要的作用，基于此，提出一種基于隨機(jī)有界長(zhǎng)度的子句刪除策略，定義短子句的長(zhǎng)度為k（即子句中文字個(gè)數(shù)為k），隨機(jī)刪除子句長(zhǎng)度大于k的子句，適當(dāng)?shù)乇４嬉恍╅L(zhǎng)子句對(duì)于推演歸結(jié)證明是必要的，實(shí)驗(yàn)表明增加隨機(jī)性對(duì)于求解部分的SAT問(wèn)題是有效的。文獻(xiàn)[19]提出折中度的概念，綜合考慮子句的長(zhǎng)度(size)、活躍值(activity)和LBD，通過(guò)折中度的大小評(píng)估學(xué)習(xí)子句的質(zhì)量。文獻(xiàn)[20]針對(duì)現(xiàn)有Glucose中基于LBD的子句刪除策略，通過(guò)大量實(shí)驗(yàn)發(fā)現(xiàn)對(duì)于LBD值為2的子句（Glue clause）的利用率過(guò)低，基于此，設(shè)置不同學(xué)習(xí)子句的生存時(shí)間是不同的。

盡管已存在多種管理學(xué)習(xí)子句策略，但由于實(shí)際問(wèn)題的多樣性，目前不存在一種管理學(xué)習(xí)子句策略適用于求解所有的實(shí)例問(wèn)題。因此，本文提出一種基于歸結(jié)演繹長(zhǎng)度評(píng)估學(xué)習(xí)子句有效性方法，并通過(guò)舉例與現(xiàn)有的基于LBD評(píng)估方法進(jìn)行了測(cè)試分析，根據(jù)學(xué)習(xí)子句排序基準(zhǔn)不同，提出兩種不同的結(jié)合算法。對(duì)比實(shí)驗(yàn)結(jié)果表明，所提策略能更好地識(shí)別對(duì)求解過(guò)程有用的學(xué)習(xí)子句，顯著地提高求解效率。

2 基礎(chǔ)知識(shí)

算法1典型CDCL算法

輸入：CNF公式Σ。

輸出：可滿足SAT或不可滿足UNSAT。

1.ξ=Ф； //ζ表示變量賦值集合

2.Δ=Ф； //Δ表示學(xué)習(xí)子句數(shù)據(jù)庫(kù)

3.dl=0； //dl表示決策層次

4.while(true)do

5.conflict=unit Propagation(Σ,ζ)；

6. if(conflict!=null)then

7.learntclause=conflict Analysis(Σ,ζ)；

8.btl=compute BackLevel(learntclause,ζ)；

9. if(btl==0)then return UNSAT

10. Δ=Δ?{learntclause}；

11.if（restart（））thenbtl=0；

12. backjump(btl)；

13.dl=btl；

14. else

15. if(ζ?Σ)then

16. return SAT；

17.if（time To Reduce（））then reduce DB(Δ)；

18.var=pick Decision Var(Σ)；

19.dl=dl+1；

20.ξ=ξ?{select Phase(var)}；

21.end

算法1為基于CDCL的SAT求解器的框架。通過(guò)變量決策分支函數(shù)pick DecisionVar（）選擇決策變量var,并通過(guò)函數(shù)select Phase（）進(jìn)行賦值（算法第18～20行），若所有變量都已被賦值，即ζ表示公式Σ的一個(gè)賦值集合，則可判定子句集Δ的屬性是可滿足的（SAT），并且終止算法（算法第15～16行）。unit Propagation（）是單元傳播函數(shù)，若單元傳播過(guò)程中發(fā)生沖突conflict，則利用conflict Analysis（）函數(shù)生成學(xué)習(xí)子句learntclause，且將學(xué)習(xí)子句添加到子句集F，并通過(guò)compute BackLevel（）函數(shù)非時(shí)序回退到?jīng)Q策層次btl，如果btl=0，則說(shuō)明子句集Δ為不可滿足的，否則，利用backjump（）函數(shù)，回退到btl，從新的決策層次重新開(kāi)始搜索賦值。restart（）表示重啟函數(shù)，當(dāng)求解器達(dá)到設(shè)置的觸發(fā)重啟條件時(shí)，則直接回退到第1決策層，撤銷之前所有的變量賦值。算法第17行的timeToReduce（）表示達(dá)到刪除學(xué)習(xí)子句的條件，此時(shí)需要調(diào)用函數(shù)reduceDB（）對(duì)學(xué)習(xí)子句數(shù)據(jù)庫(kù)Δ進(jìn)行刪除。

刪除學(xué)習(xí)子句時(shí)需考慮兩方面：（1）選擇需要?jiǎng)h除的子句，即對(duì)應(yīng)于算法1中reduce DB（）函數(shù)；（2）刪除子句的頻率，即何時(shí)需要?jiǎng)h除無(wú)用的學(xué)習(xí)子句，即對(duì)應(yīng)于算法1中的time To Reduce（）函數(shù)。Minisat和Glucose中函數(shù)timeToReduce（）滿足以下條件：沖突次數(shù)達(dá)到條件lfirst+linc×x,其中x為調(diào)用刪除策略的次數(shù)，lfirst=2000,linc=300。當(dāng)調(diào)用reduce DB（）函數(shù)時(shí)，將子句按照某種評(píng)估標(biāo)準(zhǔn)的值從大到小排序，刪除序列中前一半的子句。這里，依然保持time To Reduce（）函數(shù)的條件不變，主要研究reduce DB（）函數(shù)中學(xué)習(xí)子句質(zhì)量的評(píng)估標(biāo)準(zhǔn)。

3 基于演繹長(zhǎng)度的學(xué)習(xí)子句刪除策略

對(duì)于一個(gè)以CNF形式表示的公式F和子句Ck，若存在一個(gè)子句序列Π={C1,C2,…,Ck}，則稱Π是由公式F推導(dǎo)出子句Ck的一個(gè)歸結(jié)式。其中，?Ci∈F，子句Ci滿足以下任意條件即可：（1）Ci∈F；（2）Ci是由子句Cm和Cn(m,n≤i)推導(dǎo)出來(lái)的，其推導(dǎo)規(guī)則如下：

Cm=x∨A,Cn=-x∨B?Ci=A∨B其中A和B為子句，x為變量。

文獻(xiàn)[21]已證明基于CDCL的SAT求解器可被形式化為歸結(jié)演繹證明系統(tǒng)。因此，現(xiàn)有的CDCL-SAT求解器的求解過(guò)程可以是一個(gè)包含刪除子句集策略的歸結(jié)演繹過(guò)程。當(dāng)有沖突發(fā)生時(shí)，通過(guò)學(xué)習(xí)子句確定搜索樹(shù)的回退層次，若學(xué)習(xí)子句中每個(gè)變量相對(duì)應(yīng)的賦值層次都較小（即距離二叉搜索樹(shù)的根節(jié)點(diǎn)較近），確定的回退層次也越小，對(duì)搜索空間的約簡(jiǎn)能力也越強(qiáng)，因此認(rèn)為這些學(xué)習(xí)子句對(duì)搜索過(guò)程是相關(guān)的、有效的。學(xué)習(xí)子句可以通過(guò)歸結(jié)過(guò)程演繹得到，因此通過(guò)演繹的長(zhǎng)度length來(lái)評(píng)估學(xué)習(xí)子句的相關(guān)性。設(shè)有學(xué)習(xí)子句Cl，假設(shè)Π={C1,C2,…,Cl}是由公式F推導(dǎo)出學(xué)習(xí)子句Cl的一個(gè)歸結(jié)式，則稱學(xué)習(xí)子句Cl的演繹長(zhǎng)度length為l，記Cl(length)=l。若學(xué)習(xí)子句的l值越小，說(shuō)明通過(guò)歸結(jié)得到此學(xué)習(xí)子句演繹路徑越短，進(jìn)而此學(xué)習(xí)子句中的每個(gè)變量的決策層也較小，相對(duì)應(yīng)的回退層次也越小，這些學(xué)習(xí)子句應(yīng)該被保留。

3.1 舉例說(shuō)明

為了說(shuō)明學(xué)習(xí)子句的演繹長(zhǎng)度length和LBD值在求解過(guò)程中的變化規(guī)律，隨機(jī)選取SAT競(jìng)賽庫(kù)中的實(shí)例g2-ak128boothbg1btisc.cnf測(cè)試說(shuō)明。

3.1.1 依據(jù)LBD值排序

首先，將生成的學(xué)習(xí)子句按照LBD值從大到小排序，如圖1所示。X軸表示生成的學(xué)習(xí)子句數(shù)量，求解實(shí)例g2-ak128boothbg1btisc.cnf的沖突次數(shù)為954次，因此生成954個(gè)學(xué)習(xí)子句。Y軸表示學(xué)習(xí)子句分別對(duì)應(yīng)的LBD值。從圖1可以看出，生成的學(xué)習(xí)子句的LBD值的分布范圍不連續(xù)，有一定的區(qū)間變化。當(dāng)需要?jiǎng)h除學(xué)習(xí)子句時(shí)，按照LBD值從大到小的排序順序，刪除一半的學(xué)習(xí)子句，即刪除圖1中1到477的子句。

當(dāng)學(xué)習(xí)子句依據(jù)LBD值排序時(shí)，每條子句所對(duì)應(yīng)的length值如圖2所示。X軸表示生成學(xué)習(xí)子句數(shù)量，Y軸表示每條學(xué)習(xí)子句所對(duì)應(yīng)的LBD值和length值。

圖1 學(xué)習(xí)子句的LBD值的排序

圖2 學(xué)習(xí)子句對(duì)應(yīng)的LBD值和length值

同時(shí)統(tǒng)計(jì)了不同LBD值的學(xué)習(xí)子句在求解過(guò)程中被使用的次數(shù)（即參與單元傳播和沖突分析的總次數(shù)），如圖3所示。X軸表示每個(gè)學(xué)習(xí)子句相對(duì)應(yīng)的LBD值，Y軸表示不同LBD值的學(xué)習(xí)子句在求解過(guò)程中被使用的次數(shù)。

圖3 不同LBD值的學(xué)習(xí)子句被使用次數(shù)

從圖3可以看出，LBD＜10時(shí)學(xué)習(xí)子句被使用次數(shù)較多。當(dāng)LBD=6時(shí)，其被使用次數(shù)多達(dá)291次。

3.1.2 依據(jù)length排序

類似于3.1.1小節(jié)，圖4表示學(xué)習(xí)子句相對(duì)應(yīng)的length值的排序變化。從圖4可以看出，length值的變化范圍廣泛。

圖5表示不同length值的學(xué)習(xí)子句被使用的次數(shù)情況。從圖5可以看出，學(xué)習(xí)子句的length值越小，在求解過(guò)程中被使用的次數(shù)越多，隨著length值的增大，大多數(shù)學(xué)習(xí)子句被使用的次數(shù)為1。

圖4 學(xué)習(xí)子句的length值的排序

3.1.3 比較分析

當(dāng)求解器執(zhí)行刪除操作時(shí)，進(jìn)一步分析被刪除的學(xué)習(xí)子句的LBD值與length值之間的關(guān)系。按照3.1.1小節(jié)中基于LBD值的評(píng)估方法，1到477范圍的子句需要被刪除。但是從圖2得出，被刪除子句的length值的變化范圍較大，最小值為lengthmin=51，最大值為lengthmax=6169，因此，若這些被刪除的學(xué)習(xí)子句按照l(shuí)ength值評(píng)估其質(zhì)量時(shí)，給出不同length值的被刪除的學(xué)習(xí)子句在求解過(guò)程中被使用的次數(shù)在圖5中的分布情況，如圖6所示。圖6中綠色的點(diǎn)表示被刪除的學(xué)習(xí)子句的length值在求解過(guò)程中被使用的次數(shù)。從圖6可以看出，當(dāng)依據(jù)LBD值的評(píng)估方法刪除學(xué)習(xí)子句時(shí)，仍有部分學(xué)習(xí)子句的length較小，被使用次數(shù)較高，當(dāng)length=212時(shí)，使用次數(shù)為48次，這些子句的相關(guān)性較高，對(duì)求解作用較大，應(yīng)該被保留。

同理，當(dāng)按照3.1.2小節(jié)中l(wèi)ength值的評(píng)估方法，1到477范圍的子句需要被刪除，為了方便觀察，單獨(dú)列出圖4中被刪除學(xué)習(xí)子句所對(duì)應(yīng)的LBD值變化。如圖7所示。

從圖7可以看出，被刪除的那些學(xué)習(xí)子句部分的LBD值較小，最小LBD=9，在圖3中其對(duì)應(yīng)的被使用次數(shù)為72次。同理，給出被刪除的學(xué)習(xí)子句在依據(jù)LBD值評(píng)估時(shí)在求解過(guò)程中被使用的次數(shù)在圖3中的分布情況，如圖8所示。

圖6 被刪除學(xué)習(xí)子句不同length值的被使用次數(shù)

圖7 被刪除學(xué)習(xí)子句的LBD值

圖8 被刪除學(xué)習(xí)子句不同LBD值的被使用次數(shù)

圖8中綠色的點(diǎn)表示被刪除的不同學(xué)習(xí)子句的LBD值被使用的次數(shù)。從圖8得出，當(dāng)依據(jù)length評(píng)估標(biāo)準(zhǔn)刪除學(xué)習(xí)子句時(shí)，仍有部分子句的LBD值較小，這些子句在求解過(guò)程中被使用次數(shù)較多，當(dāng)LBD=11時(shí)，其被使用次數(shù)為112次，這些子句應(yīng)該被保留。

3.2 基于LBD和length的學(xué)習(xí)子句刪除策略

由3.1節(jié)可知，評(píng)估學(xué)習(xí)子句的標(biāo)準(zhǔn)不同，相應(yīng)刪除的子句也是不同的。因此，本文綜合考慮基于LBD值和length值兩種評(píng)估標(biāo)準(zhǔn)，盡可能保留在求解過(guò)程中被頻繁使用的子句。根據(jù)參照排序的基準(zhǔn)值不同，給出兩種不同的評(píng)估學(xué)習(xí)子句的方法。

策略1當(dāng)學(xué)習(xí)子句依據(jù)LBD值的大小排序，刪除學(xué)習(xí)子句時(shí)，同時(shí)考慮學(xué)習(xí)子句的length值，若C(length)＜threshold1，保留此學(xué)習(xí)子句，其算法如下。

算法2刪除學(xué)習(xí)子句算法reduce DB1（）

輸入：學(xué)習(xí)子句集合Δ，學(xué)習(xí)子句個(gè)數(shù)n。

輸出：新的學(xué)習(xí)子句集合Δ，學(xué)習(xí)子句個(gè)數(shù)n/2。sort Learnt Clause（）； //根據(jù)LBD值排序

算法2表示算法1中刪除學(xué)習(xí)子句reduce DB（）函數(shù)的執(zhí)行過(guò)程。首先根據(jù)定義的排序標(biāo)準(zhǔn)——LBD值，對(duì)學(xué)習(xí)子句排序；假設(shè)學(xué)習(xí)子句的總數(shù)為n，需刪除n/2的學(xué)習(xí)子句，即刪除符合條件clause.length()≥threshold1的學(xué)習(xí)子句。

為了確定參數(shù)threshold1的值，測(cè)試2015年SAT競(jìng)賽的300個(gè)Application類型的實(shí)例，運(yùn)行時(shí)間設(shè)置為2000 s。表1表示使用不同的threshold1所對(duì)應(yīng)的求解實(shí)例個(gè)數(shù)。

表1 不同threshold1的求解個(gè)數(shù)和時(shí)間

在求解過(guò)程中，每條學(xué)習(xí)子句的length值較大，因此設(shè)置threshold1的值從100開(kāi)始起步測(cè)試。從表1可以看出，隨著threshold1的值逐漸增大，其求解實(shí)例個(gè)數(shù)逐漸減少，當(dāng)threshold1=300和threshold1=400時(shí)，其求解個(gè)數(shù)相差1個(gè)，但是其平均求解時(shí)間相差較多。當(dāng)threshold1=100和threshold1=200時(shí)，二者的平均求解時(shí)間相差不大，但是threshold1=100的求解個(gè)數(shù)最多。因此，threshold1=100。

策略2當(dāng)學(xué)習(xí)子句依據(jù)length值的大小排序，刪除學(xué)習(xí)子句時(shí)，同時(shí)考慮學(xué)習(xí)子句的LBD值，若C(LBD)＜threshold2，保留此學(xué)習(xí)子句，其算法如下。

算法3刪除學(xué)習(xí)子句算法reduceDB2（）

輸入：學(xué)習(xí)子句集合Δ，學(xué)習(xí)子句個(gè)數(shù)n。

輸出：新的學(xué)習(xí)子句集合Δ，學(xué)習(xí)子句個(gè)數(shù)n/2。

sort Learnt Clause（）； //根據(jù)length值排序

ifclause.lbd()≥threshold2then

remove Clause（）；

else

save Clause（）；

init++；

returnΔ；

算法3同算法2一樣，同樣表示算法1中刪除學(xué)習(xí)子句reduce DB（）函數(shù)的執(zhí)行過(guò)程，只是二者的排序標(biāo)準(zhǔn)不同和刪除學(xué)習(xí)的條件不同。算法3中依據(jù)length排序，當(dāng)符合條件clause.lbd()≥threshold2時(shí)，刪除學(xué)習(xí)子句。在現(xiàn)有的CDCL SAT求解器中reduce DB（）函數(shù)是根據(jù)LBD值排序，刪除符合clause.lbd()≥2和clause.size()≥2的學(xué)習(xí)子句，但是通過(guò)3.1節(jié)的實(shí)驗(yàn)分析可知，此刪除標(biāo)準(zhǔn)會(huì)刪除部分對(duì)求解過(guò)程起到促進(jìn)作用的子句，因此算法2和算法3綜合考慮了兩種標(biāo)準(zhǔn)，對(duì)學(xué)習(xí)子句進(jìn)一步地刪選，保留更多的有用子句。

同理，為了確定參數(shù)threshold2的值，測(cè)試2015年SAT競(jìng)賽的300個(gè)Application類型的實(shí)例，運(yùn)行時(shí)間設(shè)置為2000 s。表2表示使用不同的threshold2所對(duì)應(yīng)的求解實(shí)例個(gè)數(shù)。

表2 不同threshold2的求解個(gè)數(shù)和時(shí)間

從表2可以看出，不同threshold2相對(duì)應(yīng)的求解個(gè)數(shù)相差較大，并不是隨著threshold2增大而逐漸減少，當(dāng)threshold2=20時(shí)的求解個(gè)數(shù)大于threshold2=15時(shí)的求解個(gè)數(shù)，但是當(dāng)threshold2=10時(shí)，其求解個(gè)數(shù)最多，且平均求解時(shí)間最少。因此，threshold2=10。

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

本文主要在求解器Glucose3.0版本的基礎(chǔ)上進(jìn)行實(shí)驗(yàn)測(cè)試，Glucose3.0是國(guó)際上知名的求解器，最近幾年國(guó)際SAT競(jìng)賽專設(shè)一個(gè)基于Glucose3.0版本求解器改進(jìn)的求解器分組比賽，測(cè)試求解器版本為4個(gè)，Glucose_lbd、Glucose_length、Glucose_lbd+len、Glucose_len+lbd。Glucose_lbd中單獨(dú)使用基于LBD的學(xué)習(xí)子句刪除策略，Glucose_length中單獨(dú)使用基于length的學(xué)習(xí)子句刪除策略，Glucose_lbd+len中實(shí)現(xiàn)策略1，參數(shù)threshold1設(shè)置為100，Glucose_len+lbd中實(shí)現(xiàn)策略2，參數(shù)threshold2設(shè)置為10。實(shí)驗(yàn)環(huán)境：Intel Core i3-3240 CPU，3.40 GHz處理器，8 GB內(nèi)存，運(yùn)行系統(tǒng)為Windows7+Cygwin2.8.1。實(shí)驗(yàn)中采用的測(cè)試實(shí)例來(lái)自于2015年SAT競(jìng)賽的300個(gè)Main-track組實(shí)例以及2016年SAT競(jìng)賽的Main-track組的300個(gè)Application類型的實(shí)例。這些實(shí)例來(lái)自于不同的實(shí)際問(wèn)題，例如軟件測(cè)試、硬件電路測(cè)試、圖著色問(wèn)題、網(wǎng)絡(luò)安全等。實(shí)驗(yàn)中每個(gè)實(shí)例的求解時(shí)間不超過(guò)3600 s。表3表示使用4種求解器求解實(shí)例的個(gè)數(shù)對(duì)比情況。

從表3可以看出，求解器Glucose_len+lbd求解實(shí)例個(gè)數(shù)最多，Glucose_lbd求解個(gè)數(shù)最少。其中，求解器Glucose_length的求解個(gè)數(shù)較Glucose_lbd增加了1.9%，說(shuō)明基于演繹長(zhǎng)度length的學(xué)習(xí)子句管理優(yōu)于基于LBD策略，增長(zhǎng)個(gè)數(shù)主要體現(xiàn)在求解不可滿足實(shí)例。求解器Glucose_len+lbd較Glucose_lbd求解個(gè)數(shù)增長(zhǎng)了4.1%，較Glucose_length求解個(gè)數(shù)增長(zhǎng)了2.1%；求解器Glucose_lbd+len較Glucose_lbd求解個(gè)數(shù)增長(zhǎng)了2.5%，較Glucose_length求解個(gè)數(shù)增長(zhǎng)了0.5%。說(shuō)明綜合考慮學(xué)習(xí)子句的評(píng)估標(biāo)準(zhǔn)的策略具有一定的優(yōu)勢(shì)。

圖9表示4個(gè)求解器Glucose_lbd、Glucose_length、Glucose_lbd+len、Glucose_len+lbd分別求解600個(gè)實(shí)例的運(yùn)行時(shí)間對(duì)比。圖9中的波點(diǎn)曲線越靠近右邊以及越靠近x軸時(shí)，說(shuō)明此曲線表示的求解時(shí)間越小和求解個(gè)數(shù)越多。由圖9可以看出，求解器Glucose_lbd+len和Glucose_len+lbd的求解性能均優(yōu)于Glucose_lbd和Glucose_length，其中，求解器Glucose_lbd+len和Glucose_len+lbd二者的求解性能較相近，但是由表3和圖9綜合來(lái)看，求解器Glucose_len+lbd在求解個(gè)數(shù)和求解時(shí)間上均表現(xiàn)了一定的優(yōu)勢(shì)，其求解性能最優(yōu)。

圖9 不同求解器的求解性能

表3 不同求解器的求解實(shí)例個(gè)數(shù)

5 結(jié)束語(yǔ)

本文提出一種新的學(xué)習(xí)子句管理策略——基于歸結(jié)演繹長(zhǎng)度評(píng)估學(xué)習(xí)子句有效性，并與現(xiàn)有的基于LBD評(píng)估方法進(jìn)行結(jié)合。實(shí)驗(yàn)結(jié)果表明，新結(jié)合算法能有效地識(shí)別出對(duì)求解過(guò)程有用的子句，提高求解效率。

本文中一些參數(shù)的設(shè)置是帶有實(shí)驗(yàn)性質(zhì)的，因此，之后可以針對(duì)參數(shù)設(shè)置做進(jìn)一步的研究，更好地提升求解器的求解能力。