本文關(guān)鍵詞：基于增量式的#SAT求解算法研究

  更多相關(guān)文章： 增量式 #SAT 更新子句 加權(quán)算法

【摘要】：可滿足(SAT)問題是判定一個合取范式真假的決策性問題,計(jì)算復(fù)雜度為NP完全。人工智能領(lǐng)域的許多問題如約束模型檢測、電路延遲故障測試等都可以轉(zhuǎn)化為SAT問題進(jìn)行求解,其中不乏相似的問題。早期的SAT求解器不能利用實(shí)例間的相似性,每個問題都要從頭開始求解。近年來,隨著增量式SAT算法的出現(xiàn)和廣泛應(yīng)用,求解這一系列實(shí)例的效率有了非常明顯的改善。作為SAT問題的擴(kuò)展,模型計(jì)數(shù)(#SAT)問題需要計(jì)算合取范式所有可滿足賦值的個數(shù),計(jì)算復(fù)雜度為#P完全。該問題在一致性規(guī)劃、概率推理等領(lǐng)域有著廣泛的應(yīng)用,其中也包含很多相似問題。由于該問題求解較為困難,因此在#SAT求解器中實(shí)現(xiàn)信息的重用顯得尤為重要。為了更有效的將求解實(shí)際生活中相似的#SAT問題,本文在精確的cachet算法基礎(chǔ)上加以改進(jìn),提出了增量式模型計(jì)數(shù)算法。首先對多個實(shí)例相互比較,找出需要更新的子句,并按照規(guī)定的格式放入輸入文件中。然后對初始公式進(jìn)行求解,并在求解過程中對可重用信息及時加以緩存。緊接著,再次讀取輸入文件,并根據(jù)緩存信息對更新子句的可滿足性進(jìn)行相應(yīng)的分析和處理。如此循環(huán)讀取并求解,直至整個輸入文件處理完畢。此外,本文還用類似的方法對加權(quán)#SAT算法進(jìn)行了增量式的改進(jìn),為處理多個相似的加權(quán)#SAT問題提供了新思路。為了測試本文算法的求解效率,我們首先選用隨機(jī)和圖著色領(lǐng)域的實(shí)例將本文算法與cachet算法進(jìn)行對比實(shí)驗(yàn),隨后又選用求解困難的概率推理領(lǐng)域的實(shí)例,將本文增量式權(quán)重#SAT算法與普通權(quán)重算法進(jìn)行比較。實(shí)驗(yàn)結(jié)果證實(shí)了本文算法在上述領(lǐng)域的有效性。
【關(guān)鍵詞】：增量式 #SAT 更新子句 加權(quán)算法
【學(xué)位授予單位】：東北師范大學(xué)
【學(xué)位級別】：碩士
【學(xué)位授予年份】：2016
【分類號】：TP18
【目錄】：

• 摘要4-5
• Abstract5-7
• 第一章 緒論7-10
• 1.1 研究背景與意義7
• 1.2 國內(nèi)外研究現(xiàn)狀7-9
• 1.3 研究內(nèi)容及論文組織架構(gòu)9-10
• 第二章 準(zhǔn)備知識10-18
• 2.1 SAT 問題和#SAT 問題10-11
• 2.2 cachet算法11-15
• 2.3 概率推理相關(guān)定義15-18
• 第三章 基于增量式的#SAT 求解算法18-27
• 3.1 增量式SAT算法18-20
• 3.2 增量式模型計(jì)數(shù)算法20-27
• 3.2.1 初步求解20-21
• 3.2.2 增量式求解21-24
• 3.2.3 增量式加權(quán)模型計(jì)數(shù)算法24-25
• 3.2.4 算法整體框架及設(shè)計(jì)25-27
• 第四章 實(shí)驗(yàn)結(jié)果與分析27-34
• 4.1 實(shí)驗(yàn)環(huán)境設(shè)置及輸入文件格式處理27-28
• 4.2 實(shí)驗(yàn)測試用例及結(jié)果分析28-34
• 第五章 總結(jié)與展望34-35
• 參考文獻(xiàn)35-38
• 致謝38

【相似文獻(xiàn)】

中國期刊全文數(shù)據(jù)庫 前10條

1 王秀,葉東毅;基于分布約簡的獲取規(guī)則的增量式方法[J];福州大學(xué)學(xué)報(自然科學(xué)版);2005年01期

2 林俊偉;葉東毅;;基于鄰域辨識矩陣的屬性約簡增量式算法[J];計(jì)算機(jī)應(yīng)用;2009年S1期

3 李斌,馬戈,孫志揮;項(xiàng)目集發(fā)生變化的關(guān)聯(lián)規(guī)則增量式更新算法[J];計(jì)算機(jī)應(yīng)用;2004年12期

4 劉韶濤;余金山;王寧生;;一種迭代增量式的程序構(gòu)建方法[J];遼寧工程技術(shù)大學(xué)學(xué)報;2005年06期

5 王軍琴;;基于三菱FX_(2N)的增量式PID控制器設(shè)計(jì)[J];現(xiàn)代電子技術(shù);2010年12期

6 董學(xué)勤;劉希璐;;基于增量式PID的改進(jìn)算法[J];浙江工商職業(yè)技術(shù)學(xué)院學(xué)報;2012年03期

7 黃文芝 ,倪國元;基于模糊相似系數(shù)的增量式聚類算法[J];微型機(jī)與應(yīng)用;2004年10期

8 羅維;;詞語對齊的快速增量式訓(xùn)練方法研究[J];北京大學(xué)學(xué)報(自然科學(xué)版);2013年01期

9 宋和平;胡成全;王力風(fēng);侯二娜;;新型雙溫度反饋增量式PID控制器的設(shè)計(jì)[J];自動化與儀表;2012年04期

10 劉宗田;屬性最小約簡的增量式算法[J];電子學(xué)報;1999年11期

中國重要會議論文全文數(shù)據(jù)庫 前6條

1 單莘;;一種網(wǎng)絡(luò)告警的增量式情景規(guī)則挖掘方法[A];中國通信學(xué)會第五屆學(xué)術(shù)年會論文集[C];2008年

2 王鑫;袁曉潔;李楠;;Native XML數(shù)據(jù)庫的增量式驗(yàn)證[A];第二十三屆中國數(shù)據(jù)庫學(xué)術(shù)會議論文集（研究報告篇）[C];2006年

3 程建軍;陳曉云;馬志新;;程序設(shè)計(jì)語言課程的增量式教學(xué)法改革與實(shí)踐[A];2005全國計(jì)算機(jī)程序設(shè)計(jì)類課程教學(xué)研討會論文集[C];2005年

4 陳恩紅;張振亞;王煦法;;基于神經(jīng)網(wǎng)絡(luò)的增量式數(shù)據(jù)索引機(jī)制研究[A];2001年中國智能自動化會議論文集（上冊）[C];2001年

5 欒江;唐常杰;黃曉冬;陰小雄;廖勇;;一種增量式支持向量機(jī)文本分類模型[A];第二十屆全國數(shù)據(jù)庫學(xué)術(shù)會議論文集（技術(shù)報告篇）[C];2003年

6 董云云;王中華;馮志全;程金;;吊車-雙擺系統(tǒng)的增量式滑�？刂芠A];第二十七屆中國控制會議論文集[C];2008年

