dastapov: (Default)
[personal profile] dastapov
Этот пост - о том, как мы строили машины, фабрики и гнали бензин на ICFPC-2010.

Кто еще не знает, что это такое - может пройти в сад почитать мой отчет об ICFPC-2006. Всех же остальных я не буду мучать долгими вступлениями и сразу перейду к сути.

Задание


Если взять официальный текс задания и убрать всю литературную обработку, то суть его сводилась к следующем:
  1. В рамках придуманной авторами задачи есть две основных сущности - машины (cars) и топливо (fuel). 
  2. Топливо - это набор из одной или нескольких квадратных матриц одинакового размера.
  3. Машина - это набор из одного или нескольких (до сотен) неравенств вида ABABAAABABACBABA - BCBDBDBABABA > 0, где A,B,C,D - это матрицы.
  4. Игроки могут придумывать свои машины (то есть, придумывать свои системы неравенств), либо же придумывать топливо к чужим машинам (то есть, подбирать набор матриц, удовлетворяющих условиям чужих неравенств)
  5. Тот, кто "заправил" машину (свою или чужую - не важно), будет регулярно получать за это "дивиденды" до самого конца соревнования. Чем раньше ты "заправил" машину, и чем компактнее твое "топливо", тем больше условных "денег" ты получишь.
  6. Победит тот, кто заработает больше всех условных денег к концу соревнования.
Казалось бы, стратегия понятна - решай чужие неравенства в каком-то Matlab-е или Mathematica-е, и придумывай свои неравенства позаковыристей.

Однако, все было не так просто.

Во-первых, описания машин давались в виде цепочек тернарных битов (тритов) 0, 1 и 2. Пример: 12222002000010010100222200200000101010

Было известно только то, что этот способ кодировки способен представить списки/векторы произвольной длины и числа произвольной размерности, а также списки списков и так далее до любого уровня вложенности. Как именно представляются данные о машине (это вектор списка списков чисел, или список векторов, или ...?), как кодируются числа, и как кодируются более сложные структуры - все это участникам предлагалось узнать самостоятельно. Кто узнавал - получал возможность декодировать описания чужих машин, и кодировать описания своих машин и своего топлива.

Но это было еще не все: организаторы не принимали в качестве решения топливо, закодированное в цепочку тритов. Надо было сделать схему (circuit) "фабрики по производству топлива" из блоков (gates), в которую организаторы подавали какую-то (неизвестную) цепочку тритов, а на выходе должна была получится цепочка тритов, кодирующих ваше топливо.

Но и это было еще не все! Внутреннее устройство гейтов было неизвестно. Организаторы только сообщали, что у них - два входа и два выхода, и к каждому входу и выходу может быть присоединен ровно один провод. Гейты можно было соединять проводами так, чтобы получалась схема с одним незамкнутым входом и одним выходом, и в таком виде подавать организаторам.

Как вы догадались, и это было не все. Схемы из гейтов надо было записывать в специальном синтаксисе. Который никак не описывался - приводился его пример, и всё:

19L:
12R13R0#1R12R,
14R0L0#4R9L,
9R10R0#3L8L,
2L17R0#5L9R,
15R1L0#10R13R,
3L18R0#6L15L,
5L11R0#13L12L,
19R16R0#11R8R,
2R7R0#11L10L,
1R3R0#18L2L,
8R4L0#16L2R,
8L7L0#15R6R,
6R0R0#14L0L,
6L4R0#14R0R,
12L13L0#17L1L,
5R11L0#16R4L,
10L15L0#17R7R,
14L16L0#18R3R,
9L17L0#19R5R,
X18L0#X7L:
19L


Оставалась одна небольшая деталь: прежде чем получить возможность полноценно участвовать в соревновании, надо было сделать и прислать организаторам схему-фабрику, выдающую 17-тритный ключ. Что такое "ключ"? Это то, что выдаст схема из примера выше, если в нее скормить последовательность [0,2,2,2,2,2,2,0,2,1,0,1,1,0,0,1,1]. А что будут подавать на вход вашей схеме организаторы? Этого вам никто не скажет ...

