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

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

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

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