第8章 SMTで数独を解く

数独の左上のマスを cell_1_1 という整数にします。この整数は1以上9以下で、初期配置が5なら cell_1_1 = 5 です。同じ行にある九つの整数には、互いに異なるという条件を加えます。 このように、整数についての式をほぼそのままソルバーへ渡せるのがSMTを使う利点です。

SMT は、論理式がある理論のもとで充足可能かを調べる方法です。正式名は Satisfiability Modulo Theoriesで、日本語では「背景理論付き充足可能性」などと訳されます。 整数算術、実数、ビットベクトル、配列、文字列といった理論を扱えます。この章では Z3 と、そのPython APIであるZ3Pyを使います。Z3は複数の理論を 扱うSMTソルバーとして、プログラム解析や検証にも組み込まれています。[1]

ここでいう理論は、整数の加算、等号、大小比較などの記号をどう解釈するか定めた規則です。 Z3Pyの整数記号は、値がすでに決まったPythonの int ではありません。たとえば x + y == 7 はその場でPythonの真偽値を求める比較ではなく、「二つの整数の和が7」という Z3の論理式を作ります。

整数の条件を解いてみる

まず、二つの整数 \(x\) と \(y\) に次の条件を与えます。

\[x+y=7, \qquad x-y=3\]

連立方程式として計算すれば \(x=5, y=2\) です。Z3Pyでは、整数変数と等式をそのまま書けます。

x, y = Ints("x y")
solver = SolverFor("QF_LIA")

# 二つの整数を、連立方程式を満たす値に制約します。
solver.add(x + y == 7)
solver.add(x - y == 3)

result = solver.check()
print(f"status: {result}")
if result == sat:
    # 充足する値をモデルから整数として読み戻します。
    model = solver.model()
    print(f"x: {model.eval(x).as_long()}")
    print(f"y: {model.eval(y).as_long()}")

solver.add() で論理式を追加し、check() で式を同時に満たす値があるか調べます。結果は sat、unsat、unknown のいずれかです。sat なら、条件を満たす値の割り当てを model() から読めます。[2]

status: sat
x: 5
y: 2

ここでいう モデル は、式に現れる記号へ値や意味を割り当て、すべての式を真にするものです。 数独では、81個の整数へ完成盤面の数字を割り当てたものがモデルになります。

SATとの違い

前章で扱ったSATは命題変数を真か偽に割り当て、論理式を満たせるか調べます。数独をSATへ変換する典型的な 方法では、「行 \(r\)、列 \(c\) のマスが数字 \(d\) である」を命題変数 \(p_{r,c,d}\) にします。9×9盤面なら \(9\times9\times9=729\) 個です。整数の大小や 加算を使いたい場合も、真偽の式へ符号化してSATソルバーへ渡します。

SMTでは、左上のマスを一つの整数変数 \(x_{1,1}\) として宣言できます。 1 <= x_1_1 や x_1_1 <= 9 は整数算術の式です。SATが扱う論理構造に、整数算術などの 理論を組み合わせたものと見ると、今回のモデルの違いがつかめます。

変数の個数だけでは速度を比較できません。ソルバー内部の変換や推論が異なり、結果は問題、符号化、 処理系によって変わります。

人間とソルバーの役割分担

段階	人間（Pythonコード）が行うこと	ソルバー（Z3）が行うこと
入力	81個の整数変数を宣言し、範囲・Distinct・初期配置を論理式として追加する	―
探索	―	論理構造をSAT的に分解しつつ、整数算術の理論ソルバーで等式・不等式の整合性を検査する
出力	モデルの各整数を as_long() で読み出し、盤面を復元・検証する	sat（モデル付き）、unsat、または unknown を返す

数独を整数の論理式へ変換する

行 \(r\)、列 \(c\) のマスを整数変数 \(x_{r,c}\) とします。各変数の範囲は次の式です。

\[1 \leq x_{r,c} \leq 9\]

各行、各列、各3×3ブロックには、九つの値が互いに異なるという条件を加えます。Z3Pyの Distinct は、渡した整数式がすべて異なるという論理式を作ります。[3] たとえば一行目は次のように書けます。

