ノノグラムを解く ― 開始位置を整数変数にする

ノノグラムを解く ― 開始位置を整数変数にする#

この章で学ぶこと#

PySAT の章では、塗り方の候補をすべて CNF にして解きました。この章では CP-SAT で解きます。

CP-SAT は整数変数を扱えるので、「各数字の開始位置」をそのまま変数にできる
開始位置から決まる塗り方を、ブール変数の AND / OR でつなぐ
45×60 の大きなパズルも解ける

参考

from ortools.sat.python import cp_model
from helper.ortools import get_all_solutions

1行分の数字を「開始位置」で表す#

1行のヒントが [2, 1]、幅が5マスなら、数字2は 0〜2 のどこかから始まり、数字1はその後ろ（1マス以上あける）から始まります。

place_numbers() は、各数字の開始位置を整数変数にして、次の制約を追加します。

n2 > n1 + 長さ … 隣り合う数字は重ならず、1マス以上あける
最後の数字は width - 長さ より後ろから始められない（はみ出し防止）

import string


def place_numbers(model, numbers, width, prefix=""):
    """各数字の開始位置を表す整数変数を作り、重ならないように制約する"""
    locations = [model.new_int_var(0, width - 1, f"{prefix}{name}")
                 for _, name in zip(numbers, string.ascii_uppercase)]
    # 隣り合う数字は、間を1マス以上あける
    for n1, n2, length in zip(locations[:-1], locations[1:], numbers):
        model.add(n2 > n1 + length)
    # 最後の数字が右端をはみ出さない
    model.add(locations[-1] <= width - numbers[-1])
    return locations


def show_all_locations(numbers, width):
    """開始位置のすべての組み合わせを表示する"""
    model = cp_model.CpModel()
    place_numbers(model, numbers, width)
    return get_all_solutions(model)

幅5マスに [2, 1] を置く場合のすべての解です。

show_all_locations([2, 1], 5)

[{'A': 0, 'B': 3}, {'A': 0, 'B': 4}, {'A': 1, 'B': 4}]

幅10マスに [3, 2, 2] を置く場合。

show_all_locations([3, 2, 2], 10)

[{'A': 0, 'B': 4, 'C': 7},
 {'A': 0, 'B': 4, 'C': 8},
 {'A': 0, 'B': 5, 'C': 8},
 {'A': 1, 'B': 5, 'C': 8}]

開始位置からマスを塗る#

開始位置が決まれば、塗るマスも決まります。あとは「開始位置」と「マスの状態」をつなぐだけです。

        graph LR
subgraph C_fill["Targets"]
direction LR
c0[1]
c1[1]
c2[0]
c3[1]
c4[0]

c0 ~~~ c1
c1 ~~~ c2
c2 ~~~ c3
c3 ~~~ c4
end

subgraph A_fill["A Fill"]
direction LR
a0[1]
a1[1]
a2[0]
a3[0]
a4[0]
a0 ~~~ a1
a1 ~~~ a2
a2 ~~~ a3
a3 ~~~ a4
end

subgraph B_fill["B Fill"]
direction LR
b0[0]
b1[0]
b2[0]
b3[1]
b4[0]
b0 ~~~ b1
b1 ~~~ b2
b2 ~~~ b3
b3 ~~~ b4
end

A["A=0 (n=2)"]
B["B=3 (n=1)"]
A --> A_fill
B --> B_fill
A_fill --> C_fill
B_fill --> C_fill

数字ごとの塗りパターン（A Fill, B Fill）を作り、マスごとに OR を取ったものが Targets（その行の最終的な塗り方）です。

CP-SAT では「開始位置が i のとき、このマスは塗る／塗らない」という条件分岐が必要になります。比較式は制約の前提条件に直接使えないので、ブール変数 b を n == i と等しくしておき、b を使って条件分岐します。

model.add(n == i).only_enforce_if(b)     # b なら n == i
model.add(n != i).only_enforce_if(~b)    # b でないなら n != i

そのうえで、各マスの状態 targets[i] と、各数字の塗り fills[i, j] を結びます。

targets[i] が真 … マス i は塗る → どの数字かは問わないので「少なくとも1つ真」
targets[i] が偽 … マス i は塗らない → すべて偽

def fill_pattern(model, numbers, targets, prefix=""):
    """numbers を targets（マスの変数）の上に配置する制約を追加する"""
    width = len(targets)
    count = len(numbers)
    locations = place_numbers(model, numbers, width, prefix)

    # fills[i, j] : マス i が数字 j で塗られるか
    fills = {}
    for i in range(width):
        for j in range(count):
            fills[i, j] = model.new_bool_var(f'{locations[j].name}_{i}')

    for j, n in enumerate(locations):
        for i in range(width - numbers[j] + 1):
            # b は「数字 j の開始位置が i である」を表すブール変数
            b = model.new_bool_var(f'{n.name}_{i}')
            model.add(n == i).only_enforce_if(b)
            model.add(n != i).only_enforce_if(~b)

            # b のとき、マス i から numbers[j] マスだけ塗る
            tmp = [fills[x, j] if i <= x < i + numbers[j] else ~fills[x, j]
                   for x in range(width)]
            model.add_bool_and(tmp).only_enforce_if(b)

    # マスの状態と、数字ごとの塗りを結ぶ
    for i, t in enumerate(targets):
        bools = [fills[i, j] for j in range(count)]
        model.add_bool_or(bools).only_enforce_if(t)          # 塗るなら、どれかの数字
        model.add_bool_and([~v for v in bools]).only_enforce_if(~t)  # 塗らないなら、全部偽


def show_all_fills(numbers, width):
    """1行分の塗り方のすべての解を表示する"""
    model = cp_model.CpModel()
    targets = [model.new_bool_var(f"{i}") for i in range(width)]
    fill_pattern(model, numbers, targets)
    for sol in get_all_solutions(model):
        print([sol[t.name] for t in targets])

幅5マスに [2, 1] を置いたときの塗り方です。

show_all_fills([2, 1], 5)

[1, 1, 0, 0, 1]
[1, 1, 0, 1, 0]
[0, 1, 1, 0, 1]

幅10マスに [3, 2, 2]。

show_all_fills([3, 2, 2], 10)

[1, 1, 1, 0, 1, 1, 0, 0, 1, 1]
[1, 1, 1, 0, 0, 1, 1, 0, 1, 1]
[1, 1, 1, 0, 1, 1, 0, 1, 1, 0]
[0, 1, 1, 1, 0, 1, 1, 0, 1, 1]