布林邏輯與邏輯閘進階：正規形式、卡諾圖到二元決策圖

同一個函數，為什麼能寫出無數種樣子？

你已經會用真值表(truth table)定義一個布林函數，也知道 AND、OR、NOT 怎麼組合成半加器。現在來看一個更刁鑽的問題：下面三個式子

$$Y_1 = A\cdot\overline{B} + A\cdot B,\quad Y_2 = A,\quad Y_3 = \overline{\overline{A}+\overline{A}\cdot B}$$

其實全部相等——對任意 $A, B$ 都輸出同一張真值表。它們長得天差地遠，卻是同一個函數的不同「外衣」。這帶出一連串入門篇沒談的硬核問題：在這無數種寫法裡，有沒有一種是標準型，能讓兩個函數一比就知道是否相等？有沒有系統化的方法，找出最省閘的那一件外衣？當變數從 2 個變成 50 個，真值表的 $2^{50}$ 列根本列不完，我們又該用什麼資料結構去「裝」一個布林函數？

這篇進階篇，我們把布林邏輯當成一門表示法(representation)的科學：從正規形式(canonical form)，到卡諾圖(Karnaugh map)的完整操作，再到能裝下天文數字輸入的二元決策圖(BDD)，最後接上計算機科學最核心的 SAT 問題。入門篇談「邏輯是什麼」，這裡談「如何有效率地表示、化簡與判定邏輯」。

正規形式：給每個函數一張身分證

要判斷兩個布林函數是否相等，最笨的辦法是把真值表全部攤開比對。但更優雅的做法，是先把每個函數轉換成一種唯一的標準寫法，這樣只要兩個標準式長得一樣，就保證函數相等。這種標準寫法叫正規形式。

關鍵零件是最小項(minterm)。對 $n$ 個變數，一個最小項是「每個變數都出現恰好一次（以原形或反相）」的 AND 乘積，它只在唯一一組輸入下為 1。例如三變數時，$A\cdot\overline{B}\cdot C$ 只在 $(A,B,C)=(1,0,1)$ 時為 1。我們把這組輸入當成二進位數 $101_2 = 5$，就稱它為 $m_5$。

任何布林函數，都等於它所有「輸出為 1」的那些最小項之 OR 總和。這叫積項之和的正規形式(Sum of Products, SOP / 主析取範式)：

$$F(A,B,C) = \sum m(\text{所有讓 } F=1 \text{ 的列})$$

對偶地，把所有「輸出為 0」的列寫成最大項(maxterm) 的 AND 乘積，得到和項之積(Product of Sums, POS / 主合取範式)。最小項用 AND 鎖定一個 1、最大項用 OR 鎖定一個 0，兩者是 De Morgan 對偶。

看一個例子：把真值表變成正規式

考慮一個三輸入的「多數決(majority)」函數：三個輸入中有兩個或以上為 1 時，輸出才是 1（這正是表決電路、容錯系統的核心元件）。

輸出為 1 的列是 3、5、6、7，所以正規 SOP 是：

$$F = m_3 + m_5 + m_6 + m_7 = \overline{A}BC + A\overline{B}C + AB\overline{C} + ABC$$

這個式子唯一——只要是同一個多數決函數，無論你一開始怎麼寫，化成正規 SOP 後一定長這樣。它是函數的「身分證」。但它顯然不是最省的寫法：四個三輸入 AND 加一個四輸入 OR，太浪費了。接下來就要化簡它。

from itertools import product

def majority(a, b, c):
    return 1 if (a + b + c) >= 2 else 0

# 自動產生正規 SOP
terms = []
for a, b, c in product([0, 1], repeat=3):
    if majority(a, b, c):
        idx = (a << 2) | (b << 1) | c
        lit = (("A" if a else "A'") +
               ("B" if b else "B'") +
               ("C" if c else "C'"))
        terms.append(f"m{idx}={lit}")
print(" + ".join(terms))
# m3=A'BC + m5=AB'C + m6=ABC' + m7=ABC

