从约束模型到可玩的益智游戏

# 从约束模型到可玩的谜题游戏 来源：https://zayenz.se/blog/post/constraint-generated-puzzle-games/ 在我的论文*Scaling Sudoku as a Constraint Problem*（https://zayenz.se/research/paper/scaling-sudoku）中，我生成了一个包含 434,201 个数独实例的仓库（https://github.com/zayenz/scaled-sudoku-instances），尺寸从 6×6 到 36×36 共五种。我用它们做约束编程实验，以探究：哪种传播方案能在不分支的情况下解出谜题；该方案如何随尺寸变化；以及有多少线索能使一个实例从一个难度类别移动到另一个难度类别。我还想实际玩一玩其中一些谜题。这个小愿望衍生出了更多东西。我现在有了可玩的数独（https://zayenz.se/games/sudoku/）、Nonogram（https://zayenz.se/games/nonogram/）、Queens（https://zayenz.se/games/queens/）、Zip（https://zayenz.se/games/zip/）、Loopy（https://zayenz.se/games/loopy/）、Tents（https://zayenz.se/games/tents/）、Patches（https://zayenz.se/games/patches/）、Wend（https://zayenz.se/games/wend/）以及它的瑞典语姐妹版 Swend（https://zayenz.se/games/swend/）。它们都汇集在一个游戏页面（https://zayenz.se/games/）上。 下面的每个游戏小节都包含一个用 MiniZinc（https://www.minizinc.org/）编写的简短模型（MiniZinc 是一种约束建模语言），并解释其对应生成器的一个部分。这些模型是说明性草图，而非生成谜题包的正式程序。大多数生成和求解代码使用 Gecode 6.4.0（https://zayenz.se/blog/post/gecode-6-3-and-6-4-released/）。其他程序负责导入、栅格化、精确覆盖和谜题包组装。 这九个游戏的共同点是：我从一个解或源图像出发，然后添加、移动或移除信息，直到预期答案唯一，或者丢弃无法干净修复的候选。其中一些相同的推导后来也用于难度分类和提示生成。生成和唯一性检查都在离线完成。浏览器只接收静态谜题和已存储的解，不运行求解器。难度标签来自传播、搜索或确定性推理的测量结果。它们提供了每个谜题包内的相对、机械推导的排序；并不估计玩家会觉得这些谜题有多难。 这些清单已用 MiniZinc 2.10.0（https://docs.minizinc.dev/en/latest/changelog.html）检查过。为了保持重点明确，它们省略了输入验证、搜索注释以及外层循环（即当存在第二个解时拒绝候选的逻辑）。除了解谜步骤如何构成谜题解之外，输出也被省略。 ## 数独：从语料库到游戏  > 一个进行中的 6×6 数独棋盘，左上角选中格内有铅笔标记 Scaling Sudoku 语料库始于 32,000 个唯一可解的基础谜题，尺寸为 6×6、9×9、16×16、25×25 和 36×36。生成器首先创建完整网格，然后在保持唯一性的前提下移除线索。Gecode 对生成的谜题进行分类。这种分类扩展了 Helmut Simonis 在 2005 年论文*Sudoku as a Constraint Problem*（https://archive.modref.org/files/papers/2005/ModRef2005-02-Sudoku-as-a-Constraint-Problem.pdf）中的设置。它尝试一组有序的传播配置。`Val`、`Bnd` 和 `Dom` 分别指值传播、边界传播和值域传播（https://zayenz.se/blog/post/benchmarking-linkedin-queens/#propagation-strength）；`BS` 和 `DS` 则添加边界剃除或值域剃除[^1]。最弱的成功配置成为谜题的难度标签。如果没有任何配置能在不分支的情况下完成求解，则标签为 `Search`。 基础数独模型非常简短。盒子尺寸作为数据输入，这使得同一个模型既能处理带 2×3 盒子的 6×6 棋盘，也能处理常见的 3×3 盒子的 9×9 棋盘。 ```minizinc include "globals.mzn"; int: n; int: box_height; int: box_width; set of int: N = 1..n; set of int: Values = 1..n; set of int: BoxTopRows = { row | row in N where (row - 1) mod box_height = 0}; set of int: BoxLeftColumns = { column | column in N where (column - 1) mod box_width = 0}; array[N, N] of 0..n: clue; array[N, N] of var Values: board; constraint forall (row in N) ( all_different(board[row,..])); constraint forall (column in N) ( all_different(board[..,column])); constraint forall (top in BoxTopRows, left in BoxLeftColumns) ( all_different(board[ top..top+box_height-1, left..left+box_width-1 ])); constraint forall (row, column in N where clue[row,column] > 0) ( board[row,column] = clue[row,column]); solve satisfy; ``` 可玩谜题包是一个可复现的固定种子样本，包含来自固定语料库修订版的 500 个基础谜题，限于 6×6 和 9×9 棋盘。一个离线导入器将选定的谜题及其已知解转换为静态谜题包。 ### 让数独看起来更像数独 生成的谜题不会自动具备人们期望出版数独所具有的视觉对称性。我不想仅仅为了展示而生成另一套谜题，因此我为选定的谜题编写了一个离线对称化处理。这里有两个有用的自由度。首先，行和列可以通过保持盒子结构的方式进行置换：一个带内的行、一个栈内的列，以及带和栈本身。其次，缺失的旋转对称伙伴可以用已知解中的值来填充。后者只会增加信息，因此不会引入第二个解，但根据传播分类器，它可能使谜题变得更简单。  > 一次小型的对称化运行。置换在添加任何线索之前将十一个缺失的对称伙伴减少到三个。新线索保持绿色；每个已有伙伴在与其匹配的线索被添加时闪烁。 对于每个谜题，优化器枚举从保持盒子的布局中可获得的所有不同旋转配对，并按实现 180° 旋转对称所需的线索数量对其进行排序。它评估三个排名最高的布局，首先尝试为每个布局补全对称性。如果这改变了难度标签，它就逐个添加伙伴线索，并且只保留 Gecode 能复现原始标签的那些添加。最后，它选择产生不对称单元格最少的布局。这一处理使 500 个谜题中的 228 个完全旋转对称，并将不对称单元格总数从 6,172 个减少到 1,928 个。 ## Nonogram：回归 regular  > 一个 10×10 心形的开始 在 Nonogram 中，玩家填充单元格，使每行和每列中的连续块与给定的线索匹配。这个游戏也回到了我早期使用 Gecode 的工作。2005 年，我编写了最初的 Gecode nonogram 示例（https://github.com/Gecode/gecode/blob/release-2.0.0/examples/nonogram.cc），使用了 Gilles Pesant 的 `regular` 约束（https://doi.org/10.1007/978-3-540-30201-8_36）。该模型通过正则表达式 `` 0* 1^a 0+ 1^b 0+ ... 0+ 1^z 0* `` 来描述长度为 `a, b, ..., z` 的连续块，其中 `1` 是填充的方块，`0` 是空白方块。Gecode 将表达式转换为有限状态机，并约束每一行和每一列都遵循该状态机。Gecode 6.4.0 示例（https://github.com/Gecode/gecode/blob/release-6.4.0/examples/nonogram.cpp）仍然使用同样的紧凑思想。 Jan Wolter 后来将该示例收录进他关于 Paint-by-Number 求解器的广泛调查（https://webpbn.com/survey/#gecode）中。他的评价相当不错：这个小型演示模型与那些大得多的专门求解器相比，表现得惊人地好。 MiniZinc 模型直接构建并应用相同的自动机。其连续块线索是列表，因此行和列可以包含不同数量的连续块而无需填充。函数 `line_regexp` 从每个列表构建正则表达式字符串。MiniZinc 将该字符串编译为有限状态机，`regular`（https://docs.minizinc.dev/en/stable/lib-globals-extensional.html#regular）将其应用于一行或一列。 ```minizinc include "globals.mzn"; enum CellStates = {Empty, Filled}; int: rows; int: columns; set of int: Rows = 1..rows; set of int: Columns = 1..columns; array[Rows] of list of int: row_runs; array[Columns] of list of int: column_runs; array[Rows, Columns] of var CellStates: board; function string: line_regexp(list of int: runs) = "Empty* " ++ join(" Empty+ ", [ "Filled{" ++ show(run) ++ "}" | run in runs ]) ++ " Empty*"; % Runs [3, 2] become % "Empty* Filled{3} Empty+ Filled{2} Empty*" constraint forall (row in Rows) ( regular( board[row,..], line_regexp(row_runs[row]) )); constraint forall (column in Columns) ( regular( board[..,column], line_regexp(column_runs[column]) )); solve satisfy; ``` 新的图标包以固定版本的 Heroicons 2.2.0（https://github.com/tailwindlabs/heroicons/releases/tag/v2.2.0）和 Phosphor Icons 2.1.1（https://www.npmjs.com/package/@phosphor-icons/core/v/2.1.1）存档中的 SVG 作为起点。一个离线栅格化器将每个图标以高分辨率渲染，适配到四种棋盘尺寸之一，并将结果阈值化为填充和空白单元格。  > 一个被接受的图标。中间面板放大了栅格预览，使其像素可见。 每个源图标被分配到一种棋盘尺寸，因此同一图像不会以多种分辨率重新出现。选择器会拒绝填充率极端、连通分量过多、指纹重复或线索平衡不佳的栅格，然后偏向已审核或细节更丰富的轮廓。导入的位图必须满足推导出的线索，并且 Gecode 必须找不到第二个解。确定性重放记录了初始行模糊度和最大初始候选集，然后测量推理轮数和未解析单元格。这些测量结果与 Gecode 的搜索节点和失败次数一起，对每个尺寸内的有效实例进行排序。 ## Queens：围绕一个解生长区域  > 一次失败的假设识别了 9×9 Queens 棋盘上的区域 9 Queens（https://zayenz.se/blog/post/linkedin-queens/）是 Star Battle（https://www.puzzle-star-battle.com/）的一星形式：在每行、每列和每个彩色区域中放置一个皇后，且任意两个皇后不能相邻。生成器从一个有效的无接触皇后排列开始，并从每个皇后生长出一个正交连通的区域。然后它沿着区域边界扰动非皇后单元格，同时保持连通性。下面这个小型示例从基础解开始，然后显示围绕它生长出的候选区域边界。  > 添加区域之前的基础解。  > 围绕基础解提出的区域边界。  > 在第二解中，另一个有效解适用于这些边界，因此这是一个无效的谜题实例。  > 一个边界单元格的移动使预期解唯一。 谜题模型每行只需一个变量即可。其值就是皇后所在的列。`all_different` 处理列规则，而在每个皇后位置对区域矩阵进行索引则一次性处理所有彩色区域。 ```minizinc include "globals.mzn"; int: n; set of int: N = 1..n; enum Regions; array[N, N] of Regions: region; array[N] of var N: board; % Each queen is in a different column constraint all_different(board); % Each queen is in a different region constraint all_different (row in N) ( region[row, board[row]]); % Queens in neighbouring rows may not touch diagonally constraint forall (row in 1..n-1) ( abs(board[row] - board[row+1]) > 1); solve satisfy; ``` 区域的重命名以及方形棋盘的八种旋转和反射被约简为一种规范指纹，防止出现伪装成不同副本的同一谜题。生成器还限制了极小和极大的区域；我是在测量了已发布的 Linkedin Queens 棋盘后选择这些限制的。难度使用与 Scaling Sudoku 相同的传播和剃除配置，当没有配置能在不分支的情况下解出棋盘时，随后使用 `Search`。 ## Zip：要求一个反例  > 7×7 Zip 路径进行到第十四个单元格 在 Zip（https://www.linkedin.com/games/zip/）中，玩家绘制一条穿过每个单元格的路径，同时按顺序访问编号线索并避开树篱。生成器将路径表示为 Gecode 的 `circuit`（https://sofdem.github.io/gccat/gccat/Ccircuit.html）约束：每个棋盘单元格有一个后继节点，一个额外的返回节点将最后一个线索连接回线索 1。`circuit` 约束排除了不连通的子环路，而逆向的 `path` 和 `position` 视图则明确表达了编号顺序约束。 模型使用行和列偏移来表示正交移动。对于每个单元格，它尝试四个方向。MiniZinc 的 `default <>` 将越界查找转换为不存在的单元格；由于不存在的单元格不可能等于后继节点，因此棋盘外的方向会从析取中消失。这避免了一个单独的邻接矩阵。 ```minizinc include "globals.mzn"; int: rows; int: columns; int: cells = rows * columns; set of int: Rows = 1..rows; set of int: Columns = 1..columns; set of int: Cells = 1..cells; set of int: Nodes = 1..cells + 1; int: return_node = cells + 1; enum Directions = {Up, Right, Down, Left}; array[Directions] of int: row_offset = [-1, 0, 1, 0]; array[Directions] of int: column_offset = [0, 1, 0, -1]; array[Rows, Columns] of Cells: board = array2d(Rows, Columns, [cell | cell in Cells]); array[Cells, Cells] of bool: hedge; % Symmetric int: number_count; array[1..number_count] of Cells: numbered_cell; array[Nodes] of var Nodes: successor; array[Cells] of var Cells: path; array[Cells] of var Cells: position; constraint circuit(successor); constraint inverse(path, position); constraint successor[return_node] = numbered_cell[1]; constraint successor[numbered_cell[number_count]] = return_node; constraint forall ( row in Rows, column in Columns where board[row,column] != numbered_cell[number_count]) ( let {Cells: cell = board[row,column] } in exists (direction in Directions) ( successor[cell] = (board[ row + row_offset[direction], column + column_offset[direction] ] default <>) ) /\ not hedge[cell,successor[cell]] ); constraint path[1] = numbered_cell[1]; constraint path[cells] = numbered_cell[number_count]; constraint forall (step in 1..cells-1) ( successor[path[step]] = path[step+1]); constraint forall (number in 1..number_count-1) ( position[numbered_cell[number]] < position[numbered_cell[number+1]]); solve satisfy; ``` 为了决定显示哪些编号和树篱，Zip 生成器首先只显示第一个和最后一个编号。然后它询问求解器：“请给我一个与这些已显示信息一致的第二条路径。” 如果求解器找不到反例，那么这种显示已经足够。如果找到了反例，生成器就会根据这个反例增加额外的约束（例如，强制该反例中的某个特定转弯无效）。它重复这个过程，直到得到唯一解，或者放弃该候选。这种方式不是通过完成所有细节来得到唯一性，而是通过故意制造并修复反例。 [^1]: 剃除是一种更强形式的传播，它通过考虑某个变量试取边界值或单个值后的结果来进一步减少值域。