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

[_adept_]

Эпиграф

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

Comments

[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 требуют специального алгоритма, и т.п.

[_navi_]

Организаторы прислали кстати письмо, и сказали, что они поправили очки для тех, кто присылал правильные решения, которые они не могли точно проверить, и что для первых 25 мест это не повлияло на позиции.

Ещё они рассказали, почему оно так писало: они использовали Z3 для доказательства эквивалентности, а он засыпается на достаточно больших задачах, конечно, так что они ожидали, что участники догадаются, что они используют Z3 и будут намеренно посылать решения, которые они не смогут проверить, чтобы получить очки на халяву (так что правила, где, если они не могут найти контрпример за какое-то время, то решение засчитывается, не работают).

По-моему, конечно, использовать Z3 - это глупости, или по-крайней мере в такой форме. Могли бы сначала прогнать на куче случайных чисел, а потом, если всё сходится, попробовать Z3. Так бы они отбросили явно читерские решения, и могли бы засчитывать таймаут Z3 как правильное решение.

[spamsink]

Интересно было бы сравнить, как Synopsys Formality справляется с формулами, на которых Z3 затыкается.

[sorhed]

В одной из их статей описывался алгоритм поиска контрпримера (с участием SMT-солвера). Я полдня пытался в этом разобраться, но потом забил.

[thedeemon]

Они каждый день это делают с помощью SMT солверов, см. проекты RISE group в Microsoft Research. Тут Z3 использовали, как пить дать.

[xoposhiy]

Вот, только что написали в письме, что да, Z3.