卡諾圖：把化簡變成「圈圈」遊戲

入門篇提過卡諾圖的名字，這裡我們把它真正操作一遍。卡諾圖的精髓是：把真值表重新排列成方格，讓相鄰格只差一個變數，於是「兩個相鄰的 1」就能合併消去那個變數。

為什麼相鄰能消去變數？靠的是布林代數的合併律：

$$X\cdot Y + X\cdot\overline{Y} = X\cdot(Y+\overline{Y}) = X\cdot 1 = X$$

只要兩個乘積項「除了一個變數一正一反、其餘完全相同」，那個變數就消失了。卡諾圖的座標用格雷碼(Gray code) 排列（00, 01, 11, 10，相鄰只翻一位），正是為了讓物理上相鄰的格子，邏輯上也只差一個變數。

動手算一下：化簡多數決函數

把上面的多數決函數填進 K-map。橫軸是 $BC$（格雷碼 00,01,11,10），縱軸是 $A$（0,1）：

        BC=00  BC=01  BC=11  BC=10
 A=0  [  0  ] [  0  ] [  1  ] [  0  ]
 A=1  [  0  ] [  1  ] [  1  ] [  1  ]

現在圈出所有能圈的、由 1 組成的矩形（大小須為 $2^k$，可上下、左右環繞相接）：

• 圈 1：$BC=11$ 那一整欄（A=0 與 A=1 都是 1）→ 兩格消去 $A$，得 $B\cdot C$。
• 圈 2：$A=1$ 列的 $BC=01$ 與 $BC=11$ → 消去 $B$，得 $A\cdot C$。
• 圈 3：$A=1$ 列的 $BC=11$ 與 $BC=10$ → 消去 $C$，得 $A\cdot B$。

每個 1 都至少被一個圈覆蓋，把三個圈 OR 起來：

$$F = BC + AC + AB$$

從原本「4 個三輸入 AND + 1 個四輸入 OR」，化簡成「3 個二輸入 AND + 1 個三輸入 OR」。直覺上也對：多數決就是「任兩個為真就成立」，而 $BC$、$AC$、$AB$ 正好窮舉了「哪兩個」。注意中間 $BC=11$ 那格的 1 被三個圈重複覆蓋——這完全允許，重疊不會改變結果，反而常是化簡的關鍵。

化簡的目標術語要記得： - 質涵蓋項(prime implicant)：無法再被更大的圈吞併的最大圈。 - 必要質涵蓋項(essential prime implicant)：某個 1 只被它一個圈覆蓋，那它非選不可。

最簡 SOP 的標準流程，就是「找出所有質涵蓋項 → 先選必要的 → 再用最少的圈補完剩下的 1」。當變數超過 4~6 個，方格畫不下，就改用入門篇提過的 Quine–McCluskey 演算法做表格化，或交給 Espresso 之類的工具用啟發式處理。

Don't-care：允許「我不在乎」的格子

真實電路裡，有些輸入組合根本不會發生，或發生時我們不在意輸出。例如 BCD 碼（用 4 位元表示 0~9）裡，$1010$ 到 $1111$ 這六種組合是非法的，這些列的輸出可標成 $X$（don't-care，無所謂）。

Don't-care 是化簡的大禮物：每個 $X$ 你可以自由當成 0 或 1，哪個能圈出更大的圈就當哪個。

看一個例子：don't-care 帶來的化簡

假設某函數 $F(A,B,C,D)$，1 出現在 $m_1, m_3, m_7$，而 $m_5, m_{15}$ 是 don't-care，其餘為 0：

          CD=00  CD=01  CD=11  CD=10
 AB=00  [  0  ] [  1  ] [  1  ] [  0  ]
 AB=01  [  0  ] [  X  ] [  1  ] [  0  ]
 AB=11  [  0  ] [  0  ] [  X  ] [  0  ]
 AB=10  [  0  ] [  0  ] [  0  ] [  0  ]

