基于DPLL的SAT算法的研究及應用.pdf

1、命題邏輯公式的可滿足性問題（SAT）是數(shù)理邏輯、計算機科學、集成電路設計與驗證和人工智能等領域中的核心問題，并且是第一個被證明出來的NP問題。SAT問題在計算復雜性理論中具有非常重要的地位，設計并實現(xiàn)解決該類問題的高效算法意義重大。但目前不存在一種求解算法在最壞情況下的時間復雜度是多項式級別，其求解速度仍是制約SAT算法發(fā)展的一大難題。因此，世界各國的學者都在努力研究新的求解算法，以尋求出一種高效的求解算法。
　　SAT算法分為完

2、備算法和局部搜索算法這兩類。其中，完備算法能給出命題邏輯公式的解或證明公式是不可滿足的，但是效率較低；而局部搜索算法求解速度相對較快，但是不一定能夠找到對應SAT問題的解。本文在對比分析這兩類算法的基礎上，對DPLL算法進行了改進，并通過實驗證明了改進后算法的優(yōu)越性。
　　基于上述思想，本文的研究工作主要包括：
　?。?）深入分析了基于DPLL的完備性SAT算法的實現(xiàn)原理，給出了算法思想和詳細的實現(xiàn)過程，并對該算法中所使用到

3、的數(shù)據(jù)結構和一些關鍵技術（加速搜索的啟發(fā)式策略、子句刪除機制、隨機重啟動機制）給予總結和分析。
　　（2）結合完備算法能夠進行完備求解和局部搜索算法能夠以較快速度進行求解的優(yōu)點，在DPLL這一基本算法框架之上提出了一種混合的SAT求解器，將局部搜索算法WALKSAT作為一個必要步驟融入到DPLL算法的求解過程中。一方面，WALKSAT算法得出的近似解可以指導DPLL對決策變量進行賦值，從而減小對決策變量賦值的隨機性和盲目性；另一方

4、面，每當頂層變量的賦值確定后，都引入WALKSAT對算法進行加速，從而提高求解效率。
　　（3）改進DPLL算法的整體框架和實現(xiàn)，給出了改進后算法的框架和實現(xiàn)步驟，并選取一些難的隨機SAT實例對改進前后的算法進行了測試，實驗結果表明，改進后的算法對于求解可滿足的隨機3-SAT實例效果顯著。
　?。?）將改進后的算法應用到圖論中的實際問題--四色問題。問題通過編碼轉換為CNF公式的形式后，輸入到改進后的DPLL求解器中進行求解