しばらく前から、Z3や、より広くはSMTソルビングに夢中になっていた。最近育休中に正規表現クロスワードパズルの存在を思い出し、Z3を使ったソルバーを書くという沼に自ら飛び込んでしまった。

せいぜい半日で手早くソルバーを作るつもりだったが、結局Z3のパフォーマンスの理解やデバッグにのめり込み、予想をはるかに超えてZ3やSMTについて学ぶことになった。この記事では、自分のアプローチと最初のソルバーについて説明し、その後に試した様々な改善やバリエーションを掘り下げていく。

コードはすべてGitHubで公開しているので、興味があれば追ってみたり最終的な成果を確認したりしてほしい。

正規表現クロスワード

簡単におさらいしておくと、正規表現クロスワードは、（未知の）文字のグリッドを埋めるパズルだ。各マスに入る文字を当てるのだが、与えられた正規表現の集合によって制約される。グリッドを埋めたとき、各行や列が対応する正規表現にマッチしなければならない。今回は特にregexleというバリエーションを解くことにした。六角形のグリッドを使うものだが、コードの大部分は他のバリエーションにも容易に適応できる。

正規表現をDFAとして扱う

Z3のような制約ソルバーでパズルを解くには、「この文字列がこの正規表現にマッチする」という制約をエンコードする方法を見つけ、あとはすべてのヒントをアサートして、すべての制約を満たすグリッドを問い合わせればよい。

最初にすぐに思いついたのは、正規表現が正規言語¹を記述するのだから、決定性有限オートマトンで認識できるという事実を利用することだった。つまり、正規表現をDFAにエンコードし、その遷移関数を使ってZ3で正規表現のマッチングを表現できる²。

つまり、3文字の文字列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

また、1つの正規表現に対する様々な表現や解析をまとめる小さな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を使っていた。六角形グリッドで動作するのだが、六角グリッドと3つの異なるヒントの軸との間で座標をマッピングする作業が、正直この演習で最も難しい部分の一つだった！ ただ、その部分は省略するとして、コード自体はとてもシンプルだ:

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,
    )

ソルバーのパフォーマンス

ここまで来て——すべての部品を組み合わせたところで——クロスワードを解けるようにはなったが、とにかく…耐え難いほど遅かった。3×3のパズルでも、M1 MacBook AirでZ3の実行に10分以上かかるものがあった！ Z3に複数コアを使わせる方法を見つけ、わずかながら定数倍の高速化はできたが、根本的に遅すぎると感じた。

漠然とした内部的な勘では、Z3ならこれらのパズルをミリ秒で解けるはずだと思っていた。だからこそ、なぜソルバーがこれほど遅いのかをデバッグして理解し、高速化する方法を探ることに時間を費やさざるを得ないと感じた。

当時の私はZ3の完全な初心者で、何を試せばよいのか、何を見ればよいのかもよく分かっていなかった。この後に続く冒険の中で、ものすごく多くのことを学ぶことになる。最終的には期待通りの速度を達成できたが、その過程では多くの空振りや驚きがあった。

このプロジェクト以前から、SMTソルバーはパフォーマンス特性が極めて不透明で不安定だという漠然とした認識はあった。それでも、たとえかなり単純だと思っていた問題でさえ、その通りになる度合いには驚かされた。遭遇した挙動の多くは今でも完全には理解できていない。

まずは、最終的に最も大きな影響を与えた2つの変更——私の知る限り高速で信頼性の高いソルバーを生み出したもの——を紹介し、その後、うまくいかなかった試みやその他の奇妙な挙動についても共有しよう。

状態の枝刈り

前述の通り、私は（当時は）Z3の専門家ではなかったが、正規表現についてはよく理解していた。そこで最初に思いついたのは、ドメイン固有の解析で追加の制約を生成し、Z3を助けることだった。

動機付けの例として、これを書いている時点での本日のregexleに出てきた正規表現(NR|Q|I)+を考えてみよう。答えにはN、R、Q、Iしか含まれ得ないことは一目で明らかだ。しかし私のコードはすべてのマスでアルファベットをA-Zに固定しており、他の文字を除外するのはZ3に任せきりになっている。実際の有効なアルファベットを検出して、Z3の問題にエンコードしたらどうだろうか？

人間なら正規表現のソースを見てすぐにその性質に気づく。そのためのコードを書くこともできるが、一般にはそれほど単純ではない。しかし、すでに持っている遷移表に対して同様の解析ができることに気づいた。しかも、今や私はエンジニアであると同時に科学者でもあるので、numpyのトリックを使って、わずか数行でやってみることにした。

FSMの状態が「dead（行き止まり）」であるとは、その状態から受理状態へ至る遷移列が存在しないことをいう。greeneryの解析パスのおかげで最小化されたFSMを扱っているため、dead状態は高々1つしか存在せず、その状態からのすべての遷移は自己ループになることが分かっている。その条件を探すことでdead状態を簡単に検出できる:

# 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))

（dead状態は0個または1個しか存在しないが、set[int]を使うことで両方のケースを集合の反復で統一的に扱え、int | Noneを使うより少しすっきりすると感じた）

dead状態が分かれば、deadな文字を、任意の初期状態から常にdead状態へ遷移する文字として定義できる:

@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

また、特定の状態から見て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の関数としてエンコードし、各(状態, 文字)ペアについて点ごとのアサーションでその振る舞いを固定すると説明した。最終的に、遷移を解釈されない関数としてではなく明示的な式として表現することで、より良いパフォーマンスが得られることを発見した。そうすることでZ3が探索に頼るのではなく等式的に関係を推論するよう促されたのだろうと推測しているが、正直なところはよく分かっていない。

