🤖 AI

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

이 논문은 평면 미로와 3차원 직조 구조를 구축하기 위한 스캐폴드(scaffold) 역할을 할 수 있도록, 입력 패턴으로부터 자기 회피(self-avoiding) 또는 레이어드(layered) 경로를 합성하는 SMT 기반 파이프라인을 제시한다.

원저자: Shengyi Wang

게시일 2026-07-14

📖 4 분 읽기☕ 가벼운 읽기

CC BY 4.0

원저자: Shengyi Wang

원본 논문은 CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) 라이선스로 제공됩니다. ✨ 이것은 아래 논문에 대한 AI 생성 설명입니다. 저자가 작성하거나 승인한 것이 아닙니다. 기술적 정확성을 위해서는 원본 논문을 참조하세요. 전체 면책 조항 읽기

당신이 옛날 비디오 게임처럼 투박하고 픽셀화된 폰트로 쓰인 비밀 메시지를 가지고 있다고 상상해 보세요. 당신은 이 메시지를 글자의 모양을 따라가는 경로가 되는 거대한, 걸어 다닐 수 있는 미로로 만들고 싶습니다. 하지만 여기 반전이 있습니다. 당신은 단순히 평면적인 미로를 원하는 것이 아니라, 마치 바구니를 엮는 것처럼 경로가 서로 교차하며 한 부분이 다른 부분의 '위'로 지나가는 3D 구조를 만들고 싶어 합니다.

이것이 바로 Shengyi Wang의 논문이 하는 일입니다. 이 논문은 사진이나 텍스트를 입력받아 픽로 사이의 완벽한 경로를 파악하고, 그 경로를 바탕으로 물리적인 3D 미로 모델을 구축하는 매우 똑똑한 설계자 역할을 합니다.

퍼즐: 완벽한 선 찾기

먼저, 컴퓨터는 루프에 빠지거나 막다른 길에 다다르지 않으면서 최대한 많은 '온(on)' 픽셀을 방문하는 하나의 연속된 선을 찾아야 합니다. 당신은 이렇게 생각할지도 모릅니다. "이거, 모든 도시를 가장 짧은 경로로 방문하려는 외판원 문제(Traveling Salesman Problem)와 비슷한 것 아닌가요?"

논문은 아니오, 그것은 함정이라고 말합니다. 외판원 문제가 가장 짧은 거리를 찾는 데 집중한다면, 이 미로 문제는 펜을 떼지 않고 모든 픽셀을 정확히 한 번씩(또는 엮는 경로라면 두 번) 방문하는 하나의 끊기지 않는 선을 그리는 것에 더 가깝습니다. 만약 표준적인 "최단 경로" 수학을 사용하려고 하면, 격자 규칙을 깨뜨리는 대각선 지름길이 생기거나 출구와 연결되지 않는 루프에 갇힐 수 있습니다.

대신, 저자는 **SMT (Satisfiability Modulo Theories)**라는 방법을 사용합니다. 이것을 매우 엄격한 퍼즐 마스터라고 생각해 보세요. 당신은 다음과 같은 규칙들을 부여합니다:

타일: 모든 픽셀은 옆면(위, 아래, 왼쪽, 오른쪽)에 작은 문이 있는 타일이라고 상상해 보세요.
규칙: 만약 어떤 타일에 오른쪽으로 열린 문이 있다면, 그 옆의 타일은 반드시 왼쪽으로 열린 문이 있어야 합니다.
목표: 시작 문부터 끝 문까지 연결하되, 가능한 많은 타일을 방문하면서도 폐쇄된 루프를 만들지 않습니다.

컴퓨터는 SMT 솔버에게 묻습니다: "모든 규칙을 만족하면서 이 타일들을 배치할 수 있는 방법이 단 하나라도 있습니까?" 만약 답이 "예"라면, 컴퓨터는 설계도를 제공합니다. 만약 "아니오"라면, 목표를 약간 줄여서 다시 시도하라고 알려줍니다.

직조의 기술: 위와 아래로 가기

