【摘要】： 可滿足問題(SAT)是第一個被證明的NP-完全問題[Cook71],是Johnson等人在上千個NP問題中總結(jié)出的六個最具代表性的問題之一,它在計算復(fù)雜性理論中具有極其重要的地位,其理論研究三十多年來從未停止過�？蓾M足問題在人工智能、集成電路設(shè)計、規(guī)劃、圖論等重要領(lǐng)域中都有所應(yīng)用(存在直接的可滿足問題或者可以轉(zhuǎn)化為可滿足實例高效求解的問題),同時,由于該問題描述和數(shù)據(jù)表示非常簡單,因此是很好的算法試驗田,從這里發(fā)展出的算法技術(shù)可以快速的應(yīng)用于其他問題上。因此,高效實用的可滿足算法設(shè)計與分析同樣是多年來的研究熱點。 本文的研究工作是針對可滿足問題的預(yù)處理問題展開的,預(yù)處理是對求解問題進行簡化,以實現(xiàn)幫助問題求解的目的。本文首先分析和介紹了可滿足問題算法一路走來過程中衍生出的幾種經(jīng)典算法,以及預(yù)處理方面的幾種常見算法。針對其中的預(yù)處理工作提出了改進的方法,并實現(xiàn)提高整個問題解決效率的目的。 本文主要的價值之處在于：(1)使用二元關(guān)系矩陣來構(gòu)建邏輯蘊含圖,使用映射關(guān)系輔助進行邏輯蘊含關(guān)系的推導(dǎo)；(2)結(jié)合高級邏輯推導(dǎo)技術(shù)以及邏輯蘊含圖的對稱性推進簡化過程。從實驗分析表明,這些措施能夠有效地提高解決可滿足問題的效率,并在一些情況下能夠獨立發(fā)現(xiàn)問題是否可滿足。
【學(xué)位授予單位】：復(fù)旦大學(xué)
【學(xué)位級別】：碩士
【學(xué)位授予年份】：2009
【分類號】：TP332

【相似文獻】

相關(guān)期刊論文 前10條

1 黃慶華;;Oracle專題——外連接過濾[J];數(shù)字技術(shù)與應(yīng)用;2011年08期

2 殷明浩;周俊萍;孫吉貴;谷文祥;;求解QBF問題的啟發(fā)式調(diào)查傳播算法[J];軟件學(xué)報;2011年07期

3 邢賾聰;;SQL案例專題-缺勤者[J];數(shù)字技術(shù)與應(yīng)用;2011年08期

4 楊振宇;;巧用SQL的查詢技術(shù)[J];軟件;2011年04期

5 崔寶合;王秋華;;信息管理與信息系統(tǒng)在醫(yī)院的應(yīng)用[J];企業(yè)導(dǎo)報;2011年12期

6 宋勃升;殷志祥;甄誠;華程;;DNA自組裝的可滿足性問題模型[J];小型微型計算機系統(tǒng);2011年09期

7 張桂燕;;基于數(shù)據(jù)庫的語句優(yōu)化經(jīng)驗之談[J];電腦知識與技術(shù);2011年17期

8 韓競鋒;;數(shù)據(jù)庫應(yīng)用系統(tǒng)性能優(yōu)化研究與實踐[J];信息安全與技術(shù);2011年06期

9 梁鳳萍;;淺析數(shù)據(jù)庫查詢優(yōu)化[J];大眾標準化;2011年S1期

10 盤青梅;;大型表SQL查詢的優(yōu)化與用戶編寫策略[J];太原城市職業(yè)技術(shù)學(xué)院學(xué)報;2011年08期

相關(guān)會議論文 前10條

1 趙英陽;許道云;;NT-HIT(k)公式的存在性[A];2005年全國理論計算機科學(xué)學(xué)術(shù)年會論文集[C];2005年

2 蔣志華;姜云飛;;一種構(gòu)造Prolog程序子句本體的方法(英文)[A];全國語域web與本體能研討會論文集[C];2006年

3 文衛(wèi)平;;英漢驢子句的差異[A];中國英漢語比較研究會第八次全國學(xué)術(shù)研討會論文摘要匯編[C];2008年

4 魏振春;汪國勝;畢翔;劉小平;;規(guī)則化描述方法中的規(guī)則化簡方法[A];全國第20屆計算機技術(shù)與應(yīng)用學(xué)術(shù)會議（CACIS·2009）暨全國第1屆安全關(guān)鍵技術(shù)與應(yīng)用學(xué)術(shù)會議論文集（上冊）[C];2009年

5 邵明;李光輝;李曉維;;提取極小布爾不可滿足子式[A];全國第13屆計算機輔助設(shè)計與圖形學(xué)（CAD/CG）學(xué)術(shù)會議論文集[C];2004年