Вот и всё задание. По объему reverse engineering-а оно было похоже на задание 2007-ой года.

UPD: вот еще одно описание задачи своими словами, даже более прикольное.

Мы читали задание час

Мы - это ваш покорный слуга (Киев), [livejournal.com profile] sorhed , [livejournal.com profile] akuklev (оба - Израиль), [livejournal.com profile] gabriel_irk (Москва) и [livejournal.com profile] kosiakk (Цюрих), выступающие командой под названием Futamura Rejection. Потратив час на чтение, мы стали записывать свои мысли в http://sync.in, а организаторы в это время ... поднимали сервер.

Сначала упала регистрация новых команд. Потом пропала возможность залогинится (server timeout). Потом сервер стал выдавать "503 Service Temporary Unavailable" и болтался в таком виде почти три часа. Не имея возможности экспериментировать со схемами и гейтами, мы набросали План Атаки:


Первоочередной задачей было получить ключ. Для этого надо было узнать, как же работают гейты, и научится строить свои схемы, выдающие нужные нам последовательности тритов.

3.5 часа после начала соревнования - синтаксис фабрик и входной поток

Заработал сервер соревнования. Мы получили возможность экспериментировать и разобрались с синтаксисом описания схем. Например, строчка "5R11L0#16R4L" парсилась как "(5R)(11L)0#(16R)(4L)" и обозначала, что на входы этом гейту подаются сигналы с правого выхода гейта номер 5 и левого выхода гейта номер 11, а выходы, соответственно, уходят в гейты 16 и 4. Строчка же "(X)(18L)0#(X)(7L)" обозначала, что у этого гейта один вход и один выход соединяются с "внешним миром" и используются для чтения входного потока тритов и выдачи результата.  Эта же информация продублирована так: до описания гейтов указано, куда присоединен вход ("19L:"), а после - куда присоединен выход (":19L").

Достаточно быстро из perl и graphviz был сделан скрипт, рисующий схемы в более удобоваримом виде, который рисовал схему из условия вот так

Мы долго и безуспешно пытались построить схему, выдающую свой собственный вход, но без понимания принципа работы гейтов это было практически невозможно.

Лишь спустя 7 часов после начала соревнования кто-то на IRC-канале #icfp-contest проговорился о том, что простейший circuit имеет в длину четыре символа, и мы догадались вбить "X::X" и получить долгожданный входной поток, используемый организаторами.

8 часов после начала соревнования - брутфорс функции гейтов на Scala

Еще до получения входного потока у нас была готова реализация "исполнителя фабрик/схем" (на Scala), в которую надо было только добавить описание функции, реализованной в гейте. Из нее достаточно быстро был сделан брутфорсер, подбирающий зависимость выходов гейта от его входов. В качестве эталонного образца использовалась информация  о том, как ведет себя засылаемая организаторам простейшая схема из одного гейта.

Параллельно с этим мы открыли общий документ в google docs и стали там рисовать простые схемы из одного-двух гейтов, скармливать их на сайт соревнования, и медитировать над получающимися результатами:


Зная входную последовательность, можно было, сличая выход от разных схем, потихоньку узнавать, какие выходы будут у гейтов на разных входных сигналах. Из схемы 2 можно было увидеть, что входы (0, 0) преобразуются в (0, ?), а из схемы 2.5 получить (0,0)->(?,2). Вместе это давало (0,0)->(0,2). Мы, кажется, все без исключения вооружились бумагой и ручкой и стали вручную выписывать получающиеся таким образом сведения.

9 часов после начала соревнования - брутфорс функции гейтов на Haskell :)

Через пол-часа я понял, что путаюсь в цифрах и у меня постоянно возникают какие-то несоответствия в записях. Я набросал быструю реализацию гейта на Haskell и стал проверять на ней свои записи:

circuit2 = outp
  where
    -- gate is  (li,ri) --> (lo,ro)
    li = inp
    outp = lo
    ri = delay ro
    (lo,ro) = unzip $ zipWith gateF li ri

delay :: [Int] -> [Int]
delay trits = (0:trits)

gate li ri = (lo,ro)
  where
    (lo,ro) = unzip $ zipWith gateF li ri

