這篇文章會(huì)介紹一種能高效操作 BDD（Binary Decision Diagrams，二叉決策圖）和布爾函數(shù)的數(shù)據(jù)結(jié)構(gòu) —— JavaBDD。二叉決策圖廣泛用于模型檢查，形式驗(yàn)證，優(yōu)化電路圖等方面。同時(shí)，該數(shù)據(jù)結(jié)構(gòu)也可以和上一篇文章中介紹的 Graphviz 聯(lián)系起來。
提示：本篇內(nèi)容略多，但如果堅(jiān)持讀完，一定會(huì)有收獲 : )

BDD與布爾函數(shù)

畢設(shè)剛開始不久，指導(dǎo)老師讓我學(xué)習(xí)一下 JavaBDD 庫(kù)。之前我也沒聽說過這玩意兒，在網(wǎng)上一查，看到 BDD 的意思是 Behavior Driven Development，行為驅(qū)動(dòng)開發(fā)。仔細(xì)了解以后，感覺和畢設(shè)題目 “ 狀態(tài)機(jī)自動(dòng)生成與圖形化仿真系統(tǒng)研究與實(shí)現(xiàn) ” 沒有半毛錢的關(guān)系。（后來才知道行為驅(qū)動(dòng)開發(fā)在近年來的熱度在逐漸上漲，是一種比較新的思想，感興趣的同學(xué)可以自行了解一下）

于是重新又搜索了幾次，重要發(fā)現(xiàn)旮旯角里的一個(gè)網(wǎng)站 http://javabdd.sourceforge.net/ 提到了 JavaBDD 這個(gè)庫(kù)，原來它就是 JavaBDD 的官網(wǎng)，古老而簡(jiǎn)陋的網(wǎng)站，信息相當(dāng)少，幾句話就介紹完了。官網(wǎng)還給出了一個(gè)介紹 BDD 的頁(yè)面，然而打開顯示 404。拜托，這到底是個(gè)啥東西！不得已只好各種查找，最后在維基百科上看到了下面的定義：

BDD 是用于表示布爾函數(shù)的數(shù)據(jù)結(jié)構(gòu)。布爾函數(shù)可以表示為有根，有向，非循環(huán)圖，它由若干決策節(jié)點(diǎn)和終端節(jié)點(diǎn)組成。有兩種類型的終端節(jié)點(diǎn)稱為0終端和1終端。每個(gè)決策節(jié)點(diǎn)都用布爾變量標(biāo)記，并有兩個(gè)子節(jié)點(diǎn)，稱為低子節(jié)點(diǎn)和高子節(jié)點(diǎn)。從節(jié)點(diǎn)到低（或高）子節(jié)點(diǎn)的邊表示0（分別為1）的賦值。如果不同的變量在來自根的所有路徑上以相同的順序出現(xiàn)，則這種BDD稱為“有序”。如果將以下兩個(gè)規(guī)則應(yīng)用于其圖表，則稱BDD為“約減”。

• 合并任何同構(gòu)子圖。
• 消除兩個(gè)孩子節(jié)點(diǎn)同構(gòu)的任何節(jié)點(diǎn)。

在流行的用法中，術(shù)語(yǔ) BDD 幾乎總是指減少有序二進(jìn)制決策圖（文獻(xiàn)中的ROBDD，當(dāng)需要強(qiáng)調(diào)排序和減少方面時(shí)使用）。ROBDD的優(yōu)點(diǎn)在于它對(duì)于特定函數(shù)和變量順序是規(guī)范的（唯一的）。該屬性使其在功能等價(jià)檢查和其他操作（如功能技術(shù)映射）中非常有用。

從根節(jié)點(diǎn)到1終端的路徑表示所表示的布爾函數(shù)為真的（可能是部分的）變量賦值。當(dāng)路徑從節(jié)點(diǎn)下降到低（或高）子節(jié)點(diǎn)時(shí)，該節(jié)點(diǎn)的變量被分配為0（分別為1）。

我估計(jì)維基百科給出的定義沒人看??能理解的同學(xué)，我給你點(diǎn)個(gè)大大的贊??至少我當(dāng)時(shí)是懵逼的。不過還好，維基百科接下來給出了例子，這次再看，應(yīng)該能理解一些了：

二叉決策圖的例子，from Wikipedia