若忽略 $X$，1 散在三處不好圈。但把 $m_5$（AB=01, CD=01）的 $X$ 當成 1，就能把 $m_1, m_3, m_5, m_7$ 圈成一個 $2\times2$ 大方塊（$A=0$ 的左下角四格，全部 $D=1$ 且 $C$ 任意、$B$ 任意但 $A=0$）。圈內 $A=0$、$D=1$ 固定，$B, C$ 都變化 → 化簡成 $\overline{A}\cdot D$。$m_{15}$ 那個 $X$ 我們選擇當 0（不圈它），免得多生一個項。最終：

$$F = \overline{A}\cdot D$$

一個原本零散的函數，靠著「不在乎的格子」竟塌縮成一個極簡的式子。這就是為什麼數位設計師對 don't-care 視若珍寶。

Shannon 展開與 BDD：裝下 50 個變數

當變數來到幾十個，真值表有 $2^{50}$ 列、卡諾圖更不可能畫。計算機科學需要一種能壓縮布林函數、又能快速運算的資料結構。出發點是 Shannon 展開(Shannon expansion)：任何布林函數都能依某個變數 $x$ 拆成兩半：

$$F = x\cdot F_{x=1} + \overline{x}\cdot F_{x=0}$$

其中 $F_{x=1}$ 是把 $x$ 固定為 1 後剩下的子函數（稱為 $F$ 對 $x$ 的餘式 cofactor），$F_{x=0}$ 同理。這就像問「先看 $x$ 是 0 還是 1，再分別處理剩下的部分」。

反覆套用 Shannon 展開，就長出一棵二元決策樹：每一層問一個變數、分兩條岔路，葉子是 0 或 1。這棵樹有 $2^n$ 個葉子，沒省到空間。真正的魔法是兩步壓縮，把它變成簡化有序二元決策圖(Reduced Ordered BDD, ROBDD)：

1. 合併同構：兩棵長得一模一樣的子圖共用一份（變成有向無環圖，不是樹）。
2. 刪除冗餘節點：某個節點的 0 邊與 1 邊指向同一處（這個變數不影響結果），就跳過它。

固定變數順序後，ROBDD 是正規形式——同一個函數的 ROBDD 唯一。於是「兩函數是否相等」變成「兩 BDD 是否為同一個圖」，可在常數時間判定（共用同一張表時只要比指標）。許多在真值表上爆炸的函數，在 BDD 上小得驚人。

# 用 functools.lru_cache 模擬 BDD 的「同構合併」精神：
# 相同 cofactor 子問題只算一次，自動共用結果
from functools import lru_cache

def make_bdd_counter(func, order):
    seen = {}                      # (level, 子函數簽章) -> 節點編號
    @lru_cache(maxsize=None)
    def build(level, assignment):
        if level == len(order):
            return func(*[assignment >> i & 1 for i in range(len(order))])
        var = order[level]
        lo = build(level + 1, assignment)                    # var=0
        hi = build(level + 1, assignment | (1 << var))       # var=1
        if lo == hi:               # 冗餘節點：跳過此變數
            return lo
        key = (level, lo, hi)
        if key not in seen:        # 同構合併：相同子圖共用
            seen[key] = len(seen)
        return ('node', seen[key])
    return build, seen

# 對多數決函數建表，觀察共用節點數
maj = lambda a, b, c: 1 if a + b + c >= 2 else 0
build, seen = make_bdd_counter(maj, order=[0, 1, 2])
build.cache_clear()
build(0, 0)
print("BDD 內部節點數:", len(seen))   # 遠少於 2^3 個葉子

BDD 是 1986 年 Randal Bryant 提出後席捲整個 EDA 與形式驗證領域的工具：它讓「比較兩顆晶片設計是否邏輯等價」「驗證一個硬體規格永遠成立」變得可行。代價是變數順序極度敏感——同一個函數，好的順序 BDD 只有幾十個節點，壞的順序可能指數爆炸，而找最佳順序本身是 NP-hard。

重點回顧

