四角に切れを解く ― マスと数字をブール変数で結ぶ

四角に切れを解く ― マスと数字をブール変数で結ぶ#

この章で学ぶこと#

「四角に切れ」は、盤面を長方形に切り分けるパズルです。この章では、切り方をブール変数で表し、SAT に解かせます。

  • 数字ごとに「その数字を含む長方形の候補」をすべて作り、ちょうど1つを選ばせる

  • マスごとに「どの数字の長方形に入るか」をちょうど1つ選ばせる

  • 「選んだ長方形の中のマスは、その数字に属する」を含意でつなぐ

補助ライブラリ helper.sat.SATHelper を使うと、CNF を短く書けます。

ルール#

  1. 長方形か正方形に分割する

    • 与えられたマス目を、長方形または正方形に切り分けます。

  2. 各領域に数字は1つ

    • 各領域には、問題の数字がちょうど1つ入ります。

  3. 数字は面積

    • その数字は、それが入る領域のマスの数を表します。

  4. すべてのマスを使う

    • 領域は重ならず、すべてのマスがどれかの領域に入ります。

パズルの初期状態

解答

四角に切れパズルのサイト

https://www.puzzle-shikaku.com/

helper.puzzle.extract_shikaku() を使うと、このサイトのパズル盤面を取得できます。ブラウザの開発者ツールを開き、盤面を表す <div> タグのコードをコピーし、この関数を実行すると、盤面が配列として取得できます。

考え方#

変数は2種類です。

変数

意味

矩形変数

「数字 p の長方形として、この矩形を選ぶ」

マス変数

「マス q は数字 p の長方形に入る」

制約は3つです。

  1. 各数字について、候補の矩形のうちちょうど1つが真（その数字の長方形が決まる）

  2. 各マスについて、どの数字に属するかのうちちょうど1つが真（すべてのマスが1つの領域に入る）

  3. 矩形を選んだなら、その中のマスはすべてその数字に属する（含意）

これだけで、領域の重なりも「数字が2つ入る」ことも自動的に防げます。

コード#

helper.sat.SATHelper は、CNF を組み立てるための小さなクラスです。

  • next() … 次の番号の変数を1つ作る

  • next(n) … n 個の変数を作り、番号のリストを返す

  • exact_n(vs, n) … vs のうち、ちょうど n 個が真になる制約を追加する

  • implies_all(a, vs) … vs の各変数 x について a → x を追加する

  • solve() … 解を求めてモデルを返す

まず、長方形の候補を作る関数を用意します。数字のマス (x, y) を含み、面積が area の長方形をすべて列挙します。

import numpy as np
from helper.sat import SATHelper
from collections import defaultdict
from itertools import product
from collections import namedtuple

Rectangle = namedtuple("Rectangle", "x y w h")   # x=列, y=行, w=幅, h=高さ


def mult_pair(n):
    """n = w * h になる (w, h) をすべて返す"""
    n = int(n)
    for w in range(1, n + 1):
        h = n // w
        if w * h == n:
            yield w, h


def generate_rectangle(x, y, area, width, height):
    """マス (x, y) を含み、面積が area の長方形をすべて返す"""
    for w, h in mult_pair(area):
        for i, j in product(range(w), range(h)):
            # 数字のマスが、長方形の中の (i, j) の位置に来るように置く
            x2, y2 = int(x) - i, int(y) - j
            if x2 >= 0 and y2 >= 0 and x2 + w <= width and y2 + h <= height:
                yield Rectangle(x2, y2, w, h)


def generate_cell(rect):
    """長方形に含まれるマスを順に返す"""
    x, y, w, h = rect
    for i, j in product(range(w), range(h)):
        yield x + i, y + j

ShikakuSolver は、次の順に変数を作ります。

  1. 数字ごとに、候補の長方形1つにつき1つの変数（rect_variables）

  2. マスごとに、「そのマスを含みうる数字」1つにつき1つの変数（cell_variables）

rect_variables[x, y] は {変数番号: 長方形}、cell_variables[x, y] は {数字の位置: 変数番号} の辞書です。

