摘 要：沖突驅(qū)動(dòng)子句學(xué)習(xí)（conflict-driven clause learning，CDCL）是現(xiàn)代SAT求解器的主流框架，而基于變量活性的分支算法是其高效求解的關(guān)鍵因素之一。將全局學(xué)習(xí)率（global learning rate，GLR）和變量決策層結(jié)合分析，得到兩個(gè)有關(guān)CDCL搜索行為的重要推論：在GLR較高時(shí)，增加低決策層變量的碰撞分?jǐn)?shù)可以降低搜索成本；而在GLR較低時(shí)，增加高決策層變量的碰撞分?jǐn)?shù)可以充分探索解空間。通過實(shí)驗(yàn)數(shù)據(jù)分析，驗(yàn)證了兩個(gè)推論的正確性。依據(jù)推論，提出一種結(jié)合GLR和變量決策層的Gdb啟發(fā)式策略來優(yōu)化現(xiàn)有分支算法，Gdb使用變量決策層設(shè)計(jì)兩個(gè)權(quán)重w₁和w₂，分別用于較高和較低GLR情況下的變量活性。此外，還分析了EVSIDS和LRB兩個(gè)分支算法的搜索行為，并針對(duì) LRB 進(jìn)行再次加權(quán)。實(shí)驗(yàn)結(jié)果表明，Gdb 分支策略有效提升了CDCL求解器的效率。

關(guān)鍵詞： 布爾可滿足性問題； CDCL； 分支策略； GLR； 變量決策層

中圖分類號(hào)： TP391

文獻(xiàn)標(biāo)志碼： A

文章編號(hào)： 1001-3695（2025）02-016-0441-07

doi： 10.19734/j.issn.1001-3695.2024.06.0230

Heuristic optimization algorithm based on variable

decision level and global learning rate

He Fei^a， Wang Xiaofeng^a，b’， Tang Ao^a， Hua Yingying^a， Peng Qingyuan^a， Wang Junxia^a

（a.School of Computer Science amp; Engineering， b.The Key Laboratory of Images amp; Graphics Intelligent Processing of State Ethnic Affairs Commission， North Minzu University， Yinchuan 750021， China）

Abstract：Conflict-driven clause learning （CDCL） is the mainstream framework in modern SAT solvers， with branching algorithms based on variable activity being one of the key factors for efficient solving. By combining global learning rate （GLR） and variable decision levels， CDCL obtained two important inferences about its search behavior： when GLR was high， increasing the collision score of low decision level variables reduced search costs; when GLR was low， increasing the collision score of high decision level variables helped explore the solution space. Experimental data confirmed the correctness of these inferences. Based on these inferences， this paper proposed Gdb heuristic strategy combining GLR and variable decision levels to optimize existing branching algorithms. Gdb used two weights， w₁ and w₂， based on variable decision levels， to adjust variable activity under high and low GLR conditions. The search behavior of the EVSIDS and LRB branching algorithms was also analyzed， and additional weighting was applied to LRB. Experimental results show that the Gdb branching strategy effectively improves the efficiency of CDCL solvers.

Key words：Boolean satisfiability problem（SAT）; CDCL; branching heuristics; GLR; variable decision level

0 引言

可滿足性問題（ＳＡＴ）是自動(dòng)推理和數(shù)學(xué)邏輯中的一個(gè)ＮＰ完全問題，不僅在計(jì)算復(fù)雜性理論中具有重要理論價(jià)值，而且在實(shí)際問題中也有廣泛應(yīng)用。例如數(shù)學(xué)定理證明、模型檢測(cè)、電子設(shè)計(jì)自動(dòng)化、形式化驗(yàn)證和頻譜分配等。此外，可滿足模數(shù)理論問題（satisfiability modulo theories，SMT）可以通過隱式或顯式轉(zhuǎn)換成SAT來解決。求解SAT的算法分為三類：a）完備性算法，如DPLL^［1］和CDCL^{［2，3］}；b）非完備性算法，代表的有近似算法^［4］、隨機(jī)局部搜索算法（stochastic local learch，SLS）^［5］和信息傳播算法^［6，7］；c）基于硬件的SAT求解算法^{［8，9］}。其中，CDCL在應(yīng)用和工業(yè)等實(shí)際問題取得了顯著成功，而SLS在隨機(jī)和難組合問題上比CDCL更有優(yōu)勢(shì)。早期的分支策略采用貪心思想^{［10～13］}，從文字出現(xiàn)次數(shù)、變量個(gè)數(shù)、子句數(shù)目和長(zhǎng)度等考慮設(shè)計(jì)分支算法。然而，基于CDCL框架的VSIDS分支啟發(fā)式^［2］，被認(rèn)為是現(xiàn)代求解器高效率的關(guān)鍵。VSIDS為每一個(gè)文字維護(hù)一個(gè)活性計(jì)數(shù)器，每當(dāng)沖突分析派生的學(xué)習(xí)子句加入子句數(shù)據(jù)庫，該子句中的文字活性計(jì)數(shù)器加1（稱碰撞）。此外，所有文字的活性將周期性除以大于1的常數(shù)f（稱衰減因子）。VSIDS選擇活性最大的文字進(jìn)行分支，若多個(gè)文字活性相同則隨機(jī)選擇。

BerkMin^［14］改進(jìn)了VSIDS，不再是為文字而是變量維護(hù)活性計(jì)數(shù)器，文字每出現(xiàn)在一個(gè)負(fù)責(zé)沖突的子句中，變量的活性就會(huì)遞增。VSIDS的變體NVSIDS^［15］、ACIDS^［16］和EVSIDS^［17］在BerkMin基礎(chǔ)上，對(duì)參與沖突分析的變量都進(jìn)行了碰撞，其碰撞方式不盡相同，但都是從變量活性增長(zhǎng)速度進(jìn)行考慮，現(xiàn)代SAT求解器的VSIDS主流實(shí)現(xiàn)形式是EVSIDS。另外，Audemard等人^［18］在Glucose求解器中提出文字塊距離（literals blocks distance，LBD）用于評(píng)估學(xué)習(xí)子句質(zhì)量，并且利用LBD改進(jìn)EVSIDS，若參與沖突分析的變量在最后一個(gè)決策層且由LBD值小于學(xué)習(xí)子句的原因子句賦值時(shí)，變量會(huì)再次被碰撞。

