🤖 AI

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

This paper presents an SMT-based pipeline that synthesizes self-avoiding or layered paths from input patterns to serve as scaffolds for constructing both planar mazes and three-dimensional woven structures.

Original authors: Shengyi Wang

Published 2026-07-14

📖 5 min read🧠 Deep dive

CC BY 4.0

Original authors: Shengyi Wang

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

Imagine you have a secret message written in a blocky, pixelated font, like an old video game. You want to turn that message into a giant, walkable maze where the solution path traces the shape of the letters. But here's the twist: you don't just want a flat maze; you want one where the path can cross over itself like a woven basket, creating a 3D structure where one part of the path goes over another.

That's exactly what Shengyi Wang's paper does. It acts like a super-smart architect that takes a picture or text, figures out the perfect route through the pixels, and then builds a physical 3D model of a maze based on that route.

The Puzzle: Finding the Perfect Line

First, the computer has to find a single, continuous line that visits as many "on" pixels as possible without getting lost in loops or dead ends. You might think, "Hey, isn't this like the Traveling Salesman Problem, where a salesman tries to visit every city in the shortest way?"

The paper says no, that's a trap. While the Traveling Salesman Problem tries to find the shortest distance, this maze problem is more like trying to draw a single, unbroken line that visits every pixel exactly once (or twice, if it's a weaving path) without lifting your pen. If you try to use standard "shortest path" math, you might end up with diagonal shortcuts that break the grid rules, or you might get stuck in a loop that doesn't connect to the exit.

Instead, the author uses a method called SMT (Satisfiability Modulo Theories). Think of this as a very strict puzzle master. You give it a set of rules:

The Tiles: Imagine every pixel is a tile with little doors on its sides (top, bottom, left, right).
The Rules: If a tile has a door open to the right, the tile next to it must have a door open to the left.
The Goal: Connect the start door to the end door, visiting as many tiles as possible, without creating any closed loops.

The computer asks the SMT solver: "Is there any way to arrange these tiles so all the rules are happy?" If the answer is "Yes," it gives you the blueprint. If the answer is "No," it tells you to try a slightly smaller goal.

The Weaving Trick: Going Over and Under

Here is where it gets cool. In a normal flat maze, paths can't cross; they have to go around each other. But in a "woven" maze, the path can cross itself. How? By pretending the path is a rope. Sometimes the rope goes over another part of the rope, and sometimes it goes under.

To make this work mathematically, the computer splits every crossing point into two invisible layers: a "horizontal" layer and a "vertical" layer. It's like having two ghost paths running through the same spot, but they never actually touch. The computer makes sure the "over" path is always higher than the "under" path.

The paper notes that allowing these crossings actually makes the puzzle easier for the computer to solve. For example, with a small "infinity" symbol pattern, the computer found a perfect solution in just 1.1 seconds. But when they tried to force the path to be flat (no crossings), it sometimes couldn't find a solution at all, or it took much longer to find a path that missed a few pixels.

Building the 3D World

Once the computer has the perfect line, it's time to build the maze.

The Skeleton: First, it fills in the rest of the maze. Imagine the solution path is a golden thread. The computer uses a random-walk method (like a drunk person stumbling around but never crossing their own path) to fill in the empty spaces with walls and corridors, ensuring the golden thread remains the only way from start to finish.
The Height Map: For the 3D version, the computer has to decide how high to build the "over" bridges and how low to dig the "under" tunnels. It uses a clever trick: it assigns the "under" paths a height of 0 and the "over" paths a height of 2.
- Why 2? The paper proves that if you keep the crossing points far enough apart (no two crossings right next to each other), you can always build a staircase that goes up one step, then another, to get from the ground to the bridge without breaking the rules. It's like a game of "keep your feet on the ground" where you can only step up one block at a time.
The Construction: Finally, it turns these numbers into 3D shapes. The "under" paths become flat platforms. The "over" paths become bridges suspended above them. Stairs connect the different levels. The result is a physical-looking maze where you can see the path weaving through itself.

The Results

The author tested this on a few patterns.

For a small "infinity" symbol with 202 pixels, it took 1.1 seconds to find the path.
For a larger "A" pattern with 447 pixels, it took about 4.8 minutes.
For an "rt" pattern with 421 pixels, it took 19.1 minutes.

In these tests, the computer successfully built mazes where the solution path traced the letters perfectly. The 3D models show a red ribbon highlighting the solution, winding through the structure, going over and under itself, just like a woven basket.

So, what's the big takeaway? The paper shows that by treating maze creation as a logic puzzle rather than a geometry problem, we can automatically turn any shape into a complex, 3D woven maze. It's not magic; it's just a very strict set of rules that a computer can follow to build something that looks like it was hand-crafted by a master weaver.

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

Problem Definition

The paper addresses the challenge of constructing maze structures from arbitrary input patterns, such as text or shapes. The core problem is decomposed into three stages:

