0
0

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?

@ynakayama(Yasuhiro Nakayama)

Python で有限状態ゲームの詰みの強制可能性を判定する

0
Posted at

詰みへ到達する指し手の系列が存在しても、相手が別の合法手を選べる場合には、詰みを強制できるとは限りません。到達可能性は「詰みへ向かう経路が一つ以上あるか」を調べます。強制可能性は「攻撃側が指し手を選び、防御側がどの応手を選んでも、有限手数で詰みに到達するか」を調べます。

この記事では、10 局面・11 遷移の有限状態ゲームを Python で作り、両者を別々に判定します。攻撃側には成功する一手が存在すること、防御側にはすべての合法な応手が成功へつながることを要求し、詰みの終端から後退解析します。

Python で検証する有限状態ゲームの前提

検証環境は Linux、Python 3.13.5 です。追加パッケージは使わず、標準ライブラリのみで実行します。

$ python3 --version
Python 3.13.5

三次元将棋から合法手の状態遷移だけを取り出す

三次元将棋では、駒の位置、成り状態、持ち駒、手番などによって次に指せる合法手が決まります。これらを含む局面全体を一つの状態とし、合法手による次の局面への移行を有向辺として表せます[1]。

今回の入力は、すでに合法手を列挙した後の状態遷移グラフです。各局面について、どちらの手番か、どの後続局面へ進めるか、詰みの終端かを与えます。この抽象化により、盤面上の駒の動きではなく、攻撃側と防御側の選択条件を検証できます。

グラフ上で手番を交替させ、目標となる終端への到達を評価する方法は、到達可能性ゲームとして扱われます[2]。

10 局面の状態遷移グラフを定義する

攻撃側の手番を A、防御側の手番を D で表します。M は防御側の王将が詰んだ終端、E は詰み以外の終端です。終端は指し手を選ぶ局面とは分離します。

局面 手番・分類 後続局面
A0 攻撃側 D1, D2
D1 防御側 A1, A2
A1 攻撃側 M
A2 攻撃側 M
D2 防御側 A3, A5
A3 攻撃側 D2
A5 攻撃側 M
A4 攻撃側 E
M 詰みの終端 なし
E その他の終端 なし

A0 から D1 を選ぶと、防御側の応手が A1 と A2 のどちらであっても、次に M へ進めます。一方、D2 では防御側が A3 を選び、A3 → D2 → A3 という循環を続けられます。D2 → A5 → M の経路も存在するため、到達可能性と強制可能性の判定結果を比較できます。

詰みと詰み以外の終端を区別する

後続局面が空であることだけを勝利条件にすると、E まで詰みとして扱ってしまいます。ここでは詰みの終端集合を {"M"} と明示し、E は勝利集合に加えません。

防御側の局面に全称条件を適用するときも、後続局面が一つ以上あることを確認します。Python の all([]) は True になるため、空集合をそのまま全称条件に渡すと終端の分類を誤ります。

詰みへの到達可能性を探索する

まず、手番による選択権を考慮せず、詰みの終端 M に至る経路を探索します。訪問済み集合を使えば、A3 と D2 の循環に入っても探索は終了します。

この判定で A3 は True です。A3 → D2 → A5 → M という系列を選べるためです。ただし D2 の応手を選ぶのは防御側なので、この結果は攻撃側の勝利保証を意味しません。

存在条件と全称条件で詰みの強制可能性を求める

詰みの強制可能性では、後続局面の選択者を区別します。攻撃側の手番なら、勝利集合に進む合法手が少なくとも一つあれば十分です。防御側の手番なら、すべての合法な応手が勝利集合へ進む必要があります。

手番 判定条件 Python での実装
攻撃側 成功する後続局面が少なくとも一つある any(child in winning for child in children)
防御側 合法な後続局面が存在し、そのすべてが成功する bool(children) and all(child in winning for child in children)

存在条件と全称条件を交互に評価する構造は、交替計算の基本的な考え方にも対応します[3]。ここでは計算量クラスを論じるのではなく、手番に応じた分岐判定に利用します。

