ナイトツアー問題

ナイトツアー問題#

ナイトツアー問題は、チェスのナイト（騎士）がボード上で1回ずつすべてのマスを訪れ、再び最初の位置に戻るという問題です。ナイトはL字型の移動を行うため、移動可能な場所に制約があります。ナイトツアー問題は、これらの制約を満たすルートを見つける問題です。

See also

OrToolsでナイトツアー問題を解く

from z3 import *
from itertools import product

困難点と解き方#

この問題の困難な点は、ナイトが次にどのマスに移動するかという選択肢が周囲の8つのマスに限られていること、さらに64回の移動を経てすべてのマスを訪れる必要があるため、膨大な探索空間を持つことです。Z3を使ってこの問題を解決するために、各マスに0から63の整数を割り当て、その整数がナイトの移動順番を表すようにします。このようにすると、制約条件は以下のように表現できます：

  • 各マスの値とその周辺のマスの値の差は必ず1であるという制約を設けます。

この方法で、ナイトが順番に移動し、すべてのマスを訪れるルートを探索することができます。

コード#

次のコードでは、ナイトツアー問題を解きます。

w, h = 8, 8
cells = {}
s = Solver()

directs = [(1, 2), (2, 1), (-1, 2), (2, -1), (-2, 1), (1, -2), (-1, -2), (-2, -1)]
for i, j in product(range(h), range(w)):
    c = cells[i, j] = Int("c_{}_{}".format(i, j))
    s.add(c >= 0, c <= w * h - 1)
    
s.add(Distinct(list(cells.values())))
    
for i, j in product(range(h), range(w)):
    c = cells[i, j]
    neighbours = []
    for di, dj in directs:
        i2, j2 = i + di, j + dj
        if (i2, j2) in cells:
            neighbours.append(cells[i2, j2])

    equal_minus_1 = [(x == c - 1, 1) for x in neighbours]
    equal_plus_1 = [(x == c + 1, 1) for x in neighbours]
    equal_zero = [(x == 0, 1) for x in neighbours]

    s.append(Implies(c < w * h - 1, PbEq(equal_plus_1, 1)))
    s.append(Implies(c > 0,     PbEq(equal_minus_1, 1)))
    s.append(Implies(c == w * h - 1, PbEq(equal_zero, 1)))

%time s.check()

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

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

ナイトのルートは以下の制約条件を用いて表現されます：

  1. 値が63未満の変数 c に対して、その周囲の8個の変数の中には必ず1つの変数が c + 1 である必要があります。

  2. 値が0より大きい変数 c に対して、その周囲の8個の変数の中には必ず1つの変数が c - 1 である必要があります。

  3. 値が63の変数 c に対して、その周囲の8個の変数の中には必ず1つの変数が 0 である必要があります。

また、PbEq() は「ちょうど1つの変数が特定の値を持つ」制約を表すために使用されます。

PbEq()#

PbEq(args, k) は、指定した条件に基づいて、リスト内の Bool 式の重み付き合計がちょうど k になるように制約を設定します。args はリストで、各項目は (Bool演算式, 重み) のペアです。Bool演算式が True である場合、その項目の重みが合計に加算されます。そして、この合計が k になるように制約を定義します。

例えば、次のコードは次のように説明できます：

x, y, z = Bools('x y z')
solve(PbEq([(x, 1), (y, 2), (z, 3)], 5))

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

ここで、x, y, z は Boolean 変数です。PbEq() の引数 [(x, 1), (y, 2), (z, 3)] は、x が True の場合に1、y が True の場合に2、z が True の場合に3の重みを持つことを意味します。そして、この重みの合計がちょうど 5 になるように制約を設定しています。

ナイト問題を解くコードでは、すべての重みが1に設定されているため、PbEq() は Bool演算式が True の数がちょうど1になるような制約条件を表現します。

Contents