• 同一個布林函數有無數種寫法，但正規 SOP（最小項之和）與 POS（最大項之積）唯一，可當函數的身分證來判斷相等。
• 卡諾圖靠格雷碼讓相鄰格只差一變數，用「圈相鄰的 1」執行合併律 $XY+X\overline{Y}=X$；目標是用最少的質涵蓋項覆蓋所有 1，必要質涵蓋項一定要選。
• Don't-care（$X$） 可自由當 0 或 1，常讓圈變更大、式子更簡，是數位設計的化簡利器。
• Shannon 展開 $F=x F_{x=1}+\overline{x}F_{x=0}$ 是分治布林函數的基礎；反覆展開加上「同構合併＋刪冗餘」即得正規的 ROBDD，能緊湊表示與比較大型函數。
• BDD 對變數順序極敏感，最佳順序是 NP-hard；但它讓硬體等價驗證與形式驗證得以實用化。

深入探討（研究所視角）

入門篇提到 SAT 是史上第一個 NP-complete 問題。這裡把那條線接到底，談從電路到 SAT 的橋樑，以及它如何反過來重塑整個驗證產業。

第一個關鍵是 Tseytin 變換(Tseytin transformation)。如果天真地把一個布林電路展開成正規 CNF（合取範式，SAT 求解器的標準輸入），式子大小可能指數爆炸。Tseytin 的巧思是：給電路中每個閘的輸出引入一個新變數，然後只為「這個新變數 = 該閘的函數」這件事寫出局部子句。例如一個 AND 閘 $z = x\cdot y$，只需三條子句 $(\overline{x}\lor\overline{y}\lor z)\land(x\lor\overline{z})\land(y\lor\overline{z})$ 就完整刻畫。整個電路的 CNF 大小因此只線性於閘數，代價是多了一堆輔助變數。這讓「任意電路 → SAT 問題」的轉換在實務上完全可行，是現代 SAT-based 工具的地基。

有了這座橋，許多硬體問題就能化約成 SAT：要驗證兩個電路 $C_1, C_2$ 是否邏輯等價，construct 一個 miter 電路——把對應輸出兩兩 XOR 再 OR 起來——然後問「這個 miter 輸出能否為 1」。若 SAT 求解器回答 UNSAT（無解），代表沒有任何輸入能讓兩電路產生不同輸出，亦即兩者等價；若回答 SAT，求解器吐回的賦值就是一個讓兩電路不一致的反例(counterexample)。這正是 BDD 之外，業界做組合等價檢查(combinational equivalence checking)的第二大主力。

值得玩味的是 BDD 與 SAT 的分工：BDD 給你正規形式，一旦建好就能 $O(1)$ 比較、還能算出滿足賦值的數量（model counting，連到 $\#P$ 複雜度類）；但它可能在建構過程就記憶體爆炸。SAT 求解器（以 CDCL──衝突驅動子句學習為核心）不求正規形式，只求找一組解或證明無解，靠衝突學習與啟發式在巨大空間裡殺出血路，能處理上百萬變數的工業實例，卻無法直接做模型計數。兩者一個重「表示」、一個重「搜尋」，恰好對應布林函數的兩種根本提問。

再往理論深處走，會碰到電路複雜度(circuit complexity) 這個尚未解決的大陸。我們可以問：某個函數最少需要幾個閘？最少需要幾層（深度，對應電路延遲）？對「平價函數(parity)」這類函數，已證明在常數深度、多項式大小的限制下（複雜度類 $\mathsf{AC}^0$），無論用多少 AND/OR 閘都算不出來——這是 Furst–Saxe–Sipser 與 Håstad 的著名下界結果，也是少數我們證得出硬度的領域。對照之下，電路複雜度的終極目標──證明某個 NP 問題需要超多項式大小的電路（這將直接推出 $P\neq NP$）──至今仍遙不可及。從一張多數決真值表出發，圈幾個卡諾圖的圈圈，竟一路通向計算理論最深的未解之謎，這正是布林邏輯作為計算機科學基石的魅力所在。