張九龍，王曉峰，2，蘆 磊，牛鵬飛，程亞南

（1.北方民族大學(xué) 計算機(jī)科學(xué)與工程學(xué)院，寧夏 銀川 750021；2.北方民族大學(xué) 圖像圖形智能處理國家民委重點實驗室，寧夏 銀川 750021）

0 引 言

命題邏輯公式的可滿足性問題（Propositional Satis?fiability Problem，SAT）是計算機(jī)理論研究的核心問題之一。SAT 問題在組合電路、邏輯優(yōu)化、人工智能、數(shù)據(jù)挖掘等各領(lǐng)域都有著廣泛應(yīng)用。通常意義下的SAT 問題是判定合取范式（Conjunctive Normal Formula，CNF）的可滿足性問題，具體可描述為：對于一組給定的布爾變量={,,…,x}，集合中的每個元素稱為變元，若變元x在子句中以自身值出現(xiàn)，對應(yīng)的文字稱為正文字，記作x，若變元x在子句中以自身的相反值出現(xiàn)，則對應(yīng)的文字稱為負(fù)文字，記作?x。若干文字的析取構(gòu)成一個子句C，記作C=(∨∨…∨x)。若干子句的合取構(gòu)成合取范式（CNF），記作=(∧…∧C∧…∧C)。SAT 問題的判定指判斷是否存在一組真值賦值，使得該CNF 公式滿足。SAT 問題的求解則是指對于任意的一個合取范式形式表達(dá)的命題邏輯公式，找出使得該公式滿足的所有布爾變元的真值指派。在SAT問題中，每個子句的長度均為的SAT 問題稱為隨機(jī)?SAT 問題。對于隨機(jī)?SAT 問題，進(jìn)一步加強(qiáng)約束條件，限定每個變元在合取范式中出現(xiàn)的次數(shù)恰好為次，形成隨機(jī)規(guī)則(,)?SAT 問題。需要注意的是，本文規(guī)定的隨機(jī)規(guī)則(,)?SAT 問題只規(guī)定了變元出現(xiàn)的次數(shù)，并未對次中變元正負(fù)出現(xiàn)的次數(shù)進(jìn)行限定。

目前，SAT 問題的求解方法主要分為兩大類：一類是基于窮舉和回溯思想的完備算法，以DPLL（Davis Putnam Logemann Loveland）算法和在其基礎(chǔ)上改進(jìn)的CDCL（Conflict?Driven Clause Learning）算 法 為 代 表；另一類是基于局部搜索思想的不完備算法，以隨機(jī)局部搜索（Stochastic Local Search，SLS）算法、消息傳遞（Message Passing，MP）算法和演化計算（Evolutionary Algorithm，EA）算法為代表。對于一個給定的CNF 公式，完備算法理論上可以求得公式的解，即使公式無解的情況下也能給出完備證明。缺點也顯而易見，當(dāng)求解大規(guī)模問題時，所用的求解時間在最壞情況下會隨問題進(jìn)入難解區(qū)域或者變元及子句的增多而呈指數(shù)形式增加，求得解的效果也逐漸變差。不完備算法的優(yōu)點是在處理大規(guī)模數(shù)據(jù)時求解速度相較于完備算法更快，但絕大多數(shù)的不完備算法均無法判斷SAT 問題的可滿足性。完備算法在解決應(yīng)用類實例時效果明顯，對于問題規(guī)模較小的應(yīng)用和組合問題，求解速度甚至快于大多數(shù)的不完備算法。完備算法的改進(jìn)主要是在保證其完備性的同時減少消耗的時間，文獻(xiàn)[5]將膜演算的思想加入DPLL 算法中，簡化了算法的推理過程。文獻(xiàn)[6]提出基于動態(tài)獎懲DRPB 的分支啟發(fā)式算法，通過減小搜索樹的規(guī)模提升求解器的性能。不完備算法求解速度快，并具有一定的并行性，在處理大規(guī)模問題時有較大優(yōu)勢。不完備算法主要分為兩個改進(jìn)方向：一個是與完備算法結(jié)合提升其求解過程的完備性；另一個是優(yōu)化啟發(fā)式策略，增強(qiáng)算法跳出局部最優(yōu)解的能力。文獻(xiàn)[7]在遺傳算法中引入了一種基于DPLL 算法的局部搜索算法，用于求解Max SAT 問題，在多樣化搜索和強(qiáng)化搜索之間實現(xiàn)了更好的平衡。文獻(xiàn)[8]提出了基于任務(wù)分配與調(diào)度的GSAT 算法，使用任務(wù)分配策略與調(diào)度策略共同指導(dǎo)貪心搜索過程，取得了較好的求解效果。

