![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
"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 бит информации, чтобы понять, какая функция там загадана.( Read more... )
В этом году соревнование ICFPC организовывали в RiSE Group из Microsoft Research, где активно занимаются солверами вроде Z3 и синтезом программ, системами доказательств и верификации, вроде Dafny и Boogie, а также исследовательскими языками вроде F*. Поэтому их задание совершенно не удивило. Сводилось оно к тому, что они загадали множество небольших функций на описанном в условии простеньком языке, и нам надо было отгадать, что это за функции. Каждая такая функция принимает на вход 64-битное целое число, и такое же возвращает. Для каждой загаданной функции можно было попросить их сервер вычислить ее на некотором наборе входных значений, и сервер отдавал результаты. После чего у игрока было 5 минут, чтобы догадаться по этим результатам и свойствам функции (для каждой загаданной функции было описано число и множество операций в ней использованных), что это за функция, и прислать текст догадки. Полного совпадения не требовалось, достаточно было эквивалентной загаданной, но только если их система будет способна понять, что загаданная и присланная функции эквивалентны. Посылать числа на вычисление и догадки можно много раз, но не чаще 5 запросов за каждые 20 секунд, и не более 5 минут между первым запросом и последней догадкой.
В моем часовом поясе соревнование начиналось (и заканчивалось!) в 7 утра, так что начало я благополучно проспал. Почитав утром задание, понял, что это классическая задача для SMT-солверов, но я с ними никогда дела не имел, и сейчас освоить не успею, поэтому буду придумывать что-то сам. Всего разных возможных функций из UInt64 в UInt64 - (264)(264) штук, но возможных функций на том языке заданного размера (по условию там было не более 30 операций) - менее 2100 штук, что для полного перебора все равно дофига, но, теоретически, задавая правильные вопросы серверу, достаточно было получить от него 100 бит информации, чтобы понять, какая функция там загадана.( Read more... )
