数回：用线把相同的数字连起来

本章的内容

数回 是把写着相同数字的两个格用线连起来的谜题。本章把这道谜题翻译成 Z3 的约束。

• 把格中的值与相邻格之间的线作为变量

• 数字格上只有一条线，空白格上恰好两条，用 PbEq 写出恰好 n 条

• 用线连起来的两个格，值取相同

PbEq() 即恰好 n 个的写法，与用 defaultdict 做格到线的对应，是本章的要点。前者负责“每个格连出几条线”，后者负责“同一条线不要建两次”。

规则

盘面

• 盘面是格子状的方格

• 有些格里写着数字

• 盘面大小不限，10×10 比较常见

目标

• 把写着相同数字的两个格用线连起来

• 所有数字的对都连上就算完成

线的规则

• 线只能上下左右走，不能斜走

• 线与线不能交叉，也不能分叉

线一旦交叉或分叉，就看不出哪一段属于哪个数字，因此这两条规则必须先满足。

完成条件

• 所有数字的对都用线连上

• 线不交叉，也没有分叉

• 所有线都连续，没有断开

参见

用 OrTools 解数回谜题

数回谜题的网站

https://puzzlemadness.co.uk/numberlink/medium

用 helper.puzzle.extract_number_link() 可以取得这个网站上的谜题盘面。打开浏览器的源代码，把 puzzledata 那一行里的 JSON 数据复制下来，传给这个函数，盘面就会以数组的形式返回。

盘面的表示方式

盘面的表示方式是二维数组。

• 0 是空白的格，不属于任何数字

• 1 以上的数值表示成对的数字，即把相同数字的两个格用线连起来

本章使用的盘面放在 data/ 目录下的文本文件里，读入之后就是一个二维数组，行列的顺序与数组下标一致。

import numpy as np

board = np.loadtxt('data/numberlink01.txt', dtype=np.uint8)
print(board)

[[1 0 0 0 0 0 0 0 0 0]
 [0 0 0 0 0 0 0 0 5 0]
 [0 6 0 1 0 0 0 0 0 0]
 [0 0 0 0 0 4 3 0 0 0]
 [0 0 0 0 0 0 6 0 5 0]
 [0 8 0 3 0 0 0 0 0 0]
 [0 0 0 4 7 0 0 0 0 0]
 [0 0 0 0 0 0 2 0 8 0]
 [0 7 0 0 0 0 0 0 0 0]
 [0 0 0 0 0 0 0 0 0 2]]

画出盘面

plot_number_link_board() 画出盘面与解，其中 links 是 (r1, c1, r2, c2) → Bool 的字典，为 True 表示格 (r1, c1) 与 (r2, c2) 相连。values 是各格的值，线的颜色由这个值决定。

from matplotlib import pyplot as plt
from matplotlib.cm import tab20
from z3 import is_true


def plot_number_link_board(board, links=None, values=None):
    """画出盘面。传入 links 和 values 时，也画出解出来的线"""
    h, w = board.shape
    fig, ax = plt.subplots(1, 1, figsize=(w * 0.4, h * 0.4))

    # 画线（颜色由格子的值决定）
    if links is not None and values is not None:
        for (r1, c1, r2, c2), link in links.items():
            if is_true(link):
                ax.plot([c1, c2], [r1, r2], color=tab20.colors[values[r1, c1]], lw=3)

    # 画数字格
    xs, ys, texts = [], [], []
    for (r, c), v in np.ndenumerate(board):
        xs.append(c)
        ys.append(r)
        texts.append(str(v))

    ax.scatter(xs, ys)
    for x, y, s in zip(xs, ys, texts):
        if s != "0":
            ax.text(x, y, s, ha='center', va='center', fontsize=12,
                    bbox=dict(facecolor=tab20.colors[int(s)], edgecolor='black',
                              boxstyle='round,pad=0.2'))

    ax.invert_yaxis()
    ax.axis('off')
    return fig


plot_number_link_board(board)

