發(fā)布時(shí)間：2021-03-16 08:53

　　有序二叉判定圖（OBDDs）是一種表示布爾函數(shù)的高效數(shù)據(jù)結(jié)構(gòu),在形式化驗(yàn)證領(lǐng)域內(nèi)有著廣泛應(yīng)用。它為符號(hào)模型檢測(cè)算法提供實(shí)現(xiàn)框架,使得模型檢測(cè)中的狀態(tài)空間爆炸問(wèn)題得以緩解。OBDDs的規(guī)模嚴(yán)重地依賴于變量序,在最壞情況下其規(guī)模是呈指數(shù)級(jí)增長(zhǎng)的。研究高效的變量排序算法,縮小其結(jié)點(diǎn)規(guī)模,對(duì)于提高符號(hào)模型檢測(cè)效率具有至關(guān)重要的意義。OBDDs變量序問(wèn)題已被證明是一個(gè)NP完全問(wèn)題�，F(xiàn)有的變量序求解算法,如:精確變量排序、啟發(fā)式變量排序等,都是根據(jù)給定的函數(shù)結(jié)構(gòu)對(duì)變量進(jìn)行排序,對(duì)初始函數(shù)依賴性較強(qiáng)。因此具有一定的局限性,不能較好的解決這一問(wèn)題。目前,遺傳算法在求解該問(wèn)題上效果較好。該算法以動(dòng)態(tài)方式搜索最優(yōu)解,擺脫了對(duì)給定函數(shù)的依賴性。但算法仍存在搜索效率低、局部?jī)?yōu)化能力弱、收斂速度慢等問(wèn)題。為提升遺傳算法求解OBDDs變量序問(wèn)題的搜索效率,文章在原遺傳算法基礎(chǔ)上引入了自適應(yīng)策略,并對(duì)其自適應(yīng)模型進(jìn)行改進(jìn)。改進(jìn)的算法根據(jù)種群進(jìn)化程度動(dòng)態(tài)調(diào)整交叉概率和變異概率,確保種群進(jìn)化朝著正確方向進(jìn)行,從而提升算法收斂速度和局部?jī)?yōu)化能力。算法通過(guò)調(diào)用軟件包Buddy中部分內(nèi)置函數(shù)測(cè)試樣本獲得實(shí)驗(yàn)數(shù)據(jù)。實(shí)驗(yàn)結(jié)果表明... 

【文章來(lái)源】：遼寧師范大學(xué)遼寧省

【文章頁(yè)數(shù)】：48 頁(yè)

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

【部分圖文】：

真值表及其對(duì)應(yīng)二叉判定樹

二叉判定樹簡(jiǎn)化過(guò)程

無(wú)序的BDDsFig.2.3TheunorderedBDDs

【參考文獻(xiàn)】：
期刊論文
[1]基于災(zāi)變遺傳算法的二叉判定圖最小化算法[J]. 王鎮(zhèn)道,陳義.  計(jì)算機(jī)工程與應(yīng)用. 2015(03)
[2]改進(jìn)的乘冪適應(yīng)度函數(shù)在遺傳算法中的應(yīng)用[J]. 楊水清,楊加明,孫超.  計(jì)算機(jī)工程與應(yīng)用. 2014(17)
[3]基于適應(yīng)度函數(shù)及交叉操作改進(jìn)的自適應(yīng)遺傳算法[J]. 竇明鑫,劉曉霞.  合作經(jīng)濟(jì)與科技. 2012(13)
[4]模擬退火算法在BDD變量最優(yōu)排序中的應(yīng)用[J]. 胡東華,張旭.  科技信息(科學(xué)教研). 2007(34)
[5]自適應(yīng)遺傳算法的改進(jìn)及在系統(tǒng)辨識(shí)中應(yīng)用研究[J]. 任子武,傘冶.  系統(tǒng)仿真學(xué)報(bào). 2006(01)
[6]二叉判定圖最優(yōu)化算法研究綜述[J]. 王明全,于海斌,王宏.  信息與控制. 2004(05)



本文編號(hào)：3085771