ナンバーリンク ― 数字のペアを線でつなぐ

この章で学ぶこと

ナンバーリンク は、同じ数字のペアを線で結ぶパズルです。この章では、パズルを Z3 の制約に翻訳します。

• マスの値と「隣り合うマスの間の線」を変数にする

• 数字マスは線が1本、空白マスは2本（PbEq で「ちょうど n 本」）

• 線でつないだマスの値は同じにする

PbEq()（「ちょうど n 個」）と defaultdict を使った「マス→線」の対応付けがポイントです。

ルール

盤面

• 盤面は格子状のマス目です。

• いくつかのマスには数字が書かれています。

• 盤面のサイズは自由で、10×10 などが一般的です。

目標

• 同じ数字が書かれた2つのマスを線でつなぎます。

• すべての数字のペアをつなげればクリアです。

線のルール

• 線は上下左右にのみ進めます（斜めは禁止）。

• 線どうしが交差したり、枝分かれしたりしてはいけません。

クリア条件

• すべての数字のペアが線でつながっている

• 線が交差せず、分岐もない

• すべての線が連続している（途切れがない）

参考

OrToolsでナンバーリンクパズルを解く

ナンバーリンクパズルのサイト

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

helper.puzzle.extract_number_link() を使うと、このサイトのパズル盤面を取得できます。ブラウザのソースコードを開き、puzzledata の行にある JSON データをコピーしてこの関数を実行すると、盤面が配列として返されます。

盤面の表し方

盤面は2次元配列で表します。

• 0 は空白のマス（どの数字にも属していない）

• 1 以上の数値はペアになる数字（同じ数字の2つのマスを線で結ぶ）

この章で使う盤面は 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)

解き方

変数は2種類です。

• value[r, c] … マス (r, c) の値（Int）

• link[r, c, r2, c2] … 隣り合うマスの間に線があるか（Bool）

線は「右」と「下」の2方向だけ作れば十分です（左と上は、隣のマスから見た右・下と同じ線だからです）。

制約は次の5つです。

1. 各マスの値は 0〜最大値

2. 数字があるマスの値は変えない

3. 数字があるマスにつながる線はちょうど1本（線の端点になる）

4. 空白マスにつながる線はちょうど2本（線が通り抜ける）

5. 線でつないだ2つのマスの値は等しい

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: 828 ms
Wall time: 863 ms

まとめ

• マスの値（Int）と、隣り合うマスの間の線（Bool）を変数にする

• 「ちょうど1本」「ちょうど2本」は PbEq([...], n) で書ける

• 線でつないだマスの値が等しくなるようにすると、同じ数字どうしが自然につながる

• 線は右と下だけ作れば足りる（重複した変数を作らない）

• このコードは「全マスを線が通る」バージョン。一般のナンバーリンクのように空きマスを許すなら、空白マスの制約を Or(PbEq(..., 0), PbEq(..., 2)) に変える