Abstract
Abstract spherical 0007-team in pure vacuum contest report. Main contribution of this paper is increased entropy.Keywords: IKS, Z3, Epic Fail, Epic Win
Introduction
Ну что ж, The ICFP Programming Contest 2013 is over! и настало время эпистолярного жанра.Дорогой читатель! Впереди тебя ждёт захватывающее и полное букв и других опасностей и приключений погружение в мир 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.
Красавцы! Отчет суперский - настоящий триллер.
ОтветитьУдалитьСпасибо :-)
ОтветитьУдалитьОрганизаторы опубликовали результаты и слайды. Еще обещают видео.
ОтветитьУдалитьТематическая публикация от Олега Киселёва. Очень кстати.
ОтветитьУдалить