李 壯,劉 磊,張桐搏,周文博,呂 帥

1(吉林大學 計算機科學與技術學院,吉林 長春 1 30012)

2(符號計算與知識工程教育部重點實驗室(吉林大學),吉林 長春 130012)

可滿足性問題(SAT)是公認的第一個NP-完全問題,是人工智能領域最重要的研究方向之一.自人工智能發(fā)展初期就引起了研究者的廣泛關注,當今SAT 求解器已能夠解決很多現(xiàn)實問題.近年來,國內外的學者致力于求解SAT問題的效率和求解能力,提出了多種方法.

1992年,Selman 等人提出的GSAT 算法證明了局部搜索算法可以應用于求解SAT 問題,其強大的求解能力為局部搜索求解SAT 問題奠定了基礎[1].隨著局部搜索方法在該領域的廣泛應用,自2002年SAT 比賽的開展以來,眾多基于局部搜索算法的求解器也相繼問世并展現(xiàn)出了各自強大的求解能力.2005年,Li 等人提出了g2wsat類算法,該算法結合隨機選擇和貪心雙模式,在求解的過程中展現(xiàn)出良好的性能[2].2011年,Li 等人提出了利用變量可滿足歷史記錄的局部搜索求解器SatTime,獲得SAT 2011 隨機組銀獎[3].2016年,KhudaBukhsh 等人提出了SATenstein 求解框架,該框架結合了多個高性能局部搜索求解器,其求解效果勝過多個主流求解器[4].近年來,由Cai 等人提出的基于局部搜索的格局檢測策略成為SAT 比賽中最具影響力的策略之一.2011年,Cai 等人設計的SWCC 算法及相關求解器皆使SAT 求解器的計算能力得到巨大地提升,并取得驚人的成績[5].隨后,Cai 等人于2012年提出的CCASat 獲得SAT 20 12年隨機組金獎[6].2014年,Cai 等人提出的CSCCSat 獲得SAT 201 4年比賽Hard-combinatorial 組銅獎和SAT 2016 比賽Random track 組銀獎[7].同時,基于局部搜索的格局檢測策略用于求解Max-SAT 問題也取得了巨大的成功[8,9],其中,CCLS 在MAX-SAT 2013 非完備性求解器組中獲得4 項金獎.2018年,Cai 等人基于局部搜索算法,在完備算法上設計了ReasonLS 求解器,并在同年SAT 國際比賽中獲得No-Limits track 組金獎[10].以上不難看出,局部搜索算法的廣泛應用和強大的效率已得到不斷突破.

經典的SAT 求解器大多基于DPLL 算法和歸結方法,2003年,Lin 等人提出的擴展規(guī)則方法打破了傳統(tǒng)思維的限制,開辟了SAT 求解的新思路[11].作為歸結方法的互補方法,通過尋找子句的極大項來判斷CNF 公式的可滿足性.他提出的ER 算法得到了國內外的廣泛認可,并為日后的研究打下了堅實的基礎.基于ER 的算法,Lin、Wu、李瑩和張立明等人分別提出了IER[11],RER[12],NER[13],SER[14]等算法,將完備的ER 算法的求解效率提升了幾個數(shù)量級的高度.在擴展規(guī)則的應用方面,2010年,殷明浩等人在可能性擴展規(guī)則的基礎上提出了EPPCCCL理論,可作為可能性知識編譯的目標語言[15].2016年,劉磊等人提出了擴展反駁方法,并在該推理方法與知識編譯之間建立了聯(lián)系[16].2017年,王強等人提出兩種加速#SAT 求解的啟發(fā)式策略,提出了CER_MW 和CER_LC&MW 兩種算法,其求解速度是其他算法的1.4 倍~100 倍,求解能力也在限定時間內可解更多的測試用例[17].2018年,楊洋等人在SWCC 算法的基礎上提出了ERACC 算法,該算法突破了傳統(tǒng)擴展規(guī)則推理對公式規(guī)模的局限,求解效率有了極大提高[18,19].