여기서 아주 멋진 부분이 나옵니다. 일반적인 평면 미로에서는 경로가 서로 교차할 수 없으며 서로 돌아가야 합니다. 하지만 "직조된(woven)" 미로에서는 경로가 스스로 교차할 수 있습니다. 어떻게 그럴 수 있을까요? 경로를 '밧줄'이라고 가정하는 것입니다. 때때로 밧줄은 다른 부분의 밧줄 위로 지나가기도 하고, 때로는 아래로 지나가기도 합니다.

이를 수학적으로 구현하기 위해, 컴퓨터는 모든 교차점을 두 개의 보이지 않는 층, 즉 "수평" 층과 "수직" 층으로 나눕니다. 이는 마치 같은 지점을 통과하지만 실제로 서로 맞닿지는 않는 두 개의 유령 경로가 달리는 것과 같습니다. 컴퓨터는 "위"를 지나는 경로가 항상 "아래"를 지나는 경로보다 높게 유지되도록 만듭니다.

논문은 이러한 교차를 허용하는 것이 컴퓨터가 문제를 해결하는 데 실제로 더 쉽다는 점을 언급합니다. 예를 들어, 작은 "무한대(infinity)" 기호 패턴의 경우, 컴퓨터는 단 1.1초 만에 완벽한 해답을 찾아냈습니다. 하지만 경로를 평면으로 강제했을 때(교차 없이), 컴퓨터는 아예 해답을 찾지 못하거나 몇 개의 픽셀을 놓친 경로를 찾는 데 훨씬 더 오랜 시간이 걸리기도 했습니다.

3D 세계 구축하기

컴퓨터가 완벽한 선을 찾아내면, 이제 미로를 건설할 차례입니다.

골격: 먼저, 미로의 나머지 부분을 채웁니다. 해결 경로가 황금 실이라고 상상해 보세요. 컴퓨터는 무작위 보행(random-walk) 방식(마치 술 취한 사람이 비틀거리며 걷지만 자신의 경로를 가로지르지는 않는 것처럼)을 사용하여 빈 공간을 벽과 복도로 채우며, 황금 실이 시작부터 끝까지 가는 유일한 길임을 보장합니다.
높이 지도: 3D 버전을 위해, 컴퓨터는 "위"로 지나가는 다리를 얼마나 높게 쌓고 "아래"로 지나가는 터널을 얼마나 낮게 팔지 결정해야 합니다. 컴퓨터는 영리한 트릭을 사용합니다: "아래" 경로는 높이를 0으로, "위" 경로는 높이를 2로 할당합니다.
- 왜 2인가요? 논문은 교차 지점들이 서로 충분히 떨어져 있다면(교차 지점들이 바로 옆에 붙어 있지 않다면), 규칙을 어기지 않으면서 지면에서 다리까지 올라가기 위해 한 단계씩 올라가는 계단을 항상 만들 수 있다는 것을 증명합니다. 이는 마치 "발을 땅에 붙이고 있어라"라는 게임처럼, 한 번에 한 블록씩만 밟고 올라갈 수 있는 것과 같습니다.
건설: 마지막으로, 이 숫자들을 3D 형상으로 변환합니다. "아래" 경로는 평평한 플랫폼이 됩니다. "위" 경로는 공중에 매달린 다리가 됩니다. 계단은 서로 다른 높이의 층을 연결합니다. 그 결과, 경로가 스스로를 엮으며 지나가는 모습이 보이는 물리적인 형태의 미로가 완성됩니다.

결과

저자는 이 과정을 몇 가지 패턴에 테스트했습니다.

202 픽셀의 작은 "무한대" 기호의 경우, 경로를 찾는 데 1.1초가 걸렸습니다.
447 픽셀의 더 큰 "A" 패턴의 경우, 약 4.8분이 걸렸습니다.
421 픽셀의 "rt" 패턴의 경우, 19.1분이 걸렸습니다.

이 테스트들에서 컴퓨터는 해결 경로가 글자의 모양을 완벽하게 추적하는 미로를 성공적으로 구축했습니다. 3D 모델은 빨간 리본이 해결 경로를 강조하며, 마치 바구니를 짠 것처럼 구조물 사이를 오르내리며 엮여 지나가는 모습을 보여줍니다.