隨著大數(shù)據(jù)時代的到來，數(shù)據(jù)量呈現(xiàn)爆炸式增長，芯片中晶體管的數(shù)量級已從千萬級進(jìn)步到百億級，計算機(jī)的硬件更迭仍滿足不了日益劇增的算力需求。因此，不斷優(yōu)化改進(jìn)求解速度更快的不完備算法是目前SAT 問題求解的一個熱門研究方向。在理論研究層面，隨機(jī)規(guī)則(,)?SAT 問題限定了每個變元在所有子句中出現(xiàn)的次數(shù)恰好為次，比隨機(jī)?SAT 問題更難求解。而現(xiàn)實的工業(yè)生產(chǎn)過程中，很多情形下也對某些具體變量的出現(xiàn)次數(shù)有要求，如現(xiàn)場可編程門陣列映射芯片的設(shè)計與制造。本文在替換的思想上提出了一種新的隨機(jī)規(guī)則(,)?SAT 實例生成RRIG 模型（Random Regular Instance Generation Model），通過實驗驗證了生成模型的正確性和實用性，并改進(jìn)了不完備算法中的模擬退火算法，得到SARSAT 算法用于求解隨機(jī)規(guī)則(,)?SAT 問 題，隨 后 將SARSAT 算 法 和 其 他 相關(guān)算法在RRIG 模型生成的實例集上進(jìn)行了測試，驗證了算法的有效性。

1 標(biāo)準(zhǔn)模擬退火算法

模擬退火思想最早由Metropolis 在1953 年提出，起初并未引起反響，直到1982 年，Kirkpatrick 等人將模擬退火的思想引入組合優(yōu)化領(lǐng)域，提出一種用于求解大規(guī)模組合優(yōu)化問題的有效近似算法——模擬退火算法（Simulated Annealing Algorithm，SAA）。模擬退火算法的思想來自熱力學(xué)與統(tǒng)計物理學(xué)中的固體退火過程，其物理原理為：對于與周圍環(huán)境交換熱量而溫度保持不變的封閉系統(tǒng)，系統(tǒng)的自發(fā)變化總是朝著自由能減少的方向進(jìn)行，當(dāng)自由能達(dá)到最小值時，系統(tǒng)達(dá)到平衡態(tài)。在求解組合優(yōu)化問題時，模擬退火算法能概率性地跳出局部最優(yōu)并趨于全局最優(yōu)。

模擬退火算法源于對固體退火過程的模擬，采用Metropolis 接受準(zhǔn)則，并通過一組稱為冷卻進(jìn)度表的參數(shù)控制算法進(jìn)程，使算法能在多項式時間內(nèi)給出一個近似最優(yōu)解。

標(biāo)準(zhǔn)模擬退火算法：

Step1：初始化，任選初始解∈，給定初始溫度，終止溫度，每個溫度下迭代的馬爾科夫鏈長度為n，令迭代指標(biāo)=0，T=；

Step2：隨機(jī)產(chǎn)生一鄰域解∈()，計算目標(biāo)值增量Δ=()-()；

Step3：若Δ＜0，無條件接受，令=轉(zhuǎn)Step4；否則，利用Metropolis 準(zhǔn)則有條件接受，產(chǎn)生∈(0,1)，若exp( -Δf T)＞，則令=；

Step4：若達(dá)到熱平衡＞n，轉(zhuǎn)Step5，否則，轉(zhuǎn)Step2；

Step5：=+1，降低T，若T＜算法停止，否則，轉(zhuǎn)Step2。