gateF 0 0 = (0,2)
gateF 0 1 = (2,undefined)
gateF 0 2 = (undefined,2)
gateF 1 0 = (1,undefined)
gateF 1 1 = (undefined,undefined)
gateF 1 2 = (2,undefined)
gateF 2 0 = (undefined,2)
gateF 2 1 = (undefined,1) 
gateF 2 2 = (0,undefine)


Когда количество "undefined" уменьшилось до четырех, я решил перебрать оставшиеся варианты программно. Увы, ни одна из комбинаций не подошла. К этому же моменту завершился брутфорс программой на Scala, которая ... тоже не нашла ни одного варианта. Можно было бы начать подозревать, что внутри у гейта есть какое-то хранимое состояние, или другие проявления недетерминизма, но, памятуя о том, сколько ошибок я уже допустил при подборе чисел на бумаге, я решил перебрать все возможные варианты зависимостей выходов от входов "с нуля".

Через пол-часа после запуска и 11.5 часов после начала соревнования моя брутфорсилка нашла единственный подходящий вариант таблицы переходов. Так закончился первый условный день.

День второй - строим фабрику, дающую префикс, и кодировки

Утром второго дня кто-то в IRC проговорился, что фабрика, выдающая на выходе ожидаемый организаторами "the key", может быть построена из шести гейтов. Поэтому с самого утра я засел писать брутфорсилку всех возможных схем из N гейтов, которые выдают заданный результат при известном входном потоке.

В это время мои коллеги в Израиле нарисовали граф всех возможных переходов между от входов к выходам в одном гейте и нашли там цикл:

      20                      10
      v                       v
01 -> 22 -> 00 -> 02 -> 12 -> 21 ->11
             ^_____________________|


Если внимательно посмотреть на цикл, то можно заметить, что среди левых и правых выходов в нем встречаются все возможные триты - и 0, и 1, и 2.  Это навело их на мысль, что можно сделать схему из гейтов, которые каким-то образом "гуляют" по состояниям из этого цикла, а с одного из их выходов мы снимаем нужную нам последовательность тритов. Вооруженные этой общей идеей, они пошли рисовать возможные схемы на бумажке.

В 11:00 у меня был готов брутфорсер, который перебирал все возможные схемы соединения N гейтов 2N+1 проводом, и вычислял, какой выход даст схема на входной последовательности, используемой организаторами.

Первая реализация была сделана фигово, и для перебора схемы из N гейтов проверяла ((2n+1)!)2 комбинаций, что для N=6 составляет 229442532802560000 :) Впрочем, мы довольно быстро заметили, что перебор идет как-то медленно, баг в моей голове был выловлен, программа переписана, и сложность уменьшилась до (2N+1)!

В это время наши конкуренты уже занимались анализом способа кодирования машин. Мы же были лишены такой возможности до тех пор, пока брутфорс не построит нам схему, выдающую "the key".

Пока брутфорс грел CPU, akuklev и sorhed нашли способ строить из 6 гейтов схемы, которые выдают на выходе только нули или только единицы, независимо от того, что подается им на вход. Возникла идея сделать из них схему, которая выдает то, что нам нужно - достаточно перед каждым таким генератором ставит "замедлитель", воторый выдает сначала какую-то константу в течении M ходов, а затем - то, что подавалось ему на вход. Правда, схема выглядела избыточной - для кодирования сообщения из M символов понадобилось бы как минимум (1+2+....+M)+M*6 гейтов, а на IRC уже кто-то говорил о том, что знает способ кодирования M символов 3*M гейтами.

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

В 15:00 брутфорсилка наконец выдала целых два варианта схемы из шести гейтов, генерирующей вожделенный "ключ":


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

В этот момент мы были на 76 месте.

Немного шары

Спустя два часа, когда мои идеи о том, как соотносить строчки вида "220000000" с сообщениями "Car must contain at least one Main reaction chamber     Ja. sections must be properly connected this car is not minimal." (стилистика и орфография оригинала соблюдены), я пошел в инет смотреть, не пишет ли уже кто-то что-то интересное про текущее соревнование.