결론적으로 무엇을 배울 수 있을까요? 이 논문은 미로 생성을 기하학적 문제가 아닌 논리 퍼즐로 다룸으로써, 어떤 모양이든 복잡한 3D 직조 미로로 자동 변환할 수 있음을 보여줍니다. 이것은 마법이 아닙니다. 단지 컴퓨터가 따라갈 수 있는 매우 엄격한 규칙의 집합일 뿐이며, 이를 통해 마치 숙련된 직조공이 손으로 만든 것 같은 구조물을 만들어내는 것입니다.

기술 요약: 패턴에서 미로 구조로: SMT 기반 경로 합성 및 2D/3D 구축

문제 정의

본 논문은 텍스트나 도형과 같은 임의의 입력 패턴으로부터 미로 구조를 구축하는 과제를 다룹니다. 핵심 문제는 다음 세 단계로 분해됩니다:

래스터화(Rasterization): 입력 패턴을 대상 그리드 위치 집합으로 변환합니다.
경로 합성(Path Synthesis): 규정된 진입점에서 출구까지 최대한 많은 대상 그리드 위치를 통과하는 유효한 경로를 찾습니다. 이 경로는 엄격한 국소 이동 규칙(직교 단계)과 전역 제약 조건(연결성, 평면 경로의 경우 자기 교차 금지, 또는 직조 경로의 경우 규정된 상하 교차 관계)을 충족해야 합니다.
미로 구축(Maze Construction): 합성된 솔루션 경로를 전체 미로(그리드 그래프의 스패닝 트리)로 확장하고, 직조 미로(woven mazes)의 경우, 이를 물리적 높이 분리가 있는 3차원 기하 구조로 구현합니다.

본 논문은 두 가지 주요 경로 유형을 구분합니다: 평면 경로(자기 회피, 교차 없음)와 계층형 경로(교차를 허용하며 규정된 상하 관계를 가짐).

방법론

1. SMT 기반 경로 합성

중심 기여는 만족 가능성 모듈 이론(Satisfiability Modulo Theories, SMT), 구체적으로는 무한 양화사가 없는 선형 정수 산술 이론(QF_LIA)을 사용하여 솔루션 경로를 합성하는 파이프라인입니다.

타일 기반 표현: 그리드는 국소 연결 패턴을 나타내는 8가지 타일 유형(그림 3)을 사용하여 모델링됩니다. 각 그리드 위치 $(r, c)$ 에는 정수 변수 $t_{r,c} \in \{1, \dots, 8\}$ 가 할당됩니다.
국소 제약 조건:
- 인접성: 양방향 함의(예: $(r,c)$ 에서 hasRight이면 $(r, c+1)$ 에서 hasLeft임)를 통해 강제됩니다.
- 경계: 경로 세그먼트는 지정된 진입/출입 지점을 제외하고는 정의된 그리드 영역을 벗어날 수 없습니다.
- 커버리지(Coverage): 목표는 입력 패턴을 덮기 위해 비어 있지 않은 타일(타입 8이 아닌 타일)의 수를 최대화하는 것입니다.
전역 연결성 제약 조건:
- 끊어진 루프나 다중 컴포넌트를 방지하기 위해, 저자들은 부모-순위(parent-rank) 시스템을 도입합니다. 모든 루트가 아닌 노드는 엄격하게 낮은 순위를 가진 부모 이웃을 선택합니다.
- 교차 처리: 직조 경로의 경우, 교차 타일(타입 7)은 두 개의 공존하는 가상 요소인 수평 요소( $h$ )와 수직 요소( $v$ )로 모델링됩니다. 부모-순위 제약 조건은 이 가상 요소들에 대해 별도로 인스턴스화되어, 경로가 유효한 평면 루프를 형성하지 않고 상하 구조를 통해 올바르게 흐르도록 보장합니다.
솔버 실행: 고정된 커버리지 경계에 대한 전체 문제는 SMT-LIB으로 인코딩되며, OpenSMT2를 사용하여 단 한 번의 호출로 해결됩니다.

2. 미로 구축 (2D 및 3D)

유효한 솔루션 경로가 합성되면, 본 논문은 전체 미로의 구축 과정을 상세히 설명합니다.

