🤖 AI

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

Este artículo presenta un flujo de trabajo basado en SMT que sintetiza caminos de autoevitación o estratificados a partir de patrones de entrada para servir como andamios para la construcción tanto de laberintos planos como de estructuras tejidas tridimensionales.

Autores originales: Shengyi Wang

Publicado 2026-07-14

📖 6 min de lectura🧠 Análisis profundo

CC BY 4.0

Autores originales: Shengyi Wang

Artículo original bajo licencia CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta es una explicación generada por IA del artículo a continuación. No ha sido escrita ni avalada por los autores. Para mayor precisión técnica, consulte el artículo original. Leer descargo de responsabilidad completo

Imagina que tienes un mensaje secreto escrito con una fuente pixelada y robusta, como la de un viejo videojuego. Quieres convertir ese mensaje en un laberinto gigante y transitable donde el camino de la solución trace la forma de las letras. Pero aquí está el giro: no quieres que sea un laberinto plano cualquiera; quieres uno donde el camino pueda cruzarse sobre sí mismo como una cesta tejida, creando una estructura 3D donde una parte del camino pase por encima de otra.

Eso es exactamente lo que hace el artículo de Shengyi Wang. Actúa como un arquitecto superinteligente que toma una imagen o un texto, deduce la ruta perfecta a través de los píxeles y construye un modelo físico 3D de un laberinto basado en esa ruta.

El rompecabezas: Encontrar la línea perfecta

Primero, la computadora tiene que encontrar una línea única y continua que visite tantos píxeles "encendidos" como sea posible sin perderse en bucles o callejones sin salida. Podrías pensar: "Oye, ¿no es esto como el Problema del Viajante, donde un vendedor intenta visitar cada ciudad de la forma más corta?".

El artículo dice que no, eso es una trampa. Mientras que el Problema del Viajante intenta encontrar la distancia más corta, este problema del laberinto es más como intentar dibujar una línea única e ininterrumpida que visite cada píxel exactamente una vez (o dos veces, si es un camino tejido) sin levantar el lápiz. Si intentas usar la matemática estándar de "camino más corto", podrías terminar con atajos diagonales que rompan las reglas de la cuadrícula, o podrías quedarte atrapado en un bucle que no conecta con la salida.

En su lugar, el autor utiliza un método llamado SMT (Satisfacibilidad de Teorías Modulares). Piensa en esto como un maestro de acertijos muy estricto. Le das un conjunto de reglas:

Las Baldosas: Imagina que cada píxel es una baldosa con pequeñas puertas en sus lados (arriba, abajo, izquierda, derecha).
Las Reglas: Si una baldosa tiene una puerta abierta hacia la derecha, la baldosa de al lado debe tener una puerta abierta hacia la izquierda.
El Objetivo: Conectar la puerta de inicio con la puerta de fin, visitando la mayor cantidad de baldosas posible, sin crear ningún bucle cerrado.

La computadora le pregunta al solucionador SMT: "¿Existe alguna forma de organizar estas baldosas para que todas las reglas se cumplan?". Si la respuesta es "Sí", te da el plano. Si la respuesta es "No", te dice que intentes un objetivo ligeramente menor.

El truco del tejido: Ir por encima y por debajo

Aquí es donde se pone genial. En un laberinto plano normal, los caminos no pueden cruzarse; tienen que rodearse unos a otros. Pero en un laberinto "tejido", el camino puede cruzarse a sí mismo. ¿Cómo? Fingiendo que el camino es una cuerda. A veces la cuerda pasa por encima de otra parte de la cuerda, y otras veces pasa por debajo.

Para que esto funcione matemáticamente, la computadora divide cada punto de cruce en dos capas invisibles: una capa "horizontal" y una capa "vertical". Es como tener dos caminos fantasma corriendo a través del mismo punto, pero que nunca se tocan realmente. La computadora se asegura de que el camino de "arriba" esté siempre más alto que el de "abajo".

El artículo señala que permitir estos cruces en realidad hace que el rompecabezas sea más fácil de resolver para la computadora. Por ejemplo, con un pequeño patrón de un símbolo de "infinito", la computadora encontró una solución perfecta en solo 1.1 segundos. Pero cuando intentaron forzar el camino a ser plano (sin cruces), a veces no podía encontrar una solución en absoluto, o tardaba mucho más en encontrar un camino que omitía algunos píxeles.

Construyendo el mundo 3D

Una vez que la computadora tiene la línea perfecta, es hora de construir el laberinto.