一些VSIDS變體應(yīng)用CDCL其它技術(shù)設(shè)計(jì)新的啟發(fā)式策略。Du等人^［19］考慮沖突層和變量決策層提出DLBH分支策略，活性更新公式為s′=s/2+n^（d-d_i^）/d。Chen等人^［20］認(rèn)為賦值順序會(huì)對(duì)求解產(chǎn)生不同的影響，結(jié)合決策層和沖突提出CRB分支策略。Chang等人^［21］根據(jù)學(xué)習(xí)子句的LBD值和其決定的回溯層大小，設(shè)計(jì)新的變量獎(jiǎng)勵(lì)機(jī)制，其變量活性更新公式為s′=s+1/lbd+1/btl。王萌等人^［22］利用變量作為決策變量出現(xiàn)的次數(shù)以及變量每次出現(xiàn)所在的決策層提出DVT分支策略。Chowdhury等人^［23］將膠水子句與決策變量聯(lián)系起來設(shè)計(jì)新的GB分支策略，LBD值為2的學(xué)習(xí)子句為膠水子句^{［18，24］}。

對(duì)于EVSIDS，一些改進(jìn)方法被提出。沈雪等人^［25］提出RACT分支策略對(duì)被撤銷賦值的變量再次給予獎(jiǎng)勵(lì)，獎(jiǎng)勵(lì)值由變量上次參與沖突分析時(shí)的總沖突次數(shù)與當(dāng)前的沖突次數(shù)的比值給出。王釔杰等人^［26］考慮到?jīng)Q策變量的子句數(shù)目對(duì)BCP的影響，提出VDALCD分支策略，減少被刪除子句中變量的活性。Liang等人^［27］在MapleCOMSPS求解器中，提升原因側(cè)變量的分?jǐn)?shù)。Jamali等人^［28］利用公式結(jié)構(gòu)，增加高中性變量的碰撞值。Al-Yahya等人^［29］利用公式結(jié)構(gòu)中的backbones和backdoors來提高CDCL求解器的性能。

除了VSIDS-類分支啟發(fā)式，基于強(qiáng)化學(xué)習(xí)思想的分支啟發(fā)式被提出。Liang等人在2016年同時(shí)提出CHB^［30］和LRB^［31］分支啟發(fā)式，兩種啟發(fā)式將變量選擇優(yōu)化問題建模成多臂賭博問題，選擇的變量是可以最大化被稱為獎(jiǎng)勵(lì)值和學(xué)習(xí)率的度量。此外，Xiao等人^［32］根據(jù)依賴假設(shè)，考慮變量與沖突之間的最長(zhǎng)距離提出距離（distance）分支啟發(fā)式。主流的求解器的決策組件實(shí)現(xiàn)都比較復(fù)雜，且大部分遵循在聚焦模式使用VMTF策略^［16］，在穩(wěn)定模式下使用VSIDS和CHB（LRB）^［24］。Cherif等人^［33］在Kissat求解器的穩(wěn)定模式中應(yīng)用多臂賭博框架切換VSIDS和CHB，Gao^［34］在此基礎(chǔ)上使用傳播次數(shù)而非決策次數(shù)設(shè)計(jì)新的臂獎(jiǎng)勵(lì)函數(shù)。CDCL求解器嵌入SLS搜索已經(jīng)成為標(biāo)準(zhǔn)，Cai等人^［35］嘗試?yán)肧LS搜索反饋的信息調(diào)整EVSIDS和LRB的活性分?jǐn)?shù)。

綜合現(xiàn)有研究表明，目前分支啟發(fā)式改進(jìn)方式有五種：a）VSIDS變體從變量活性分?jǐn)?shù)增長(zhǎng)方面考慮，在動(dòng)態(tài)搜索和平穩(wěn)搜索中尋找平衡；b）使用權(quán)重w提升“重要變量”的活性分?jǐn)?shù)，如Glucose求解器再次碰撞變量，Liang提升原因側(cè)變量分?jǐn)?shù)等，該方法是目前主流方法；c）使用CDCL其他參數(shù)指標(biāo)（LBD、變量決策層、回溯層和子句管理等）設(shè)計(jì)新的變量碰撞方法，該方法的缺點(diǎn)是不能及時(shí)反映搜索情況；d）利用SLS搜索反饋的信息提升變量活性分?jǐn)?shù)；e）混合運(yùn)行多種分支啟發(fā)式。除了a）e）兩種，現(xiàn)有分支啟發(fā)式的改進(jìn)方法不盡相同，但核心思想都是提高沖突率，即提高GLR^［36］。

文獻(xiàn)［23，36，37］表明不可滿足實(shí)例的平均GLR比可滿足實(shí)例的平均GLR高，這種差異給本文提供了研究靈感。即，在不同GLR情況下，CDCL搜索行為是否存在差異？本文從CDCL搜索行為的理論分析出發(fā)，結(jié)合GLR和變量決策層，得到兩個(gè)推論。首先，若GLR高于某個(gè)閾值，那么變量決策層越低（越接近根結(jié)點(diǎn)）變量越重要；其次，若GLR低于某個(gè)閾值，變量決策層越高變量越重要，詳細(xì)分析見第2章。依據(jù)這兩個(gè)推論，本文使用變量決策層設(shè)計(jì)兩個(gè)權(quán)重w，根據(jù)CDCL搜索的GLR情況選擇相應(yīng)權(quán)重w，然后使用權(quán)重調(diào)整VSIDS或LRB的活性分?jǐn)?shù)。

不同于文獻(xiàn)［19，20，22，27］使用變量決策層的方式，本文定量分析出兩種CDCL搜索行為，并使用變量的決策層加快兩種CDCL搜索進(jìn)程。實(shí)驗(yàn)結(jié)果表明，本文方法有效提高了SAT求解器的求解效率，并且易于集成到復(fù)雜的求解器中。

1 相關(guān)知識(shí)

1.1 SAT基礎(chǔ)知識(shí)

設(shè)v={x₁，x₂，…，x_n}是一組布爾變量，文字是變量x或其否定┐x。子句是文字的析取，而合取范式（CNF）公式F=C₁∧C₂∧…∧C_m是子句的合取。真值指派α是一個(gè)從變量集V到的映射。其中0代表假（1），1代表真（true）。若變量x被賦值為true（1），則滿足文字x（┐x）。若一個(gè)子句中至少有一個(gè)文字被滿足，則該子句被滿足。如果所有子句被滿足，則滿足公式F。空子句總是不滿足，用⊥表示，并且表示一個(gè)沖突。SAT問題是在CNF公式F中找到一個(gè)滿足所有子句的賦值α，或證明這樣的賦值不存在，即不可滿足。

GLR衡量CDCL求解器在給定問題下生成沖突的能力，設(shè)求解器解決給定公式F一共需要decisions次決策并生成conflicts個(gè)沖突，那么GLR定義為GLR=conflicts/decisions。

CDCL是在DPLL基礎(chǔ)上，引入沖突分析、子句學(xué)習(xí)、重啟、布爾約束傳播（Boolean constraint propagation，BCP）、分支決策和子句刪除等^［38］發(fā)展而來。算法1給出CDCL算法基本框架。

算法1 CDCL算法

輸入：CNF公式F。

