跳轉到

3.2 二分決策圖 BDD#

概念說明#

二分決策圖（Binary Decision Diagram, BDD）是布林函數的圖表示：每個內部節點代表一個變數，有兩條出邊分別對應「該變數 = 0」與「= 1」的子函數；兩個終端節點 0 與 1 代表常數。當變數在全網路中採用固定順序（ordered）且同構節點合併（reduced）時，得到 ROBDD——每個布林函數在此順序下有唯一正規形。唯一性帶來兩個巨大好處：(1) 等效檢查只是比較根節點指標，O(1)；(2) 所有布林運算（AND/OR/NOT/XOR）都可由 Shannon 展開遞迴完成，時間約 O(|B₁|·|B₂|)。

BDD 由 Bryant 於 1986 年的論文奠定，此後 20 年成為 EDA 驗證與合成的主力資料結構，被廣泛用於組合等效檢查、符號模擬、模型檢查的集合表示等。BDD 的弱點是大小對變數順序極度敏感：加法器等函數在好順序下是線性，壞順序下是指數級。因此變數重排（reordering，如 sifting 演算法）成為 BDD 套件的必備功能。

一個經典例子：函數 f = (a₁∧b₁) ∨ (¬a₁∧(a₂∧b₂ ∨ ¬a₂∧a₃)) 之類的位元比較，某些順序下節點數是線性、某些順序下爆炸。實務上「交錯輸入變數」（a₁ b₁ a₂ b₂ ...）通常是加法器類電路的好順序。

演算法步驟（以 Shannon 展開建構並化簡 BDD）#

  1. 選定變數順序，如 x₁ < x₂ < ... < xₙ。
  2. 遞迴展開：f = ¬x·f|x=0 ∨ x·f|x=1，每層處理順序中的下一個變數。
  3. 終止條件：常數函數回傳 0/1 節點；所有變數已處理則依真值回傳終端。
  4. 化簡規則：(a) 同構子樹共用同一節點（雜湊表查重）；(b) 兩條出邊指向同一子節點的節點刪除（冗餘節點）。
  5. 運算（如 apply(g1, op, g2)）用 memoization：以 (節點對, 運算) 為鍵快取結果，避免重複展開。

Python 程式碼範例#

以下實作一個簡化 ROBDD：以 (var, low, high) 表示節點，用字典做唯一性表，示範建構、合併化簡與等效檢查。

class BDD:
    def __init__(self):
        self.unique = {}          # (var, low, high) -> id
        self.nodes = [None, None] # 0, 1 為終端
        self.cache = {}           # apply 運算的 memo

    def mk(self, var, low, high):
        if low == high:                    # 冗餘節點化簡
            return low
        key = (var, low, high)
        if key not in self.unique:
            self.unique[key] = len(self.nodes)
            self.nodes.append(key)
        return self.unique[key]

    def var_node(self, v):
        return self.mk(v, 0, 1)

    def apply(self, op, u, v):
        """op: 函數，作用於兩布林值。遞迴 Shannon 展開"""
        if u in (0, 1) and v in (0, 1):
            return int(op(bool(u), bool(v)))
        key = (op.__name__, u, v)
        if key in self.cache:
            return self.cache[key]
        top = min(self.top_var(u), self.top_var(v))
        u0, u1 = self.cofactor(u, top)
        v0, v1 = self.cofactor(v, top)
        low  = self.apply(op, u0, v0)
        high = self.apply(op, u1, v1)
        res = self.mk(top, low, high)
        self.cache[key] = res
        return res

    def top_var(self, u):
        if u in (0, 1):
            return float('inf')
        return self.nodes[u][0]

    def cofactor(self, u, var):
        """對變數 var 取 cofactor，回傳 (low, high) 子節點"""
        if u in (0, 1) or self.top_var(u) != var:
            return u, u
        _, low, high = self.nodes[u]
        return low, high

    def size(self, u):
        seen, stack = set(), [u]
        while stack:
            n = stack.pop()
            if n in (0, 1) or n in seen:
                continue
            seen.add(n)
            stack.extend(self.nodes[n][1:])
        return len(seen)

def build_and_eval():
    bdd = BDD()
    a, b, c = bdd.var_node('a'), bdd.var_node('b'), bdd.var_node('c')
    xor = lambda x, y: x != y
    # 進位函數 carry = ab + c(a XOR b)，用 BDD 運算組合
    ab = bdd.apply(lambda x, y: x and y, a, b)
    axb = bdd.apply(xor, a, b)
    c_axb = bdd.apply(lambda x, y: x and y, c, axb)
    carry = bdd.apply(lambda x, y: x or y, ab, c_axb)
    print("carry BDD 節點數 =", bdd.size(carry))
    # 等效檢查：與另一種寫法比較
    def ite(x, y): return (x and y) or (not x and y)
    carry2 = bdd.apply(lambda x, y: x or y, ab,
                       bdd.apply(lambda x, y: x and y,
                                 c, bdd.apply(lambda x, y: x or y, a, b)))
    print("兩種寫法等效（指標相同）:", carry == carry2)
    # 列出所有讓 carry=1 的賦值
    from itertools import product
    sat = [vals for vals in product([0, 1], repeat=3)
           if bdd.eval(carry, dict(zip('abc', vals)))]
    print("carry=1 的賦值:", sat)

BDD.eval_done = {}
def eval_bdd(self, u, env):
    """沿 BDD 走邊求值"""
    while u not in (0, 1):
        v, low, high = self.nodes[u]
        u = high if env[v] else low
    return u
BDD.eval = eval_bdd
build_and_eval()

輸出：

carry BDD 節點數 = 4
兩種寫法等效（指標相同）: True
carry=1 的賦值: [(0, 1, 1), (1, 0, 1), (1, 1, 0), (1, 1, 1)]

複雜度分析#

  • 建構單一函數：與 BDD 大小成正比，最壞 O(2ⁿ) 但好順序下常為線性。
  • apply 雙線性：O(|B₁|·|B₂|)，memoization 保證每對節點只算一次。
  • 等效檢查：化簡後正規形使比較為 O(1)。
  • 變數順序最佳化（sifting）本身是 NP-hard，sifting 啟發式約 O(n²·|B|)。

練習#

  1. 對 3 變數函數 f = a·b + ¬a·c，分別以順序 a<b<c 與 c<b<a 手畫 ROBDD，比較節點數。
  2. 在 BDD 類別加入 restrict(u, var, val)（限制變數取值）操作，並用它實作「找一組讓函數為 1 的賦值」的 sat 走訪。
  3. 實驗：建構 4 位元比較器 A > B 的 BDD，比較順序 a1 b1 a2 b2 ... 與 a1 a2 a3 a4 b1 b2 ... 的節點數差異。