ノノグラムを解く ― 位置変数でCNFを小さくする#
この章で学ぶこと#
ノノグラム（イラストロジック）を SAT で解きます。この章の主役は、CNF をいかに小さく作るかです。
1行分のヒントから、塗り方の候補をすべて列挙する
候補をそのまま CNF にすると、組み合わせ爆発で遅くなる
各数字の「開始位置」を変数にすると、CNF が桁違いに小さくなる
最後に、45×60 の大きなパズルも解きます。
ノノグラムのルール#
ノノグラムは、数字を手がかりにマスを塗るパズルです。
盤面は正方形のグリッドで、各マスは黒か白に塗る
行の左にある数字は、その行の連続する黒マスの長さを順番に並べたもの
列の上（下）にある数字も同じ
すべての黒マスを決めれば完成
各マスを「黒なら True」のブール変数で表し、行・列のヒントを制約にします。
from matplotlib import pyplot as plt
import numpy as np
import itertools
1行分の解をすべて列挙する#
paint_numbers(numbers, count) は、長さ count の1行に numbers の数字を並べるすべての塗り方を作ります。塗るマスを 1、塗らないマスを -1 で表します。
再帰で書けます。終了条件は2つです。
数字を並べるのに必要なマス数が
countより多い … 解なし（例：[2, 1, 5]には最低 2+1+5+2 = 10 マス必要）残りの数字が1つ … その長さのブロックを、置けるすべての位置に置く
終了しない場合は、2つに分岐します。
最初の数字をここに置いて、残りを再帰で解く（
numbers[0]マス塗って、1マス空ける）このマスを空けて、残りを再帰で解く
def paint_numbers(numbers, count):
"""numbers の数字を幅 count に並べる、すべての塗り方を返す（1=黒, -1=白）"""
if sum(numbers) + len(numbers) - 1 > count:
return # 1. マスが足りない
if len(numbers) == 1:
n = numbers[0]
for i in range(count - n + 1): # 2. 最後の1つは、置ける位置すべて
yield [-1] * i + [1] * n + [-1] * (count - i - n)
return
# 3. 先頭の数字を今の位置に置く（その後ろに1マス空ける）
for rest in paint_numbers(numbers[1:], count - numbers[0] - 1):
yield [1] * numbers[0] + [-1] + rest
# 4. このマスを空けて、1つ右にずらす
for rest in paint_numbers(numbers, count - 1):
yield [-1] + rest
[2, 1, 5] を12マスに並べる例です。読みやすいように、-1 は 0 にして表示します。
for line in paint_numbers([2, 1, 5], 12):
print([int(x > 0) for x in line])
[1, 1, 0, 1, 0, 1, 1, 1, 1, 1, 0, 0]
[1, 1, 0, 1, 0, 0, 1, 1, 1, 1, 1, 0]
[1, 1, 0, 1, 0, 0, 0, 1, 1, 1, 1, 1]
[1, 1, 0, 0, 1, 0, 1, 1, 1, 1, 1, 0]
[1, 1, 0, 0, 1, 0, 0, 1, 1, 1, 1, 1]
[1, 1, 0, 0, 0, 1, 0, 1, 1, 1, 1, 1]
[0, 1, 1, 0, 1, 0, 1, 1, 1, 1, 1, 0]
[0, 1, 1, 0, 1, 0, 0, 1, 1, 1, 1, 1]
[0, 1, 1, 0, 0, 1, 0, 1, 1, 1, 1, 1]
[0, 0, 1, 1, 0, 1, 0, 1, 1, 1, 1, 1]
9通りの塗り方があります。人間が1行ずつ見ると「ここは必ず黒」が分かりますが、SAT ソルバーには、このすべての候補を教える必要があります。
DNF から CNF へ#
paint_numbers() の返す塗り方は、それぞれが「このマスは黒で、このマスは白」という AND の条件です。それが OR で並ぶので、これは DNF（選言標準形）です。SAT ソルバーは CNF（連言標準形）しか解けないので、変換が必要です。
DNF → CNF の素朴な変換（分配法則）は、式が爆発します。そこで新しい変数を導入します。たとえば「A, B, C のうちちょうど1つが偽」という DNF
の各項に新しい変数 X, Y, Z を割り当て、等価（\(\Leftrightarrow\)）で結びます。
\(P \Leftrightarrow Q\) は CNF で
と書けます。これを \(X \Leftrightarrow (\neg A \wedge B \wedge C)\) に当てはめると、次の4つの節になります。
SymPy で確かめてみます。
from sympy import symbols, Equivalent
from sympy.logic.boolalg import to_cnf
X, A, B, C = symbols("X A B C")
to_cnf(Equivalent(X, ~A & B & C))
同じ形になっています（節の順番は違います）。この変換は「Tseitin 変換」と呼ばれ、式の長さを抑えられるのが利点です。
dnf_to_cnf(dnf) は、DNF の各項に新しい変数を割り当てて、上の4つの節を作ります。
各項について、新しい変数
zを作るz → 各リテラル…[-z, v]を作る（v は項に含まれる変数）項 → z…[z] + [-v for v in term]を作る最後に
zをすべて OR でつないだ節を1つ作る
新しい変数は、既存の変数の最大番号より大きくする必要があります。new_vars を渡すと、その番号の続きを使ってくれます。
def dnf_to_cnf(dnf, new_vars=None):
"""DNF を Tseitin 変換で CNF にする"""
if new_vars is None:
# 既存の変数の最大番号より後ろを使う
start = max(max(map(abs, term)) for term in dnf) + 1
new_vars = iter(range(start, start + len(dnf)))
zlist = [] # 新しい変数のリスト
cnf = []
for term in dnf:
z = next(new_vars)
zlist.append(z)
cnf.append([z] + [-v for v in term]) # 項なら z（項 → z）
for v in term:
cnf.append([-z, v]) # z なら各リテラル（z → リテラル）
cnf.append(zlist) # z のどれかは真
return cnf
3つの変数のうち1つだけが偽、という DNF で試します。得られた解が「ちょうど1つが偽」になっていることを確認してください。enum_models() は、条件を満たす解をすべて返します。
from pprint import pprint
from pysat.solvers import Solver
dnf = [[-1, 2, 3], [1, -2, 3], [1, 2, -3]]
cnf = dnf_to_cnf(dnf)
print("CNF")
pprint(cnf)
print("solutions")
sat = Solver()
sat.append_formula(cnf)
for sol in sat.enum_models():
print([int(x > 0) for x in sol])
CNF
[[4, 1, -2, -3],
[-4, -1],
[-4, 2],
[-4, 3],
[5, -1, 2, -3],
[-5, 1],
[-5, -2],
[-5, 3],
[6, -1, -2, 3],
[-6, 1],
[-6, 2],
[-6, -3],
[4, 5, 6]]
solutions
[0, 1, 1, 1, 0, 0]
[1, 0, 1, 0, 1, 0]
[1, 1, 0, 0, 0, 1]
新しい変数 4, 5, 6 が増え、最初の3つ（元の変数）はどれも「1つだけ偽」になっています。
paint_numbers() の結果と一致するかも試します。DNF の解と、CNF にして解いた結果が同じ集合になるはずです。
n = 12
solutions = list(paint_numbers([2, 1, 5], n))
variables = list(range(1, n + 1))
# 塗り方を DNF にする（変数番号 × 1 or -1）
dnf = [[v * t for v, t in zip(variables, term)] for term in solutions]
sat = Solver()
sat.append_formula(dnf_to_cnf(dnf))
# 変数 n 個分だけ取り出して、符号を -1/1 にそろえる
solutions_cnf = [[x // abs(x) for x in res[:n]] for res in sat.enum_models()]
print(sorted(solutions) == sorted(solutions_cnf))
True
ノノグラムを解く（素直な方法）#
行と列のヒントから、そのまま CNF を作ります。
各マスにブール変数（1〜幅×高さ）を割り当てる
変換で使う新しい変数の番号を用意する
行・列それぞれについて
paint_numbers()で DNF を作り、CNF に変換して追加するSolverで解き、(高さ, 幅)の形に戻すplot()で描く
class NonogramSimpleSolver:
"""ヒントをそのまま CNF にする、素直なソルバー"""
def __init__(self, rows, cols, width=None, height=None):
if width is None:
width = len(cols)
if height is None:
height = len(rows)
self.rows = rows
self.cols = cols
self.width = width
self.height = height
self.var_count = width * height
# 各マスの変数（行ごとに並べた2次元配列）
self.vars = np.arange(1, self.var_count + 1).reshape(-1, width)
# 変換で使う新しい変数の番号（マスの変数の次の番号から）
self.new_vars = itertools.count(self.var_count + 1)
self.cnf = []
for i, row in enumerate(rows):
self.add_constraints(row, width, self.vars[i, :].tolist())
for j, col in enumerate(cols):
self.add_constraints(col, height, self.vars[:, j].tolist())
def add_constraints(self, numbers, count, variables):
"""1行（または1列）分のヒントを CNF に変換して追加する"""
dnf = []
for pattern in paint_numbers(numbers, count):
dnf.append([v * p for v, p in zip(variables, pattern)])
self.cnf.extend(dnf_to_cnf(dnf, new_vars=self.new_vars))
def solve(self):
sat = Solver()
sat.append_formula(self.cnf)
if not sat.solve():
raise ValueError("解が見つかりませんでした")
model = sat.get_model()
solution = np.sign(np.array(model[:self.var_count])).reshape(self.height, self.width)
self.solution = (solution + 1) // 2 # -1/1 を 0/1 に直す
return self.solution
def plot(self, font_size=9):
from helper.plot import plot_nonogram_board
return plot_nonogram_board({"rows": self.rows, "cols": self.cols},
self.solution, font_size=font_size)
小さなパズルを解いてみます。
rows = [
[3],
[2, 1],
[2],
[7],
[9],
[2, 3, 2],
[4, 4],
[9],
[2, 3, 2],
[3, 3],
[7],
[5]
]
cols = [
[6],
[8],
[2, 2, 3],
[8, 2],
[6, 2, 2],
[1, 6, 2],
[2, 2, 2, 3],
[8],
[6]
]
pbn = NonogramSimpleSolver(rows, cols)
pbn.solve()
pbn.plot();
ファイルから読み込んで解く#
solve_and_paint(fn, solver) は、JSON ファイルのパズルを solver で解いて描きます。
ノノグラムパズルのサイト
https://www.nonograms.org/nonograms
helper.puzzle.extract_nonogram() を使うと、このサイトのノノグラムパズルの盤面を取得できます。ブラウザの開発者ツールを開き、盤面を表す <table> タグをコピーし、この関数を実行すると、盤面を表す辞書が返されます。
import json
def solve_and_paint(fn, solver, font_size=9):
if isinstance(fn, dict):
data = fn
else:
with open(fn) as f:
data = json.load(f)
pbn = solver(data["rows"], data["cols"])
pbn.solve()
pbn.plot(font_size=font_size)
nonogram02.json を解いて、時間を測ります。
%time solve_and_paint("data/nonogram02.json", solver=NonogramSimpleSolver)
CPU times: total: 15.3 s
Wall time: 16.1 s
10秒以上かかりました。マスが増えると、1行あたりの塗り方の候補が急増し、CNF の節の数も爆発するためです。
位置変数で速くする#
DNF → CNF の変換は、候補の数だけ新しい変数と節を作ります。たとえば数字が [1, 2, 3, 2, 1] で幅30なら、塗り方は 26,334 通りもあります。
len(list(paint_numbers([1, 2, 3, 2, 1], 30)))
26334
この組み合わせ爆発を避けるために、各数字の開始位置を変数にします。
幅10に [1, 2, 3] を置くなら、数字1の開始位置は 0, 1, 2 の3通りだけです。候補の「塗り方」を数えるのではなく、「各数字がどこから始まるか」を数えればよい、という発想です。
create_position_variables(numbers, count, new_bool_variables) は、各数字について {開始位置: 変数番号} の辞書を作ります。
start_pos()… 数字を詰めて並べたときの、各数字の開始位置end_pos()… 右端をそろえたときの、各数字の開始位置（これが置ける最大の開始位置）
たとえば [1, 2, 3] を幅10に置く場合、数字3の開始位置は 5〜7 です。
def start_pos(numbers, count):
"""左に詰めたときの、各数字の開始位置"""
s = 0
for n in numbers:
yield s
s += n + 1
def end_pos(numbers, count):
"""右に詰めたときの、各数字の開始位置（= 置ける最大の開始位置）"""
width = sum(numbers) + len(numbers) - 1
start = count - width
for pos in start_pos(numbers, count):
yield start + pos
def create_position_variables(numbers, count, new_bool_variables):
"""{開始位置: 変数番号} のリストを作る"""
pos_variables = []
for a, b in zip(start_pos(numbers, count), end_pos(numbers, count)):
pos_variables.append({j: next(new_bool_variables) for j in range(a, b + 1)})
return pos_variables
numbers = [1, 2, 3]
count = 10
pos_variables = create_position_variables(numbers, count, itertools.count(1))
pos_variables
[{0: 1, 1: 2, 2: 3}, {2: 4, 3: 5, 4: 6}, {5: 7, 6: 8, 7: 9}]
数字1は 0〜2、数字2は 2〜4、数字3は 5〜7 から始められます。paint_numbers() の候補と見比べてみてください。
for line in paint_numbers([1, 2, 3], 10):
print([int(x > 0) for x in line])
[1, 0, 1, 1, 0, 1, 1, 1, 0, 0]
[1, 0, 1, 1, 0, 0, 1, 1, 1, 0]
[1, 0, 1, 1, 0, 0, 0, 1, 1, 1]
[1, 0, 0, 1, 1, 0, 1, 1, 1, 0]
[1, 0, 0, 1, 1, 0, 0, 1, 1, 1]
[1, 0, 0, 0, 1, 1, 0, 1, 1, 1]
[0, 1, 0, 1, 1, 0, 1, 1, 1, 0]
[0, 1, 0, 1, 1, 0, 0, 1, 1, 1]
[0, 1, 0, 0, 1, 1, 0, 1, 1, 1]
[0, 0, 1, 0, 1, 1, 0, 1, 1, 1]
位置変数の制約#
位置変数には、2種類の制約が必要です。
各数字の開始位置は、候補のうちちょうど1つ
数字
iの開始位置をp1、次の数字の開始位置をp2とすると、p2 >= p1 + num[i] + 1（1マス以上あける）
2番目は「p1 と p2 の組のうち、間隔が足りないものは同時に真にならない」という節 [-p1_var, -p2_var] で表せます。
only_one_true() は「ちょうど1つ」、pairwise() は隣り合う要素の組を作るヘルパーです。
def only_one_true(variables):
"""変数のうち、ちょうど1つが True になる CNF"""
yield list(variables) # 少なくとも1つ
for i, j in itertools.combinations(variables, 2):
yield [-i, -j] # 2つ同時はダメ
def pairwise(iterable):
"""(a0,a1), (a1,a2), ... を作る"""
a, b = itertools.tee(iterable)
next(b, None)
return zip(a, b)
def position_variables_constraint(pos_variables, numbers):
cnf = []
# 1. 各数字の開始位置は1つだけ
for pos_var in pos_variables:
cnf.extend(only_one_true(pos_var.values()))
# 2. 隣り合う数字は、重ならないように離す
for i, (pos_var1, pos_var2) in enumerate(pairwise(pos_variables)):
gap = numbers[i] + 1
for pos1, pos2 in itertools.product(pos_var1, pos_var2):
if pos2 < pos1 + gap:
cnf.append([-pos_var1[pos1], -pos_var2[pos2]])
return cnf
cnf = position_variables_constraint(pos_variables, numbers)
cnf
[[1, 2, 3],
[-1, -2],
[-1, -3],
[-2, -3],
[4, 5, 6],
[-4, -5],
[-4, -6],
[-5, -6],
[7, 8, 9],
[-7, -8],
[-7, -9],
[-8, -9],
[-2, -4],
[-3, -4],
[-3, -5],
[-5, -7],
[-6, -7],
[-6, -8]]
cnf を解いて、マスの塗り方に戻してみます。
開始位置の変数が真 → その数字を、その位置から
num[i]マス塗るcell_mapは「変数番号 → (開始位置, 数字)」の対応表
sat = Solver()
sat.append_formula(cnf)
cell_map = {}
for n, pos_var in zip(numbers, pos_variables):
for pos, var in pos_var.items():
cell_map[var] = (pos, n)
for sol in sat.enum_models():
cells = [0] * count
for var, v in enumerate(sol, 1):
if v > 0:
pos, n = cell_map[var]
for j in range(pos, pos + n):
cells[j] = 1
print(cells)
[1, 0, 1, 1, 0, 1, 1, 1, 0, 0]
[1, 0, 1, 1, 0, 0, 1, 1, 1, 0]
[1, 0, 1, 1, 0, 0, 0, 1, 1, 1]
[1, 0, 0, 0, 1, 1, 0, 1, 1, 1]
[0, 0, 1, 0, 1, 1, 0, 1, 1, 1]
[0, 1, 0, 0, 1, 1, 0, 1, 1, 1]
[0, 1, 0, 1, 1, 0, 1, 1, 1, 0]
[1, 0, 0, 1, 1, 0, 1, 1, 1, 0]
[1, 0, 0, 1, 1, 0, 0, 1, 1, 1]
[0, 1, 0, 1, 1, 0, 0, 1, 1, 1]
同じ10通りが得られました。paint_numbers() と比べて、変数も節もずっと少なくて済んでいます。
マスの変数と位置変数をつなぐ#
ここまでは「1行の中の位置」を決めました。ノノグラムでは、行と列が同じマスを共有します。そこで、マスの変数と位置変数を結びつける制約を追加します。
マス j と位置の関係は、次の4通りです。
最初のブロックより前のマスは白 …
pos[0]より前はcell = 0最後のブロックより後のマスは白 …
pos[-1] + num[-1]以降はcell = 0ブロックの中は黒 …
pos[i] <= j < pos[i] + num[i]はcell = 1ブロックの間は白 …
pos[i] + num[i] <= j < pos[i+1]はcell = 0
「位置変数が真なら、マス変数はこうなる」という含意（-pos_var, cell_var など）で書けます。
def cell_variables_constraint(pos_variables, cell_variables, numbers, count):
cnf = []
# 3. ブロックの中は黒
for i, pos_var in enumerate(pos_variables):
for pos, var in pos_var.items():
for j in range(numbers[i]):
cnf.append([-var, cell_variables[pos + j]])
# 1. 最初のブロックより前は白
for pos, var in pos_variables[0].items():
for j in range(pos):
cnf.append([-var, -cell_variables[j]])
# 2. 最後のブロックより後は白
for pos, var in pos_variables[-1].items():
for j in range(pos + numbers[-1], count):
cnf.append([-var, -cell_variables[j]])
# 4. ブロックの間は白
for i, (pos_var1, pos_var2) in enumerate(pairwise(pos_variables)):
for pos1, pos2 in itertools.product(pos_var1, pos_var2):
if pos2 > pos1 + numbers[i]:
for j in range(pos1 + numbers[i], pos2):
cnf.append([-pos_var1[pos1], -pos_var2[pos2], -cell_variables[j]])
return cnf
10マス・[1, 2, 3] で、すべての制約を組み合わせて解きます。cell_variables はマスの変数（1〜10）、位置変数はその次の番号から作ります。
numbers = [1, 2, 3]
count = 10
cell_variables = list(range(1, count + 1))
pos_variables = create_position_variables(numbers, count, itertools.count(count + 1))
cnf = position_variables_constraint(pos_variables, numbers)
cnf += cell_variables_constraint(pos_variables, cell_variables, numbers, count)
sat = Solver()
sat.append_formula(cnf)
for sol in sat.enum_models():
print([int(x > 0) for x in sol[:count]])
[1, 0, 1, 1, 0, 1, 1, 1, 0, 0]
[1, 0, 1, 1, 0, 0, 1, 1, 1, 0]
[1, 0, 1, 1, 0, 0, 0, 1, 1, 1]
[1, 0, 0, 1, 1, 0, 0, 1, 1, 1]
[0, 1, 0, 1, 1, 0, 0, 1, 1, 1]
[0, 1, 0, 1, 1, 0, 1, 1, 1, 0]
[1, 0, 0, 1, 1, 0, 1, 1, 1, 0]
[1, 0, 0, 0, 1, 1, 0, 1, 1, 1]
[0, 1, 0, 0, 1, 1, 0, 1, 1, 1]
[0, 0, 1, 0, 1, 1, 0, 1, 1, 1]
paint_numbers() と同じ塗り方が出ました。これで、行と列を別々に作っても、同じマスの変数を通して整合性が取れます。
速いソルバー#
NonogramFastSolver は NonogramSimpleSolver を継承し、add_constraints() だけを差し替えたものです。
class NonogramFastSolver(NonogramSimpleSolver):
"""位置変数を使う、速いソルバー"""
def add_constraints(self, numbers, count, cell_variables):
pos_variables = create_position_variables(numbers, count, self.new_vars)
self.cnf.extend(position_variables_constraint(pos_variables, numbers))
self.cnf.extend(cell_variables_constraint(pos_variables, cell_variables,
numbers, count))
同じパズルを解いて、時間を比べます。
%time solve_and_paint("data/nonogram02.json", solver=NonogramFastSolver)
CPU times: total: 203 ms
Wall time: 213 ms
NonogramSimpleSolver では10秒以上かかっていたパズルが、1秒もかからずに解けました。候補の塗り方を全部 CNF にする代わりに「開始位置」だけを変数にしたので、式が桁違いに小さくなったためです。
最後に、45×60 の大きなパズルを解いてみます。
%time solve_and_paint("data/nonogram03.json", solver=NonogramFastSolver, font_size=6)
CPU times: total: 3.98 s
Wall time: 4.15 s
検算#
解いた盤面が、ヒントと本当に一致しているか確かめます。「連続する黒の長さ」を数えて、行・列のヒントと比べます。
def runs(line):
"""1行の並びから、連続する1の長さを順に取り出す"""
result, n = [], 0
for x in line:
if x:
n += 1
elif n:
result.append(n)
n = 0
if n:
result.append(n)
return result
def check_nonogram(rows, cols, solution):
ok_rows = [runs(solution[i]) for i in range(len(rows))] == [list(r) for r in rows]
ok_cols = [runs(solution[:, j]) for j in range(len(cols))] == [list(c) for c in cols]
return ok_rows and ok_cols
print("小さなパズル:", check_nonogram(rows, cols, pbn.solution))
with open("data/nonogram02.json") as f:
data02 = json.load(f)
pbn02 = NonogramFastSolver(data02["rows"], data02["cols"])
pbn02.solve()
print("nonogram02 :", check_nonogram(data02["rows"], data02["cols"], pbn02.solution))
小さなパズル: True
nonogram02 : True
まとめ#
1行分のヒントは
paint_numbers()ですべての塗り方に展開できるそのまま CNF にすると、候補の数だけ節が増えて爆発する（幅30で2万通り超）
各数字の開始位置を変数にすると、候補は「置ける位置」の数だけになり、式がとても小さくなる
「ちょうど1つ」「同時に真にならない」は
only_one_true()のような小さな部品で書ける行と列は、マスの変数を共有させてつなぐ
この章の高速化で、十数秒かかっていたパズルが 0.2 秒ほどになり、45×60 のパズルも数秒で解ける