輸出：SAT或UNSAT。

1 dl ←0; //決策層

2 α ←; //指派

3 Δ←; //學(xué)習(xí)子句數(shù)據(jù)庫

4 if （UnitPropagation（）==CONFLICT）

5

return UNSAT;

6 while （not AllVariablesAssigned（））

7

dl← dl+1;

8

（x，v）← PickBranchVar（）; //選擇α中未賦值的變量并賦值

9

α←α∪{（x，v）}; //變量賦值保存到指派

10

if （UnitPropagation（）==CONFLICT）

11

（bl，c）← ConflictAnalysisAndLearning（）;

12

Δ←Δ∪（c） //保存學(xué)習(xí)子句到子句數(shù)據(jù)庫

13

if （bllt;0）

14

return UNSAT;

15

else

16

Backtrack（bl）; //回溯

17

dl ← bl;

18

if （TimeToRestart（））//觸發(fā)重啟條件

19

Backtrack（0）;

20

dl←0;

21

if （TimeToReduce（））//觸發(fā)子句刪除條件

22

ReduceLearnedClauses（Δ）;

23 return SAT

CDCL主要使用UnitPropagation（）函數(shù)執(zhí)行布爾約束傳播，一旦BCP發(fā)生沖突，就會(huì)通過ConflictAnalysisAndLearning函數(shù)對(duì)沖突進(jìn)行分析并派生學(xué)習(xí)子句和回溯層bl，然后將學(xué)習(xí)子句添加到子句數(shù)據(jù)庫，最后回溯到bl以避免相同的錯(cuò)誤路徑。對(duì)于18～22行，當(dāng)滿足條件時(shí)就會(huì)觸發(fā)重啟和子句刪除。值得注意的是，算法1并沒有給出CDCL的其他高級(jí)特性，如時(shí)序回溯、SLS組件、有界變量消除和子句活化等。

1.2 主流的分支啟發(fā)式

目前先進(jìn)的CDCL求解器大多采用EVSIDS和LRB分支，下面介紹這兩種啟發(fā)式：

a）EVSIDS對(duì)參與沖突分析的變量活性遞增為var_inc，每次沖突后更新為var_inc/var_decay，MiniSat中var_decay值為0.95，var_inc初值為1。在Glucose中，var_decay從0.8開始，每隔5 000次沖突增加0.01直至0.95。公式表示如下：

activity［x］=activity［x］+（1f）ⁱ（1）

其中： f指var_decay；i是沖突次數(shù)。

b）LRB變量的活性初值為0，其活性更新公式如下：

LRB（x）=（1-α）×LRB（x）+α×p（x，I）L（I）（2）

其中：I是x的賦值到被撤銷賦值發(fā)生的沖突序列（既間隔時(shí)間段）；p（x，I）表示在間隔I內(nèi)包含變量x的學(xué)習(xí)子句數(shù)；L（I）表示在間隔I內(nèi)所有的學(xué)習(xí)子句數(shù)量；α是步長(zhǎng)參數(shù)，其值經(jīng)驗(yàn)初始化為0.4，每次沖突后減小10^－6，直到達(dá)到0.06。

2 基于決策層和GLR的分支策略

2.1 提出動(dòng)機(jī)

GLR作為一種新的指標(biāo)，用于衡量求解器每個(gè)決策所生成的學(xué)習(xí)子句數(shù)量，直觀上學(xué)習(xí)率越高求解器的性能就越好，因?yàn)樯傻膶W(xué)習(xí)子句越多，可裁減的錯(cuò)誤分支就越多。文獻(xiàn)［36］研究表明，一個(gè)好的分支啟發(fā)式往往擁有更高的GLR水平，同時(shí)學(xué)習(xí)子句的LBD值也會(huì)越低。文獻(xiàn)［23，36，37］試圖最大化GLR來改進(jìn)求解器的性能，并且實(shí)驗(yàn)展示了不可滿足實(shí)例比可滿足實(shí)例有更高的平均GLR。雖然變量決策層已經(jīng)被嘗試改進(jìn)分支策略，但并沒有給出合適的解釋說明變量決策層發(fā)揮的作用，文獻(xiàn)［19］也只是從低決策層變量得分增量大于高決策層變量的角度解釋變量決策層可能發(fā)揮的作用。

本文提供一個(gè)新視角審視變量決策層?；跊_突的分支啟發(fā)式從未賦值變量中選擇活性最高的變量作為決策變量。因此，未碰撞前，從根節(jié)點(diǎn)到?jīng)_突節(jié)點(diǎn)沖突分析所涉及的決策變量，變量活性遞減，而決策層遞增。不過，由 BCP 蘊(yùn)涵推導(dǎo)的變量，其活性由過去沖突分析歷史決定（通常由于衰減，活性趨近于0）。此外，SAT 問題的滿足性是變量與子句約束之間的滿足關(guān)系，較強(qiáng)的子句約束，CDCL 搜索過程沖突越頻繁，相應(yīng)的變量活性越高。由此，可以認(rèn)為低決策層的變量在過去搜索中，比高決策層的變量滿足的子句約束多。

現(xiàn)有SAT求解器沒有應(yīng)用GLR的先例，考慮到GLR可以反映CDCL搜索情況：GLR較高時(shí)表明沖突經(jīng)常發(fā)生，且回溯和撤銷賦值頻繁；而GLR較低時(shí)沖突被抑制（較少發(fā)生），變量活性沒有區(qū)分度。那么，結(jié)合變量決策層，有如下推論：

a）當(dāng) GLR 較高時(shí)，增加低決策層變量活性可以快速找到重要變量，從而減少后續(xù)沖突成本，加速探索其他有希望路徑。

b）當(dāng) GLR 較低時(shí)，低決策層的變量可以被認(rèn)為滿足大部分約束，而新的高決策層變量未被充分探索。因此增加高決策層變量活性分?jǐn)?shù)，可以充分探索高決策層區(qū)域的變量解空間，并且可以打破多個(gè)變量活性分?jǐn)?shù)相同的情況。

依據(jù)推論a）b），圖1和2分別表示增加低決策層和高決策層變量活性分?jǐn)?shù)后，CDCL搜索行為示意圖：

圖1、2中，重要變量指的是，在某一段CDCL搜索過程，選擇該變量可以滿足該搜索空間中的子句約束關(guān)系或者跳過該搜索分支；決策變量指的是，在撤銷的變量賦值序列中，活性最高的變量，也即在下一個(gè)搜索中第一個(gè)被選擇作為決策變量；分支節(jié)點(diǎn)，指的是重要變量經(jīng)多次沖突分析及回溯，其活性達(dá)到在下一次搜索中被選作決策變量條件。