模擬退火算法發(fā)展至今，因其所需要的參數(shù)少、對初始解的容忍性及算法本身良好的收斂性，已廣泛應(yīng)用于各個領(lǐng)域求解組合優(yōu)化問題。文獻(xiàn)[11]從數(shù)學(xué)角度證明了模擬退火算法在固定溫度下迭代足夠長時間，再將溫度降低到下一級，當(dāng)溫度趨近于零時，可獲得最低能量狀態(tài)。若想求得解的效果好，模擬退火算法降溫的過程需要足夠慢，這就會導(dǎo)致算法執(zhí)行所需要的時間較長。因此，在使用模擬退火算法求解不同實際問題時需要做出相應(yīng)的改進(jìn)。目前對模擬退火算法的改進(jìn)主要分為兩個大的方向：一類是將模擬退火算法與其他算法結(jié)合使用，各算法間取長補短；另一類是在標(biāo)準(zhǔn)的模擬退火算法的基礎(chǔ)上對退火策略、擾動策略等進(jìn)行相應(yīng)的改進(jìn)，從而提升算法性能。

標(biāo)準(zhǔn)模擬退火算法的算法流程如圖1 所示。

圖1 標(biāo)準(zhǔn)模擬退火算法流程圖

2 規(guī)則(k,d)?SAT 生成模型

現(xiàn)有的隨機(jī)正則(,)?SAT實例生成模型有文獻(xiàn)[17]提出的格局模型、文獻(xiàn)[18]提出的嚴(yán)格隨機(jī)正則SRR 模型等。其中，在格局模型生成的實例中，有可能存在著兩種非法情形：某個變元在某個子句中重復(fù)出現(xiàn)多次，或者出現(xiàn)若干重復(fù)的子句。由于格局模型生成隨機(jī)實例的方式較為簡單，且在證明隨機(jī)正則(,)?SAT 問題的可滿足臨界值中易于進(jìn)行相關(guān)的概率分析，所以該模型生成的實例通常用來證明可滿足臨界而非用于求解。在嚴(yán)格隨機(jī)正則SRR 模型中，為了防止產(chǎn)生非法公式，在生成實例的過程中也會增加一定的限制，因此SRR模型在可滿足臨界時不易做相關(guān)的概率分析。除此之外，兩個模型生成的實例均為正負(fù)變元出現(xiàn)次數(shù)相等或至多差一次的情況，用于研究正則SAT 判定及其相關(guān)的證明問題，而非本文中不限變元正負(fù)出現(xiàn)次數(shù)的隨機(jī)規(guī)則SAT 問題。本文使用替換的思想在兩個模型的基礎(chǔ)上改進(jìn)后得到隨機(jī)規(guī)則(,)?CNF 實例產(chǎn)生模型——RRIG(,,)模型。該模型包括變元規(guī)模、子句長度和變元出現(xiàn)次數(shù)等3 個參數(shù)，在RRIG 模型產(chǎn)生的實例中，每個子句恰有個不同的文字，每個變元恰好出現(xiàn)次。下面給出RRIG（,,）模型生成隨機(jī)規(guī)則(,)?SAT 實例的具體過程。

Input：變元出現(xiàn)次數(shù)，子句長度和變元規(guī)模。

Step1：置=，=，=0；

Step2：對于每個變元v，隨機(jī)產(chǎn)生random（0，）個正文字，?random（0，）個負(fù)文字置于盒子中；

Step3：若中文字個數(shù)D＜且文字種類type ＜，轉(zhuǎn)Step5；

Step4：從中不放回的隨機(jī)選取個文字?,?,…,?組成一個子句C；

Step4.1：若＜-轉(zhuǎn)Step4.2，否則，轉(zhuǎn)Step5；

Step4.2：若選取的文字互不相同，且C沒有出現(xiàn)在中，轉(zhuǎn)Step6，否則，=+1，轉(zhuǎn)Step4；

Step5：若1 ＜type ＜轉(zhuǎn)Step5.1；否則，轉(zhuǎn)Step5.2；

Step5.1：隨機(jī)選取type 個不含C中文字的子句，在每個子句中任意選擇一個變元替換C中的變元，轉(zhuǎn)Step6；

Step5.2：隨機(jī)選取個不含C中文字的子句，從中任選一個文字進(jìn)行替換，轉(zhuǎn)Step6；

Step6：將C以合取的方式連接到中，置={?,?,…,?}，=+1；

Step7：若＜，返回Step3，否則，輸出并結(jié)束處理。