不僅如此,各種經典的技術也相繼應用于擴展規(guī)則求解的過程中,如啟發(fā)式和并行處理等技術.2009年,李瑩等人針對IER 算法提出了IMOM 和IBOHM 兩種啟發(fā)式,其求解效率較IER 提高了10 倍~200 倍[20].Zhang等人基于其PSER 的半擴展規(guī)則策略提出了分割解空間的PPSER 算法,證明了該算法具有合理的執(zhí)行效率,并優(yōu)于NER、DR、IER 等算法[21].

由以上不難看出,基于擴展規(guī)則的推理方法如今已得到了廣泛的應用.但與局部搜索等推理方法相比,仍然具有很大的提升空間和完善度.本文基于ERACC 算法,從李瑩的IMOM 啟發(fā)式算法和張立明的PPSER 并行算法中得到啟示,提出了PERACC 算法.該算法基于楊洋等人[18,19]的ERACC 算法,調用啟發(fā)式算法CPVI,通過選擇變量并調用PERM 算法,用變量的組合將原解空間分割成不同的子空間,每個子空間通過SIMT 算法選擇初始極大項,隨后進行并行處理.最后實驗證明,該算法較ERACC 算法的求解效率有較大的提高[22].

本文第1 節(jié)介紹了局部搜索和擴展規(guī)則的基礎知識并給出了相關定義.第2 節(jié)提出啟發(fā)式策略CPVI 算法、并行處理策略PERM 算法和變量賦初始值策略SIMT 算法,并將它們有機結合,在ERACC 算法基礎上提出了PERACC 算法.第3 節(jié)進行了實驗的對比,證明了我們的算法在特定的問題上較原算法快出1.6 倍~117 倍不等.

1 基礎知識

1.1 局部搜索

定義1.在一個布爾變量集合V={x1,x2,…,xn}中,每個變量呈正、負兩種文字形式xi和?xi以析取的形式存在于CNF(conjunctive no rmal form)公式的每個子句Ci中,公式中的每個子句之間是合取的.找到一個或多個解釋能使CNF 公式為可滿足的真值指派過程,稱為SAT 求解.

SAT問題的求解是按照某種特定規(guī)則對變量進行選取、賦值和剪枝等過程,找到可滿足的解釋.完備的算法如DPLL,其功能在于不僅可以判斷子句集的可滿足性,而且可以找到可滿足的解.局部搜索作為不完備的方法采取完全不同的方式對SAT 問題進行求解,該方法通過不斷變換部分子句空間所有變量賦值使得可滿足的子句不斷增加,最終達到子句集可滿足的目的.當處理不可滿足的問題時,由于子句集無解而使變量賦值無限地變換下去.因此,局部搜索只能求解可滿足的子句集,且其求解效率遠高于完備的算法,卻無法處理不可滿足的子句集.

1.2 擴展規(guī)則

傳統(tǒng)的歸結方法是通過歸結出空子句來判斷子句集不可滿足;而作為歸結的互補方法,擴展規(guī)則是通過對CNF 公式中的子句能否擴展出所有極大項來判斷其可滿足性.其基本定義如下.

定義2.CNF 公式中的一個子句C,變量l的文字形式不在C中出現(xiàn).有D={C∨l,C∨?l},則稱C到D的過程為擴展規(guī)則,D是子句C關于變量l擴展后的結果.

定義3.若一個子句包含所有變量對應的正文字或負文字之一,則稱該子句為變量集的一個極大項.

