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

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

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

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

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