圖1左側(cè)展示重要變量在多次沖突分析后也未能成為分支節(jié)點(diǎn)，而圖1右側(cè)展示了增加低決策層變量活性碰撞分?jǐn)?shù)后，較早地使重要變量成為分支節(jié)點(diǎn)，從而減少?zèng)_突分析及回溯成本。圖2則表示在較低GLR情況下，增加高決策層的變量，以滿足局部區(qū)域的子句約束關(guān)系，充分探索有希望分支。

2.2 結(jié)合決策層和GLR優(yōu)化的有效性分析

為驗(yàn)證本文的推論，本文以Glucose 4.2.1為基礎(chǔ)，收集求解器運(yùn)行時(shí)變量活性與變量對(duì)應(yīng)的決策層的信息進(jìn)行分析。具體步驟是，在求解器經(jīng)10 000次沖突后，每隔20 000個(gè)沖突開始收集一次。為方便統(tǒng)計(jì)，在撤銷賦值而非沖突分析中收集信息，原因是在撤銷賦值后，變量會(huì)在下一次搜索中立即進(jìn)行分支。選擇撤銷的時(shí)機(jī)滿足變量的決策層數(shù)目大于2，且撤銷的變量數(shù)目大于50，不收集重啟撤銷的賦值。

由于低學(xué)習(xí)率的SAT實(shí)例撤銷的賦值變量可以達(dá)到幾百上千個(gè)，為方便研究，本文實(shí)現(xiàn)一個(gè)簡(jiǎn)易采樣算法，均勻地按比例采集每個(gè)決策層的變量信息，且保證每個(gè)決策層至少有一個(gè)變量被采集。算法2給出采樣算法的偽代碼：

算法2 dataSampler

輸入：collectData。 //決策層和變量活性對(duì)的向量

輸出：sampleData。

1 totalSamples ← 50;//總共篩選50個(gè)數(shù)據(jù)

2 if size of collectData≤totalSamples

3

return collectData; //直接返回采集的數(shù)據(jù)

4 categorizedData ← new Map;

5 for each （level， activity） in collectData

6 categorizedData［level］.append（activity）;//按決策層分類

7 sort each categorizedData［level］ in descending order;

8 將categorizedData中每個(gè)類別的首個(gè)值添加到 sampledData;

9 rs ← totalSamples-size（sampledData）; //計(jì)算剩余樣本空間

10 for each key in keys（categorizedData）

11

cs ← size（categorizedData［key］）; //獲取類別樣本數(shù)

12

prop ← cs/size（collectData）; //計(jì)算比例

13

sc ← round（prop×rs） //按比例分配剩余樣本

14

step ← cs/（sc+1）; //計(jì)算采樣步長(zhǎng)step

15

index ← step; //初始索引 index

16

while scgt;0 and indexlt;cs //均勻選取樣本

17

ri ← roud（index）-1; //下標(biāo)四舍五入

18

向sampledData添加（key，categorizedData［key］［ri］）;

19

index ← index+step;

20

sc ← sc-1;

21 return sampleData

注意到變量活性的數(shù)量級(jí)相差較大，因此使用下面公式對(duì)其縮放：

activity［x］=activity［x］varInc×100（3）

隨機(jī)選擇2023年SAT Competition中兩個(gè)競(jìng)賽實(shí)例進(jìn)行分析，分別是mchess16-mixed-45percent-blocked.cnf和SC23_Time-table_C_476_E_50_Cl_32_D_6_T_50.cnf，GLR分別為0.77和0.024。每次收集采樣后的數(shù)據(jù)按變量活性從小到大排序，圖3和4分別給出CDCL在較高和較低GLR水平時(shí)的變量與決策層情況。GLR閾值為0.5，超過0.5則稱是較高GLR水平，反之則是較低GLR水平。

從圖3可以看出，GLR大于0.5情況下，高活性的變量其決策層小于低活性變量的決策層，呈現(xiàn)降低趨勢(shì)，說明低決策層的變量很可能是重要變量，增加低決策層變量的活性可以減少搜索重要變量的沖突成本，驗(yàn)證了本文推論a）的正確性。

由圖4可知，變量活性越高，其決策層也越高，呈現(xiàn)上升趨勢(shì)，說明高決策層的變量還會(huì)引發(fā)后續(xù)的沖突，為選找有希望分支應(yīng)繼續(xù)探索高決策層的變量。另外，圖4變量分布較為集中，變量活性相差不大，甚至大部分相同，因此應(yīng)用變量決策層可以打破活性分?jǐn)?shù)相同情況。驗(yàn)證了本文推論b）的正確性。

2.3 Gdb分支策略

在引言中已經(jīng)提到，一些文獻(xiàn)利用權(quán)重系數(shù)w調(diào)整分支啟發(fā)式的碰撞值，本文沿用此做法。不過，使用w調(diào)整LRB和EVSIDS的位置分別是lrb（x）=（1－α）×lrb（x）+α×reward×w和activity［x］=activity［x］+inc×w，reward和inc分別表示LRB的學(xué)習(xí)率和EVSIDS的碰撞值。Gdb方法具體如下：

設(shè)λ=（nlevel-xlevel）/nlevel，nlevel表示發(fā)生沖突的決策層（稱當(dāng)前決策層），xlevel表示變量的決策層。λ越小則越接近沖突層，而λ越大則越接近低決策層。Gdb的權(quán)重w公式如下：

w=μ×log₂（2-λ）+1

GLRlt;ε

μ×log₂（1+λ）+1

GLR≥ε（4）

其中：μ和ε是兩個(gè)參數(shù)，μ是控制權(quán)重w的范圍，ε是GLR的閾值。算法3給出Gdb的偽代碼。

算法3 Gdb算法

輸入：變量。

1 w ← 1;

2 nlevel ← decisionLevel（）;//獲取當(dāng)前決策層

3 if （GLR≠0 and nlevel≠0）

4

xlevel ← level（x）;//獲取變量對(duì)應(yīng)的決策層

5

λ=（nlevel-xlevel）/nlevel;

6

if （GLRlt;ε） //若GLR小于閾值

7

w ← μ×log₂（2-λ）+1;

8

else

9

w ← μ×log₂（1+λ）+1;

10 act［x］=act［x］+inc×w或lrb（x）=（1-α）×lrb（x）+α×reward×w

求解器每次執(zhí)行PickBranchVar（）函數(shù)，就會(huì)計(jì)算GLR的值。每次重啟，GLR清零，下一次搜索時(shí)再重新計(jì)算。另外，若求解器混合使用EVSIDS和LRB，則還需要區(qū)分計(jì)算GLR。

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

3.1 實(shí)驗(yàn)配置