初始的擴展規(guī)則推理方法是通過計數(shù)每個子句所能擴展出的極大項個數(shù),利用容斥原理計算所能擴展出極大項總數(shù).如果極大項個數(shù)是2n(n為變量個數(shù)),則CNF 公式是不可滿足的;否則是可滿足的.這種完備算法的缺點在于:其處理的CNF 規(guī)模十分有限,當子句數(shù)超過一定閾值,將會造成內存溢出.李瑩等人提出的NER 算法通過一定次序判斷當前極大項T是否能被CNF 公式中的子句擴展出來:當所有極大項都能被擴展出來時,子句集不可滿足;當存在至少一個極大項不能被擴展,則子句集可滿足.該算法的求解效率遠優(yōu)于ER 和IER 算法,但缺點在于機械地變換極大項,暴力的求解方式滿足了算法的完備性,卻丟失了很多啟發(fā)式信息.楊洋等人提出的ERACC 算法基于局部搜索的格局檢測方法,通過得分機制選取變量,根據(jù)變量的鄰居關系精確格局信息,并通過雙向半擴展規(guī)則來限制變量的選取范圍.該算法在時間復雜度和空間復雜度上都有了很大的改進,并且利用了局部搜索的高效性,使求解可滿足問題的求解效率達到了質的飛躍.

1.3 基于精確格局檢測的擴展規(guī)則算法

基于局部搜索的擴展規(guī)則推理方法的本質在于:以尋找極大項空間不可擴展的極大項為目標,利用貪心策略限定極大項空間,以變量的鄰居變量設定格局信息,從而減少了冗余搜索步驟,犧牲了算法完備性,從而達到了高效求解的效果.

ERACC 算法的精髓在于對極大項中反轉變量的選擇,通過最大左度和最小右度的概念,限定兩集合中的變量.如果集合為空,則退一步選擇得分高的變量取反.精確了變量的選擇直接控制了極大項的變換,使得推理過程更加精確(算法的具體流程見文獻[18,19]).但是算法仍存在以下不足:初始極大項的選擇并沒有明確的啟發(fā)式;串行的處理也使得ERACC 算法無法發(fā)揮出極致的效果;忽略了預處理技術,使子句集沒有化簡的過程.下文將針對以上問題提出PERACC 算法,使求解的性能發(fā)揮到極致.

2 PERACC 算法

傳統(tǒng)的基于擴展規(guī)則的并行推理方法將子句集的極大項空間分解為若干個子空間,并對其進行逐一求解.這種并行方式并未加入啟發(fā)式信息,使得分割空間無層次.即使分割的子空間彼此毫無關聯(lián),但整體推理的空間復雜度并無降低.

本文提出的并行處理是一種結合了對解空間化簡的預處理方法.在選擇特定的變量之后,對原子句集進行化簡,化簡后的子句集與原子句集是邏輯等價的,這也極大地降低了對整個子句集求解的空間需求;并在ERACC 算法中加入了對初始值的賦值限制,改變了ERACC 對初始值賦為1 的單調做法,使求解器整體求解能力得到了較大地提升.

2.1 CPVI算法

我們通過選取變量的啟發(fā)式算法,對出現(xiàn)在每個子句中的文字賦予權值.從文字出現(xiàn)在各個子句中的累計次數(shù)計算出得分最高的變量.首先,遍歷原始子句集獲得所有文字的數(shù)組,從數(shù)組中選取最大數(shù)對應的變量.如果同等數(shù)量的變量有若干個,那么從中隨機選取需求個數(shù)作為初始變量,變量個數(shù)由所劃分的解空間參數(shù)決定.變量選取算法如下,其中,vs=(var,score)表示變量及對應的得分,其中,var表示變量,score表示變量的得分.

算法1.計算選取的變量CPVI(computing the picking variables initially).

算法1 采取一種遍歷求和排序的方式來計算各個變量的得分集合,從而選取權重最高的變量作為化簡子句集的初始變量.算法第2 行表示程序遍歷了整個子句集F并統(tǒng)計了所有變量集合;第3 行~第5 行對所有的變量及其得分清零;第6 行~第10 行分別描述了對所有變量和每個變量在各個子句中的雙重循環(huán),得到變量集合的得分數(shù)組vsi.score,并對其進行排序;第12 行~第24 行表示當出現(xiàn)得分均等的若干個變量時,從中隨機選取所需個數(shù)變量;最后輸出所選擇的變量.

