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

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

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

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

【部分圖文】：

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

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



本文編號(hào)：3382544