Если кто не в курсе, на днях прошел очередной ICFP Programming Contest. Это уже третий раз, когда я принимаю в нем участие, я и еще двое моих друзей: Леша и Саша. О наших прошлых выступлениях можно прочитать по тегу icfpc. В прошлом году мы выступили очень слабо, так что я сделал полезные для себя выводы, и в этот раз получилось все в целом неплохо.
В этом году соревнования проводили Microsoft Research. Накануне они объявили, что нам стоит освежить свои знания в области program synthesis (синтез программ). Понятно, что никаких знаний по этой теме у нас не было, поэтому освежать было нечего. Однако я вяло поковырял Интернет и убедился, что на русском языке нет вообще ничего по данному вопросу, а на английском кроме коротенькой статьи в Википедии все ссылки ведут на работы Microsoft Research. Кто бы сомневался, ага. Я пролистал пару их статей, понял, что ничего не понятно, и с легким сердцем лег спать.
Задание
Есть набор программ (около полутора тысяч штук), которые нужно отгадать. Программа – это функция вида
f(x) = ((~(x + 1) & 1) << 1) ^ 1
Все операции побитовые, аргумент и результат – 64-битные беззнаковые целые. Программа задается в стандартной для функциональных языков нотации:
(lambda x (xor (shl1 (and (not (plus x 1)) 1)) 1))
Помимо битовых операторов есть две константы – 0 и 1, тернарный оператор сравнения if0 и хитрый оператор fold, который тоже хорошо знаком функциональным программистам (в некоторых языках он называется reduce и идет в паре с оператором map, MapReduce! :) Для каждого байта из первого аргумента fold вычисляет функцию lambda(x, y), переданную в качестве третьего аргумента, при этом x – это текущий байт, а y – текущее значение аккумулятора. Результат итерации снова записывается в аккумулятор. Начальное значение аккумулятора задает второй аргумент fold. Подробное описание задания можно прочитать на страничке соревнований.
Есть сервер, у которого можно спросить список программ. Для каждой программы известен набор операторов, из которых она состоит, и ее размер (фактически количество операторов в функции). Можно задать произвольное 64-битное число, и сервер ответит, чему равно значение функции для этого аргумента. За раз можно спросить максимум 256 значений, спрашивать можно раз в несколько секунд. Можно передать на сервер текст предполагаемой функции. В ответ сервер либо скажет, что функция угадана верно, либо вернет число, для которого неизвестная функция дает отличный от нашего результат. Результат тоже возвращается.
После того, как мы попросили значения функции, начинает тикать таймер. Если в течение 5 минут мы не угадали программу, они «сгорает», и больше угадывать ее нельзя. Для тренировки можно попросить специальные тренировочные программы, которые не «сгорают».
Brute force
Фактически, задача состоит в следующем: подобрать такую комбинацию из заданных операторов, которая дает правильный результат для определенных значений. Легко сообразить, что комбинаторная сложность перебора быстро улетает в небеса по мере роста размера угадываемой программы. По условиям соревнований максимально возможный размер программы в предлагаемом наборе равен 30, что лежит далеко за пределами возможностей тупого перебора.
Забегая вперед, скажу, что не существует также простого и элегантного решения этой задачи, потому что она является NP-полной. Поэтому тут нужен не тупой, а «умный» перебор. Соответственно, чей перебор будет умнее, тот и победил.
Мы принялись за дело. Леша начал писать тупой перебор, Саша – эвалюатор полученных выражений, а я занялся инфраструктурой: взаимодействие с сервером, работа со списком программ, сабмит решений и прочее.
Язык у нас был Python. В прошлом году у меня были с ним большие проблемы, так как я совсем его не знал. В этом году я твердо решил его освоить. Правда, в силу ленности я так и не почитал заранее какой-нибудь краткий туториал, но компенсировал это усердным поиском по stackoverflow в течение всего контеста.
К исходу первых 24 часов у нас был готов тупой брутфорсер, который успешно решал задачи длиной до 9. Мы прорешали им сколько смогли, чтобы заявиться в Lightning Division. Это отдельное соревнование для тех, кто успел хоть что-то сделать за первые сутки. После чего с чистой совестью легли спать.
Soft force и SMT-solver
На следующий день ребята пытались оптимизировать перебор, отсекать бесполезные ветки поиска, ускорять эвалюатор. Я читал майкрософтовские статейки в поисках идей. Идей было несколько.
Наша задача эквивалента задаче SAT: доказательству того, что для заданной булевой формулы можно подобрать такой набор операндов, что формула будет истинной. Задача SAT NP-полная. Для решения задач, сводимых к SAT, используют специальные программы: SAT-solvers. В нашем случае требуется не просто SAT, а более общий SMT-solver, который умеет решать задачи для разных логических формул, не только булевых. Чтобы воспользоваться готовым SMT-солвером, нужно описать нашу задачу на его языке, что не так просто.
По наводке из статей я скачал бесплатный SMT-солвер Yices и немного поигрался с ним. Когда я попросил его найти функцию, которая при x1 дает y1, а при x2 дает y2, он ничтоже сумняшеся выдал примерно такое:
if x == x1:
return y1
elif x == x2
return x2
Что ж, логично. Теперь ему нужно объяснить, что можно использовать только те операторы, которые заданы, при этом длина программы должна быть такая-то и, возможно, еще какие-то дополнительные ограничения. После этого он должен начать неистово синтезировать нужные нам функции.
Затем я обнаружил более удобный солвер Z3 от Microsoft Research (хе-хе), который, к тому же, имел биндинги для Python. Немного поковырявшись с ним я отвлекся на побочную идею из все тех же статей о подготовке шаблонов, на базе которых SMT-солвер будет искать функцию.
Я начал писать штуку, которая сначала берет набор операторов, из которых должна состоять угадываемая функция, и генерирует все возможные функции из них. Затем она добавляет один оператор из первоначального набора и генерирует все функции для нового набора, в котором один из операторов повторяется дважды, и так далее, пока не достигнет заданной длины функции. Так вот, оказалось, что для угадывания функции длиной, скажем, 10, достаточно сгенерировать функцию длиной 5!
Как так? А вот так. Если посмотреть глазами на тренировочные функции, то в них полно конструкций типа (shl1(shr1 x)), а то и вовсе (or 0 0). То есть угадываемые функции скорее всего сгенерированы случайно и могут быть подвергнуты серьезному упрощению. То есть размер угадываемой программы нужно трактовать не как ее точный размер, а как максимальный. К слову, мы тоже написали мини-сервер, который генерировал случайные функции, для тренировки.
Я рассказал ребятам о своих изысканиях, и Саша вызвался обучить Z3 решать нашу задачу. Мне тоже страшно хотелось поковыряться с SMT-солвером, но, подчиняясь командной игре, я вернулся к своему генератору последовательных решений.
В итоге мой генератор довольно уверенно решал все до размера 15, а иногда удавалось решить и что-то из района 20-25. Все зависит от того, как сильно может быть упрощена неизвестная функция. Саша наконец добил Z3 и синтезировал программы размером 20-25, хотя и не всегда успешно. Надо сказать, что SMT-солвер ожидаемо не стал серебрянной пулей, NP он и в Африке NP. Именно поэтому половина статей посвящена эффективному поиску решений с помощью SMT. Леша мучал перспективную в общем-то идею предгенерации наборов функций, но как-то не довел ее до победного конца.
Последние несколько часов соревнований мы запускали наши солверы на всех доступных машинах, с целью выбить как можно больше очков.
Результаты
В Lightning Division мы набрали 176 очков, это примерно 60-65 место из 150. В основном зачете мы набрали 569 очков, что соответствует 124 месту из 275. Для людей далеких от функционального программирования, математических проблем и командных соревнований это наверное неплохо. В следующем году постараемся снова сделать правильные выводы и выступить еще лучше.