變量得分的計算,令F為CNF 公式,Ci={l1,…,lk}為子句集中任意子句(i∈(0,m]),m為子句數(shù),Wi為子句相關聯(lián)文字的權值.則變量v基于F的得分函數(shù)為

在以上公式中,δ為二元謂詞特征函數(shù),代表多值邏輯的取值.令l表示在子句Ci中變量v所對應文字的取值.δ的具體定義如下:

以上公式給出了變量得分的計算方式,基本思想為:根據(jù)文字出現(xiàn)在子句中的形式取相應的值.正文字取1(變量所對應文字為l時取1),負文字取?1(變量所對應文字為?l時取?1).通過求和計算累計變量的得分,根據(jù)得分將變量排序,進而選取所需變量.該方法的時間復雜度是線性的,因此,該預處理方法所需時間在求解的過程中所占比重是極小的.

例1:令CNF 公式F={A∨C∨?D,?B∨?G∨H,?A∨E∨G∨?H,C∨E∨H,?D∨G∨?H},在該測試用例中,每個變量相對應的文字權值Wi為1,則變量的得分如下:

?Score(A)=|1×1|+|0×1|+|(?1)×1|+|0×1|+|0×1|=2;

?Score(B)=|0×1|+|(?1)×1|+|0×1|+|0×1|+|0×1|=1;

?Score(C)=|1×1|+|0×1|+|0×1|+|1×1|+|1×1|=2;

?Score(D)=|(?1)×1|+|0×1|+|0×1|+|0×1|+|(?1)×1|=2;

?Score(E)=|0×1|+|0×1|+|1×1|+|1×1|+|0×1|=2;

?Score(G)=|0×1|+|(?1)×1|+|1×1|+|0×1|+|1×1|=3;

?Score(H)=|0×1|+|1×1|+|(?1)×1|+|1×1|+|(?1)×1|=4.

由例1 可以看出:給定CNF 公式F中,所有文字的權值為1,在對變量選擇的過程中掃描一次即可得知變量的得分.在選取變量階段,我們選取得分最高的變量(例1 中的變量F).在硬件條件允許的條件下,我們可以選擇多個變量.如果我們選擇3 個變量,那么會根據(jù)得分依次選擇變量G和變量H,而第3 個變量的選取則在得分相等的變量{A,C,D,E}中隨機選取一個.

我們的目的在于對原解空間進行最大程度化簡,因此選擇了得分最高的變量作為初始變量.最理想的情況是存在某個變量出現(xiàn)在每個子句中,這樣可以最大程度地降低子句集規(guī)模,得到的問題規(guī)模最小.即:在預處理階段約簡了原子句集,其約簡后的結果與原子句集是邏輯等價的.

定理1.預處理階段,化簡后的子句集與原子句集是邏輯等價的.

證明:固定了極大項中的文字之后,原子句集中帶有互補文字的子句可直接忽略,因為這樣的子句是無法擴展出當前極大項的;而帶有相同的文字可以忽略不計,只看除了該文字剩余部分的子句.這樣,剩余變量的模型組成了新的極大項,與化簡后的子句集相對應,即,同原極大項和原子句集是邏輯等價的.

例2:令CNF 公式F={A∨B∨C∨D,?A∨B∨?C∨E,?A∨?B∨?G,?A∨B∨?D∨?E,B∨C∨?D∨G},按照算法1 選取變量,我們應選擇的變量為A和B.如果我們單看其中的一個子空間,變量取值為?A和B,那么化簡的原子句集為F′={?C∨E,?D∨?E,C∨?D∨G},新的解空間是由變量{C,D,E,G}所組成的極大項空間.

由例2 可以看出:在保證了邏輯等價的前提下,化簡后的子句集規(guī)模已經遠遠地小于原子句集的規(guī)模.實驗證明:不論在時間還是空間上,都有了很大的提高.

2.2 PERM算法

