有一陣子以來，我一直對 Z3 以及更廣義的 SMT 求解很著迷。最近在休育嬰假時，我想起了正則表達式填字遊戲的存在，於是忍不住讓自己掉進這個坑，寫了一個以 Z3 為後端的求解器。

我原本以為大概花個一下午就能快速拼出一個求解器；結果卻深陷其中，開始研究與除錯 Z3 的效能，也學到了遠比預期多得多的 Z3 與 SMT 知識。在這篇文章裡，我會先說明我的做法與最初的求解器，再深入探討後來嘗試的各種改進與變化。

我所有的程式碼都已在 GitHub 上公開，如果你想跟著實作或查看最終成果，都可以去看看。

正則表達式填字遊戲

簡單回顧一下：正則表達式填字遊戲由一個（未知的）字元網格組成，這些字元有待填入。這些字元受到一組給定的正則表達式限制，填好之後，每一列或每一欄都必須符合對應的正則表達式。我選擇的是regexle這個變體，它使用六角形網格，不過我大部分的程式碼應該都能輕鬆套用到其他變體上。

把正則表達式看作 DFA

要用像 Z3 這樣的約束求解器來解這個謎題，我們得想辦法把「這串字元符合這個正則表達式」這樣的限制編碼進去，然後把所有線索都加上去，再請它找出一個滿足所有限制的網格。

我第一個直覺是利用這個事實：正則表達式描述的是一個正則語言¹，因此可以用確定性有限自動機來辨識。也就是說，我可以把正則表達式編碼成 DFA，再透過它的轉移函數在 Z3 裡表達正則匹配²。

也就是說，如果我們有一個三字元的字串 S = [c0, c1, c2]，以及這個正則表達式的轉移表 T : State × Char → State，我們就可以把「這個正則表達式符合 S」表達成類似這樣：

state_0 = init_state
state_1 = T(state_0, c0)
state_2 = T(state_1, c1)
state_3 = T(state_2, c2)
assert(state_3 in accept_states)

把正則表達式轉成 DFA

稍微搜尋了一下，我找到了 qntm 的 greenery 函式庫，正好完全符合我的需求——這是一個相對簡潔的 Python 函式庫，用來操作正則表達式，包含在正則語法與 DFA（它稱之為FSM）之間來回轉換。它會幫我們建好 FSM，整體來說非常直觀，設計上追求的是簡潔、易用、方便實驗，而非極致效能，這對我們來說完全沒問題——反正繁重的工作都要交給 Z3 去做。

有一個小麻煩是，greenery 處理的是涵蓋任意 Unicode 字元的正則表達式；為了避免產生巨大的查詢表，它用字元區間來表示轉移，這讓我覺得處理起來有點麻煩。在這個專案裡，我願意假設字母表只有英文字母（A-Z），所以我寫了一個小幫手，把 greenery 的結構轉成扁平的 numpy 轉移表：

ALPHABET = string.ascii_uppercase

def flatten_fsm(fsm):
    nstate = len(fsm.states)
    nvocab = len(ALPHABET)

    assert fsm.states == set(range(nstate))
    state_map = np.full((nstate, nvocab), -1, dtype=np.int32)
    for st, map in fsm.map.items():
        for i, c in enumerate(ALPHABET):
            for cc, dst in map.items():
                if cc.accepts(c):
                    state_map[st, i] = dst
                    break
    return state_map

我也定義了一個小小的 dataclass，把單一正則表達式的各種表示法與分析結果包在一起：

@dataclass
class Regex:
    pattern: str
    parsed: greenery.Pattern

    # 2d: (state, vocab) -> new state
    transition: np.ndarray
    # 1d: state -> bool
    accept: np.ndarray

    @classmethod
    def from_pattern(cls, pattern: str):
        parsed = greenery.parse(pattern)
        fsm = parsed.to_fsm().reduce()

        transition = flatten_fsm(fsm)
        nstate = transition.shape[0]
        accept = np.zeros((nstate,), bool)
        for st in fsm.finals:
            accept[st] = True

        return cls(
            pattern=pattern,
            parsed=parsed,
            transition=transition,
            accept=accept,
        )

