Лабораторная 1

[TonitaN]

Обсуждения и вопросы по первой лабораторной. Слайды с условием будут сегодня. Отсчёт времени - с завтрашнего дня.

Анонс дополнительной консультации: 12-30 11 сентября, в 330аю. Разбор арктических матриц и ординальной арифметики.

Кто (один человек, приоритетно - г. Задворных) желает взять альтернативную лабораторную (факторизация регулярок, собранных со StackOverflow, по модулю обратных ссылок), учитываем, что это - часть большого проекта, и 2 недели по ней - жёсткий дедлайн, после которого 1 лабораторная блокируется и становится стоимостью 0 баллов. Спойлер: если взять и сразу начать делать, такого не будет, идеологически она попроще, чем базовые, но технических деталей там больше.

[TonitaN]

Условия добавлены. В позапрошлом году условие 1 лабораторной составляло 6 слайдов, в прошлом - 9, в этом - 19. Тенденция...

[TonitaN]

Почин есть - первый сдавший.

EDIT: И как минимум двое сдающих на Рефале... А Haskell в этом году старательно обходят стороной - неужели с учётом опыта прошлых поколений?

[TonitaN]

На всякий случай, чтобы не возникло сомнений: лабораторные присылать по ночам можно, и к падению репутации это не приводит, если эта ночь - не перед штрафом или контрольным мероприятием. То есть сегодня и завтра ночью (считаем до 6 утра) вы можете спокойно их присылать, а вот ночью с воскресенья на понедельник - со штрафом в репутации 5 баллов. И с чуть меньшим штрафом в репутации (2 балла) - если пришлёте в воскресенье с 6 утра и до 10 вечера.

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

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

Важный EDIT (надеюсь, его мало кто заметит): Следование принципу "сгорел сарай - гори и хата" (выбирать рандомные варианты, чтобы уронить репутацию до нуля, попасть в "избранные" и не париться насчёт сроков сдачи и дальнейшего выбора вариантов) приведёт к появлению специальных санкций для "избранных". Которые коснутся всех с нулевой репутацией, а не только гения стратегии, буде таковой найдётся.

[TonitaN]

Раздача поощрений за качество будет, возможно, уже во вторник (в понедельник могу не успеть). Но коснётся тех, кто сдал лабораторную максимум в воскресенье.

[TonitaN]

Вариант номер 3 (арктические матрицы)

• лучшая синергия с z3: @Encapsulateed . Отчасти это "приз за везение", т.к. вряд ли кто-то экспериментировал с порядком записи в smt-файл с точки зрения скорости работы решателя. Но этот пункт напоминает, что рассматривать такие генераторы в отрыве от решателя не стоит. В общем, в этом варианте оправдался принцип "чем проще, тем лучше". +1 балл
• оригинальное решение: @Kabane-UN . Естественно, раскрытие скобок негативно сказалось на скорости работы солвера из-за возникновения экспоненциально разрастающихся определений функций :( Но это было красиво по идее и работает правильно. Ещё один человек использовал тот же принцип, но вы первый пошли этой дорогой, поэтому бонус достаётся вам. +1 балл
• первопроходец: @Kabane-UN. Здесь важен фактор не только "первого пославшего лабу", но и то, что решение было сразу чистым. +1 балл
• избежавшие "тетради смерти": их пятеро, все получают по +1. И это не значит, что вопросов по этой лабораторной не будет на экзамене :)

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

[TonitaN]

Вариант номер ординалы

• Во-первых, в этой группе есть избранный (репутация -75 баллов)! Его имя самому ему известно, а публично оглашать не буду.
• Во-вторых, в тетрадь смерти в этой группе попали все без исключения. Но поощрение за чистоту (по +1) всё-таки получают три человека из тех, чей компромат наиболее скромен.
• первопроходец: @OkDenAl, и кстати, один из лучших по чистоте решения. И ему же пришлось отдать один из призов за "лучшую синергию": ну что делать, если с поправкой на то что у конкурента некоторые предложения дублировались (кстати, для z3 это не проблема), их решения биективно отображались друг в друга. Итог: +2 балла
• второй приз за синергию (и почти наибольшую чистоту из всех): @vicadlsn
• оригинальный выбор: @GarryNeKasparov. Он единственный, кто предпочёл использовать другой солвер, который, кстати, считается ничем не хуже. +1 балл за любознательность.

[TonitaN]

Вариант с обычными функциями

• Только в этом варианте есть особая номинация "плоть и кровь девяточки": за самый вдохновенный парсер, учитывающий даже размерности конструкторов. И мне таки удалось его сломать, но на радостях я потеряла тест... (ничего, ещё найду) @VyacheslavIsWorkingNow, этот балл ваш.
• И опять тетрадь смерти пополнилась записями безусловно про всех... Однако у четверых баги наиболее безобидны (скажем, не уходят дальше парсера, или я могу сделать модель работоспособной мелкими штрихами), поэтому они получают по +1 баллу за чистоту.
• На домене, где багов минимум, лучшее быстродействие - у @Blackdeer1524 , причём разница в скорости работы z3 похожа на экспоненту! Тактика раскрытия всех скобок однозначно привела к идеальной синергии с z3 именно в этом варианте. +1 балл за синергию заслуженно ваш.
• Интересное решение - у @softylord : использовать API питона с z3. К сожалению, без багов на этом пути не обошлось, но локализовывать их мне оказалось очень трудно, из-за альтернативного синтаксиса входного файла. +1 балл за оригинальность ваш.

P.S. - Долгие размышления, кого же сделать первопроходцами, привели к мысли, что нужно наградить +1 баллом дополнительно всех, кто старался. Потому что старались многие.

[TonitaN]

Если вам вот вообще не понятно, что происходит и что должно происходить в лабораторной работе (неохота "курить условие" по несколько часов), есть простой приём, чтобы проверить, пора ли отправлять решение на проверку.

1. Берёте чужую лабораторную, получившую от меня высокую оценку
2. Запускаете тесты на ней и на вашей лабораторной (вот тогда и прочувствуете боль от использования альтернативного синтаксиса, не только же мне с этим мучиться)
3. Если солвер вернул один и тот же ответ на 10+ тестах (модели могут различаться, но они должны быть обе SAT или обе UNSAT одновременно) - возможно, ваша лаба действительно работает адекватно. Если нет - смотрите, на каких тестах произошло что-то странное.

И при этом надо брать нормальные достаточно разнообразные тесты, а не только f->ff и f->gh. Не лишне понять, глядя на них, является ли система по существу завершающейся (если даже является, не факт, что солвер это докажет. А вот откровенно sat на незавершайках быть категорически не должно).

Честно скажу - я стала уменьшать репутацию за плохо протестированные лабораторные, в которых исправляется строго указанный мною тест, без попыток заглянуть на шаг дальше. И если у первопроходцев было оправдание (непонятно, к чему стремиться, и соответствующие попытки могли трактоваться как запрос к Minimally Adequate Teacher), то у мейнстрима уже есть ориентиры, и вроде бы должны появиться зачатки умения фазз-тестирования.

P.S. - Режим MATа (Minimally Adequate Teacher) для таких кейсов скоро отключится. Будет просто "есть ошибки, переделывайте", потому что хватит уже злоупотреблять.