第10章モデル検査で数独を解く¶

数独の初期配置を初期状態とします。行優先の固定順で次の空きマスへ数字を入れると、次の状態へ移ります。同じ行、列、ブロックで数字が重なる移り方は禁止します。この操作を空きマスの数だけ繰り返し、完成盤面へ到達する経路があるか調べます。

モデル検査は、状態と状態遷移で表したシステムが、指定した性質を満たすか検査する方法です。通常は回路や制御器、通信プロトコルなど、時間とともに状態が変わるシステムの検証に使われます。有限状態のシステムと時相論理による性質を組み合わせる方法は、モデル検査の初期の研究から扱われています。 [1]

数独は完成盤面を探索する静的な問題です。本章では「一マス埋める」操作を時間の一ステップとしてモデル化し、状態遷移系を構築します。状態、遷移、および到達不能性の検証における「反例」の対応をコードにより検証します。

到達経路を反例として得る¶

小さな例として、入口 entrance、通路 hall、目的地 goal の三部屋を移動します。入口では入口に留まるか通路へ進み、通路では留まるか目的地へ進めます。目的地へ着いた後はそこに留まります。

この章で使うSMV言語の表記¶
表記	読み方
`VAR`	状態変数の宣言セクション
`ASSIGN`	初期値と次状態の規則を書くセクション
`init(v) := 値`	変数 `v` の初期値
`next(v) := case ... esac`	次の状態で `v` が取り得る値。条件分岐で記述する
`{a, b}`	`a` または `b` のどちらかを非決定的に選ぶ
`INVAR 式`	すべての状態で常に満たす不変条件
`LTLSPEC G 式`	「どの時点でも式が成り立つ」という検査対象の性質

MODULE main

VAR
  room : {entrance, hall, goal};

ASSIGN
  init(room) := entrance;
  next(room) := case
    room = entrance : {entrance, hall};
    room = hall : {hall, goal};
    TRUE : goal;
  esac;

-- 「goalへは到達しない」という性質を検査する。
-- 偽なら、反例の実行経路がgoalまでの道順になる。
LTLSPEC NAME goal_is_unreachable := G room != goal;

VAR は状態変数、ASSIGN は初期値と次状態の規則を宣言する箇所です。case から esac までは条件分岐で、どの条件にも当てはまらない場合は TRUE の行を使います。LTLSPEC は検査する性質を指定します。

room が現在の状態です。init(room) は初期状態、next(room) は次に取り得る状態を表します。波括弧で二つの値を並べた箇所は、どちらへ移るかを一つに決めていません。このような選択を 非決定的 な遷移と呼びます。これは乱数で一つを選ぶという意味ではなく、可能な次状態をすべて残すという意味です。

最後の G room != goal は「どの時点でも部屋は goal ではない」という性質です。G は線形時相論理（LTL）の演算子で、その後のすべての状態で式が成り立つこと（Globally）を表します。モデル検査器は、初期状態から始まるすべての実行経路についてこの性質を調べます。一本でも goal へ着く経路があれば性質は成り立たないため、検査結果は偽になります。

property: goal is unreachable
result: false
counterexample: entrance -> hall -> goal

反例 entrance -> hall -> goal は、検査した性質を破る実行経路です。同時に、入口から目的地へ到達できることを示す経路でもあります。「目的地へ到達しない」という性質を検査し、その反例を到達経路として使うのが、この章の手順です。

盤面を状態と遷移へ変換する¶

9×9数独では、81個のマスを 0..9 の状態変数にします。0 はまだ埋めていないマスです。もう一つ、何個目の空きマスを埋めているかを示す step も用意します。空きマスが \(m\) 個なら、step の範囲は0から \(m\) です。

初期状態では、ヒントのマスをその数字に、空きマスを0にします。空きマスは行優先の固定順で埋めます。step = k の遷移では、\(k\) 番目の空きマスだけに1から9のいずれかを入れ、 step を1増やします。ほかのマスは値を変えません。

同じ行、列、ブロックの二マスについて、次の条件をすべての状態に課します。

\[x_i=0 \lor x_j=0 \lor x_i\ne x_j\]