再看左邊的類似二叉樹的圖，根節(jié)點(diǎn)對(duì)應(yīng)著第一個(gè)布爾變量 x1，第二層和第三層的節(jié)點(diǎn)對(duì)應(yīng)著第二個(gè)和第三個(gè)布爾變量。這些代表布爾變量的圓形的非葉子節(jié)點(diǎn)也就是上面的定義中的決策節(jié)點(diǎn)，而方形的葉子節(jié)點(diǎn)只有 0 和 1 兩個(gè)取值，代表著布爾函數(shù)的值，就是上面的定義中的終端節(jié)點(diǎn)。最后，對(duì)于一個(gè)決策節(jié)點(diǎn)來說，都有兩條邊，一虛一實(shí)，分別表示該節(jié)點(diǎn)代表的布爾變量的值取假（0）或取真（1）。

那么這個(gè)類似二叉樹的東西（二叉決策樹）和布爾函數(shù) f (x1, x2, x3) 有什么關(guān)系呢？仔細(xì)觀察可以發(fā)現(xiàn)，從根節(jié)點(diǎn)到任意一個(gè)葉子節(jié)點(diǎn)的路徑，其實(shí)對(duì)應(yīng)著三個(gè)布爾變量的取值和布爾函數(shù)的取值，而這些取值和真值表是對(duì)應(yīng)的。比如我們看到真值表的第一行，x1, x2, x3 都為零，對(duì)應(yīng)的就是根節(jié)點(diǎn) x1 走左邊的虛邊（因?yàn)樘撨厡?duì)應(yīng)的取值是 0，實(shí)邊對(duì)應(yīng)的取值是 1），到達(dá)第二個(gè)節(jié)點(diǎn) x2 后，繼續(xù)走虛的那條邊邊，到達(dá)第三個(gè)節(jié)點(diǎn) x3 后，仍然走左邊的虛邊，就到達(dá)了為 1 的葉子節(jié)點(diǎn)，意味著布爾函數(shù)值為 1（也就是布爾函數(shù)結(jié)果為真）。而真值表第一行 f 的取值也是 1。再比如讓 x1=0, x2=1, x3=0，那么從根節(jié)點(diǎn)開始先往左，再往右，再往左，到達(dá)了為 0 的葉子節(jié)點(diǎn)，意味著布爾函數(shù)為假，真值表第三行的結(jié)果確認(rèn)了這一點(diǎn)。

所以我們可以發(fā)現(xiàn)，實(shí)際上左邊的二叉決策樹使用了另外一種方式表示了布爾函數(shù)真值表的信息！也就是說，一個(gè)布爾函數(shù)是可以由二叉決策樹來表示的?。ǜ杏X真的很神奇，就像以前上學(xué)第一次聽到老師講數(shù)形結(jié)合的時(shí)候，老師在黑板上列了一個(gè) y 關(guān)于 x 的函數(shù)，然后把它在直角坐標(biāo)系中畫了出來，感覺這種數(shù)與形的轉(zhuǎn)換很有意思）

那么實(shí)際上，左邊的圖是可以進(jìn)一步壓縮的。為啥要壓縮呢，很簡(jiǎn)單，因?yàn)槎鏇Q策樹中的節(jié)點(diǎn)數(shù)目隨著布爾變量的增加會(huì)以指數(shù)方式增大，2 個(gè)變量對(duì)應(yīng)的節(jié)點(diǎn)數(shù)是 1+2，3 個(gè)變量對(duì)應(yīng)的節(jié)點(diǎn)數(shù)是 1+2+4，4 個(gè)變量對(duì)應(yīng)的節(jié)點(diǎn)數(shù)是 1+2+4+8 ... 那么 x 個(gè)變量對(duì)應(yīng)的節(jié)點(diǎn)數(shù)是 2^x - 1 這么多?。ㄗⅲ哼@個(gè)地方不太嚴(yán)謹(jǐn)，因?yàn)椴煌牟紶柡瘮?shù)對(duì)應(yīng)的二叉決策樹，每層節(jié)點(diǎn)數(shù)并不一定是按 1, 2, 4, 8... 這樣的規(guī)律增加的，這里為了簡(jiǎn)化就這么寫，但不管怎樣，如果不壓縮的話，節(jié)點(diǎn)數(shù)目的增長(zhǎng)速度肯定是越來越快的 : ) 大家理解一下）

