ナイトツアー ― すべてのマスを1回ずつ訪れるルートを探す

ナイトツアー ― すべてのマスを1回ずつ訪れるルートを探す#

この章で学ぶこと#

チェスのナイト（騎士）が、8×8 の盤面のすべてのマスを1回ずつ訪れるルートを探します。最後はスタート地点に戻る「閉じたルート」にします。

各マスに「何番目に訪れたか」を表す整数を割り当てる
「隣り合う番号はナイトの移動先にある」を PbEq() で書く
ルールをそのまま制約にすると、Z3 が数秒でルートを見つける

ナイトツアー問題は、OrToolsでナイトツアー問題を解くでも扱っています。

考え方#

各マスに 0 から 63 までの整数を割り当て、**その数が「何番目に訪れたか」**を表すようにします。

すべてのマスの値は 0〜63 で、すべて異なる（Distinct）
値が c のマスのとなりのどこかに、値 c+1 のマスがある
値が c のマスのとなりのどこかに、値 c-1 のマスがある
最後（63番目）のマスのとなりに、0番目のマスがある（閉じたルートにするため）

「となり」は、ナイトの動き（L字型の8方向）で行けるマスだけです。

この制約は、ナイトが移動できる範囲でしか満たせないので、自然にルートが決まります。

from z3 import *
from itertools import product

# ナイトの8方向の動き
KNIGHT_MOVES = [(1, 2), (2, 1), (-1, 2), (2, -1), (-2, 1), (1, -2), (-1, -2), (-2, -1)]

コード#

盤面の各マスに整数変数を作り、制約を追加します。

w, h = 8, 8
N = w * h

cells = {}
solver = Solver()

for i, j in product(range(h), range(w)):
    c = cells[i, j] = Int(f'c_{i}_{j}')
    solver.add(c >= 0, c <= N - 1)

# 訪れる順番はすべて異なる
solver.add(Distinct(list(cells.values())))

for i, j in product(range(h), range(w)):
    c = cells[i, j]
    neighbours = [cells[i + di, j + dj] for di, dj in KNIGHT_MOVES
                  if (i + di, j + dj) in cells]

    next_is = [(x == c + 1, 1) for x in neighbours]   # となりに c+1 があるか
    prev_is = [(x == c - 1, 1) for x in neighbours]   # となりに c-1 があるか
    start_is = [(x == 0, 1) for x in neighbours]      # となりに 0 があるか

    # 最後のマス（63）以外は、となるどこに c+1 がある
    solver.add(Implies(c < N - 1, PbEq(next_is, 1)))
    # 最初のマス（0）以外は、となるどこに c-1 がある
    solver.add(Implies(c > 0, PbEq(prev_is, 1)))
    # 最後のマス（63）は、となるどこに 0 がある（閉じたルート）
    solver.add(Implies(c == N - 1, PbEq(start_is, 1)))

%time solver.check()
m = solver.model()

for i in range(h):
    for j in range(w):
        print(f'{m[cells[i, j]].as_long():2d}', end=' ')
    print()

CPU times: total: 1.86 s
Wall time: 1.88 s
60 45 10 47 58 23 20 
11 62 59 24 21 48 57 
0  9 46 27 56 19 22 
43 36  3 54 25 28 49 
8  1 26 35  4 55 18 
13 40 53  2 31 50 29 
38 15 34  5 52 17 32 
41  6 39 16 33 30 51 

表のように、各マスに「何番目に訪れたか」が入りました。0 から 63 までが1回ずつ現れていることを確認してください。

見つけたルートを検算する#

Z3 が出した答えが本当にナイトツアーになっているか、自分で確かめるコードも書いておきます。

def check_tour(board):
    """各マスの値を、ナイトの移動順に並べて確認する"""
    h, w = len(board), len(board[0])
    pos = {board[i][j]: (i, j) for i in range(h) for j in range(w)}

    if sorted(pos) != list(range(h * w)):
        return "番号が 0〜63 の1回ずつになっていません"

    for k in range(h * w):
        i, j = pos[k]
        i2, j2 = pos[(k + 1) % (h * w)]
        if (i2 - i, j2 - j) not in KNIGHT_MOVES:
            return f"{k} 番目から {k + 1} 番目がナイトの動きになっていません"

    return "OK: ナイトの動きで 0 → 1 → … → 63 → 0 と一周しています"


tour = [[m[cells[i, j]].as_long() for j in range(w)] for i in range(h)]
print(check_tour(tour))

OK: ナイトの動きで 0 → 1 → … → 63 → 0 と一周しています

制約の意味#

制約	意味
`Implies(c < N - 1, PbEq(next_is, 1))`	最後以外のマスは、となるどこに `c+1` のマスがある
`Implies(c > 0, PbEq(prev_is, 1))`	最初以外のマスは、となるどこに `c-1` のマスがある
`Implies(c == N - 1, PbEq(start_is, 1))`	最後のマスは、となるどこに `0` のマスがある
`Distinct(...)`	0〜63 が重複しない

「c+1 のマスがある」と「c-1 のマスがある」は、片方だけでも同じ意味になります（c+1 のマスから見れば c は c-1 です）。両方書いておくと、Z3 が探索しやすくなります。

`PbEq()` とは#

PbEq(args, k) は、重み付きの合計がちょうど k になるという制約です。args は (条件, 重み) のリストで、条件が True なら重みが加算されます。

例：重みが 1 の条件が2つ真、重み 2 が1つ真なら合計 4 です。

x, y, z = Bools('x y z')

s = Solver()
s.add(PbEq([(x, 1), (y, 2), (z, 3)], 5))
s.check()
print(s.model())

[y = True, z = True, x = False]

x が1点、y が2点、z が3点で、合計がちょうど 5 になる組み合わせが選ばれました（y と z が真）。

ナイトツアーのコードでは、どの条件の重みも 1 にしています。つまり PbEq(..., 1) は**「条件が真になるのはちょうど1つ」**という意味になります。

Sum(...) == 1 でも同じことが書けますが、PbEq() のほうが「ちょうど1つ」という意図がはっきりして、Z3 も速く解けます。

まとめ#

移動の順番を各マスの整数にすると、「隣どうしがナイトの移動先」という制約でルートが決まる
Distinct で 0〜63 を1回ずつ使うことを保証する
「ちょうど1つ」は PbEq([...], 1) で書ける
出てきた答えは、自分で検算するコードを用意すると安心（check_tour()）