骑士巡游：找出把每一格都访问一次的路线

骑士巡游：找出把每一格都访问一次的路线#

本章的内容#

本章要找出这样一条路线：国际象棋的骑士在 8×8 的棋盘上把每一格都访问一次，最后回到出发点，形成一条闭合的路线。

  • 给每一格分配一个表示第几个访问的整数

  • 用 PbEq() 写出相邻的编号必须在骑士的落点上

  • 把规则原样写成约束之后，Z3 数秒之内就能找出路线

骑士巡游问题在 用 OrTools 解骑士巡游问题 中也出现过。

思路#

给每一格分配 0 到 63 的整数，使这个数表示该格是第几个被访问的。

  • 所有格的值都在 0 到 63 之间，并且互不相同，用 Distinct 约束

  • 值为 c 的格的某个相邻格中，存在值为 c+1 的格

  • 值为 c 的格的某个相邻格中，存在值为 c-1 的格

  • 值为 63 的格的相邻格中，存在值为 0 的格，这样才成为闭合的路线

这里的相邻只指骑士的走法，即 L 字形的八个方向上能够到达的格。给每一格一个编号，同时表达了两件事：这一格在第几步被访问，以及 0〜63 的每个数各出现一次。

只要编号满足这些约束，这个编号方案本身就是一条巡游路线，不必再追加条件。首尾相接的约束把路线从“走完就停”的路径变成回路，骑士因此可以从最后一格回到出发点。

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

从表中可以看到，每一格都填上了访问的次序，0 是出发的格。可以核对 0 到 63 的每个数是否恰好出现一次。

验算找到的路线#

Z3 给出的答案是否真的是骑士巡游，值得另写一段代码确认：约束写错时，求解器照样会返回 sat，只有独立的验算才能发现。下面就是这段验算的代码，运行之后就能看出结果是否成立。

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 各一次"

    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 互不重复

表中三行 Implies 分别对应三种情形：中间格的后继、中间格的前驱、末格回到起点。

存在值为 c+1 的格与存在值为 c-1 的格这两条，只写一条也是等价的，因为从 c+1 那一格来看，c 就是它的 c-1。两条都写上，Z3 的搜索会更容易一些。多出来的这一条不改变解集，只是把不可能的分支提前剪掉。

什么是 PbEq()#

PbEq(args, k) 是加权和恰好等于 k 的约束。args 是 (条件, 权重) 的列表，条件为 True 时对应的权重就计入和里。

例如权重为 1 的两个条件为真、权重为 2 的一个条件为真，和就是 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) 就表示恰好有一个条件为真。

用 Sum(...) == 1 也能写出同样的效果，但 PbEq() 更能表明恰好一个的意图，Z3 解起来也更快。

小结#

  • 把访问顺序做成每一格的整数之后，用相邻格在骑士的落点上这条约束就能确定路线

  • 用 Distinct 保证 0〜63 各用一次

  • 恰好一个可以写成 PbEq([...], 1)

  • 得到的答案最好用自己写的验算代码确认一遍，即 check_tour()