你可能會(huì)說，那咋辦嘛，我不知道怎么壓縮。這個(gè)時(shí)候，維基百科的定義就發(fā)揮作用了！請(qǐng)往上翻到定義那里，將粗體定義再次閱讀一遍，相信會(huì)有新的收獲 (??????)??

定義中說 BDD 一般指的都是 ROBDD（Reduced Ordered BDD，約減且有序的BDD），也就是說 BDD 默認(rèn)都是約減的和有序的。約減需要滿足兩個(gè)條件：合并任何同構(gòu)子圖，以及消除兩個(gè)孩子節(jié)點(diǎn)同構(gòu)的任何節(jié)點(diǎn)。這兩個(gè)條件比較繞，翻譯成更通俗的語(yǔ)言就是：把兩個(gè)一模一樣的部分合并到一塊，以及對(duì)于任意兩個(gè)節(jié)點(diǎn)，如果它們左孩子一樣，右孩子也一樣（注意，這里沒說左右孩子是一樣的。事實(shí)上，如果左右孩子都一樣，說明這個(gè)節(jié)點(diǎn)不論取真還是假都不會(huì)對(duì)結(jié)果有一些，也就是說這個(gè)節(jié)點(diǎn)是冗余的，可以刪掉），那么就刪除其中一個(gè)節(jié)點(diǎn)（或者說把這兩個(gè)節(jié)點(diǎn)合并到一起）。有序則需要滿足，從根節(jié)點(diǎn)出發(fā)的所有路徑上，布爾變量出現(xiàn)的順序都是相同的。這一段話如果看不懂，不用急，當(dāng)作了解就可以，如果之后接觸 BDD 比較多，這些概念到時(shí)候順其自然就理解了。

接下來再次翻到上面的圖，看到最右邊，就是布爾函數(shù) f (x1, x2, x3) 對(duì)應(yīng)的 BDD（或者說是 ROBDD）了。仔細(xì)觀察它和左邊的二叉決策樹的區(qū)別，可以發(fā)現(xiàn)有不少變化：

• 二叉決策樹中的節(jié)點(diǎn)，虛邊都在左側(cè)，實(shí)邊都在右側(cè)，但 BDD 中不一定這樣，而且在虛邊都標(biāo)記了 0，實(shí)邊都標(biāo)記了 1，顯得更清晰了；
• 終端節(jié)點(diǎn)只有兩個(gè)了，分別為 0 和 1。這是約減過的結(jié)果，因?yàn)椴紶柡瘮?shù)最后的取值只有這兩種情況，因此之前有很多冗余的 0 節(jié)點(diǎn)和 1 節(jié)點(diǎn)；
• 對(duì)應(yīng) x1 節(jié)點(diǎn)取 1 的這一側(cè)，x2 節(jié)點(diǎn)直接就指向終端節(jié)點(diǎn)了，沒有了 x3 節(jié)點(diǎn)。這也是約減過的結(jié)果，在二叉決策樹中可以看到，有兩個(gè) x3 節(jié)點(diǎn)不管取真還是假，到達(dá)的終端節(jié)點(diǎn)都一樣，這意味著它們是冗余的，可以刪去，而指向 x3 節(jié)點(diǎn)的邊只需要直接指向 x3 節(jié)點(diǎn)的孩子即可；
• 有多個(gè)邊可以同時(shí)指向一個(gè)節(jié)點(diǎn)，比如終端節(jié)點(diǎn)就是這樣。實(shí)際上對(duì)于 BDD 來說這是沒問題的，這實(shí)現(xiàn)了節(jié)點(diǎn)的復(fù)用，進(jìn)一步壓縮了節(jié)點(diǎn)數(shù)。

因此，在維基百科的定義里才會(huì)說，布爾函數(shù)可以表示為有根，有向，非循環(huán)圖，它由若干決策節(jié)點(diǎn)和終端節(jié)點(diǎn)組成。這也就是說 BDD（或者說ROBDD）本質(zhì)是一個(gè)圖，且有根，有向，非循環(huán)，可以用來表示布爾函數(shù)。之前說了這么多，也就是想闡明布爾函數(shù)和 BDD 之間的轉(zhuǎn)換關(guān)系。那么知道了這個(gè)有什么用呢？當(dāng)然有用！它為我們提供了一種全新的解決布爾函數(shù)相關(guān)問題的思路！就像之前用數(shù)形結(jié)合法解題，有時(shí)候你看著函數(shù)就是不知道怎么做題，但是當(dāng)你把他在直角坐標(biāo)系中畫出來，你可能瞬間就明白了答案是什么。布爾函數(shù)也是這樣。當(dāng)涉及到大型、復(fù)雜的布爾函數(shù)時(shí)，我們可以將其轉(zhuǎn)換成圖的形式（BDD），然后使用圖論相關(guān)的知識(shí)或者其他的性質(zhì)來高效的解決問題。就是這么厲害~~~

