動(dòng)靜結(jié)合排序決策的可滿足性問題解決器.pdf

1、可滿足性問題是被廣泛研究的基本NP問題之一。電子設(shè)計(jì)自動(dòng)化、人工智能、計(jì)算機(jī)科學(xué)、運(yùn)籌管理等方面的許多問題都可以簡(jiǎn)化成可滿足性問題，可滿足性問題的算法上的改進(jìn)也極大地促進(jìn)這些相關(guān)領(lǐng)域的發(fā)展。 本文在研究、探討可滿足性問題算法及其實(shí)現(xiàn)技術(shù)的基礎(chǔ)上，選擇目前的主流算法——基于DPLL完全算法，針對(duì)其中很重要的組成部分——搜索決策方面作了深入的研究，提出了一種新的、高效的搜索決策策略，采用動(dòng)靜態(tài)排序相結(jié)合的策略可滿足性問題解決器。

2、 具體貢獻(xiàn)是： 1)研究了靜態(tài)排序?qū)λ惴ǖ呢暙I(xiàn)，針對(duì)靜態(tài)排序的特點(diǎn)，采用了一種有效地體現(xiàn)實(shí)際問題特征的靜態(tài)分析方法，根據(jù)變量正反文字出現(xiàn)次數(shù)的乘積，進(jìn)行初始排序，優(yōu)先考慮正反文字出現(xiàn)次數(shù)較多變量的賦值； 2)權(quán)衡比較了多種動(dòng)態(tài)排序策略，采用一種既能及時(shí)反映算法過程中問題特征，動(dòng)態(tài)更新排序，又不需耗費(fèi)大量計(jì)算機(jī)資源的策略，給沖突子句中的變量活躍性因子增加一個(gè)隨時(shí)間增大的變量，把變量順序提到比它活躍性因子小的前面，體現(xiàn)了