Output：隨機(jī)規(guī)則(,)?CNF 公式。

在隨機(jī)?SAT 問題中，當(dāng)≥3 時，問題屬于NP?完全問題，通過分析算法的計算復(fù)雜性，求解NP 復(fù)雜類中所有的判定或者優(yōu)化問題，在最壞的情況下會與?SAT（≥3）的判定難度相當(dāng)。隨機(jī)3?SAT 問題作為隨機(jī)?SAT 問題中最簡潔的NP?完全問題，在計算機(jī)復(fù)雜性理論研究中有著重要的作用。因此，將取值為3 得到RRIG（,3,）模型生成隨機(jī)規(guī)則（3，）?CNF 實例。

為驗證RRIG（,3,）生成模型的準(zhǔn)確性，在不同的取值下各生成100 個實例，使用完備SAT 求解算法MiniSat 進(jìn)行求解得到不同的值下滿足實例的比例。為子句個數(shù)，為變元個數(shù)，以約束密度=作為橫坐標(biāo)，可滿足性為縱坐標(biāo)畫出在不同值下實例的可滿足性變化，得到RRIG 模型生成的隨機(jī)規(guī)則（3，）?SAT 實例的相變?nèi)鐖D2 所示。

圖2 RRIG（N，3，d）模型生成實例可滿足性相變圖

目前對于隨機(jī)3?SAT 的相變點，理論上研究表明：3.52 ≤α(3)≤4.489 8，實驗表明，α(3)4.267。在隨機(jī)3?SAT 問題中，當(dāng)＜α(3)時，實例有較大的概率有解；當(dāng)＞α(3)時，實例有解的概率是較小的；當(dāng)處于α(3)附近時，隨機(jī)3?SAT 問題是比較難解的。隨機(jī)規(guī)則（3，）?SAT 作為隨機(jī)3?SAT 的子類，在添加隨機(jī)規(guī)則后難解程度變大，相變點應(yīng)相應(yīng)變小，通過圖2 分析可得，利用RRIG(,3,)模型生成實例的約束密度在4.21附近，故此模型是準(zhǔn)確的。

3 SARSAT 算法

SARSAT 算法優(yōu)化模型保留了標(biāo)準(zhǔn)SA 算法的主體框架，針對隨機(jī)規(guī)則(,)?SAT 問題，分別對擾動策略、選擇策略退火過程等做出了相應(yīng)改進(jìn)。

3.1 問題的轉(zhuǎn)化

利用命題邏輯公式中限制性公式的相關(guān)理論，可將SAT 問題等價轉(zhuǎn)換為多項式函數(shù)優(yōu)化問題。對于給定的CNF 公式，將∧看成乘，將∨看成加，將變元v視為實參數(shù)x，令表示這種轉(zhuǎn)換，用()表示公式的能量函數(shù)，則SAT 問題可以轉(zhuǎn)化為一個求相應(yīng)函數(shù)最小值的優(yōu)化問題。如：

當(dāng)在一組真值指派σ∈{0,1}下使得能量函數(shù)取值為0 時，公式是滿足的，稱σ為此SAT 問題的一個解。

3.2 擾動策略

在標(biāo)準(zhǔn)模擬退火算法中，每個溫度下都需要擾動盡可能多的次數(shù)才能保證找到的狀態(tài)是當(dāng)前溫度下能量較低的狀態(tài)，這正是模擬退火算法中最影響效率的部分。為了減少模擬退火算法擾動過程消耗的時間，提升算法性能，本文采用了一定的啟發(fā)式策略來指導(dǎo)擾動過程。對于給定的隨機(jī)規(guī)則(,)?CNF 公式，在算法開始前隨機(jī)給定一組真值賦值∈{0,1}，記作，記公式在賦值下滿足的子句集合為，不滿足的子句集合為。統(tǒng)計中的變元及其出現(xiàn)的次數(shù)，構(gòu)建一個用于記錄變元滿足性的矩陣，中每列代表一個變元，行代表變元a第（∈(1,)）次在子句中出現(xiàn)時的滿足情況。若滿足記為1，不滿足記為0。將得到的矩陣記為：

