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

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

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

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

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