SAT問題是計算機科學(xué)理論和人工智能中的著名問題。NP完全問題（NP-complete,NPC）排在千禧年七大難數(shù)學(xué)問題之首,許多NP完全問題都可以在多項式時間內(nèi)轉(zhuǎn)換為SAT問題進行求解。SAT問題廣泛應(yīng)用于數(shù)學(xué)定理證明、計算機軟件與理論、工程技術(shù)、軟件驗證以及邏輯電路等價性驗證等多個領(lǐng)域。因而SAT問題一直是國內(nèi)外學(xué)者關(guān)注的熱點問題,設(shè)計并實現(xiàn)求解SAT問題的高效算法具有重要的鉆研意義和應(yīng)用遠景。DPLL求解器開創(chuàng)了求解SAT問題的先河,但其算法自身的回溯機制對大規(guī)模問題的求解有一定程度的制約性。為了提升DPLL算法的求解效率,國內(nèi)外學(xué)者們進行了大量的研究,添加了一些關(guān)鍵技術(shù)。例如啟發(fā)式分支策略、基于沖突分析和子句學(xué)習(xí)、非時序回溯、學(xué)習(xí)子句的刪除和周期性重啟等,形成了當(dāng)前最流行的CDCL（Conflict-Driven-Clause-Learning,CDCL）求解器�；贑DCL算法結(jié)構(gòu),本文做了以下研究工作:一、借鑒VSIDS策略及其延伸策略的思想,研究變量的決策層和變量參與沖突的沖突次數(shù)對分支決策階段的影響,在此基礎(chǔ)上提出一種改進的啟發(fā)式分支策略——基于變量決策層的啟發(fā)式變量選... 

【文章來源】：西南交通大學(xué)四川省211工程院校教育部直屬院校

【文章頁數(shù)】：59 頁

【學(xué)位級別】：碩士

【部分圖文】：

不同刪除比例的求解性能對比

圖 5-1 不同求解器對 2017 年測試?yán)那蠼庑阅軐Ρ?2.2 2018 年 SAT 競賽結(jié)果表 5-3 列出了四個求解器對 2018 年 SAT 國際競賽問題中 Main Track 組中 400 個

不同求解器對2018年測試?yán)那蠼庑阅軐Ρ?br>
【參考文獻】：
期刊論文
[1]基于演繹長度的學(xué)習(xí)子句刪除策略[J]. 常文靜,徐揚,吳貫鋒.  計算機工程與應(yīng)用. 2018(16)
[2]一種求解SAT問題的人工蜂群算法[J]. 郭瑩,張長勝,張斌.  東北大學(xué)學(xué)報(自然科學(xué)版). 2014(01)
[3]著色歸結(jié)、PI著色碰撞及其完備性[J]. 陸汝占,林凱,孫永強.  計算機學(xué)報. 1987(12)

博士論文
[1]基于矛盾體分離的命題邏輯動態(tài)自動演繹推理求解系統(tǒng)研究[D]. 陳青山.西南交通大學(xué) 2018

碩士論文
[1]基于CDCL結(jié)構(gòu)的SAT問題優(yōu)化策略的研究[D]. 杜忠和.西南交通大學(xué) 2018
[2]布爾可滿足關(guān)鍵問題研究[D]. 王藝源.吉林大學(xué) 2014
[3]基于DPLL的SAT算法的研究及應(yīng)用[D]. 陳穩(wěn).電子科技大學(xué) 2011



本文編號：3616929