6 劉新;;10FL中(μ,ν)-歸結(jié)原理的完備性[A];模糊集理論與模糊應(yīng)用專輯——中國系統(tǒng)工程學(xué)會模糊數(shù)學(xué)與模糊系統(tǒng)委員會第十屆年會論文選集[C];2000年

7 廖加彬;林世平;;基于聚類的中文淺層語義模式識別[A];中國電子學(xué)會第十五屆信息論學(xué)術(shù)年會暨第一屆全國網(wǎng)絡(luò)編碼學(xué)術(shù)年會論文集（下冊）[C];2008年

8 練睿婷;史曉東;;語篇標注語料庫的建設(shè)研究[A];第四屆全國學(xué)生計算語言學(xué)研討會會議論文集[C];2008年

9 高印芝;黃冬梅;;關(guān)于Fuzzy邏輯函數(shù)的性質(zhì)的進一步討論[A];模糊集理論與應(yīng)用——98年中國模糊數(shù)學(xué)與模糊系統(tǒng)委員會第九屆年會論文選集[C];1998年

10 陳敏;;應(yīng)用DCG文法分析漢語[A];語言文字應(yīng)用研究論文集（Ⅰ）[C];1995年

相關(guān)重要報紙文章 前10條

1 貴州 王偉;用ORDER BY子句排序[N];電腦報;2004年

2 貴州 王偉;用GROUPBY子句分組[N];電腦報;2004年

3 邱曉理;Oracle數(shù)據(jù)庫系統(tǒng)性能優(yōu)化策略[N];計算機世界;2006年

4 河南 張華貴;數(shù)據(jù)庫中參數(shù)化查詢的實現(xiàn)[N];電腦報;2001年

5 ;檢閱DB2 Viper[N];計算機世界;2006年

6 山東 任立群;深挖SQL語句潛力查詢效率自然高[N];電腦報;2004年

7 王珂;你想的才是你要的[N];中國電腦教育報;2002年

8 ;實例破解Flash[N];電腦報;2001年

9 Warton;Java的異常處理[N];電腦報;2004年

10 逍遙;用SQL實現(xiàn)樹的查詢[N];計算機世界;2002年

相關(guān)博士學(xué)位論文 前10條

1 許有軍;基于擴展規(guī)則的若干SAT問題研究[D];吉林大學(xué);2011年

2 張立明;結(jié)合可滿足的基于模型等價性驗證及不一致診斷問題研究[D];吉林大學(xué);2012年

3 王秀芹;基于SAT的數(shù)字電路形式驗證方法研究[D];哈爾濱工程大學(xué);2009年

4 呂帥;基于自動推理技術(shù)的智能規(guī)劃方法研究[D];吉林大學(xué);2010年

5 石振國;資源網(wǎng)絡(luò)的精化學(xué)習(xí)及應(yīng)用研究[D];上海大學(xué);2011年

6 劉全;基于tableau的自動推理研究[D];吉林大學(xué);2004年

7 于鵬;統(tǒng)計關(guān)系模型學(xué)習(xí)方法的研究[D];吉林大學(xué);2008年

8 古華茂;描述邏輯概念可滿足性推理研究[D];浙江大學(xué);2009年

9 周俊萍;自動推理與規(guī)劃問題最小上界和相變規(guī)律研究[D];吉林大學(xué);2011年

10 許中衛(wèi);基于雙向搜索的ILP算法構(gòu)建漢語語義自動切分系統(tǒng)[D];安徽大學(xué);2006年

相關(guān)碩士學(xué)位論文 前10條

1 傅陽春;基于2-SAT求解器的SAT算法研究[D];華南理工大學(xué);2010年

2 霍翔;SMT求解器增強技術(shù)的研究[D];北京交通大學(xué);2011年

3 馮陸;子句型信念集靜態(tài)非修正處理方法的優(yōu)化研究[D];大連海事大學(xué);2012年

4 咸愛勇;合取范式最大不全滿足與最大可滿足問題的局部搜索算法研究[D];山東大學(xué);2012年

5 杜巧霞;子句主語的英漢對比研究[D];湖南大學(xué);2012年

6 趙英陽;NT-HIT公式的存在性[D];貴州大學(xué);2006年

7 王迪海;一類SAT Benchmark的算法研究及其應(yīng)用[D];電子科技大學(xué);2010年

8 李淑霞;基于局部搜索隱蔽集算法的QBF求解器研究[D];東北師范大學(xué);2010年

9 宋勃升;DNA自組裝計算模型的應(yīng)用研究[D];安徽理工大學(xué);2011年

10 劉雷;縱覽傳播算法求解隨機3-SAT問題[D];吉林大學(xué);2010年

本文編號：2778422