Мое любопытство было вознаграждено находкой http://github.com/cail/icfpc2010-tbd - публичного репозитория команды TBD на github :) Решив, что в борьбе все средства хороши, мы стянули оттуда два скрипта на питоне для заливки топлива и машин, посмотрели, что команда использует для создания фабрик SAT solver, решили, что нам с ними не по пути, и в дальнейшем в чужой код не лазили.

Кодировки

В это время akuklev и akosenkov занимались, кажется, математикой преобразования "топлива" в "машине", и пытались отыскать способ решения неравенств, закодированных в машине. Все остальные грызли гранит encoding-а.

В какой-то момент, получив сообщение "In the car, tank 2 is not properly connected to itself" я стал менять по одному символу и довольно быстро получил "In the car, tank 3 is not properly connected to itself". Ага! Похоже, можно расколоть способ кодирования чисел, а потом уже разобраться со всем, что останется.

Однако, мой энтузиазм быстро иссяк. Получить "In the car, tank 4 is not properly connected to itself" никак не удавалось. Я стал смотреть на то, как выглядит кодировки машин, заливаемых другими командами (а такие уже были!) и крутить тритики в них.

К моему большому удивлению, строчка "22011200000" давала "In the car, tank 3 is not properly connected to itself", а строчка "112200000" - "In the car, tank 4 is not properly connected to itself". Как говорится, "make me unsee it".

Впрочем, достаточно быстро было найдено, что, похоже:
010 = 0
0110 = 1
0111 = 2
0112 = 3
1122000 = 4
1122001 = 5


Походив еще некоторое время вокруг да около, я пошел в Jabber сравнивать записи с jabber-ru (Алексеем Щепиным). В результате схема была уточнена до:
010 = 0
0110 = 1
0111 = 2
0112 = 3
1220xx = xx + 4
12210xxx = xxx + 13
12211xxxx = xxxx + 40
12212xxxxx = xxxxx + 121

Спустя еще 2 часа кто-то на IRC сказал: "the smallest car is 122000010 - think about how that car would look like". Самая маленькая машина, удовлетворяющая всем условиям - это "AA - A > 0" или "A - AA > 0". Объединив этот хинт с нашими текущими знаниями, мы продолбались еще буквально два часа, и в конце концов декодировали эту простейшую машину.

Выяснилось, что всего в кодировании используются два типа данных - числа и списки. Списки кодируются так:
  • 0 - пустой список
  • 1 - список из одного элемента (сразу за "1" идет этот элемент)
  • 22 - список из двух или более элементов. За "22" идет число, равное "длина списка - 2", затем - указанное кол-во элементов без всяких разделителей
Числа кодировались сходным образом:
  • 0 - это ноль
  • 1x  - это x+1
  • 22<length><trits> - это (fromBase3 trits) + (fromBase3 "111...11111"), где единиц всего (length)
Таким образом, "122000010" парсится как  "1(22(0)((0),(0)),0,1(0))", и декодируется как "([0,0],0,[0])". То есть, машина - это список камер, каждая камера - это просто три элемента подряд. Сначала список, кодирующий верхнюю трубу, затем число-признак того, Main эта камера или Auxillary, затем - список, кодирующий нижнюю трубу.

Ура! Наконец-то мы получили возможность кодировать топливо для чужих машин, и кодировать дизайны собственных машин.

Конечно, для начала нам все еще не хватало способа генерировать фабрики/схемы, выдающие на выходе нужную нам последовательность тритов. Поэтому я и gabriel-irk стали писать encoder-decoder для машин и топлива, а все остальные занялись поиском способа построения фабрик.

Large Trit Collider

Я не знаю точно, как именно продвигалась в этот момент работа у других, т.к. был занят борьбой с багами в encoder-е чисел. Покажу вам всего одну картинку из рабочего процесса:


Цитата: "Я всё алгоритм для циклов пишу. Много бумажной работы подобрать в графе именно те циклы, которые будут выдавать что надо. Когда я это сделаю, реализация будет тривиальная. Там будет мап, который нужно будет с перестановкой фолдлить к последовательности и мы получим устройство нашего цикла, который это выдаёт.". Как видите, построить генератор фабрик было проще простого :)

