Solution to Problem #127

9-12 июля 2021 года прошёл очередной ICFPContest, в котором наша команда WinterMUTE снова приняла участие.

См. наши отчёты о предшествующих ICFPContest 2020, ICFPContest 2019 и ICFPContest 2018.

Задача

За две недели до начала контеста в твиттере организаторов появился анонс:

Slightly less than two weeks until ICFP Contest 2021 starts! We're looking forward to seeing some old friends again this year!

Old friends

А за несколько дней до начала контеста организаторы опубликовали загадочный спойлер:

Specification 1.0

Суть его стала понятна уже после публикации лаконичной спецификации на старте контеста, из которой следовало, что участники (а точнее, их решения) будут играть в популярное в Японии развлечение Human Tetris.

Specification 1.0

Входными данными для решения каждой проблемы были:

В качестве решения отправлялись целочисленные координаты вершин трансформированной фигуры.

Решение (поза) считалось корректным при выполнении следующих условий:

Далее для каждого корректного решения вычислялись "дизлайки" как сумма квадратов расстояний от каждого вершины дыры до ближайшей вершины трансформированной фигуры. Иными словами, меньше дизлайков получали решения, которые покрывали бОльшую часть дыры, оставаясь в её пределах.

На основе вычисленных дизлайков решения, а также минимальных дизлайков среди всех решений других команд и размерности решаемой проблемы вычислялась оценка отправленного решения:

Scoring

Взаимодействие участников и организаторов осуществлялось через простой HTTP API: получение JSON с описанием проблемы, отправка JSON с решением.

Наконец, организаторы заранее предупредили о расписании последующих апдейтов спецификации и публикации новых проблем через 12, 24, 36 и 48 часов.

Кстати, вот пример проблемы (и наш старый друг):

Problem #10

Команда

Как и в прошлом году во-многом из-за COVID-19 все взаимодействовали удалённо. Команда была распределённой, но в рамках всего нескольких часовых поясов.

Вначале для коммуникации мы планировали использовать сервис Gather, но из-за требовательности к ресурсам откатились на проверенный Google Meet, где практически нонстопом все сидели с видео и звуком.

Команда на этот раз была компактной, вот эти ребята:

Решение

Перед соревнованием мы решили, что наибольшим общим знаменателем для большинства участников остаётся Java, но всё равно практически сразу втащили в дополнение к Java язык Kotlin (и регулярно фрустрировались от скорости его компиляции).

Day 0

Когда прочитали спеку и поняли, что взаимодействовать с организаторами будем через API, а паковать свой код и отправлять его никуда не будет нужно, решили быстро перейти с Ant (где это всё у нас уже было реализовано) на Gradle. Чтобы было интерактивнее, попробовали кодить вместе через Code With Me, но отказались от этой идеи, когда осознали, что код, который одновременно редактируют несколько человек, почти никогда не компилируется. В итоге стали работать по-старому: через пуши в одну ветку без всякого code review и голосовые анонсы с изменениями и просьбами их подтянуть к себе.

Сперва занялись обязательными задачами. Я втащил Gradle. Антон взялся за модель предметной области и её (де)сериализацию. Андрей запилил клиента к API, выкачал и распарсил все доступные проблемы.

Возникло обоснованное подозрение, что задача в общем случае алгоритмически неразрешима и для лучшего понимания различных крайних случаев можно начать с разнообразных тактик модификации фигур. Фактически задачу можно свести к поиску оптимального решения системы нелинейных уравнений, т.е. нахождению целочисленных координат фигуры, которые удовлетворяют ряду ограничений: сохранение длин рёбер в допустимых пределах и нахождение всех рёбер в дыре -- а также минимизируют дизлайки, но к этому мы ещё вернёмся.

Олег начал пилить ламповый графический клиент (далее UI), без которого в текущем контесте было никуда. На Kotlin.

UI позволял отображать дыру и текущую позу, модифицировать позу через простой интерфейс Action, а также проверять различные инварианты: попадание в дыру, допустимое растягивание/сжатие рёбер и многое другое -- но об этом дальше, а пока UI выглядел так:

Our UI

Андрей реализовал базовые MoveAction и RotateAction на основе афинных преобразований Java AWT, а также проверку, что поза находится в дыре. Олег интегрировал их в UI и продолжил наращивать функциональность нашего главного интерфейса.

Я загорелся идеей реализовать PushAction, который позволит оттягивать/заталкивать вершины фигуры с сохранением соотношений ребёр (как будто мы толкаем вершины модели на шарнирах), и начал придумывать прототип:

Inventing PushAction

Через некоторое время стало понятно, что перемещение интересующей вершины в указанную пользователем точку с последующим поиском координат всех других вершин, удовлетворяющих топологии модели -- это практически та же задача, которую мы пытаемся решить изначально. Т.е. наивная реализация PushAction могла работать только в простейших случаях перемещения сегмента из отрезков.

Дело шло к ночи нулевого дня, но Олег не останавливался, реализовал проигрывание модификаций позы вперёд/назад во времени и подсвечивание цветами проблемных вершин:

Move/Rotate

Все ушли спать, но не Антон, который запилил FoldAction: он позволял складывать позу вдоль указанного отрезка в указанном направлении (как показала практика, наш основной боевой инструмент):

Before After

Day 1

Наступил следующий день.

FoldAction Антона и бурное развитие UI произвели фурор.

Андрей помогал с реализацией геометрии средствами Java AWT.

Олег переключился на геометрию, реализовал расчёт и отображение выпуклой оболочки, центрирование позы и дыры, а также AutoRotateAction, который совмещал основные направления позы и дыры:

Autorotate

После этого Олег реализовал AutoFoldAction, который использовал примитив Антона и пытался сворачивать позу, пока уменьшалась площадь её выпуклой оболочки.

Я на тот момент ещё не отказался от PushAction и пытался его доработать без значительного усложнения, но имеющиеся проблемы не позволяли его использовать, несмотря на возлагаемые надежды.

Антон реализовал отправку решений -- дело шло к окончанию Lightning Round (первые сутки контекста).

Очень хотелось что-то уже нарешать и отправить, поэтому Олег реализовал первую стратегию автоматического решения задач AutoKutuzoffStrategy. Она комбинировала реализованные к данному моменту Actionы: AutoFoldAction, смещения и повороты -- пытаясь, преобразовать и запихнуть фигуру в дырку.

И тут нас ждала первая засада.

Дело в том, что все координаты в постановке задачи и принимаемых решениях целочисленные, а мы всё считали в double. Но нельзя так просто взять и округлить double-координаты вершин, не изменив длины смежных рёбер (если вершина и так уже не находится в целых координатах). С учётом того, что граф фигуры связан, возникает каскадный эффект. До этого момента мы почему-то считали, что epsilon это просто хак, чтобы позволить участникам всё считать в double, а затем спокойно округлять. Но оказалось, что epsilon это жёсткое ограничение пространства валидных вариантов в условиях целочисленности координат.

Антон занялся этой проблемой и запилил PosifyAction, который берёт каждую вершину с double-координатами и пытается округлить её так (комбинации ceil()/floor для x/y), чтобы не нарушить ограничения на длины всех рёбер (с учётом epsilon).

Олег допилил и зафиксил AutoFoldAction, потому что в общем случае фигуру можно согнуть не по произвольному отрезку. В итоге мы даже что-то отправили в Lightning Round, но эти решения оказались невалидными, и тут мы поняли (в очередной раз), что надо работать над собственной валидацией решений перед отправкой. Кстати, организаторы и в этот раз подумали о brute force, поэтому решение каждой проблемы можно было присылать не чаще, чем раз в 5 минут.

Тем временем Lightning Round закончился, и было опубликовано обновление спеки: проблемы (и старые тоже) могли содержать бонусы, которые можно было взять, если поставить вершину своей позы на указанную точку, а затем эти бонусы можно было использовать, но уже при решении других проблем. Именно эти бонусы отмечены цветными кругами на приведённых примерах проблем. Мы решили не заниматься бонусами, пока не научимся хорошо решать основную задачу.

Обложили все Actionы проверками, чтобы вылавливать тех, кто трансформирует позу с поломкой ограничений, и остаток дня занимались вылавливанием и фиксом багов.

Day 2

Олег выделил отдельную эвристику WiggleAction, которая пыталась потеребить позу в небольших пределах с надеждой, что она влезет в дыру, а затем подключился к проблеме округлений и запилил сетку и функции отладки в UI:

Debug Posify

Отладка положения вершин с перемещением по целым числам показала, что это не всегда возможно, и если что-то двигать при трансформации позы, то рёбра целиком. Но и тут некоторые варианты после FoldAction и RotateAction оказывались несовместными. Стало понятно, что проблема с epsilon гораздо серьёзнее, чем мы думали.

Я тоже не мог пройти мимо и реализовал предварительное смещение всей позы целиком для уменьшения дробной части в координатах всех вершин (в среднем), чтобы хоть как-то помочь PosifyAction, который лечил каждую отдельно взятую вершину, но мог покалечить смежные.

К этому моменту какие-то проблемы у нас решались, отправленные решения принимались, но возникло отчётливое понимание, что нам нужна не эволюция, а революция и драйв. И тут понеслось...

У меня в очередной раз засвербило, наконец, попробовать формализовать задачу и попробовать какой-нибудь Solver. Я полистал tutorialы, набросал транслятор проблемы в систему уравнений в виде модели SMT 2, натравил Z3 Prover и о чудо! Solver выдал нам автоматически найденное решение проблемы #11:

$ time z3 011.smt
sat
(
  (define-fun v0y () Int
    0)
  (define-fun v1y () Int
    10)
  (define-fun v1x () Int
    10)
  (define-fun v2x () Int
    0)
  (define-fun v0x () Int
    10)
  (define-fun v2y () Int
    10)
  (define-fun h0y () Int
    0)
  (define-fun h0x () Int
    10)
  (define-fun h1y () Int
    10)
  (define-fun h2x () Int
    0)
  (define-fun h1x () Int
    10)
  (define-fun h2y () Int
    10)
)

