二元判斷圖BDD及其JAVA實(shí)現(xiàn)的應(yīng)用與研究.pdf

1、在數(shù)字控制系統(tǒng)、計(jì)算機(jī)輔助設(shè)計(jì)(CAD)，計(jì)算機(jī)輔助測(cè)試(CAT)、人工智能(AI)以及可編程控制器等領(lǐng)域的許多問(wèn)題都可以表示成一系列關(guān)于布爾函數(shù)的運(yùn)算，這些運(yùn)算有賴(lài)于布爾函數(shù)的符號(hào)表示和算法的有效性。一般而言，我們通常采用布爾函數(shù)表達(dá)式或真值表來(lái)描述數(shù)字邏輯函數(shù).布爾函數(shù)是一種可以精確地描述數(shù)字邏輯函數(shù)的方法。 但隨著大規(guī)模和超大規(guī)模集成電路的迅速發(fā)展，數(shù)字邏輯函數(shù)的運(yùn)算變得日益復(fù)雜，上述的傳統(tǒng)方法逐漸暴露出一些缺點(diǎn)，比如使用

2、布爾函數(shù)來(lái)表示數(shù)字邏輯函數(shù)的話(huà)，表達(dá)式往往會(huì)變得龐大和復(fù)雜，使得函數(shù)處理時(shí)間過(guò)長(zhǎng)：而使用真值表方式的話(huà)，則需要占用大量的存儲(chǔ)空間，只能用在一些特殊的領(lǐng)域。鑒于上述的情況，研究人員不斷的探索，試圖找到描述更加簡(jiǎn)潔、操作更加方便的數(shù)字邏輯函數(shù)表達(dá)方式。 1986年，E.R.Bryant提出了用二元判斷圖BDD(BinaryDecisionDiagram)來(lái)表示布爾函數(shù)，和其他表示法相比BDD在人們尋找大型數(shù)字系統(tǒng)的有效分析、測(cè)試和計(jì)

3、算方法中，由于其固有的優(yōu)越性能而日益受到重視。綜合來(lái)說(shuō)，BDD具有如下的優(yōu)點(diǎn)： (1)直觀，明了，便于邏輯電路的分析。 (2)能反映數(shù)字電路的邏輯描述的細(xì)節(jié)，這點(diǎn)對(duì)電路的分析和測(cè)試非常重要。 (3)便于計(jì)算機(jī)的存儲(chǔ)，編寫(xiě)的程序比布爾代數(shù)方法編寫(xiě)的程序更短。 (4)便于使用人工智能的方法，啟發(fā)式進(jìn)行求解空間搜索。 (5)不管是硬件還是軟件實(shí)現(xiàn)，都能獲得比布爾代數(shù)算法更高的執(zhí)行速度。 (6)可

4、應(yīng)用并行圖論算法，進(jìn)一步提高運(yùn)算速度。 模型檢測(cè)主要是驗(yàn)證某-模型生成的有限狀態(tài)系統(tǒng)是否滿(mǎn)足模型所要求的屬性。模型檢測(cè)技術(shù)可以抽象地描述為：給定一個(gè)模型M和邏輯描述的性質(zhì)P，檢查模型M中性質(zhì)P是否成立。模型檢測(cè)主要是驗(yàn)證某-模型生成的有限狀態(tài)系統(tǒng)是否滿(mǎn)足模型所要求的屬性。模型檢測(cè)中最大的挑戰(zhàn)就是狀態(tài)空間的爆炸問(wèn)題。這個(gè)問(wèn)題源于系統(tǒng)中有許多不同部件的交互，或者系統(tǒng)中有取值范圍很大的復(fù)雜數(shù)據(jù)結(jié)構(gòu)，在這種情況下系統(tǒng)狀態(tài)的規(guī)模將變得非常

