前言第二部分 邏輯表示方式以及處理算法
Boolean Representation via BDDs and SATBDD Binary Decision DiagramsBDD是什么 。 Binary Decision Diagrams 二進制決策圖
二進制決策圖是表示和操作布爾邏輯的最通用和有用的數據結構之一 。
那么二進制決策圖長什么樣呢 。



如圖所示，就是樹狀圖，每一個分支對應一個輸入的確定，從而確定輸出，這也表示了所有狀態下輸入和輸出的對應關系 。 但是呢，這樣的表示方法在輸入增加時，樹狀圖層指數增長，所以我們顯然需要一些方法來簡化 。
忽略節點：當某一情況下的某一輸入對結果不發生影響時，我們忽略這一輸入對應的兩個分支 。 如圖所示



共用節點：共用節點存在兩種類型 。 第一種是由于輸出一定是0或者1，我們只需要將所有分支的最終輸出指向0或者1，就可以減少輸出的分支 。 第二種是對于多個輸入輸出對應關系，在經過一些0/1簡化后，可能存在相同狀況，即從某一分支開始，之后的部分邏輯關系完全一致，我們將這一部分邏輯關系用同一個樹狀圖表示，僅僅是前置的輸入指向不同 。 又或者是不同對應關系在最初的部分邏輯關系中存在相同情況，我們同樣可以將這一部分邏輯關系用同一個樹狀圖表示，僅僅是輸出指向不同節點 。
接下來的圖片分別對應第一種類型和第二種類型的兩種情況






除此之外，輸入判斷的先后會對整個樹狀圖的大小有極其重要的影響 。
如圖所示，當我們先判斷a_1,a_2,a_3…..，然后判斷b_1,b_2,b_3….我們會發現，一直判斷到b_1才會出現第一個可能的輸出，然而在n次判斷后，這一次判斷的分支會存在2^（n+1），毫無疑問，這是一個巨大的工程量 。 而當我們先判斷a_1b_1時，無疑會減少一個巨大的分支 。






SAT satisfiability對于一個邏輯關系，我們往往需要的是該邏輯關系成立，比如network repair中z = ! (F xor G)，我們特意在最后結尾添加非運算，使得真才是我們期待的結果 。 這既符合現實邏輯上的關系，又符合電子邏輯關系 。
所以，對一個系統來說，有時候我們并不期望得到所有的結果，只需要知道這件事情在某種條件下能夠成立，我們去盡力滿足這個條件即可 。 因此，SAT被提了出來 。
在一個概念被提出之后，我們需要做的就是找到一個方法實現這個概念 。 首先我們提出一個表達方式CNF Conjunctive Normal Form，連接的一般方式 。 其形式是XXX+XXXX+XXXX，語言描述就是多個命題的和 。
為什么選擇和的形式呢 。
因為or邏輯中有一出一，我們只需要判斷或者找到其中一個命題成立，這整個邏輯就成立 。 除此之外，每個命題都可以轉化成和的形式 。 AB可以轉化成^(^A+^B)這是基于雙重否定消除（非非為本身）以及的摩根定律（^(AB) = ^A+^B），(A+B)C 可以轉化成AC+BC 這是根據分配率得到 。
我們用和的形式表示所有邏輯門（為了簡化表示，所以都轉化成AB的形式）
z=(x) [^x + z][x + ^z]

猜你喜歡

• 西安火車站到北站及返程線路建議
• 初二/八年級期末禁毒知識考試參考答案 青驕第二課堂怎么答題
• 青驕第二課堂2020全國青少年禁毒知識競賽答題中學組題庫答案
• office2016安裝，激活，玩轉破解版
• Microsoft Visual C++ 6.0下載地址及安裝教程
• 安卓手機上Java模擬器的安裝與使用
• Photoshop CC 2018安裝破解教程
• 茶樣女子（二)，杭州龍井茶
• 如何去安慰人
• 安溪茶文化，苦丁茶能減肥嗎