中國重要報紙全文數(shù)據(jù)庫 前1條

1 中國社會科學(xué)院金融研究所研究員 易憲容;地方增量式金融改革亟待有序規(guī)范[N];上海證券報;2012年

中國博士學(xué)位論文全文數(shù)據(jù)庫 前4條

1 顧斌杰;精確增量式在線v-支持向量回歸機(jī)的研究[D];江南大學(xué);2015年

2 朱真峰;快速增量式分類算法研究[D];復(fù)旦大學(xué);2010年

3 王毅;注塑模改模知識的增量式發(fā)現(xiàn)研究[D];廣東工業(yè)大學(xué);2014年

4 陳春雷;面向GPGPU的并行增量式聚類算法研究[D];西北工業(yè)大學(xué);2014年

中國碩士學(xué)位論文全文數(shù)據(jù)庫 前10條

1 王惠賢;基于增量式的#SAT求解算法研究[D];東北師范大學(xué);2016年

2 倪國元;基于模糊聚類的增量式挖掘算法研究[D];華中科技大學(xué);2004年

3 張晶;增量式關(guān)聯(lián)規(guī)則挖掘算法研究及其在飛行品質(zhì)監(jiān)控中的應(yīng)用[D];中國民航大學(xué);2008年

4 陳楠;基于粗集理論的增量式屬性約簡研究[D];長春理工大學(xué);2005年

5 張長城;基于增量式低秩學(xué)習(xí)的視頻目標(biāo)跟蹤[D];大連理工大學(xué);2014年

6 何志剛;多約束增量式布局[D];武漢理工大學(xué);2011年

7 陳飛龍;基于偏序關(guān)系的快速增量式概念格構(gòu)建算法[D];西安電子科技大學(xué);2011年

8 孫巖;增量式貝葉斯網(wǎng)絡(luò)結(jié)構(gòu)學(xué)習(xí)研究[D];杭州電子科技大學(xué);2011年

9 郝允允;增量式數(shù)據(jù)競爭檢測[D];中國科學(xué)技術(shù)大學(xué);2009年

10 賴桃桃;增量式屬性約簡更新算法研究[D];廈門大學(xué);2009年

，

本文編號：832599