Resumo Técnico: De Padrões a Estruturas de Labirinto: Síntese de Caminhos Baseada em SMT e Construção 2D/3D

Definição do Problema

O artigo aborda o desafio de construir estruturas de labirinto a partir de padrões de entrada arbitrários, como textos ou formas. O problema central é decomposto em três estágios:

1. Rasterização: Conversão de um padrão de entrada em um conjunto de posições de grade alvo.
2. Síntese de Caminho: Encontrar um caminho válido de uma entrada prescrita para uma saída que atravesse o maior número possível de posições de grade alvo. Este caminho deve satisfazer regras estritas de movimento local (passos ortogonais) e restrições globais (conectividade, ausência de autointerseções para caminhos planares, ou cruzamentos sobre-baixo prescritos para caminhos tecidos).
3. Construção de Labirinto: Expansão do caminho da solução sintetizado em um labirinto completo (uma árvore geradora do grafo da grade) e, para labirintos tecidos, a realização da topologia como uma geometria tridimensional com separação de altura física.

O artigo distingue dois tipos primários de caminhos: caminhos planares (autoevitantes, sem cruzamentos) e caminhos em camadas (que permitem cruzamentos com relações sobre-baixo prescritas).

Metodologia

1. Síntese de Caminho Baseada em SMT

A contribuição central é um pipeline para sintetizar o caminho da solução usando Satisfatibilidade Modular de Teorias (SMT), especificamente a teoria livre de quantificadores da aritmética inteira linear (QF_LIA).

• Representação Baseada em Tiles: A grade é modelada usando um conjunto de 8 tipos de tiles (Figura 3) que representam padrões de conectividade local. Cada posição da grade $(r, c)$ recebe uma variável inteira $t_{r,c} \in \{1, \dots, 8\}$.
• Restrições Locais:
  • Adjacência: Aplicada via implicações bidirecionais (ex: hasRight em $(r,c)$ implica hasLeft em $(r, c+1)$).
  • Fronteira: Segmentos de caminho não podem sair do domínio definido da grade, exceto em pontos de entrada/saída designados.
  • Cobertura: O objetivo é maximizar o número de tiles não vazios (aqueles que não são do tipo 8) para cobrir o padrão de entrada.
• Restrições de Conectividade Global:
  • Para evitar loops desconectados ou múltiplos componentes, os autores introduzem um sistema de rank de pai (parent-rank). Todo nó que não é raiz seleciona um vizinho pai com um rank estritamente menor.
  • Tratamento de Cruzamentos: Para caminhos tecidos, um tile de cruzamento (tipo 7) é modelado como dois elementos co-localizados: um elemento horizontal ($h$) e um elemento vertical ($v$). As restrições de rank de pai são instanciadas separadamente para esses elementos virtuais, garantindo que o caminho flua corretamente através da estrutura sobre-baixo sem formar loops planares inválidos.
• Execução do Solver: Todo o problema para um limite de cobertura fixo é codificado em SMT-LIB e resolvido em uma única chamada usando OpenSMT2.

2. Construção de Labirinto (2D e 3D)

Uma vez que um caminho de solução válido é sintetizado, o artigo detalha a construção do labirinto completo:

• Conclusão Topológica: O caminho de solução prescrito é tratado como um subgrafo fixo. As posições restantes da grade são conectadas a este subgrafo usando um algoritmo de árvore geradora (caminhada aleatória com apagamento de loop de Wilson para labirintos planares; uma abordagem estilo Kruskal para labirintos tecidos). Isso garante que o labirinto final seja "perfeito" (caminho único entre quaisquer duas células) enquanto preserva o caminho sintetizado como a rota única de entrada-saída.
• Realização Geométrica 3D (Labirintos Tecidos):
  • Planejamento de Altura: O artigo propõe uma convenção de nível fixo onde todos os cruzamentos "baixo" estão na altura 0 e todos os cruzamentos "sobre" estão na altura $g$ (onde $g=2$).
  • Prova de Viabilidade: Os autores provam que, se os tiles de cruzamento não forem adjacentes (uma condição de espaçamento imposta durante a síntese), esta atribuição de nível fixo é compatível com as restrições locais de mudança de altura (nós adjacentes diferem em no máximo 1 nível).
  • Otimização: Um algoritmo de programação dinâmica é usado para minimizar a variação total de altura e o perfil geral para nós que não são de cruzamento, garantando transições suaves (escadas) entre níveis.
  • Geração de Geometria: O grafo rotulado por altura é convertido em primitivas 3D: plataformas para nós, pontes para cruzamentos "sobre", conectores para ligações de mesmo nível e escadas para mudanças de nível.

Principais Resultados

O artigo apresenta resultados experimentais usando OpenSMT2 em um MacBook Pro M1 Max:

• Instância Pequena (padrão "∞", $|P|=202$): Resolvida em ~1,1 segundos com cobertura total usando 3.232 variáveis e 5.503 restrições.
• Instâncias Maiores:
  • Padrão "A" ($|P|=447$): Resolvida em ~4,8 minutos.
  • Padrão "rt" ($|P|=421$): Resolvida em ~19,1 minutos.
• Cruzamento vs. Não-Cruzamento: O estudo observa que permitir cruzamentos aumenta significativamente a probabilidade de encontrar uma solução de cobertura total. Instâncias sem cruzamento frequentemente exigem a redução do limite de cobertura para se tornarem satisfatórias e frequentemente resultam em tempos de execução mais longos.
• Saída Visual: O artigo fornece exemplos de ambos os labirintos planares e complexos labirintos tecidos 3D (Figuras 1, 6 e 7), demonstrando a tradução bem-sucedida de padrões 2D para estruturas geométricas 3D.

Significância e Alegações

O artigo afirma estender um artigo anterior da conferência Bridges 2026 ao fornecer um relato mais abrangente da transição da síntese de caminho para a construção concreta de labirintos.

• Framework Unificado: A metodologia demonstra que tanto as estruturas de caminho planar quanto as tecidas podem ser derivadas dos mesmos primitivos locais dentro de uma única codificação SMT, diferenciando-se apenas pela permissão de tiles de cruzamento.
• Raciocínio Baseado em Restrições: O trabalho ilustra como o SMT pode lidar efetivamente com a complexa interação entre regras de movimento local, conectividade global e cobertura de padrão, resolvendo questões de existência de limite fixo em uma única chamada de solver sem a necessidade de pós-processamento iterativo comum em problemas de TSP ou programação inteira.
• Realização Geométrica: O artigo fornece um método rigoroso e provável para converter caminhos tecidos topológicos em geometrias 3D físicas com atribuições de altura consistentes, unindo a lacuna entre o design combinatório e a construção 3D.
• Reprodutibilidade: Os autores fornecem código de código aberto tanto para a síntese de caminho baseada em SMT quanto para a subsequente construção de labirinto/exportação de geometria, facilitando pesquisas adicionais neste domínio.

O artigo mantém um tom modesto, focando no pipeline técnico e nas contribuições específicas da codificação SMT e do algoritmo de atribuição de altura, em vez de reivindicar aplicabilidade ampla além do escopo da geração de padrões para labirintos.