solver.add(Distinct(cells[0]))

初期配置があるマスには \(x_{r,c}=d\) を追加します。これで、空きマスを特別な値で表す 必要はありません。入力で使う0は「初期配置なし」を示すだけで、SMTの整数変数は1から9までを 取ります。

各行には1から9の範囲にある整数が九つあり、Distinct によって重複がありません。そのため、 九つの値は1から9を一度ずつ含む順列になります。列とブロックについても同じです。

def build_solver(board: Board):
    """盤面をQF_LIAの式へ変換し、ソルバーと81個の整数変数を返します。"""
    side = isqrt(len(board))
    box = isqrt(side)
    cells = [[Int(f"cell_{row + 1}_{col + 1}") for col in range(side)] for row in range(side)]
    solver = SolverFor("QF_LIA")

    # 各マスは、盤面の大きさに応じた数字だけを取ります。
    for row in range(side):
        for col in range(side):
            solver.add(1 <= cells[row][col], cells[row][col] <= side)

    # 同じ行と列の整数を、すべて異なる値に制約します。
    for row in range(side):
        solver.add(Distinct(cells[row]))
    for col in range(side):
        solver.add(Distinct([cells[row][col] for row in range(side)]))

    # 各ブロックにも、行や列と同じDistinct制約を加えます。
    for box_row in range(0, side, box):
        for box_col in range(0, side, box):
            solver.add(
                Distinct(
                    [
                        cells[row][col]
                        for row in range(box_row, box_row + box)
                        for col in range(box_col, box_col + box)
                    ]
                )
            )

    # 初期配置があるマスは、その整数に固定します。
    for position, given in enumerate(board):
        if given:
            row, col = divmod(position, side)
            solver.add(cells[row][col] == given)

    return solver, cells

Distinct の意味は、任意の二マス \(i,j\) について \(i\ne j\) なら \(x_i\ne x_j\) とすることです。第5章「制約プログラミング」の all_different と直観的には類似しますが、 ここでは整数項に対する論理式を構成しており、CPソルバーのグローバル制約と同じ伝播アルゴリズムの 適用を指示するものではありません。

SolverFor("QF_LIA") は、量化子なし線形整数算術向けのソルバーを作ります。QFは Quantifier-Free（量化子なし）、LIAはLinear Integer Arithmetic（線形整数算術）の略です。今回の 数独モデルには、整数の範囲、等式、不等式と、それらを組み合わせた論理式だけが現れます。 変数同士の乗算や量化子は使いません。Z3が扱う整数算術の範囲と方式は、公式ガイドにも まとまっています。[4]

モデルから完成盤面を読み戻す

check() が sat を返したら、solver.model() でモデルを得ます。各 cell をモデルの もとで評価し、Z3の整数値を as_long() でPythonの整数へ変換して完成盤面を復元します。 復元した盤面は共通検証器へ渡し、初期配置、行、列、ブロックを改めて確認します。

一意性を調べるには、最初のモデルと異なるモデルをもう一度探します。最初の完成盤面を \(m_{r,c}\) とすると、追加する式は次のとおりです。

\[\bigvee_{r,c} x_{r,c} \ne m_{r,c}\]

どこか少なくとも一マスが最初の盤面と異なる、という式です。この式を加えて check() し、 二つ目も sat なら複数解です。unsat なら、最初の盤面以外に解はありません。