class ShikakuSolver:
    def __init__(self, board):
        board = np.array(board)
        height, width = board.shape
        self.height = height
        self.width = width

        sat = SATHelper()

        # 1. 数字ごとに、候補の長方形を作る
        rect_variables = {}
        for y, x in zip(*np.where(board > 0)):
            x, y = int(x), int(y)
            area = int(board[y, x])
            number_rects = {}
            for rect in generate_rectangle(x, y, area, width, height):
                number_rects[sat.next()] = rect
            rect_variables[x, y] = number_rects

        # 2. マスごとに、そのマスを含みうる数字を集める
        cells = defaultdict(set)
        for (x0, y0), number_rects in rect_variables.items():
            for rect in number_rects.values():
                for xc, yc in generate_cell(rect):
                    cells[xc, yc].add((x0, y0))

        # 3. マスごとに、数字1つにつき1つの変数を作る
        cell_variables = {}
        for cell, numbers in cells.items():
            cell_variables[cell] = dict(zip(numbers, sat.next(len(numbers))))

        self.rect_variables = rect_variables
        self.cell_variables = cell_variables
        self.sat = sat
        self.board = board

    def solve(self):
        sat = self.sat
        rect_variables = self.rect_variables
        cell_variables = self.cell_variables

        # 制約1：各数字の長方形は1つだけ
        for rects in rect_variables.values():
            sat.exact_n(rects.keys(), 1)

        # 制約2：各マスは、ちょうど1つの数字に属する
        for numbers in cell_variables.values():
            sat.exact_n(numbers.values(), 1)

        # 制約3：長方形を選んだら、その中のマスはその数字に属する
        for pos, rects in rect_variables.items():
            for var_rect, rect in rects.items():
                var_cells = [cell_variables[xc, yc][pos] for xc, yc in generate_cell(rect)]
                sat.implies_all(var_rect, var_cells)

        # 解を求めて、選ばれた長方形を取り出す
        model = sat.solve()
        if model is None:
            self.sol_rects = []
            return []

        self.solution = model
        self.sol_rects = [rect
                          for rects in rect_variables.values()
                          for var_rect, rect in rects.items()
                          if model[var_rect - 1] > 0]
        return self.sol_rects

パズルを解いて、結果を描きます。

puzzle = np.loadtxt("data/shikaku01.txt", dtype=np.int16)
solver = ShikakuSolver(puzzle)
rects = solver.solve()
print(len(rects), "個の長方形に分かれました")

45 個の長方形に分かれました

from helper.plot import plot_shikaku_board

plot_shikaku_board(solver.board, rects);
_images/183261351da9899738a95080846dd7142c275427d20847a137d29636bc41bdf3.png

変数の中身を見る#

rect_variables は「数字ごとの候補」を持っています。座標 (3, 1) の数字4の候補を見てみます（solver.rect_variables[3, 1]）。

solver.rect_variables[3, 1]

{26: Rectangle(x=3, y=1, w=1, h=4),
 27: Rectangle(x=3, y=0, w=1, h=4),
 28: Rectangle(x=3, y=1, w=2, h=2),
 29: Rectangle(x=3, y=0, w=2, h=2),
 30: Rectangle(x=2, y=1, w=2, h=2),
 31: Rectangle(x=2, y=0, w=2, h=2),
 32: Rectangle(x=3, y=1, w=4, h=1),
 33: Rectangle(x=2, y=1, w=4, h=1),
 34: Rectangle(x=1, y=1, w=4, h=1),
 35: Rectangle(x=0, y=1, w=4, h=1)}

数字4を含む長方形は、面積が4になるもの（1×4, 2×2, 4×1）で、盤面からはみ出さない位置に限られます。

この中から1つだけ選ぶのが exact_n(rects.keys(), 1) です。実際にどれが選ばれたか、モデルを見てみます。

# rect_variables[3, 1] の変数番号を、モデルから引く
for var, rect in solver.rect_variables[3, 1].items():
    if solver.solution[var - 1] > 0:
        print(var, rect)

