Fair Guessing of Bit Vectors, или как я участвовал в ICFPC 2013.

[_adept_]

Эпиграф

Нас было 7 человек. У нас было 20 модулей на хаскеле, приватный репозиторий на гитхабе, 6 веток в этом репозитории, ImplicitParams, MagicHash и UndecidableInstances в коде и одна highmem нода на амазоне, а также hangouts для общения, юнит-тесты, просто тесты, google docs для заметок и куча статей про SMT-солверы. Не то что бы мы это все

Comments

[spamsink]

Неприятная задача. Если в таком духе дело пойдет, через пару лет будут задавать задачи на placement and routing, не особенно скрываясь. :)

Так мы лишились одного очка (почему это важно, станет ясно позднее).

Так вы на 10-м месте в lightning (или делите), а были бы на 9-м, думаешь?

Due to popular demand, these are the scores for the lightening division:

#5 is around 520
#10 is at 457

[_adept_]

Ух ты! Похоже, это мы на десятом месте!

[sorhed]

Призовым в лайтнинге считается только первое, а почётного упоминания удостаиваются лишь top 5. :)

[spamsink]

At the end of 72 hours, if your team's score is among the top 20, you will be contacted (at the email address you provided in EasyChair) and asked to submit a two-page abstract describing your solution.

Если этого не произошло, то вы на 21-24 месте. gnuplot со smooth bezier говорит, что вы на 22 месте.

[antilamer]

Пришло вот такое.

Dear Eugene,
You are receiving this message because:
-- You placed in the top 25 of the ICFP contest's main division
-- Or, you placed in the top 5 of the lightning division

И.т.п.

[spamsink]

Описание решения попросили?

[antilamer]

Ага.

[alex_akts]

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

[spamsink]

If r.status is "error", then the message field contains an explanation. Note, if the Game server is unable to prove that your guess is functionally equivalent to the secret program,
then you do NOT score a point. You can either try another guess,
or move on to another problem. If you make reasonable guesses,
we do not expect this to happen.

Короче, "если функции непохожи текстуально, но мы не можем найти контрпример, мы вернем error, и поминай как звали".

[_navi_]

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

Но конечно, фраза "If you make reasonable guesses, we do not expect this to happen", и вообще сам факт, что они не засчитывают такие программы - это свинство. Как я понимаю, если они таки сравнивают с expected short answer, под "reasonable guesses" здесь подразумевается, что порядок поиска у нас должен быть такой же как и у них. А вычурные оптимизации это нарушают.

[spamsink]

Я, конечно, утрировал. Для тривиального доказательства эквивалентности многих выражений может быть достаточно элементарных преобразований типа де Моргана и приведения повторных сложений к сдвигам. Более сложные эквивалентности типа x + (x << 1) + (x << 2) + ((x << 2) << 1) == (x << 4) + ~x + 1 требуют специального алгоритма, и т.п.

[sorhed]

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

Командное взаимодействие происходило посредством Google Hangouts и общего документа в Google Docs. Отлично работает.

А реальной жизни не существует. Ну, на эти 72 часа - точно. :)

[xoposhiy]

По мне так весь icfpc это про балланс между "придумывать светлые идеи" и "не заниматься бесполезной хернёй". Так весь контест и мечешься между ними :)

Все командное взаимодействие сводится к "следить, чтобы никто не занимался бесполезной херней :)"

[pbl]

Это универсальный феномен, по-видимому: все пытались убедить SMT отдаться, но решали форсом различных степеней брутности и терабайтом рама(тм). Вообще я в процессе получил сносно удовольствия, но по послеконтестному дискурсу начинает казаться, что задачка все-таки была дрянь. Кстати, в одной из статей организаторов, которые гугл любезно выдает сверху на program synthesis, бесцикловые функции сравнимой сложности генерились SMT солвером за ~час.

[sorhed]

Ну так уж и терабайта. Мы из 60 гигабайт использовали максимум 20. :)

[pbl]

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

[thedeemon]

Я сразу решил, что даже не буду пытаться с существующими солверами разобраться, все равно не успею. А переборщику на D хватало 10 мегов памяти. :)