Организаторы прислали кстати письмо, и сказали, что они поправили очки для тех, кто присылал правильные решения, которые они не могли точно проверить, и что для первых 25 мест это не повлияло на позиции.
Ещё они рассказали, почему оно так писало: они использовали Z3 для доказательства эквивалентности, а он засыпается на достаточно больших задачах, конечно, так что они ожидали, что участники догадаются, что они используют Z3 и будут намеренно посылать решения, которые они не смогут проверить, чтобы получить очки на халяву (так что правила, где, если они не могут найти контрпример за какое-то время, то решение засчитывается, не работают).
По-моему, конечно, использовать Z3 — это глупости, или по-крайней мере в такой форме. Могли бы сначала прогнать на куче случайных чисел, а потом, если всё сходится, попробовать Z3. Так бы они отбросили явно читерские решения, и могли бы засчитывать таймаут Z3 как правильное решение.
no subject
Ещё они рассказали, почему оно так писало: они использовали Z3 для доказательства эквивалентности, а он засыпается на достаточно больших задачах, конечно, так что они ожидали, что участники догадаются, что они используют Z3 и будут намеренно посылать решения, которые они не смогут проверить, чтобы получить очки на халяву (так что правила, где, если они не могут найти контрпример за какое-то время, то решение засчитывается, не работают).
По-моему, конечно, использовать Z3 — это глупости, или по-крайней мере в такой форме. Могли бы сначала прогнать на куче случайных чисел, а потом, если всё сходится, попробовать Z3. Так бы они отбросили явно читерские решения, и могли бы засчитывать таймаут Z3 как правильное решение.