SMT路径合成：文本形状自动生成2D/3D迷宫
速览
本文提出一种从文本或形状等输入模式构建迷宫结构的管道。核心路径合成问题被编码为可满足性模理论(SMT)中的全局约束，包括邻接、连续性和模式约束覆盖，一次调用即可求解固定边界实例。生成的路径可以是平面自避路径或具有指定交叉的三维遍历路径，并作为构建平面迷宫和三维编织迷宫的骨架。该报告扩展了Bridges 2026会议论文，提供更多SMT-LIB示例，展示了形式化方法在几何构造中的应用。
AI 深度解读
背景
迷宫作为一种古老而富有魅力的空间结构，长期以来被用于娱乐、教育和理论研究。传统迷宫设计依赖于手工绘制或启发式算法，难以精确地将用户指定的图案（如文字、形状）转化为迷宫路径。近年来，随着可满足性模理论（Satisfiability Modulo Theories, SMT）在组合优化和路径规划领域的成熟，研究者开始尝试用形式化方法自动生成符合复杂约束的路径。本文是发表在 Bridges 2026 会议上的论文的扩展版本，提出了一种基于 SMT 的管道，能够从任意输入图案（如文本或几何形状）合成迷宫结构，并进一步扩展到 2D 平面迷宫和 3D 编织迷宫的构建。
核心内容
本文提出了一套完整的迷宫构建管道，核心步骤为路径合成和结构构建。路径合成问题被编码为 SMT 实例，在固定边界的网格上通过一次求解器调用完成。SMT 编码建立了三类全局约束：
- 邻接约束：保证路径中相邻节点在几何上相连，形成连续的步进序列。
- 连续性约束：确保路径不自交、不间断，同时维持平面性（2D 情况）或允许指定的上下交叉（3D 情况）。
- 图案约束覆盖：路径必须覆盖输入图案所定义的区域，例如文字轮廓或形状内部，使得最终路径在宏观上呈现图案的形态。
求解器输出一条经典的自避行走路径（对于 2D 迷宫）或带有预设交叉点的分层遍历路径（对于 3D 编织迷宫）。该路径作为骨架，用于构造两类实体迷宫：
- 平面迷宫：将路径转化为墙壁和通道，生成传统二维迷宫。
- 三维编织迷宫：利用路径的上下交叉信息，在三维空间中构建类似编织结构的迷宫实体。
论文还提供了更具代表性的 SMT-LIB 编码示例，展示了如何将图案约束转化为逻辑公式，并详细说明了从合成路径到具体迷宫构造的完整映射过程。对比 Bridges 2026 会议短论文，本扩展版本更全面地覆盖了 SMT 模型的细节和二维/三维构造的步骤。
关键要点
- 编码方式：使用 SMT 一次性编码全部约束，无需迭代或启发式搜索，求解器直接返回满足条件的路径。
- 图案适应性：输入可以是任意文字、形状或用户定义的像素级图案，路径必须被图案区域“覆盖”。
- 路径类型：
- 2D 路径：平面、自避免（self-avoiding）的简单路径。
- 3D 路径：分层遍历路径，带有预设的“上-下”交叉点以模拟编织。
- 构造输出：
- 平面迷宫：传统的 2D 通道-墙壁结构。
- 3D 迷宫：编织迷宫实体，具有空间交错特性。
- 扩展内容：相比会议论文，增加了详细的 SMT-LIB 代码示例以及从路径到实体构造的完整流程描述。
意义与影响
该工作为图案驱动的自动迷宫生成提供了第一个形式化、可验证的 SMT 解决方案。其意义体现在三个方面：
- 方法论创新：将迷宫路径合成问题转化为 SMT 全局约束求解，避免了传统启发式算法的局部最优问题，确保输出严格满足所有约束。
- 跨维度统一：相同的 SMT 编码框架既支持平面迷宫，也支持三维编织迷宫，只需调整交叉约束即可，体现了框架的通用性。
- 艺术与工程结合：迷宫生成不仅是算法问题，更与视觉图案、文字艺术和交互设计相关。该管道使非程序员也能通过指定图案获得定制迷宫，为教育、游戏、数字艺术提供了新工具。
未来该工作可能进一步扩展到非矩形网格、动态约束或交互式迷宫设计，同时在 SMT 求解效率方面仍有优化空间（例如处理更大尺寸的图案）。本文为形式化方法在创意生成领域的应用提供了一个有趣且直观的案例。