選擇變量的目的在于化簡解空間,而并行的目的是基于化簡基礎上能夠全面地對子句集求解.由于選擇的變量組合的不同,對子句集化簡的程度也不同.基于該問題,我們會選擇幾種化簡后,求解效率最高的那個子空間作為判斷的標準.我們提出了PERM 算法來解決這一問題.

PERM 算法過程如下:

算法2.并行擴展的推理方法PERM(parallel extensionrulereasoning method).

算法2 給出在極大項子空間中分割原始極大項解空間的并行算法PERM.首先輸入原CNF 公式和已選取的變量,預處理程序通過二進制方法將變量的2α種析取將子句集的極大項空間分解為threadnum個獨立的子空間,并記錄每個子空間的返回結果,然后對每個極大項子空間并行地調用ERACC 算法進行極大項的判定.當某一個極大項子空間EndThread(i)中返回的結果為SAT,即該子空間中存在某個極大項在規(guī)定時間內不能被擴展出來的子句,則子句集是可滿足的.將該結果返回至主程序,推理過程結束.

2.3 SIMT算法

由第1 節(jié)我們可知,NER 和ERACC 兩種算法都是以尋找子句集擴展不出的極大項為目標來進行推理的,所以我們采取的途徑是變換和調整極大項的模型.在ERACC 中已詳細地說明了如何去變換調整極大項,忽略了對初始極大項的重視,采用了單純的對初始極大項中沒個變量賦值為1.初始的極大項中,變量的賦值在整個推理過程中占據(jù)重要的位置.如果沒有針對性地給初始極大項賦值,則會在求解過程中走很大的彎路,間接地增加了冗余的推理過程.

為了使推理過程更直接、高效,我們提出了SIMT 算法,有針對性地解決對初始極大項中變量賦初始值的選擇.由于極大項中的每個變量可以賦值為正和負兩種文字形式,而每種文字形式的賦值概率為50%,我們提出的算法是每個變量根據(jù)原子句集中文字出現(xiàn)的比率來確定初始極大項中變量的取值概率.實驗結果表明,我們的策略是有效的.

SIMT 算法過程如下.

算法3.選擇初始極大項方法SIMT(selection of initial maximum term).

算法3 中,i代表初始的極大項,通過遍歷子句集得到F中的變量數(shù)n,再根據(jù)每個變量所對應的文字統(tǒng)計其正、負文字出現(xiàn)的個數(shù),n(li)表示變量對應的文字總個數(shù).第5 行~第10 行是一個循環(huán).根據(jù)正負文字出現(xiàn)的個數(shù)與變量對應的文字總個數(shù),計算對應極大項中該變量應該賦值的概率,即有指向性地調整了變量賦值的概率.逐一對變量賦值之后,當賦值變量的個數(shù)完成了第n個后,說明初始極大項已經產生,算法結束.有針對性地選擇初始極大項,會使下一步的推理更加精準,提高了推理效率.

2.4 PERACC算法

結合了以上算法,基于ERACC 算法,我們提出了基于精確格局檢測的并行擴展規(guī)則算法,算法過程如下.

算法 4.基于精確格局檢測的并行擴展規(guī)則算法 PERACC(parallel e xtension rule ba sed on accurate configuration checking).

算法PERACC 的執(zhí)行過程大致如下:第1 行~第4 行通過調用CPVI 算法選擇初始變量,通過變量選擇的數(shù)量,得到分解解空間的數(shù)量,并對各個解空間進行化簡,然后對各個解空間進行求解;第5 行調用算法SIMT 來計算各個解空間的初始極大項;第6 行~第18 行是調用ERACC 算法對每個解空間的求解,其詳細過程可參考文獻[18,19];第19 行~第22 行是一個死循環(huán),當各個解空間中,某一個解空間找到了擴展不出的極大項,那么跳出該循環(huán).

3 實驗結果與分析