實(shí)驗(yàn)數(shù)據(jù)選自2023年SAT Competition的400個(gè)實(shí)例，其中包括123個(gè)SAT、123個(gè)UNSAT和154個(gè)UNKNOWN實(shí)例。競(jìng)賽實(shí)例是參賽者提交的來自各個(gè)領(lǐng)域的SAT問題，其中306個(gè)是抽取2023年提交的實(shí)例，96個(gè)來自周年紀(jì)念賽道實(shí)例。

實(shí)驗(yàn)環(huán)境配置為：Ubuntu 22.04.1 ×64，Intel^? Xeon^? Gold 6154@3.00 GHz CPU×2，內(nèi)存大小為256 GB。每個(gè)實(shí)例求解截止時(shí)間按SAT競(jìng)賽要求的5 000 s。對(duì)于實(shí)驗(yàn)結(jié)果，本文顯示了成功求解SAT和UNSAT的數(shù)量，以及總的解決數(shù)目。另外，使用國(guó)際競(jìng)賽常用的懲罰平均運(yùn)行時(shí)間PAR-2（Penalized Average Runtime-2）評(píng)估求解器性能，其計(jì)算方式是對(duì)求解器的求解時(shí)長(zhǎng)進(jìn)行求和，如果超時(shí)未解決，求解時(shí)長(zhǎng)將被懲罰為截止時(shí)間的兩倍，最后將結(jié)果除于實(shí)例集數(shù)目得到PAR-2分?jǐn)?shù)。

以Glucose-4.2.1、MapleLCMDistChronoBT-DL-v3、lstech_maple和Kissat-3.1.1為基準(zhǔn)求解器實(shí)現(xiàn)Gdb方法。Glucose求解器在2017年之前多次在SAT Competition獲獎(jiǎng)。Maple-LCMDistChronoBT-DL-v3是2019年SAT Competition主賽道的冠軍求解器，其改進(jìn)版本lstech_maple求解器在2021年SAT Competition獲得第2名。Kissat則是2020年的冠軍求解器，也是目前較先進(jìn)的求解器，自2020年以來，SAT Competition獲獎(jiǎng)求解器都是以Kissat求解器為基礎(chǔ)改進(jìn)的。

Glucose是較為經(jīng)典的CDCL求解器，沒有集成復(fù)雜的組件。除了Glucose，其他三個(gè)求解器實(shí)現(xiàn)了時(shí)序回溯。另外，lstech_maple和Kissat添加了SLS組件，不同的是lstech_maple使用SLS反饋的信息調(diào)整變量的活性分?jǐn)?shù)，而Kissat則沒有。在本文的實(shí)驗(yàn)中，GLR參數(shù)ε的值由經(jīng)驗(yàn)給出，設(shè)置為0.5。

3.2 Gdb在Glucose中實(shí)現(xiàn)

對(duì)于Glucose求解器，使用Gdb改進(jìn)的求解器命名為Glucose+gdb，參數(shù)μ為0.5時(shí)表示為Glucose+gdb-0.5。表1給出Glucose基準(zhǔn)與Glucose+gdb的運(yùn)行結(jié)果。

從表1可知，Glucose+gdb-0.5比Glucose基準(zhǔn)多求解4個(gè)實(shí)例，PAR2分?jǐn)?shù)也比基準(zhǔn)少90.55，Glucose+gdb在μ為0.4和0.6時(shí)，求解個(gè)數(shù)有所下降。前面提到，若變量在最后一個(gè)決策層且由LBD值小于當(dāng)前學(xué)習(xí)子句的原因子句賦值時(shí)，變量會(huì)再次被碰撞，這可能是導(dǎo)致Glucose求解器對(duì)參數(shù)μ敏感的原因。為了驗(yàn)證推論a）b）是單獨(dú)有益于求解器效率提升，還是共同發(fā)揮作用，本文分別使用Glucose+gdb-H和Glucose+gdb-L表示僅使用高GLR和低GLR的權(quán)重w，其參數(shù)μ使用效果最佳的0.5，結(jié)果如表2所示。

表2中，Glucose+gdb-H和Glucose+gdb-L的求解個(gè)數(shù)均比基準(zhǔn)低，這表明推論a）b）對(duì)求解器的效率提升都發(fā)揮了作用。應(yīng)用高GLR的權(quán)重w時(shí)，UNSAT實(shí)例下降明顯，這表明在低GLR情況時(shí)，充分探索高決策層的變量是十分有價(jià)值的。另外，應(yīng)用低GLR的權(quán)重時(shí)，求解個(gè)數(shù)相比基準(zhǔn)下降不多，這并不意外，通常沖突分析很大概率碰撞高決策層的變量。

為了詳細(xì)觀察Glucose求解器求解情況，圖5給出Glucose及其改進(jìn)的求解器的累積分布函數(shù)圖（cumulative distribution function，CDF），曲線越高，求解器越好。

從圖5可知，Glucose+gdb-0.5的求解性能一直優(yōu)于基準(zhǔn)，這表明了本文方法的有效性。然而，遺憾的是Glucose+gdb對(duì)參數(shù)μ敏感，Glucose+gdb-0.4在1 500～3 000 s明顯比基準(zhǔn)差。Glucose+gdb-H的求解性能在5 000 s內(nèi)一直表現(xiàn)很差，令人意外的是，Glucose+gdb-L在前2 000 s內(nèi)優(yōu)于基準(zhǔn)。

3.3 Gdb在MapleLCMDistChronoBT-DL-v3中實(shí)現(xiàn)

MapleLCMDistChronoBT-DL-v3求解器在運(yùn)行初期使用distance分支啟發(fā)式^［32］，后續(xù)運(yùn)行在EVSIDS和LRB之間切換。使用MapleLCMDistChronoBT-DL-v3的目的是觀察Gdb方法是否與時(shí)序回溯配合發(fā)揮最大效果。為方便起見，用mldc表示MapleLCMDistChronoBT-DL-v3求解器，且EVSIDS和LRB的參數(shù)μ相同，表示為mldc+gdb-μ。表3給出運(yùn)行結(jié)果。

從表3可知，對(duì)于MapleLCMDistChronoBT-DL-v3求解器，Gdb方法是有益的，額外求解個(gè)數(shù)最少5個(gè)，最多求解13個(gè)。此外，可以看到，Gdb方法對(duì)于UNSAT實(shí)例的求解效率的提升是明顯的。這不難得出原因，因?yàn)閁NSAT實(shí)例需要更多的沖突才能找到重要的變量，而Gdb減少了沖突成本。此外，對(duì)于SAT實(shí)例提升不明顯，甚至求解個(gè)數(shù)下降1～2，考慮到UNSAT實(shí)例提升明顯，可以忽略這個(gè)影響。為了進(jìn)一步分析，圖6給出mldc基準(zhǔn)及其mldc+gdb求解器的CDF圖。

