解四角分割：用布尔变量把格与数字连起来

本章的内容

四角分割是把盘面切成若干个长方形的谜题，本章把切法用布尔变量表示，交给 SAT 求解，由求解器把区域切出来。

• 对每个数字，列出所有包含它的长方形候选，让求解器恰好选一个

• 对每一格，让求解器恰好选一个所属的数字

• 用蕴含关系把两者连起来，即选了某个长方形，其中的格就属于该数字

使用辅助库 helper.sat.SATHelper 可以把 CNF 写得很短。三类约束里最关键的是蕴含关系。

规则

1. 切成长方形或正方形

   • 把给定的格子切成若干个长方形或正方形

2. 每个区域一个数字

   • 每个区域中恰好包含一个题目给出的数字

3. 数字表示面积

   • 这个数字表示它所在区域的格数

4. 使用全部格子

   • 区域互不重叠，并且每一格都属于某一个区域

谜题的初始状态	解答

四角分割谜题的网站

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

用 helper.puzzle.extract_shikaku() 可以取得这个网站上的谜题盘面。打开浏览器的开发者工具，把表示盘面的 <div> 标签的代码复制下来，交给这个函数执行，盘面就会以数组的形式取得。

思路

变量有两类。

变量	含义
矩形变量	把这一矩形选作数字 p 的长方形
格变量	格 q 属于数字 p 的长方形

约束有三条。

1. 对每个数字，候选矩形中恰好一个为真，该数字的长方形由此确定

2. 对每一格，所属的数字中恰好一个为真，所有格都归入某个区域

3. 选定某个矩形之后，其中的格全部属于该数字，即蕴含关系

仅凭这三条，区域重叠与一个区域里有两个数字这两种情况就被自动排除，不必再为重叠另外写约束。两层“恰好一个”分别从数字与格出发：前者决定每个数字占据哪一块区域，后者决定每一格属于哪个数字。

代码

helper.sat.SATHelper 是一个便于拼装 CNF 的小类。

• next()：造出下一个编号的变量

• next(n)：造出 n 个变量，返回编号的列表

• exact_n(vs, n)：追加 vs 中恰好 n 个为真的约束

• implies_all(a, vs)：对 vs 中的每个变量 x 追加 a → x

• solve()：求解并返回模型

这些方法都只往 CNF 里追加子句，求解之前的拼装因此可以写得很短。

先准备一个造出长方形候选的函数，把包含数字格 (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. 对每个数字，候选长方形各对应一个变量，即 rect_variables

2. 对每一格，可能包含它的数字各对应一个变量，即 cell_variables

rect_variables[x, y] 是 {变量编号: 长方形} 的字典，cell_variables[x, y] 是 {数字的位置: 变量编号} 的字典。两套变量分别从数字与格出发，编号由 next() 分配，因此不会重复。

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. 对每个格子，每个数字造一个变量
        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：每个数字的矩形只有一个
        for rects in rect_variables.values():
            sat.exact_n(rects.keys(), 1)

        # 约束2：每个格子恰好属于一个数字
        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);

查看变量的内容

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 三种，并且位置不能超出盘面。候选的个数随盘面变大而增加，但生成长方形的逻辑与盘面大小无关。

从这些候选中只选一个，就是 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)

模型里只选中了一个，候选再多也一样，这就是 exact_n 的作用。

接着看格的一侧，cell_variables[2, 1] 保存着格 (2, 1) 可能属于哪个数字的长方形。

solver.cell_variables[2, 1]

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

这一格可能属于三个数字的长方形，其中只有一个为真，由 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。

连接两类变量

最后一条约束是选了长方形之后，其中的格就属于该数字。

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 条约束，即每格只属于一个数字，共同保证了长方形之间不会重叠。两个长方形若共用一格，这一格就会同时属于两个数字，而格这一侧只允许一个为真，于是矛盾。

更难的谜题

出题网站上最难的那一类谜题也能解出来。题目的规模只影响候选的个数，代码不用改。

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

验算

检查解出的长方形是否满足谜题的规则。

def check_shikaku(board, rects):
    """每个矩形是否只含一个数字、面积与数字一致、所有格子各用一次"""
    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) 就是恰好一个为真，做法分两步：禁止 n+1 = 2 个同时为真，再禁止 len - n + 1 = len 个，即全部，同时为假。两步合起来才是恰好一个：只做第一步会允许全假，只做第二步会允许多真。

小结

• 对每个数字造出长方形候选，用 exact_n(vs, 1) 让求解器选一个

• 对每一格造出所属数字的候选，用 exact_n(vs, 1) 让求解器选一个

• 用蕴含关系把长方形的格与数字连起来，重叠就自动被排除

• 使用 helper.sat.SATHelper 可以把 CNF 的拼装写得很短

• 解出的结果要用验算代码确认