El Esqueleto: Primero, rellena el resto del laberinto. Imagina que el camino de la solución es un hilo dorado. La computadora utiliza un método de caminata aleatoria (como una persona ebria tropezando pero sin cruzar jamás su propio camino) para rellenar los espacios vacíos con paredes y pasillos, asegurando que el hilo dorado sea la única vía de principio a fin.
El Mapa de Altura: Para la versión 3D, la computadora tiene que decidir qué tan alto construir los puentes de "arriba" y qué tan profundo excavar los túneles de "abajo". Utiliza un truco ingenioso: asigna a los caminos de "abajo" una altura de 0 y a los caminos de "arriba" una altura de 2.
- ¿Por qué 2? El artículo demuestra que si mantienes los puntos de cruce lo suficientemente separados (que no haya dos cruces justo uno al lado del otro), siempre puedes construir una escalera que suba un escalón, luego otro, para ir desde el suelo hasta el puente sin romper las reglas. Es como un juego de "mantén los pies en el suelo" donde solo puedes subir un bloque a la vez.
La Construcción: Finalmente, convierte estos números en formas 3D. Los caminos de "abajo" se convierten en plataformas planas. Los caminos de "arriba" se convierten en puentes suspendidos sobre ellos. Las escaleras conectan los diferentes niveles. El resultado es un laberinto con apariencia física donde puedes ver el camino tejiéndose a través de sí mismo.

Los Resultados

El autor probó esto en algunos patrones.

Para un pequeño símbolo de "infinito" con 202 píxeles, tomó 1.1 segundos encontrar el camino.
Para un patrón de la letra "A" más grande con 447 píxeles, tomó alrededor de 4.8 minutos.
Para un patrón de "rt" con 421 píxeles, tomó 19.1 minutos.

En estas pruebas, la computadora construyó con éxito laberintos donde el camino de la solución trazaba las letras perfectamente. Los modelos 3D muestran una cinta roja resaltando la solución, serpenteando a través de la estructura, pasando por encima y por debajo de sí misma, tal como una cesta tejida.

Entonces, ¿cuál es la gran conclusión? El artículo muestra que, al tratar la creación de un laberinto como un acertijo lógico en lugar de un problema de geometría, podemos convertir automáticamente cualquier forma en un complejo laberinto 3D tejido. No es magia; es simplemente un conjunto de reglas muy estrictas que una computadora puede seguir para construir algo que parece haber sido diseñado a mano por un maestro tejedor.

Resumen Técnico: De Patrones a Estructuras de Laberinto: Síntesis de Caminos Basada en SMT y Construcción 2D/3D

Definición del Problema

El artículo aborda el desafío de construir estructuras de laberintos a partir de patrones de entrada arbitrarios, como texto o formas. El problema central se descompone en tres etapas:

Rasterización: Conversión de un patrón de entrada en un conjunto de posiciones de rejilla objetivo.
Síntesis de Caminos: Búsqueda de un camino válido desde una entrada prescrita hasta una salida que atraviese la mayor cantidad posible de posiciones de rejilla objetivo. Este camino debe satisfacer reglas de movimiento local estrictas (pasos ortogonales) y restricciones globales (conectividad, sin auto-intersecciones para caminos planos, o cruces sobre-bajo prescritos para caminos tejidos).
Construcción de Laberintos: Expansión del camino de solución sintetizado en un laberinto completo (un árbol de expansión de spanning tree del grafo de la rejilla) y, para laberintos tejidos, la realización de la topología como una geometría tridimensional con separación de altura física.

El artículo distingue entre dos tipos primarios de caminos: caminos planos (auto-evitables, sin cruces) y caminos por capas (permiten cruces con relaciones sobre-bajo prescritas).

Metodología

1. Síntesis de Caminos Basada en SMT

La contribución central es un flujo de trabajo para sintetizar el camino de solución utilizando Satisfacibilidad Mediante Teorías (SMT), específicamente la teoría libre de cuantificadores de la aritmética entera lineal (QF_LIA).

Representación Basada en Teselas: La rejilla se modela utilizando un conjunto de 8 tipos de teselas (Figura 3) que representan patrones de conectividad local. A cada posición de la rejilla $(r, c)$ se le asigna una variable entera $t_{r,c} \in \{1, \dots, 8\}$ .
Restricciones Locales:
- Adyacencia: Impuesta mediante implicaciones bidireccionales (por ejemplo, hasRight en $(r,c)$ implica hasLeft en $(r, c+1)$ ).
- Límite: Los segmentos del camino no pueden salir del dominio definido de la rejilla excepto en los puntos de entrada/salida designados.
- Cobertura: El objetivo es maximizar el número de teselas no vacías (aquellas que no son tipo 8) para cubrir el patrón de entrada.
Restricciones de Conectividad Global:
- Para evitar bucles desconectados o múltiples componentes, los autores introducen un sistema de jerarquía de padres (parent-rank). Cada nodo que no es la raíz selecciona un vecino padre con un rango estrictamente menor.
- Manejo de Cruces: Para caminos tejidos, una tesela de cruce (tipo 7) se modela como dos elementos co-localizados: un elemento horizontal ( $h$ ) y un elemento vertical ( $v$ ). Las restricciones de jerarquía de padres se instancian por separado para estos elementos virtuales, asegurando que el camino fluya correctamente a través de la estructura sobre-bajo sin formar bucles planos inválidos.
Ejecución del Solver: Todo el problema para un límite de cobertura fijo se codifica en SMT-LIB y se resuelve en una sola llamada utilizando OpenSMT2.

