Автор играет с двухлетним сыном в деревянные поезда Brio. Сын не разрешает трогать паровозики, но позволяет строить треки. Постепенно автор начинает относиться к Brio как к алгоритмической задаче: можно ли из заданного набора деталей собрать замкнутый путь, где все разъёмы соединены?
Первый подход — рекурсивный перебор (backtracking). Кладётся деталь, затем следующая, если не подходит — откат назад. Для восьми кривых E solver находит круг за 254 состояния. Добавление двух прямых A увеличивает количество состояний до 1930 — экспоненциальный рост. Но на маленьких наборах перебор работает мгновенно.
Дальше появляются перекрёстки (crossing H3) и развилки (L и M branches). Граф трека становится сложнее. Backtracking справляется, но тупики обнаруживаются только когда кончаются детали. Автор пробует превратить задачу в задачу удовлетворения ограничений (CSP). Добавляет forward checking (короткие списки вариантов на каждый разъём) и conflict-directed backjumping (прыжок к истинной причине тупика). Вопреки ожиданиям, forward checking не помогает: Brio-тупики почти всегда глобальны, локальные списки остаются полными. Эффективной оказывается глобальная проверка — достаточно ли коннекторов и могут ли оставшиеся детали закрыть расстояния. Это сокращает поиск в 2–9 раз, но не на всех наборах.
Третий шаг — SAT solver. Проблема сводится к булевой выполнимости. Каждое возможное положение детали — своя переменная true/false. Но Brio не привязан к сетке, поэтому предварительно собираются все достижимые позиции через короткий поиск (scouting). SAT solver использует конфликтно-управляемое обучение клаузам (CDCL): запоминает причины противоречий в виде новых правил и не повторяет их. Это позволяет не просто проверить данный набор, а подобрать оптимальный — максимум разветвлений при минимальном количестве деталей (если что-то не закрывается, запрос ослабляется). Пример: два L и два M — семь узлов из 49 деталей.
Итог: три подхода отвечают на разные вопросы. Backtracking — быстрый и простой, но только «закроется ли этот набор?». CSP с глобальными ограничениями эффективнее, но тоже только для фиксированного набора. SAT solver меняет вопрос: «какие детали дадут самую сложную сеть?» — и хотя он медленнее и требует больше памяти, он умеет выбирать, а не проверять.