本文關鍵詞：基于擴展規(guī)則的模型計數(shù)方法研究，由筆耕文化傳播整理發(fā)布。

【摘要】：早在二十世紀五十年代,智能規(guī)劃一經(jīng)提出便成為了人工智能領域中的一個前沿研究領域,自此,隨著國內(nèi)外諸多研究學者們不懈努力,在該領域的研究成果方面取得了突破性的進展。目前求解該問題存在著許多種方法,其中一種較為高效的求解方法則是將規(guī)劃問題編譯為命題可滿足性問題(SAT問題),然后利用SAT求解器進行求解。有時此種間接求解的方法會比直接求解的方法更為高效快捷,目前已成為求解智能規(guī)劃問題的主流方法之一。在1971年,Cook等人證明SAT問題是NP完全的。事實上,許多NP問題都可以轉(zhuǎn)為SAT問題進行求解。然而,在人工智能研究領域還有許多經(jīng)典問題的計算復雜度是高于NP的,對于這些問題的求解僅僅判斷給定命題公式是否可滿足是不夠的,還需要知道問題模型的個數(shù)。由此擴展出了模型計數(shù)問題(#SAT問題)。如貝葉斯網(wǎng)絡推理,概率規(guī)劃問題等都可以轉(zhuǎn)化成#SAT問題進行求解。因此,如何高效地求解#SAT問題,對人工智能的很多領域都有重要意義。目前,求解#SAT問題的算法可以分為精確求解和近似求解兩種。精確算法可以保證計算出給定命題公式的準確模型個數(shù);而近似算法只能計算出給定公式模型的近似個數(shù)。在精確求解的算法中主要有基于DPLL(Davis Putnam Logemann and Loveland)的方法和基于擴展規(guī)則的方法。這兩種方法是互補的求解方法。一般情況下,當互補因子較高時,基于擴展規(guī)則的求解方法要優(yōu)于基于DPLL求解方法;反之,當互補因子較低時,要差于基于DPLL求解方法。本文在對基于擴展規(guī)則的模型計數(shù)求解方法CER深入研究的基礎上,從不同角度對其進行改進,提出了兩種更為高效的求解方法:(1)結(jié)合擴展規(guī)則重構(gòu)的#SAT問題增量求解方法:對CER中的重要計算公式進行重構(gòu),并證明了重構(gòu)的正確性;給出了極大項相交集和擴展極大項相交集的定義,并提出結(jié)合兩者關系復用極大項相交集求解結(jié)果的增量計算方法,還刪減了所有廣義互補子句集對應的擴展極大項相交集,有效避免了許多冗余計算;給出用互補表記錄子句間互補關系的方法,提出一種對極大項相交集的基礎子句集進行增量判定互補的方法,很好地避免了在判定子句間及基礎子句集互補性時的大量冗余計算。實驗結(jié)果表明:與CER方法相比,RCER方法效率更高,尤其是互補因子較低的情況下。(2)結(jié)合互補度的基于擴展規(guī)則#SAT問題求解方法:在計算給定子句集的模型個數(shù)時,利用SE-Tree(set enumeration tree)形式化地表達計算過程,逐步生成需要計算的子句集合。并在SE-Tree中添加終止結(jié)點,避免大部分含互補文字子句集合的生成,且不會因剪枝而導致求解不完備。提出互補度的概念,在擴展SE-Tree結(jié)點時按照互補度由大到小的順序擴展,較早地生成含互補文字且長度較小的子句集合,有效減少枚舉樹生成的結(jié)點個數(shù),進而減少對子句集合判斷是否含互補文字的計算次數(shù)。實驗結(jié)果表明,與CER方法相比該方法效率較好,且進一步改進了CER方法在互補因子較低時求解效率低下的不足。以上兩種方法從不同角度對CER方法進行了改進,并取得了較好的效果。兩種方法分別利用了CER方法中重要公式的計算項間的關系和計算順序減少了求解過程中的冗余計算,從而達到提高效率的目的。
【關鍵詞】：智能規(guī)劃 命題可滿足性問題 模型計數(shù) 擴展規(guī)則 增量方法
【學位授予單位】：吉林大學
【學位級別】：碩士
【學位授予年份】：2016
【分類號】：TP18
【目錄】：

• 摘要4-6
• Abstract6-10
• 第1章 緒論10-16
• 1.1 研究背景和意義10-12
• 1.2 研究現(xiàn)狀12-13
• 1.3 本文工作13-16
• 第2章 模型計數(shù)問題16-31
• 2.1 算法的復雜度16-17
• 2.2 SAT問題17-19
• 2.3 SAT問題求解方法19-24
• 2.4 #SAT問題24-26
• 2.5 #SAT問題求解方法26-31
• 第3章 基于擴展規(guī)則的#SAT問題求解方法31-39
• 3.1 擴展規(guī)則31-33
• 3.2 CER算法33-37
• 3.3 本章小結(jié)37-39
• 第4章 結(jié)合擴展規(guī)則重構(gòu)的#SAT問題增量求解方法39-51
• 4.1 公式重構(gòu)39-44
• 4.2 極大項相交集增量計算方法44-46
• 4.3 互補表增量判定方法46-47
• 4.4 實驗結(jié)果與分析47-51
• 第5章 結(jié)合互補度的基于擴展規(guī)則#SAT問題求解方法51-58
• 5.1 互補度51-52
• 5.2 集合枚舉樹52-53
• 5.3 CDCER算法53-56
• 5.4 實驗結(jié)果與分析56-58
• 第6章 總結(jié)與展望58-61
• 6.1 工作總結(jié)58-59
• 6.2 展望59-61
• 參考文獻61-66
• 作者簡介及在學期間所取得的科研成果66-67
• 致謝67

【相似文獻】

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

1 徐東霞,陳為民,陳衛(wèi),陳雍樂;凸輪軸測量中計數(shù)方法的研究[J];微計算機應用;2003年03期

2 陳本永,吳曉維,李達成;一種新型的干涉條紋軟件計數(shù)方法及其實現(xiàn)研究[J];傳感技術(shù)學報;2004年03期

3 于杰;肖國強;代毅;;粘連蠶卵計數(shù)方法的研究[J];計算機工程與應用;2011年08期

4 孫洋;;視頻中行人快速檢測計數(shù)方法研究[J];數(shù)字技術(shù)與應用;2013年11期

5 朱亞華;;懸浮細胞圖像的計數(shù)方法研究[J];佳木斯大學學報(自然科學版);2010年01期

6 趙斌,侯金龍;外差干涉信號的一種相位計數(shù)方法[J];華東交通大學學報;2003年02期

7 鄒應國;康宜華;;成捆鋼筋快速計數(shù)方法的研究[J];機床與液壓;2006年02期

8 ;其它測量[J];電子科技文摘;1999年11期

9 楊慧贊;林勇;唐章生;張永德;陳忠;黃姻;甘西;;基于圖像處理的魚卵計數(shù)方法研究[J];水生態(tài)學雜志;2011年05期

10 王曉城,高小榕;基于混合隱Markov模型的紅細胞計數(shù)方法[J];清華大學學報(自然科學版);2004年06期

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

1 王彥敏;林小竹;杜天蒼;田瑞卿;;基于watershed變換的粘連物體的分割和計數(shù)方法[A];第十二屆全國圖象圖形學學術(shù)會議論文集[C];2005年

2 鐘新玉;劉峽壁;魏雪;曹月;;融合視頻與激光信息的雙向人流計數(shù)方法[A];全國第22屆計算機技術(shù)與應用學術(shù)會議(CACIS·2011)暨全國第3屆安全關鍵技術(shù)與應用（SCA·2011）學術(shù)會議論文摘要集[C];2011年

3 馮愛平;;基于種子搜索法的金屬棒材計數(shù)方法研究[A];2010年西南三省一市自動化與儀器儀表學術(shù)年會論文集[C];2010年

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

1 記者 鄧暉;清華簡《算表》或為“九九”表延伸[N];光明日報;2014年

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

1 賈鳳雨;基于擴展規(guī)則的模型計數(shù)方法研究[D];吉林大學;2016年

2 高靜偉;通濟橋高密度人群計數(shù)方法研究與實現(xiàn)[D];中山大學;2013年

3 辛海濤;基于運動目標檢測的行人計數(shù)方法[D];河北工業(yè)大學;2011年

4 李姝霖;智能監(jiān)控系統(tǒng)中行人計數(shù)方法的研究與實現(xiàn)[D];西安電子科技大學;2011年

5 劉向東;高密度人群計數(shù)方法的研究與應用[D];浙江工業(yè)大學;2012年

6 唐亮;一種新的發(fā)光二極管自動精確計數(shù)方法[D];復旦大學;2012年

7 黃奕國;基于Flow Mosaicking的視頻行人計數(shù)方法研究[D];中山大學;2013年

8 雷波;基于數(shù)字圖像處理的卡片計數(shù)方法研究[D];華中科技大學;2013年

9 于杰;粘連物體計數(shù)方法研究[D];西南大學;2011年

  本文關鍵詞：基于擴展規(guī)則的模型計數(shù)方法研究，，由筆耕文化傳播整理發(fā)布。

本文編號：288580