由圖6可知，Gdb方法在本文給出的參數(shù)中，求解效率一直比基準(zhǔn)求解器高，可說明本文方法的有效性。此外，給出的參數(shù)中，前2 500 s左右圖中曲線幾乎一致。而在2 500 s后，差異逐漸顯現(xiàn)，說明對(duì)于較難求解的實(shí)例，參數(shù)的設(shè)置至關(guān)重要。

EVSIDS和LRB的GLR水平是不同的，一般而言LRB擁有比EVSIDS更高的GLR^［36］。為了分析Gdb在EVSIDS和LRB中的區(qū)別，對(duì)EVSIDS和LRB單獨(dú)應(yīng)用Gdb方法，分別表示為mldc+gdb-E和mldc+gdb-L，參數(shù)μ使用表3中結(jié)果最好的0.5和0.6，表4給出mldc+gdb-E和mldc+gdb-L實(shí)驗(yàn)結(jié)果。

由表4可知，Gdb應(yīng)用在EVSIDS比LRB有更好的結(jié)果，可以推測(cè)，Gdb帶來的性能提升，大部分由EVSIDS貢獻(xiàn)。此外，結(jié)合表3的結(jié)果，兩個(gè)分支策略同時(shí)應(yīng)用Gdb的求解效率提升大于單獨(dú)的改進(jìn)。為了分析EVSIDS和LRB應(yīng)用Gdb時(shí)效果差異原因，隨機(jī)選擇兩個(gè)2023年競(jìng)賽實(shí)例，圖7給出EVSIDS和LRB搜索期間每次重啟時(shí)記錄的決策深度。

從圖7可以看出，EVSIDS折線的波動(dòng)幅度比LRB的大，說明EVSIDS每次重啟或回溯的決策層深度相差相比LRB較大，這有利于Gdb更好區(qū)分不同決策層所在的變量的重要性。因此，Gdb對(duì)EVSIDS的求解效率的提升比LRB高。

為進(jìn)一步分析，圖8給出mldc+gdb-E和mldc+gdb-L運(yùn)行的CDF圖。從圖8可知，大部分實(shí)例在前3 000 s內(nèi)解決，并且在此期間，mldc+gdb-L-0.6略微優(yōu)于mldc，而在3 000 s后，落后于mldc。從整體來看，mldc+gdb-L-0.6的求解效率略差于mldc，PAR2相差9.69也證明這點(diǎn)。此外，mldc+gdb-E-0.5和mldc+gdb-E-0.6的CDF曲線幾乎一致，相比mldc+gdb-L，參數(shù)μ的影響較小。

3.4 Gdb在lstech_maple中實(shí)現(xiàn)

lstech_maple作為MapleLCMDistChronoBT-DL-v3求解的改進(jìn)版本，實(shí)現(xiàn)了SLS搜索有希望的分支，并在相位選擇和分支啟發(fā)式利用了局部搜索賦值和變量沖突頻率。

CDCL結(jié)合SLS是現(xiàn)代SAT求解器的關(guān)鍵特征，為分析Gdb方法是否對(duì)SLS組件有影響，在lstech_maple實(shí)現(xiàn)了Gdb方法，與上一節(jié)描述類似，lstech_maple+gdb-μ表示在EVSIDS和LRB都應(yīng)用Gdb，且參數(shù)μ相同。表5給出其運(yùn)行結(jié)果。

從表5可知，lstech_maple+gdb僅在μ為0.1和0.2時(shí)，總共多求解2個(gè)實(shí)例，SAT實(shí)例求解個(gè)數(shù)在μ為0.2時(shí)減少1個(gè)，而UNSAT求解個(gè)數(shù)分別增加2～3個(gè)。對(duì)于μ為0.3、0.4和0.5，UNSAT求解個(gè)數(shù)分別減少3、2、3，而SAT實(shí)例在μ為0.4時(shí)增加2個(gè)。進(jìn)一步地，圖9給出lstech_maple基準(zhǔn)及其lstech_maple+gdb運(yùn)行結(jié)果的CDF圖。

由圖9可知，lstech_maple在1 000～1 500 s，求解個(gè)數(shù)高于lstech_maple+gdb所有參數(shù)的求解個(gè)數(shù)，但在其后求解效率落后于μ為0.1、0.2和0.4時(shí)的lstech_maple+gdb。2 000 s后，μ=0.3、0.5的lstech_maple+gdb幾乎與lstech_maple基準(zhǔn)相似?？梢钥吹絣stech_maple受參數(shù)μ的影響較大，并表現(xiàn)出求解SAT和UNSAT實(shí)例的差異，為分析該情況，對(duì)lstech_maple的EVSIDS和LRB分別單獨(dú)應(yīng)用Gdb方法。lstech_maple+gdb-E表示使用Gdb改進(jìn)EVSIDS，lstech_maple+gdb-L則是Gdb改進(jìn)LRB。

考慮到LRB回溯時(shí)變量決策層數(shù)較少的缺點(diǎn)，對(duì)權(quán)重w再次加權(quán)，為w′=1.1^w，w′比w更有區(qū)分度，其加權(quán)的求解器用后綴p表示，lstech_maple+gdb-μ_p則表示EVSIDS和LRB的參數(shù)μ一樣，但對(duì)LRB進(jìn)行了再次加權(quán)。參數(shù)μ選擇表5中效果最好的0.2和μ最大的參數(shù)0.5，表6給出運(yùn)行結(jié)果。

從表6可以看到，lstech_maple+gdb-E在參數(shù)μ為0.2和0.5的情況下，求解個(gè)數(shù)并沒有減少。然而，lstech_maple+gdb-L的總的求解個(gè)數(shù)分別下降4和3個(gè)，更具體地，僅是UNSAT求解個(gè)數(shù)減少導(dǎo)致的。由此可知，UNSAT實(shí)例求解個(gè)數(shù)的減少主要是LRB導(dǎo)致的。另外，可以看到lstech_maple+gdb-L-0.2p和lstech_maple+gdb-L-0.5p與其沒有加權(quán)的版本相比，UNSAT實(shí)例求解個(gè)數(shù)分別增加3和4個(gè)，這樣的結(jié)果再次驗(yàn)證3.3節(jié)中本文對(duì)EVSIDS和LRB差異性分析結(jié)果的正確性。

圖10給出表6中列出的求解器的運(yùn)行結(jié)果CDF圖。由圖10可知，lstech_maple+gdb-0.5p的求解性能最好，而lstech_maple+gdb-E-0.5和lstech_maple+gdb-L-0.5p略微優(yōu)于lstech_maple基準(zhǔn)求解器。此外，除了lstech_maple+gdb-0.5p，其他求解器在前1 000 s的曲線幾乎一致，而在1 000 s后逐漸體現(xiàn)出差異，說明對(duì)于較容易解決的實(shí)例，Gdb方法影響不大，而對(duì)較難求解的實(shí)例，需要更合理地設(shè)計(jì)LRB的權(quán)重w。對(duì)于EVSIDS，Gdb方法則實(shí)現(xiàn)了很好的兼容，不需要調(diào)整權(quán)重就能提高求解效率。