JavaBDD庫(kù)與一篇論文

終于要開始寫 JavaBDD 這個(gè)庫(kù)了。。。它是由美國(guó)斯坦福大學(xué)的 John Whaley 領(lǐng)導(dǎo)的團(tuán)隊(duì)設(shè)計(jì)開發(fā)的開源代碼庫(kù)，采用 Java 開發(fā)。這個(gè)庫(kù)相當(dāng)優(yōu)秀，在此膜拜一下作者，但是還是得吐槽一下，為什么文檔這么爛?。?！是的，這個(gè)庫(kù)幾乎就是沒有文檔，官網(wǎng)中唯一給出的只有 API 文檔 http://javabdd.sourceforge.net/apidocs/index.html，各位可以感受一下它的酸爽。網(wǎng)上關(guān)于 JavaBDD 的資料也極少，可能是因?yàn)橛玫娜瞬欢喟?。?！?/p>

我查了很久也沒有找到任何的資料，倒是找到了 John Whaley 在 ResearchGate 上介紹 JavaBDD 的一篇論文，但是無法查看和下載。。。還有就是 Stackoverflow 上的這個(gè)回答?？梢哉f我是根據(jù)這個(gè)回答，然后對(duì)照著 API 文檔和源碼各種嘗試、失敗、重復(fù)才一點(diǎn)點(diǎn)知道 JavaBDD 是怎么使用的。從這一點(diǎn)上來說，JavaBDD 真的很坑。

在這段探索的過程中，我做了一些 JavaBDD 的使用筆記，比較簡(jiǎn)單，就先不發(fā)出來了，如果有同學(xué)需要可以在文章底部留言。同時(shí)在搜集資料期間，也發(fā)現(xiàn)了一些和 BDD 相關(guān)的有些用的資料，分別是一個(gè)講座 PPT OBDD原理及其應(yīng)用 以及知網(wǎng)的一篇論文《二元判斷圖BDD及其JAVA實(shí)現(xiàn)的應(yīng)用與研究》。

這里對(duì)于這個(gè)論文，我得重點(diǎn)說幾句。首先它對(duì)我的畢設(shè)幫助還是很大的，里面也有一點(diǎn)使用 JavaBDD 的代碼，是我探索過程中很好的參考。但是我在之后做畢設(shè)的過程中發(fā)現(xiàn)，這篇論文相當(dāng)有意思。首先看它的目錄如下圖：

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

還沒完，在這篇論文的第 4.3.2 節(jié)的第一段中，有一句這樣的話：

《二元判斷圖BDD及其JAVA實(shí)現(xiàn)的應(yīng)用與研究》第 4.3.2 節(jié)的第一段

可以說，整篇論文，除了第一章和部分第四章的內(nèi)容是作者寫的，論文的核心第二三章絕大部分都是來自別人的成果。作者除了提供背景說明、一些分析以及一些 JavaBDD 的代碼之外，其實(shí)做的很有限。作為碩士畢業(yè)論文，這樣的情況其實(shí)是不應(yīng)該發(fā)生的。希望看到這里的同學(xué)能夠以此為鑒。

接下來開始真正的介紹 JavaBDD 的用法了！
（我怎么感覺都要寫完了才開始介紹。。。）

JavaBDD 庫(kù)能夠方便地操作 BDD 并進(jìn)行一些復(fù)合操作。在 JavaBDD 中創(chuàng)建 BDD 需要用到 BDDFactory 類，首先需要通過 init() 方法初始化一個(gè)BDDFactory 對(duì)象。該方法接收兩個(gè) int 類型的參數(shù)，分別表示初始節(jié)點(diǎn)表大小和操作緩存大小。

