Записи с меткой «icfpc»

ЭВМ/ Синтез функций на ICFPC 2013

15.08.2013

Если кто не в курсе, на днях прошел очередной 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. Для людей далеких от функционального программирования, математических проблем и командных соревнований это наверное неплохо. В следующем году постараемся снова сделать правильные выводы и выступить еще лучше.

ЭВМ/ Первые результаты ICFPC 2012

01.08.2012

Вывесили первый результаты. В блице мы заняли 60 место и вылетели. Кстати, вообще добились хоть какого-то результата в этом зачете всего 82 команды из почти двухсот, остальные показали нули. В основном зачете мы на 65 месте из 190 и проходим в следующий тур. В прошлом году, напомню, мы тоже были 65-ми. Что ж, стабильность – признак мастерства.

ЭВМ/ До начала ICFPC 2012 осталось пара часов!

13.07.2012

В 16 часов по Москве стартует очередной чемпионат по программированию ICFP Programming Contest 2012! Команда Trup 16 в составе трех человек сидит на даче в Подмосковье готовая к бою. О нашем прошлогоднем выступлении можно почитать здесь. Пожелайте нам удачи!

ЭВМ/ Финал ICFPC 2011

20.09.2011

Подвели итоги ICFP Programming Contest 2011, выявили победителей. Но самое главное — опубликовали презентацию от организаторов, очень интересный инсайд. Рекомендую почитать тем, кто осилил мой отчет о нашем участии.

ЭВМ/ Результаты ICFPC 2011

27.06.2011

Мы на 65-ом месте из 199.

ЭВМ/ Лямбда-магия на ICFPC 2011

24.06.2011

Каждый год осенью или в самом конце лета проходит международная конференция по функциональным языкам программирования — ICFP. Чтобы привлечь больше внимания к этому событию, за несколько месяцев до конференции организаторы устраивают соревнование для программистов — ICFP Programming Contest. Организаторы и страна проведения конференции каждый год разные, разные и задания для соревнования. Но все задания разных лет объединяет одно свойство, редкое для спортивного программирования: чрезвычайная необычность и увлекательность. Собственно именно эта черта «зацепила» меня и моих друзей, не участвовавших ни в каких соревнования, наверное, со школьных времен. В Интернете можно найти множество интересных отчетов участников прошлых лет, именно из одного такого отчета мы и узнали о ICFP.

Соревнование длится ровно трое суток. Участвовать могут все, у кого есть доступ к Интернету. Можно участвовать как одному, так и собираться в команды. Понятно, что выгодно собирать команду из людей, живущих в разных часовых поясах, чтобы пока один спит, другой работает. После завершения соревнований подводят предварительные итоги, оглашение окончательных результатов и награждение победителей происходит на самой конференции. В этом году конференцию и соревнование проводит университет Тохоку (Япония).

Не смотря на слово «функциональный» в названии, знание функционального программирования для участия не требуется. Также нет никаких ограничений на используемые языки программирования. Но те, кто хорошо знаком с функциональным программированием, метапрограммированием, DSL и прочими вещами из мира теории программ имеют неоспоримое преимущество, так как задания ICFP Contest всегда так или иначе связаны с этими проблемами. В нашей команде «функциональщиков» не было, писали мы на Python в объектно-императивном стиле, но это не помешало нам показать не самые плохие результаты. (далее…)

ЭВМ/ ICFP Contest 2011 завершен

20.06.2011

Это были незабываемые трое суток. За столь короткий срок я узнал огромное количество новых для себя вещей: что такое лямбда-исчисление, как программировать с помощью комбинаторов и как писать на Python. Мне даже захотелось освоить наконец функциональное программирование. Так что, думаю, свою основную задачу — популяризацию функционального программирования — организаторы выполнили отлично.

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

В течение нескольких дней организаторы проведут турниры между присланными программами и сформируют таблицу результатов. А пока предлагаю прочитать подробный отчет о событиях последних трех суток, увлекательную историю о том, как мы играли в магическую функциональную ролевую игру «Lambda: The Gathering».

ЭВМ/ ICFP’11 уже вот-вот

16.06.2011

Меньше суток осталось до начала соревнований. У нас в итоге получилась команда из трех человек; немного, зато общаться легко. Старт назначен на завтра 00:00 UTC, то есть в 4 утра по Москве. Я в это время буду сладко спать, поэтому начинать придется двум коллегам. Один живет на другом конце планеты, а другой любит работать по ночам.

Думаю, все уже решили разогревочную загадку с книжкой на сайте соревнований. Судя по всему, будем играть в карты. В функциональные карты конечно же. Всем удачи!

ЭВМ/ ICFP Contest 2011 быть!

03.05.2011

Итак, в этом году соревнования программистов ICFPC 2011 пройдет с нуля часов 17-го июня до нуля часов 20 июня по Гринвичу. Поэтому берите отпуск, больничный, просто внезапно исчезайте на трое суток, смазывайте свои боевые текстовые редакторы и компиляторы и готовьтесь.

ЭВМ/ Метасоцсеть

14.03.2011

Я вот и не знал, а, оказывается, в той бесчисленной веренице сервисов, которые наклепал или купил Гугл, есть средство для создания собственной простенькой социальной сети — Friend Connect. А узнал я об этом случайно, зайдя на сайт ICFPC и с удивлением обнаружив, что версия 2011 года хостится на гугловском Blogger и использует этот самый FC.

P.S. Никаких подробностей о ICFP 2011 пока на том сайте нет.

, ,

ЭВМ/ Соревнования

08.10.2010

Я тут смеху ради решил принять участие в яндексовской олимпиаде для сисадминов. Ну а что, тряхну стариной, я ведь когда-то администрировал пару серверов в студенческом общежитии. Первая игра начнется в понедельник в 19:00, так что еще не поздно зарегистрироваться.

А в более глобальных планах — поучаствовать с друзьями в следующем году в ICFP Programming Contest. Это командное соревнование по программированию, приуроченное к ежегодной конференции, посвященной функциональным языкам.  Впрочем на соревнованиях никто не заставляет использовать именно функциональные языки. Но, подозреваю, они лучше подходят для решения предлагаемых задач. Соревнование длится 72 часа; мне кажется, это очень романтично, выключиться на трое суток из привычной жизни, чтобы с головой окунуться в мир головоломок и алгоритмов.

Задания на ICFP очень интересные. Скажем, в 2006 году нужно было ковыряться в древней Unix-подобной системе, работающей в эмуляторе древнего компьютера. Один из живописных отчетов об этом вы, возможно, раньше встречали.

Сейчас для тренировки пытаюсь решать задачи прошлых лет. В частности для уже упоминавшегося задания 2006 года написал эмулятор древнего компьютера и немного поковырялся внутри.

,