CDCL SAT求解器中的分支變量啟發(fā)式算法研究.pdf

1、命題邏輯公式的可滿足性問題（即SAT問題）是人工智能和計算機科學領(lǐng)域的核心問題之一。1971年Stephen.Cook從算法時間復雜度的角度證明了SAT問題是NP完全問題，而NP完全問題在七大數(shù)學難題中排在首位，可見SAT問題是一類非常困難的問題。由于SAT問題在約束可滿足問題、數(shù)理邏輯、自動推理、軟件及硬件驗證等領(lǐng)域具有廣泛的應(yīng)用，因此研究SAT問題的求解具有重要的理論價值和應(yīng)用前景。
　　目前求解SAT問題的算法大致可歸為兩類

2、:一類是完備的求解算法;一類是不完備的求解算法?；贒PLL算法的CDCL(Conflict Derive Clause Learning)算法是目前比較流行的完備算法，由該算法設(shè)計的求解器(CDCLSAT求解器)的求解過程主要分為三大階段，分別是分支變量選擇階段、布爾約束傳播階段和沖突分析及回溯階段。其中，變量選擇階段的分支變量啟發(fā)式算法可歸結(jié)為兩類:第一類是沒有與沖突分析過程相結(jié)合的啟發(fā)式算法，比如JW算法(Jeroslow-Wan

3、g)、DLIS(Dynamic LargerIndependent Sum)算法等;第二類是與沖突分析過程相結(jié)合的啟發(fā)式算法，比如VSIDS(Variable State Independent Decaying Sum)算法、CHB(Conflict History-based BranchingHeuristic)算法、LRB（Learning Rate Branching）算法等。由于第一類分支變量啟發(fā)式算法計算代價大，第二類分支

4、變量啟發(fā)式算法未能很好地利用子句固有的信息以及未體現(xiàn)出學習子句中變量的不同。故為了盡可能減少這些算法的不足以及選出更好的分支變量，本文以經(jīng)典的VSIDS算法為基本框架設(shè)計了基于獎勵的分支變量啟發(fā)式算法，并用該算法代替MiniSat求解器中的分支變量啟發(fā)式算法，得到新的求解器一Modified-MiniSat求解器。
　　本文就新算法的提出主要做了以下四方面的工作:
　　1.對于一般的SAT問題，短予句較長子句更難被滿足，依據(jù)

5、子句的長度賦予每個子句權(quán)重，進而給出變量在子旬以及子句集中的權(quán)重的定義。并用變量在子句集中的權(quán)重刻畫變量的活性，從而盡可能準確地反映變量在子句集中的活躍度。
　　2.設(shè)計了與決策層有關(guān)的獎勵函數(shù)。在問題求解過程中，當學習子句添加到子句集時，根據(jù)學習子句中變量所在決策層的不同，獎勵變量，以便增大學習子句中的變量活性。
　　3.基于上述兩方面的工作，給出了基于獎勵的分支變量啟發(fā)式算法，并用該算法代替MiniSat求解器中的分支變