一類SAT Benchmark的算法研究及其應(yīng)用.pdf

1、SAT問題是計算機科學(xué)和人工智能研究的領(lǐng)域的著名問題。在實際生活中有許多問題可以轉(zhuǎn)化為SAT問題,并通過SAT算法得到很好的解決。故而研究高效的SAT算法是當前重要且具有實際應(yīng)用價值的研究主題。SAT問題來源非常廣泛,由此構(gòu)成了不同類型的SAT Benchmark。然而同一種SAT算法在不同類型的Benchmark上其效率存在較大的差異,人們普遍認為出現(xiàn)這種現(xiàn)象主要由于內(nèi)部結(jié)構(gòu)上的差異造成?；谶@一考慮,SATzilla將眾多的SAT算

2、法整合起來,在求解過程中為不同的類型的Benchmark選擇不同的算法,并且取得了成功。從中也可以看出為不同類型的Benchmark設(shè)計不同的算法將是解決SAT問題的一個重要的發(fā)展趨勢之一。本文主要針對結(jié)構(gòu)類似于Model RB模型生成的一類SAT Benchmark設(shè)計了一種高效的算法,并將該算法成功地用于解決圖著色問題。
　　 SAT算法主要分為完備算法和不完備算法兩大類。完備算法與不完備性算法不同,它不僅可以保證為可滿足S

3、AT問題的給出它的一個模型,同時可以證明不可滿足SAT問題的不可滿足性,故而大多數(shù)SAT算法都是完備性算法。在當前的完備性算法中,大多數(shù)都是基于DPLL算法框架設(shè)計高效的SAT算法,如zChaff、Rsat等。本文也是基于DPLL框架來設(shè)計算法。
　　 本文在設(shè)計算法時,首先對該類SAT Benchmark的結(jié)構(gòu)進行了分析,將變量進行分組處理,在此基礎(chǔ)上將其等價性地轉(zhuǎn)化為分別從各變量分組中選取滿足條件的變量的問題,并以DPLL運

4、算框架設(shè)計出wRBsat算法。算法使用了向量數(shù)組來存儲數(shù)據(jù),實現(xiàn)算法對數(shù)據(jù)的高效訪問與操作。在設(shè)計分支決策時,將決策過程分為兩步:首先,分組的選取,并以此實現(xiàn)搜索樹的構(gòu)建;其次,變量的選取,在該步驟中實現(xiàn)搜索路徑的選取。該方式使得算法能夠更好地選取決策變量,控制搜索樹的大小,從而提高算法的效率。算法的運算框架使得在算法中的回溯層次相對較少,歷史數(shù)據(jù)的存儲也非常方便,從而使得整個沖突分析和回溯的效率都相對較高。
　　 本文對算法進