def solve(board: Board, limit: int = 1) -> SolveResult:
    solver, cells = build_solver(board)
    solutions: list[Board] = []

    while len(solutions) < limit:
        result = solver.check()
        if result == sat:
            # モデルを完成盤面として読み戻し、別の検証器でも確かめます。
            solution = board_from_model(solver.model(), cells)
            valid, errors = validate_solution(solution, board)
            if not valid:
                raise RuntimeError("invalid Z3 model: " + "; ".join(errors))
            solutions.append(solution)

            # 次のcheckでは、今の盤面と少なくとも一マス違う解を要求します。
            solver.add(
                Or(
                    [
                        cells[row][col] != solution[row * len(cells) + col]
                        for row in range(len(cells))
                        for col in range(len(cells))
                    ]
                )
            )
        elif result == unsat:
            status = "solved" if solutions else "unsat"
            return SolveResult(status, tuple(solutions), search_complete=True)
        elif result == unknown:
            # unknownをunsatとして扱わず、Z3が返す理由も保存します。
            status = "solved" if solutions else "unknown"
            return SolveResult(status, tuple(solutions), False, solver.reason_unknown())
        else:
            raise RuntimeError(f"unexpected Z3 result: {result}")

    return SolveResult("solved", tuple(solutions), search_complete=False)

Z3の結果は三通りに分けます。unknown は、Z3が sat と unsat のどちらかを 決定できなかったという結果です。コードは solver.reason_unknown() も保存し、誤って unsat と表示しないようにしています。

実行と検証

実行手順とオプションは examples/07-smt/README.md にまとめています。最初のモデルを得た後、 そのモデルを除外してもう一度Z3へ問い合わせた結果を含めると、三問の出力は次のようになります。

Z3で三つの盤面を調べた結果

問題	status	解数	search_complete	unique
一意解	solved	1	yes	yes
矛盾	unsat	0	yes	対象外
複数解	solved	2	no	no

一意解問題では、最初のモデルを除外した二回目の問い合わせが unsat になりました。 search_complete: yes は、その問い合わせが最終判定まで終わったことを示します。複数解問題では 二回目も sat となり、共通検証器を通る異なる二盤面が得られました。二解で打ち切るため search_complete は no ですが、一意解でないことの判定には十分です。

解がない場合と、解が複数ある場合

矛盾問題では、初回の判定で unsat が返されます。初期配置を保ちながら、行、列、ブロックの条件をすべて満たす整数の割り当てが存在しないためです。

複数解問題では、最初のモデルを除外した後も判定が sat となり、異なる2つの完成盤面が得られます。2つの解が得られた時点で一意解ではない（複数解を持つ）ことが判定されます。

この方法で分かること

今回の数独モデルは、各整数の範囲が1から9に限られ、すべての制約を量化子なしの線形整数算術で 書きます。Z3が sat を返した場合はモデルから完成盤面を取得し、unsat を返した 場合は、その制約を満たす盤面が存在しないと判定します。

数独の完成盤面は、範囲、Distinct、初期配置の式をすべて満たします。反対に、これらの式を 満たすモデルでは、各行、列、ブロックが1から9までの順列になるため、数独の完成盤面として 成立します。この双方向の対応があり、モデルへの変換によって解を増減させていないことが、 この解法の完全性を支えます。ただし、unknown の場合は充足可能性について結論を出しません。

一意性は、最初のモデルを除外した二回目の問い合わせで調べます。二回目が unsat なら一意、 sat なら複数解です。二回目が unknown なら、一解を得ていても一意性は未判定のままです。 Z3は理論や制限時間などの条件によって unknown を返すことがあるため、一般のSMTプログラムは 三通りを分けて扱います。[2]

この実装は乱数を使いません。ただし、別のZ3バージョンやオプションでは、複数解のうち最初に 返るモデルが変わることがあります。速度についても、SATや制約プログラミングとの優劣はこの 一問の実行結果から判断できません。

参考文献

[1]

Leonardo de Moura and Nikolaj Bjørner. Z3: An Efficient SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems, volume 4963 of Lecture Notes in Computer Science, 337–340. 2008. doi:10.1007/978-3-540-78800-3_24.

[2] (1,2)

Microsoft Research. Basic Commands. URL: https://microsoft.github.io/z3guide/docs/logic/basiccommands/ (visited on 2026-08-08).

[3]

Z3 Project. Z3Py API: Distinct. URL: https://z3prover.github.io/api/html/namespacez3py.html (visited on 2026-08-08).

[4]

Microsoft Research. Arithmetic. URL: https://microsoft.github.io/z3guide/docs/theories/Arithmetic/ (visited on 2026-08-08).