基于DPLL的SAT算法的研究及應(yīng)用.pdf

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

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

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

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