Rasterization: Converting an input pattern into a set of target grid positions.
Path Synthesis: Finding a valid path from a prescribed entry to an exit that traverses as many target grid positions as possible. This path must satisfy strict local movement rules (orthogonal steps) and global constraints (connectivity, no self-intersections for planar paths, or prescribed over-under crossings for woven paths).
Maze Construction: Expanding the synthesized solution path into a full maze (a spanning tree of the grid graph) and, for woven mazes, realizing the topology as a three-dimensional geometry with physical height separation.

The paper distinguishes between two primary path types: planar paths (self-avoiding, no crossings) and layered paths (allowing crossings with prescribed over-under relationships).

Methodology

1. SMT-Based Path Synthesis

The central contribution is a pipeline for synthesizing the solution path using Satisfiability Modulo Theories (SMT), specifically the quantifier-free theory of linear integer arithmetic (QF_LIA).

Tile-Based Representation: The grid is modeled using a set of 8 tile types (Figure 3) representing local connectivity patterns. Each grid position $(r, c)$ is assigned an integer variable $t_{r,c} \in \{1, \dots, 8\}$ .
Local Constraints:
- Adjacency: Enforced via bidirectional implications (e.g., hasRight at $(r,c)$ implies hasLeft at $(r, c+1)$ ).
- Boundary: Path segments cannot exit the defined grid domain except at designated entry/exit points.
- Coverage: The objective is to maximize the number of non-empty tiles (those not type 8) to cover the input pattern.
Global Connectivity Constraints:
- To prevent disconnected loops or multiple components, the authors introduce a parent-rank system. Every non-root node selects a parent neighbor with a strictly lower rank.
- Crossing Handling: For woven paths, a crossing tile (type 7) is modeled as two co-located virtual elements: a horizontal element ( $h$ ) and a vertical element ( $v$ ). The parent-rank constraints are instantiated separately for these virtual elements, ensuring that the path flows correctly through the over-under structure without forming invalid planar loops.
Solver Execution: The entire problem for a fixed coverage bound is encoded into SMT-LIB and solved in a single call using OpenSMT2.

2. Maze Construction (2D and 3D)

Once a valid solution path is synthesized, the paper details the construction of the full maze:

Topological Completion: The prescribed solution path is treated as a fixed subgraph. The remaining grid positions are connected to this subgraph using a spanning tree algorithm (Wilson's loop-erased random walk for planar mazes; a Kruskal-style approach for woven mazes). This ensures the final maze is "perfect" (unique path between any two cells) while preserving the synthesized solution path as the unique entry-exit route.
3D Geometric Realization (Woven Mazes):
- Height Planning: The paper proposes a fixed-level convention where all under-crossings are at height 0 and all over-crossings are at height $g$ (where $g=2$ ).
- Feasibility Proof: The authors prove that if crossing tiles are not adjacent (a spacing condition enforced during synthesis), this fixed-level assignment is compatible with local height-change constraints (adjacent nodes differ by at most 1 level).
- Optimization: A dynamic programming algorithm is used to minimize total height variation and overall profile for non-crossing nodes, ensuring smooth transitions (stairs) between levels.
- Geometry Generation: The height-labeled graph is converted into 3D primitives: platforms for nodes, bridges for over-crossings, connectors for same-level links, and stairs for level changes.

Key Results

The paper presents experimental results using OpenSMT2 on an M1 Max MacBook Pro:

Small Instance ("∞" pattern, $|P|=202$ ): Solved in ~1.1 seconds with full coverage using 3,232 variables and 5,503 constraints.
Larger Instances:
- "A" pattern ( $|P|=447$ ): Solved in ~4.8 minutes.
- "rt" pattern ( $|P|=421$ ): Solved in ~19.1 minutes.
Crossing vs. Non-Crossing: The study observes that allowing crossings significantly increases the likelihood of finding a full-coverage solution. Non-crossing instances often require lowering the coverage bound to become satisfiable and frequently result in longer runtimes.
Visual Output: The paper provides examples of both planar mazes and complex 3D woven mazes (Figures 1, 6, and 7), demonstrating the successful translation from 2D patterns to 3D geometric structures.

Significance and Claims

The paper claims to extend a previous Bridges 2026 conference paper by providing a more comprehensive account of the transition from path synthesis to concrete maze construction.

Unified Framework: The methodology demonstrates that both planar and woven path structures can be derived from the same local primitives within a single SMT encoding, differing only in the allowance of crossing tiles.
Constraint-Based Reasoning: The work illustrates how SMT can effectively handle the complex interplay of local movement rules, global connectivity, and pattern coverage, solving fixed-bound existence questions in a single solver call without the need for iterative post-processing common in TSP or integer programming approaches.
Geometric Realization: The paper provides a rigorous, provable method for converting topological woven paths into physical 3D geometries with consistent height assignments, bridging the gap between combinatorial design and 3D construction.
Reproducibility: The authors provide open-source code for both the SMT-based path synthesis and the subsequent maze construction/geometry export, facilitating further research in this domain.

The paper maintains a modest tone, focusing on the technical pipeline and the specific contributions of the SMT encoding and the height-assignment algorithm, rather than claiming broad applicability beyond the scope of pattern-to-maze generation.