Автоматизация через логические ограничения
В статье, представленной на arXiv (2607.09781), описывается новый подход к процедурной генерации. Вместо случайного заполнения сетки, метод использует Satisfiability Modulo Theories (SMT) для кодирования глобальных ограничений. Это позволяет решить задачу синтеза пути за один вызов солвера, гарантируя соблюдение строгих правил: непрерывности, отсутствия самопересечений и соответствия входному паттерну (тексту или форме).
Два типа топологии путей
Результирующий путь служит каркасом для построения лабиринтов. Исследование выделяет два основных типа структур, которые могут быть сгенерированы:
- Плоские маршруты: самоизбегающие пути (self-avoiding routes) на двумерной плоскости.
- Слоистые обходы: трехмерные структуры с заданными пересечениями «сверху-снизу» (over-under crossings), имитирующими переплетения.
От абстракции к геометрии
Ключевая инновация заключается в трансформации абстрактного пути в конкретную геометрию. Синтезированный путь используется как скелет для:
- Построения классических 2D-лабиринтов.
- Создания 3D-реализаций «сплетенных» (woven) лабиринтов, где важно пространственное расположение элементов.
Практическая значимость
Метод расширяет результаты конференции Bridges 2026, предлагая не только теоретическую модель, но и примеры кода SMT-LIB. Это открывает возможности для точного контроля над формой лабиринтов, что может быть применено в геймдеве, архитектурном моделировании и визуализации данных, где важна не только сложность, но и эстетическая или функциональная структура пути.
Источник: arXiv cs.AI ↗