5、龐大。由于BDD所用的存儲(chǔ)空間較少，因此研究人員將BDD引入到了模型檢驗(yàn)中，使得模型檢驗(yàn)所能驗(yàn)證的系統(tǒng)規(guī)模得到了很大的提高。 時(shí)態(tài)邏輯在模型檢測(cè)中占有非常重要的地位，模型檢測(cè)是基于時(shí)態(tài)邏輯，時(shí)態(tài)邏輯的模型可能由幾個(gè)狀態(tài)構(gòu)成，時(shí)態(tài)邏輯公式可能在一些狀態(tài)為真，在其它為假，因此，該公式的值隨著狀態(tài)的變化而變化。依據(jù)對(duì)系統(tǒng)狀態(tài)的時(shí)間路徑的不同刻畫(huà)，時(shí)態(tài)邏輯可以分成兩大類(lèi)：計(jì)算樹(shù)時(shí)態(tài)邏輯(CTL)和線性時(shí)態(tài)邏輯(LTL)。 CTL

6、是由Clarke和Emerson提出的。它的運(yùn)算符具有簡(jiǎn)單的性質(zhì)，可以有效地計(jì)算某一公式在有窮狀態(tài)模型處于某一狀態(tài)時(shí)是否滿(mǎn)足。它是一種時(shí)間模型采用樹(shù)的方式、具有多個(gè)分支的不確定狀態(tài)路徑構(gòu)成。 在模型檢測(cè)過(guò)程中采用BDD的主要原因是：采用BDD表達(dá)的兩個(gè)謂詞公式時(shí)，兩個(gè)BDD范式邏輯相等當(dāng)且僅當(dāng)這兩個(gè)BDD范式是語(yǔ)法相等，即兩個(gè)BDD范式邏輯相等，當(dāng)且僅當(dāng)這兩個(gè)BDD范式是同一個(gè)BDD范式。目前，利用BDD來(lái)對(duì)規(guī)劃問(wèn)題求解的基本思

7、想是：先將規(guī)劃問(wèn)題的狀態(tài)和動(dòng)作表示為BDD范式，再將其輸入劍BDD的求解器，然后將求解得劍的結(jié)果轉(zhuǎn)化為一般規(guī)劃問(wèn)題的表示。 JAVABDD是一套非常優(yōu)秀的用于BDD的生成，執(zhí)行各種邏輯操作，描述狀態(tài)變化的Java開(kāi)源軟件包。可以利用套軟件包開(kāi)發(fā)出CTL的各種公式，實(shí)現(xiàn)簡(jiǎn)單的模型檢測(cè)功能。 1.為了能夠有效地使用和擴(kuò)充JavaBDD這套軟件，我們對(duì)該軟件的主要算法進(jìn)行了代碼分析。包括： (1)MK算法和Build算

8、法：JavaBDD是如何將數(shù)組的存儲(chǔ)效率和哈希表的查找效率有效地結(jié)合起來(lái)，從而建立ROBDD的數(shù)據(jù)結(jié)構(gòu)，使其占空間少，查找速度快。 (2)APPLY算法：JavaBDD是如何實(shí)現(xiàn)兩個(gè)布爾表達(dá)式之間的邏輯操作。 (3)RESTRIC算法，JavaBDD如何計(jì)算布爾表達(dá)式的賦值結(jié)果(4)SATCOUNT算法：計(jì)算ROBDD中的可滿(mǎn)足集元素個(gè)數(shù)。 (5)ANYSAT算法：尋找一個(gè)可滿(mǎn)足的賦值。 (6)ALISA

9、Y算法：尋找全部可滿(mǎn)足賦值。 (7)JavaBDD中存在量詞，全稱(chēng)量詞與唯一量詞的算法實(shí)現(xiàn)。 2.為JavaBDD增加了差集運(yùn)算功能。 3.將皇后問(wèn)題轉(zhuǎn)化為邏輯操作，利用JavaBDD計(jì)算結(jié)果。 4.利用JavaBDD進(jìn)行電路電路功能分析與等價(jià)性判斷。 5.利用JavaBDD實(shí)現(xiàn)計(jì)算樹(shù)時(shí)序邏輯的AX,EX,AF,EF，AG,EG,AU,EU操作符。 6.利用JavaBDD完成Miner's