這篇文章會介紹一種能高效操作 BDD（Binary Decision Diagrams，二叉決策圖）和布爾函數的數據結構 —— JavaBDD谷婆。二叉決策圖廣泛用于模型檢查蛾绎，形式驗證涵亏，優(yōu)化電路圖等方面。同時发乔，該數據結構也可以和上一篇文章中介紹的 Graphviz 聯系起來。
提示：本篇內容略多雪猪，但如果堅持讀完栏尚，一定會有收獲 : )
BDD與布爾函數
畢設剛開始不久，指導老師讓我學習一下 JavaBDD 庫只恨。之前我也沒聽說過這玩意兒译仗，在網上一查，看到 BDD 的意思是 Behavior Driven Development官觅，行為驅動開發(fā)纵菌。仔細了解以后，感覺和畢設題目 “ 狀態(tài)機自動生成與圖形化仿真系統研究與實現 ” 沒有半毛錢的關系休涤。（后來才知道行為驅動開發(fā)在近年來的熱度在逐漸上漲咱圆，是一種比較新的思想，感興趣的同學可以自行了解一下）
于是重新又搜索了幾次功氨，重要發(fā)現旮旯角里的一個網站 http://javabdd.sourceforge.net/ 提到了 JavaBDD 這個庫序苏，原來它就是 JavaBDD 的官網，古老而簡陋的網站疑故，信息相當少杠览，幾句話就介紹完了。官網還給出了一個介紹 BDD 的頁面纵势，然而打開顯示 404踱阿。拜托，這到底是個啥東西钦铁！不得已只好各種查找软舌，最后在維基百科上看到了下面的定義：
BDD 是用于表示布爾函數的數據結構。布爾函數可以表示為有根牛曹，有向佛点，非循環(huán)圖，它由若干決策節(jié)點和終端節(jié)點組成。有兩種類型的終端節(jié)點稱為0終端和1終端超营。每個決策節(jié)點都用布爾變量標記鸳玩，并有兩個子節(jié)點，稱為低子節(jié)點和高子節(jié)點演闭。從節(jié)點到低（或高）子節(jié)點的邊表示0（分別為1）的賦值不跟。如果不同的變量在來自根的所有路徑上以相同的順序出現，則這種BDD稱為“有序”米碰。如果將以下兩個規(guī)則應用于其圖表窝革，則稱BDD為“約減”。
- 合并任何同構子圖吕座。
- 消除兩個孩子節(jié)點同構的任何節(jié)點虐译。
在流行的用法中，術語 BDD 幾乎總是指減少有序二進制決策圖（文獻中的ROBDD吴趴，當需要強調排序和減少方面時使用）漆诽。ROBDD的優(yōu)點在于它對于特定函數和變量順序是規(guī)范的（唯一的）。該屬性使其在功能等價檢查和其他操作（如功能技術映射）中非常有用史侣。
從根節(jié)點到1終端的路徑表示所表示的布爾函數為真的（可能是部分的）變量賦值拴泌。當路徑從節(jié)點下降到低（或高）子節(jié)點時，該節(jié)點的變量被分配為0（分別為1）惊橱。
我估計維基百科給出的定義沒人看??能理解的同學蚪腐，我給你點個大大的贊??至少我當時是懵逼的。不過還好税朴，維基百科接下來給出了例子回季，這次再看，應該能理解一些了：
請各位仔細看左下角的布爾函數 f (x1, x2, x3)泡一，這是一個典型的布爾函數，包括三個布爾變量 x1, x2, x3觅廓。該函數的真值表在上圖中間鼻忠，里面很清晰的注明了布爾變量和布爾函數值的對應關系。
再看左邊的類似二叉樹的圖杈绸，根節(jié)點對應著第一個布爾變量 x1帖蔓，第二層和第三層的節(jié)點對應著第二個和第三個布爾變量。這些代表布爾變量的圓形的非葉子節(jié)點也就是上面的定義中的決策節(jié)點瞳脓，而方形的葉子節(jié)點只有 0 和 1 兩個取值塑娇，代表著布爾函數的值，就是上面的定義中的終端節(jié)點劫侧。最后埋酬，對于一個決策節(jié)點來說哨啃，都有兩條邊，一虛一實写妥，分別表示該節(jié)點代表的布爾變量的值取假（0）或取真（1）拳球。
那么這個類似二叉樹的東西（二叉決策樹）和布爾函數 f (x1, x2, x3) 有什么關系呢？仔細觀察可以發(fā)現耳标，從根節(jié)點到任意一個葉子節(jié)點的路徑醇坝，其實對應著三個布爾變量的取值和布爾函數的取值，而這些取值和真值表是對應的次坡。比如我們看到真值表的第一行，x1, x2, x3 都為零画畅，對應的就是根節(jié)點 x1 走左邊的虛邊（因為虛邊對應的取值是 0砸琅，實邊對應的取值是 1），到達第二個節(jié)點 x2 后轴踱，繼續(xù)走虛的那條邊邊症脂，到達第三個節(jié)點 x3 后，仍然走左邊的虛邊淫僻，就到達了為 1 的葉子節(jié)點诱篷，意味著布爾函數值為 1（也就是布爾函數結果為真）。而真值表第一行 f 的取值也是 1雳灵。再比如讓 x1=0, x2=1, x3=0棕所，那么從根節(jié)點開始先往左，再往右悯辙，再往左琳省，到達了為 0 的葉子節(jié)點，意味著布爾函數為假躲撰，真值表第三行的結果確認了這一點针贬。
所以我們可以發(fā)現，實際上左邊的二叉決策樹使用了另外一種方式表示了布爾函數真值表的信息拢蛋！也就是說桦他，一個布爾函數是可以由二叉決策樹來表示的！（感覺真的很神奇谆棱，就像以前上學第一次聽到老師講數形結合的時候快压，老師在黑板上列了一個 y 關于 x 的函數，然后把它在直角坐標系中畫了出來础锐，感覺這種數與形的轉換很有意思）
那么實際上嗓节，左邊的圖是可以進一步壓縮的。為啥要壓縮呢皆警，很簡單拦宣，因為二叉決策樹中的節(jié)點數目隨著布爾變量的增加會以指數方式增大，2 個變量對應的節(jié)點數是 1+2，3 個變量對應的節(jié)點數是 1+2+4鸵隧，4 個變量對應的節(jié)點數是 1+2+4+8 ... 那么 x 個變量對應的節(jié)點數是 2^x - 1 這么多３衤蕖（注：這個地方不太嚴謹，因為不同的布爾函數對應的二叉決策樹豆瘫，每層節(jié)點數并不一定是按 1, 2, 4, 8... 這樣的規(guī)律增加的珊蟀，這里為了簡化就這么寫，但不管怎樣外驱，如果不壓縮的話育灸，節(jié)點數目的增長速度肯定是越來越快的 : ) 大家理解一下）
你可能會說，那咋辦嘛昵宇，我不知道怎么壓縮磅崭。這個時候，維基百科的定義就發(fā)揮作用了瓦哎！請往上翻到定義那里砸喻，將粗體定義再次閱讀一遍，相信會有新的收獲 (??????)??
定義中說 BDD 一般指的都是 ROBDD（Reduced Ordered BDD蒋譬，約減且有序的BDD）割岛，也就是說 BDD 默認都是約減的和有序的。約減需要滿足兩個條件：合并任何同構子圖犯助，以及消除兩個孩子節(jié)點同構的任何節(jié)點癣漆。這兩個條件比較繞，翻譯成更通俗的語言就是：把兩個一模一樣的部分合并到一塊也切，以及對于任意兩個節(jié)點扑媚，如果它們左孩子一樣，右孩子也一樣（注意雷恃，這里沒說左右孩子是一樣的疆股。事實上，如果左右孩子都一樣倒槐，說明這個節(jié)點不論取真還是假都不會對結果有一些旬痹，也就是說這個節(jié)點是冗余的，可以刪掉）讨越，那么就刪除其中一個節(jié)點（或者說把這兩個節(jié)點合并到一起）两残。有序則需要滿足，從根節(jié)點出發(fā)的所有路徑上把跨，布爾變量出現的順序都是相同的人弓。這一段話如果看不懂，不用急着逐，當作了解就可以崔赌，如果之后接觸 BDD 比較多意蛀，這些概念到時候順其自然就理解了。
接下來再次翻到上面的圖健芭，看到最右邊县钥，就是布爾函數 f (x1, x2, x3) 對應的 BDD（或者說是 ROBDD）了。仔細觀察它和左邊的二叉決策樹的區(qū)別慈迈，可以發(fā)現有不少變化：
- 二叉決策樹中的節(jié)點若贮，虛邊都在左側，實邊都在右側痒留，但 BDD 中不一定這樣谴麦，而且在虛邊都標記了 0，實邊都標記了 1伸头，顯得更清晰了细移；
- 終端節(jié)點只有兩個了，分別為 0 和 1熊锭。這是約減過的結果，因為布爾函數最后的取值只有這兩種情況雪侥，因此之前有很多冗余的 0 節(jié)點和 1 節(jié)點碗殷；
- 對應 x1 節(jié)點取 1 的這一側，x2 節(jié)點直接就指向終端節(jié)點了速缨，沒有了 x3 節(jié)點锌妻。這也是約減過的結果，在二叉決策樹中可以看到旬牲，有兩個 x3 節(jié)點不管取真還是假仿粹，到達的終端節(jié)點都一樣，這意味著它們是冗余的原茅，可以刪去吭历，而指向 x3 節(jié)點的邊只需要直接指向 x3 節(jié)點的孩子即可；
- 有多個邊可以同時指向一個節(jié)點擂橘，比如終端節(jié)點就是這樣。實際上對于 BDD 來說這是沒問題的通贞，這實現了節(jié)點的復用朗若，進一步壓縮了節(jié)點數。
因此昌罩，在維基百科的定義里才會說哭懈，布爾函數可以表示為有根，有向茎用，非循環(huán)圖遣总，它由若干決策節(jié)點和終端節(jié)點組成睬罗。這也就是說 BDD（或者說ROBDD）本質是一個圖，且有根彤避，有向傅物，非循環(huán)，可以用來表示布爾函數琉预。之前說了這么多董饰，也就是想闡明布爾函數和 BDD 之間的轉換關系。那么知道了這個有什么用呢圆米？當然有用卒暂！它為我們提供了一種全新的解決布爾函數相關問題的思路！就像之前用數形結合法解題娄帖，有時候你看著函數就是不知道怎么做題也祠，但是當你把他在直角坐標系中畫出來，你可能瞬間就明白了答案是什么近速。布爾函數也是這樣诈嘿。當涉及到大型、復雜的布爾函數時削葱，我們可以將其轉換成圖的形式（BDD）奖亚，然后使用圖論相關的知識或者其他的性質來高效的解決問題。就是這么厲害~~~
JavaBDD庫與一篇論文
終于要開始寫 JavaBDD 這個庫了析砸。昔字。。它是由美國斯坦福大學的 John Whaley 領導的團隊設計開發(fā)的開源代碼庫首繁，采用 Java 開發(fā)作郭。這個庫相當優(yōu)秀，在此膜拜一下作者弦疮，但是還是得吐槽一下夹攒，為什么文檔這么爛！９彝薄芹助！是的，這個庫幾乎就是沒有文檔闲先，官網中唯一給出的只有 API 文檔 http://javabdd.sourceforge.net/apidocs/index.html状土，各位可以感受一下它的酸爽。網上關于 JavaBDD 的資料也極少伺糠，可能是因為用的人不多吧蒙谓。。训桶。
我查了很久也沒有找到任何的資料累驮，倒是找到了 John Whaley 在 ResearchGate 上介紹 JavaBDD 的一篇論文酣倾，但是無法查看和下載。谤专。躁锡。還有就是 Stackoverflow 上的這個回答≈檬蹋可以說我是根據這個回答映之，然后對照著 API 文檔和源碼各種嘗試、失敗蜡坊、重復才一點點知道 JavaBDD 是怎么使用的杠输。從這一點上來說，JavaBDD 真的很坑秕衙。
在這段探索的過程中蠢甲，我做了一些 JavaBDD 的使用筆記，比較簡單据忘，就先不發(fā)出來了鹦牛，如果有同學需要可以在文章底部留言。同時在搜集資料期間勇吊，也發(fā)現了一些和 BDD 相關的有些用的資料能岩，分別是一個講座 PPT OBDD原理及其應用 以及知網的一篇論文《二元判斷圖BDD及其JAVA實現的應用與研究》。
這里對于這個論文萧福，我得重點說幾句。首先它對我的畢設幫助還是很大的辈赋，里面也有一點使用 JavaBDD 的代碼鲫忍，是我探索過程中很好的參考。但是我在之后做畢設的過程中發(fā)現钥屈，這篇論文相當有意思悟民。首先看它的目錄如下圖：
不知道大家還記不記得 JavaBDD 庫的官網，如果有同學打開過篷就，應該記得在為數不多的幾句介紹中有這樣一句：“有關BDD數據結構的精彩概述射亏，請參閱Henrik Reif Andersen的這套 講義〗咭担”然而這個鏈接的打不開的智润。后來我嘗試著搜索 “ Henrik Reif Andersen Binary Decision Diagrams ”，發(fā)現第一個結果正是這篇講義的 PDF未辆。當時我很激動窟绷，認為找到寶了，雖然是全英文的咐柜，但是也能大致理解其中的內容。但是當我看了一部分以后，感覺似乎內容有些似曾相識康愤，再一看論文针饥，發(fā)現第二章的內容基本就是從講義里摘取的，圖片都是一樣的雇寇，文字就是從英文翻譯成中文，然后再加上了少量自己的東西。
還沒完病曾，在這篇論文的第 4.3.2 節(jié)的第一段中，有一句這樣的話：
當時我對論文中的有些地方不太懂涉瘾，但又不知道在哪里找資料知态，突然看到了這句話，就想著找到這本書來看看立叛，或許能得到一下啟發(fā)负敏。但是這個書已經很老了，圖書館里也沒有秘蛇，我又不想買???經過多方查找其做，在 這個網站 發(fā)現可以在線閱讀。在頁面右邊點擊 “圖書館文獻傳遞”赁还，登錄后就可以看了妖泄，從 103 頁開始，論文中第三章的內容和書中基本是重復的艘策。同時蹈胡，論文第 4.2 節(jié)中的例子也是套用的 Henrik Reif Andersen 的講義中的內容。
可以說朋蔫，整篇論文罚渐，除了第一章和部分第四章的內容是作者寫的，論文的核心第二三章絕大部分都是來自別人的成果驯妄。作者除了提供背景說明荷并、一些分析以及一些 JavaBDD 的代碼之外，其實做的很有限青扔。作為碩士畢業(yè)論文源织，這樣的情況其實是不應該發(fā)生的。希望看到這里的同學能夠以此為鑒微猖。
接下來開始真正的介紹 JavaBDD 的用法了谈息！
（我怎么感覺都要寫完了才開始介紹。凛剥。黎茎。）
JavaBDD 庫能夠方便地操作 BDD 并進行一些復合操作。在 JavaBDD 中創(chuàng)建 BDD 需要用到 BDDFactory 類当悔，首先需要通過 init() 方法初始化一個BDDFactory 對象傅瞻。該方法接收兩個 int 類型的參數踢代，分別表示初始節(jié)點表大小和操作緩存大小。
接下來需要對該 BDDFactory 對象調用 setVarNum() 方法嗅骄，接收一個 int 類型的參數胳挎，設置需要使用的 BDD 變量個數。接下來就可以對 BDDFactory 對象調用 ithVar() 方法創(chuàng)建表示第 i 個變量的BDD 變量溺森∧脚溃可以將返回值看成一個節(jié)點，子節(jié)點為 true 和 false屏积。除此之外医窿，請求的變量必須在setvarnum 定義的范圍內。
當創(chuàng)建了若干變量之后炊林，就可以調用 and()姥卢、or() 等方法進行操作了。如果要獲得結果BDD 的詳情渣聚，主要有兩種方式独榴，一是調用 printDot() 方法以 DOT 方式打印這個 BDD，二是調用 printSet() 方法奕枝，打印此 BDD 指定的真值分配集合棺榔。注意，這里的 printDot() 方法非常重要隘道，正是由于這個方法症歇，BDD 才能以 DOT 的格式輸出，還記得上一篇文章里的 Graphviz 嗎谭梗，Graphviz 接收 DOT 格式的輸入当船，然后可以直接輸出一張圖片。這樣的話默辨，我們就可以看到抽象的 BDD 了！我感覺這應該不是巧合苍息，可能是 JavaBDD 的作者也使用 Graphviz缩幸，覺得很好用，就實現了這個 printDot() 方法竞思。JavaBDD 與 Graphviz表谊，就可以通過這個方法結合起來了~~~
上述的步驟描述可能有些抽象，接下來舉一個例子說明盖喷。首先通過以下的代碼創(chuàng)建一個 BDDFactory 對象和兩個 BDD 對象：
BDDFactory B = BDDFactory.init(16, 16);
B.setVarNum(3);
BDD a = B.ithVar(0);
BDD b = B.ithVar(1);
接下來對 a 和 b 執(zhí)行 or 操作爆办，并將結果賦給一個新的 BDD 變量 c，然后用 printDot() 和 printSet() 兩種方法獲得它的信息：
BDD c = a.or(b);
c.printDot();
c.printSet();
就可以看到控制臺有了以下兩個輸出：
（如果是在 64 位電腦上用课梳，會有錯誤提示距辆，但是不用管）
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>
其中從第一行到倒數第二行是 printDot() 的輸出余佃，這就是一個用 DOT 語言描述的圖】缢悖可以用 Graphviz 自帶的 gvedit 工具渲染查看最終效果爆土，如下圖所示。它實際上就是 BDD 變量 c诸蚕，是由a 和b 相與得到的步势，所以實際上可以理解成布爾函數 c = a or b，當 a 或 b 為真的時候 c 為真背犯，當 a 和 b 均為假的時候c 為假坏瘩。這一點也可以從圖中看出來。
接下來看到第二個輸出 <0:0, 1:1><0:1>漠魏，仔細觀察可以發(fā)現倔矾，每個尖括號都代表著一種真值分配的情況，每個冒號前的數字代表著 BDD 變量的索引蛉幸，冒號后的數字代表著取值情況破讨。這個輸出就包含著兩種情況，第一種情況是 0 節(jié)點為假奕纫，1 節(jié)點為真提陶；第二種情況是 0 節(jié)點為真。這兩種情況就是使得布爾函數為真的所有情況匹层。
JavaBDD 中重要方法的探究
在這里給出一些 JavaBDD 中很重要的方法的說明隙笆，基于我的筆記進行了一些補充：
public abstract BDD apply(BDD that, BDDFactory.BDDOp opr)：返回將二元運算符 opr 應用于兩個 BDD 變量的結果。通過查看源碼升筏，可以發(fā)現 BDDOp 類是一個枚舉類撑柔，定義了十種二元運算符，分別為 and（邏輯與您访，符號是∧）铅忿，xor（邏輯異或），or（邏輯或灵汪，符號是∨）檀训，nand（邏輯與非），nor（邏輯或非）享言，imp（邏輯蘊含峻凫，符號是→），biimp（邏輯同或览露，符號是?）荧琼，diff（第一個操作數和第二個操作數的非相與，相當于 p∧?q），less（第一個操作數的非和第二個操作數相與命锄，相當于 ?p∧q）堰乔，invimp（邏輯反蘊含，符號是←）累舷。
public abstract BDD ite(BDD thenBDD, BDD elseBDD)：if-then-else 運算符浩考。例如當對 BDD 變量 a、b 和 c 使用 a.ite(b, c) 時被盈，如果 a 是真析孽，那么該方法返回 b；如果a 是假只怎，那么該方法返回 c袜瞬。實際上這個方法可以轉化成普通的二元操作，相當于布爾表達式 a·b+a’·c身堡，用 JavaBDD 的方式表示就是 BDD result = a.and(b).or(a.not().and(c))邓尤。
public abstract BDD replace(BDDPairing pair) ： 該方法傳入的參數是一個 BDDPairing 對象，該對象可以通過對 BDDFactory 變量調用 makePair() 方法得到贴谎。BDDPairing 對象本質上存放著一個或多個需要被替換的節(jié)點和新的節(jié)點汞扎，當它作為 replace() 的參數被某個 BDD 變量調用時，該方法會返回一個 BDD 對象擅这，其中所有變量都替換為 pair 定義的變量澈魄。成對的每個條目都由一個新舊變量組成。每當在這個 BDD 中找到舊的變量時仲翎，就會插入一個具有新變量的新節(jié)點痹扇。
public abstract BDD restrict(BDD var)：對于調用該方法的 BDD，將其節(jié)點中同時也包含在參數 BDD 中的變量限制為常量值溯香。如果節(jié)點變量包含在作為參數的 BDD 變量的正形式中鲫构，則將此 BDD 中的變量限制為常量真；如果變量包含在負形式中玫坛，則將其限制為常量假结笨。對節(jié)點的約束會使得所有指向該節(jié)點的指針重定向。如果節(jié)點為真湿镀，則使之指向其 1-分支子節(jié)點炕吸；如果為假則使之指向其 0-分支子節(jié)點。
public abstract boolean equals(BDD that)：該方法用于判斷兩個 BDD 變量是否相等肠骆。如果參數中的 BDD 變量等于調用該方法的 BDD 變量，則返回true塞耕，否則返回 false蚀腿。
BDDDomain 類：代表 BDD 變量的域，可以將其看成是若干 BDD 變量的集合，對于描述有限狀態(tài)機及其各種狀態(tài)之間的轉化十分有用莉钙±啵可以通過對 BDDFactory 變量調用 extDomain() 得到一個 BDDDomain 數組，稍后可以用于有限狀態(tài)機的遍歷和有限域上的其他操作磁玉。該函數接收一個 int 類型的數組停忿，數組的元素個數等于返回的 BDDDomain 數組的個數，設數組中某個元素的大小為 i蚊伞，則其對應的 BDDDomain 變量包含 log2(|i|) 個 BDD 變量席赂。一般情況下，會將整型數組的長度設為 2 以表示變化前和變化后的兩個布爾函數时迫，而且如果布爾函數有 n 個變量颅停，那么整型數組的每個元素值都應該是 2n。最后需要注意的是掠拳，為了達到更好的效果癞揉，extdomain 方法返回的 BDDDomain 中 BDD 變量的編序是交錯的。這意味著假設域 D0 需要2 個 BDD 變量 x1 和 x2溺欧，而另一個域 D1 需要 4 個 BDD 變量 y1喊熟、y2、y3 和 y4姐刁，那么它們的編序將是 x1芥牌、y1、x2龙填、y2胳泉、y3、y4岩遗∩壬蹋可以對 BDDFactory 變量調用 getDomain(i) 返回通過調用 extdomain() 定義的第 i 個 BDDDomain。
使用 JavaBDD 表示狀態(tài)集和遷移關系
在文章開始的引言里宿礁，提到了二叉決策圖廣泛用于模型檢查案铺，形式驗證，優(yōu)化電路圖等方面梆靖。實際上控汉，這些應用都和狀態(tài)有著密不可分的關系。
在之前介紹 BDD 的時候返吻，提到它是一種表示布爾函數的有力工具姑子。但是狀態(tài)集和遷移關系似乎與布爾函數并沒有什么聯系，它們如何能被 BDD 表示测僵？實際上街佑，對于一個單獨的狀態(tài)來說谢翎，它能滿足部分布爾變量，當處于該狀態(tài)時這些布爾變量是成立的沐旨。因此可以將這個狀態(tài)看成是一個布爾函數森逮，它等于所有滿足的布爾變量相與，再和其他不滿足的布爾變量的非相與磁携，就得到了該狀態(tài)的布爾函數表示褒侧。
以上圖為例，該系統包含的布爾變量為 a谊迄、b 和 c闷供，狀態(tài)集為 S0、S1 和 S2（表示包含這三個狀態(tài)）鳞上，遷移關系（也就是狀態(tài)之間的轉換關系）也很清晰这吻。對于 S0，滿足 a 和 b篙议，不滿足 c唾糯，也就是說在這個狀態(tài)下，布爾變量 a 和 b 為真鬼贱，c 為假移怯。如果要用 BDD 表示該狀態(tài)，就應該是 S0 = a∧b∧?c这难。同理舟误，S1 = ?a∧b∧c，S2 = ?a∧?b∧c姻乓。接下來如果要表示狀態(tài)集嵌溢，就需要將所有的單個狀態(tài)的布爾函數相加，對應到邏輯關系中就是或操作蹋岩。在這個例子中赖草，狀態(tài)集 S = (a∧b∧?c)∨(?a∧b∧c)∨(?a∧?b∧c)。在 JavaBDD 中剪个，需要將與操作轉換成 and 方法秧骑，或操作轉換成 or 方法，邏輯非轉化成 not 方法扣囊。最終 S 對應的 BDD 如下圖所示乎折，其中的 0、1 和 2 節(jié)點對應著布爾變量 a侵歇、b 和 c骂澄。
仔細觀察可以發(fā)現，在這個 BDD 中惕虑，到達終點 1 節(jié)點的路徑有兩條坟冲，但是實際上包含著三種情況士修。在 0 節(jié)點為假、2 節(jié)點為真的情況下樱衷，1 節(jié)點為真或為假都是可以的，BDD 沒有將這兩種情況分開表示酒唉，而是通過合并它們減少了所需的空間矩桂。這三種情況也對應著狀態(tài)集 S 的布爾函數中被邏輯與∨分開的三部分。因此痪伦，布爾函數的組成部分和其BDD 中到達終點1 節(jié)點的路徑是可以對應上的侄榴。
對于遷移關系的 BDD 表示，需要用到之前提到的 BDDDomain 類网沾。因為該系統一共有 3 個布爾變量癞蚕，因此給 extDomain 方法傳入一個包含兩個 int 變量的 int 數組，每個 int 的值都是 2^3 也就是 8辉哥。這樣會生成兩個 BDDDomain 變量桦山，每個都包含 3 個BDD，且為了更高的效率醋旦，它們的編序是交替的恒水，第一個 BDDDomain 變量的編序是 0，2饲齐，4钉凌，第二個的編序是 1，3捂人，5御雕。將它們分別看成遷移前和遷移后對應的狀態(tài)，遷移關系的布爾函數就是將遷移前后狀態(tài)滿足的狀態(tài)相與滥搭。以之前的模型示意圖中的遷移關系 S0—>S1 為例酸纲，其布爾函數為 a∧b∧?c∧?a’∧b’∧c’，同理论熙，總遷移關系的布爾函數就是所有單獨遷移關系的布爾函數相加福青，對應到邏輯關系中就是或操作。在這個例子中脓诡，由于有 4 個遷移關系无午，因此總遷移關系可以表示成它們相與，也就是 (a∧b∧?c∧?a’∧b’∧c’) ∨ (a∧b∧?c∧?a’∧?b’∧c’) ∨ (?a∧b∧c∧?a’∧?b’∧c’) ∨ (?a∧?b∧c∧?a’∧?b’∧c’)祝谚。這實際上也是一個布爾函數宪迟，它對應的 BDD 如下圖所示，其中的 0交惯、2次泽、4 節(jié)點對應著布爾變量 a穿仪、b、c意荤，而 1啊片、3、5 節(jié)點則對應著布爾變量 a’玖像、b’紫谷、c’。
可以看到捐寥，雖然到終點 1 節(jié)點的路徑只有兩條笤昨，但是每條路徑都包含著兩種情況，因此最終有 4 種使總遷移關系的布爾函數為真的情況握恳，這一點從上面的布爾函數也可以看出來瞒窒。
OK，這篇文章內容就先寫到這里了乡洼，下一篇會進一步介紹 JavaBDD 的應用——布爾表達式的運算崇裁。以布爾函數 result = (A or C)and(B or A)為例，如何利用 JavaBDD 瞬間得到它的真值表束昵？聰明的同學應該能猜到了寇壳，不就是從根節(jié)點走完每條路徑嘛！
欲知后事如何妻怎，且聽下回分解~~~
感謝大家的閱讀壳炎，如果覺得這篇文章很有幫助，贊賞支持一波啊~~~
金額不重要逼侦，態(tài)度是關鍵???
