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

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

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