1、基于矛盾體分離的命題邏輯動態(tài)自動演繹推理求解系統(tǒng)研究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)先地位。針對主流的CDCLSA俅解算法的不足，本文基于徐揚教授提出的基于矛盾體分離的演

2、繹自動推理理論,在構(gòu)建動態(tài)、多元的矛盾體分離的演繹算法核心方面進行了深入的研究,并開發(fā)了獨立的基于矛盾體分離的命題邏輯動態(tài)自動演繹推理求解器和基于矛盾體分離的命題邏輯動態(tài)自動演繹推理核心與CDCLH合的求解器。實現(xiàn)了基于矛盾體分離的命題邏輯動態(tài)自動演繹推理求解基礎(chǔ)算法,并針對CDC印解算法規(guī)避潛在搜索沖突的機制進行了研究，提出了基于矛盾體重構(gòu)的子句學(xué)習(xí)算法。利用CDC印解器沖突分析給出的回溯層與當(dāng)前沖突層之間的決策信息，在子句集中選擇合適子句重新構(gòu)造矛盾體,并生成新的學(xué)習(xí)子句。重構(gòu)過程與CDCL沖突分析過程同步化進行,解決了矛盾體構(gòu)造中的演繹子句不確定性問題、演繹文字不確定性問題和演繹深度不確

3、定性問題。同時，使得CDC印解器每次可以得到兩個學(xué)習(xí)子句,分別代表兩個不同的沖突搜索空間，增強了CDC求解器規(guī)避沖突的能力。針對CDC印解算法單一分支決策機制決策效率不高的問題,提出了基于矛盾體分離的擴充求解算法。該算法以CDC印解器給出的決策文字為起步文字，在剩余未滿足子句中構(gòu)造矛盾體,并生成一組局部可滿足賦值序列,引導(dǎo)求解器優(yōu)先搜索賦值序列所在解空間。通過不斷地構(gòu)造矛盾體并將被滿足的子句成組地從剩余子句中分離,逐漸減小問題規(guī)模。對于可滿足公式,可以通過迭代調(diào)用演繹過程,將局部可滿足解成組地擴充為全局可滿足解;對于不可滿足公式,如果演繹結(jié)果出現(xiàn)空子句,則可以直接判定。局部可滿足賦值序列是矛盾

4、體構(gòu)造得出的結(jié)論,本身反映了潛在搜索沖突,相比每次僅給出一個分支決策文字的決策機制,具有更高的決策效率。研究了CDC啟發(fā)式分支決策策略，在分析了已有啟發(fā)式分支決策算法不能有效選擇下一個分支變元之后,提出了基于活躍度綜合評估的啟發(fā)式分支文字選擇算法。在沖突分析過程中,當(dāng)變元出現(xiàn)在沖突子句和學(xué)習(xí)子句中時,其活躍度增量與變元所在決策層和被賦值時的總沖突次數(shù)均緊密有關(guān)。變元所在決策層體現(xiàn)了局部搜索對應(yīng)子空間的劃分關(guān)系,變元被賦值時的總沖突次數(shù)體現(xiàn)了全局搜索中的沖突變化趨勢。本文算法綜合考慮變元所在決策層和被賦值時的總沖突次數(shù)之間的關(guān)系,給出了決策層和沖突次數(shù)的作用調(diào)節(jié)因子。實驗表明，該算法比經(jīng)典的EV

5、SIDS平估方式更加科學(xué)合理。研究了學(xué)習(xí)子句刪除算法,在分析了已有學(xué)習(xí)子句刪除算法隨意性大且保留的子句利用率不高的問題之后,提出了基于沖突分析頻率的學(xué)習(xí)子句刪除算法和基于動態(tài)趨勢評估的學(xué)習(xí)子句刪除算法?；跊_突分析頻率的學(xué)習(xí)子句刪除算法通過強制刪除被使用次數(shù)較少的子句,保留（或隨機保留）次數(shù)較多的子句,能夠顯著改善求解性能?；趧討B(tài)趨勢評估的演繹結(jié)果刪除算法給出了學(xué)習(xí)子句趨勢強度的量化方法和輕量級的實現(xiàn)算法。通過建立學(xué)習(xí)子句狀態(tài)趨勢轉(zhuǎn)移模型可將隨機的、離散的時序信息轉(zhuǎn)換為連續(xù)的累積趨勢強度。在刪除周期到達時,強制刪除累積趨勢強度小于設(shè)定閾值的學(xué)習(xí)子句。該算法總體性能顯著優(yōu)于學(xué)習(xí)子旬活躍度評估算法，與LBD算法性能基本相當(dāng)。研究了重復(fù)演繹路徑識別問題,在分析了現(xiàn)有重啟算法與搜索過程聯(lián)系不太緊密、觸發(fā)條件隨意性大的問題后,提出了基于向量空間模型的搜索路徑識別算法。該算法借助Luby序列觸發(fā)延時重啟判斷,將當(dāng)前搜索路徑和已搜索路徑轉(zhuǎn)換為向量空間模型,通過計算向量空間相似度