🤖 AI

From Patterns to Maze Structures: SMT-Based Path Synthesis and 2D/3D Construction

本文提出了一种基于 SMT 的流水线，该流水线通过从输入模式中合成自回避或分层路径，为构建平面迷宫和三维编织结构提供支架。

原作者： Shengyi Wang

发布于 2026-07-14

📖 1 分钟阅读☕ 轻松阅读

原作者： Shengyi Wang

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象一下，你有一个用块状、像素化字体（就像旧式视频游戏那样）书写的秘密信息。你想把这个信息变成一个巨大的、可步行的迷宫，而解题路径会勾勒出字母的形状。但这里有一个转折：你不仅想要一个平面的迷宫，你还想要一个路径可以像编织篮子一样相互交错、重叠的 3D 结构，其中一部分路径会从另一部分“上方”经过。

这正是王圣义（Shengyi Wang）的论文所做的事情。它就像一个超级聪明的建筑师，通过一张图片或一段文字，计算出完美的路径，并根据这条路径构建出一个物理 3D 模型迷宫。

谜题：寻找完美的线条

首先，计算机必须找到一条单一且连续的线，尽可能多地访问“开启”状态的像素，同时又不陷入循环或死胡同。你可能会想：“嘿，这不就像旅行商问题（Traveling Salesman Problem）吗？即推销员试图以最短路径访问所有城市。”

论文说不，那是一个陷阱。虽然旅行商问题试图寻找“最短距离”，但这个迷宫问题更像是尝试画出一条单一、不间断的线，在不抬笔的情况下访问每个像素一次（或者如果是一个编织路径，则是两次）。如果你尝试使用标准的“最短路径”数学方法，你可能会得到破坏网格规则的对角线捷径，或者陷入一个无法连接到出口的循环。

相反，作者使用了一种叫做 SMT（满足性模理论，Satisfiability Modulo Theories） 的方法。把它想象成一个非常严格的谜题大师。你给它一套规则：

瓷砖（Tiles）： 想象每个像素都是一块带有侧边小门的瓷砖（上、下、左、右）。
规则： 如果一块瓷砖向右打开了一扇门，那么相邻的瓷砖必须向左打开一扇门。
目标： 连接起点门和终点门，访问尽可能多的瓷砖，且不创建任何闭合回路。

计算机询问 SMT 解算器：“是否存在任何一种方式来排列这些瓷砖，使得所有规则都得到满足？”如果答案是“是”，它就会给你一份蓝图。如果答案是“否”，它会让你尝试一个稍微缩小一点的目标。

编织技巧：向上与向下

这是最酷的地方。在普通的平面迷集中，路径不能交叉；它们必须绕开彼此。但在“编织型”迷集中，路径可以自我交叉。怎么做到的呢？通过把路径伪装成一根绳子。有时绳子会经过另一段绳子的“上方”，有时则经过“下方”。

为了在数学上实现这一点，计算机将每个交叉点拆分为两个隐形层：一个“水平”层和一个“垂直”层。这就像是在同一个位置运行的两条幽灵路径，但它们实际上并不接触。计算机确保“上方”的路径始终高于“下方”的路径。

论文指出，允许这些交叉实际上让这个谜题对计算机来说变得更容易解决了。例如，对于一个小的“无穷大”符号图案，计算机仅用 1.1 秒 就找到了完美解。但当他们试图强制路径保持平面（不进行交叉）时，计算机有时根本找不到解，或者需要花费更长时间才能找到一个遗漏了一些像素的路径。

构建 3D 世界

一旦计算机有了完美的线条，建造迷宫的时间就到了。

骨架： 首先，它填充迷宫的其余部分。想象一下解题路径是一根金色的丝线。计算机使用随机游走法（类似于一个醉汉踉跄行走，但绝不会走过自己的路径）来用墙壁和走廊填满空白空间，确保那根金色的丝线是通往起点到终点的唯一路径。
高度图： 对于 3D 版本，计算机必须决定如何建造“上方”的桥梁以及如何挖掘“下方”的隧道。它使用了一个巧妙的技巧：它将“下方”路径的高度分配为 0，将“上方”路径的高度分配为 2。
- 为什么是 2？论文证明，如果你让交叉点保持足够的距离（没有两个交叉点紧挨在一起），你总能建造一个楼梯，先向上走一步，再走一步，从而从地面到达桥梁而不违反规则。这就像是一个“脚踏实地”的游戏，你只能一次迈上一个方块的高度。
施工： 最后，它将这些数字转化为 3D 形状。“下方”路径变成了平坦的平台，“上方”路径变成了悬挂在上面的桥梁。楼梯连接着不同的高度。结果是一个具有物理感的迷宫，你可以看到路径在自身之间编织穿梭。

结果

作者在几个图案上测试了这一点。

对于一个拥有 202 个像素的小型“无穷大”符号，它用了 1.1 秒 找到路径。
对于一个较大的“A”型图案（447 个像素），它大约用了 4.8 分钟。
对于一个“rt”型图案（421 个像素），它用了 19.1 分钟。

在这些测试中，计算机成功构建了路径完美勾勒出字母的迷宫。3D 模型展示了一条红色的丝带，它高亮显示了路径，在结构中蜿蜒穿行，在自身上方和下方穿梭，就像一个编织好的篮子一样。

那么，核心结论是什么？这篇论文表明，通过将迷宫创建视为一个逻辑谜题而非几何问题，我们可以自动将任何形状转化为复杂的 3D 编织迷宫。这并非魔法；这只是计算机遵循的一套非常严格的规则，它利用这些规则构建出了看起来像是出自编织大师之手的作品。