После Большого Тритового Коллайдера была, кажется, идея собирать фабрику из слоев по три гейта. На вход самых верхних подавать "00,11,22", а затем перестановками проводов между слоями делать так, чтобы на одном (самом левом) выходе каждого слоя выдавался нужный нам трит ...

В этот момент я дописал декодер и энкодер и пошел спать. Все остальные еще мучали гейты и пытались решать задачу подбора топлива в Mathematica.

День третий - "пошла мазута!"

В ожидании момента, когда же уже можно будет наконец что-то засылать организаторам, я начал третий день с того, что написал скрипты для автоматического производства решений. Эти скрипты:
  • сливали с сайта данных о всех новых машинах
  • декодировали их
  • запускали бы решатель-подбиратель топлива (которого у нас еще не было)
  • кодировали топливо
  • генерировали бы фабрику, которая выдает закодированную строку (чего у нас тоже еще не было)
  • заливали результат на сайт соревнования
Затем я помогал другим: писал декодер машин в формат, пригодный для скармливания в Matlab и Mathematica. Писал утилиту, которая может склеивать несколько схем "нос в хвост", перенумеровывая гейты и провода.

После этого, в ожидании нормальой решалки топлива, я набросал еще одну тупую брутфорсилку, которая пробовала подставить в неравенства, закодированные в машине, все возможные комбинации матриц 1x1 от [1] до [8], и сохраняла первый подошедший вариант.

К моему удивлению, эта брутфорсилка бодро решила около 200 чужих машин и сказала: "Давайте еще!". Брутфорсилка была доработана так, чтобы выбирать объем перебора в зависимостри от размеров неравенств, и скрипт по автоматическому выкачиванию и решению был поставлен на "боевое дежурство"

К 15:00 мои коллеги решили задачу построения Большого Тритового Коллайдера, и я стал помогать им ее кодировать. Спустя час мы ее закодировали. Спустя еще три часа стало понятно, что эта идея - не работающая :(

К этому моменту у нас уже было 440 решенных "топлив", которые надо было бы заливать и получать "дивиденды".

"Бегущая строка"

Еще спустя час появилась новая идея: "Нам нужно три блока гейтов P0, P1 и P2 о одном входе и выходе. Независимо от входа на выходов они должны на первом шаге выдавать 0, 1 или 2 соответственно, а затем просто повторять то, что им дают на вход. Ставя такие блоки в столбик, мы выведем любую последовательность"

Через час был найден способ построить P0, P1 и P2 из трех гейтов каждый. Еще через час я реализовал склеивалку их в нужном порядке. Еще через час я реализовал склеивалку без багов :)

В 22:00 у нас, наконец, появился способ кодировать N тритов фабрикой из N*3 гейтов.

Ура! Ну сейчас мы зальем все наше топливо, и ворвемся в группу лидеров!

И тут у организаторов под нагрузкой лег сервер.

Поднялся. И снова лег.

И еще раз.

И еще раз.

Все остальные занимались поиском способа более эффективно вести поиск подходящего топлива, в том числе - и матричного. А я занимался автоматизацией заливки решений организаторам.

В конце-концов ближе к полночи сайт поднялся, заливалка заработала, и я пошел спать. К этому момент мы зааплоадили 393 решения "топлива" для чужих "машин".

День четвертый - "всенощная" и гонки за лидером

Утром я обнаружил, что почти все мои коллеги организовали "всенощную", написали утилиту для кодирования машин (которая выполняла подставновки и перестановки труб и камер в поисках самого компактного варианта кодирования) и до самого утра занимались дизайном машин и их сабмитом. Всего им удалось сделать 7 нетривиальных машин, не имеющих решения в матрицах 1x1, но спать они уляглись где-то в 5-7 утра (по моему времени).

По состоянию на утро наш статус был таков:
Total cars:     2119
-------------------
Cars decoded:   2119
Fuels solved:   876
Fuels encoded:  872
Fuels tested:   872
Fuels OK:       872
Fuels uploaded: 872

