常文靜，徐 揚，吳貫鋒

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

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

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

3.系統(tǒng)可信性自動驗證國家地方聯(liá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 引言

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

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

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

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

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

2 基礎(chǔ)知識

算法1典型CDCL算法

輸入：CNF公式Σ。

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

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

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

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

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

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

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

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

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

3.1 舉例說明

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

3.1.1 依據(jù)LBD值排序

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

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

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

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

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

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

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

3.1.2 依據(jù)length排序

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

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

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

3.1.3 比較分析

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

輸出：新的學(xué)習(xí)子句集合Δ，學(xué)習(xí)子句個數(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í)行過程，只是二者的排序標準不同和刪除學(xué)習(xí)的條件不同。算法3中依據(jù)length排序，當符合條件clause.lbd()≥threshold2時，刪除學(xué)習(xí)子句。在現(xiàn)有的CDCL SAT求解器中reduce DB（）函數(shù)是根據(jù)LBD值排序，刪除符合clause.lbd()≥2和clause.size()≥2的學(xué)習(xí)子句，但是通過3.1節(jié)的實驗分析可知，此刪除標準會刪除部分對求解過程起到促進作用的子句，因此算法2和算法3綜合考慮了兩種標準，對學(xué)習(xí)子句進一步地刪選，保留更多的有用子句。

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

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

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

4 實驗

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

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

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

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

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

5 結(jié)束語

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

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