接下來需要對(duì)該 BDDFactory 對(duì)象調(diào)用 setVarNum() 方法，接收一個(gè) int 類型的參數(shù)，設(shè)置需要使用的 BDD 變量個(gè)數(shù)。接下來就可以對(duì) BDDFactory 對(duì)象調(diào)用 ithVar() 方法創(chuàng)建表示第 i 個(gè)變量的BDD 變量?？梢詫⒎祷刂悼闯梢粋€(gè)節(jié)點(diǎn)，子節(jié)點(diǎn)為 true 和 false。除此之外，請(qǐng)求的變量必須在setvarnum 定義的范圍內(nèi)。

當(dāng)創(chuàng)建了若干變量之后，就可以調(diào)用 and()、or() 等方法進(jìn)行操作了。如果要獲得結(jié)果BDD 的詳情，主要有兩種方式，一是調(diào)用 printDot() 方法以 DOT 方式打印這個(gè) BDD，二是調(diào)用 printSet() 方法，打印此 BDD 指定的真值分配集合。注意，這里的 printDot() 方法非常重要，正是由于這個(gè)方法，BDD 才能以 DOT 的格式輸出，還記得上一篇文章里的 Graphviz 嗎，Graphviz 接收 DOT 格式的輸入，然后可以直接輸出一張圖片。這樣的話，我們就可以看到抽象的 BDD 了！我感覺這應(yīng)該不是巧合，可能是 JavaBDD 的作者也使用 Graphviz，覺得很好用，就實(shí)現(xiàn)了這個(gè) printDot() 方法。JavaBDD 與 Graphviz，就可以通過這個(gè)方法結(jié)合起來了~~~

上述的步驟描述可能有些抽象，接下來舉一個(gè)例子說明。首先通過以下的代碼創(chuàng)建一個(gè) BDDFactory 對(duì)象和兩個(gè) BDD 對(duì)象：

BDDFactory B = BDDFactory.init(16, 16);
B.setVarNum(3);
BDD a = B.ithVar(0);
BDD b = B.ithVar(1);

接下來對(duì) a 和 b 執(zhí)行 or 操作，并將結(jié)果賦給一個(gè)新的 BDD 變量 c，然后用 printDot() 和 printSet() 兩種方法獲得它的信息：

BDD c = a.or(b);
c.printDot();
c.printSet();

就可以看到控制臺(tái)有了以下兩個(gè)輸出：
（如果是在 64 位電腦上用，會(huì)有錯(cuò)誤提示，但是不用管）

digraph G {
0 [shape=box, label="0", style=filled, shape=box, height=0.3, width=0.3];
1 [shape=box, label="1", style=filled, shape=box, height=0.3, width=0.3];
2 [label="0"];
2 -> 3 [style=dotted];
2 -> 1 [style=filled];
3 [label="1"];
3 -> 0 [style=dotted];
3 -> 1 [style=filled];
}
<0:0, 1:1><0:1>

其中從第一行到倒數(shù)第二行是 printDot() 的輸出，這就是一個(gè)用 DOT 語(yǔ)言描述的圖。可以用 Graphviz 自帶的 gvedit 工具渲染查看最終效果，如下圖所示。它實(shí)際上就是 BDD 變量 c，是由a 和b 相與得到的，所以實(shí)際上可以理解成布爾函數(shù) c = a or b，當(dāng) a 或 b 為真的時(shí)候 c 為真，當(dāng) a 和 b 均為假的時(shí)候c 為假。這一點(diǎn)也可以從圖中看出來。

用 DOT 語(yǔ)言描述的 BDD 的渲染結(jié)果

JavaBDD 中重要方法的探究

在這里給出一些 JavaBDD 中很重要的方法的說明，基于我的筆記進(jìn)行了一些補(bǔ)充：

public abstract BDD apply(BDD that, BDDFactory.BDDOp opr)：返回將二元運(yùn)算符 opr 應(yīng)用于兩個(gè) BDD 變量的結(jié)果。通過查看源碼，可以發(fā)現(xiàn) BDDOp 類是一個(gè)枚舉類，定義了十種二元運(yùn)算符，分別為 and（邏輯與，符號(hào)是∧），xor（邏輯異或），or（邏輯或，符號(hào)是∨），nand（邏輯與非），nor（邏輯或非），imp（邏輯蘊(yùn)含，符號(hào)是→），biimp（邏輯同或，符號(hào)是?），diff（第一個(gè)操作數(shù)和第二個(gè)操作數(shù)的非相與，相當(dāng)于 p∧?q），less（第一個(gè)操作數(shù)的非和第二個(gè)操作數(shù)相與，相當(dāng)于 ?p∧q），invimp（邏輯反蘊(yùn)含，符號(hào)是←）。