Я попробовал почитать логи "всенощной", но быстро понял, что автостроителя из меня не выйдет. Получалось, что единственный способ добится преимущства - это научиться кодировать топливо более компактными фабриками, ведь за более компактные решения давали больше очков.

Я стал изучать фабрику из 6 гейтов, которая была найдена полным перебором для генерации "ключа" (см. картинку выше). Через некоторое время стало очевидно, что она использует тот же фокус с "протаскиванием" выхода более нижних гейтов через более верхние, но она не сохраняет триты на пути следования (как это делали в своей схеме мы), а изменяет их по пути. Но к финишу они всегда приходят в "нужную форму".

Некоторое время я пытался нарисовать что-то подобное на бумаге, а затем ко мне в Jabber постучался sannysanoff из THIRTEEN, и мы решили одну его проблему и одну мою :) У него начало правильно кодироваться топливо, а я получил идею о том, как сделать задуманное. В 13:00, за два часа до окончания соревнования(!!!) у меня был готов построитель фабрик, который кодировал "0" одним гейтом, а "1" и "2" - двумя, плюс в конец схемы ставился еще один вспомогательный гейт, т.е. в среднем уходило 1.66 гейта на трит:


Буквально за 15 минут был написан скрипт для заливки более хороших вариантов топлива. Все коллеги по команде (которые начали просыпаться где-то в 10 и снова засели за дизайн машин) получили Четкие Указания о том, что и как запускать, и мы стали в четыре руки заливать более "эффективое" топливо. Параллельно продолжал работать скрипт, выкачивающий и решающий все новые "машины".

Ударная заливка продолжалась до самого финала. К сожалению, начиная с самого утра сервер у организаторов опять тормозил, и залить все свои решения мы так и не успели. Зато мы успели самыми последними заслать дизайн машины (за 5 секунд до финала)!
В конце-концов наши достижения были такими:
Total cars:     3784
-------------------
Cars decoded:   3784
Cars bforced:   3784
Fuels solved:   2048
Fuels encoded:  2048
Fuels tested:   1944
Fuels OK:       1944
Fuels uploaded: 1654


Еще через час очки в таблице результатов обновились последний раз, и мы заняли 31 место в общем зачете, набрав 683,889 балла. За последние 3 часа мы набрали около 200 очков, что на фоне прогресса остальных команд выглядело, как мне кажется, впечатляюще. Эх, было бы еще пару часов времени ... :) Но в целом результатом я доволен - он, вобщем-то, соответствует нашим достижениям.

Спасибо организатором за интересное задание, спасибо моим коллегам по команде за проявленное рвение и достигнутые результаты, и, как всегда, спасибо моей жене за то, что я смог на три дня отключиться от обычной жизни! Родина (в моем) лице вас не забудет

PS
Отчет пишется "с пылу-с жару", а изменения и дополнения, если будут, пойдут отдельным постом.

PPS
Организаторы раскрыли математическую подоблеку заданий: http://icfp.gnumaniacs.org/2010/06/21/whats-this-thing-with-cars-and-fuels/. Использовать результаты одного конкурса для организации другого конкурса - это, по меткому выражению [livejournal.com profile] murkt, "верх цинизма" :)

PPPS
Ах да. Приборы и материалы:
  • Языки: Haskell, Scala, Perl, цельнотянутый Python, Matlab, Mathematica, graphviz
  • VCS: git
  • Коммуникации: teamspeak, jabber
  • Совместное редактирование: sync.in (текст) и google docs (картинки)
  • В эпизодах: bash, grep, awk, find и другие
PPPS
Исходники можно взять тут: http://github.com/adept/icfpc2010-futamura-rejection
From:
Anonymous
OpenID
Identity URL: 
User
Account name:
Password:
If you don't have an account you can create one now.
Subject:
HTML doesn't work in the subject.

Message:

 
Notice: This account is set to log the IP addresses of everyone who comments.
Links will be displayed as unclickable URLs to help prevent spam.

Profile

dastapov: (Default)
Dmitry Astapov

July 2017

M T W T F S S
     12
3456789
1011 1213141516
17181920212223
24252627282930
31      

Most Popular Tags

Style Credit

Expand Cut Tags

No cut tags