詰みの終端から固定点まで集合を拡張する

最初の勝利集合を W0 = {"M"} とし、次の規則で新しい局面を追加します。

  • 攻撃側の局面では、後続局面の少なくとも一つが現在の勝利集合に属するとき追加します。
  • 防御側の局面では、後続局面が一つ以上あり、すべてが現在の勝利集合に属するとき追加します。

各反復で新しく追加される局面を同時に確定します。反復番号は、そこから必ず詰みに到達させられる状態遷移回数の最小の上限 r(S) になります。新しい局面が追加されなくなった集合が最小固定点です。

以下が探索、後退解析、検証を含む実行用コード全文です。

forced_mate.py
from collections import deque


SUCCESSORS = {
    "A0": ("D1", "D2"),
    "D1": ("A1", "A2"),
    "A1": ("M",),
    "A2": ("M",),
    "D2": ("A3", "A5"),
    "A3": ("D2",),
    "A5": ("M",),
    "A4": ("E",),
    "M": (),
    "E": (),
}

TURN = {
    "A0": "attacker",
    "A1": "attacker",
    "A2": "attacker",
    "A3": "attacker",
    "A4": "attacker",
    "A5": "attacker",
    "D1": "defender",
    "D2": "defender",
}

MATE = {"M"}
OTHER_TERMINAL = {"E"}
TERMINAL = MATE | OTHER_TERMINAL


def validate_graph():
    assert len(SUCCESSORS) == 10
    assert sum(len(children) for children in SUCCESSORS.values()) == 11
    assert set(SUCCESSORS) == set(TURN) | TERMINAL
    assert set(TURN).isdisjoint(TERMINAL)
    assert MATE.isdisjoint(OTHER_TERMINAL)

    for state, children in SUCCESSORS.items():
        assert all(child in SUCCESSORS for child in children)
        if state in TERMINAL:
            assert not children
        else:
            assert children
            for child in children:
                if child in TURN:
                    assert TURN[state] != TURN[child]


def reachable_mate(start):
    queue = deque([start])
    visited = set()

    while queue:
        state = queue.popleft()
        if state in visited:
            continue
        visited.add(state)
        if state in MATE:
            return True
        queue.extend(SUCCESSORS[state])

    return False


def forced_mate():
    winning = set(MATE)
    rank = {state: 0 for state in MATE}
    depth = 0

    while True:
        added = set()
        for state, turn in TURN.items():
            if state in winning:
                continue
            children = SUCCESSORS[state]
            if turn == "attacker":
                accepted = any(child in winning for child in children)
            else:
                accepted = bool(children) and all(
                    child in winning for child in children
                )
            if accepted:
                added.add(state)

        if not added:
            break
        depth += 1
        winning.update(added)
        rank.update({state: depth for state in added})

    return winning, rank


def main():
    validate_graph()
    winning, rank = forced_mate()

    assert winning == {"M", "A1", "A2", "A5", "D1", "A0"}
    assert rank == {
        "M": 0,
        "A1": 1,
        "A2": 1,
        "A5": 1,
        "D1": 2,
        "A0": 3,
    }
    assert reachable_mate("A0")
    assert reachable_mate("A3")
    assert reachable_mate("D2")
    assert not reachable_mate("A4")
    assert not reachable_mate("E")
    assert "A3" not in winning and "D2" not in winning
    assert "A4" not in winning and "E" not in winning

    for state in winning - MATE:
        children = SUCCESSORS[state]
        if TURN[state] == "attacker":
            assert any(
                child in rank and rank[child] < rank[state]
                for child in children
            )
        else:
            assert all(rank[child] < rank[state] for child in children)

    for state in ("A0", "A3", "D2", "A4"):
        print(
            f"{state}: reachable={reachable_mate(state)}, "
            f"forced={state in winning}"
        )
    print("winning:", ", ".join(sorted(winning)))
    print("ranks:", ", ".join(f"{s}={rank[s]}" for s in sorted(rank)))
    print("all assertions passed")