public abstract BDD ite(BDD thenBDD, BDD elseBDD)：if-then-else 運(yùn)算符。例如當(dāng)對(duì) BDD 變量 a、b 和 c 使用 a.ite(b, c) 時(shí)，如果 a 是真，那么該方法返回 b；如果a 是假，那么該方法返回 c。實(shí)際上這個(gè)方法可以轉(zhuǎn)化成普通的二元操作，相當(dāng)于布爾表達(dá)式 a·b+a’·c，用 JavaBDD 的方式表示就是 BDD result = a.and(b).or(a.not().and(c))。

public abstract BDD replace(BDDPairing pair) ： 該方法傳入的參數(shù)是一個(gè) BDDPairing 對(duì)象，該對(duì)象可以通過對(duì) BDDFactory 變量調(diào)用 makePair() 方法得到。BDDPairing 對(duì)象本質(zhì)上存放著一個(gè)或多個(gè)需要被替換的節(jié)點(diǎn)和新的節(jié)點(diǎn)，當(dāng)它作為 replace() 的參數(shù)被某個(gè) BDD 變量調(diào)用時(shí)，該方法會(huì)返回一個(gè) BDD 對(duì)象，其中所有變量都替換為 pair 定義的變量。成對(duì)的每個(gè)條目都由一個(gè)新舊變量組成。每當(dāng)在這個(gè) BDD 中找到舊的變量時(shí)，就會(huì)插入一個(gè)具有新變量的新節(jié)點(diǎn)。

public abstract BDD restrict(BDD var)：對(duì)于調(diào)用該方法的 BDD，將其節(jié)點(diǎn)中同時(shí)也包含在參數(shù) BDD 中的變量限制為常量值。如果節(jié)點(diǎn)變量包含在作為參數(shù)的 BDD 變量的正形式中，則將此 BDD 中的變量限制為常量真；如果變量包含在負(fù)形式中，則將其限制為常量假。對(duì)節(jié)點(diǎn)的約束會(huì)使得所有指向該節(jié)點(diǎn)的指針重定向。如果節(jié)點(diǎn)為真，則使之指向其 1-分支子節(jié)點(diǎn)；如果為假則使之指向其 0-分支子節(jié)點(diǎn)。

public abstract boolean equals(BDD that)：該方法用于判斷兩個(gè) BDD 變量是否相等。如果參數(shù)中的 BDD 變量等于調(diào)用該方法的 BDD 變量，則返回true，否則返回 false。

BDDDomain 類：代表 BDD 變量的域，可以將其看成是若干 BDD 變量的集合，對(duì)于描述有限狀態(tài)機(jī)及其各種狀態(tài)之間的轉(zhuǎn)化十分有用?？梢酝ㄟ^對(duì) BDDFactory 變量調(diào)用 extDomain() 得到一個(gè) BDDDomain 數(shù)組，稍后可以用于有限狀態(tài)機(jī)的遍歷和有限域上的其他操作。該函數(shù)接收一個(gè) int 類型的數(shù)組，數(shù)組的元素個(gè)數(shù)等于返回的 BDDDomain 數(shù)組的個(gè)數(shù)，設(shè)數(shù)組中某個(gè)元素的大小為 i，則其對(duì)應(yīng)的 BDDDomain 變量包含 log2(|i|) 個(gè) BDD 變量。一般情況下，會(huì)將整型數(shù)組的長(zhǎng)度設(shè)為 2 以表示變化前和變化后的兩個(gè)布爾函數(shù)，而且如果布爾函數(shù)有 n 個(gè)變量，那么整型數(shù)組的每個(gè)元素值都應(yīng)該是 2n。最后需要注意的是，為了達(dá)到更好的效果，extdomain 方法返回的 BDDDomain 中 BDD 變量的編序是交錯(cuò)的。這意味著假設(shè)域 D0 需要2 個(gè) BDD 變量 x1 和 x2，而另一個(gè)域 D1 需要 4 個(gè) BDD 變量 y1、y2、y3 和 y4，那么它們的編序?qū)⑹?x1、y1、x2、y2、y3、y4。可以對(duì) BDDFactory 變量調(diào)用 getDomain(i) 返回通過調(diào)用 extdomain() 定義的第 i 個(gè) BDDDomain。