遷移表を、（状態, 文字）の入力を解析する明示的なif-thenの連鎖として表現するPython関数を書いてみよう。まずは1つの変数に対する「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の異なる機能を示す2つの戦略を見つけた。

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」という名のタクティクがある。Z3のタクティクは、コアのSMTソルバーの外側で、ユーザー主導の簡約化や変換パスを可能にするものだ。macro-finderは多くの変換を実装しているが、最も基本的なところでは、関数の意味を「定義」するforallアサーションを見つけ、その関数の呼び出し箇所に実質的にコピー＆ペーストする。つまり、我々のforallバリアントを「毎回明示的な式」バリアントに変換するのだが、C++で実装されZ3コアにより近いところで動作するため、非常に効率的にそれを行う。

3つのアプローチ（明示的な式、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に切り替えた当初、大幅な高速化が見られた！

しかし、その高速化の理由についての私の推測は、良くても部分的にしか正しくなかったことが分かった。同じプロットに2つの新しいパネルを追加したものがこちらだ。1つは点ごとの関数定義を依然として使うが後述する小さな変更を加えたもの、もう1つは上で説明した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のトレースや統計情報を調べてみると、Enumの場合にxfer(st, ch) == st_nextというアサーションを通じて等式的に推論するのにZ3がなぜか苦労し、少し余分な探索とバックトラックが必要になっているように見えるが、なぜそうなるのかは分からない。

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が何よりもまず非常に汎用的なツールであり、多くの異なる問題タイプに対して統一的なインターフェースを提供することに長けている点が最大の強みだ。努力を惜しまず、実験を行い、ドメイン固有の専門知識を投入する気があるなら、複雑さを自分側で引き受ける代わりに、より速くインスタンスを解ける可能性は十分にある。

結論

楽しいプロジェクトだった！ 当初はちょっとした気晴らしのつもりで、午後の暇つぶしになればと思っていたし、実際最初のスクリプトは1〜2時間でさっと作れた。しかし、最適化したい、Z3をもっと理解したいという衝動を抑えられず、それ以来、リファクタリングやバリエーションの探索、ベンチマークの実行、プロットの作成などに、やや不合理なほどの時間を費やしてしまった。とはいえ、そのおかげでZ3とSMT-LIBについての理解が以前よりはるかに深まったのだから、そもそもの当初の目標は達成できたわけだ！ 今後、これらを本気で活用する機会をもっと見つけていくのが楽しみだ。

最後に、この経験から得たZ3を扱う上でのいくつかの振り返り／教訓で締めくくろう。

Z3は思っていたよりもはるかに多くの機能をサポートしている。

これまでZ3には、整数やビットベクトル、時には配列を含む問題のソルバーとして（通りすがりに）触れてきた程度だった。Z3がサポートする多くの新しいデータ型や理論について学んだ:

• 文字列、シーケンス、正規表現
• 代数的データ型
• 解釈されない関数、再帰関数を含む

Z3のタクティクシステムについても、これまで出会ったことがなかった。タクティクは、ベースのSMTソルバーの手に負えない問題を解くのを助けるためにも、特定の問題クラスに最適化するためのカスタムな書き換え／簡約化戦略を実装するためにも使える。私のお気に入りのZ3ベースのツールであるAlive2が、Alive2が生成する特定の種類の式に最適化するためにZ3のタクティクを多用していることも知った。

Z3のパフォーマンスは、確かに時にかなり不安定で予測不可能だ。

前述の通り、この性質については以前から漠然と耳にしてはいたが、このプロジェクトで本当に身にしみて実感した。この問題に対して思いついた様々なエンコーディングやアプローチの組み合わせを調整することで、ドメイン固有の枝刈り最適化を除いても、ソルバーを100倍も高速化したり低速化したりできた。そして、整数の範囲境界をわずかに緩めることで10倍高速化したといった、不可解なパフォーマンス挙動もいくつかあったのだ！

より予測可能なパフォーマンスのためにZ3の列挙型を使おう

パフォーマンスに関する、ちょっとした戦術的／具体的なアドバイスだ。

もしZ3に「N個の可能性のうちの1つ」を表すような問題をエンコードしたい場合で、それらの可能性が自然に数値的な解釈を持たない（例えば、それらを整数として扱って合計したりしない）なら、単に整数でラベル付けするのではなく、新しい列挙ソートを宣言することをお勧めする。

私の経験が参考になるなら、この変更はしばしば何の違いも生まないが、時折、数に関するZ3の専門知識や算術などのソルバーを回避することで、不可解なパフォーマンスの不安定性や10倍のスローダウンを避けられることがある。

ただし、使い勝手に関する注意点が一つある。新しいソートはz3のContextごとにグローバルなので、例えば「State」という名前のEnumSortを宣言した場合、プログラムを再起動したりまったく新しいコンテキストオブジェクトを作成したりしない限り、同じ名前で異なる値の集合を持つ別のものを再宣言することはできない。

Z3のドキュメントはまだらだが、存在はする

当初は、Z3の内部や戦略、表面的な使い方を超えた深い疑問に答えてくれる良いドキュメントを見つけるのがかなり難しいと感じていたが、最終的にはかなりのリストを集めることができた。「専門家に聞く」が依然としてZ3を使う上で圧倒的に最も効果的な方法だと思う（このプロジェクト中に質問に答えてくれたHillel Wayne氏に感謝！）が、他にも見つけた優れたリンクをいくつか紹介しておこう:

• MicrosoftのZ3 Guide。そのタクティクの一覧やソルバーオプションを含む。
• Z3開発者の何人かによる論文Programming Z3。
• Z3 Internalsには、Z3が内部でどのように動作するかについての優れた詳細が含まれている。