34 Rectangle(x=1, y=1, w=4, h=1)

1つだけ選ばれていることが分かります。

次に、マスの側です。cell_variables[2, 1] は「マス (2, 1) が、どの数字の長方形に入るか」の候補を持っています。

solver.cell_variables[2, 1]

{(0, 1): 1048, (3, 1): 1049, (12, 2): 1050}

このマスは、3つの数字の長方形に入る可能性があります。このうち1つだけが真になるのが exact_n(numbers.values(), 1) です。

for pos, var in solver.cell_variables[2, 1].items():
    print(pos, var, solver.solution[var - 1] > 0)

(0, 1) 1048 False
(3, 1) 1049 True
(12, 2) 1050 False

選ばれた数字の位置が、True になっています。

2種類の変数をつなぐ#

最後の制約は「長方形を選んだら、その中のマスはその数字のもの」です。

for pos, rects in rect_variables.items():
    for var_rect, rect in rects.items():
        var_cells = [cell_variables[xc, yc][pos] for xc, yc in generate_cell(rect)]
        sat.implies_all(var_rect, var_cells)

implies_all(A, Bs) は、Bs の各変数 X について A → X（-A | X）を追加します。長方形を選んだ瞬間、その中のすべてのマスが「その数字のもの」に固定されるわけです。

これと制約2（各マスは1つの数字だけ）が組み合わさって、長方形どうしが重ならないことが保証されます。

もっと難しいパズル#

パズルサイトの最難関クラスも解けます。

puzzle = np.loadtxt("data/shikaku02.txt", dtype=np.int16)
solver = ShikakuSolver(puzzle)
rects = solver.solve()
plot_shikaku_board(solver.board, rects);
_images/17cdd3a8cbd0bad354c328d01d97fd277e64b8f8c77f5afb770f2e9261cc581e.png

検算#

解いた長方形が、ルールを満たしているか確かめます。

def check_shikaku(board, rects):
    """各長方形に数字が1つだけ入り、面積が数字と一致し、全マスが1回ずつ使われているか"""
    height, width = board.shape
    covered = np.zeros_like(board, dtype=int)

    for x, y, w, h in rects:
        numbers = [board[y + j, x + i]
                   for j in range(h) for i in range(w)
                   if board[y + j, x + i] > 0]
        if len(numbers) != 1 or numbers[0] != w * h:
            return False
        covered[y:y+h, x:x+w] += 1

    return bool((covered == 1).all())


print(check_shikaku(solver.board, rects))

True

SATHelper の実装#

exact_n() と implies_all() の中身です。どちらも短いので、読んでおくと CNF の作り方に慣れます。

def exact_n(self, variables, n, extend=True):
    cnfs = []
    variables = [int(v) for v in variables]
    # n+1 個が同時に真になるのを禁止する
    for c in combinations(variables, n + 1):
        cnfs.append([-v for v in c])
    # 「少なくとも n 個」… 偽になるのが len - n + 1 個を超えないようにする
    for c in combinations(variables, len(variables) - n + 1):
        cnfs.append([v for v in c])
    if extend:
        self.extend(cnfs)
    return cnfs


def implies(self, A, B, extend=True):
    if isinstance(B, int):
        B = [B]
    cnf = [-A] + B          # A → B は (~A | B)
    if extend:
        self.extend([cnf])
    return cnf


def implies_all(self, A, Bs, extend=True):
    return [self.implies(A, B, extend=extend) for B in Bs]

exact_n(vs, 1) は「1つだけ真」になります。n+1 = 2 個の組を禁止し、len - n + 1 = len 個（全部）が偽になるのも禁止する、という2段構えです。

まとめ#

  • 数字ごとに長方形の候補を作り、exact_n(vs, 1) で1つ選ばせる

  • マスごとに所属先の候補を作り、exact_n(vs, 1) で1つ選ばせる

  • 「長方形を選んだら、中のマスはその数字」を含意でつなぐと、重なりも自動的に防げる

  • helper.sat.SATHelper を使うと、CNF の組み立てが短く書ける

  • 出てきた解は、検算のコードで確かめる