2.1 香農 1937 論文之後：布林代數如何進入工程世界#
今天任何一個寫過 Verilog 或 Veryl 的人，大概都不會覺得「邏輯閘可以用代數來算」這件事有什麼稀奇。a & b | ~c 這樣的式子我們每天都在寫，合成工具在背後對它做化簡、展開、映射，一切都顯得理所当然。但這個「理所当然」其實是一段不長也不短的歷史疊加出來的結果：數學家先發明了一套關於真假的代數，工程師花了大約八十年才把它變成設計數位電路的日常語言。這段歷史的分水嶺，通常被定在 1937 年，一位二十一歲的 MIT 碩士生 Claude Elwood Shannon 的學位論文。
在香農之前：一門「無用」的數學#
George Boole 在 1854 年出版《An Investigation of the Laws of Thought》，把亞里士多德的邏輯推理改寫成一種代數：變數只能取 0 或 1，運算只有「與、或、非」三種，但這套系統擁有與普通代數類似的結構性質——交換律、結合律、分配律都成立，甚至還有一條普通代數沒有的奇特恆等式 \(x(x+y) = x\) 。Boole 的動機是哲學的：他想把「思考的法則」形式化。此後將近八十年，這套代數主要在哲學與純數學圈子裡流轉，對工程界而言幾乎不存在。
讓它重新變得「數學」的一步，是 Harvard 的 Edward V. Huntington 在 1904 年發表的論文。Huntington 給了布林代數一組精簡的公設（今天教科書裡常見的 Huntington postulates）：封閉性、交換律、結合律、分配律、補元存在，以及至少兩個相異元素。這看起來只是抽象代數的例行工作，但它產生了一個深遠的副作用——從此「這是不是一個布林代數」變成一個可以用公設檢驗的問題，而「布林代數的定理」變成可以從少數幾條公理機械化推導的結果。公理化把這套系統從哲學搬進了工程可以安全使用的範圍：工程師不需要理解 Boole 的思辨哲學，只需要相信一組檢驗過的公理和從中推出的定理表。
1937 年：把開關變成變數#
Shannon 在 MIT 的碩士論文《A Symbolic Analysis of Relay and Switching Circuits》於 1937 年完成，1938 年發表於 Transactions of the AIEE。他的洞見極其簡單卻又驚人：電話交換機裡的繼電器（relay）是雙態元件——觸點閉合或斷開——而串聯與並聯恰好對應布林代數裡的「與」和「或」。於是「電路」與「布林表達式」之間存在一個完整的同構：給定任何布林表達式，可以機械地畫出一個等效的繼電器網路；反之，任何串並聯繼電器電路都可以機械地讀成一個布林表達式，而且兩者的行為完全等價。
這件事的工程意義遠超過「方便」。在 1937 年之前，設計一個複雜的繼電器控制電路（電話路由、工廠聯鎖、電梯控制）依賴的是經驗、直覺與試誤；電路對不對，要靠接線圖逐條追。Shannon 之後，設計變成了代數操作：你可以把需求寫成方程式，用布林代數的定理化簡，每一個化簡步驟都對應實際省下的繼電器——而繼電器就是錢。論文裡著名的例子是那個「五個開關控制一盞燈」的電路：用窮舉真值表得到的直接設計需要大量觸點，經過代數化簡（特別是利用互斥條件）可以砍到驚人地少。省下的每一個繼電器都是真金白銀，這就是為什麼這篇論文立刻被貝爾實驗室與工業界認真對待——Shannon 本人當時正是在貝爾實驗室實習。
用今天的話說，Shannon 完成的是一次「表示法革命」：他證明了一個領域（電路設計）可以被完整地嵌入另一個領域（代數），而且嵌入之後，後者累積的全部定理與計算技巧都自動變成前者的生產力。這正是後來所有 EDA 演算法的原型——本書接下來要講的 BDD、AIG、SAT，全部都是這個模式在不同時代的重演：找到更好的表示法，然後在表示法上做更聰明的計算。
繼電器計算機與兩級邏輯的工程文化#
Shannon 的理論落地得非常快。1940 年代，貝爾實驗室的 Model I relay computer（George Stibitz 主導）與哈佛的 Mark I/Mark II（Howard Aiken、Grace Hopper 等人參與）、IBM 的繼電器計算機，全都建立在繼電器邏輯之上，而繼電器電路的設計與檢查已經可以按 Shannon 式的代數方法進行。貝爾實驗室內部把這套方法發展成系統的「switching algebra」，培養出一整代把邏輯當代數算的工程師。戰後晶體管與積體電路出現，繼電器換成了電晶體閘，但表示法不變——因為雙態這個本質沒有變。
與此同時，一種特有的工程文化開始定型，它的核心是兩個互補的物件：真值表（truth table）與兩級邏輯（two-level logic）。對一個 \(n\) 輸入的函數，真值表窮舉 \(2^n\) 行，是「語義」的完備表示；而積之和（SOP，sum of products）與和之積（POS，product of sums）則是「語法」上的標準形——任何布林函數都能寫成最小項之和或最大項之積，對應到電路上就是「AND 陣列接到 OR 陣列」的兩級閘結構。這個文化的優點是簡單、可檢驗、可自動化：真值表可以直接比對規格，兩級結構對應的物理實現（當年是二極體矩陣，後來是 PLA）延遲均勻、容易分析。
兩級邏輯最佳化因此成為邏輯合成的第一個系統性研究對象。1950 年代末，Quine 與 McCluskey 把「找最小 SOP」形式化：真值表裡所有讓函數為 1 的最小項，先合併成質蘊含項（prime implicants），再用集合覆蓋（set covering）選出成本最小的那一組。McCluskey 的列表法讓這個過程可以交給機器做——這可能是歷史上第一個真正意義上的「邏輯合成演算法」。後來 Espresso 這類啟發式工具（1980 年代，Berkeley）把兩級化簡做到了實用規模，而 PLA 作為一種可程式化邏輯元件，正是兩級邏輯文化的硬體化身。直到今天，任何 EDA 工具內部處理小型控制函數時，質蘊含項與覆蓋的思想仍然隨時會冒出來。
但兩級邏輯有著先天的天花板：對很多函數（例如加法器的進位鏈、多數函數），最小的兩級實現遠大於多級實現，而且真值表的 \(2^n\) 指數成長讓「窮舉表示」在輸入數一多時徹底失效。工程界於是被迫面對一個延續至今的問題：有沒有一種表示法，既是正準的（canonical，同一函數只有一種寫法，方便判等價），又是簡潔的（compact，函數大表示也不會爆），而且支援高效的操作（化簡、組合、等價檢查）？遺憾的是，可以證明這三個願望原則上互相衝突——但二十世紀末的兩場革命，先後把其中兩個願望用驚人的方式實現了。
教育、產業與制度的固化#
歷史不只是演算法史，也是制度史。Shannon 之後，布林代數迅速進入了工程教育：1940 到 1950 年代，switching circuits 成為電機系與計算機科學系的標準課程，教材（例如 Marcus 的《Switching Circuits for Engineers》、稍後 McCluskey 的教科書）把 Karnaugh 圖——1953 年 Maurice Karnaugh 在貝爾實驗室提出的化簡圖解法——變成了幾代工程師的共同記憶。卡諾圖本質上是真值表的一種幾何重排，讓相鄰的最小項在紙面上相鄰，人眼可以一眼看出合併機會。它是 Quine-McCluskey 的手工版，也正是「EDA 是把手工技巧自動化」這條主線最早的例證之一。
產業方面，貝爾系統對交換電路的可靠性要求催生了早期形式化的驗證與測試思想；IBM 則在其邏輯設計自動化部門裡，從 1950 年代末就開始寫程式做邏輯化簡與綜合——這條內部工具的脈絡一路演化，最終與學術界（特別是 Berkeley 的 LSSD、MIS、SIS 傳統）會合，成為今日商業合成工具的遠祖。換句話說，Shannon 論文之後的三十年間，社會完成了三件讓後續一切成為可能的事：把布林代數寫進了大學課綱、把兩級邏輯寫進了工廠流程、把「用程式處理邏輯」寫進了公司組織。沒有這三個制度性的固化，1980 年代 EDA 作為一個產業的誕生（Mentor、Synopsys、Cadence 的前身工具）將無從談起。
回頭看，1937 年那篇論文真正留下來的遺產，不是繼電器（繼電器早就被淘汰了），而是一個信念：邏輯設計可以被計算。接下來的三節，我們將沿著這個信念追蹤三條主線：首先是 1986 年 Randy Bryant 的 BDD——它第一次給出「正準又相對簡潔」的表示，讓等價性檢查與符號驗證成為可能；然後是 Mishchenko 的 AIG 與 ABC——邏輯最佳化在「非正準但可操作」方向上的集大成；最後是 SAT 求解器——把 Shannon 的窮舉精神推向實用規模的引擎。三條線共享同一個起點，也共享同一個教訓：表示法的選擇決定一切。
延伸閱讀#
- C. E. Shannon, "A Symbolic Analysis of Relay and Switching Circuits," Trans. AIEE, 1938（1937 年 MIT 碩士論文）。
- E. V. Huntington, "Sets of Independent Postulates for the Algebra of Logic," Trans. AMS, 1904。
- E. J. McCluskey, "Minimization of Boolean Functions," Bell System Technical Journal, 1956。
- W. V. Quine, "The Problem of Simplifying Truth Functions," Amer. Math. Monthly, 1952。
下一節：當兩級邏輯與真值表都被指數爆炸卡住之後，Bryant 在 1986 年提出的約化有序二元決策圖（ROBDD），如何用一張有向圖同時解決「正準性」與「操作效率」，並點燃形式驗證的火焰。