На пути к EXPTIME-трудности Raumschach: проверенная конструкция гаджетов
Кандидатная редукция от обобщённой географии, с механически проверенной корректностью гаджетов — подана на рецензирование
1. Введение
Классический результат Френкеля и Лихтенштейна (1981) показывает, что определение победителя обобщённой позиции n×n шахмат требует времени, экспоненциального по n, при любом фиксированном алгоритме, посредством редукции от PSPACE-трудной чередующейся формульной игры, играемой на планарном графе. Устойчивое техническое препятствие в этой конструкции, и в последующей работе, её расширяющей, состоит в том, что граф потока управления редукции в общем случае не планарен, что вынуждает использовать явный гаджет «пересечения проводников» для прокладки одного логического сигнала поверх другого на двумерной доске.
Raumschach, трёхмерный шахматный вариант 5×5×5, разработанный Фердинандом Мааком (1907), устраняет это препятствие по структурной причине: доска с подлинным третьим пространственным измерением допускает два коридора, не разделяющих одну плоскость, так что пересечение не является особым случаем, требующим собственного гаджета, — это попросту два непересекающихся пути. Эта работа развивает данное наблюдение в кандидатную редукцию и сообщает полностью как о текущем состоянии редукции, так и об ошибке, найденной и исправленной в процессе её проверки.
Эта работа следует дуге разработки, зафиксированной внутренне в Технических заметках IRF 1–15 (заметки 1–14 сохранены как институциональная запись, отдельно не публиковались) и сводной работе Raumschach и вычислительная сложность, которую эта работа заменяет собой конкретно в отношении конструкции условия победы / вентиля И (раздел 6 той работы), согласно исправлению в Технической заметке 15, которая опубликована. Читателям, желающим ознакомиться с анализом пространства состояний и размера дерева партии, не затронутым ничем в этой работе, следует обратиться непосредственно к той работе.
Чем эта работа является и чем не является. Это технический отчёт, описывающий набросок редукции, набор гаджетов и программу вычислительной проверки этих гаджетов на конечных экземплярах — включая один полностью проработанный нетривиальный пример с шестью булевыми переменными, реальной чередующейся игрой и подтверждённым матом. Это не завершённое, общее математическое доказательство того, что редукция корректна для произвольного размера формулы, и мы не заявляем здесь EXPTIME-трудность как установленную теорему. Мы точно описываем, где в настоящий момент проходит граница между «проверено на проверенных нами экземплярах» и «доказано для всех экземпляров», в разделе 8.
2. Предварительные сведения
2.1 Raumschach
Raumschach играется на доске 5×5×5, координаты (У, к, р) ∈ {1,…,5}3 в стандартной нотации (уровень, колонка, ряд). Фигуры включают обычные Ладью, Слона, Ферзя, Короля и Пешку, а также Единорога, который движется по чистым триагональным лучам — все три координаты меняются на ±1 на каждом шаге. Для редукции мы работаем на увеличенной доске n×n×n, где n полиномиально по размеру формулы, следуя стандартной практике в этой области исследований: использовать доску завышенного размера для встраивания редукции, а затем доказывать, что конструкция уважает тот набор фигур и те правила движения, которые определяет базовая игра.
2.2 Исходная задача
Мы редуцируем от двухигроковой чередующейся формульной игры в стиле формулировок «обобщённая география» / игра-QBF, используемых в конструкциях типа Френкеля–Лихтенштейна: булева формула φ(x1,…,xn) в некотором фиксированном базисе (здесь достаточно И и ИЛИ, по закону де Моргана и наличию подлинного НЕ через присвоение хода игроку — см. раздел 7), вместе с разбиением переменных между двумя игроками, Игроком A и Игроком B, и фиксированным порядком, в котором они устанавливаются. Игрок A выигрывает, если результирующее присвоение удовлетворяет φ; в противном случае выигрывает Игрок B. Определение того, у какого игрока есть выигрышная стратегия в таких играх, в общем случае PSPACE-полно, и литература по шахматным редукциям далее сочетает это с соображениями о размере доски, чтобы получить EXPTIME-трудность для задачи принятия решения на досках подходящего размера. Мы не выводим здесь заново этот общий теоретико-сложностный костяк; мы принимаем его как цель и сосредотачиваемся на редукции уровня доски.
2.3 Что должна делать корректная редукция
Редукция от этой игры к определению победителя позиции Raumschach должна предъявлять, для каждой формулы φ и разбиения/порядка переменных, позицию Raumschach такую, что: (а) позиция может быть построена за время, полиномиальное по |φ|; (б) ходы двух игроков в результирующей шахматной партии в точности соответствуют их выборам присвоения переменных, в том же порядке; и (в) белые (без потери общности — игрок, представляющий A) имеют форсированный выигрыш в шахматной партии тогда и только тогда, когда A имеет выигрышную стратегию в формульной игре. Каждый гаджет в разделе 4 существует, чтобы обеспечить выполнение некоторой части этого соответствия; раздел 5 указывает, гаджет за гаджетом, за какую часть отвечает каждый.
3. Обзор редукции
Доска разделена на непересекающиеся области: одна область на переменную формулы (коридор, оканчивающийся точкой бинарного ветвления, согласно разделу 4.1), одна область на логическую связку в дереве разбора формулы (экземпляр вентиля ИЛИ или И, разделы 4.3–4.4), заполнение предохранителем выравнивания темпа везде, где два коридора разной естественной длины подают сигнал в одну и ту же точку порядка чередования (раздел 4.5), и единственный гаджет условия победы (раздел 4.6), чья собственная легальность подключена — а не составлена через общее поле, см. раздел 5.4 — к итоговому значению истинности формулы. Безопасность Короля устанавливается один раз, независимо от формулы (раздел 4.6.1), с использованием шести из семи трёхмерных направлений полей бегства Короля, запечатанных обычным блокирующим материалом, и седьмого, оставленного открытым специально для того, чтобы быть закрытым собственным механизмом вскрытого шаха гаджета условия победы.
4. Гаджеты
4.1 Коридор переменной
Каждая переменная xi, контролируемая данным игроком, представлена Пешкой, ограниченной одной колонкой, продвигающейся на одну клетку за ход (Пешки Raumschach, как и их двумерный аналог, движутся ровно на одну клетку вперёд за не-взятие), с восхождением (второй тип одношагового хода Пешки, меняющий уровень на единицу), заблокированным неподвижной Ладьёй на каждой клетке вдоль коридора, кроме последней. На последней клетке и продвижение вперёд, и восхождение оставлены открытыми: восхождение представляет xi = Истина (Пешка полностью покидает уровень коридора), продолжающееся продвижение вперёд представляет xi = Ложь. Это реальное, единственное бинарное ветвление, разрешаемое фактическим ходом против фактического генератора легальных ходов, а не значением, предполагаемым заранее.
4.2 Межуровневый переход
Там, где путь сигнала в дереве разбора формулы на двумерной доске должен был бы пересечь другой такой путь, третье измерение Raumschach используется напрямую: пересекающий путь прокладывается через смежный уровень, при этом восхождение Пешки со сменой уровня (либо шаг Слона/Единорога, в зависимости от типа фигуры коридора) служит «переходом». Специализированный гаджет пересечения, какого требует планарная конструкция Френкеля–Лихтенштейна, не нужен; два коридора на разных уровнях попросту не пересекаются.
4.3 Вентиль ИЛИ
Единственному токену-Ладье выделяются ровно два действующих ладейных направления, каждое независимо огорожено токеном отрицания: присутствующим (блокирующим), если соответствующий вход Ложен, отсутствующим, если Истинен. Остальные четыре направления запечатаны навсегда. У токена есть легальный ход тогда и только тогда, когда открыто хотя бы одно из двух вентилируемых направлений, т.е. тогда и только тогда, когда истинен хотя бы один вход — реализуя ИЛИ. Этот гаджет не изменился по сравнению с разделом 7 сводной работы и не затронут ошибкой, описанной в разделе 6 ниже, поскольку его собственный токен не стоит на луче какой-либо атакующей фигуры.
4.4 Вентиль И (исправленный)
См. раздел 6 об ошибке, найденной в исходно специфицированной версии этого гаджета, и раздел 7 об исправленной конструкции: полностью запечатанная Ладья (все четыре боковых направления и «неправильное» направление огорожены) с ровно одним смежным блокирующим токеном, присутствующим тогда и только тогда, когда НЕ(xa И xb). Эта конструкция обобщается на более чем два входа лишь путём вложения экземпляров самой себя (И из И), а не путём сцепления нескольких токенов на линии одного вентиля; см. раздел 7.2.
4.5 Предохранитель выравнивания темпа
Там, где два коридора, подающих сигнал в одну и ту же точку порядка чередования, имеют разную естественную длину (число форсированных ходов продвижения до их точки ветвления), более короткий коридор заполняется дополнительными клетками форсированного продвижения (восхождение заблокировано, как в разделе 4.1), так что оба коридора достигают своей точки ветвления после одного и того же числа ходов. Это сохраняет строгое чередование ходов между двумя игроками при параллельных коридорах иначе несовпадающей длины.
4.6 Гаджет условия победы
Ладья V стоит в той единственной точке доски, где её собственная рядовая линия пересекается с триагональным лучом к Королю, — том же луче, который уже занимает назначенный атакующий Единорог, размещённый дальше по этому лучу со свободным путём. Четыре боковых направления V и её «неправильное» направление запечатаны навсегда; её единственное оставшееся направление удерживает ровно один смежный блокирующий токен (раздел 7.1), присутствующий тогда и только тогда, когда формула в целом Ложна. Если у V есть легальный ход — что, с учётом запечатывания, происходит тогда и только тогда, когда формула Истинна, — совершение этого хода освобождает домашнее поле V, вскрывая шах от Единорога вдоль теперь свободного луча прямо к Королю.
4.6.1 Безопасность Короля
Остальные шесть трёхмерных направлений полей бегства Короля (из его полной 26-соседней подвижности, минус одно направление вдоль использованного выше триагонального луча) запечатаны обычным блокирующим материалом (Пешками, Ладьями, Слонами, защищающими друг друга по мере необходимости), независимо от формулы, так что единственный способ, которым позиция Короля меняется с «безопасно, одно поле бегства» на «мат, ноль полей бегства и под шахом», — это механизм из 4.6, который вентилируется значением истинности формулы и ничем иным.
5. Корректность, гаджет за гаджетом
Мы формулируем свойство корректности, за которое отвечает каждый гаджет. Они сформулированы на том уровне строгости, который рецензент должен ожидать возможности проверить осмотром конструкции и, там, где существует вычислительная проверка, дополнительно подтвердить, что утверждение выполнялось на проверенных экземплярах; они не заявляются как машинно проверенные формальные доказательства.
5.1 (Коридор переменной). Для каждой переменной xi у Пешки коридора есть ровно один легальный ход на каждой клетке перед последней (форсированный, неинформативный относительно xi), и ровно два легальных хода на последней клетке, чьи назначения различимы исключительно по тому, разделяет ли назначение уровень коридора с исходной точкой (Ложь) или нет (Истина). Проверено вычислительно для длин коридора до 3 с заполнением предохранителем, раздел 9.
5.2 (Вентиль ИЛИ). У токена ИЛИ есть легальный ход тогда и только тогда, когда отсутствует хотя бы один токен отрицания входа. Проверено вычислительно для всех комбинаций входов до 4 входов (два независимых 2-входовых экземпляра, подающих сигнал в третий вентиль), раздел 9.
5.3 (Вентиль И, исправленный). У токена И есть легальный ход тогда и только тогда, когда отсутствует смежный блокиратор, что подключено происходить тогда и только тогда, когда оба входа Истинны. Это не утверждение о цепочке независимо подвижных токенов (что раздел 6 показывает ложным); это утверждение о присутствии или отсутствии единственного токена, что является более простым и, как мы полагаем, теперь корректно сформулированным свойством. Проверено вычислительно для всех комбинаций до 6 составленных переменных через 4 экземпляра вентилей, раздел 9.
5.4 (Композиция). Отдельные экземпляры вентилей занимают непересекающиеся клетки доски и непересекающиеся бесконечные линии (оси Ладьи, диагонали Слона, триагонали Единорога), кроме тех мест, где соединение намеренно (напр., выход вентиля ИЛИ, подключённый к блокиратору вентиля И), что проверяется механически через реестр коллизий координат (раздел 9.1), а не осмотром вручную. Мы считаем именно этот реестр, а не проверку человеком, надлежащим стандартом доказательности для этого конкретного утверждения, поскольку собственная ошибка заметки 15 возникла в точности из того рода случайного совпадения, для отлова которого и построен реестр.
5.5 (Условие победы). У V есть легальный ход тогда и только тогда, когда подключённое значение формулы Истинно, и совершение этого хода порождает фактический мат (Король под шахом, ноль легальных ответов), подтверждённый на генераторе легальных ходов, а не предположенный из геометрического описания гаджета. Проверено вычислительно для проработанного примера раздела 9.3.
6. Найденная ошибка и чему она учит
Исходно предложенная конструкция вентиля И (раздел 6 сводной работы, до исправления настоящей работой) сцепляла несколько независимо подвижных булевых токенов напрямую вдоль собственной рядовой линии V, исходя из рассуждения, что отступление V легально лишь тогда, когда каждый токен освободил место. Механическая проверка, с использованием того же генератора легальных ходов, на который опирается этот проект на всём своём протяжении, показала это ложным: луч атакующего Единорога вскрывается в тот момент, когда V покидает своё домашнее поле, по любой причине и на любое поле назначения, — а не только по достижении конкретного, полностью отступленного поля. Следовательно, важен лишь токен, ближайший к V: как только он освобождает место, у V появляется некий легальный ход независимо от состояния любого токена дальше по линии, и мат следует независимо от этого. Конструкция, в том виде, как она была специфицирована, вычисляла нечто более близкое к ИЛИ, чем к заявленному И. Полные детали, включая случай, изолирующий это от любого артефакта размещения, зафиксированы в Технической заметке IRF 15.
Мы сообщаем об этом не просто как об исправлении, а потому, что это иллюстрирует опасность, специфичную для этого стиля конструкции: гаджеты, построенные вокруг одной физической фигуры, служащей одновременно вычислительным элементом (здесь — цепочкой блокираторов рядовой линии) и компонентом механизма доставки мата (стоящей на луче атакующей фигуры), подтверждаются неполной проверкой-заместителем таким образом, что выглядят корректными, пока сам механизм мата не будет проверен напрямую и в сочетании. Каждый тест в этом проекте до того, что нашёл эту ошибку, проверял достижимость одного конкретного поля, а не реальное условие победы (есть ли у V вообще хоть какой-либо легальный ход); эти два вопроса совпадают лишь в однотокенном случае. Мы рассматриваем это как предостережение для рецензентов конструкций такого стиля в целом, а не только для данного конкретного гаджета.
7. Исправленная конструкция
7.1 Один токен, полностью запечатанный
Исправление (разделы 4.4, 4.6) ограничивает V, и любой вентиль И, построенный на том же принципе, ровно одним смежным блокирующим токеном, при этом все прочие направления — включая «неправильное» направление вдоль собственной оси вентиля — запечатаны навсегда. Этот случай был напрямую повторно подтверждён корректным: присутствие токена влечёт ноль легальных ходов; отсутствие токена влечёт ровно один легальный ход, чьё исполнение порождает подтверждённый мат (конкретно для V) либо намеченный логический сигнал (для внутреннего вентиля И).
7.2 Композиция через отделение, а не через совместное использование
Многопеременные формулы обрабатываются путём вычисления значения каждой подформулы с использованием вентилей, построенных полностью на координатах, не пересекающихся ни с V, ни с лучом какой-либо атакующей фигуры, так что движение собственного токена ни одного из под-вентилей не может само по себе спровоцировать вскрытый шах, и подключения результирующего значения к единственному смежному блокиратору следующего вентиля выше по дереву (в конечном счёте — к V). И более чем двух входов реализуется вложением экземпляров вентиля И (И из И), а не добавлением токенов на линию одного вентиля.
Это исправление имеет реальную цену, изложенную прямо, а не преуменьшенную: более не верно, что одна физическая фигура может нести тройную нагрузку, будучи одновременно собственным подвижным токеном подформулы, блокиратором рядовой линии и фигурой на атакующем луче, — как предполагала исходная конструкция и как предполагал, не проверяя, более ранний этап собственной проверочной работы этого проекта (до заметки 15). Композиция теперь требует явного шага подключения между проверенной подформулой и тем единственным токеном, который важен для следующего вентиля выше по дереву. Существует ли конструкция, восстанавливающая однотокенную композицию без подключения, не возрождая при этом изъян раздела 6, насколько нам известно, остаётся открытым.
8. Что установлено, а что нет
Мы считаем важным для документа, предназначенного для рецензирования, быть недвусмысленным в этом отношении.
Установлено, в смысле механически проверенного на конечных экземплярах: заявленное свойство корректности каждого отдельного гаджета (раздел 5), для конкретных проверенных размеров экземпляров; отсутствие коллизии координат для конкретных проверенных собранных экземпляров; и, для одной проработанной шестипеременной формулы с реальной чередующейся игрой и двумя выровненными по темпу коридорами, что полный конвейер — коридоры, вентили, композиция, условие победы — порождает минимаксное значение, совпадающее с независимым теоретико-игровым рассуждением об этой формуле, причём итоговая позиция выигрышной линии подтверждена как фактический мат на генераторе.
Не установлено: общее, параметрическое по размеру доказательство (напр., индукцией по структуре формулы) того, что конструкция корректна для произвольного n, произвольной глубины вложения и произвольного разбиения переменных между игроками; формальный учёт всех правил Raumschach, не задействованных построенными гаджетами (взятия, взаимодействующие с материалом гаджета за пределами того, что предусматривают собственные стены каждого гаджета, превращение, любое взаимодействие с троекратным повторением или правилом 50 ходов, и тонкости защищённых фигур за пределами аргумента безопасности Короля из 4.6.1); машинно проверенное или проверенное вручную формальное доказательство в том смысле, которого потребовал бы теоретик сложности для готовой к публикации в журнале теоремы трудности; и формальная граница, связывающая размер формулы с построенным размером доски n (необходимая для подтверждения того, что редукция подлинно полиномиальна по времени, а не лишь выглядит полиномиальной на опробованных экземплярах).
Соответственно, мы описываем общее утверждение этой работы так: исправленный набор гаджетов, переживший каждую проверку, которую мы смогли провести на независимом генераторе, представленный вместе с этими проверками, в поддержку предполагаемого результата EXPTIME-трудности для Raumschach, который мы пока не доказали в общем случае.
9. Методология вычислительной проверки
9.1 Реестр коллизий координат
Каждый экземпляр гаджета декларирует клетки доски, которые он занимает, и, для каждой подвижной фигуры, бесконечные линии (ось Ладьи, семейство диагональных плоскостей Слона, семейство триагоналей Единорога), вдоль которых она в принципе могла бы скользить. Реестр проверяет, по мере добавления каждого гаджета в сборку, разделяет ли он клетку или линию с любым ранее добавленным гаджетом, с которым не было явно декларировано намеренное соединение. Эта проверка статична (геометрическая), независима от легальности хода и специально спроектирована для отлова того класса ошибок — два по-отдельности корректных гаджета, совпадающих по случайному совпадению координат, — с которым этот проект сталкивался более одного раза в гаджетах, построенных до появления реестра.
9.2 Генератор легальных ходов
Независимый генератор ходов (скользящие ходы Ладьи, Слона, Единорога, Ферзя; шаг-и-безопасность Короля; одношаговое продвижение и восхождение Пешки) используется для прямой проверки каждого утверждения гаджета: наборы легальных ходов в конкретных позициях, статус шаха/мата Короля через square_attacked_by и полное перечисление ходов Короля, а для составного примера — полный поиск методом обратной индукции по каждому реальному ветвящемуся полуходу.
9.3 Проработанный пример
Формула φ = (ИЛИ(x1,x2) И ИЛИ(x3,x4)) ИЛИ И(x5,x6), шесть переменных, Игрок A контролирует x1,x4,x5, а Игрок B контролирует x2,x3,x6, была собрана с коридором x1 естественной длины 3 и коридором x2 естественной длины 1, дополненным 2-ходовым предохранителем, оба подтверждены как достигающие своей точки ветвления синхронно после ровно 3 форсированных ходов каждый, чередуемых ход за ходом. Полная обратная индукция по результирующему дереву партии из 64 листьев обнаружила, что у A есть форсированный выигрыш (φ = Истина при наилучшей игре), что совпадает с независимым рассуждением: A контролирует одну переменную в каждой клаузе ИЛИ первого дизъюнкта формулы и может форсировать обе клаузы в Истину в одностороннем порядке, независимо от любого выбора, доступного B. Терминальная позиция выигрышной линии была подтверждена как подлинный мат — Король под шахом, ноль легальных ответов — на генераторе, а не предположена из геометрии конструкции.
10. Связанные работы
Френкель и Лихтенштейн (1981) установили основополагающий результат, от которого происходит целевое утверждение о сложности этой работы, включая препятствие пересечения проводников, которое использование третьего пространственного измерения в этой работе призвано обойти. Нам не известны более ранние работы, применяющие это конкретное наблюдение к Raumschach; сводная работа, которую этот документ частично заменяет собой (раздел 6), представляет собственную более раннюю попытку этого проекта, здесь исправленную.
11. Заключение
Мы представили набор гаджетов для редукции чередующейся булевой формульной игры к определению победителя позиции Raumschach, исправили подлинную ошибку корректности, найденную в ходе механической проверки (задокументированную отдельно в Технической заметке 15), и проверили исправленную конструкцию вычислительно на экземплярах вплоть до шести переменных с реальной чередующейся игрой и подтверждённым матом. Мы считаем отдельные гаджеты и их композицию хорошо подкреплёнными этой проверкой, и мы считаем общее доказательство корректности для произвольного n, вместе с полным учётом правил Raumschach за пределами того, что задействуют гаджеты, открытой работой. Мы подаём эту работу в этом духе: как строгий, честно очерченный по объёму набросок для рецензирования, а не как закрытый результат.
Источники
- Fraenkel, A. S., & Lichtenstein, D. (1981). Computing a perfect strategy for n×n chess requires time exponential in n. Journal of Combinatorial Theory, Series A, 31(2), 199–214.
- Международная федерация Raumschach. (2026). Raumschach and Computational Complexity: State Space, Game-Tree Size, and an EXPTIME-Hardness Sketch. complexity-of-raumschach.html (анализ пространства состояний и размера дерева партии не затронут этой работой; раздел 6 заменён согласно Технической заметке 15).
- Международная федерация Raumschach. (2026). IRF Technical Note No. 15: The AND-Gate Does Not Gate. technical-notes-15.html (ошибка, исправленная в разделах 6–7 этой работы, в полных деталях).
- Международная федерация Raumschach. (2026). IRF Technical Notes, Nos. 1–14 (внутренний журнал разработки, предшествующий сводной работе; отдельно не публиковался).
- Maack, F. (1907). Raumschach (исходное описание варианта 5×5×5).