使用 JavaBDD 表示狀態(tài)集和遷移關(guān)系

在文章開始的引言里，提到了二叉決策圖廣泛用于模型檢查，形式驗(yàn)證，優(yōu)化電路圖等方面。實(shí)際上，這些應(yīng)用都和狀態(tài)有著密不可分的關(guān)系。

在之前介紹 BDD 的時(shí)候，提到它是一種表示布爾函數(shù)的有力工具。但是狀態(tài)集和遷移關(guān)系似乎與布爾函數(shù)并沒有什么聯(lián)系，它們?nèi)绾文鼙?BDD 表示？實(shí)際上，對(duì)于一個(gè)單獨(dú)的狀態(tài)來說，它能滿足部分布爾變量，當(dāng)處于該狀態(tài)時(shí)這些布爾變量是成立的。因此可以將這個(gè)狀態(tài)看成是一個(gè)布爾函數(shù)，它等于所有滿足的布爾變量相與，再和其他不滿足的布爾變量的非相與，就得到了該狀態(tài)的布爾函數(shù)表示。

一個(gè)模型示意圖的例子

狀態(tài)集 S 對(duì)應(yīng)的 BDD

對(duì)于遷移關(guān)系的 BDD 表示，需要用到之前提到的 BDDDomain 類。因?yàn)樵撓到y(tǒng)一共有 3 個(gè)布爾變量，因此給 extDomain 方法傳入一個(gè)包含兩個(gè) int 變量的 int 數(shù)組，每個(gè) int 的值都是 2^3 也就是 8。這樣會(huì)生成兩個(gè) BDDDomain 變量，每個(gè)都包含 3 個(gè)BDD，且為了更高的效率，它們的編序是交替的，第一個(gè) BDDDomain 變量的編序是 0，2，4，第二個(gè)的編序是 1，3，5。將它們分別看成遷移前和遷移后對(duì)應(yīng)的狀態(tài)，遷移關(guān)系的布爾函數(shù)就是將遷移前后狀態(tài)滿足的狀態(tài)相與。以之前的模型示意圖中的遷移關(guān)系 S0—>S1 為例，其布爾函數(shù)為 a∧b∧?c∧?a’∧b’∧c’，同理，總遷移關(guān)系的布爾函數(shù)就是所有單獨(dú)遷移關(guān)系的布爾函數(shù)相加，對(duì)應(yīng)到邏輯關(guān)系中就是或操作。在這個(gè)例子中，由于有 4 個(gè)遷移關(guān)系，因此總遷移關(guān)系可以表示成它們相與，也就是 (a∧b∧?c∧?a’∧b’∧c’) ∨ (a∧b∧?c∧?a’∧?b’∧c’) ∨ (?a∧b∧c∧?a’∧?b’∧c’) ∨ (?a∧?b∧c∧?a’∧?b’∧c’)。這實(shí)際上也是一個(gè)布爾函數(shù)，它對(duì)應(yīng)的 BDD 如下圖所示，其中的 0、2、4 節(jié)點(diǎn)對(duì)應(yīng)著布爾變量 a、b、c，而 1、3、5 節(jié)點(diǎn)則對(duì)應(yīng)著布爾變量 a’、b’、c’。

總遷移關(guān)系對(duì)應(yīng)的 BDD

可以看到，雖然到終點(diǎn) 1 節(jié)點(diǎn)的路徑只有兩條，但是每條路徑都包含著兩種情況，因此最終有 4 種使總遷移關(guān)系的布爾函數(shù)為真的情況，這一點(diǎn)從上面的布爾函數(shù)也可以看出來。

OK，這篇文章內(nèi)容就先寫到這里了，下一篇會(huì)進(jìn)一步介紹 JavaBDD 的應(yīng)用——布爾表達(dá)式的運(yùn)算。以布爾函數(shù) result = (A or C)and(B or A)為例，如何利用 JavaBDD 瞬間得到它的真值表？聰明的同學(xué)應(yīng)該能猜到了，不就是從根節(jié)點(diǎn)走完每條路徑嘛！

欲知后事如何，且聽下回分解~~~

感謝大家的閱讀，如果覺得這篇文章很有幫助，贊賞支持一波啊~~~
金額不重要，態(tài)度是關(guān)鍵???