从模式到迷宫结构：基于SMT的路径合成与2D/3D构建

# 从图案到迷宫结构：基于SMT的路径合成与2D/3D构建  
来源：https://arxiv.org/html/2607.09781  

###### 摘要。  
我们提出了一种从输入图案（如文字或形状）构建迷宫结构的流水线。核心的路径合成问题被编码为可满足性模理论（Satisfiability Modulo Theories, SMT）中的全局约束，涉及邻接性、连续性和图案约束覆盖，使得每个固定规模的实例只需一次调用即可求解。所得路径要么是平面的、自回避的路线，要么是具有预设上/下交叉的分层遍历，并作为构建平面迷宫和三维编织迷宫实现的骨架。本报告扩展了已发表的Bridges 2026会议论文，增加了更具代表性的SMT-LIB示例，并更全面地描述了合成路径如何具体转化为平面和三维形式的迷宫构建。††版权：无  

## 1. 引言  
本报告扩展了Bridges 2026会议论文（Wang, 2026 (https://arxiv.org/html/2607.09781#bib.bib4)），该论文引入了基于SMT从输入图案合成迷宫解路径的公式化方法。当前版本保留了该公式，但将范围从路径合成拓宽到迷宫构建。具体而言，它给出了更具代表性的SMT-LIB片段，描述了合成路径如何被补全为平面和编织迷宫结构，并开发了将分层交叉实现为三维迷宫几何所需的高度信息。我们从同一输入图案中推导出两条不同的迷宫解路径：一条平面路径和一条具有交叉的分层路径。每条解路径随后作为迷宫构建的骨架。图1 (https://arxiv.org/html/2607.09781#S1.F1)给出了由此产生的平面迷宫和编织迷宫的示例，分别带有和不带高亮解路径。  

参见图注(a) 参见图注(b) 参见图注(c) 参见图注(d)  
**图1.** 从同一“∞”解图案推导出的平面迷宫和编织迷宫：(a) 平面迷宫，(b) 带解的平面迷宫，(c) 编织迷宫，(d) 带解的编织迷宫。  
四张从无穷形状图案推导出的迷宫图像，展示了平面和编织版本，分别带有和不带高亮解。  

本文所考虑的迷宫构建可视为一个三步过程，如图2 (https://arxiv.org/html/2607.09781#S1.F2)所示。首先，给定的文本或图像被转换为一组网格位置。其次，在该网格上构建一条路径，从指定的入口位置开始，到指定的出口位置结束，同时尽可能多地遍历目标网格位置。根据预期的迷宫类型，该路径可能被要求是平面的，或者允许分层交叉。第三，从所得路径生成迷宫。  

**输入图案（文本或图像）→ 网格位置（光栅化）→ 解路径（平面或分层）→ 迷宫构建**  
（步骤1 → 步骤2 → 步骤3）  
**图2.** 从输入图案到迷宫的三步流水线。  
从左到右的流水线：从输入图案到网格位置到解路径到迷宫构建。  

在这些步骤中，第一步是直接的，可以使用现有图像处理工具处理，例如光栅化后通过二值阈值化从输入图案中提取目标网格位置集。会议版本主要关注第二步：在保持对输入图案忠实的同时，找到一条满足全局结构约束的合适路径。本报告保留了该公式，并更详细地发展了第三步，包括平面迷宫补全和分层交叉的三维实现。第三步基于标准的迷宫生成思想，例如（Buck, 2015 (https://arxiv.org/html/2607.09781#bib.bib2)）中综述的那些。从图论角度看，平面迷宫生成可视为在底层网格图上构建一棵生成树，并受合成解路径约束。在分层情况下，交叉关系提供了额外的拓扑信息，在构建三维迷宫几何之前必须将其转化为兼容的高度数据。  

## 2. 路径合成  
本节描述作为后续迷宫构建组合骨架的解路径的合成。路径被建模为网格位置上的一系列移动，当允许编织路径时，还包含额外的交叉信息。在此阶段，目标不是构建迷宫墙壁或三维几何，而是获得一条满足规定局部移动规则、全局连通性要求和覆盖目标的合法路径。我们首先将此任务与更熟悉的路径优化问题进行比较，然后描述SMT编码，最后总结观察到的求解器性能。  

### 2.1. 问题分析  
我们首先考虑图1 (https://arxiv.org/html/2607.09781#S1.F1)和图1 (https://arxiv.org/html/2607.09781#S1.F1)中所示的平面设置，其中迷宫解是网格上的正交、自回避路径。给定由输入图案导出的一组网格位置，任务是构建一条从指定入口位置到指定出口位置的路径，并尽可能多地访问这些位置。一个自然的初步比较是旅行商问题（TSP），这是一个NP完全问题（Papadimitriou, 1977 (https://arxiv.org/html/2607.09781#bib.bib5)）。在其经典公式中，TSP寻求一条访问给定位置集的最短路径，并且此类最短解通常避免自交。这使得使用现有TSP求解器解决当前设置很有吸引力（Cook, 2012 (https://arxiv.org/html/2607.09781#bib.bib1)）。在理想情况下，如果一条路径通过相邻位置之间的连续移动访问了n个网格位置，则其总长度恰好为n-1。任何对角线段的长度都会大于1（√2 > 1），因此在存在单位步长连接时，最优解中不应出现对角线段。然而在实践中，由于两个原因，这种理想行为并不可靠。首先，由输入图案导出的网格位置集可能不允许路径达到n-1的界限，因此即使是最优解也可能不得不包含更长的连接。其次，在大规模实例上，实际求解器可能返回非最优路径，其中可能出现对角捷径。在这两种情况下，所得解都违反了预期的正交、网格跟随结构，并且需要大量临时的后处理。  

从图论角度看，该问题更准确地被描述为网格图上的哈密顿路径问题，而不是度量优化问题。哈密顿路径问题在一般图中是NP完全的（Garey和Johnson, 1979 (https://arxiv.org/html/2607.09781#bib.bib6)），这种困难性即使对于网格图也依然存在（Itai等人, 1982 (https://arxiv.org/html/2607.09781#bib.bib7)），从而排除了针对任意图案的简单构造性或纯局部解。现有的哈密顿路径/圈的SAT编码已经需要非平凡的全局连通性约束（Zhou, 2020 (https://arxiv.org/html/2607.09781#bib.bib8)），而将它们扩展到优化变体则相应地更加繁琐。  

另一种工作路线是由基于瓦片的方法构建单线画图所暗示的，例如Bosch和Snyder的方法（Bosch和Snyder, 2023 (https://arxiv.org/html/2607.09781#bib.bib3)）。在该设置中，局部路径片段在全局一致性约束下被组装，整体问题被公式化为（混合）整数线性规划。初始解可能包含额外的不相交环，可以通过合并它们或添加环消除不等式（类似于子途消除）并重新求解模型来处理。在我们的工作中，我们采用相同的基于瓦片的局部路径片段表示，但不同之处在于，我们不将整体问题公式化为整数规划，而是将全局连通性和图案覆盖约束编码为专门为迷宫路径设计的可满足性模理论（SMT）公式。现代SMT求解器为表达命题结构和整数约束提供了自然框架，允许每个固定规模的存在性问题在一次求解器调用中判定。基于瓦片的表示的一大优点是它能够在单一统一框架内表达结构上不同的路径类型。在这种表示下，平面和分层情况仅在交叉瓦片的可接受性上有所不同：平面路径禁止交叉，而分层路径允许交叉。这表明两种路径结构都源自相同的局部基元；平面情况仅通过不允许交叉瓦片而获得。  

### 2.2. SMT编码  
在描述约束编码之前，我们首先形式化底层路径构建问题。设P ⊂ N²为通过光栅化输入图案并保留对应于前景像素的位置而得到的有限网格位置(r,c)（行/列索引）集合。如果|r - r'| + |c - c'| = 1，则两个位置(r,c), (r',c') ∈ N²被称为相邻。给定两个指定位置s,t ∈ P，目标是找到一条正交路径 s = a₀, a₁, ..., aₙ = t，其中每个aᵢ ∈ P，且连续位置相邻。在平面设置中，每个网格位置最多被访问一次；在分层设置中，最多可被访问两次。在所有此类路径中，我们寻求最大化访问位置数量，即长度n。  

为了编码此路径构建问题，我们首先使用基于瓦片的公式化表示路径。每个网格位置与一个瓦片相关联，该瓦片指定局部路径连通性模式。图3 (https://arxiv.org/html/2607.09781#S2.F3)中所示的瓦片类型作为此表示的基本基元。在这种公式下，合法路径的存在性被简化为放置瓦片的问题，使得满足局部连通性约束，并且全局路径结构浮现出来。  

**图3.** 编码局部路径连通性模式的瓦片类型。  
八种瓦片类型，每种代表一种局部路径连通性模式或一个空瓦片。  

然后，我们将所得的瓦片放置问题编码为线性整数算术的无量词理论（QF_LIA），这是SMT的一个片段，允许同时推理布尔条件和整数线性约束。在此编码中，布尔变量表示由瓦片连通性导出的邻接和顺序决策，而整数约束强制全局属性，如连通性、度和覆盖。对于固定的覆盖界限，一次对SMT求解器的调用即可确定是否存在满足所有约束的合法路径，当实例可满足时返回一个模型，否则报告不可满足。  

对于每个网格位置(r,c) ∈ P，我们引入一个整数值瓦片变量 t_{r,c} ∈ {1,2,...,8}，其值选择图3 (https://arxiv.org/html/2607.09781#S2.F3)中所示的瓦片类型之一。局部连通性语义由一组关于瓦片类型的辅助函数指定，总结在(1)中。这些定义构成了所有后续局部和全局约束的基础。每个瓦片变量 t_{r,c} 被声明为一个整数，受约束于 inRange。  

(1)  
inRange(t) = 1 ≤ t ≤ 8,  
hasUp(t) = t ∈ {1,4,5,7},  
hasRight(t) = t ∈ {1,2,6,7},  
nonWhite(t) = 1_{t≠8},  
hasDown(t) = t ∈ {2,3,5,7},  
hasLeft(t) = t ∈ {3,4,6,7}.  

这些定义可以用SMT的标准输入语言SMT-LIB（Barrett等人, 2025 (https://arxiv.org/html/2607.09781#bib.bib13)）编码。例如：  
``  
(define-fun hasUp ((t Int)) Bool (or (= t 1) (= t 4) (= t 5) (= t 7)))  
(define-fun nonWhite ((t Int)) Int (ite (= t 8) 0 1))  
``  

使用(1)中定义的指示函数 nonWhite，我们通过参与路径的网格位置总数来衡量候选路径的长度。具体地，我们定义覆盖值(2)：  
C = ∑_{(r,c)∈P} nonWhite(t_{r,c})  
根据求解器支持，此覆盖可以直接最大化，或约束为超过规定的下界。在SMT-LIB中，后者通过断言覆盖约束来表达：  
``  
(assert (>= (+ (nonWhite tile_3_1) (nonWhite tile_3_2) ...) K))  
``  
如果支持，此约束也可以替换为直接最大化目标。  

#### 2.2.1. 局部连通性约束  
局部连通性约束强制相邻瓦片之间的一致性，并调节路径如何与网格边界交互。我们首先施加邻接一致性，然后处理边界行为，区分一般边界位置与指定的入口和出口。  

对于任何两个水平相邻的网格位置(r,c)和(r,c+1)，从(r,c)右侧退出的路径段必须从(r,c+1)左侧进入。垂直相邻的条件类似。形式上，对于域内所有相邻的网格位置对，我们要求：  
hasRight(t_{r,c}) ⇔ hasLeft(t_{r,c+1}),  
hasDown(t_{r,c}) ⇔ hasUp(t_{r+1,c}).  

在导出域P的边界处，不允许路径段离开P：每当相邻位置不在P中时，该方向必须被禁用。对于P中除指定入口和出口位置之外的任何位置(r,c)，我们施加以下边界闭合约束：  
如果(r,c) ∉ {s,t} 且 (r,c-1) ∉ P ⇒ ¬hasLeft(t_{r,c}),  
如果(r,c) ∉ {s,t} 且 (r,c+1) ∉ P ⇒ ¬hasRight(t_{r,c}),  
如果(r,c) ∉ {s,t} 且 (r-1,c) ∉ P ⇒ ¬hasUp(t_{r,c}),  
如果(r,c) ∉ {s,t} 且 (r+1,c) ∉ P ⇒ ¬hasDown(t_{r,c}).  

指定的入口和出口位置 s = (r_s, c_s) 和 t = (r_t, c_t) 假定位于边界上，并被作为边界约束的显式例外处理。为了确保与外部的单一连接，每个端点处的瓦片类型根据其边界位置固定：如果端点位于左边界或右边界，则强制使用水平瓦片；如果它位于……（原文在此中断）