どちらかが空なら許し、両方に数字が入っているなら異なる値を要求する式です。nuXmvでは、常に満たす状態制約を INVAR で記述します。非決定的に選んだ数字が重複を起こす遷移は、この制約を満たさないため、実行経路に含まれません。

def build_model(board: Board, excluded: tuple[Board, ...] = ()) -> str:
    """盤面を有限状態機械として表すnuXmvモデルを作ります。"""
    side = isqrt(len(board))
    empty_cells = [index for index, value in enumerate(board) if value == 0]
    order = {index: step for step, index in enumerate(empty_cells)}
    choices = "{" + ", ".join(str(digit) for digit in range(1, side + 1)) + "}"

    lines = ["MODULE main", "", "VAR", f"  step : 0..{len(empty_cells)};"]
    lines.extend(
        f"  {cell_name(index, side)} : 0..{side};"
        for index in range(len(board))
    )

    lines.extend(("", "ASSIGN", "  init(step) := 0;"))
    if empty_cells:
        lines.extend(
            (
                "  next(step) := case",
                f"    step < {len(empty_cells)} : step + 1;",
                "    TRUE : step;",
                "  esac;",
            )
        )
    else:
        lines.append("  next(step) := step;")

    for index, given in enumerate(board):
        name = cell_name(index, side)
        lines.append(f"  init({name}) := {given};")
        if given:
            lines.append(f"  next({name}) := {name};")
        else:
            # このマスの手番だけ、1から盤面サイズまでの値を非決定的に選びます。
            lines.extend(
                (
                    f"  next({name}) := case",
                    f"    step = {order[index]} : {choices};",
                    f"    TRUE : {name};",
                    "  esac;",
                )
            )

    # 同じ行、列、ブロックにある二マスは、0以外の同じ値を取れません。
    peer_pairs = {
        tuple(sorted((first, second)))
        for unit in units(board)
        for offset, first in enumerate(unit)
        for second in unit[offset + 1 :]
    }
    lines.append("")
    for first, second in sorted(peer_pairs):
        left = cell_name(first, side)
        right = cell_name(second, side)
        lines.append(f"INVAR {left} = 0 | {right} = 0 | {left} != {right};")

    # 全空きマスを埋めた状態のうち、既に見つけた盤面は目標から外します。
    goal = f"step = {len(empty_cells)}"
    for solution in excluded:
        goal += f" & !{exclusion_expression(solution)}"
    lines.extend(
        (
            "",
            "DEFINE",
            f"  goal := {goal};",
            "",
            "-- goalへ到達しないという安全性を、既知の最大深さで検査します。",
            "LTLSPEC NAME goal_is_unreachable := G !goal;",
        )
    )
    return "\n".join(lines) + "\n"

step = m なら、すべての空きマスを一度ずつ埋め終えています。途中の各状態で重複を禁止しているので、この状態を完成状態 goal として扱えます。初期配置も状態変数の初期値として保たれます。

限定した長さの遷移を調べる¶

この章では nuXmv 2.2.0を使います。nuXmvは有限状態と無限状態の同期遷移系を扱うモデル検査器で、有限状態向けのSATベース手法や、無限状態向けのSMTベース手法などを備えています。[2]

採用したのは限定モデル検査（BMC）です。BMCは状態遷移を指定した長さまで展開し、性質を破る経路があるかSATソルバーで調べます。[3] 初期状態を \(I\)、遷移関係を \(T\) とすると、深さ \(m\) で完成状態へ到達する問い合わせは、おおよそ次の形です。

\[I(s_0) \land \bigwedge_{k=0}^{m-1}T(s_k,s_{k+1}) \land goal(s_m)\]

たとえば \(m=2\) なら、式は \(I(s_0)\land T(s_0,s_1)\land T(s_1,s_2)\land goal(s_2)\) です。初期状態から二回遷移し、二回目の後に完成状態へ着く経路を一つ探します。

この式を満たせれば、\(s_0\) から \(s_m\) までの値が反例経路として返ります。満たせない場合は、その長さの経路では完成状態へ到達できません。サンプルはnuXmvの check_ltlspec_bmc_onepb を使い、一つの境界に対応するSAT問題をMiniSatで検査します。 [4]