3.5 Gdb在Kissat中實(shí)現(xiàn)

Kissat使用的分支啟發(fā)式是VMTF和EVSIDS，在聚焦模式下使用VMTF，在穩(wěn)定模式下使用EVSIDS。考慮到VMTF只專注于最后一次沖突中涉及的文字。因此，本文僅對(duì)EVSIDS實(shí)現(xiàn)了Gdb方法，表7給出Kissat基準(zhǔn)及其改進(jìn)的求解器運(yùn)行結(jié)果。

從表7可知，在Kissat中應(yīng)用Gdb方法，求解個(gè)數(shù)增加1～4。具體地，SAT實(shí)例增加2～4，UNSAT實(shí)例減少1～2個(gè)?？傮w來說，Gdb提高了Kissat的求解效率。圖11給出Kissat及其改進(jìn)的CDF圖。

從圖11可知，Kissat+gdb-0.2和Kissat+gdb-0.3的曲線一直略高于Kissat基準(zhǔn)求解器，Kissat+gdb-0.1、0.4在2 600～4 000 s內(nèi)，求解效率明顯高于Kissat基準(zhǔn)，而在其他時(shí)間段與Kissat基準(zhǔn)不相上下。

Kissat是經(jīng)過高度優(yōu)化的求解器，即使增加一個(gè)求解實(shí)例也是十分困難的，例如2023年SAT Competition主賽道排名前幾的Kissat求解器，其求解個(gè)數(shù)差異僅2到3個(gè)。因此，可以看出，本文方法是十分有效的，且不會(huì)破壞求解器的效率。

4 結(jié)束語

本文通過實(shí)驗(yàn)分析了不同全局學(xué)習(xí)率情況下，CDCL搜索行為的差異，即較高GLR情況下，低決策層的變量往往更重要；而較低GLR情況下，高決策層的變量是比較重要?；诒疚牡姆治觯Y(jié)合GLR和變量的決策層，提出Gdb方法優(yōu)化EVSIDS和LRB分支啟發(fā)式，實(shí)驗(yàn)表明Gdb有效地提高了求解器效率和求解實(shí)例數(shù)量，特別是MapleLCMDistChronoBT-DL-v3，額外解決了13個(gè)。引用SAT求解領(lǐng)域的權(quán)威專家Audemard等人^［39］的一句話：“我們必須先說，改進(jìn)SAT求解器通常是一個(gè)殘酷的世界。以此來舉例，通過解決至少十個(gè)以上的實(shí)例（在競(jìng)賽的一組固定基準(zhǔn)上）通常會(huì)顯示出一個(gè)關(guān)鍵的新特性。通常情況下，競(jìng)賽的獲勝者是根據(jù)解決了幾個(gè)額外的基準(zhǔn)而決定的?！本湍苷f明這問題。因此，本文Gdb方法顯示出SAT求解器的一個(gè)關(guān)鍵特性。

此外，本文還分析了EVSIDS和LRB搜索行為的差異，并在lstech_maple改善了這種差異帶來的不良效果。最后，在更復(fù)雜的Kissat求解器中，Gdb方法可以輕松在Kissat中集成，并且提升了求解效率，而不降低其性能。

不足之處在于GLR的閾值ε和范圍參數(shù)μ不是根據(jù)實(shí)例情況設(shè)置，不同實(shí)例有不同的最佳值。在后續(xù)的研究中，將分析不同實(shí)例的情況，以確定最佳值的設(shè)置。

參考文獻(xiàn)：

［1］Davis M， Logemann G， Loveland D. A machine program for theorem-proving ［J］. Communications of the ACM， 1962， 5（7）： 394-397.

［2］Moskewicz M W， Madigan C F， Zhao Y， et al. Chaff： engineering an efficient SAT solver ［C］// Proc of the 38th Design Automation Conference. Piscataway，NJ：IEEE Press，2001： 530-535.

［3］沈雪， 陳樹偉， 徐揚(yáng)， 等. 基于回跳層數(shù)的SAT求解器學(xué)習(xí)子句刪除策略 ［J］. 計(jì)算機(jī)應(yīng)用研究， 2020， 37（11）： 3316-3320. （Shen Xue， Chen Shuwei， Xu Yang， et al. Back-jump levels based learnt clauses deletion strategy for SAT solver ［J］. Application Research of Computers， 2020， 37（11）： 3316-3320.）

［4］Johnson D S. Approximation algorithms for combinatorial problems ［C］// Proc of the 5th Annual ACM Symposium on Theory of Computing. New York：ACM Press， 1973： 38-49.

［5］Chu Yi， Luo Chuan， Cai Shaowei， et al. Empirical investigation of stochastic local search for maximum satisfiability ［J］. Frontiers of Computer Science， 2019， 13： 86-98.

［6］吳宇翔， 王曉峰， 丁紅勝， 等. 一種改進(jìn)的警示傳播算法求解Max-SAT問題 ［J］. 計(jì)算機(jī)應(yīng)用研究， 2022， 39（8）： 2290-2294. （Wu Yuxiang， Wang Xiaofeng， Ding Hongsheng， et al. Improved warning propagation algorithm for solving Max-SAT problem ［J］. App-lication Research of Computers， 2022， 39（8）： 2290-2294.）

［7］蘆磊， 王曉峰， 牛鵬飛， 等. 求解多文字可滿足SAT問題的置信傳播算法 ［J］. 計(jì)算機(jī)應(yīng)用研究， 2021， 38（9）： 2710-2715. （Lu Lei， Wang Xiaofeng， Niu Pengfei， et al. Belief propagation algorithm for solving multi literal satisfiability problem ［J］. Application Research of Computers， 2021， 38（9）： 2710-2715.）

［8］Ma Kefan， Xiao Liquan， Zhang Jianmin， et al. Accelerating an FPGA-based SAT solver by software and hardware co-design ［J］. Chinese Journal of Electronics， 2019， 28（5）： 953-961.

［9］趙海軍， 陳華月， 崔夢(mèng)天. 基于改進(jìn)連續(xù)時(shí)間動(dòng)態(tài)系統(tǒng)的模擬SAT求解器 ［J］. 計(jì)算機(jī)應(yīng)用研究， 2024， 41（1）： 200-205. （Zhao Haijun， Chen Huayue， Cui Mengtian. Analog SAT solver based on improved continuous-time dynamic systems ［J］. Application Research of Computers， 2024， 41（1）： 200-205.）

［10］Jeroslow R G， Wang Jinchang. Solving propositional satisfiability problems ［J］. Annals of Mathematics and Artificial Intelligence， 1990，1（1）： 167-187.

