Я захотел сделать Sokoban без JavaScript. Совсем. Только HTML и CSS.
На экране должна быть карта, человечек, ящики, цели и четыре кнопки: вверх, вниз, влево, вправо. Нажимаешь кнопку - человечек делает ход. Если перед ним ящик и за ящиком свободная клетка, ящик тоже сдвигается. Если ход невозможен, ничего не происходит. Когда все ящики стоят на целях, появляется поздравление и ссылка на следующий уровень.
Звучит как обычная маленькая браузерная игра, пока не вспоминаешь главное: CSS не умеет выполнять код.
Как вообще хранить состояние в CSS
В HTML есть элементы формы, которые могут хранить состояние сами по себе. Например:
1 | <input type="checkbox" id="x0"> |
Если нажать на label, браузер переключит checkbox. А CSS может увидеть это через
:checked:
1 | #x0:checked ~ .game { |
Это старый checkbox hack. Обычно его используют для табов, меню, модальных окон или простых игрушек. Но Sokoban неприятнее: один ход может менять сразу две вещи - позицию игрока и позицию ящика.
Первое искушение - хранить отдельно координаты игрока и координаты ящиков. Но тогда
push-ход должен за один клик поменять и игрока, и ящик. Один label так не умеет:
он связан с одним input. Значит состояние надо хранить целиком:
1 | состояние = где стоит игрок + где стоят все ящики |
И тогда один ход - это переход из одного целого состояния в другое.
Если состояние хранится в нескольких checkbox’ах, то каждое состояние можно представить бинарным числом. Например:
1 | 0000 |
Клик по label переключает ровно один checkbox. Значит любой допустимый ход должен
переводить нас в состояние, код которого отличается ровно одним битом.
Получается не совсем CSS-задача. Получается задача про граф.
Первый уровень
Для начала я взял совсем маленький уровень:
1 | #### |
Здесь # - стена, @ - игрок, $ - ящик, . - цель, на которую надо
поставить ящик. Пробелы - обычный пол.
Здесь один ящик, одна цель и почти нечего делать. Но даже у такого уровня уже есть нетривиальный граф состояний.
В первом ручном разборе я не останавливал игру сразу после победы. То есть если ящик уже стоит на цели, игрок всё ещё может походить вокруг. Поэтому получилось 15 состояний.
Начальное состояние:
1 | #### |
После хода вниз игрок толкает ящик на цель:
1 | #### |
А после хода вправо из начального состояния игрок просто переходит вправо:
1 | #### |
Если выписать все достижимые состояния и все переходы между ними, получится такой граф:
Вершина графа - это целое состояние игры. Теперь внутри каждой вершины нарисована карта: где стоит игрок и где стоит ящик. Сверху подписан номер состояния и бинарный код, который я подобрал руками. Зелёная рамка означает, что ящик уже стоит на цели. Серые линии - обычные обратимые перемещения. Оранжевые стрелки - push-переходы, которые в этой маленькой карте необратимы: ящик ушёл дальше, и обратно его уже не подтолкнуть.
Для CSS важнее всего не направление стрелки, а сам факт соседства. Если между двумя состояниями есть ход, их коды должны отличаться ровно одним битом.
Например:
1 | 0: 0000 |
Из состояния 0 можно попасть в 1 и 2.
1 | 0000 xor 0010 = 0010 // отличается один бит |
Дальше становится интереснее. У состояния 4 сразу три соседа:
1 | 1: 0010 |
И код 4 должен быть на расстоянии одного бита от каждого из них:
1 | 0011 xor 0010 = 0001 |
Это ещё можно подобрать руками. Но уже видно, что выбор кода для одной вершины влияет на много будущих переходов.
Ручная разметка
Вот вся ручная разметка этого уровня:
1 | 0: 0000 |
Четырёх checkbox’ов хватает для всех 15 состояний. Это почти минимум просто по количеству: в трёх битах есть только 8 разных кодов, а состояний 15.
После этого CSS устроен довольно механически:
1 | #x3:not(:checked) ~ #x2:not(:checked) ~ #x1:not(:checked) ~ #x0:not(:checked) ~ #board { |
Такое правило говорит: если текущее состояние 0000, поставь игрока в нужную клетку.
Другие правила в этом же состоянии показывают ящик и расставляют четыре label-кнопки
так, чтобы доступные направления переключали нужные checkbox’ы.
Например, если из 0000 ход вниз ведёт в 0010, значит кнопка “вниз” должна быть
label for="x1". Нажатие переключит второй бит, и браузер сам окажется в состоянии
0010.
На этом маленьком уровне всё получилось. Но это был ручной фокус, а не алгоритм. Следующий вопрос: можно ли такую разметку строить автоматически?
Попытка: идти по глубине
Первая идея автоматизации была такая: построить граф всех достижимых состояний, обойти его в ширину от начальной позиции и кодировать состояние по его глубине.
Глубина - это минимальное число ходов от старта. Начальное состояние имеет глубину 0,
его соседи - глубину 1, следующие состояния - глубину 2 и так далее.
Тогда можно попробовать назначать коды так, чтобы количество единичных битов равнялось глубине:
1 | depth 0: 0000000 |
На первый взгляд это очень похоже на то, что нужно. Если каждый новый ход просто
включает один новый бит, то один клик по label действительно меняет ровно один
checkbox.
На картинке это не готовое решение, а форма ограничения: все состояния на глубине
d должны получить код, в котором ровно d включенных битов.
Для маленького уровня состояния разбиваются по глубине так:
1 | depth 0: 0 |
Если следовать этому правилу буквально, понадобилось бы как минимум 7 битов:
самые дальние состояния лежат на глубине 7, значит в их коде должно быть 7
единиц. А для этой конкретной неостанавливающейся версии уровня даже 7 битов
мало: на глубине 7 два состояния, а в 7-битном числе с семью единицами есть
только один вариант - 1111111. Значит пришлось бы брать уже 8 битов или
как-то иначе ослаблять правило.
Это уже хуже ручной разметки, где хватило 4 битов. Но на этом этапе это казалось нормальной платой за автоматизацию: пусть код будет не минимальный, зато его можно будет строить механически.
Проблема начинается там, где у состояния несколько родителей.
Например, если в состояние C можно попасть из A и из B, то код C должен
отличаться одним битом и от A, и от B:
1 | A ---- C |
Если A = 0011, а B = 0101, то есть естественный кандидат:
1 | C = 0111 |
Он отличается от обоих родителей ровно одним битом. Отлично.
Но граф Sokoban - не дерево. В нём есть циклы: игрок может обойти ящик с другой стороны, вернуться к похожей позиции, сделать push из другого места. Из-за этого выбор кода в одном слое влияет не только на соседний слой, но и на ограничения, которые встретятся гораздо позже.
В gen-level.js я пытался решать это локально. Скрипт проходил состояния по глубинам,
для состояний с одним родителем выбирал, какой нулевой бит включить, а для состояний с
несколькими родителями пытался брать что-то вроде OR от родительских кодов. Если
вариантов было много, запускалась маленькая генетическая эвристика: сгенерировать
популяцию кандидатов, посчитать штрафы за конфликты, скрестить лучшие варианты,
немного помутировать и повторить.
Для простого уровня это ещё можно было заставить работать. Но на следующем уровне эвристика начинала тонуть.
И дело не в том, что генетический алгоритм был недостаточно хитрым. Ограничение
число единиц = глубина само по себе слишком жёсткое. Моя ручная 4-битная разметка
первого уровня уже нарушает это правило: например, состояние 10 находится на глубине
5, но имеет код 1000, где всего одна единица.
То есть хороший код может идти не только “вперёд”, включая новые биты. Иногда ход должен выключить бит. Checkbox не знает, вперёд мы идём по графу или назад, он просто переключается.
После этого стало понятно, что задача глубже, чем “придумать удобную нумерацию по слоям”. Нужно искать такое вложение всего графа, где каждое ребро меняет ровно один бит, а все вершины остаются различными. Это уже не локальная задача про BFS, а глобальная задача про форму графа.
Спросим solver
Следующая идея была: а что если вообще не придумывать правило разметки?
Не требовать, чтобы количество единиц совпадало с глубиной. Не пытаться идти по слоям. Не выбирать биты жадно. Просто описать условия, которым должна удовлетворять разметка, и попросить solver найти любые коды, если они существуют.
Для этого хорошо подходит Z3. Это SMT-solver: ему можно дать переменные и ограничения,
а он ответит sat, если нашёл значения, или unsat, если таких значений не бывает.
Для каждого состояния заводим переменную:
1 | code[0], code[1], code[2], ... |
Если мы хотим попробовать B checkbox’ов, то каждый code[i] - это B-битное
число. Дальше ограничения почти буквально повторяют CSS-механику:
1 | code[0] = 0 |
Первое условие означает, что начальное состояние - все checkbox’ы выключены. Это удобно для HTML: страница открылась, ничего ещё не нажато, мы уже в стартовой позиции.
Второе условие нужно потому, что код - это всё состояние игры. Если два разных состояния получат одинаковый код, CSS не сможет понять, где должен быть игрок, где ящики и какие кнопки сейчас доступны.
Третье условие - самое важное. Для двух соседних состояний считаем:
1 | x = code[i] xor code[j] |
xor показывает, какие биты отличаются. Нам нужно, чтобы отличался ровно один бит.
Для этого есть классический трюк:
1 | x != 0 |
Почему это работает? Если в числе включен ровно один бит, то число является степенью двойки:
1 | 00010000 |
Если вычесть 1, все младшие нули превратятся в единицы, а этот единственный
включенный бит выключится:
1 | 00010000 - 1 = 00001111 |
И тогда пересечение будет нулевым:
1 | 00010000 |
А если включенных битов больше одного, хотя бы один из них останется:
1 | 00010100 |
То есть условие x & (x - 1) == 0 проверяет, что x содержит не больше одного
включенного бита. А x != 0 отдельно запрещает случай, когда коды вообще одинаковые.
В итоге вся задача для solver’а становится очень маленькой по смыслу:
1 | найди разные B-битные числа для всех вершин графа, |
В самом .smt2-файле для Z3 это выглядит непривычно, но не страшно. Например,
если мы пробуем 8 checkbox’ов, то переменные объявляются как 8-битные числа:
1 | (set-logic QF_BV) |
Начальное состояние фиксируем нулём:
1 | (assert (= c0 (_ bv0 8))) |
А ребро между состояниями 0 и 1 записывается так:
1 | (assert |
Это ровно та же проверка:
1 | t = c0 xor c1 |
Только записанная в синтаксисе SMT-LIB: bvxor - xor для bitvector’ов,
bvand - побитовое and, bvsub - вычитание.
В конце файла добавляется ограничение, что все состояния различны, и команда “попробуй решить”:
1 | (assert (distinct c0 c1 c2 c3 ...)) |
Если Z3 отвечает sat, он ещё и печатает найденные значения c0, c1, c2 и
так далее. Эти значения потом можно положить в JSON и сгенерировать из них CSS.
В JavaScript-генераторе это выглядит почти так же. Скрипт просто собирает строки:
1 | for (let i = 0; i < N; i++) { |
То есть никакой хитрой процедуры поиска здесь нет. JavaScript строит граф Sokoban и печатает формулы, а Z3 уже сам ищет подходящие бинарные коды.
Для маленького уровня можно посмотреть полный файл целиком: level0-nonabsorbing-b4.smt2.
Он сгенерирован такой командой:
1 | node scripts/embed-z3-direct.mjs levels/level0.txt 0 4 0 \ |
Параметры здесь такие:
1 | levels/level0.txt // входной уровень |
Если запустить Z3 на этом файле:
1 | z3 dist/embeddings/level0-nonabsorbing-b4.smt2 |
он отвечает:
1 | sat |
А дальше печатает модель - конкретные значения переменных. В шестнадцатеричном виде
это выглядит вроде #x0, #x1, #xf; если перевести в двоичный вид и отсортировать
по номеру состояния, получается:
1 | 0: 0000 |
Это не та же самая разметка, которую я подобрал руками. Но она тоже правильная:
все 15 состояний разные, стартовое состояние равно 0000, и каждое ребро графа
меняет ровно один бит.
Для первого уровня Z3 тоже находит 4-битное решение. Оно может отличаться от моей ручной разметки, и это нормально: правильных разметок может быть много. Важно, что каждый ход всё равно переключает ровно один checkbox.
Гораздо интереснее оказался следующий уровень. В level1 уже 140 состояний. Значит
7 checkbox’ов точно не хватит просто по количеству:
1 | 2^7 = 128 |
А 8 checkbox’ов хватило. Solver нашёл разметку, где все 140 состояний различны, и каждый переход меняет ровно один бит.
Это приятный момент: для level1 получилось не просто “какое-то рабочее решение”, а
минимальное возможное число checkbox’ов. Меньше 8 быть не может, потому что некуда
положить 140 разных состояний. А 8 уже работает.
Так неудачная генетическая эвристика превратилась в точную задачу:
1 | граф состояний Sokoban нужно вложить в гиперкуб |
Гиперкуб - это просто все бинарные строки длины B, соединённые рёбрами, если они
отличаются ровно одним битом. В четырёх битах это 16 вершин, в восьми битах - 256
вершин. Нам не нужно занимать их все; нужно только аккуратно разложить внутри них
состояния игры.
На этом месте я попробовал применить прямой Z3-подход к другим уровням.
Результат получился такой:
1 | level0: 15 состояний, 4 checkbox'а |
Для этих уровней всё хорошо: solver быстро находит binary-разметку, и для level1
она даже минимальная.
А дальше начинаются другие масштабы:
1 | level4: 3789 состояний |
Формулировка задачи не меняется, но прямой solver начинает тяжело думать. Особенно
дорого стоит требование все code[i] различны: для тысяч состояний это уже очень
много пар, которые нужно удерживать в голове одновременно.
И даже если solver найдёт разметку, остаётся вторая проблема: CSS тоже растёт по числу состояний. Для каждого состояния надо уметь нарисовать игрока, ящики и правильно подключить кнопки направлений.
Значит точная binary-разметка - очень красивый метод для маленьких уровней, но не финальный ответ для всей игры.