위상적 완성(Topological Completion): 규정된 솔루션 경로는 고정된 부분 그래프로 취급됩니다. 나머지 그리드 위치는 스패닝 트리 알고리즘(평면 미로의 경우 Wilson의 루프 제거 랜덤 워크, 직조 미로의 경우 Kruskal 스타일 접근법)을 사용하여 이 부분 그래프에 연결됩니다. 이는 최종 미로가 "완벽한"(임의의 두 셀 사이에 유일한 경로가 존재함) 상태를 유지하면서도, 합성된 솔루션 경로를 유일한 진입-출구 경로로 보존하도록 보장합니다.
3D 기하학적 실현 (직조 미로):
- 높이 계획: 모든 하단 교차(under-crossing)는 높이 0에, 모든 상단 교차(over-crossing)는 높이 $g$ ( $g=2$ )에 위치하는 고정 레벨 관례를 제안합니다.
- 타당성 증명: 저자들은 교차 타일이 인접하지 않을 경우(합성 과정에서 강제되는 간격 조건), 이 고정 레벨 할당이 국소 높이 변화 제약 조건(인접한 노드는 높이가 최대 1단계 차이 남)과 호환됨을 증명합니다.
- 최적화: 비교차 노드에 대해 전체 높이 변화와 전체 프로파일을 최소화하기 위해 동적 계획법 알고리즘이 사용되어, 레벨 간의 매끄러운 전환(계단)을 보장합니다.
- 기하 구조 생성: 높이가 라벨링된 그래프는 3D 프리미티브로 변환됩니다: 노드를 위한 플랫폼, 상단 교차를 위한 브릿지, 동일 레벨 연결을 위한 커넥터, 그리고 레벨 변화를 위한 계단.

주요 결과

본 논문은 M1 Max MacBook Pro에서 OpenSMT2를 사용한 실험 결과를 제시합니다:

소규모 인스턴스 ("∞" 패턴, $|P|=202$ ): 3,232개의 변수와 5,503개의 제약 조건을 사용하여 전체 커버리지로 약 1.1초 만에 해결되었습니다.
대규모 인스턴스:
- "A" 패턴 ( $|P|=447$ ): 약 4.8분 소요.
- "rt" 패턴 ( $|P|=421$ ): 약 19.1분 소요.
교차 여부 비교: 연구 결과, 교차를 허용하는 것이 전체 커버리지 솔루션을 찾을 가능성을 크게 높이는 것으로 관찰되었습니다. 비교차 인스턴스는 만족 가능해지기 위해 커버리지 경계를 낮춰야 하는 경우가 많으며, 종종 더 긴 실행 시간을 요구합니다.
시각적 출력: 논문은 2D 패턴에서 3D 기하 구조로의 성공적인 변환을 보여주는 평면 미로와 복잡한 3D 직조 미로의 예시(그림 1, 6, 7)를 제공합니다.

의의 및 주장

본 논문은 경로 합성에서 구체적인 미로 구축으로의 전환에 대한 더 포괄적인 설명을 제공함으로써 이전의 Bridges 2026 컨퍼런스 논문을 확장한다고 주장합니다.

통합 프레임워크: 본 방법론은 단일 SMT 인코딩 내에서 교차 타일의 허용 여부만 다를 뿐, 두 가지 유형의 경로 구조가 동일한 국소 프리미티브로부터 유도될 수 있음을 보여줍니다.
제약 기반 추론: 본 연구는 SMT가 어떻게 복잡한 국소 이동 규칙, 전역 연결성, 그리고 패턴 커버리지 사이의 상호작용을 효과적으로 처리하여, TSP나 정수 계획법에서 흔리한 반복적인 후처리 없이 고정된 경계 존재 문제를 단일 솔버 호출로 해결할 수 있는지 보여줍니다.
기하학적 실현: 본 논문은 일관된 높이 할당을 가진 물리적 3D 기하 구조로 위상적 직조 경로를 변환하는 엄격하고 증명 가능한 방법을 제공하여, 조합론적 설계와 3D 구축 사이의 간극을 메웁니다.
재현성: 저자들은 SMT 기반 경로 합성 및 후속 미로 구축/기하 구조 내보내기를 위한 오픈 소스 코드를 제공하여, 이 분야의 추가적인 연구를 용이하게 합니다.

본 논문은 광범위한 적용 가능성을 주장하기보다는 기술적 파이프라인과 SMT 인코딩 및 높이 할당 알고리즘의 구체적인 기여에 집중하며 겸손한 어조를 유지합니다.