［11］Freeman J W. Improvements to propositional satisfiability search algorithms ［D］. Philadelphia： University of Pennsylvania， 1995.

［12］Marques-Silva J. The impact of branching heuristics in propositional satisfiability algorithms ［C］// Proc of the 9th Portuguese Conference on Artificial Intelligence. Berlin： Springer， 1999： 62-74.

［13］Buro M， Kleine-Buning H. Report on a SAT competition ［R］. Pader-born： University of Paderborn， 1992.

［14］Goldberg E， Novikov Y. BerkMin： a fast and robust SAT-solver ［J］. Discrete Applied Mathematics， 2007， 155（12）： 1549-1561.

［15］Biere A. Adaptive restart strategies for conflict driven SAT solvers ［C］//Proc of the 11th International Conference on Theory and Applications of Satisfiability Testing. Berlin： Springer， 2008： 28-33.

［16］Biere A， Frohlich A. Evaluating CDCL variable scoring schemes ［M］//Heule M， Weaver S. Theory and Applications of Satisfiability Testing. Berlin： Springer， 2015： 405-422.

［17］Eén N， S?rensson N. An extensible SAT-solver ［C］//Proc of International Conference on Theory and Applications of Satisfiability Testing. Berlin： Springer， 2003： 502-518.

［18］Audemard G， Simon L. Predicting learnt clauses quality in modern SAT solvers ［C］// Proc of the 21st International Joint Conference on Artificial Intelligence. 2009： 399-404.

［19］Du Zhonghe， Song Zhenming. A branching heuristic based on variable decision levels ［C］// Proc of the 12th International Conference on Intelligent Systems and Knowledge Engineering. Piscataway，NJ：IEEE Press， 2017： 1-5.

［20］Chen Qingshan， Xu Yang， Wu Guanfeng， et al. Conflicting rate based branching heuristic for CDCL SAT solvers ［C］//Proc of the 12th International Conference on Intelligent Systems and Knowledge Engineering. Piscataway，NJ：IEEE Press， 2017： 1-5.

［21］Chang Wenjing， Xu Yang， Chen Shuwei. A new rewarding mechanism for branching heuristic in SAT solvers ［J］. International Journal of Computational Intelligence Systems， 2018， 12（1）： 334-341.

［22］王萌， 何星星. 一種基于加權(quán)決策變量決策層的分支策略 ［J］. 計(jì)算機(jī)科學(xué)， 2019， 46（S2）： 19-22. （Wang Meng， He Xingxing. Branching strategy based on weighted decision variable level ［J］. Computer Science， 2019， 46（S2）： 19-22.）

［23］Chowdhury M S， Müller M， You J H. Exploiting glue clauses to design effective CDCL branching heuristics ［C］//Proc of the 25th International Conference on Principles and Practice of Constraint Programming.Cham： Springer， 2019： 126-143.

［24］Oh C. Between SAT and UNSAT： the fundamental difference in CDCL SAT ［C］//Proc of International Conference on Theory and Applications of Satisfiability Testing. Cham： Springer， 2015： 307-323.

［25］沈雪， 陳樹偉， 艾森陽. 基于獎(jiǎng)勵(lì)機(jī)制的SAT求解器分支策略 ［J］. 計(jì)算機(jī)科學(xué)， 2020， 47（7）： 42-46. （Shen Xue， Chen Shuwei， Ai Senyang. Reward mechanism based branching strategy for SAT solver ［J］. Computer Science， 2020， 47（7）： 42-46.）

［26］王釔杰， 徐揚(yáng)， 吳貫鋒. 基于學(xué)習(xí)子句刪除策略的SAT求解器分支策略 ［J］. 計(jì)算機(jī)科學(xué)， 2021， 48（11）： 294-299. （Wang Yijie， Xu Yang， Wu Guanfeng. Branching heuristic strategy based on learnt clauses deletion strategy for SAT solver ［J］. Computer Science， 2021， 48（11）： 294-299.）

［27］Liang J H， Oh C， Ganesh V， et al. MapleCOMSPS， MapleCOMSPS LRB， MapleCOMSPS CHB ［EB/OL］. （2016）. https：//maplesat.github.io/solvers.html.

［28］Jamali S， Mitchell D. Centrality-based improvements to CDCL heuristics ［C］// Proc of the 21st International Conference on Theory and Applications of Satisfiability Testing. Cham：Springer， 2018： 122-131.

［29］Al-Yahya T， Menai M E B A， Mathkour H. Boosting the performance of CDCL-based SAT solvers by exploiting backbones and backdoors ［J］. Algorithms， 2022， 15（9）： 302.

［30］Liang J H， Ganesh V， Poupart P， et al. Exponential recency weighted average branching heuristic for SAT solvers ［C］// Proc of the 30th AAAI Conference on Artificial Intelligence. Palo Alto， CA： AAAI Press， 2016： 3434-3440.

［31］Liang J H， Ganesh V， Poupart P， et al. Learning rate based bran-ching heuristic for SAT solvers ［C］// Proc of the 19th International Conference on Theory and Applications of Satisfiability Testing. Cham：Springer， 2016： 123-140.

［32］Xiao Fan， Li Chumin， Luo Mao， et al. A branching heuristic for SAT solvers based on complete implication graphs ［J］. Science China Information Sciences， 2019， 62： 1-13.

［33］Cherif M S， Habet D， Terrioux C. Kissat mab： combining VSIDS and CHB through multi-armed bandit ［C］// Proc of SAT Competition： Solver and Benchmark Descriptions.2021：1-20.

［34］Gao Y. Kissat MAB prop in SAT competition 2023 ［EB/OL］. （2023）. https：//satcompetition.github.io/2023/.

［35］Cai Shaowei， Zhang Xindi， Fleury M， et al. Better decision heuristics in CDCL through local search and target phases ［J］. Journal of Artificial Intelligence Research， 2022， 74： 1515-1563.

［36］Liang J H， Govind H V K， Poupart P， et al. An empirical study of branching heuristics through the lens of global learning rate ［C］// Proc of the 20th International Conference on Theory and Applications of Satisfiability Testing. Berlin：Springer， 2017： 119-135.

［37］Chowdhury M S， You Jia. Guiding CDCL SAT search via random exploration amid conflict depression ［C］// Proc of AAAI Conference on Artificial Intelligence. Palo Alto， CA： AAAI Press， 2020： 1428-1435.

［38］Marques-Silva J， Lynce I， Malik S. Conflict-driven clause learning SAT solvers ［M］// Handbook of Satisfiability.［S.l.］： IOS Press， 2021： 133-182.

［39］Audemard G， Simon L. Refining restarts strategies for SAT and UNSAT ［C］//Proc of the 18th International Conference on Principles and Practice of Constraint Programming. Berlin： Springer， 2012： 118-126.