def check_invariant(model_text: str, nuxmv: str, bound: int) -> InvariantResult:
    """指定した深さで、目標へ到達しないという性質を検査します。"""
    with tempfile.TemporaryDirectory(prefix="sudoku-nuxmv-") as directory:
        model_path = Path(directory) / "sudoku.smv"
        model_path.write_text(model_text, encoding="utf-8")
        commands = "\n".join(
            (
                f"read_model -i {model_path}",
                "go_bmc",
                f"check_ltlspec_bmc_onepb -P goal_is_unreachable -k {bound} -l X",
                "quit",
                "",
            )
        )
        try:
            completed = subprocess.run(
                [nuxmv, "-int"],
                input=commands,
                text=True,
                capture_output=True,
                timeout=120,
                check=False,
            )
        except subprocess.TimeoutExpired:
            return InvariantResult("unknown", "nuXmv timed out after 120 seconds")

    output = completed.stdout + completed.stderr
    if completed.returncode != 0:
        raise RuntimeError(f"nuXmv exited with {completed.returncode}:\n{output}")
    if re.search(r"-- specification .* is false", output):
        return InvariantResult("counterexample", output)
    if "-- no counterexample found with bound" in output:
        return InvariantResult("no_counterexample", output)
    if re.search(r"-- specification .* is unknown", output):
        return InvariantResult("unknown", output)
    raise RuntimeError("nuXmvの検査結果を読み取れませんでした:\n" + output)

BMCでは、任意に決めた深さまで反例がなかっただけで、一般に「今後も反例はない」とは言えません。この数独モデルでは、次の三点から空きマス数 \(m\) が完全な上界になります。

step は遷移ごとに必ず1増えます。
どの完成盤面も、固定順にその数字を置けば \(m\) 回の遷移で到達できます。
step = m の後は、マスも step も変化しません。

したがって、深さ \(m\) のSAT問題が充足不能なら、より長い経路で新しい完成盤面が現れることもありません。この結論はBMC一般の性質ではなく、この章で作った遷移モデルに固有のものです。

反例から盤面を復元する¶

性質が偽なら、nuXmvは初期状態から完成状態までの反例を表示します。各状態には、その時点で変わったマスと step が含まれます。コードはマスの値を順に上書きして最終状態を復元し、共通検証器で初期配置、行、列、ブロックを確認します。nuXmvの反例では、前の状態から変わらない変数は省略されることがあります。省略されたマスは以前の値を保つものとして読みます。

一意性を調べるときは、最初に得た完成状態だけを goal から除きます。最初の盤面を \(a_1,\ldots,a_{81}\)、最終状態のマスを \(x_1,\ldots,x_{81}\) とすると、二回目の目標は次の式です。

\[step=m \land \lnot\bigwedge_{i=1}^{81}(x_i=a_i)\]

別の反例が出れば二解目です。深さ \(m\) で反例が存在しない状態は、最初の盤面以外の完成状態へ到達不能であることを意味し、一意解であると確定します。

def solve(board: Board, nuxmv: str, limit: int = 1) -> SolveResult:
    solutions: list[Board] = []
    checks = 0
    bound = sum(value == 0 for value in board)

    while len(solutions) < limit:
        # 見つけた盤面を目標から除き、別の完成状態へ到達できるか再検査します。
        model = build_model(board, tuple(solutions))
        result = check_invariant(model, nuxmv, bound)
        checks += 1

        if result.outcome == "counterexample":
            # 「到達しない」が偽なので、反例は完成状態までの実行経路です。
            solution = solution_from_trace(result.output, board)
            if solution in solutions:
                raise RuntimeError("除外した盤面が再び返されました")
            solutions.append(solution)
        elif result.outcome == "no_counterexample":
            status = "solved" if solutions else "unsat"
            return SolveResult(status, tuple(solutions), True, checks)
        else:
            status = "solved" if solutions else "unknown"
            return SolveResult(status, tuple(solutions), False, checks, "BMC returned unknown")

    return SolveResult("solved", tuple(solutions), False, checks)