統(tǒng)計下各變元對應(yīng)滿足的子句個數(shù)S，則每個變元對應(yīng)的不滿足的子句個數(shù)為-S。采用改進(jìn)的輪盤賭平方策略，各變元被選擇的概率如下：

3.3 退火過程

影響模擬退火算法效率的另一個關(guān)鍵是冷卻進(jìn)度表，通常情況下一個冷卻進(jìn)度表包括以下參數(shù)：控制參數(shù)的初值；控制參數(shù)的衰減函數(shù)；控制參數(shù)的終值。

初值和終值需要根據(jù)具體實際問題進(jìn)行賦值。冷卻進(jìn)度表中最重要的是衰減函數(shù)的選擇，衰減函數(shù)的好壞會直接影響找到解的質(zhì)量。若溫度降低太快，容易導(dǎo)致算法找到的不是全局最優(yōu)解，反之若溫度降低速度太慢，又會影響算法的執(zhí)行效率。常用的降溫策略有快速降溫和指數(shù)降溫，本文在指數(shù)降溫的基礎(chǔ)上增加了回溫過程。溫度衰減函數(shù)如式（4）所示：

式中：為初始溫度；為終止溫度；為降溫因子；為升溫因子。取=1000,=0.01，=0.96，=0.6，可得到該情況下的降溫曲線如圖3 所示。

圖3 T0 =1 000,Tf =0.01,δ =0.96,η=0.6 時降溫曲線

指數(shù)降溫的過程不緊不慢，是模擬退火中最常用的降溫函數(shù)。在指數(shù)降溫的基礎(chǔ)上加入回溫過程，若溫度降低到一定程度時還未找到最優(yōu)解，將溫度升高，根據(jù)Metropolis 準(zhǔn)則接受壞解的概率變大，使得算法在求解過程中有多次跳出局部最優(yōu)的機(jī)會，從而更容易找出全局最優(yōu)解。

3.4 SARSAT 算法

SARSAT 算法流程如下：

Step1：初始化，，、總迭代次數(shù)、馬氏鏈長度。隨機(jī)給定一組真值賦值。

Step2：在每個不滿足的子句中采用式（3）選擇變元進(jìn)行擾動，使用貪心策略選擇擾動得到的個個體中能量最小的狀態(tài)記為()，計算能量差值Δ=(-)。

Step3：令=+1，若Δ＜0，則轉(zhuǎn)Step4，否則，若exp( -Δ)≤random(0,1)，轉(zhuǎn)Step2。

Step4：令=,()=()。

Step5：若＜，轉(zhuǎn)Step2。

Step6：根據(jù)式（4）的降溫過程，判斷是否達(dá)到最大迭代次數(shù)，是就停止，否則，轉(zhuǎn)Step2。

4 實驗分析

實驗中主機(jī)配置為Inter Core i5?6300HQ CPU，NVIDIA GeForce GTX960M 顯卡，在Python 3.8.2 下編程實現(xiàn)，編程軟件為Pycharm，版本為2020.2。

隨機(jī)規(guī)則(,)?SAT 是隨機(jī)?SAT 的子集，為驗證本文改進(jìn)的模擬退火算法的有效性，將本文算法SARSAT 與求解隨機(jī)?SAT 問題的不完備算法Walksat、混合蟻群遺傳HAGSAT 算法進(jìn)行對比實驗，SARSAT算法使用的初始參數(shù)如表1 所示。

表1 算法運行參數(shù)

本文使用的實例取自RRIG(,3,)模型產(chǎn)生的不同變元數(shù)和變元出現(xiàn)次數(shù)的實例，每種情況下各產(chǎn)生20 個實例。對每一個實例，使用三種算法各重復(fù)20 次實驗并記錄實驗中求解的平均準(zhǔn)確率、無法找到解時的不滿足子句占總子句數(shù)的比例ns，變元平均翻轉(zhuǎn)次數(shù)，所得的實驗記錄如表2 所示。

