Any sufficiently complicated ICFP Contest submission contains an ad-hoc, informally specified, bug-ridden, slow implementation of half of a CSP-solver.
Отчёт о прошлогоднем ICFPC-2016 опять публикуется за несколько часов до начала следующего.
Видимо, такой формат у этого медиа. Ничего не поделаешь.
TLDR; Предчувствия не обманули.
Сказать, что задача была замечательной, — это не сказать вообще ничего.
Никаких лабиринтов и классических компьютерных игр, правда и никаких WAM-машин тоже.
Итак.
Что мы знаем о Стране Восходящего Солнца?
Самураи. Традиции. Сакура.
Ортодоксальная столярка.
Дроно-гейши, способные гнуть реальность через 4-ое измерение.
Древнейшее искусство Оригами...
Пятница
Прочитав задание я лично сразу понял, что дело пахнет керосином.
Во-первых, столько рациональной геометрии нам за три дня не осилить даже и в лучшие годы.
А во-вторых, чёрт его знает, чем все эти simple valley fold'ы отличаются друг от друга, почему некоторые из них impossible, и зачем нужны дроно-гейшы, работающие в четвёром измерении.
Задание на отрез отказывалось укладываться в голове.
Поняв, что ничего не понимаю, я решил заняться интеграцией: база данных для проблем и решений, взаимодействие с орговским сервером, сохранение лидерборда — вот это вот всё.
Базу для пущего развлечения развернул на Raspberry Pi Zero, для миграций использовал liquibase, скрипты на bash'е...
Ну и как-то оно постепенно завертелось.
Как водится, на интеграцию был убит весь день.
Правда в этот раз оно-таки выстрелило ближе к вечеру воскресенья.
Лёха разрушительной рефлексии не поддался и сразу же увлёкся визуализатором задач и решений на python'е, на что и ухлопал весь день.
Судя по git log'у проблем там тоже было немало.
Первый день для меня закончился беглым чтением каких-то статей и даже книг про математику оригами.
Количество теории в этой области превосходило всякие разумные рамки.
Аксиомы Huzita-Hatori, связь с системами полиномиальных уравнений, физически реализуемые и нереализуемые складки и их обобщения.
Постепенно у меня стала зреть мысль, что нужно идти другим путём...
Суббота
Постоянных читателей моего блога не удивит тот факт, что утром я проснулся с чётким пониманием того, как следует решать задачу, а именно: искать замощение единичного квадрата предложенными в силуэте полигонами, удовлетворяющее ограничениям на valid submission. С этого момента теория стала развиваться с бешеной скоростью.
Очевидно, что площадь всех отобранных полигонов с учётом их кратности должна суммироваться в единицу.
Внешний периметр, очевидно, должен суммироваться к 4, а периметр каждой из сторон — к 1.
Стороны с иррациональной длиной не могут участвовать в периметре.
Для замощения достаточно использовать только выпуклые полигоны — доказательство оставляю в качестве лёгкого упражнения для читателя, — что здорово упрощает геометрические изыскания, но имеет свои скрытые пока в мутной воде грабли.
Кроме того, должны выполняться требования спека к решению: отсутствие пересечений внутренностей полигонов на исходнике, пересечение ребёр только в вершинах, 5000 байт на кодирование решения итд.
Таким образом наклёвывался поиск в дереве (ok, в DAG'е), где узлом является частично заполненный полигонами единичный квадрат.
Корень дерева — квадрат вообще без полигонов.
Первый слой дерева — квадраты, в которых один из полигонов как-то уложен в угол.
Последующие слои — узлы, где к уже уложенным полигонам пристроены вплотную новые по всем правилам спецификации.
И дальше только борьба с симметриями, тупиковыми ветвями и мб поиск хороших эвристик.
Easy, right? Но мы пошли другим путём...
Поскольку недавно прочитана AIMA-book, в голове срабатывает pattern-matching на слово CSP.
Т.к. про CSP я знаю пока только теоретически, то обращаюсь за советом к Лёхе.
Тот вздыхает, смотрит на меня с экзистенциальной грустью в глазах и говорит: "Ну, возьми minizinc", — и отправляется ковыряться дальше со своим питоном.
Дело там, видимо, идёт не очень, т.к. в репозитории начинают появляться какие-то статьи, копирайты чужого кода и прочие полезные для решения задач вещи.
Впрочем, появляются и какие-то решения для отдельных проблем, очевидно, добытые врукопашную.
На minizinc я убиваю весь день.
В чём-то оно выглядит перспективно и иногда даже может мне сказать, сколько нужно и каких полигонов взять для решения задачи.
Но выразить все геометрические ограничения над полем рациональных чисел на языке уравнений практически нереально.
А при нехватке уравнений эта система имеет слишком много симметрий...
Воскресенье
В воскресенье становится ясно, что мы продолжаем пребывать у разбитого корыта. Солвера нет.
Закапываем minizinc, и я сажусь за C++ писать "точный" солвер, контуры которого более или менее понятны (pun is not intended).
Лёха занимается "неточным" солвером на питоне. С помощью какой-то оптимизации он подбирает четырёхугольник с рациональными сторонами, который покрывает заданный силуэт, а дальше ищет простую последовательность fold'ов, приводящую единичный квадрат к этому четырёхугольнику.
К шести вечера становится понятно, что точного солвера у нас не будет. Зато неточный выбирается из квасов и начинает активно дробить числа. Я переключаюсь из dev в ops и гоняю интеграцию.
Пайплайн работает как часы, ведётся строжайший учёт. Задача либо решается, либо отправляется к Лёхе в R&D отдел на исследование. Правила для valid submission на самом деле довольно тонкие, поэтому сбоев много. Но всё равно задачи решаются сотнями, пусть мы и рубим мало очков, применяя неточный солвер. Лёха периодически выкатывает новые версии солвера. Интеграция позволяет перерешать только проблемные кейсы. Паровоз летит вперёд.
К вечеру мы прорешиваем все задачи, кроме тех, которые вообще нельзя решить нашей технологией.
Промежуточные итоги
Компетишн, мы, конечно, зафейлили. Точного солвера не запилили.
Зато, как это ни смешно, заняли исторически самое высокое (72-ое) место за всю историю участия в ICFP Contest.
Прямо вау...
Естественно, всё дело в интеграции.
Учитывая наличие порядка 3k проблем, ручной их процессинг без какого-то строго учёта просто не скейлился.
На том и выехали.
Постфактум шансы для нашей команды разработать за трое суток точный солвер оцениваю как околонулевые из-за необходимости реализации большого количества всякой тонкой геометрии.
Хотя многим другим командам это удалось.
Возможно, они просто умеют готовить boost + gmp...
Послешоу
...Через пару дней после окончания контеста я вернулся к идее точного солвера и начал периодически что-то попиливать, благо орги лидерборд не отключали, а только перевели его в режим postmortem, где он стал чаще обновляться.
Почти сразу солвер научился решать задачку-пример из спецификации, а через несколько дней уже окреп до того, что осилил 17-ую Проблему (которая содержала какую-то нетривиальную складку).
[19:36, 8/13] AP: Не знаю, чего все так парятся с 17-ой задачей...
Пока я 3 часа гулял, мой солвер нашёл решение :-)
[19:37, 8/13] AP: Правда, я его еще не проверял формально, но на вид вполне ok
[22:17, 8/13] AS: Так долго искал решение для 17? Где 5 полигонов??
[22:18, 8/13] AS: Это прекрасно, что он его нашёл.
И это отличный результат для субботы.
Для той, что была неделю назад :)
[22:18, 8/13] AP: Ну, не 5, а 8.
Ну а чего ты хотел от неоптимизированного поиска в глубину?
[22:18, 8/13] AP: Зато решил!
[22:18, 8/13] AP: Да, суббота пропала не зря.
[22:19, 8/13] AS: Это да, это чудесно :). Точный солвер тоже есть в копилке :)
[22:21, 8/13] AP: Это ведь на самом деле поразительный результат.
Три часа ты ждёшь неизвестно чего
(и даже не знаешь, сколько часов будешь еще ждать)
и вдруг получаешь ответ, который валидируется на бумажке
А 17-го числа та же 17-ая проблема уже решалась за несколько миллисекунд в интерпретаторе...
Следующим этапом была 50-ая. После серии мелких фиксов она тоже стала решаться за миллисекунды.
Версия 1.4 солвера, выпущенная 19 августа, уже позволила войти в top-10 postmortem'а, несмотря на то, что в лидерборде до сих пор были какие-то активные участники. К этому моменту было точно решено 1423 из 3654 задач. Все низковисящие фрукты были сбиты, требовались новые идеи. Самой очевидной было реализовать поддержку дырок в силуэтах, но для начала я решил покопаться в имеющемся датасете и попробовать поклассифицировать задачи.
Само собой, сразу начались откровения. Разве вот это не прекрасно?
Человек мгновенно видит решение, а солвер дохнет на этапе составления списка выпуклых полигонов... И подобных задач нашёлся огромный пласт, что и стало драйвером дальнейших улучшений.
Следующей фичей солвера v1.5 стала поддержка дыр в силуэтах, что позволило немедленно подняться до top-7.
А ко 2-му сентября тот же солвер дотянулся до top-5 при 2110 решённых задачах из 3764.
Кстати, всё это запускалось урывками на обыкновенном яблочном лэптопе.
8-го сентября я пильнул точный выпуклый солвер, что оказалось весьма непросто.
Некоторые заботливые граждане так тщательно, знаете ли, подбирали угол поворота силуэта, чтобы его было очень сложно вернуть обратно в единичный квадрат.
Особо отметим авторов 5391, 6214, 3272 и 78.
Но и это затруднение было преодолено в итоге.
Жаль, что недорешённых выпуклых задач было совсем чуть.
9-го случилось очередное озарение (прошло предыдущее помутнение...) и солвер стал перебирать намного меньше эквивалентных поддеревьев.
Кратковременно был взят top-4, но малину испортили Дикие Башкортостанские Маги со своим солвером OXYETHYLENE, которые спихнули меня обратно на 5-ую позицию.
19-го я выпустил версию 1.11 с кучей новых отсечений плюс некоторые апгрейды к интеграции, которые позволяли не решать эквивалентные задачи.
А также я заглянул, наконец, в профайлер, отчего десятикратно увеличилась скорость перебора.
На этом, к сожалению, всё и закончилось, т.к. после объявления результатов орги отключили лидерборд.
Моя система позволяла работать и без сервера, но это было как-то скучно.
Поразительно, но даже в этой версии всё еще оставался баг из-за которого иногда неправильно вычислялась точка пересечения двух отрезков...
В качестве финального аккорда я еще упоролся и проанализировал группу симметрий каждой из проблем и добавил-таки поддержку вращательных симметрий в солвер (+45 решённых задач).
А в итоге осталось 975 нерешённых задач из 3764 и что с ними делать стало совершенно непонятно.
Единственный вариант — это повторить весь экзерцис но только уже с невыпуклыми полигонами, как в солвере unagi.
Но на этом мой энтузиазм оказался исчерпан.
Окончательные итоги
Задача у оргов получилась просто на зависть.
Красивая, геометрическая, многоплановая, с кучей возможных подходов.
Кто-то использовал увлекающуюся оригами жену как чит-код. Кто-то придумывал задачки.
Невероятный Алексей jabber.ru в жесточайшей борьбе c unagi взял лайтнинг фактически врукопашную.
Сами unagi реализовали примерно то же самое, что описано в этом посте, только для невыпуклых полигонов и уложившись в 3 дня, а не в 3 месяца, и заняли первое место с колоссальным отрывом.
TBD опубликовали проблему, которую никто не смог решить, за что и удостоились судейского приза.
Много всяких интересных отчётов можно найти на reddite'е.
Ну, а ваш покорный слуга так и не согнул ни одного листа бумаги. Никаких частных случаев.
Сезон 2017
Судя по всему, в этот раз мы хлебнём каких-то азартных игр в lambda casino, где некий lambda punter будет зарабатывать какие-то lambda point'ы.
А может быть, всё будет совсем не так, и будем мы управлять какой-то лямбда-плоскодонкой в бурлящей реке жидкого гелия...
В любом случае, без лямбд не обойдётся на этот раз. Жутко интересно.
Опять я целый год протупил с отчётом об ICFPC-2015.
Время однако поджимает, ибо уже через несколько часов начнётся очередная серия этой нескончаемой саги.
Правда подстёрлись эмоции и трудно расшифровать свои заметки, поэтому графоманства и фрустрации наверное будет меньше, чем обычно. А может быть и нет...
Начать нужно с того, что в этом (ok, в 2015-ом) году наша команда усилилась и стала интернациональной.
К нам присоединился довольно-таки известный в узких кругах окамлист Fred. (Sorry, Fred, use google translate or something to read this...)
Какая нелёгкая занесла его в Москву, я не помню, но всё срослось удачно, и Fred все три дня активно упарывался вместе с нами и в итоге сделал львиную долю работы.
И если бы не моя тупость, то это даже могло сказаться на нашем результате. Но не будем забегать вперёд.
Проблема
Надо признать, что парни из Galois неплохо отжигали хинтами.
Тут тебе и Ктулху, и роботы, и диарсен(?) и какое-то непонятное
и при чём здесь казалось бы арбузы? Ой, а еще вычислительная археология, национальная безопасность, сельское хозяйство, гольф, криптография, языки программирования, теория сложности и чумовой логотип 1600x794...
Всё это выглядело очень многообещающе и спровоцировало много обсуждений и волны переписки.
А в итоге в качестве проблемы было предложено написать банальный AI для гексагонального тетриса.
Вместо лямбд, виртуальных машин и вот этого всего мы получили простую как доска задачу дискретной оптимизации.
Т.ч. сделанные в предыдущем посте предсказания отчасти сбылись.
В общем, проблема выглядела удивительно не по-icfpc'шному.
Кстати, гексагональный тетрис на поверку оказался и не тетрисом вообще, т.к. фишка была не столько в укладывании unit'ов, сколько в правильной траектории каждого юнита.
Ну, хорошо, всё подробно изложено на официальной странице, а я очень кратенько.
Дан "прямоугольный" стакан с гексагональной сеткой (может быть частично заполненный). И дан конечный список unit'ов — фигурок в том порядке, в котором они будут появляться.
Фигурки могут состоять из одной или нескольких клеточек (cells) и вращаться вокруг центра вращения (pivot point).
Центр вращения не обязательно лежит "внутри" фигурки, что позволяет им проходить сквозь сплошную среду.
Очередная фигурка появляется вверху по центру стакана и двигается под воздействием команд: влево, вправо, влево-вниз, вправо-вниз, поворот по и против часовой (на pi/3).
Если очередная команда неприменима, то фигурка застывает в текущем положении (lock) и дальнейшая последовательность команд применяется к следующей фигурке.
По правилам игры фигурка не имеет права возвращаться в состояние, в котором уже была. Поэтому последовательности команд типа "влево-вправо" или "6 поворотов по часовой" всегда приводят к застыванию фигурки.
("The Old Ones do not take kindly to stuttering computations!" )
Как и положено в тетрисе, после того, как ряд стакана полностью заполнен, он исчезает и верхние ряды смещаются вниз.
В гексагональной сетке это приводит к достаточно специфическим эффектам.
So far, so good.
А теперь самая забавная часть. Каждая команда для фигурки может быть закодирована одним из множества символов.
Например, команда "влево" может быть представлена любым из символов {p, ', !, ., 0, 3}.
Таким образом в последовательность команд можно было вплетать т.н. фразы силы (power phrases).
И вот за них-то и давали больше всего очков.
Было известно, что всего фраз силы существует 18 штук и приводилась самая короткая из них: "Ei!".
Остальные фразы предлагалось открывать самостоятельно.
Пятница
Лично я в пятницу общался с риэлторами - удивительная порода людей, конечно, - и прискакал в поту и в мыле в офис где-то за час до публикации задания.
Только-только успел охладиться под кондиционером и попить чайку. Мозги были тотально выедены.
Фред в четверг бухал с какими-то русскими в бане и выглядел тоже не лучшим образом.
Лёха тоже на что-то жаловался: то ли на работе его доставали, то ли дома, то ли что-то еще. По-моему, работать заставляли, изверги.
В общем, команда наша подошла к контесту в классическом своём состоянии тотального раздолбайства.
Прочитав задание, мы созвонились, обсудили его и каждый взялся за своё.
Лёха, естественно, принялся хакать сервер оргов и строить питоновскую обвязку.
Fred героически взял на себя разработку интерпретатора игры на окамле.
А я некоторое время потупил, понял, что толку от меня мало и принялся изучать творчество Лавкрафта на предмет поиска фраз силы.
Неожиданно выяснилось, что Fred в теме. Он не только принёс нам первую фразу силу (вынесенную в эпиграф данного поста), но и подсказал мне какие-то вещи про этот волшебный R'lyehian язык.
Более того, вооружившись grep'ом, make'ом, полным собранием сочинений Лавкрафта и английским словарём он запилил первую версию NLP фреймворка, с помощью которого я в течение остатка вечера охотился на фразы силы. Всех обнаруженных подозреваемых я отправлял Лёхе в "уютную пытшную", где он их верифицировал через прогон на серваке организаторов. В итоге, там что-то верифицировалось не так, потому что единственная найденная за вечер фраза была "R'lyeh", хотя впоследствии выяснилось, что нашёл я их немало.
Разочарованный таким низким КПД я полез в википедию и поизучал до кучи пантеон Лавкрафтовских богов.
К счастью, организаторы вовремя опубликовали в твиттере следущее: "We are enjoying watching contestants search for power phrases, but the Deep Ones discourage cutting & pasting from Wikipedia."
А то могло случиться страшное.
Еще одна полезная вещь, которую я сделал тем вечером, - это наваял и запустил скрипт, который должен был скачивать leaderboard каждую минуту.
Правда, как выяснилось через три дня, скачивал он совсем не то, что нужно. :-)
Суббота
В субботу я проснулся с готовым решением проблемы в голове, о чём не замедлил сообщить при встрече парням.
Неожиданно, оба согласились, что план мой не лишён смысла...
Идея состояла в том, что общая задача дискретной оптимизации неплохо декомпозировалась на две ортогональные подзадачи: оптимальное укладывание отдельной фигурки в стакане и поиск максимально длинной (дорогостоящей) последовательности "терминалов". Терминалами или терминальными положениями мы называли финальное положение фигурки, в котором она в итоге застывала в стакане.
Фразы силы предполагалось вплетать независимо в траекторию каждой отдельной фигурки. Как в точности это делать было не совсем понятно, хотя и ясно, что это будет какой-то поиск в дереве возможных ходов, в котором множество "элементарных" ходов будет расширено фразами силы. Еще было непонятно, где, собственно, брать эти самые фразы силы, поэтому решено было этот вопрос отложить в долгий ящик, т.е. где-то до понедельника.
Является ли положение фигурки в стакане возможным терминалом определяется двумя свойствами: наличием легальной траектории от начального положения до искомого и наличием нелегального хода в искомом положении. Поэтому проблему поиска множества всех терминалов предлагалось решать при помощи нехитрого динпрожика, который бы дал множество всех достижимых положений, и фильтра по числу доступных из данного положения легальных ходов.
Если представить себе множество терминалов, как множество возможных ходов из данного узла дерева, то высокоуровневая задача оптимизации неожиданно превращается в задачу поиска самого ценного пути от корня до листа в дереве. Истинную ценность пути, правда, определить нелегко, а с учётом наличия в задании ограничения на объём памяти и время самым разумным вариантом казался алгоритм типа beam search с высотой "центра масс" в качестве эвристики.
В общем, не протупив и трёх часов с момента общего сбора я приступил выполнению первой задачи: построения множества терминалов для данной фигурки и стакана. Естественно, на хаскеле.
У меня, правда, еще не было способа строить все возможные ходы для фигурки из данного положения, т.к. Fred продолжал бороться с вращениями.
В целом у него всё нормально работало, но иногда он приходил ко мне и произносил текст, начинающийся с фразы: "Ok, Sasha...", что означало, что он нашёл еще один какой-нибудь забавный косяк.
Косяков было много. Во-первых, одна из команд сумела-таки расшевелить The Old Ones тем, что обнаружила возможность сделать бесконечный цикл... Потом была куча разъяснений и дополнений к правилам. В итоге орги даже выложили кино правильной обработки ходов для некоторых проблем.
Но лично я был спокоен как мамонт. Ясно было, что Fred в итоге добьёт интерпретатор и я таки заимею правильный "внутренний граф" для проблемы динамического программирования. А пока сойдёт и кривенький. Поэтому можно спокойно двигаться вперёд по заранее намеченному плану, не обращая внимания ни на какие внешние раздражители. Даже на весёлое рубилово, происходившее по всем фронтам: в leaderboard'е, официальном irc и неофициальном русскоязычном jabber'е. Похоже, везде успевала отжигать команда "Диких Башкортостанских Магов". Запомните это имя. Оно еще встретится. Дело дошло до того, что самим Древним пришлось вмешаться и орги попросили прекратить вакханалию и поубивать клоны команды "Hack the loop" :-)
Лёха тем временем конкретно упоролся питоновской обвязкой и полностью захватил власть над орговским сервером.
Fred'у тоже нужно было сабмиттить какие-то решения для отладки, а Лёха уже пользовался Fred'овским интерпретатором для визуализации и скоринга решений.
В общем, пока я витал в своём динпрожьем астрале, эта парочка неплохо спелась.
Кстати, я к тому моменту ни разу и не запускал Fred'овский интерпретатор, т.ч. даже не посмотрел, какие квалификационные проблемы предложены оргами.
Т.е. решал поставленную задачу в своей обычной манере: полностью абстрактно, игнорируя любую конкретику. Частные случаи нас не интересуют, знаете ли.
В общем-то на разработку динпрожика, доставание из него множества терминалов и кратчайшего пути до каждого терминала, на простенькую запускалочку, на парсинг входных и генерацию выходных форматов весь день у меня и ушёл. Зато последний коммит был "WOW!" и разъяснялось, что весь этот колхоз умеет генерировать решение проблемы на глубину единственной фигурки. Один слой beam search, если угодно.
Это было очень близко к полностью рабочему решению. А ведь еще была только середина контеста. Очень непохоже на нашу команду. Правда на лайтнинг мы опять не успели.
Лёха тоже воодушевился моими успехами и под шумок закоммитил нечто под названием cppsolver. Правда на тот момент оно только и умело, что парсить входной json.
Воскресенье
В воскресенье я со свежими силами вонзился в хаскельный солвер.
Для начала прорешал все 25 квалификационных проблем на глубину 1 юнита. Если вы думаете, что это заняло минут 15, то очень ошибаетесь.
Это заняло 4 часа, если предположить, что мы встретились в 9 утра. Правда по дороге я что-то пофиксил в солвере а заодно подготовил три полудохлых хетцнеровских сервачка к ночному дежурству.
В ночь на понедельник им по моему замыслу предстояло считать...
Дальнейшие действия были совершенно понятны. Нужно было развивать то, что мы называли Higher Level AI, а именно: переходить от одноюнитовой решалки к многослойной.
Т.ч. я принялся колхозить какой-то beam search.
Опять же пришлось наплевать на всякую конкретику: отсутствие поддержки вращений, баги в inner graph, отсутствие функции вычисления высоты центра масс стакана, отсутствие функции определения следующей фигурки итд итп.
Ну, нам не привыкать работать в условиях неопределённости.
Ничего страшного, что программу нельзя запустить, лишь бы компилировалась.
Fred конкретно разогнался к воскресенью и сыпал коммитами как из пулемёта. К полудню он разобрался с наиболее неприятными багами, воспроизвёл орговское кино и стал атаковать моё поделие, пытаясь интегрировать в него свои наработки. В итоге, к 16 часам мы неожиданно научились решать проблему на глубину двух юнитов. Чёрт его знает, откуда появилось это промежуточное решение и почему нельзя было сразу запилить нормальный поиск на произвольную глубину.
В итоге beam search запилил к 18 часам Fred, а я стал заниматься всякими формальностями, типа поддержки command-line интерфейса и сортировки проблем по ожидаемой сложности.
И к 19 часам мы имели полностью работающее решение, отвечающее требованиям к сабмишену и даже генерирующее какие-то решения. Правда без фраз силы и очень медленное.
В этот момент на сцену ворвался Лёха, который был подозрительно тих весь день. Оказалось, что он поизучал мой динпрожек на хаскеле, попытался переложить его на c++, не осилил, сварганил промежуточное решение на python, отладил и с него сделал кальку на c++. Всё бы хорошо, только оказалось, что это работает неправильно и генерит невалидные программы. А как отлаживать? Пришлось мне тут продемонстрировать Лёхе всю мощь Emacs'овских макросов... Ладно, это шутка.
На самом деле у меня тогда был уже полнейший цейтнот. Мне хотелось срочно доделать поддержку ограничений по памяти и cpu и успеть запустить 24 проблемы считаться на всю ночь.
И тут Лёха ехидно задал простой и незатейливый вопрос:
- А сколько времени у вас один динпрог решается?
Стали разбираться и выяснилось, что для референсной 14-ой проблемы один юнит решается что-то в районе 100 миллисекунд.
Тогда Лёха для справки сообщил, что а) 100 ms - это примерно вечность б) хаскель - унылая хрень в) моё решение с обновлением всего массива до фиксированной точки, когда там могут меняться лишь несколько ячеек на итерацию, - это "решение математика, но не программиста" г) его c++-ное решение тратит меньше миллисекунды на динпрог.
Поразмышляв несколько вечностей над вышесказанным, я понял, что с этим действительно надо что-то делать.
И тут удачно подвернулся Fred, у которого закончились свои идеи. В итоге он взял на себя все недобитые задачи и позволил мне сосредоточиться на профилировании и оптимизации.
А сделавший своё грязное дело Лёха вернулся к своему питону и плюсам и накоммитил в репозиторий каких-то загадочных кривых решений, которые нам здорово аукнулись в понедельник (справеливости ради, некоторые из них были лучшими, из того, что у нас было).
В 11-ом часу мы таки добили всё, что было нужно для ночного запуска.
Я адски устал, но всё-таки заставил себя аккуратно запустить 24 screen'а с солверами.
В метро мы еще пытались рассуждать о том, как нам быть с фразами силы.
Я был в таком коматозе, что напрочь забыл, что еще в субботу придумал, как их вплетать в готовую цепочку терминалов.
Вместо этого я предложил пробовать вплетать их... sed'ом в уже готовые решения.
Fred, который явно чувствовал себя свежее других, из вежливости соглашался со мной.
Но если задуматься, то может это было и не самое тупое решение, т.к. предполагалось, что у нас уже не будет времени перерешивать квалификационные проблемы, и нам придётся сабмиттить то, что насчитается ночью.
Понедельник
В понедельник первым делом обнаружились две проблемы.
Во-первых, один из хетцнеровских серваков перегрелся и выключился. Таким образом мы потеряли решения 8 проблем. Еще две проблемы сдохли по ограничению на память.
Во-вторвых, я не перенаправил вывод решений в файл и их пришлось доставать из screen'а вручную. Из 24 скринов вручную. А решения там о-о-о-очень длинные.
А screen не позволяет скопировать сразу весь свой буфер, приходилось экран за экраном аккуратно буковка к буковке... Fred раскопал, как сохранить весь буфер screen'а в файл, но по каким-то причинам это не сработало.
Короче, часа два мы занимались тем, что на разные лады спасали эти 14 выживших ночных решений. Я доставал их как мог из screen'а (еще и с лишними переносами строк или какой-то другой проблемой с форматом - не помню), а Лёха с Fred'ом их раскладывали по каким-то файлам, чистили, прогоняли на интерпретаторе, скорили и пытались в них вокнуть известные фразы силы. Короче, тупняк удался на славу.
Особенно, если учесть, что это был рабочий день и мы были в разных офисах.
Fred параллельно с этой с этой деятельностью еще успел оптимизировать динпрог, используя свойства симметричных фигурок. Цифр не знаю, но можно предположить, что динпрог ускорился пропорционально количеству симметрий фигурки. Т.е. для одноячеистой - в 6 раз.
Дальше настал мой черёд и я прооптимизировал своё "математическое" решение, сделав его примерно вдвое более "программистским".
Далее была еще череда мелких улучшений и внезапно то, что считалось всю ночь, стало можно посчитать за полчаса. Что и было сделано для 8 проблем-погорельцев и двух неудачников по памяти.
За час до окончания контеста солвер был дополнительно распараллелен, а также был улучшен time и memory management.
Fred даже приколхозил какую-то поддержку фраз силы. Правда я почему-то уже решил себя, что "это сложно и мы сейчас делать не будем" и даже не думал об этой проблеме.
Хотя очевидное решение лежало на поверхности, было известно с субботы и потребовало всего полчаса на реализацию после контеста... Epic Fail.
Еще один фейл поменьше случился при подготовке финального сабмишена, когда за 15 минут до дедлайна, Лёха с Fred'ом что-то не поделили в репозитории, ситуация как-то резко вышла из под контроля, и мы в итоге на последних секундах засабмитили какой-то адский трэш: хорошие решения вперемешку со всяким случайным шлаком из репозитория.
Итоги
А в итоге мы заняли почётное 117-ое место, причём почему-то без единой фразы силы.
На самом деле, я заморочился пересчитать наш "очищенный" от трэшака рейтинг и выяснил, что мы бы заняли 95-ое место, если бы не зафакапили сабмишн. Т.ч. невелика беда.
А вот отсутствие фреймворка для фраз сил, который пилился на самом деле за полчаса, - это Настоящая Печаль. Потому что, емнип, он выводил бы нас в top-25. Правда при условии знания всех фраз силы.
В общем, конечно, в Final Leaderboard мы бы не попали, но всё равно обидно.
Что касается процесса, то всё было сравнительно неплохо. И Fred нас реально усилил. Что там говорить, благодаря ему, наша команда прыгнула выше собственной головы, и впервые у нас был нормальный Графический Визуализатор! С координатной сеткой, зумом, статистикой, скорингом и отображением следующих фигурок.
Fred шутил, что может теперь продавать эту игру.
Если бы мой скрипт для фотографирования leaderboard'а сработал, то сейчас можно было бы проверить, действительно ли в начале контеста мы поднимались до 5-го места благодаря быстро запиленному интерпретатору и Лёхе, который прорешал кучу задач врукопашную. Кстати, интересной особенностью задания была возможность такого человеко-машинного взаимодействия для решения задач квалификационного раунда.
Я же в течение контеста ухитрился даже не посмотреть, что там за решения мы нагенерили. Это было сделало уже когда пыль улеглась. И сразу выяснилось, тетрис как бы не совсем тетрис. Большинство задач наша тривиальная эвристика с центром масс решала просто до конца, укладывая все фигурки. При этом многие стаканы были такими большими (и пустыми), что даже идеальное укладывание всех фигурок не давало возможность заполнить и убрать много рядов. На таких картах фишка была именно во фразах силы.
Еще было два типа карт, которые наша эвристика могла не прорешать до конца. Во-первых, это сложные карты, где требовалась точная укладка и заглядывание вперёд. Во-вторых, это карты, на которых были какие-то воздушные конструкции в центре, игравшие роль сита: часть фигурок просачивалась вниз, а часть - не могла. Я пытался как-то дополнить эвристику выбора терминала соображениями по "плотности упаковки", но толком ничего не получилось. Ну, что сказать. Как известно, Ктулхи плохо композируются (см. problem 13).
Еще хочу сказать за динпрог. После всех улучшений оказалось, что наш солвер на 14-ой проблеме тратит не более 9 ms на решение одного стакана. А если верить профайлеру, то и не более 4 ms. Т.е. всё еще в 4 раза хуже, чем c++, но в 25 раз лучше первой реализации. Тут сказались не только оптимизации в самом динпроге, но оптимизации, связанные с симметриями, с инкрементальным вычислением центра масс стакана итп. Как выяснилось, там было, чему тормозить и без всякого динпрога.
Кстати, пакет vector оказался совсем неплох. Мне не удалось переписать программу на какие-нибудь мутабельные массивы так, чтобы заработало быстрее.
Вообще, динпрог изначально пилился с дальним прицелом на GPU. Задача как будто очень подходящая для этого дела. Но, то ли я совсем не умею готовить accelerate, то ли древний gtx 8800 уже совсем не может пару чисел сложить, но динпрог на GPU работает крайне медленно. Можно было попробовать на маке, но их греть стрёмно - уж больно нежные ноуты. GPU просто отпаивается и сгорает. Проверено.
Если бы accelerate нормально завёлся, то можно было бы попробовать еще одну интересную оптимизацию: решать весь пучок задач параллельно. Никто, в общем-то не запрещает в один массив запихать несколько стаканов и в каждом из них гнать свой независимый динпрог. Для GPU - самое то.
А для CPU был неплохой вариант не пересчитывать все динпроги в пучке с нуля, а воспользоваться тем, что на каждом слое в каждом стакане падает одна и та же фигурка. Стаканы же в пучке, как правило, начинают различаться только ближе ко дну. Соотвественно, пересчитывать все верхние ряды стаканы каждый раз смысла нет. Аналогичная оптимизация возможна, если та же самая фигурка выпадает позже в этом же стакане. Оба варианта остались нереализованными.
До кучи я попробовал inline-c. Это, опять же, работало слишком медленно. Видимо, маршаллинг между хаскелем и c слишком накладен.
Можно было вообще отказаться от динпрога и подумать о каком-нибудь эвристическом алгоритме. Но мне кажется, что мы в производительность построения множества терминалов на самом деле не упирались. Гораздо важнее было улучшить эвристику отбора терминалов для beam search и запилить фреймворк для вплетения фраз силы.
По завершении контеста я его и запилил. Просто жадный поиск по дереву вариантов ходов из текущей позиции с эвристикой "максимально ценного хода". Ходом считается как "элементарный" ход (0 очков), так и подходящая "фраза силы". Очень дешёвая и сердитая штука получилась.
Потом, воодушевлённый отчётом "Диких Башкортостанских Магов", решил попробовать сделать что-то более содержательное для вплетания фраз силы. В итоге родился нечеловечески сложный алгоритм под названием ultimate, который я сейчас уже совершенно не понимаю. Нет, по сути это, опять же некий динпрог, но для сокращения фазового пространства там возникают какие-то метасостояния, свёрнутые измерения и квантовое туннелирование. В общем, работает немножко медленно... На этом мой пыл и интерес к этой задаче окончательно иссяк.
Орги тоже подвели итоги, признались, что задача была "планом Б", т.к. с "планом А" они переборщили, а также опубликовали дичайший отжиг от все тех же WBM:
Оргам респект за то, что честно отыграли роли до конца, за leaderboard и за публикацию официального репозитория. Но задачка не для icfpc всё-таки, imho.
Посмотрим, что через 3 часа нам предложат японские товарищи.
Пока всё выглядит очень интересно. Мы имеем следующие хинты:
Машинная плавающая точка
Хило- и метаморфизмы
Совиный комбинатор
Элементарая Теория Чисел
Летающие Подушки
Покер
и "Hello, fold/unfold!"
Предчувствие такое, что проблема будет отличная :-)
Лямбдами же чё хочешь можно закодировать:
хоть ДНК для Endo, хоть управление для Hohmann Transfer,
хоть стратегию для робота в лабиринте… дело такое Народная мудрость
Dreaming of the Crash
Строго говоря, этот пост я начал писать 26 июня 2014 года. К тому времени уже были известны имена организаторов и мне хотелось сделать обзорчик их работ, а заодно и накидать черновик будущего отчёта...
С той поры прошёл уже год с лишним, в течение которого было несколько безуспешных подходов к этому снаряду. Наверное, пора уже дожать, пока меня не догнала сингулярность...
Об остальных оргах известно меньше, но, например, Martin `mariusz` Lester пишет о себе, что "was part of the team ... that won the ICFP Programming Contest in 2011"...
Чего ждать от всех этих оксфордских джентльменов в плане задания к контесту было совершенно непонятно. Оставалось надеяться, что с всё будет по крайней мере неплохо организовано.
Cornfield Chase
По мере того, как счётчик приближался к приобретшим вдруг "сакральный смысл" датам 25-28 июля, я стал поковыривать свой хаскельный сетап. Честно говоря, это каждый раз напоминает алхимию и поиски философского камня.
Помимо выкладывания фоточки (надеюсь, в будущем обойдётся без обязательного инстаграмма...) орги еще намекнули, что нам потребуется "много фруктов", а также опубликовали это:
% = \...o.....
Выглядело чертовски похоже на биндинг некоторого лямбда-выражения с пропусками вместо подтермов и переменных. Правда не совсем понятно было, что за "%" слева от "=". К чему 3072? И при чём тут фрукты?
Последние несколько дней перед стартом мы с Лёхой по-полной проникались атмосферой контеста, разгадывали хинты оргов, обсуждали современный c++, прошлогодние SMT-солверы, алгоритмическую разрешимость евклидовой геометрии и философские основания нашего участия в ICFPC.
Day One
В пятницу в четыре часа дня счётчик на странице контеста пересекает 0 снизу вверх и через несколько секунд там появляется Спецификация Проблемы. Сейчас она, как и всякие дополнительные материалы доступна в официальном репозитории.
Первым делом я её отправляю на принтер — незначительная деталь, которая непременно сыграет свою роль в дальнейшем повествовании, — и углубляюсь в чтение. Следующий час проходит за изучением 30-страничного документа и сумбурной перепиской по скайпу.
На первый взгляд задание подозрительно напоминает тот самый Lambda Mining 2012-го года, о котором с ностальгией пишет в своей работе г-н Wu. Снова нужно управлять какой-то хреновиной в двумерном лабиринте, чего-то собирать, от чего-то уворачиваться.
- AP> опять eating pills and evading ghosts?
Дальнейшее чтение показывает, что ностальгируют орги не только по 2012-ому, но и по 80-ым (полностью поддерживаю). Особенно по компьютерным играм (ой, да ладно?).
Что мы имеем? Злые призраки (":=") и гоняются по лабиринту за хорошим LambdaMan'ом ("λ"). Код призраков исполняется на более или менее классическом 8-битном "микроконтроллере" GHC (GHost Cpu) с минималистичным набором инструкций. 256 байт на код, 256 байт на данные, 1024 такта на принятие решения на каждом ходу, ввод/вывод через прерывания.
С LambdaMan'ом ситуация интереснее. Задание содержит подробную многостраничную спецификацию его "микропроцессора" GCC (General Computing Processor), построенного на 4 регистрах: S(tack), E(nvironment), C(control) и D(ump). Микропроцессор имеет частоту 3.072Mhz и исполняет одну инструкцию за такт. Программе доступно 10^6 CONS-ячеек памяти. Одна "минута" машинного времени на инициализацию, одна "секунда" — на ход. К счастью, орги дали не только референсную реализацию GCC, но и симулятор Игровой Механики на js.
К счастью, потому что сама игровая механика весьма нетривиальна. Понятие машинного такта, связанные с ним хитрые правила совершения ходов и набора очков, изменение скорости перемещения юнитов и море всяких прочих мелких технических деталей, включая "секретные параметры" и "неиспользуемые прерывания" (technical debt?). Даже возможность при определённых обстоятельствах разминуться с призраком в узком коридоре (Как в том любимом анекдоте Никулина: "...и не встретились. Не судьба!"). И совершенно неясно, сделано ли это всё оргами из чистой любви к искусству или имеет какой-нибудь практический смысл.
Правда с SECD-машиной я в последний раз сталкивался году этак в 2007-ом, когда только начинал изучать FP. А PacMan — это вообще из детства. Т.ч. толку от такого знания было мало.
Тем не менее вырисовывается план действий. Нам предстоит научиться программировать на ассемблере SECD-машины им. тов. Лэндина. Мы даже собираемся что-нибудь засабмитить в лайтнинг. А после этого, предстоит, очевидно, разработка компилятора.
План был хорош, но при попытке его воплощения в жизнь сразу полезли некоторые трудности. Во-первых, выяснилось, что референсная реализация не понимает ассемблер с метками и комментариями. Т.ч. нам требуется Макропроцессор. Во-вторых, Лёха наотрез отказывается параллелить задачи и доверить мне разработку Компилятора ("я тоже хочу повозиться с компилятором") или Стратегии (чем мотивировал — не помню). В итоге решили, что я запилю по-быстрому Макропроцессор, а там видно будет.
Макропроцессор я пилил аж 5 с лишним часов... Вместо того, чтобы сделать всё по-простому на awk, я сразу запилил под это дело целый проект на haskell'е. Идея была в том, чтобы выдавать нормальные сообщения об ошибках (строка, позиция) в исходнике. В конечном итоге это сработало, но поначалу я тупанул и вооружился attoparsec'ом. Только для того, чтобы через 2 часа, уже выписав грамматику со всеми комментариями и метками, выяснить, что из него нельзя достать текущую позицию токена. Пришлось всё срочно переписывать на parsec'е... Ну и была еще пара фейлов помельче.
В общем в 12-ом часу ночи новенький сияющий Макропроцессор был интегрирован в master-ветку репозитория. Жаль, что ошалевший к тому времени от отсутствия комментариев и меток Лёха не был способен оценить мою гордость. Впрочем, Макропроцессор этот выдержал test-of-time и был использован во всех наших решениях, как в течение контеста, так и по его окончании.
Пока я развлекался с Макропроцессором, Лёха "тихо ненавидел html и javascript". Он потихоньку экспериментировал с ассемблером SECD-машины и копался в потрохах референсных симуляторов (скомпилированных ghcjs, ага...)
Пятницу мы провели, очевидно, совершенно бездарно.
Stay
Суббота начинается с того, что Лёха долго выясняет, как проехать ко мне на работу и где правильно парковать машину, а потом не приезжает. Какой-то у него там форс-мажор. Меня это не слишком расстраивает, потому что план на день совершенно понятен. С лайтнингом мы были, очевидно, в пролёте, поэтому предстоит делать компилятор для SECD-машины. А где SECD-машина, там, естественно, Lisp. Не, ну была одна безумная идея с хаскелем... Впрочем, не будем забегать вперёд.
Можно было даже реализовать подмножество какого-нибудь стандартного лиспа, типа clojure или EmacsLisp (Лёха заморочился-таки с racket'ом). Это позволило бы отлаживать какие-то элементы Стратегии вообще не имея компилятора. Но я от этой идеи отказался, потому что распараллелить работы по созданию Компилятора и Стратегии мне было не с кем, а искусственно завязываться на определённый синтаксис не хотелось.
Message from Home
К 12 на связи появляется Лёха, который доехал-таки к себе на работу. Поначалу он продолжает заниматься ассемблерными разработками. С появлением макропроцессора дела у него идут получше и он всё чаще присылает мне какие-то адские простыни с комментариями в духе "смотри, какой читаемый код!" Вроде такой:
; Мне нужна одна локальная переменная t, поэтому создаю окружение из одной переменной
DUM 1
LDC 0
LDF init
RAP 1
STOP
init:
; Здесь мы получаем замыкание с локальными переменными в родительском стеке
DUM 2 ; x, y
LDC 1 ; x = 1
LDC 2 ; y = 2
LDF getsum
RAP 2
; В этом месте нам вернули в качестве параметра функцию sum z, у которой также захвачены переменные x и y
ST 0 0 ; t := sum 1 2
LDC 10
LD 0 0
AP 1 ; sum 10
RTN
; get_sum x y
getsum:
; В этой функции 2 локальных переменных: x,y
LD 0 0
LD 0 1
CONS
DBUG
; Теперь захватываем родительский контекст и возвращаем наружу адрес функции sum z
LDF sum
RTN
sum:
; Функция sum принимает 1 параметр z, извлекает из родительского стека x и y, возвращает x+y+z
LD 1 0
LD 1 1
LD 0 0
CONS
CONS
DBUG
LD 1 0
LD 1 1
LD 0 0
ADD
ADD
RTN
Совершенно очевидно... эээ... что здесь демонстрируется владение такими концепциями как замыкания (LDF), различные механизмы вызова функций (AP/RAP+DUM), мутабельные переменные (ST) итп.
The Wormhole
Меня это к тому времени не очень впечатляет, так как к половине второго я уже умею компилировать арифметические выражения.
Петля положительной обратной связи затягивается, я только успеваю добавлять новые фичи в lmc: определение (defun) и вызов (apply) функций, булевские переменные и операторы... Они, как правило, сразу работают. Но не все.
Mountains
Первым камнем преткновения стал... if. Мало того, что для правильной генерации меток, пришлось протащить через весь "чистый" (ну не переписывать же в самом деле из-за этого всё на монады?) код состояние — счётчик меток, — так еще и пришлось ввести понятие "блока" кода. Дело в том, что специальная форма (if b t f) моделируется, по сути, как
И если раньше compile возвращал один блок просто как список инструкций (с символьными метками) и такие списки просто конкатенировались в программу, то теперь стало нужно куда-то приткнуть список инструкций, начинающийся с метки t_xxx. Если бы я к тому моменту знал, что в списке инструкций есть jmp (замаскированный под TSEL), то можно было бы влепить этот блок перед compile(b) и перепрыгнуть его. Но я поленился внимательно прочитать про хвостово-рекурсивные расширения SECD-машины и мне пришлось изменить compile так, чтобы он мог возвращать два блока: основной и дополнительный. Дополнительные блоки лепились в конце программы (а точнее — в конце top-level выражения).
TLDR, некоторые баги в этом механизме смогли продержаться еще как минимум сутки :-)
Afraid of Time
Тем не менее, за 15 минут до окончания лайтнинга я "почти умею" считать элементы ряда Фибоначчи. Ну, или, точнее вот так:
(defun main () (apply fib 4))
(defun fib (n) (if (<= n 1) 1 (+ (apply fib (- n 1)) (apply fib (- n 2)))))
Остаток дня занимаюсь добавлением поддержки таплов (tuple/nth), списков (list/car/cdr) и всяких мелочей, вроде отладочной печати. Заодно читаю, наконец, про pascal extensions и закрываю для себя другие белые пятна Спека.
В метро по дороге домой до меня доходит, что на базе TSEL легко организовать jmp, которого так не хватало весь день.
А по приезду домой я еще замутил поддержку let-выражений — давно подозревал, что для этого будет достаточно defun/apply, — и прикрутил магический оператор rap для интерфейса процессор-сопроцессор. Это позволяло исполнять программы не только в симуляторе GCC, но и в симуляторе Игровой Механики, т.е. подступиться к созданию Стратегии.
A Place Among the Stars
К этому моменту основные черты языка Poor LambdaMan Lisp уже утряслись и хочется по ним быстренько пройтись. Должен сказать, что изобретение своего лиспа оказалось довольно увлекательным занятием. По крайней мере более увлекательным, чем последующее программирование на нём...
Во-первых, нужно было понять, каков будет порядок редукции. Я пошёл по пути наименьшего сопротивления и остановился на строгой семантике — аргументы вычисляются слева направо перед вызовом функции. Это хорошо ложилось на SECD-машину. Впрочем, ввиду отсутствия сайд-эффектов — а внедрять "pascal extensions" я не собирался, — это было не слишком важно.
Во-вторых, и тут свободы никакой не было, нужна была поддержка булевских и арифметических выражений, таплов и списков. Орги заботливо предусмотрели в спеке, чтобы все эти примитивы использовались в Игровой Механике. Как, кстати, и замыкания, что я долго обходил с помощью магического оператора (rap), не понимая толком, что он делает.
А дальше — полная свобода. Например, поддерживать или не поддерживать каррирование и частичное применение функций? Я согласился с предложением Лёхи "забить сразу", т.к. не придумал лучшей реализации, чем такая (на примере функции __eq из компилятора ghclm, см. ниже):
Ну, а дальше пошло-поехало. Вместо паттерн-матчинга — распаковка с помощью let и nth/car/cdr. Никаких лямбда-функций. Вообще никаких вложенных функций: только top-level, только хардкор. Соответственно, и замыкания не нужны. О системе типов я вообще молчу, потому что даже соответствие числа формальных и фактических аргументов при вызове функции не проверяется...
Надеюсь, происхождение названия языка теперь понятно. Ладно, вот пример.
т.к. контекст env приходится протаскивать через аккумулятор fold'а. Особенно это доставляет, если нужно добавить еще одно поле в AIState.
Running Out
Если хотите утром сразу включиться в работу, то надо с вечера себе оставить какую-нибудь маленькую приятную задачку.
У меня в воскресенье такой задачкой была реализация fold'а. Конечно, fold можно просто сделать функцией и дело с концом. Но т.к. lmc не поддерживает хвостовую рекурсию, то такая реализация мне не нравится. Вместо этого я решаю сделать fold специальной формой. Она заводит себе на стэке DUMMY-контекст для значения аккумулятора и далее использует pascal extension ST для его обновления и TSEL для реализации цикла. Дёшево и сердито.
I'm Going Home
После появления fold'а, я реализую Первую Тривиальную Стратегию LambdaMan'а, которая заставляет его двигаться строго курсом 0:
Практического смысла в этой стратегии, понятное дело, никакого нет. Зато есть очень важный символический смысл. Она есть доказательство того, что теперь можно писать код не только под симулятор GCC, но и в связке с Игровой Механикой.
Вторая Тривиальная Стратегия исполняет заданную программу команд:
Я привожу эту Стратегию целиком, потому что она стала основой для всех будущих построений. Особое внимание следует обратить на rmoves, в котором сохраняется информация, необходимая для возврата в исходную точку.
Coward
Идея отступления лежит в основе моей единственной эвристики по работе с призраками. Заключается она в том, чтобы при виде призрака в клетке, куда собирается наступить LambdaMan, развернуться и трусливо бежать (кроме тех случаев, когда ГГ обдолбался powerpile'ом, конечно).
Параметр rmoves в AIState как раз и является заготовкой под эту логику. Позже в нём будет сохраняться непосредственно список команд, т.ч. для режима паники будет достаточно поменять в нужный момент списки moves и rmoves местами. Et voilà!
Detach
На этом тривиальные конструкции закончились и нужно было строить более содержательную Стратегию. Однако строить было не из чего. Поэтому воскресенье я посвятил разработке Стандартной Библиотеки.
Естественно, начать пришлось со всяких примитивов: length, reverse, splitAt итп. В процессе полезли всякие грабли в компиляторе, которые приходилось тут же исправлять. К вечеру я добрался уже до таких абстракций, как двоичные деревья, которые заменяли мне массивы за неименением последних. Правда деревья были несбалансированными, а на практике так даже и всегда вырожденными в списки. Но я себе честно поставил TODO это исправить, если потребуется...
Наконец, в 9 вечера случился первый прорыв в области Стратегии. Для каждой точки карты я научился вычислять список всех возможных направлений движения из неё. Представлялось это "двумерным массивом" ([вырожденным] бинарным деревом [вырожденных] бинарных деревьев) списков. Теперь, зная пару координат (j,i) можно было получить список всех возможных направлений движения из данной точки карты (maze) с помощью:
(apply ij i j maze)
К 11 я уже умел находить на карте все "интересные" точки: пересечения, тупики и стартовую позицию LambdaMan'а. А к двум часа ночи для каждой пары смежных точек у меня была "программа перехода" между ними. Идея была в том, чтобы принимать решения только в узлах графа, вершинами которого являются "интересные" точки, а рёбрами — "программы перехода". В промежуточных точках, не являющихся интересными, нужно было просто исполнять программу, не забывая поглядывать под ноги, чтобы не наступить на призрака.
S.T.A.Y.
Следует, наверное, пару слов сказать о призраках. Хотя, если често, по причинам, которые станут полностью ясны позднее, мне про призраков сказать особо нечего. Все мои знания почёрпнуты из чтения спека и отчётов других команд.
Через систему прерываний призраки могут задавать своё новое направление движения и получать информацию об окружающей обстановке: содержимое ячеек карты, положение LambdaMan'а, положение второго LambdaMan'а (подразумевался multiplayer?), свой порядковый номер, стартовые и текущие координаты любого из призраков, их текущее состояние и направление движения.
Призраки имеют ряд ограничений. В частности, они могут менять направление движения только на перекрёстках, поворотах и в тупиках. При этом на 180 они могут разворачиваться только в тупиках. Некорректно выбранные направления движения игнорируются. Итп.
На этих фактах, например, основана приведённая в reference materials программа призрака fickle.ghc:
; Keep track of how long we have spent travelling in each direction.
; Try to go in the direction we've travelled in least.
; Count of time spent going in direction 0 is in memory address 0, and so on.
mov a,255 ; A is the min value.
mov b,0 ; B is the corresponding direction.
mov c,255 ; C is the candidate direction for the new min.
; Start of loop.
inc c ; Pick new direction.
jgt 7,[c],a ; Jump if count of direction C is above best so far.
; We have a new min.
mov a,[c] ; Save new min.
mov b,c ; Save direction.
jlt 3,c,3 ; Jump target. Loop back if we have not tried all 4 directions.
mov a,b ; Actually set desired direction.
int 0
int 3 ; Get our ghost index in A.
int 6 ; Get out current direction in B.
inc [b] ; Increment corresponding count.
hlt ; Stop.
По сути, здесь реализована "условно-рандомная" стратегия-бродилка, которая всё время пытается пойти по тому направлению, по которому призрак ходил реже всего. Понятно, что с такими призраками каши не сваришь.
Наиболее state-of-the-art призрачные решения, встречающиеся в отчётах команд, не только реализуют алгоритмы преследования (и уклонения от) LambdaMan'а разной степени нетривиальности, но и эффективно противодействуют тенденции "кластеризации" призраков в одном коридоре, что важно и для задачи преследования, и для задачи уклонения. Встречаются также попытки охраны powerpiles и "межпризрачного взаимодействия".
Некоторые решения стараются по-максимуму использовать выделенные 1024 такта на ход, намеренно генерят невалидные направления движения или вообще ошибки исполнения программы призраков. Связано это с тем, что недокументированный параметр программы LambdaMan'а, оказывается, представляет собой список закодированных программ призраков. Были даже команды (например THIRTEEN), которые реализовали эмулятор призрачного "микропроцессора" для SECD-машины. Однако, насколько мне известно, никто из этого ничего полезного не выжал.
Where We're Going
Утро понедельника начинается с Лёхиного телефонного звонка. Зевая рассказываю ему о своих успехах и планах. Лёха бодается с вычислением функции Беллмана. Ну-ну...
У меня уже ни с чем сил бодаться нет, но — чёрт возьми! — неужто столько работы пойдёт коту под хвост?
И я иду пилить Стратегию дальше. Для начала нужно хоть как-нибудь научиться обходить граф в отсутствие призраков. По построению графа это гарантировало бы сбор всех pile'ов.
First Step
В качестве простейшей реализации алгоритма обхода выбран следующий. С каждым маршрутом ассоциируется число — количество раз, которое этот маршрут был выбран LambdaMan'ом в качестве текущей программы. При попадании в один из узлов графа LambdaMan выбирает тот маршрут, по которому ходил реже всего. Т.к. граф маршрутов у меня ориентированный, то это приводит к тому, что LambdaMan зачастую проходит некоторый коридор сначала в одну сторону, а потом сразу же в обратную. "Эффективность? Не, не слышали!..". Тем не менее, такой алгоритм набирает 1040 очков на World Classics и удостаивается комментария "WOW!!!" в git'е.
Flying Drone
Таким образом за 3.5 часа до окончания контеста свет в конце тоннеля забрезжил и у меня появилась, наконец, первая содержательная Стратегия. Первый работающий девайс, способный, если ему сильно не мешать, обойти всю карту и собрать все pile'ы и powerpile'ы.
Наблюдать за его тупейшим поведением очень забавно. Например, как он пощёлкивая клювом проходит мимо коридора с фруктом и ничтоже сумняшеся поворачивает в коридор навстречу призраку...
Atmospheric Entry
К этому моменту Компилятор и Стандартная Библиотека практически не путаются под ногами. Баги повыпилены, структуры данных — позапилены. Конечно, Poor LambdaMan Lisp по-прежнему доставляет, но тут уже ничего поделать нельзя.
Времени до окончания контеста остаётся мало и понятно, что никаких принципиально новых решений не появится. Но тем не менее я уже набрал приличный момент в разработке Стратегии. Хочется потратить оставшееся время эффективно и выжать максимум из существующего решения.
No Need to Come Back
Следующим изменением становится добавление счётчика посещений не только маршрутам, но и узлам.
Теперь LambdaMan сортирует маршруты сначала по весу узла, а потом — по весу маршрута. Эта простенькая модификация была отлажена за какой-то час и давала 2170 очков на World Classics. Недурно.
Imperfect Lock
Далее нужно научиться что-то делать с призраками. Идея у меня была готова еще в воскресенье и за час до окончания контеста я успеваю её воплотить. Ну, вы знаете уже: режим паники, программа отступления, — вот это вот всё. Это даёт примерно 50%-ные шансы спастись при встрече с призраком на узкой дорожке.
Этого, конечно, совершенно недостаточно для настоящих Ghost Busters, но на World Classics сей нехитрый приём даёт 8700 очков, что близко ко вчерашнему максимуму лидеров на этой карте. Круто...
Кстати, уже после окончания контеста я еще улучшил это решение, заменив сортировку рёбер по числу посещений на сортировку по общему количеству оставшихся ништяков в коридоре. На World Classics эта дало 10200 очков.
No Time for Caution
Почему я вдруг говорю о вчерашнем максимуме?
Тут нас ждёт неожиданная развязка сюжета с распечаткой задания. Дело в том, что весь понедельник у меня не было интернета (пользуясь случаем передаю привет провайдеру). Поэтому получив 8700 очков на World Classics практически за час до окончания контеста, я расслабился и стал неторопясь готовить submission... по распечатанному пятничному рецепту, т.е. по правилам lightning round'а...
Я уже готов был диктовать sha1-сумму своего решения Лёхе по телефону, чтобы он засабмитил за меня хотя бы хэш (чему тот был бы явно не рад, т.к. в этот момент в панике пытался тоже что-нибудь засабмитить), но тут случилось чудо — интернет дали. В итоге я спокойно и без нервотрёпки залил своё решение и поехал на работу.
Где с удивлением узнал, что в финальном раунде нужно было сабмиттить не только стратегию LambdaMan'а, но и призраков. Понятное дело, что в моём решении никакими призраками и не пахло, не было даже стандартного fickle.ghc. Однако решение не забанили на этом основании. Видимо, запускали конкурентов без кода моих призраков вообще (что эквивалентно тупейшим призракам, долбящим строго вниз). Результат понятен.
Забавно при этом, что Лёха не успел выложить своё решение до дедлайна, но успел выложить хэш. В итоге орги связались с ним и приняли его решение.
What Happens Now?
Настало время рассказать об еще одной замечательной идее, которая нашла своё воплощение лишь после завершения контеста. Идея состояла в том, чтобы делать не компилятор Lisp'а, а компилятор Haskell'а... Да, ровно так: компилятор подмножества языка хаскелл для SECD-машины.
На первый взгляд такая задача может показаться гораздо более сложной, чем исходная, но чем больше я о ней думал, тем больше понимал, что попробовать стоит.
Согласно AOS и GHC Wiki есть как минимум три "точки расширения" в GHC, пригодных для нашей цели. Во-первых, это API, позволяющий использовать GHC как библиотеку. Во-вторых, возможность реализовать свой кодогенератор для компиляции из Cmm. В-третьих, возможность реализовать свой Core-to-Core Pass плагин.
Меня больше всего заинтересовал последний вариант, т.к. из всех представлений хаскельной программы именно GHC Core проще всего транслировать в код SECD-машины. Опять же, плагин для Core-to-Core преобразования элементарно подключается к GHC ключом командной строки.
Так появился на свет проект ghclm. Плагин к GHC, реализующий тождественное Core-to-Core преобразование с небольшим сайд-эффектом в виде .gcc-файла.
Не могу сказать, что познал все тонкости System FС / GHC Core, но кучу базовых тестов по работе с числами, таплами, списками, рекурсией итп плагин честно проходит в связке с официальным GCC-симулятором, запущенным под node.js. Также, в качестве proof-of-concept я замутил рандомную стратегию-бродилку, которая компилируется и исполняется в официальной Игровой Механике. 27 часов на всё про всё, включая тесты. Совсем неплохо.
Конечно, ghclm поддерживает только тот набор типов данных, которые присутствовали в спецификации задачи: числа, 2-таплы, списки. Никаких тебе алгебраических типов данных, массивов, даже строк. Такой себе Poor LambdaMan's Haskell.
Также имеются шероховатости и в самой процедуре трансляции.
Во-первых, как и в компиляторе lmc, не поддерживается хвостовая рекурсия и другие pascal extensions. На практике не такая уж большая проблема, но можно было бы генерить несколько более эффективный код.
Во-вторых, нет поддержки дебажного вывода (DBUG). Вот это действительно неудобно.
В-третьих, есть несколько моментов, связанных со спецификой самого GHC Core. Например, для форсирования thunk'а в этом языке используется конструкция
case thunk of thunk1 {
__DEFAULT -> ...
}
Моя же разновидность хаскеля предполагала строгую семантику, так-то толку генерить такие case'ы не было. Но до столь тонких оптимизаций руки не дошли.
Еще один пример. В GHC Core все лямбда-выражения имеют только один формальный параметр, а LambdaMan'овская SECD-машина поддерживает вызов функций от нескольких переменных (AP/RAP n). Я не стал заморачиваться, поэтому вызов многоместной функции превращается в цепочку из нескольких последовательных вызовов. А можно было бы сэкономить несколько машинных тактов и CONS-ячеек в Env'е. Зато автоматически поддерживается каррирование функций, чего так не хватало в lmc.
В общем, проблемы есть. Это уж не говоря про то, что прототип остался прототипом и иногда тривиальные изменения в исходном коде стратегии приводят к тому, что мозги компилятора взрываются в панике или плагин генерирует некорректный код.
С другой стороны, плюсы разработки стратегии LambdaMan'а на почти полноценном хаскеле легко перевешивают любые неудобства. Вплоть до того, что можно использовать часть функций из Prelude и даже других библиотек. Т.ч. если бы я догадался до этого варианта в пятницу, то стоило бы попробовать.
Кстати, команда, которая провернула аналогичную афёру с OCaml'ом — gagallium, — получила judges prize :-)
Do Not Go Gentle Into That Good Night
Финальные результаты можно посмотреть в официальном репозитории. Наши с Лёхой команды называются IKS и SKY (искать ближе к концу списка...). Лёха еще и на 100 с лишним очков обойти меня ухитрился.
Да, к сожалению, из-за небольшого форс-мажора у нас случился split-brain, поэтому команд две, а не одна.
Мы не смогли воспользоваться естественным разбиением Проблемы на подзадачи: Компилятор, Стандартная Библиотека, Стратегия, Призраки, — каждый делал всё. На выходе получилось два работающих компилятора, две стандартные библиотеки, две независимые стратегии и ни одного призрака.
Натупили мы напару тоже немало. Взять хотя бы то, что Лёха реализовал подмножество racket'а, но не сообразил, что можно отлаживать Стратегию (или хотя бы Стандартную Библиотеку) на racket'е же. Это как, вообще?! Ха-ха-ха! Я уж молчу про то, что компилятор лиспа в SECD-машину на лиспе гуглится ровно за секунду... Мда.
Отчёты участников в этот раз довольно унылые, честно говоря (или я что-то пропустил?). У _adept_'а, вон, вообще не задался :-) Т.ч. упомяну только отчёт обладателя first prize — Supermassive Black Hom-set и отчёт обладателя judges prize — gagallium.
Зато отжигают организаторы.
Да и вообще, ICFPC держит марку. Огромная благодарность оргам за возможность полноценной offline-работы, отсутствие особых требований к железу и отличную Проблему.
Ну, тренд понятен... Ждём теперь тетрис для НАМ, sokoban для КАМ, minesweeper для МП итд :-)
The Imitation Game
Ну и пользуясь случаем вангую, что в этом году организатором ICFPC-2015 будет небезызвестная контора Galois.
Да-да, high-assurance cryptography, вот это вот всё. Так что дружно ботаем Cryptol и Co, пока еще есть немного времени.
Дорогой читатель! Впереди тебя ждёт захватывающее и полное букв и других опасностей и приключений погружение в мир NP-полноты и SMT-солверов. Кто не спрятался - я не виноват.
Организаторы, а в этом году это была широко известная в узких кругах группа RiSe из MS Research, дали несколько хинтов. Во-первых, что задание будет содержать элементы "program synthesis". Во-вторых, что надо освежить свои навыки работы с json и S-выражениями. В-третьих, что нужен будет постоянный доступ к Сети. И в-четвёртых, что чем больше у нас будет вычислительных ресурсов - тем лучше. Ну, это как водится.
Мы с Лёхой заранее были настроены участвовать и даже слегка готовились. Что касается S-выражений, json'а и постоянного доступа в Сеть, то тут было всё достаточно прозрачно. Для разминки я немного повозился с aeson и сделал небольшой интерпретатор для чего-то такого... с S-выражениями, в общем.
В качестве "считалочки" у нас был Windows-сервер с 12 ядрами и 96 гигами памяти. В резерве еще был 8-ядерный сервер с 32 гигами памяти и, в принципе, можно было еще по сусекам наскрести немного. Т.ч. мы считали, что вычислительными ресурсами обижены не сильно.
Самым пикантным моментом оставались пресловутые элементы "program synthesis". Академическими изысканиями на эту тему мне заниматься как-то не приходилось, зато коллеги ежедневно страдают от моей замороченности на тему корректности программ вообще и на тему систем типов в частности. Короче, в качестве подготовки к "program synthesis" я на каких-то выходных реализовал простенький аналог djinn. Правда только для Минимальной Логики/Просто типизированной лямбды, потому что вмешался один фокусник со своей "домашкой"...
Лёха же, как недавно выяснилось, еще в университете успел позаниматься верификацией параллельных протоколов, и ему тема была видна под другим углом. Время от времени он стал произносить заклинание "SAT-солвер", которое я успешно игнорировал.
До кучи мы прошерстили сайт MS Research на предмет "program synthesis". В частности, я посмотрел львиную долю работ из этого списка. Статьи, конечно, читались по диагонали, но главная идея была усвоена.
Задачи, будь то верификации, синтеза или доказательства каких-нибудь свойств программ, формулируются в виде системы уравнений, связывающей пред- и постусловия всей программы и/или её фрагментов, инварианты циклов итп. Все дальнейшие рассуждения ведутся в терминах полученной системы. В конечном итоге она скармливается какому-нибудь SAT/SMT-солверу и всё - profit.
Всё бы хорошо, но есть маленький нюанс. Дело в том, что записанная наивно система уравнений для задачи верификации получается в логике первого порядка. А для задачи синтеза - в логике второго порядка. В силу некоторых теоретических затруднений современные SMT-солверы, скажем так, не отличаются умом и сообразительностью в этих задачах. Интрига многих статей как раз и заключается в том, как бы переписать систему уравнений для выбранного класса задач (выбрать класс задач, чтобы система уравнений переписалась...) в приемлемую для солвера "безкванторную" форму в какой-нибудь "разрешимой" теории, сохранив при этом разумный порядок числа переменных и уравнений.
Желающие могут ознакомиться, например со статьями "From Program Verification to Program Synthesis" или "Synthesis of Loop-Free Programs". Я читал обе до контеста, но почему-то даже не вспомнил про них в процессе. А жаль, потому что во второй статье уже в abstract'е написано, что их чудо-синтезатор "can efficiently synthesize highly nontrivial 10-20 line loop-free bitvector programs". Как выясняется при дальнейшем чтении, слово "эффективно" здесь означает "быстрее, чем за час" (справедливости ради: только 4 задачи из рассмотреных 27 в статье решались дольше 5 минут).
А вот идея поинтересоваться всё-таки, что же за солвер такой используют авторы статей, поставить его, пройти какой-нибудь туториал... она как-то даже и не возникла.
Еще пара технических моментов. Как всегда я пытался пролоббировать хаскель в качестве основного языка нашей команды. Но оказалось, что, во-первых, Лёха на нём давно (собственно, год) не программировал и не готов на такие подвиги. Во-вторых, выяснилось, что ghc-7.6.3 неважно поддерживает 64-битные Windows и скомпилированная программа стабильно валится при попытках аллоцировать много памяти. Разработчики об этом знают и даже собираются починить в светлом будущем... В общем, мои надежды устроить хаскельному рантайму стресс-тест на 96 гигах были зарублены на корню.
В итоге мы опять решили использовать две технологии - haskell и c# - и бороться потом с "языковым барьером".
Интеграцию я себе представлял в виде каши из bash/curl/grep/sed итп. Поскольку на Windows все эти высокотехнологичные вещи малодоступны (а поставить cygwin до контеста Лёха наотрез поленился...), то мы решили, что сабмитить будем с моего ноута. Взаимодействие с сервером-"считалочкой" могло быть, например, реализовано через git. А я автоматически становился ответственным за "обвязку" (sick!)
За всеми этими приятными хлопотами время неумолимо прикатилось к утру пятницы, 9 августа 2013-го года...
1. Пятница
Мы с Лёхой договорились встретиться у него на работе в Новых Черёмушках в 9 утра. Поскольку Новые Черёмушки от меня лишь чуть ближе, чем бесконечность, то пришлось ставить будильник на нехарактерные 7 утра. Спалось почему-то плохо и я проснулся в 6 с копейками. Впрочем, никакого желания вставать, изучать задание и начинать что-то с этим делать я в себе не обнаружил. Пришлось сделать вид, что я приокрываю один глаз только для того, чтобы выключить будильник, который заорёт минут через 40. На эту маленькую хитрость организм купился и дальше пошло полегче: вместо отключения будильника я рефрешнул на телефоне страничку контеста и начал читать. Изучив в первом приближении задание, переключился на твиттер (и "много думал", ага). В твиттере ничего особенно интересного не было, тематические jabber и irc по-прежнему не освоены, поэтому скоро читать стало решительно нечего. Воспользовавшись вернувшимся к этому моменту стереоскопическим зрением и проклиная всё на свете, а особенно свой дурацкий фанатизм насчёт программерских контестов в 6 утра, я поплёлся в душ, обдумывая по дороге задание.
Задание при первом прочтении не вызывало никакого энтузиазма. Это был точно такой же "program synthesis", как в упомянутых выше статьях. Нам предлагалось сыграть в игру "угадай мою функцию за 5 минут". Причём сыграть в неё можно было 1420 раз (впоследствии количество задач увеличили двумя бонус-паками до 1820). Причём каждые 20 секунд на сервер можно было посылать не более 5 запросов. Запросы, по существу, были двух видов: "вычисли мне загаданную функцию вот на этом наборе входов (не более 256 штук за один запрос)" и "вот мой ответ, соглашайся или дай контрпример". При первом обращении к задаче начинал тикать таймер и если не успеть засабмитить правильный ответ в течение пяти минут, то всё - задача продалбывалась. За решённую задачу давали ровно одно очко вне зависимости от её сложности.
Функции-загадки записывались на специальном языке \BV, синтаксис которого прилагался:
program P ::= "(" "lambda" "(" id ")" e ")"
expression e ::= "0" | "1" | id
| "(" "if0" e e e ")"
| "(" "fold" e e "(" "lambda" "(" id id ")" e ")" ")"
| "(" op1 e ")"
| "(" op2 e e ")"
op1 ::= "not" | "shl1" | "shr1" | "shr4" | "shr16"
op2 ::= "and" | "or" | "xor" | "plus"
id ::= [a-z][a-z_0-9]*
и действовали из пространства 64-битных векторов в него же. Как можно видеть, функции здесь все тотальные, вычисление гарантированно завершается за фиксированное число шагов, бинарные операторы коммутативны, из констант есть только "0x0000000000000000" и "0x0000000000000001".
Единственной нетривиальной конструкцией является оператор fold, правила поведения которого были подробно описаны. Он позволяет проитерироваться по байтам своего первого аргумента и может встречаться в программе не более одного раза. Остальные недостающие детали предлагалось выяснять с помощью тренировочного режима.
Про каждую задачу был заранее известен её "размер" (фактически, количество узлов в дереве лямбда-выражения) и "класс" (набор операторов, используемых в записи исходной задачи). Решение должно было быть из того же класса (или более узкого). При этом оно могло быть любого размера до 100 включительно.
Оставался тонкий вопрос с тем, как организаторы собираются проверять решения и строить контрпримеры.
На самом деле, до контеста я успел поиграть с Pex'ом, поэтому тут мне тоже всё было понятно.
И эквивалентность докажут, и контрпример построят.
Правда делалась оговорка, что если доказать эквивалентность решения и загаданной функции не получится, то решение засчитано не будет - таков регламент.
Короче говоря, на выходе из душа я твёрдо знал следующее. Решать задачу мы будем путём превращения её в систему уравнений и скармливания их какому-нибудь "промышленному солверу". В нашей команде за направление "промышленных солверов" отвечает Лёха, который периодически возится с ними по работе. Он грозился всё настроить на серваке, т.ч. технология у нас уже должна быть. Размеры задач в 30 узлов с виду страшными совсем не казались. Наоборот, было ощущение, что "монстры" всё решат еще в лайтнинге (а может и уже решили - скорборда-то нет...), реализовав оптимальный для этой задачи перебор. Правда, понятно, что орги могут легко увеличить максимальный размер... или добавить операторов... или еще что-нибудь.
А мне предстоит заниматься страшно ответственной и безумно интересной работой по "обвязке". Ну, вы знаете уже... curl/sed/grep/bash...
Прочитав Лёхину sms'ку на тему:
Да!!!! Это классная задача!
я вздохнул и поехал на Новые Черёмушки...
В толчее метро в мозгу произошло какое-то спонтанное нарушение симметрии и он зачем-то стал думать над задачей. Какие к ней могут быть подходы, помимо сведения к SMT? Брутфорс я отбросил сразу по причине неинтересности и задался таким вопросом: можно ли по известным парам входов/выходов проанализировать влияние каждого бита входного слова на каждый бит выходного. В общем виде эта задача казалась какой-то подозрительно сложной, зато теория "линейных операций" выстроилась достаточно быстро.
На выходе из метро я сообщил об этом Лёхе. Тот сказал: "Отлично!" - и следующие трое суток категорически отказался слушать меня на эту тему. Частные случаи его, видите ли, не интересуют. Ему общее решение подавай с утра пораньше. Ну, ok.
Добравшись до места, мы заварили себе кофе и стали держать совет. Лёха изложил план действий, который просто подкупал своей новизной. Он собирался выписать уравнения, описывающие класс "линейных задач", потом переложить их на c# и скормить через API какому-то SAT/constraint-солверу. Я же в это время должен был - внезапно! - реализовать "обвязку". Потом мы должны были объединить наши усилия и только тут узнать, является ли "промышленный солвер" достаточно промышленным для наших задач или требуются менее технологичные решения.
Стоп-стоп... т.е. выясняется, что Лёха "никогда этот солвер в таком режиме не использовал" и что он не может дать никаких оценок, получится ли из него выжать "общее решение" или нет. Т.е. мы в очередной раз собираемся инвестировать драгоценное время контеста в освоение какой-то неземной технологии, которая еще непонятно, сработает или нет. Т.е. опять в который раз по тем же граблям... Тем не менее, этот безумный план утверждается, и мы приступаем к его реализации.
Нет, наверное всё-таки надо объясниться, почему я вообще повёлся на всякие там солверы и прочую чёрную магию. Ну, во-первых, всегда есть толика здорового любопытства - интересно же повозиться с новой игрушкой. Во-вторых, всегда есть толика нездорового любопытства - а вдруг сработает? В-третьих, были прочитанные статьи MS Research (и надежды, что Лёхин солвер попромышленнее окажется, чем микрософтовский). И, в-четвёртых, было вдумчивое изучение базового для всех SMT-солверов DPLL-алгоритма, который вроде как намекал на способ, которым солверу можно давать хинты. И вот это очень хотелось попробовать.
Когда перебор дерева вариантов программируется руками, то всегда есть риск попасть в ситуацию, когда ты что-то такое знаешь о задаче в целом, но это очень сложно выразить в виде локального направления перебора, сидя в конкретном узле дерева вариантов. А на языке уравнений высокоуровневые ограничения вроде "в искомом лямбда выражении не менее трёх раз встречается операция shl1" или даже "в лямбда выражении скорее всего встречается подвыражение and x b, где b имеет размер не более 3 и состоит только из op1" выражаются очень изящно и добавляются "аддитивно" (ad-hoc), не требуя изменения логики перебора, протаскивания и хранения в узлах дерева дополнительных параметров итп. И очень хочется верить, что "умный" солвер учтёт предложенные ограничения и гипотезы для сокращения перебора. И как потом оказалось, иногда это действительно отлично работает. Но всё это было чуть позже, а пока что мы засучив рукава принялись за дело.
Ну, насчёт "засучив рукава" - это сильно сказано. На самом деле, мы засели, уткнувшись каждый в свой комп, и стали тихонько что-то делать. Никакого адреналина, спонтанных обсуждений и споров до хрипоты. Всё спокойно и по регламенту. Ну т.е. совершенно не готовы морально оказались к контесту...
Судя по git-логу, за первый час я запилил интерпретатор \BV и далее занялся "обвязкой", как сам её понимал.
А понимал я её примерно так. "Обвязка" запускает "решалку" и подаёт ей на вход размер задачи, набор разрешённых операторов и набор пар вход/выход. Далее ждёт от неё на выходе решение, обрабатывает его и если находит контрпример, то опять же докармливает им "решалку". При этом я дико опасался, что сервер организаторов будет под нагрузкой лежать так же, как это было в 2010-ом, да и жрать лимит http-запросов не хотелось. Поэтому первый тренировочный режим был реализован вообще без обращений к серверу. Для построения контрпримеров использовался quickcheck... Опасения мои, кстати, оказались напрасными - в этот раз у оргов всё работало как часы. Да и лимит по запросам оказался весьма гуманным. Мы, во всяком случае, в него не упирались :-)
Вся эта интеграционная деятельность была закончена тоже примерно за час, т.е. к полудню пятницы. И где-то в это же время Лёха выдал на гора первую версию своего синтезатора. Чем мы занимались следующие два часа я ума не приложу. Видимо, скрещивали ежа с ужом, а потом фиксили в обоих баги? А где соответствующие коммиты? Следующий мой коммит был в 13:45 и в нём была всего лишь добавлена поддержка if0 и fold в интерпретатор. Но это было даже не важно, потому что синтезатор на тот момент всё равно не умел их использовать.
Потом мы пошли обедать и дела наши стали совсем плохи, потому что следующий содержательный коммит был аж в семь вечера. И еще пачка коммитов в районе десяти, когда мы стали собираться домой. Что, чёрт возьми, мы делали всё остальное время? Забегая вперёд скажу, что нам в итоге не пригодилось практически ничего из того, что было сделано за день.
В принципе, к вечеру наш солвер уверенно щёлкал линейные задачи небольших размеров. Более того, Лёха успел реализовать и поддержку каких-то бинарных операций. Но накопился за день и ворох неразрешённых проблем...
Во-первых, официально занимаясь "обвязкой" и вопросами "интеграции" я ухитрился даже список наших задач не скачать, чтобы посмотреть как там распределяются классы и размеры. Это было сделано только ближе к часу ночи после возвращения домой. Это, конечно, не техническая проблема, но она здорово мешала :-)
Во-вторых, программирование уравнений в смешном синтаксисе c# оказалось весьма неэффективным занятием. Большую часть времени Лёха убил на поиск и исправление однобайтных ошибок из серии "я опять где-то накосячил с индексами" и вкуривание загадочных исключений, вылетающих из API проприетарного солвера. Ситуация еще усугублялась тем, что...
В-третьих, Лёха так и не смог выжать из своего "промышленного солвера" теорию 64-битных векторов. Поэтому изначально солвер вообще использовался в режиме SAT, а не SMT. Это приводило к тому, что вместо каждого одного уравнения над битовыми векторами приходилось записывать 64 уравнения над булевскими переменными.
Например, вместо простого уравнения
$$
x_i = \shl\ x_{i+1}
$$
приходилось писать что-то в духе
\begin{equation*}
\begin{split}
& x_i^0 = 0,\, \\
& x_i^j = x_{i+1}^{j-1},\, j=1..63 \\
\end{split}
\end{equation*}
И если с большинством операторов из op1 и op2, а также с if0 это прокатывало, то представьте себе, во что превращалось простенькое
$$
z = \plus x \, y
$$
О том, чтобы реализовать таким способом fold мы даже и не помышляли...
В течение дня решение неоднократно переписывалось то в терминах двух 32-битных векторов (для упрощения реализации plus), то в терминах восьми байтов на переменную (с прицелом на fold). Что-то мне подсказывает, что Лёха так наигрался со всевозможными "битами переноса", что его даже троллить на эту тему опасно :-)
И, наконец, в-четвёртых, было не очень понятно, как кодировать структуру дерева лямбда-выражения. Для линейных операций использовались простые целочисленные переменные \(c_i^{op}\) - индикаторы того, что в i-ом узле используется операция op:
\begin{equation*}
\begin{split}
& c_i^{op} \in \{0,1\} \, - \text{индикатор, 0 или 1} \\
& \sum_{op} c_i^{op} = 1,\, i=1..size \, - \text{в каждом узле ровно одна операция} \\
\end{split}
\end{equation*}
С бинарными операциями структура лямбда-выражения переставала быть линейной и превращалась в дерево неизвестной заранее топологии. Очень хотелось придумать такое "естественное" кодирование для этого дерева, чтобы оно максимально ухватывало структуру задачи. Как минимум арность операторов и их коммутативность. Но желательны были также возможность обойтись решением меньшего или большего размера, отсечение заведомо тупиковых ветвей перебора, отсечение перебора заведомо эквивалентных поддеревьев... Если задуматься, то на выбранном нами пути получения решения с помощью SMT-солвера это была единственная содержательная задача.
Самое смешное, что к вечеру так и не образовалось ясности в главном вопросе этого блога "о жизни, вселенной и всём прочем": будет ли пригодно наше решение для синтеза бинарных операций, if0'я и fold'а или всё-таки только 42? И да, у нас даже не хватило пороху дожать "интеграцию" и набрать эти самые 42 символических очка на линейных задачах.
На этой радостной ноте мы расстались и поехали по домам, договорившись встретиться на следующее утро в 10.
Однако по пути домой ситуация стала неуловимо меняться. Очень, знаете ли, полезно иногда оторваться от компа и пообщаться с напарником по команде. Пусть даже и посредством sms:
- Лёш, есть идея, как по eval оценивать число op2 в дереве. Завтра.
- Да, такие свойства было бы чертовски полезно выводить по входам/выходам.
На следующий день Лёха опять мне зарубит все идеи по анализу входов/выходов, обозвав их частными случаями, и опять потребует "общего решения". Но сейчас я еду в метро домой и в голове постепенно начинают шевелиться мысли, которых очень не хватало там весь день...
Заканчиваю первую треть контеста чтением каких-то статей по криптографии. Хочется понять, можно ли на языке \BV реализовать какую-нибудь относительно криптостойкую функцию хэширования. Если бы это было возможно, то с оргов сталось бы запилить таких функций... Например, с прицелом на judges prize. Но если учесть, насколько сложно на \BV хотя бы поменять два соседних бита местами, то вроде бы любая криптография отпадает.
2. Суббота
В субботу я снова просыпаюсь раньше времени, но на этот раз не от какой-то безумной бессонницы, а от того, что голову разрывают новые прекрасные идеи. "Теория линейного синтеза" за ночь превратилась в стройную науку с матричными неравенствами и "критерием полного тестового покрытия". Кроме того, некоторые её обобщения уже позволяют извлекать кое-какие факты - хинты для солвера - о структуре дерева искомого лямбда-выражения.
Всеми этими соображениями я спешу поделиться с партнёром по команде и поэтому зачем-то приезжаю на Новые Черёмушки на полчаса раньше назначенного срока. В итоге на матричные неравенства Лёха чуть было не повёлся, но всё-таки сообразил, что ему продают вчерашнего слона, и выдал следующее:
- Я тут вчера вечером про их SMT-солвер Z3 почитал.
Предлагаю тебе сегодня получить свою порцию фана от возни с солвером, а я займусь "обвязкой".
Такого нелинейного поворота сюжета ваш покорный слуга не выдержал и сходу согласился.
Честно говоря, я не ожидал, что Лёха так легко откажется от своего решения с "промышленным солвером".
Поэтому я собирался заняться развитием теории входов/выходов, чтобы получше разобраться в свойствах задачи. В результате ожидалась улучшенная кодировка дерева или хотя бы какие-то хинты-эвристики для солвера. Тем более, что некоторые я уже знал.
Но, очевидно, Лёха за ночь вынес своему решению приговор. "Промышленный солвер" оказался слишком SAT для этой задачи и нам нужно либо что-то более SMT, либо вообще что-то совсем другое. Кроме того, Лёха очень страдал от отсутствия возможности порешать тренировочные задачки в условиях, максимально приближенных к боевым. Почему-то ему не нравилось, что я за весь прошлый день так и не автоматизировал этот процесс...
План повторял вчерашний с точностью до названия солвера и замены исполнителей. Я ставлю Z3 и учусь с ним работать из haskell. Лёха делает "обвязку" на .net с базой данных задач, блекджеком и всеми лямбдами. На вечер запланировано преодоление языкового барьера и запуск конструкции в боевом режиме хотя бы на линейных задачах.
На освоение Z3 у меня ушёл весь день...
Сначала часа 2-3 я проходил туториал по Z3 и экспериментировал с ним. Еще часа два убилось на сборку Z3 под Mac OS X 10.7. На тот момент я еще не знал чудесного слова cvc4. Еще какое-то время понадобилось на то, чтобы набить руку в формировании основных синтаксических конструкций SMT-LIB 2, и на парсинг ответов солвера (S-выражения!). Чудесного слова sbv я тоже еще не знал, хотя Лёха его уже где-то вычитал и периодически произносил.
С самими уравнениями никаких особых проблем не возникло, тем более, что в полной красе проявились преимущества SMT-солвера перед SAT, а именно наличие встроенной bitvector-теории для векторов произвольного размера. В итоге, уравнения для plus выглядели примерно так:
(assert (= z (bvadd x y))
Во второй половине дня новый солвер повторил достижения вчерашнего и стал щёлкать линейные задачки. Ближе к вечеру мы продрались через подводные грабли "интеграции", победили очередной раз буферизацию и '\r\n' и запустили всю конструкцию в боевом режиме на линейных задачах. Через несколько минут она нам решила их все и мы получили свои первые 42 очка :-)
Кроме того, у нас появилась база тренировочных задач, статистика по решённым, история ответов сервера как в тренировочном, так и в боевом режиме. Правда я воспользоваться всей этой .net'ной красотой не мог и довольствовался теми крохами с барского стола, которые Лёха присылал мне в скайп по моим заявкам. Можно еще попридираться, что новая "обвязка" не поддерживала "инкрементальный" режим решения. Т.е. если сервер оргов выдавал контр-пример, то мы не пытались использовать ту же сессию солвера, а запускали всё по-новой. Это неэффективно, но я не знаю, сколько мы в итоге задач зафейлили из-за этого. Вряд ли много. Мы также не пытались использовать какие-либо многопоточные возможности Z3 и могли задействовать только одно ядро для решения одной задачи.
Конечно, как всегда, нам было бы неплохо всё это сделать на сутки раньше... Наверное, это уже можно считать девизом нашей команды.
В любом случае для меня суббота была очень продуктивной, и домой я ехал полон желания улучшать наше решение завтра и реализовать-таки бинарные операции, а может даже замахнуться и на if0 с fold'ом. Кроме того, я по-прежнему делал ставку на хинты для солвера и очень хотел, чтобы теперь уже Лёха занялся построением соответствующей теории.
Приехав домой, я за 36 минут запрограммировал "уравнения транзитивного замыкания" \eqref{equation:transitive} для деревьев и на этом, наконец, успокоился.
3. Воскресенье
К утру воскресенья мой субботний запал в значительной степени иссяк. Правда еще ночью я прочитал то, что утром Лёха мне прислал в виде sms'ки:
Блин. Топ 50 - это 300 очков. Работать!!!
А что еще оставалось?
План работ на день был более или менее понятен. Я затребовал себе 4 часа времени на реализацию бинарных операций и попытался убедить Лёху разработать-таки теорию анализа входов/выходов. Но он был неумолим (или не особо доверял моему решению...) и взялся программировать альтернативную версию "решалки" на базе C# + Z3. Я понял, что останусь без хинтов для солвера...
Загоняться на эту тему времени не было, и я просто занялся делом. И практически точно в заявленный час дня у нас появляется первая рабочая версия солвера для задач из op2. Я сдаю её Лёхе "на опыты", запускаю решаться какую-то сравнительно большую задачу и иду обедать. Чертовски хочется спать. А еще предстоит реализация if0, а может и fold'а.
После обеда выясняется очевидное. Солвер тормозит-с... Нужно дать ему хинтов, оптимизировать уравнения, подобрать начальный набор входов/выходов и вообще - навести красоту.
А еще нужно, наконец, уже выписать сами уравнения.
Итак. Поскольку никакой лучшей кодировки дерева придумано не было, то в качестве "естественной" была использована следующая. Каждому узлу дерева присваивается номер от 1 до N. Далее вводятся следующие переменные:
\begin{equation}
\begin{split}
& t_{ij} :: Bool \, - \text{индикатор того, что i-ый узел дерева является родителем j-ого;} \\
& s_{ij} :: Bool \, - \text{индикатор того, что i-ый узел является предком j-ого;} \\
& c_i^{op} :: Bool \, - \text{индикатор того, что в i-ом узле используется оператор op;} \\
& x_i^k :: BV64 \, - \text{значение выражения в i-ом узле дерева на k-ом входе;} \\
& u_k, v_k :: BV64 \, - \text{значение k-го входа и выхода;} \\
& i,j = 1..N, \, \text{где N - размер задачи;} \\
& k=1..M, \, \text{где M - число известных пар вход/выход;} \\
& op \in \Op, \, \text{где Op - множество разрешённых для данной задачи операторов.} \\
\end{split}
\end{equation}
Узел под номером 1 произвольно объявляется корнем дерева. Сделать это можно разными способами. Например, можно потребовать, чтобы из него был путь в любой другой узел:
\begin{equation}
\label{equation:notroot}
s_{1j} = \true, \, j=2..N
\end{equation}
Но этот способ позволяет искать решения только в точности заданного размера. А к этому моменту нам уже известно, что очень часто можно найти решения меньшего размера, чем указано в задаче. Поэтому мы вместо \eqref{equation:notroot} требуем, чтобы из любого другого узла не было пути в корневую вершину:
\begin{equation}
\label{equation:root}
s_{j1} = \false, \, j=2..N
\end{equation}
Идея была в том, чтобы разрешить несвязные графы и "леса" вместо деревьев. На практике это привело к появлению решений как меньшего, так и большего размера :-)
Поскольку переменные \(s_{ij}\) кодируют отношение "есть путь из i в j", то соответствующая матрица должна быть "почти антисимметричной":
\begin{equation}
\begin{split}
& s_{ij} \Rightarrow \neg s_{ji}, i \neq j \\
& s_{ii} = \false \\
\end{split}
\end{equation}
Значения на диагонали особой роли не играют.
Гвоздь программы - те самые "уравнения транзитивного замыкания", изобретённые Лёхой за пару минут на коленке еще в пятницу:
\begin{equation}
\label{equation:transitive}
\begin{split}
& s_{ij} = \bigvee_{k \neq i,k \neq j} t_{ik} \wedge s_{kj} \\
& t_{ij} \Rightarrow s_{ij} \\
\end{split}
\end{equation}
Пожалуй, оставлю без комментариев...
Далее нужны уравнения на арность узлов дерева. Это "ахиллесова пята №1" нашего решения...
Для кодирования арности каждого узла вводятся вспомогательные переменные
$$
a_i^r :: Bool, r=0..2 - \text{индикатор того, что арность i-го узла равна r.}
$$
Их значения связываются "очевидным" образом с одной стороны с \(t_{ij}\):
\begin{equation}
\begin{split}
& a_i^0 = \bigwedge_{j \neq i} (\neg t_{ij}) \\
& a_i^1 = \bigvee_{l \neq i} (t_{il} \wedge \bigwedge_{j \neq i,j \neq l} (\neg t_{ij})) \\
& a_i^2 = \bigvee_{q \neq i, p \neq i, p \neq q}
(t_{iq} \wedge t_{ip} \wedge \bigwedge_{j \neq i,j \neq q,j \neq p} (\neg t_{ij})) \\
\end{split}
\end{equation}
а с другой стороны с \(c_i^{op}\):
\begin{equation}
\begin{split}
& c_i^{op} \Rightarrow a_i^0, \, op \in \Op_0 - \text{листовые узлы дерева} \\
& c_i^{op} \Rightarrow a_i^1, \, op \in \Op_1 - \text{унарные операции} \\
& c_i^{op} \Rightarrow a_i^2, \, op \in \Op_2 - \text{бинарные операции} \\
\end{split}
\end{equation}
Т.е. вместо изящных уравнений на арность вроде такого:
$$
c_i^{\and} \Rightarrow (2 = \sum_{j \neq i} t_{ij})
$$
получился какой-то ад 4-ой степени сложности от числа узлов дерева. А всё потому, что я сходу не нашёл приемлемого способа использовать переменные разных теорий в одном уравнении. А потом так и не вернулся к этому вопросу. Наверняка, это можно как-то легко упростить. Более того, в процессе контеста несколько раз появлялись идеи, как вообще можно отказаться от уравнений на арность.
Но, увы.
"Ахиллесовой пятой №2" нашей кодировки было то, что солвер мог перебирать много деревьев, отличающихся лишь нумерацией узлов. Это отчасти было исправлено в процессе "диагонализации" уравнений при реализации if0. Но потенциал для сокращения пространства перебора всё равно остался огромный.
Далее нам требуются уравнения связей между значениями в узлах дерева:
\begin{equation}
\begin{split}
& c_i^{op} \Rightarrow x_i^k = \op u_k, \, \op \in \Op_0 \\
& c_i^{op} \wedge t_{ij} \Rightarrow x_i^k = \op x_j^k, \, \op \in \Op_1 \\
& c_i^{op} \wedge t_{ij} \wedge t_{il} \Rightarrow x_i^k = \op x_j^k x_l^k, \, \op \in \Op_2 \\
\end{split}
\end{equation}
Уравнения на индикаторы операций в одном узле:
\begin{equation}
c_i^{op} \Rightarrow \bigwedge_{op' \neq op} (\neg c_i^{op'})
\end{equation}
И, наконец, уравнения для выходов:
\begin{equation}
x_1^k = v_k
\end{equation}
Вот, собственно, и вся высокая наука.
После обеда Лёха сгенерил несколько ценных идей по оптимизации уравнений.
Во-первых, матрица \(s_{ij}\) была приведена к верхнетреугольному виду. Т.е. были запрещены деревья, в которых присутствовали рёбра, ведущие из вершин с большими номерами в вершины с меньшими. В отсутствии хинтов это не приводит к потери общности, т.к. нумерация узлов произвольная, а корневая вершина всегда имеет номер 1. При этом в теории пространство перебора очень сильно сокращается, но непонятно, есть ли от этого счастье на практике.
Во-вторых, все уравнения были соответствующим образом "диагонализированы" с учётом нового ограничения и система стала примерно вдвое компактнее. Одновременно с этим появилась возможность различать аргументы операций. Для коммутативных операций свойство бессмысленное, но очень нужное для реализации if0, который и был в итоге запилен ближе к семи вечера. В итоге адские уравнения арности получили сложность \(O(n^5)\)...
Тем не менее "решалка" достаточно уверенно справлялась с задачами размером в 9-10 узлов. Браться за реализацию fold'а под вечер не хотелось, поэтому сдав Лёхе очередную версию солвера в "интеграцию" я решил вернуться к вопросу хинтов и прочих эвристик.
Первой эвристикой была такая:
$$
\label{heuristics:const0}
c_j^0 \wedge t_{ij} \Rightarrow c_i^{\not} \vee c_i^{\ifzero}
$$
Логика здесь простая. Если некоторый узел - это просто константа 0, то её родителем может быть только if0 или not. Все остальные варианты - сразу бессмысленные, и перебирать их точно не нужно. Этот нехитрый приём сразу ускорил работу "решалки" в несколько раз, поэтому версия солвера с "оптимизированным нулём" была немедленно отправлена в "интеграционные мастерские".
Далее я попытался упростить перебор несвязных компонент дерева, сразу объявив их константами:
$$
\neg s_{1i} \Rightarrow c_i^1
$$
Это не произвело солвер ни малейшего впечатления, поэтому "оптимизация" была немедленно выпилена обратно.
По-хорошему, дальше надо было попробовать изжить всякие тривиальные цепочки, типа not-not или shl1-shr1-shl1, но я их оставил "на потом" (и благополучно забыл об этом) и попытался реализовать наблюдение, что в тестовых задачах очень часто (всегда?) последний аргумент любой бинарной (и тернарной) операции - это либо 1, либо x.
Это не сработало ни в виде гипотезы:
$$
h \Rightarrow (c_i^{op2} \wedge t_{ij} \wedge t_{ik} \wedge k>i \Rightarrow c_k^1 \vee c_k^x)
$$
ни в виде гвоздями прибитого уравнения:
$$
c_i^{op2} \wedge t_{ij} \wedge t_{ik} \wedge k>i \Rightarrow c_k^1 \vee c_k^x
$$
Тем не менее мы почему-то решаем, что наблюдение о "последнем аргументе" - ценное и следующие полтора часа я трачу на то, чтобы превратить бинарые операции в унарные. Вместо and появляются andX и and1, вместо or - orX и or1 и так далее. Бинарные операторы исчезают как класс вместе со всеми своими уравнениями. Это работает неплохо и отправляется в "продакшн". Вопросов о "потере общности" и бонусных задачах почему-то не возникает.
Еще одна прикольная оптимизация, которая осталась нереализованной, была такая. Предлагалось искусственно ввести в язык произвольные константы. Далее по аналогии с технологией "оптимизации нуля" потребовать, чтобы константы можно было использовать только в качестве последнего аргумента бинарных операций, а также второго или третьего аргумента if0. Решать полученную задачу обычным образом с помощью Z3, а потом пытаться сгенерить необходимые константы с помощью моей "теории линейного синтеза". Если этот номер не проходил (из-за ограничения в 100 узлов или класса задачи), то к уравнениям можно было бы добавить запрет на использование "неправильных" констант и попросить солвер перерешать.
Время уже в районе половины десятого, Лёха перестаёт принимать новые версии. Более того, он почему-то категорически отказывается запустить несколько кастомизированных солверов, оптимизированных на разные классы задач, в параллель. Аргументирует тем, что "мы сейчас накосячим в последние десять минут". Препираемся мы на эту тему значительно дольше, чем мне бы потребовалось времени на реализацию солвера для бонусных задач...
За день Лёха успел сделать свою альтернативную реализацию на базе C# + Z3. Но даже не пытается протолкнуть её в продакшн. По крайней мере моё изделие ни разу не сгенерило некорректную задачу и не выдало unsat: либо model, либо timeout. Да и работает вроде как пошустрее. Именно оно и объявляется той финальной версией, которая будет автономно работать до самого окончания контеста. Наконец, всё настроено, окончательно утверждён SQL-запрос для выборки задач в "правильном" порядке, настроены таймауты и даже подключен многопоточный executor, который позволит нам худо-бедно утилизировать все 12 ядер сервака. Поехали!
И мы поехали домой. По приезду домой я обнаруживаю, что мы набрали около 230 очков и число это более не меняется. Это не согласуется с тем, как бодро решались первые задачи сразу после команды "ключ на старт". Поэтому я решил, что у нас всё-таки что-то сломалось (наутро оказалось, что это не так - просто солвер добрался до задачек содержательного размера и стал их фейлить по 12 штук каждые 5 минут). Дёргать Лёху по этому поводу смысла не было - он и так под конец устал и откровенно ныл.
Я тоже устал и чертовски хотел спать. Но решил сделать еще одно небольшое усилие над собой. Дело в том, что пока я ехал час в метро, я понял, как можно быстро реализовать tfold (это особый вариант fold'а, когда он является top-level оператором в дереве). Ну как быстро... два часа провозился-таки и закончил примерно в половину третьего. При этом я был уверен, что контест заканчивается в три по Москве, "интеграции" у меня не было, поэтому я стал неспешно решать tfold-задачи в "полуавтоматическом" режиме. И так увлёкся этим процессом, что обнаружил себя за этим занятием примерно в 20 минут четвёртого, решив к этому времени штук 20 задач. Тут я понял, что не знаю, во сколько заканчивается контест, но без автоматизации дальше двигаться нельзя, т.к. уже идёт конкретная тупка при выполнении рутинных операций. Пришлось запилить, наконец, ту самую легендарную "обвязку" из не скажу чего и палок, curl/grep/sed итп. На это ушло ровно 40 минут и первый запуск "интеграции" в боевом режиме состоялся, как потом показало вскрытие, точно в 4:00. Сервер организаторов не оценил моего порыва и сказал, что "финита ля комедия". Я тупил уже совсем конкретно, поэтому еще несколько минут ломился на него и пытался понять, что не так и почему мне не дают задач :-)
Ну вот, собственно, и всё. На выходе у нас 254 очка в основном зачёте и место между 200 и 175.
Картинка для привлечения внимания
Future directions
А если бы не SMT, то кто? Очевидно, переборчик. Например, такой.
Для выбранного класса задач запускается программа, которая генерирует в разделяемой памяти все деревья лямбда-выражений из этого класса размером от 1 до сколько хватит памяти и кое-какую метаинформацию о них. Конечно, на самом деле смысла хранить все деревья нет. Нас интересуют только неэквивалентные лямбда-выражения. Поэтому все описанные выше оптимизации, типа "оптимизации 0" или "not-not" и любые другие, которые можно придумать, остаются в силе.
В качестве метаинформации достаточно было бы хранить, например, 32-битный хэш от вектора значений функции на фиксированном векторе входов. Но если чуть-чуть помечтать, то для быстрого "инкрементального" вычисления значений хэша он должен обладать таким свойством:
h . map f x = f . h x
Навскидку я знаю только одну функцию h, которая удовлетворяет такому свойству для любых операторов f из \BV и непустых наборов входных векторов - это функция head :-) Но тут можно подумать еще.
Так вот, даже тот (ужасно неэффективный) способ представления построенного множества деревьев, который я придумал во время поездок на метро в процессе контеста, позволяет в 48 гигах памяти разместить порядка \(2^{32}\) деревьев и искать их по хэшу за логарифмическое время. И наверняка можно с помощью каких-нибудь трюков либо еще на порядок увеличить число хранящихся деревьев, либо хотя бы оптимизировать доступ к этому каталогу с учётом особенностей NUMA-архитектуры.
Строить этот каталог можно достаточно долго (даже часами), учитывая структуру задачи и применяя все возможные оптимизации для исключения эквивалентных деревьев вплоть до запуска Z3 для пар деревьев с совпадающими хэшами.
Зато после того, как каталог построен, поиск решений становится очень эффективным. Сначала нужно попросить сервер вычислить функцию на том входном наборе значений, который был использован для вычисления хэшей. Потом за логарифмическое время найти все функции с совпадающим хэшом. Если хэш-функция хорошая и эквивалентные деревья при построении каталога отсекались эффективно, то таких функций будет очень мало. Далее надо продолжать сужать это множество, запрашивая контр-примеры у сервера. Если множество сузилось до пустого, то готового решения в нашем каталоге нет и нужно запускать перебор.
Перебор может быть запущен с той точки, где остановилось построение каталога. При этом нам уже не нужно особо заморачиваться с эквивалентными деревьями. Всё, что нас интересует - это значение хэша и значение функции на контр-примерах. Поиск может быть распараллелен на несколько ядер например по значению top-level оператора в искомом дереве.
А если еще учесть, что построенный каталог можно сохранить на диск и загрузить на другой машине, то открываются просто нечеловеческие возможности спустить денег на амазоновские himem-ноды...
Найденные решения имело смысл добавлять к каталогу, потому что функции-загадки часто повторялись. Заодно было бы неплохо сразу запилить все функции из bithacks.
Попробовать этот подход на деле мне мешает только врождённая лень и отсутствие опубликованного списка функций-загадок. В основном - первое.
Еще кучу всяких ссылок можно найти на неофициальном скорборде, который доступен нам благодаря ребятам из Контура.
Conclusions
Многие недоумевают по поводу очередного отсутствия скорборда в этом году и даже пишут, что
Долбаные академики не понимают, что такое компетишн.
Всё они понимают... Регламент в этом году технически был вообще практически безупречен. Был небольшой сомнительный момент с необходиомстью предварительной регистрации и жёстким требованием "один человек - одна команда". Но нам это не помешало в духе современных политических технологий зарегистрировать дополнительную команду-спойлер. Не то, чтобы мы собирались как-то читерить, просто на случай если что-нибудь конкретно запорем из основной команды. В итоге, команда-дублёр не пригодилась.
Очень крутая тема с ограничением в 5 минут на задачу. Приходится хорошо думать, перед тем, как "открыть" задачку, потому что тратить их просто так очень не хочется. Особенно нервно наблюдать, когда сервер выдаёт тебе контр-пример к задаче, которую ты решал минуту или больше. Но интересно то, что мы большинство задач решали с первой-второй попытки. И только одна задача потребовала четырёх попыток и была решена на третьей минуте. Это говорит не только о том, что мы удачно подобрали входы, но и о хорошей продуманности самой проблемы.
А от скорборда "долбанные академики" отказались совершенно сознательно. При его наличии было бы очень трудно заставить себя позаниматься какими-нибудь SMT-солверами. Ну я бы точно не стал этого делать, будь у меня возможность наблюдать, как растут показатели других команд. Т.е. целью организаторов было получить максимальное разнообразие подходов к проблеме. До какой-то степени они, наверное, своего добились. А те, кому задача показалась слишком простой или скучной - их тоже можно понять, но наверняка они просто запилили брут-форс :-) В общем, оргам грандиознейший респект в этом году. Было бы интересно что-нибудь почитать про "кухню": как готовились, что под капотом и можно ли всё-таки на \BV реализовать криптостойкую хэш-функцию :-)
Что касается результатов нашего выступления то тут чувства смешанные... С одной стороны, 254 очка и 200-175 место, отсутствие драйва и общий прогрессирующий маразм - это Epic Fail.
С другой стороны, наше решение действительно получилось весьма общим и переключаться между классами задач было очень легко.
Если бы мы сразу использовали Z3 с первого дня и инвестировали-таки время в эвристики (которые даже никакие не эвристики, а самая что ни на есть структура задачи), то скорее всего решили бы все задачи из классов op1+op2+if0+tfold где-то до 20-го размера (это около 600 задач).
Кроме того, мы наверняка решили бы полностью первый бонусный пакет (+200).
Т.е. набрали бы где-то половину от максимально возможного количества очков или около того, что опять же говорит об отличной сбалансированности проблемы.
Возможно ли эффективно адаптировать наше решение для оставшихся неохваченными частей (настоящий fold, задачи большого размера и второй бонус-пак) или нет - я не знаю.
Есть еще одно странное последствие контеста. Теперь у меня на компе поселились такие доселе неведомые звери, как Z3, cvc4 и yices. И не просто поселились, а прямо-таки прописались - откровенно ищу, где их можно применить в текущей деятельности. Ну хоть бы одна завалящая NP-трудная задачка попалась в нашем интернет-проекте. Короче, я проникся Великой Идеей и имею заявить следующее: SAT/SMT-солверы - это правильный "промышленный" способ смотреть на прикладные задачи из NP, на которые другими способами и смотреть-то страшно. Т.ч. в этом смысле контест удался на славу - Epic Win.
Ну и выводы 2010-го и 2012-го годов остаются в силе, конечно...
Вот, кажется, и всё. Пользуясь случаем, поздравляю всех с днём программиста, который в этом году удачно выпал на пятницу, 13.
