SAT問題是一類特殊的約束滿足問題（CSP）,也是信息科學(xué)領(lǐng)域一個著名的決策問題。在理論應(yīng)用領(lǐng)域,許多經(jīng)典的可計算問題,諸如覆蓋問題、打包問題、路由選擇問題、排序問題等都可以轉(zhuǎn)換為SAT問題求解;在實際應(yīng)用領(lǐng)域,諸如模型檢驗、軟件形式化驗證、硬件形式化驗證、智能規(guī)劃、知識編譯以及其他組合優(yōu)化領(lǐng)域的問題也可以轉(zhuǎn)換為SAT問題求解。因此,研究高效的SAT求解算法有著重要的理論價值和應(yīng)用價值。由于SAT問題是NP完全的,迄今為止沒有發(fā)現(xiàn)哪一個SAT求解器長期處于領(lǐng)先地位。針對主流的CDCL SAT求解算法的不足,本文基于徐揚教授提出的基于矛盾體分離的演繹自動推理理論,在構(gòu)建動態(tài)、多元的矛盾體分離的演繹算法核心方面進(jìn)行了深入的研究,并開發(fā)了獨立的基于矛盾體分離的命題邏輯動態(tài)自動演繹推理求解器和基于矛盾體分離的命題邏輯動態(tài)自動演繹推理核心與CDCL融合的求解器。實現(xiàn)了基于矛盾體分離的命題邏輯動態(tài)自動演繹推理求解基礎(chǔ)算法,并針對CDCL求解算法規(guī)避潛在搜索沖突的機制進(jìn)行了研究,提出了基于矛盾體重構(gòu)的子句學(xué)習(xí)算法。利用CDCL求解器沖突分析給出的回溯層與當(dāng)前沖突層之間的決策信息,在子句集中選擇合適子... 

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

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

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

【部分圖文】：

8bits_10.dimacs運行中決策層及沖突次數(shù)變化情況

【參考文獻(xiàn)】：
期刊論文
[1]求解SAT問題的量子免疫克隆算法[J]. 李陽陽,焦李成.  計算機學(xué)報. 2007(02)



本文編號：3382544