2008 Z3 與 SMT 革命：理論求解器的聯合偵查#
案件編號：2008-Z3。報案人：軟體驗證、合約檢查、符號執行。案情：純 SAT 不懂整數、陣列與位元向量。破案者：de Moura 與 Bjorner。
案發現場#
2001 年 Chaff 讓純布林 SAT 快如閃電，但軟體驗證的公式不是純布林的。它們長這樣：「陣列 \(a\) 在 \(i\) 處更新後讀回是否等於 \(v\) ？」「32 位元無號加法是否溢位？」「整數計數器是否永不為負？」把這些硬編成 CNF，又大又慢，還丟失高層結構。
學界早有各理論的判定程序：等式與未解釋函數（EUF）、線性算術、陣列、位元向量，各自為政。缺少的是一個「聯合偵查指揮部」：讓 SAT 求解器管布林骨架，讓理論求解器管各自公理，兩者互相通報、共同破案。
2008 年，微軟的 de Moura 與 Bjorner 發布 Z3，高效、免費、介面友善，一舉把 SMT（Satisfiability Modulo Theories）送進千家萬戶。
偵查過程（含數學式/表格/理論）#
線索一：DPLL(T) 的雙向通報架構#
Z3 的心臟是 DPLL(T)：SAT 引擎與理論求解器 \(T\) 的迴圈。布林抽象把每個理論原子（如 \(x + y \le 5\) ）看成布林變數 \(p\) ，SAT 先找布林模型，理論再檢查該模型在 \(T\) 下是否一致：
流程如審訊：SAT 提出嫌疑賦值 \(\sigma\) ，理論求解器驗身。若理論不一致（如 \(x > 0 \land x < 0\) 同真），回傳理論引理（theory lemma） \(\neg (p_1 \land p_2)\) ，SAT 學入子句再搜。懶惰（lazy）而高效，兼有早期剪枝與傳播。
表格：DPLL(T) 分工。
| 角色 | 負責 | 例子 |
|---|---|---|
| SAT 核心（CDCL） | 布林搜尋、學習、回跳 | \(p \lor q\) |
| EUF 求解器 | 等式、同餘閉包 | \(f(x) = f(y) \Leftarrow x = y\) |
| 算術求解器 | 線性/非線性約束 | \(x + 2y \le 5\) |
| 陣列/位元向量 | 記憶體與機器整數 | \(read(write(a,i,v),i) = v\) |
線索二：理論表——每一條公理都是證詞#
SMT 的威力來自理論公理。精選對照表：
| 理論 | 簽名 | 關鍵公理 |
|---|---|---|
| EUF | \(=\) 、未解釋 \(f\) | \(x = y \Rightarrow f(x) = f(y)\) |
| 線性整數 LIA | \(+\) 、 \(\le\) | Fourier–Motzkin 消元 |
| 陣列 | \(read\) 、 \(write\) | \(read(write(a,i,v),i) = v\) |
| 陣列外延 | 同上 | \(i \ne j \Rightarrow read(write(a,i,v),j) = read(a,j)\) |
| 位元向量 | \(+_{32}\) 、 \(<<\) 、 \(\&\) | 模 \(2^{32}\) 算術 |
| 量詞 | \(\forall\) 、 \(\exists\) | E-matching 實例化 |
偵查示例：要證 \(read(write(a,i,v),i) = v\) ，EUF＋陣列公理一次結案，無需展開記憶體。位元向量理論則讓 \(x +_{32} 1 >_{u} x\) 的溢位查詢變成精確判定，而非抽象近似。
SMT-LIB 標準語言（2003 起，後續版本成熟）讓基準與求解器互通，SMT competition 複刻 SAT 的軍備賽榮景。
線索三：從合約驗證到 VS Code#
Z3 的破案範圍迅速擴大：
- Dafny、Spec#、F* 把前後條件與不變式丟給 Z3，合約驗證按鍵即判。
- 符號執行（SAGE、KLEE）把路徑條件丟給 Z3，每秒數千查詢。
- VS Code 等現代編輯器的靜態檢查、依賴分析、甚至排程求解背後，常有 Z3 或其親戚。
- Lean 4 的 de Moura 血統亦源於此：求解器與證明器本是一家。
表格：應用鏈。
| 應用 | 編碼 | Z3 角色 |
|---|---|---|
| 有界模型檢查 | 單次賦值＋ \(SS A\) | 位元向量判定 |
| 合約驗證 | \(VC\) 蘊含 | 量詞＋算術＋陣列 |
| 符號執行 | 路徑條件 | 增量求解 |
| 類型推斷/合成 | 約束集 | 組合優化 \(\nu Z\) |
結案報告#
案件告破。Z3 證明：SAT 管骨架、理論管血肉，雙向引理交換即可馴服軟體公式。SMT 從論文走向基礎設施，驗證從實驗室走向按鍵。
遺產有三：
- SMT-LIB＋競賽建立開放生態，CVC5、Yices、Boolector 百花齊放。
- 程式驗證工具鏈（Boogie、Dafny、F*、SeaHorn）統一以 SMT 為後端。
- 求解器即服務：Z3 Python/OCaml/C++ 綁定讓約束求解變成三行程式的事。
從因果鏈看，Z3 上承 DPLL、Chaff CDCL、歸結與各理論判定程序，下啟自動驗證普及與 Lean/AI 證明時代。
證據與工具#
證據 A：架構圖再現，獨立成行。
左箭頭送理論引理，右箭頭送布林賦值，迴圈至 SAT 或 UNSAT。
證據 B：SMT-LIB 示例。
(set-logic QF_ABV)
(declare-const a (Array (_ BitVec 32) (_ BitVec 8)))
(declare-const i (_ BitVec 32))
(declare-const v (_ BitVec 8))
(assert (= (select (store a i v) i) v))
(check-sat)
此查詢應得 \(sat\) ，其否定則 \(unsat\) ，正好對應陣列公理。
證據 C：增量求解模式。 push 、 assert 、 check-sat 、 pop 四步迴圈，符號執行靠它重用學習子句，查詢吞吐提升數量級。
證據 D：延伸閱讀。de Moura 與 Bjorner 2008 年〈Z3: An Efficient SMT Solver〉；Barrett 等《Handbook of Satisfiability》SMT 章；SMT-LIB 官網基準庫與 Z3 GitHub 教程。