對應到 Z3

要把各個部分組合起來，我們得讓 Z3 認識每個線索的轉移函數，為網格中的每個字元定義 Z3 變數，然後用對應的轉移函數對這些字元加上適當的限制。

我選擇把狀態和字元都用整數來表示（並加上斷言確保它們在合法範圍內），因為這樣看起來最簡單。接著，我們需要把狀態與字元之間的轉移函數關係編碼進去。

Z3 支援函式型別，可以在表達式和斷言中宣告與操作。因此，我宣告了一個對應型別的函式，並透過對轉移表中每一筆資料各加一個斷言，來告訴 Z3 轉移表的內容：

def build_func(solv: z3.Solver, clue: Clue):
    ctx = solv.ctx
    state_func = z3.Function(
        clue.name + "_trans",
        z3.IntSort(ctx),
        z3.IntSort(ctx),
        z3.IntSort(ctx),
    )
    pat = clue.pattern

    for (state, char), next_state in pat.all_transitions():
        solv.add(state_func(state, char) == next_state)

    return state_func

有了這個定義，再給定一個字串（以字元列表表示），我們就能輕鬆表達「符合正則表達式」這個限制：

def assert_matches(solv: z3.Solver, clue: Clue, chars: list[z3.AstRef]):
    state_func = self.build_func(solv, clue)
    pat = clue.pattern

    # Create constants for each state
    states = z3.IntVector(clue.name + "_state", 1 + nchar, ctx=solv.ctx)

    # Express the transition requirement
    for i, ch in enumerate(chars):
        solv.add(state_func(states[i], ch) == states[i + 1])

    # Each state must be valid
    for st in states:
        solv.add(0 <= st)
        solv.add(st < pat.nstate)
    # State zero is the initial state
    solv.add(states[0] == 0)

    # The final state must be accepting
    solv.add(z3.Or([
        states[-1] == i
        for i, ok in enumerate(pat.accept) if ok
    ])

組合起來

有了這些基本元件，我們現在只需要定義一個字元網格，並加上適當的斷言。我還是用regexle作為測試案例的來源；它使用六角形網格，而要在六角網格與三個不同線索軸之間對應座標，說實話是這整個練習中最困難的部分之一！不過先略過那部分，程式碼本身相當簡潔：

def make_char(solv: z3.Solver, name: str) -> z3.ExprRef:
    ch = z3.Int(name, solv.ctx)
    solv.add(0 <= ch)
    solv.add(ch < len(ALPHABET))
    return ch

grid = [
    [make_char(solv, f"grid_{x}_{y}") for y in range(maxdim)]
    for x in range(maxdim)
]

for clue in all_clues:
    coords = word_coords(clue.axis, clue.index)
    chars = [grid[x][y] for x, y in coords]

    assert_matches(
        solv,
        clue,
        chars,
    )

求解器效能

到了這個階段——把所有部分組合起來之後——我已經可以解填字遊戲了，但速度……慢得讓人痛苦。有些 3x3 的謎題在我的 M1 MacBook Air 上竟要花上超過十分鐘的 Z3 運算時間！我研究出如何讓 Z3 使用多核心，雖然有了一點常數倍的加速，但本質上還是太慢了。

憑著模糊的直覺，我預期 Z3 應該能在幾毫秒內解開這些謎題。因此，我覺得有必要花點時間去除錯、弄清楚我的求解器到底為什麼這麼慢，以及該怎麼讓它變快。

當時我對 Z3 完全是個新手，根本不知道該嘗試什麼、該看哪裡；在接下來的探索過程中，我學到了非常多。最終我確實達到了預期的速度，但中間也遇到了許多誤導和意外。

就算在這個專案之前，我也隱約知道 SMT 求解器出了名的不透明、效能也不太穩定不穩定。不過，我還是對這個說法在一個我以為相當簡單的問題上竟如此成立感到驚訝。有不少我遇到的行為，到現在我都還沒完全搞懂。

我會先分享最終影響最大的兩個改動——就我所知，它們產生了一個快速又可靠的求解器——然後再來聊聊那些失敗的嘗試和其他奇怪的現象。

剪除狀態

如我所說，我不是（當時也不是？）Z3 專家，但我對正則表達式倒是相當了解。因此，我的第一個想法是透過領域相關的分析來產生額外的限制，幫 Z3 一把。

舉個具體的例子，考慮我寫這篇文章當天的 regexle 出現的正則表達式 (NR|Q|I)+。很明顯，答案只可能包含 N、R、Q 和 I 這幾個字母。然而，我的程式碼卻為所有格子硬性設定了 A-Z 的字母表，得靠 Z3 自己去排除其他字母。如果我們能偵測出實際合法的字母表，並把它編碼進 Z3 問題裡，會怎麼樣呢？

人類只要看一下正則表達式的原始碼，就能輕易發現這個特性。我們當然也可以寫程式做類似的分析，但一般來說問題沒那麼單純。不過我意識到，我們反而可以對手上已有的轉移表做類似的分析。而且，因為我現在也是個科學家而不只是工程師了，我決定用幾行 numpy 技巧就搞定。

我們把 FSM 中一個狀態定義為「死亡」狀態，如果從該狀態出發，不存在任何轉移序列能到達任何接受狀態。因為我們使用的是經過一次 greenery 分析處理後的最小化 FSM，我們知道最多只會有一個死亡狀態，而且從該狀態出發的所有邊都會是自迴圈。我們可以透過尋找這個條件來輕鬆偵測死亡狀態：

# Method on the above class `Regex`
@cached_property
def dead_states(self) -> set[int]:
    looped = self.transition == np.arange(self.nstate)[:, None]
    return set(np.flatnonzero(looped.all(-1) & ~self.accept))

（注意，我們永遠只會有零個或一個死亡狀態，但使用 set[int] 可以讓我們透過遍歷集合來統一處理這兩種情況，我覺得這比用 int | None 來得乾淨一些）

有了死亡狀態，我們就可以把死亡字元定義為：無論從哪個狀態出發，都一定會轉移到死亡狀態的字元：

@cached_property
def dead_vocab(self) -> set[int]:
    dead = set()
    for d in self.dead_states:
        dead |= set(np.flatnonzero((self.transition == d).all(0)))
    return dead

我們也可以問，從任意給定狀態出發，哪些字元是死亡的：

def dead_from(self, state: int) -> set[int]:
    dead = set()
    for d in self.dead_states:
        dead |= set(np.flatnonzero((self.transition == d)[state]))
    return dead

有了這些資訊，我們就能給 Z3 再多加幾個限制：

for d in pat.dead_vocab:
    for ch in chars:
        solv.add(ch != d)

for d in pat.dead_from(0):
    solv.add(chars[0] != d)

for d in pat.dead_states:
    for st in states:
        solv.add(st != d)

嚴格來說，這些限制是多餘的，但我們的期望是，憑藉我們對問題結構的了解，能比 Z3 更輕鬆地找出這些事實，讓 Z3 更快專注在搜尋空間中「有趣」的部分。

的確，我覺得這個剪枝練習是個很有趣的例子，說明了如何在使用 Z3 這類通用證明器／求解器的同時，透過領域相關的啟發式方法來提升效能。我的感覺是，這種混合做法在實務上相當常見；求解器並非魔法，如果你能透過領域分析推導出額外的結構，往往能給求解器帶來重要的助力。

如果我願意，要讓 Z3 在某些特定謎題上額外驗證這些限制確實是多餘的，其實相當直接，這會是個有用的正確性檢查。不過對這個小玩具專案，我就懶得做了。

明確定義轉移函數

前面我提到，我把每個正則表達式的轉移表編碼為 Z3 函式，然後用針對每個 (state, character) 組合的逐點斷言來固定它的行為。我後來發現，如果把轉移表示為一個明確的表達式，而不是未解譯函式，就能獲得更好的效能；我猜測這樣做會促使 Z3 用等式推導的方式來推理這個關係，而不是退回搜尋，但老實說我也不太確定。

我們來寫一個 Python 函式，把轉移表表示為一個分析 (state, character) 輸入的明確 if-then 階梯。先從一個幫手函式開始，它實際上就是對單一變數做「match」或「switch」：

def build_match(
    var: z3.AstRef,
    test: list[z3.AstRef],
    result: list[z3.AstRef],
) -> z3.AstRef:
    """Return a Z3 `if` ladder comparing var against each `test` value.

    If `var == test[i]`, the ladder evaluates to `result[i]`. If no
    `test` matches, evaluate to `result[-1]`; it is anticipated that
    normally the list of tests will be exhaustive.
    """
    expr = result[-1]
    for test_, then_ in zip(test[:-1], result[:-1], strict=True):
        expr = z3.If(var == test_, then_, expr)
    return expr

現在，給定對應狀態和字元的 Z3 表達式，我們就能建構一個計算新狀態的明確表達式：

def build_next_state(
    self, clue: Clue, st: z3.AstRef, ch: z3.AstRef
) -> z3.AstRef:
    pat = clue.pattern
    by_state = [
        build_match(
            ch,
            self.alphabet,
            [self.states[out] for out in pat.transition[i]],
        )
        for i in range(pat.nstate)
    ]

    return build_match(
        st,
        self.states[: pat.nstate],
        by_state,
    )

現在，原本我們寫的是 state_func(states[i], ch) == states[i + 1]，我們可以改為為每次轉移直接嵌入整個表達式：

for i, ch in enumerate(chars):
    solv.add(self.build_next_state(clue, states[i], ch) == states[i + 1])

這個方法帶來了可觀的加速，尤其是讓效能變得穩定許多；在較大的謎題尺寸下，比起舊的逐點斷言做法，我遇到的「慢速謎題」少了很多。

不幸的是，這個直接的做法有個明顯的缺點：建構龐大的 Z3 if-then 階梯本身非常耗時，甚至花在建構 Z3 表達式上的時間，遠比實際求解的時間還長！

共用表達式

有沒有辦法兩全其美呢？我花了不少時間挖掘和實驗，終於找到一種方法，既能達到明確表達式同樣的效能，又只需要建構一次表達式。事實上，我找到了兩種不同的策略，也順便展示了 Z3 的一些功能。

使用 Z3 lambda 表達式

與其使用 Z3 函式物件，我們可以把龐大的 if 階梯包在 z3.Lambda 表達式裡，這樣就能用不同的參數多次明確地實例化它。以上面的 build_next_state 函式為基礎，這只是個很小的改動：

st = z3.Int("st")
ch = z3.Int("ch")

lambda_ = z3.Lambda([st, ch], self.build_funcexpr(clue, st, ch))

for i, ch in enumerate(chars):
    solv.add(lambda_[states[i], ch] == states[i + 1])

使用 Z3 函式與 macro-finder

不過，在探索其他選項時，我正在閱讀 SMT-LIB 規格，注意到 SMT-LIB 允許用明確的函式主體來定義函式：

(define-fun double ((x Int)) Int (* x 2))

;; evaluates to `8`
(simplify (double 4))

Z3 讓我們可以使用這些工具，所以我試著這樣做：

state_expr = self.build_funcexpr(clue, st, ch)
solv.add(z3.ForAll([st, ch], state_func(st, ch) == state_expr))

這個方法就產生正確解而言是可行的，但結果卻是我嘗試過的方法中最慢的之一！

不過，經過更多挖掘後，我找到了解法！Z3 有一個名為「macro-finder」的「tactic」。Z3 的 tactic 是一種轉換機制，允許使用者在核心 SMT 求解器之外，主導簡化或轉換的過程。macro-finder 實作了多種轉換，但最基本的功能是找出那些「定義」函式意義的 forall 斷言，並有效地把函式呼叫的地方直接以其定義替換掉。本質上，它把我們的 forall 變體轉換成「每次都用明確表達式」的變體，但因為它是用 C++ 實作、更接近 Z3 核心，所以執行得相當高效。

我發現這三種方法（明確表達式、z3.Lambda，以及 forall+macro-finder）在 Z3 中的求解時間都差不多，而 z3.Lambda 和 macro-finder 在定義問題的執行時間上也同樣快速。

失敗的嘗試

接下來，我們來深究那些行不通、或至少不是必要的事情。在這個過程中，我們會學到更多 Z3 的功能，以及一些令人驚訝的效能行為。如果你比較想直接看結論，也可以跳到我的總結。

Z3 EnumSort

Z3 對整數了解很多，並且針對不同類別的整數運算有許多不同的求解器。我在想：能不能改用別的資料型別，完全避開那些整數邏輯，來加速求解器呢？

因此，我嘗試把狀態和字元換成 SMT-LIB 列舉型別（在 Python 中以 z3.EnumSort 提供）。

我們可以為狀態和字元各定義一個列舉排序，建立一個除了恰好有 N 個不同值之外沒有任何其他行為的新型別：

nstates = max(c.pattern.nstate for c in all_clues)
state_sort, states = z3.EnumSort(
    "State",
    [f"S{i}" for i in range(nstates)],
)

char_sort, alphabet = z3.EnumSort("Char", list(ALPHABET))

程式碼的其他部分也只需要做很小的改動；我們需要在轉移函式的宣告中把 IntSort 換掉，並且在編碼特定狀態或字元時，把 i 換成 states[i] 或 alphabet[i]。

EnumSort 的效能

當我第一次改用 EnumSort 時，我看到效能大幅提升！

不過，後來發現我對於為何會看到這種加速的解釋，最多只對了一半。這是同一張圖，但現在我又加了兩個新的對照組：一個仍然使用逐點函式定義，但做了個等一下會提到的小改動，另一個則使用前面提過的 z3.Lambda 編碼：

以我目前的程式碼來說，在逐點函式定義下 IntSort 反而更快，而且明確編碼轉移函數所帶來的加速，遠遠超過其他任何改動。

一個詭異的效能不穩定現象

那我在「(old)」和「(new)」之間到底改了什麼？

當我們用整數來表示狀態時，會用額外的斷言來限制整數的範圍。前面我展示了我最初為這些範圍寫的程式碼：

# Each state must be valid
for st in states:
    solv.add(0 <= st)
    solv.add(st < pat.nstate)

當我在重構程式碼以實驗其他表示法時，無意間把行為改成了用所有線索中狀態數的最大值來限制狀態，而不是只用當前線索的狀態數：

max_nstate = max(clue.pattern.nstate for clue in all_clues)

for st in states:
    solv.add(0 <= st)
    solv.add(st < max_nstate)

至少在我這個版本的 Z3 上，第二種做法——這可是更寬鬆的限制！——卻快得多。我相信，這個改動就是 IntSort 在「(old)」和「(new)」圖表中唯一有意義的差異！

此外，我其實也不明白為什麼 EnumSort 在逐點函式定義下會比較慢。我查看了 Z3 的追蹤紀錄和統計資料，看起來 Z3 在列舉型別的情況下，似乎難以用等式推導的方式處理我們 xfer(st, ch) == st_next 的斷言，因而需要更多的搜尋與回溯，但我不明白原因何在。

使用 Z3 的正則表達式

在重構程式碼以支援各種表示法的組合，並對它們進行效能分析與繪圖的過程中，我也嘗試了一種完全不同的方法來解決這個問題！

結果發現，Z3 也有一個正則表達式理論！我們可以完全繞過狀態機的機制，直接把正則表達式線索編碼成 Z3 的正則表達式。

Z3 並沒有內建正則表達式解析器，而是提供了像 z3.Re(char)、z3.Range(start, end)、z3.Star(re) 等組合子來建構模式。因此，我寫了一個簡單的轉譯層，遞迴地遍歷 greenery 的 Pattern AST，並把它轉成 Z3 的正則表達式。接著，我們只需要把每個未知字元宣告為 Z3 字串物件，並像這樣為每個線索加上斷言：

re = greenery_to_z3(clue.pattern)

string = z3.Concat(chars)
solv.add(z3.InRe(string, re))

可以說簡單多了！那它快嗎？嗯……還算不錯。

一方面——特別是對大尺寸謎題——透過運用我在這篇文章中討論的所有技巧，我們可以快得多地解開謎題。另一方面，使用 Z3 正則表達式的求解器可能是我考慮或實作過的方法中最簡單的，而且它比我最初那個天真的嘗試快了將近 10 倍。

我猜這個模式是可以類推的：如果 Z3 對你的問題領域有第一級的支援，那就值得從那裡開始！不過，Z3 最閃耀的地方在於它是一個非常通用的工具，能為許許多多不同的問題類型提供一致的介面；如果你願意投入心力、做實驗、並運用領域專業知識，很有機會解得更快，代價則是在你這邊增加複雜度。

結論

這是個很有趣的專案！我本來以為這會是個有趣的下午小坑，事實上我最初的腳本也只花了一兩個小時就拼湊出來了。然而，我卻無法擺脫想要優化和更深入了解 Z3 的衝動，從那之後我花了相當多——甚至有點過頭——的時間重構、探索各種變化、跑效能測試、繪圖等等。不過，透過這些過程，我現在對 Z3 和 SMT-LIB 的理解都深入了許多，而這畢竟就是我最初的目標！我很期待未來能找到更多機會，真正把這些技術派上用場。

最後，我想用從這次經驗中得到的一些關於使用 Z3 的心得與教訓來作結。

Z3 支援的功能比我想像的多得多。

我過去大多是在處理整數、位元向量，有時還有陣列的問題時，順帶接觸到 Z3。我在這次學到了它所支援的許多新資料型別與理論，包括：

• 字串、序列與正則表達式
• 代數資料型別
• 未解譯函式，包含遞迴函式

我以前也從未接觸過 Z3 的 tactic 系統，它既可以用來解決超出基礎 SMT 求解器能力的問題，也可以用來實作客製化的重寫／簡化策略，以針對某類問題進行優化。我得知，我個人最喜歡的 Z3 驅動工具 Alive2，就大量使用了 Z3 tactic 來針對 Alive2 所產生的特定表達式進行優化。

Z3 的效能，的確有時相當不穩定、難以預測。

如我前面所提，我隱約知道這個特性，算是偶然聽說過，但這個專案真的讓我深刻體會到了。透過調整我為這個問題想到的各種編碼與方法的組合，即使不算領域相關的剪枝優化，我也能讓求解器的速度相差約 100 倍。而有些效能行為更是令人費解，例如僅僅稍微放寬整數範圍限制，竟帶來了 10 倍的加速！

使用 Z3 列舉來獲得更可預測的效能

關於效能，給一點具體的戰術性建議。

如果你要把某個問題編碼進 Z3，其中需要表示「N 種可能性之一」，而這些可能性本身沒有自然的數值意義（例如，我們並不是要把它們當作整數來相加），那麼我會建議宣告一個新的列舉排序，而不是僅僅用整數來標記它們。

以我的經驗來看，這個改動通常不會有什麼差別，但偶爾卻能避免神祕的效能不穩定與 10 倍的變慢，方法是繞開 Z3 對算術和其他數值特性所擁有的專門知識與求解器。

不過，在可用性上有個要注意的地方：新的排序在每個 Z3 Context 中是全域的，所以如果你（例如）宣告了一個名為「State」的 EnumSort，在不重新啟動程式或建立全新 context 物件的情況下，就無法用相同名稱但不同取值集合來重新宣告它。

Z3 的文件參差不齊，但確實存在

一開始，我發現要找到能回答關於 Z3 內部運作、策略或超越表面用法等深入問題的好文件相當困難，但最終我還是收集了一份不錯的清單。我認為「直接問專家」仍然是使用 Z3 最有效的方法（感謝 Hillel Wayne 在我進行這個專案期間回答了我的一些問題！），不過以下也是我找到的一些很棒的資源：

• Microsoft 的 Z3 Guide，包含其中的 tactic 列表和 求解器選項。
• Programming Z3，一篇由幾位 Z3 開發者撰寫的論文。
• Z3 Internals 詳細介紹了 Z3 底層的運作方式。