本節(jié)對算法PERACC 算法進行實現(xiàn),并且將其與擴展規(guī)則領域主流的求解器SER,ERACC 以及國際主流的SWCC 求解器進行了對比.實驗結果證明了PERACC 算法不僅勝過了傳統(tǒng)的擴展規(guī)則方法,而且大大地縮短了與國際主流求解器的距離.

實驗環(huán)境:Arch Linux 16.04 操作系統(tǒng),12 核CPU,內存8GB.對于每一問題測試用例,均將算法執(zhí)行50 次,最終取平均值作為結果.由于本文提出的算法屬于不完備算法,所以解決的問題都是可滿足性的問題.測試用例來源于https://www.cs.ubc.ca/~hoos/SATLIB/index-ubc.html,SWCC 的源代碼來源于他的個人主頁https://lcs.ios.ac.cn/~caisw/SAT.hrml,g2wsat 的源碼來源于國際SAT 比賽官網https://www.satcompetition.org/.

首先,我們采用處于相變區(qū)域的Uniform Random-3-SAT 問題,不論是對于系統(tǒng)的SAT 求解器或者是隨機的局部搜索算法都是很難的問題.在以往的擴展規(guī)則算法測試中,由于受到求解規(guī)模的限制,只能求解一些小規(guī)模的測試用例.而在文獻[18]中,ERACC 求解器已經展現(xiàn)出了其強大的求解能力,可以求解先前求解器無法求解的測試用例.所以在我們的測試中,首先選擇了ERACC 所能求解的規(guī)模最大的測試用例.我們選擇變量250、子句數(shù)為1 065 的規(guī)模最大的問題.由于測試用例規(guī)模較小,所以該組實驗我們將運行30 秒未結束的測試用例定為Time o ut.由表1 不難看出:傳統(tǒng)的SER 算法已經無法解決規(guī)模龐大的測試用例,而ERACC 算法和PERACC 算法顯然已經突破了傳統(tǒng)算法的限制,發(fā)揮了極大的潛力.在這組測試用例中,PERACC 算法的求解效率并沒有ERACC 好.原因在于預處理的過程需要少量的時間,而ERACC 算法沒有預處理的過程.因此,在處理規(guī)模相對較小的問題時,并不能凸顯出PERACC 算法的優(yōu)勢,即先前所能求解的測試用例已經無法凸顯我們算法的優(yōu)勢.

在表1 實驗中,我們默認PERACC 算法在預處理過程中選擇4 個變量,并不確定選擇4 個變量就是最優(yōu)的選擇.

Table 1 Experiment results on uniform random-3-SAT instances uf250(CPU time/s)表1 隨機3-SAT 測試用例uf250 實驗結果(CPU time/s)

帶著以上兩個問題,我們做出了以下實驗.

表2 選擇了圖著色問題中一些較難的大型Random-3-SAT 測試用例.圖著色類測試用例包含200 個頂點和479 條邊,將GCP 測試用例編譯為SAT 問題后,成為600 個變量和2 237 條子句.我們選擇以下測試用例的原因在于它們的復雜性更高,求解時間較長,所以該組實驗我們將運行500 秒未結束的測試用例定為Time o ut.這些測試用例與表1 相比規(guī)模更大,更能突出PERACC 的性能,符合我們對上述問題的實驗論證.

為了測試SIMT 算法的有效性,我們在表2 中加入了基于ERACC 算法,結合了SIMT 的算法ERACC+.通過ERACC 和ERACC+兩組實驗我們不難看出:在21 個測試用例中,ERACC+組有18 個測試用例優(yōu)于ERACC 組,其中效果最好的一組對比數(shù)據(jù)提高了82 倍.而平均時間也提高了近3.5 倍.由此我們得知,加入SIMT 算法比單純的將初值賦為1 效果要好很多.