解法

变量有两类。

• value[r, c]：格 (r, c) 的值，类型为 Int

• link[r, c, r2, c2]：相邻格之间是否有线，类型为 Bool

线只需要按右与下两个方向建立，左与上的线在相邻格看来就是那个格向右或向下的线。这样每个相邻对只建一次，变量数减半，约束里也不会出现两个变量指向同一条线。

约束有下列五条。

1. 每格的值在 0 到最大值之间

2. 有数字的格，值保持不变

3. 数字格上连的线恰好一条，即线在这里结束

4. 空白格上连的线恰好两条，即线从这里穿过

5. 用线连起来的两个格，值相等

有了第 3 条与第 4 条，线既不会分叉，也不会中断，而值相等的关系会沿线一路传下去，因此相同数字的两个格自然就连在一起了。一条线从头到尾只能连同一个数字，不同的两个数字无法被同一条线接通。至于线不能交叉，同样不必另写：线只走上下左右，两条线若要相交，就要共用同一个格，那个格上的线数会超过上限。

这段代码解的是空白格也必须有线穿过的版本，即把整个盘面填满。

from z3 import *
from collections import defaultdict


def solve_number_link(board):
    """解出盘面，返回 (links, values)"""
    h, w = board.shape
    max_value = int(board.max())

    # 每个格子的值
    value = {(r, c): Int(f'C_{r}_{c}') for r, c in np.ndindex(h, w)}

    # 相邻格子之间的线（只生成右和下）
    link = {}
    cell_links = defaultdict(list)      # 格子 → 连到这个格子的线
    for r, c in np.ndindex(h, w):
        for r2, c2 in ((r, c + 1), (r + 1, c)):
            if r2 < h and c2 < w:
                b = Bool(f'L_{r}_{c}_{r2}_{c2}')
                link[r, c, r2, c2] = b
                cell_links[r, c].append(b)
                cell_links[r2, c2].append(b)

    solver = Solver()

    # 1. 值的范围
    for v in value.values():
        solver.add(0 <= v, v <= max_value)

    for (r, c), v in np.ndenumerate(board):
        if v > 0:
            solver.add(value[r, c] == int(v))                          # 2. 数字保持不变
            solver.add(PbEq([(b, 1) for b in cell_links[r, c]], 1))    # 3. 端点有 1 条线
        else:
            solver.add(PbEq([(b, 1) for b in cell_links[r, c]], 2))    # 4. 通道有 2 条线

    # 5. 用线连起来的格子值相等
    for (r, c, r2, c2), b in link.items():
        solver.add(Implies(b, value[r, c] == value[r2, c2]))

    if solver.check() != sat:
        raise ValueError("没有找到解")

    m = solver.model()
    solved_links = {key: m.eval(b, model_completion=True) for key, b in link.items()}
    solved_values = {key: m.eval(v, model_completion=True).as_long() for key, v in value.items()}
    return solved_links, solved_values

运行示例

下面直接求解，并把线画出来。

links, values = solve_number_link(board)
plot_number_link_board(board, links, values)

更复杂的谜题

格数增加之后，线的组合也会增加，但 Z3 用同一段代码就能解。变量与约束的写法不随盘面大小改变，需要换的只是输入数据。

%%time
board = np.loadtxt('data/numberlink02.txt', dtype=np.uint8)
links, values = solve_number_link(board)
plot_number_link_board(board, links, values)

CPU times: total: 1.28 s
Wall time: 1.3 s

小结

• 把格的值 Int 与相邻格之间的线 Bool 作为变量

• 恰好一条、恰好两条可以写成 PbEq([...], n)

• 让用线连起来的格值相等之后，相同数字的格自然就连接起来

• 线只需按右与下两个方向建立，避免重复建立同一个变量

• 这段代码是所有格都有线穿过的版本。若要像一般的数回那样允许空格，把空白格的约束改成 Or(PbEq(..., 0), PbEq(..., 2)) 即可