通過分析表2 可知，當(dāng)控制變元出現(xiàn)的次數(shù)不變時，隨著變元個數(shù)的增加，三種算法的執(zhí)行所需要的時間均變長，變元翻轉(zhuǎn)的次數(shù)增多，且三種算法執(zhí)行所消耗的時間趨勢也不同，HAGSAT 算法增長最快、Walksat算法次之、SARSAT 算法增長最慢。在變元數(shù)目及子句個數(shù)較少時，采用啟發(fā)策略的HAGSAT 算法與SARSAT算法求解速度均比隨機(jī)游走算法Walksat 快。因HAGSAT 算法使用了新的初始解生成方式，通過兩個閾值控制初始解的盲目性，所以求解小規(guī)模SAT 問題時HAGSAT 算法的速度甚至優(yōu)于隨機(jī)生成初始解的SARSAT 算法，但是當(dāng)變元數(shù)目進(jìn)一步增大或者問題逐漸逼近難解區(qū)域時，HAGSAT 算法消耗的時間超過了其他兩種算法，HAGSAT 算法這種初始解的生成方式增加了算法的執(zhí)行時間，且隨著問題進(jìn)入難解區(qū)域，初始解的優(yōu)劣對最終解的影響也變小。因為采用的是和相關(guān)的啟發(fā)式翻轉(zhuǎn)策略，SARSAT 算法相較于Walksat 算法中的以固定概率選擇翻轉(zhuǎn)和HAGSAT 算法變異雜交等策略，執(zhí)行效率更高，變元平均翻轉(zhuǎn)次數(shù)也最少，SARSAT 算法的求解時間在總體上優(yōu)于WalkSAT 算法和HAGSAT 算法。在空間復(fù)雜度方面，Walksat 算法優(yōu)于使用信息素矩陣的HAGSAT 算法和使用變元滿足性矩陣的SARSAT 算法，隨著數(shù)據(jù)存儲技術(shù)及計算機(jī)硬件的發(fā)展，這種以空間換時間和準(zhǔn)確率的取舍完全可以接受。SARSAT 算法中的Metropolis 接受準(zhǔn)則以及改進(jìn)后的輪盤賭策略賦予了SARSAT 算法較強(qiáng)的跳出局部最優(yōu)的能力，對于同一個實例SARSAT 算法的準(zhǔn)確率和無法找到解時的不滿足子句占總子句數(shù)的比例均優(yōu)于其他兩種算法。

表2 實驗結(jié)果對比

為進(jìn)一步驗證SARSAT 算法翻轉(zhuǎn)策略的有效性，對本文SARSAT 算法與隨機(jī)擾動的模擬退火算法SASAT算法進(jìn)行了對比，SASAT 算法的擾動策略為在每個不滿足的子句中隨機(jī)選擇一個變元進(jìn)行翻轉(zhuǎn)，兩種算法的對比效果如圖4 及圖5 所示。

圖4 n=120，d=12，m=960

通過對圖4 分析可知，對于相同變元數(shù)的實例，當(dāng)變元出現(xiàn)次數(shù)較小時，SARSAT 算法與SASAT 算法的求解效率都比較快，溫度還未降至就已找到解，且在降溫過程中，SARSAT 算法可滿足的子句數(shù)目比SASAT 算法多。在圖5 中，曲線SARSAT?代表的是首次降溫未找到解后依據(jù)式（4）升溫再次求解的過程，不難看出，當(dāng)問題進(jìn)入難解區(qū)域，SASAT 算法已無法找到問題的解，而SARSAT 算法通過回溫的過程順利跳出局部最優(yōu)進(jìn)而再一次降溫得到局部最優(yōu)解，驗證了本文溫度衰減函數(shù)的有效性。

圖5 n=120，d=13，m=1 040

5 結(jié) 語

本文提出了一種隨機(jī)規(guī)則(,)?SAT 實例生成模型RRIG（,,）模型，用于生成合法的隨機(jī)規(guī)則CNF 公式，在模擬退火算法求解隨機(jī)規(guī)則可滿足問題上對擾動策略、降溫策略等做出了相應(yīng)改進(jìn)，通過與Walksat 算法和HAGSAT 算法的對比，本文SARSAT 算法在準(zhǔn)確率、變元翻轉(zhuǎn)次數(shù)和執(zhí)行時間上優(yōu)于其他兩種算法，可以有效求解隨機(jī)規(guī)則可滿足問題。當(dāng)問題規(guī)模進(jìn)一步增大時，利用模擬退火算法的可并行性來大幅度提高算法性能，是本文接下來的一個改進(jìn)方向。