![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
Entry tags:
ICFPC '13
"The story so far: As usual, Ginger and I are engaged in our quest to find out what the hell is going on and save humanity from my nemesis, some bastard who is presumably responsible."
В этом году соревнование ICFPC организовывали в RiSE Group из Microsoft Research, где активно занимаются солверами вроде Z3 и синтезом программ, системами доказательств и верификации, вроде Dafny и Boogie, а также исследовательскими языками вроде F*. Поэтому их задание совершенно не удивило. Сводилось оно к тому, что они загадали множество небольших функций на описанном в условии простеньком языке, и нам надо было отгадать, что это за функции. Каждая такая функция принимает на вход 64-битное целое число, и такое же возвращает. Для каждой загаданной функции можно было попросить их сервер вычислить ее на некотором наборе входных значений, и сервер отдавал результаты. После чего у игрока было 5 минут, чтобы догадаться по этим результатам и свойствам функции (для каждой загаданной функции было описано число и множество операций в ней использованных), что это за функция, и прислать текст догадки. Полного совпадения не требовалось, достаточно было эквивалентной загаданной, но только если их система будет способна понять, что загаданная и присланная функции эквивалентны. Посылать числа на вычисление и догадки можно много раз, но не чаще 5 запросов за каждые 20 секунд, и не более 5 минут между первым запросом и последней догадкой.
В моем часовом поясе соревнование начиналось (и заканчивалось!) в 7 утра, так что начало я благополучно проспал. Почитав утром задание, понял, что это классическая задача для SMT-солверов, но я с ними никогда дела не имел, и сейчас освоить не успею, поэтому буду придумывать что-то сам. Всего разных возможных функций из UInt64 в UInt64 - (264)(264) штук, но возможных функций на том языке заданного размера (по условию там было не более 30 операций) - менее 2100 штук, что для полного перебора все равно дофига, но, теоретически, задавая правильные вопросы серверу, достаточно было получить от него 100 бит информации, чтобы понять, какая функция там загадана. Большую часть первого дня я провел в раздумьях, но так ничего особо умного не придумал. Тогда решил сделать наивный переборщик, использовать его в lightning round (первые 24 часа), а потом уже придумать что-то поинтересней. Переборщик перебирает все возможные программы заданного размера с учетом множества операций, используемых в данной функции, каждую выполняет на наборе случайных чисел и сравнивает с результатами выполнения на тех же числах загаданной программы на сервере, пока не найдет совпадающие. Заметил, что все двуместные операции в их языке (and, or, xor, plus) коммутативны, поэтому нет нужды перебирать все возможные их операнды: достаточно перебрать лишь те, где размер первого больше размера второго, а если их сумма должна быть четной, то отдельно для случая равных размеров перебирать неповторяющиеся пары: если множество возможных значений одного операнда это [a,b,c], то нас интересуют не 9 вариантов, а только 6 - [(a,a), (b,a), (b,b), (c,a), (c,b), (c,c)]. Впервые за много лет в качестве языка реализации я взял не Окамл. И подозреваю, что это было ошибкой. Для реализации наивного переборщика я взял хаскель, на котором раньше почти не писал, но который показался наиболее удобным для выражения идей. Сделал переборщик, решил им пару задач, стало ясно, что нужно процесс запроса значений и отсылки ответов автоматизировать. С HTTP на хаскеле я последний раз имел дела года два назад, с JSON еще ни разу не имел, но вспомнил слово Aeson, быстренько научился им пользоваться, отличная штука. В итоге автоматический решатель задач у меня был готов где-то в T+23, за час до окончания лайтнинг раунда. И тут я уперся в ограничение по частоте запросов к серверу. Поэтому в T+23 у меня было около 0 очков, в T+25 их стало 384, но в момент T+24 было всего 248. Решив почти четыре сотни задач, мой солвер дошел до задач размером 14, где внезапно объем потребляемой памяти резко вырос и перестал умещаться в 2 гига, положенные 32-битному процессу. На улице давно рассвело, было 8 утра, и я пошел спать.
На второй день я решил, что аккуратно разрулить вопрос с ленивыми списками и потреблением памяти на хаскеле у меня вряд ли получится из-за малого опыта, но есть же и энергичные языки со схожими по выразительности средствами и гарантиями по памяти. Тогда я взялся переписать переборщик на D, где есть волшебные range'ы - последовательности, которые можно map'ить, chain'ить, делать декартово произведение и т.п., и все это с сохранением свойств, вроде известной длины или способности сохраняться. Вместо
...
Получилось
Имея работающий код на хаскеле, перевести его на D довольно просто. А у D'шных рэнджей есть ключевое свойство: в отличие от ленивых списков, которые легко ненароком развернуть в памяти вместо потребления по мере генерации, рэнджи гарантированно не хранят в памяти более одного значения. Поэтому новому переборщику на D хватало 10 мегов памяти на любой задаче. Скорость я особо мерять не стал, т.к. на глаз она выглядела неплохой, а главное, перебощик на D стал щелкать как орешки те задачи, где хаскельный падал с переполнением памяти. Несмотря на относительную простоту перевода, к методу выражения алгоритма на ренджах следовало приноровиться, и на перевод ушел весь второй день. Одна из основных неприятностей D'шных рэнджей: операции над ними меняют тип - нельзя просто написать
condition ? r : chain(r,r)
или
if (use_if) return chain(r, ifs);
else return r;
т.к. комбинаторы вроде chain, map и т.п. каждый раз создают новый безымянный тип с нужным интерфейсом, но новой реализацией. Приходится использовать обертку inputRangeObject, превращающую этот новый тип в объект заданного интерфейса, такой уже можно вернуть из функции в разных местах.
"The story so far: In my continuing quest to find out just who is behind it all, and by 'all' I do mean ALL, Ginger and I have been invited to an evening at Her Majesty's pleasure, but we can't get there because we're in prison."
На третий день я надеялся придумать что-нибудь более умное, чем такой перебор, да ничего толком не придумал, прозанимался большую часть времени небольшими улучшениями. При этом с сервером по-прежнему общалась моя программа на хаскеле, а для поиска решений она запускала переборщик на D. Задачи были отсортированы по возрастанию размера, и разделены между двумя процессами: один решал четные задачи, другой нечетные, так два процесса параллельно потихоньку запрашивали задачи и решали их по мере сил. Сил, однако, хватало все реже по мере роста размера задач. Обнаружил, что очень многие "большие" задачи решаются программами значительно меньшего размера. Сделал простой хак: для задач размером больше 13 сперва делалась попытка найти решение размером 13, а потом только указанным в условии размером. Добавил ограничение по таймеру. Процесс щелкания задачек шел стабильно, поэтому придумывать что-то радикально новое особой мотивации не было. За несколько часов до конца родилась мысль: генерить не все возможные программы нужного размера и состава, а лишь те, что на входе 0xFF...FF дают тот же ответ, что и сервер. Для этого при генерации программы сверху передавались два значения: target_value и target_mask, генериться должны лишь такие программы, которые на 0xFF..FF дадут result такой, что result & target_mask == target_value. Тогда унарные операции меняют target_value и target_mask согласно своей сути, а бинарные операции либо тоже лишь меняют эту пару (для and и or), либо перебирают все значения одного операнда, вычисляют подходящее значение для target_value второго операнда, и варианты второго генерят уже с таким таргетом. Что делать с циклами (fold'ом) в этой схеме у меня в тот момент не было четкого понимания, но решил, что хотя бы на безфолдовых задачах попробую. Однако реализовать эту схему так и не успел: код стал слишком сложным для DMD и тот стал чудить - то сгенерит явную чепуху, то даже сам упадет при компиляции. Ибо комбинаторы рэнджей принимают функции-аргументы в виде шаблонных параметров, там задействуется всякая шаблонная метапрограммная магея, и результат порой оказывается не по зубам бедному написанному на плюсах компилятору. Сыроват он еще, к сожалению. Возможно, когда фронтенд перепишут на D, станет поумнее и постабильнее. Так я и приехал к финишу на паре работающих довольно простых переборщиков, которые все чаще выдавали таймауты, но между ними продолжали стабильно угадывать некоторые задачи даже довольно большого размера. 400 строк на хаскеле, 300 на D. К завершению третьих суток я набрал лишь 850 очков, что приведет на какое-то место между 75 и 100 позицией. А писал бы на окамле, избежал бы и пожирания памяти ленивыми списками, и багов компилятора, возможно, и результат был бы получше.
"How did my nemesis shrink himself? When will Ginger find a better method for discovering waterproof dwarfs? Why don't kids parties have real booze any more, like they did when I was a dwarf? Find out in the next enthralling installment of the surprising adventures of Sir Digby Chicken Caesar."
В этом году соревнование ICFPC организовывали в RiSE Group из Microsoft Research, где активно занимаются солверами вроде Z3 и синтезом программ, системами доказательств и верификации, вроде Dafny и Boogie, а также исследовательскими языками вроде F*. Поэтому их задание совершенно не удивило. Сводилось оно к тому, что они загадали множество небольших функций на описанном в условии простеньком языке, и нам надо было отгадать, что это за функции. Каждая такая функция принимает на вход 64-битное целое число, и такое же возвращает. Для каждой загаданной функции можно было попросить их сервер вычислить ее на некотором наборе входных значений, и сервер отдавал результаты. После чего у игрока было 5 минут, чтобы догадаться по этим результатам и свойствам функции (для каждой загаданной функции было описано число и множество операций в ней использованных), что это за функция, и прислать текст догадки. Полного совпадения не требовалось, достаточно было эквивалентной загаданной, но только если их система будет способна понять, что загаданная и присланная функции эквивалентны. Посылать числа на вычисление и догадки можно много раз, но не чаще 5 запросов за каждые 20 секунд, и не более 5 минут между первым запросом и последней догадкой.
В моем часовом поясе соревнование начиналось (и заканчивалось!) в 7 утра, так что начало я благополучно проспал. Почитав утром задание, понял, что это классическая задача для SMT-солверов, но я с ними никогда дела не имел, и сейчас освоить не успею, поэтому буду придумывать что-то сам. Всего разных возможных функций из UInt64 в UInt64 - (264)(264) штук, но возможных функций на том языке заданного размера (по условию там было не более 30 операций) - менее 2100 штук, что для полного перебора все равно дофига, но, теоретически, задавая правильные вопросы серверу, достаточно было получить от него 100 бит информации, чтобы понять, какая функция там загадана. Большую часть первого дня я провел в раздумьях, но так ничего особо умного не придумал. Тогда решил сделать наивный переборщик, использовать его в lightning round (первые 24 часа), а потом уже придумать что-то поинтересней. Переборщик перебирает все возможные программы заданного размера с учетом множества операций, используемых в данной функции, каждую выполняет на наборе случайных чисел и сравнивает с результатами выполнения на тех же числах загаданной программы на сервере, пока не найдет совпадающие. Заметил, что все двуместные операции в их языке (and, or, xor, plus) коммутативны, поэтому нет нужды перебирать все возможные их операнды: достаточно перебрать лишь те, где размер первого больше размера второго, а если их сумма должна быть четной, то отдельно для случая равных размеров перебирать неповторяющиеся пары: если множество возможных значений одного операнда это [a,b,c], то нас интересуют не 9 вариантов, а только 6 - [(a,a), (b,a), (b,b), (c,a), (c,b), (c,c)]. Впервые за много лет в качестве языка реализации я взял не Окамл. И подозреваю, что это было ошибкой. Для реализации наивного переборщика я взял хаскель, на котором раньше почти не писал, но который показался наиболее удобным для выражения идей. Сделал переборщик, решил им пару задач, стало ясно, что нужно процесс запроса значений и отсылки ответов автоматизировать. С HTTP на хаскеле я последний раз имел дела года два назад, с JSON еще ни разу не имел, но вспомнил слово Aeson, быстренько научился им пользоваться, отличная штука. В итоге автоматический решатель задач у меня был готов где-то в T+23, за час до окончания лайтнинг раунда. И тут я уперся в ограничение по частоте запросов к серверу. Поэтому в T+23 у меня было около 0 очков, в T+25 их стало 384, но в момент T+24 было всего 248. Решив почти четыре сотни задач, мой солвер дошел до задач размером 14, где внезапно объем потребляемой памяти резко вырос и перестал умещаться в 2 гига, положенные 32-битному процессу. На улице давно рассвело, было 8 утра, и я пошел спать.
На второй день я решил, что аккуратно разрулить вопрос с ленивыми списками и потреблением памяти на хаскеле у меня вряд ли получится из-за малого опыта, но есть же и энергичные языки со схожими по выразительности средствами и гарантиями по памяти. Тогда я взялся переписать переборщик на D, где есть волшебные range'ы - последовательности, которые можно map'ить, chain'ить, делать декартово произведение и т.п., и все это с сохранением свойств, вроде известной длины или способности сохраняться. Вместо
triangle :: [a] -> [(a,a)]
triangle xs = [(a,b) | (a,is) <- zip xs (tail $ inits xs), b <- is]
boperands :: Spectrum -> Char -> [Exp String] -> Int -> [(Exp String, Exp String)]
boperands sp v env n
| n .&. 1 == 1 = [(e1,e2) | k <- [1.. n `div` 2], e1 <- gen sp v env k, e2 <- gen sp v env (n-k) ]
| otherwise = [(e1,e2) | k <- [1.. n `div` 2 - 1], e1 <- gen sp v env k, e2 <- gen sp v env (n-k) ] ++
(triangle $ gen sp v env (n `div` 2))
gen :: Spectrum -> Char -> [Exp String] -> Int -> [Exp String]
gen sp v env 1 = [Zero, One] ++ env
gen sp v env 2 = [Uop op exp | op <- allowed_ops1 sp, exp <- gen sp v env 1]
gen sp v env 3 = boplist ++ uoplist where
boplist = [Bop op e1 e2 | op <- allowed_ops2 sp, (e1,e2) <- triangle $ gen sp v env 1]
uoplist = [Uop op e | op <- allowed_ops1 sp, e <- gen sp v env 2]...
Получилось
Exp[][] size1exps; //filled once on start
Exp mkUop(Tuple!(Op1, Exp) oe) { return cast(Exp) new Uop(oe[0], oe[1]); }
Exp mkBop(Tuple!(Op2, Tuple!(Exp, Exp)) oee) { return cast(Exp) new Bop(oee[0], oee[1][0], oee[1][1]); }
alias fwd = inputRangeObject;
auto triangle(R)(R r)
{
return zip(r.save, sequence!"n").map!(en => r.take(en[1]+1).map!(e => tuple(en[0], e))).joiner;
}
ForwardRange!Exp gen(Spectrum sp, int v, int n)
{
if (n==1) return size1exps[v].fwd;
if (n==2) return cartesianProduct(sp.ops1, gen(sp, v, 1)).map!mkUop.fwd;
if (n==3) {
auto uops = cartesianProduct(sp.ops1, gen(sp, v, 2)).map!mkUop;
auto bops = cartesianProduct(sp.ops2, triangle(gen(sp, v, 1)))
.map!(oee => cast(Exp) new Bop(oee[0], oee[1][0], oee[1][1]));
return chain(uops, bops).fwd;
}
...
Имея работающий код на хаскеле, перевести его на D довольно просто. А у D'шных рэнджей есть ключевое свойство: в отличие от ленивых списков, которые легко ненароком развернуть в памяти вместо потребления по мере генерации, рэнджи гарантированно не хранят в памяти более одного значения. Поэтому новому переборщику на D хватало 10 мегов памяти на любой задаче. Скорость я особо мерять не стал, т.к. на глаз она выглядела неплохой, а главное, перебощик на D стал щелкать как орешки те задачи, где хаскельный падал с переполнением памяти. Несмотря на относительную простоту перевода, к методу выражения алгоритма на ренджах следовало приноровиться, и на перевод ушел весь второй день. Одна из основных неприятностей D'шных рэнджей: операции над ними меняют тип - нельзя просто написать
condition ? r : chain(r,r)
или
if (use_if) return chain(r, ifs);
else return r;
т.к. комбинаторы вроде chain, map и т.п. каждый раз создают новый безымянный тип с нужным интерфейсом, но новой реализацией. Приходится использовать обертку inputRangeObject, превращающую этот новый тип в объект заданного интерфейса, такой уже можно вернуть из функции в разных местах.
"The story so far: In my continuing quest to find out just who is behind it all, and by 'all' I do mean ALL, Ginger and I have been invited to an evening at Her Majesty's pleasure, but we can't get there because we're in prison."
На третий день я надеялся придумать что-нибудь более умное, чем такой перебор, да ничего толком не придумал, прозанимался большую часть времени небольшими улучшениями. При этом с сервером по-прежнему общалась моя программа на хаскеле, а для поиска решений она запускала переборщик на D. Задачи были отсортированы по возрастанию размера, и разделены между двумя процессами: один решал четные задачи, другой нечетные, так два процесса параллельно потихоньку запрашивали задачи и решали их по мере сил. Сил, однако, хватало все реже по мере роста размера задач. Обнаружил, что очень многие "большие" задачи решаются программами значительно меньшего размера. Сделал простой хак: для задач размером больше 13 сперва делалась попытка найти решение размером 13, а потом только указанным в условии размером. Добавил ограничение по таймеру. Процесс щелкания задачек шел стабильно, поэтому придумывать что-то радикально новое особой мотивации не было. За несколько часов до конца родилась мысль: генерить не все возможные программы нужного размера и состава, а лишь те, что на входе 0xFF...FF дают тот же ответ, что и сервер. Для этого при генерации программы сверху передавались два значения: target_value и target_mask, генериться должны лишь такие программы, которые на 0xFF..FF дадут result такой, что result & target_mask == target_value. Тогда унарные операции меняют target_value и target_mask согласно своей сути, а бинарные операции либо тоже лишь меняют эту пару (для and и or), либо перебирают все значения одного операнда, вычисляют подходящее значение для target_value второго операнда, и варианты второго генерят уже с таким таргетом. Что делать с циклами (fold'ом) в этой схеме у меня в тот момент не было четкого понимания, но решил, что хотя бы на безфолдовых задачах попробую. Однако реализовать эту схему так и не успел: код стал слишком сложным для DMD и тот стал чудить - то сгенерит явную чепуху, то даже сам упадет при компиляции. Ибо комбинаторы рэнджей принимают функции-аргументы в виде шаблонных параметров, там задействуется всякая шаблонная метапрограммная магея, и результат порой оказывается не по зубам бедному написанному на плюсах компилятору. Сыроват он еще, к сожалению. Возможно, когда фронтенд перепишут на D, станет поумнее и постабильнее. Так я и приехал к финишу на паре работающих довольно простых переборщиков, которые все чаще выдавали таймауты, но между ними продолжали стабильно угадывать некоторые задачи даже довольно большого размера. 400 строк на хаскеле, 300 на D. К завершению третьих суток я набрал лишь 850 очков, что приведет на какое-то место между 75 и 100 позицией. А писал бы на окамле, избежал бы и пожирания памяти ленивыми списками, и багов компилятора, возможно, и результат был бы получше.
"How did my nemesis shrink himself? When will Ginger find a better method for discovering waterproof dwarfs? Why don't kids parties have real booze any more, like they did when I was a dwarf? Find out in the next enthralling installment of the surprising adventures of Sir Digby Chicken Caesar."
no subject
no subject