2. Construcción de Laberintos (2D y 3D)

Una vez sintetizado el camino de solución válido, el artículo detalla la construcción del laberinto completo:

Completitud Topológica: El camino de solución prescrito se trata como un subgrafo fijo. Las posiciones restantes de la rejilla se conectan a este subgrafo utilizando un algoritmo de árbol de expansión (spanning tree) (el paseo aleatorio de eliminación de bucles de Wilson para laberintos planos; un enfoque tipo Kruskal para laberintos tejidos). Esto asegura que el laberinto final sea "perfecto" (camino único entre cualquier par de celdas) mientras preserva el camino de solución sintetizado como la ruta única de entrada-salida.
Realización Geométrica 3D (Laberintos Tejidos):
- Planificación de Altura: El artículo propone una convención de niveles fijos donde todos los cruces bajo están a la altura 0 y todos los cruces sobre están a la altura $g$ (donde $g=2$ ).
- Prueba de Factibilidad: Los autores demuestran que si las teselas de cruce no son adyacentes (una condición de espaciado impuesta durante la síntesis), esta asignación de nivel fijo es compatible con las restricciones locales de cambio de altura (los nodos adyacentes difieren en máximo 1 nivel).
- Optimización: Se utiliza un algoritmo de programación dinámica para minimizar la variación total de altura y el perfil general para los nodos que no son de cruce, asegurando transiciones suaves (escaleras) entre niveles.
- Generación de Geometría: El grafo etiquetado con alturas se convierte en primitivas 3D: plataformas para los nodos, puentes para los cruces sobre, conectores para los enlaces del mismo nivel y escaleras para los cambios de nivel.

Resultados Clave

El artículo presenta resultados experimentales utilizando OpenSMT2 en un MacBook Pro M1 Max:

Instancia Pequeña (patrón "∞", $|P|=202$ ): Resuelta en ~1.1 segundos con cobertura total usando 3,232 variables y 5,503 restricciones.
Instancias Más Grandes:
- Patrón "A" ( $|P|=447$ ): Resuelto en ~4.8 minutos.
- Patrón "rt" ( $|P|=421$ ): Resuelto en ~19.1 minutos.
Cruces vs. No Cruces: El estudio observa que permitir cruces aumenta significamente la probabilidad de encontrar una solución de cobertura total. Las instancias sin cruces a menudo requieren reducir el límite de cobertura para ser satisfactorias y frecuentemente resultan en tiempos de ejecución más largos.
Salida Visual: El artículo proporciona ejemplos tanto de laberintos planos como de complejos laberintos tejidos en 3D (Figuras 1, 6 y 7), demostrando la traducción exitosa de patrones 2D a estructuras geométricas 3D.

Significado y Reivindicaciones

El artículo afirma extender un trabajo previo de la conferencia Bridges 2026 al proporcionar un relato más exhaustivo de la transición de la síntesis de caminos a la construcción concreta de laberintos.

Marco Unificado: La metodología demuestra que tanto las estructuras de caminos planos como las tejidas pueden derivarse de las mismas primitivas locales dentro de una única codificación SMT, diferenciándose solo por la permisibilidad de las teselas de cruce.
Razonamiento Basado en Restricciones: El trabajo ilustra cómo SMT puede manejar eficazmente la compleja interacción entre las reglas de movimiento local, la conectividad global y la cobertura de patrones, resolviendo preguntas de existencia de límite fijo en una sola llamada al solver sin la necesidad de un post-procesamiento iterativo común en los enfoques de TSP o programación entera.
Realización Geométrica: El artículo proporciona un método riguroso y demostrable para convertir caminos tejidos topológicos en geometrías 3D físicas con asignaciones de altura consistentes, cerrando la brecha entre el diseño combinatorio y la construcción 3D.
Reproducibilidad: Los autores proporcionan código de código abierto tanto para la síntesis de caminos basada en SMT como para la subsiguiente construcción de laberintos/exportación de geometría, facilitando la investigación adicional en este dominio.

El artículo mantiene un tono modesto, centrándose en el flujo de trabajo técnico y las contribuciones específicas de la codificación SMT y el algoritmo de asignación de altura, en lugar de reclamar una aplicabilidad amplia más allá del alcance de la generación de patrones a laberintos.