PERACC(i)代表啟發(fā)式過程中選擇i個變量.從ERACC(2)和PERACC(4)兩組數(shù)據(jù)可以看出:針對比較復雜的問題,PERACC(4)算法已經比較明顯地凸顯出了其性能的優(yōu)勢.從這兩組數(shù)據(jù)也不難看出:選擇變量的數(shù)量越多,其求解效率越高.結合表 1 分析,雖然 PERACC 算法在啟發(fā)式階段花掉了少許時間,但是整體來看,PERACC(4)比ERACC 效率提高了4 倍~25 倍不等,這也符合了磨刀不誤砍柴工的道理.

我們將繼續(xù)延伸我們的思路,加入了當前國際著名的局部搜索求解器SWCC 進行對比.從數(shù)據(jù)上不難看出,PERACC 比ERACC 的效率提升了1.6 倍~117 倍不等.雖然PERACC 的求解效率并沒有超過SWCC 求解器,但是相對于當前擴展規(guī)則領域最高效的ERACC 而言,PERACC 已大大地縮短了與SWCC 的距離.

Table 2 Experiment results on graph Colouring instances flat200-479(CPU time/s)表2 圖著色測試用例flat200-479 實驗結果(CPU time/s)

我們將實驗的證明繼續(xù)擴大化,選擇了AIM 類問題.該類問題結構性很強,變量個數(shù)以及正負文字比例存在一定規(guī)律,解的個數(shù)只有一個,求解難度較高.1_6 和2_0 代表子句與變量的比率,測試用例的變量為100 個.所以,我們將運行1 200s 未結束的測試用例定為Time out.

從表3 可以看出:在前4 個測試用例中,并沒有拉開PERACC 和ERACC 的差距,g2wsat 在規(guī)定時間內未找到解,SWCC 的數(shù)據(jù)兩極分化比較嚴重;后4 個測試用例中,仍然體現(xiàn)出了PERACC 的高效性,并且大大地拉開了與g2wsat 的求解差距.雖然在多半用例,我們仍然無法超越SWCC.我們分析:對于結構性較強的AIM 類問題,局部搜索求解結構SAT 問題并不占優(yōu)勢.對于少數(shù)測試結果,PERACC 算法超過了SWCC 求解器,這在擴展規(guī)則領域是史無前例的,從中也看出擴展規(guī)則方法在求解SAT 問題上的巨大潛力.

Table 3 Experiment results on AIM instances(CPU time/s)表3 AIM 類問題測試實驗結果(CPU time/s)

以上實驗結果表明:PERACC 算法在求解復雜性較高、規(guī)模較大的測試用例時,更能凸顯PERACC 的高效性能,同時縮短了與SWCC 求解器的差距,得到了比較良好的效果.

基于擴展規(guī)則的推理方式本身是與歸結方法截然相反的求解過程,它是從問題的解空間入手來尋求答案.基于擴展規(guī)則的ERACC 算法相比于成熟的局部搜索求解器確有不足,因此,我們在原有基礎上做出了一系列改進,進一步研究擴展規(guī)則的適用性.我們相信,雖然擴展規(guī)則推理方法還處于初級階段,但與不完備的局部搜索方法相結合,必將發(fā)揮出它更大的潛力.

4 總結與展望

本文基于ERACC 算法提出了并行框架,提出了PERACC 算法,我們先后提出了預處理、化簡解空間等技術,并行處理各個子空間.通過實驗顯示:該算法較原算法的求解效率有較大的提高,并不斷縮短了與國際著名算法SWCC 的差距.

PERACC 算法在原有算法的基礎上進一步大膽地嘗試了擴展規(guī)則方法領域中不完備推理的發(fā)展.下一步,我們決定將DPLL 算法中的單文子傳播機制加入其中,從而進一步完善預處理的效果.另一方面,我們將知識約簡方法應用于并行前和并行后,通過對復雜問題約簡手段的不斷提高,才能讓我們去不斷地求解復雜性更高、規(guī)模更大的測試用例.具體的方法還需要進一步進行理論分析和大量的實驗來證明想法的可行性,合理與PERACC 結合,使算法的求解能力得到最大化的提升.