技术摘要：从图案到迷宫结构：基于 SMT 的路径合成与 2D/3D 构建

问题定义

本文解决了从任意输入图案（如文本或形状）构建迷宫结构的挑战。核心问题被分解为三个阶段：

光栅化（Rasterization）： 将输入图案转换为一组目标网格位置。
路径合成（Path Synthesis）： 寻找一条从预设入口到出口的有效路径，该路径尽可能多地遍历目标网格位置。该路径必须满足严格的局部移动规则（正交步进）和全局约束（连通性、平面路径的无自交性，或编织路径中预设的上下穿插关系）。
迷宫构建（Maze Construction）： 将合成的解路径扩展为完整的迷宫（网格图的生成树），并且对于编织迷宫，将其拓扑结构实现为具有物理高度差的三维几何体。

论文区分了两种主要的路径类型：平面路径（自回避，无交叉）和分层路径（允许带有预设上下关系的交叉）。

方法论

1. 基于 SMT 的路径合成

核心贡献是使用 满足性模理论（SMT），特别是无量词线性整数算术理论（QF_LIA），构建的路径合成流水线。

基于平铺的表示（Tile-Based Representation）： 网格使用一组 8 种平铺类型（图 3）进行建模，代表局部连通模式。每个网格位置 $(r, c)$ 被分配一个整数变量 $t_{r,c} \in \{1, \dots, 8\}$ 。
局部约束：
- 邻接性： 通过双向蕴含关系强制执行（例如， $(r,c)$ 处的 hasRight 蕴含 $(r, c+1)$ 处的 hasLeft）。
- 边界： 除指定的入口/出口外，路径段不能超出定义的网格域。
- 覆盖率： 目标是最大化非空平铺（即非类型 8 的平铺）的数量，以覆盖输入图案。
全局连通性约束：
- 为了防止不连通的环路或多个组件，作者引入了一个**父节点秩（parent-rank）**系统。每个非根节点选择一个具有严格较低秩的父节点邻居。
- 交叉处理： 对于编织路径，交叉平铺（类型 7）被建模为两个共位的虚拟元素：一个水平元素（ $h$ ）和一个垂直元素（ $v$ ）。父节点秩约束分别为这些虚拟元素实例化，以确保路径正确地流经上下穿插结构，而不会形成无效的平面环路。
求解器执行： 对于固定的覆盖界限，整个问题被编码为 SMT-LIB，并使用 OpenSMT2 进行单次调用求解。

2. 迷宫构建（2D 与 3D）

一旦合成了有效的解路径，论文详细说明了完整迷宫的构建过程：

拓扑补全： 预设的解路径被视为一个固定的子图。剩余的网格位置通过生成树算法连接到该子图（平面迷宫使用 Wilson 的回路擦除随机游走；编织迷的是使用类似 Kruskal 的方法）。这确保了最终迷宫是“完美的”（任何两点之间有唯一路径），同时保留了合成的解路径作为唯一的入口-出口路径。
3D 几何实现（编织迷宫）：
- 高度规划： 论文提出了一个固定层级约定，其中所有下穿处（under-crossings）都在高度 0，所有上穿处（over-crossings）都在高度 $g$ （其中 $g=2$ ）。
- 可行性证明： 作者证明，如果交叉平铺不相邻（在合成过程中强制执行的间距条件），则这种固定层级分配与局部高度变化约束（相邻节点高度差最多为 1）是兼容的。
- 优化： 使用动态规划算法来最小化非交叉节点的总高度变化和整体轮廓，确保层级之间的平滑过渡（楼梯）。
- 几何生成： 高度标记后的图被转换为 3D 原语：用于节点的平台、用于上穿处的桥梁、用于同层连接的连接器以及用于层级变化的楼梯。

主要结果

论文展示了使用 M1 Max MacBook Pro 运行 OpenSMT2 的实验结果：

小规模实例（“∞”图案， $|P|=202$ ）： 在约 1.1 秒内完成全覆盖求解，使用了 3,232 个变量和 5,503 个约束。
更大规模实例：
- “A”图案（ $|P|=447$ ）：求解时间约为 4.8 分钟。
- “rt”图案（ $|P|=421$ ）：求解时间约为 19.1 分钟。
交叉与非交叉对比： 研究观察到，允许交叉显著增加了找到全覆盖解的可能性。非交叉实例通常需要降低覆盖界限才能实现可满足性，并且经常导致更长的运行时间。
视觉输出： 论文提供了平面迷宫和复杂的 3D 编织迷宫的示例（图 1、6 和 7），展示了从 2D 图案到 3D 几何结构的成功转换。

重要性与主张

该论文声称通过提供从路径合成到具体迷宫构建更全面的描述，扩展了之前的 Bridges 2026 会议论文。

统一框架： 该方法论证明了平面路径和编织路径结构都可以通过单一的 SMT 编码从相同的局部原语导出，区别仅在于是否允许交叉平铺。
基于约束的推理： 这项工作阐明了 SMT 如何有效地处理局部移动规则、全局连通性和图案覆盖之间的复杂相互作用，在单次求解器调用中解决固定界限的存在性问题，而无需使用 TSP 或整数规划中常见的迭代后处理方法。
几何实现： 论文提供了一种严谨且可证明的方法，将拓扑编织路径转换为具有一致高度分配的物理 3D 几何体，弥合了组合设计与 3D 构建之间的鸿沟。
可复现性： 作者提供了用于 SMT 路径合成以及随后的迷宫构建/几何导出的开源代码，以促进该领域的进一步研究。

论文保持了谦逊的基调，侧重于技术流水线以及 SMT 编码和高度分配算法的具体贡献，而非声称其在路径到迷宫生成范围之外的广泛适用性。