real  0m0.666s
user  0m0.628s
sys  0m0.000s

Проблема #11 выглядит одной из самых простых и была выбрана для простоты отладки генерации SMT, а существующие эвристические стратегии с ней пока не справлялись:

Problem #11

Так у нас вечером предпоследнего дня появилась ещё одна SolverStrategy, которая запускала Z3 внешним процессом и, если решения не было через минуту, убивала его. Какое-то время было потрачено на попытки втащить Java-биндинги к Z3, но они все увенчались провалом: то артефакты без POM, то недостающие зависимости, то ещё что-то. Ещё какое-то время ушло на эксперименты с Google OR-Tools, но проект до сих пор не Maven-изирован, кроме того, по результатам беглого просмотра документации и примеров не было очевидно, что удастся выразить и решить систему квадратичных уравнений. Но это не точно.

Всё это не было бы возможно без помощи Олега, который параллельно реализовал нарезание дыры на треугольники, что было необходимо для формирования ограничений на расположение вершин в виде наборах SMT assertов, а затем реализовал автоматическое извлечение запрещённых треугольников из выпуклой оболочки дыры -- исходные данные для ещё одного набора ограничений на расположение рёбер позы.

В итоге SolverStrategy удалось решить несколько (всего, но хоть что-то) задач, с которыми не справлялась KutuzoffStrategy (которая работала на AutoFoldAction).

Тем временем Антон упоролся по полной...

Он подхватил брошенную идею с PushAction, разобрался, погрузился и втащил в наш проект сторонний физический движок, который позволил сделать именно то, о чём мы мечтали все эти три дня:

Physics

Можно хватать и тащить за любые вершины и граф динамически перестраивается с сохранением инвариантов. С ходу Антон успешно заслал ручные решения для нескольких тяжёлых проблем, которые были не по зубам ни одной из существующих стратегий, но до автоматического применения эту модель мы, к сожалению, довести уже не успели.

Впрочем, на задачах с маленьким epsilon (строгим ограничением на длину рёбер) возникали определённые проблемы: приходилось многократно теребить вершины, чтобы получить валидное решение.

Day 3

К концу контеста кода (не тестов) становилось всё больше, а с ростом объёма кода увеличивалось и количество багов. Антон заметил, что некоторые валидные решения мы считали невалидными и наоборот валидные на наш взгляд решения не принимались организаторами. Олег ловким движением перевёл валидацию решения на проверку ограничений на треугольники дыры по аналогии с SolverStrategy -- наступила тотальная консистентность.

Оставшиеся часы до окончания контеста мы провели в оптимизациях и прогоне различных стратегий на всех имеющихся вычислительных ресурсах, чтобы окончательно обсчитать проблемы со всеми фиксами и отправить успешные решения.

В последний час я внезапно вспомнил, что наша SolverStrategy не принимает во внимание epsilon, т.е. ищет координаты вершин позы, которые сохраняют длины рёбер строго неизменными, хотя в большинстве проблем допустимо растяжение/сжатие в определённых пределах. И это ведь сильно сужает пространство решений, верно?

Мы тоже так решили. Я наспех ослабил ограничения на длины рёбер в уравнениях SMT с точностью до epsilon и... Solver теперь за разумное время решает только примитивную проблему #11. Может быть, свобода это не всегда благо?

Итоги

Судя по Scoreboard, команда WinterMUTE вошла в ТОП100 (100-е место из 160). Скромный результат...

Но вся команда получила море фана, а лично я закрыл гештальт по применению SMT Solver к реальной задаче (и напряг мозги, вспоминая школьные основы геометрии).

Выводы

Большое спасибо организаторам! Всё работало как никогда идеально (на той стороне точно не роботы?!).

На мой личный взгляд, по сравнению с некоторыми контестами прошлых лет не хватало нетехнической (хотя бы небольшой художественной) части и/или какого-то discovery. С другой стороны, несмотря на лаконичную спецификацию, сами проблемы были оригинальными, разнообразными, а распределение очков команд на Scoreboard явно свидетельствует об удачном выборе задачи.

На этот раз у нас практически отсутствовало дублирование функциональности: либо размер команды был оптимальным, либо просто не хватало рук, чтобы ещё и велосипедировать, либо мы стали опытнее.

В этом году у нас произошло фиаско с модульными тестами. В первый день новые тесты ещё появлялись, а дальше их как будто только поддерживали. И я тоже. В итоге значительное время каждый день уходило на вылавливание багов всеми участниками.

На протяжении контеста озвучивалось множество идей: и генетические алгоритмы, и метод ветвей и границ, и тот же автоматический аналог PushAction на физической модели -- но даже на проработку откровенно не хватало рук. В пользу нехватки людей говорит и тот факт, что мы не добрались ни до оптимизации дизлайков, ни до бонусных фич.

Кому интересно, исходники нашего решения лежат здесь.

comments powered by Disqus
Copyright © 2013-2024 Vadim Tsesko (Вадим Цесько)