第8章「SMT」の手法では、完成盤面を表す81個の整数へ範囲と Distinct の式を加え、その式を満たす値を直接問い合わせます。本章では初期状態、遷移、完成状態を分離し、途中の状態を含む遷移経路を検査します。今回のBMCは内部でSAT問題へ変換されますが、定式化で定義しているのは最終解の状態のみならず、各ステップにおける状態変化と遷移関係です。

実行と検証¶

実行手順とオプションは examples/11-model-checking/README.md にまとめています。checks は nuXmvへ問い合わせた回数です。最初の検査で解を探し、解が得られた場合だけ、その完成盤面を除外した二回目の検査で一意性を調べます。

nuXmvのBMCで三つの盤面を調べた結果¶
問題	`status`	検査回数	解数	`search_complete`	`unique`
一意解	`solved`	2	1	`yes`	`yes`
矛盾	`unsat`	1	0	`yes`	対象外
複数解	`solved`	2	2	`no`	`no`

一意解問題では、一回目の反例の最終状態から完成盤面を復元しました。二回目は最初の盤面を除外し、完全な展開限界まで別の反例がないことを確認しています。複数解問題では二回目にも反例が見つかり、そこから異なる完成盤面を復元した時点で検査を止めています。

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

矛盾問題では、完成状態へ至る深さ \(m\) の反例が存在しません。モデル固有の完全な限界まで検査した結果、反例が存在しないことから解なし（unsat）と判定されます。

複数解問題では、最初の完成状態を除外した2回目の検査においても別の反例（解盤面へ至る経路）が検出され、一意解ではない（複数解を持つ）ことが判定されます。

この方法で分かること¶

数独の完成盤面があれば、固定したマス順にその数字を置く経路を作れます。途中の盤面も重複を起こさないため、生成した遷移モデルで goal へ到達します。反対に、goal へ到達した経路はすべての空きマスを埋め、各行、列、ブロックの重複禁止条件を満たします。1から9までの九マスが重複しないので、それぞれ1から9の順列です。この双方向の対応により、反例の最終状態を数独の解と対応付けます。

最初の検査で完全な上界まで反例がなければ解なしです。一解を目標から除いた二回目の検査で反例がなければ一意解、反例があれば複数解です。処理系が制限時間などで検査を完了しなければ、解なしとはせず unknown とします。

この実装は乱数を使いません。ただし、許される経路のうちどの反例を先に返すかは、nuXmvや SATソルバーの版、内部設定によって変わる可能性があります。状態変数や境界が増えれば、BMCが作る SAT問題も大きくなります。今回の結果だけから、別のモデル検査アルゴリズムやSAT、SMTとの速度差は判断できません。

参考文献¶

[1]

Edmund M. Clarke, E. Allen Emerson, and A. Prasad Sistla. Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications. ACM Transactions on Programming Languages and Systems, 8(2):244–263, 1986. doi:10.1145/5397.5399.

[2]

Roberto Cavada, Alessandro Cimatti, Michele Dorigatti, Alberto Griggio, Alessandro Mariotti, Andrea Micheli, Sergio Mover, Marco Roveri, and Stefano Tonetta. The nuXmv Symbolic Model Checker. In Computer Aided Verification, volume 8559 of Lecture Notes in Computer Science, 334–342. Springer, 2014. doi:10.1007/978-3-319-08867-9_22.

[3]

Armin Biere, Alessandro Cimatti, Edmund M. Clarke, and Yunshan Zhu. Symbolic Model Checking without BDDs. In Tools and Algorithms for the Construction and Analysis of Systems, volume 1579 of Lecture Notes in Computer Science, 193–207. Springer, 1999. doi:10.1007/3-540-49059-0_14.

[4]

Marco Bozzano, Roberto Cavada, Alessandro Cimatti, Michele Dorigatti, Alberto Griggio, Alessandro Mariotti, Andrea Micheli, Sergio Mover, Marco Roveri, and Stefano Tonetta. nuXmv 2.2.0 User Manual. Fondazione Bruno Kessler, 2026. URL: https://nuxmv.fbk.eu/downloads/nuxmv-user-manual.pdf (visited on 2026-08-08).

第10章 モデル検査で数独を解く¶