С Андреем я впервые увиделся на январской смене МКН в Сириусе. Я там вместо теоретического курса со всякими доказательствами решил прочитать более практический курс, где участники должны были решать разные трудные комбинаторные задачи при помощи SAT- и ILP-солверов: http://bit.ly/sirius_sat Начиналось всё с головоломок (ферзи, судоку, японские кроссворды, греко-латинские квадраты) и постепенно переходило к задачам, имеющие разные практические приложения (клики, раскраски, коммивояжёр). Все эти задачи вполне можно было решить, хоть в некоторых из них и надо было повозиться. И мне хотелось дать в конце также задачу, над которой пришлось бы поломать голову. Я несколько дней пытался придумать такую задачу, но у меня не вышло, и я решил дать задачу, которую за несколько дней абсолютно точно не решить, с одной стороны, с другой — всё равно полезно с ней поковыряться, потому что в процессе можно что-то новое узнать. Задача была связана с синтезом булевых схем при помощи SAT-солверов. Где-то десять лет назад у нас была про это публикация. Потом наше сведение реализовал Кнут, когда писал раздел 7.2.2.2 Satisfiability в четвёртом томе TAOCP. В общем, вы уже догадались, к чему я веду: Андрей всё это реализовал за выходные. Поздравляем наших ребят с победой на международной олимпиаде по программированию!
Завершилась самая престижная индивидуальная олимпиада школьников по информатике IOI 2020. Российская сборная выступила великолепно: три золотых и одна серебряная медали!
Золото завоевал студент факультета МКН и выпускник Президентского физико-математического лицея 239 Андрей Ефремов. Мы знакомы с Андреем с январской смены МКН в Сириусе, следим за его успехами и знаем, что это заслуженная награда. От души поздравляем Андрея! 👏🏻👏🏻👏🏻