if __name__ == "__main__":
    main()

reachable_mate() は探索経路の存在だけを調べ、forced_mate() は終端集合から手番ごとの条件で勝利集合を増やします。追加される局面を一反復ごとに確定するため、rank はその局面が初めて勝利集合に入った段階と一致します。

固定点と循環局面を検証する

コードを forced_mate.py として保存し、実行します。

$ python3 forced_mate.py
A0: reachable=True, forced=True
A3: reachable=True, forced=False
D2: reachable=True, forced=False
A4: reachable=False, forced=False
winning: A0, A1, A2, A5, D1, M
ranks: A0=3, A1=1, A2=1, A5=1, D1=2, M=0
all assertions passed

固定点へ至る過程を整理すると、次のようになります。

段階 新しく追加する局面 判断の根拠
W0 M 詰みの終端
W1 A1, A2, A5 攻撃側が一手で M へ進める
W2 D1 防御側の応手 A1, A2 が両方とも W1 にある
W3 A0 攻撃側が D1 を選べる
W4 追加なし 固定点に到達

勝利集合は {M, A1, A2, A5, D1, A0} です。A0 で攻撃側が D1 を選べば、相手の応手にかかわらず高々 3 回の状態遷移で M に到達します。r(A0) = 3 は、このモデル内で保証できる遷移回数の最小の上限です。

詰みへの経路が存在しても強制できない局面を確認する

A3 からは A3 → D2 → A5 → M という経路があるため、reachable_mate("A3") は True です。しかし D2 の手番で防御側は A3 を選べます。A3 は D2 に戻るしかないため、防御側はこの応手を繰り返して詰みを回避できます。

同じ理由で D2 も勝利集合に入りません。D2 の後続局面のうち A5 は勝利集合に属しますが、もう一つの A3 が属さないためです。この反例により、グラフ探索の到達可能性と、相手の全応手を考慮した強制可能性が異なることを確認できます。

一方、勝利集合に入る各局面には r(S) が定義されます。攻撃側は順位が減少する後続局面を選び、防御側のすべての応手も順位を減少させます。順位は 0 以上の整数なので、この選択を続けると有限回で r = 0、すなわち詰みの終端へ到達します。コード末尾の assertion は、この順位の減少条件も調べています。

三次元将棋への適用範囲と制約

ここで検証したのは、合法な後続局面がすべて与えられた有限状態ゲームです。実際の三次元将棋へ適用するには、駒の立体的な移動、走り駒の遮断、王将の安全性、持ち駒、成りなどを反映して、各局面の合法手を生成する処理が必要になります。

また、同一盤面に戻ることによる終局規則など、履歴に依存する判定を採用する場合は、その判定に必要な情報も状態へ含めます。そうして区別した終端局面のうち、詰みを勝利集合の初期値に設定します。

このモデルで得られる固定点は、相手の応手にかかわらず有限回の状態遷移で詰みを強制できる局面集合です。A3 と D2 のように詰みへの経路だけが存在する局面は除外され、A0 のように防御側のすべての応手に対応できる局面が含まれます。局面数の大きい将棋系ゲームでも、判定の基準となる存在条件・全称条件・終端分類は同じ形で使用できます。

参考文献

  1. id774, 三次元将棋で詰みを強制できる局面はどう決まるのか（2026-10-27）. https://blog.id774.net/entry/2026/10/27/5822/
  2. Nathanaël Fijalkow (ed.), Introduction（2026-04-25）. https://doi.org/10.1017/9781009500678.002
  3. Ashok K. Chandra, Dexter C. Kozen, Larry J. Stockmeyer, Alternation（1981-01）. https://doi.org/10.1145/322234.322243
0
0
0

Register as a new user and use Qiita more conveniently

  1. You get articles that match your needs
  2. You can efficiently read back useful information
  3. You can use dark theme
What you can do with signing up
Sign upLogin
0
0

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?