МКН Александр Куликов. Выполнимость: задача на миллион. 1. Причины популярности

Александр Куликов, доктор физ.-мат. наук, старший научный сотрудник ПОМИ РАН, профессор МКН СПбГУ, член совета Computer Science центра, руководитель образовательных проектов JetBrains.

Задача выполнимости — одна из самых популярных трудных алгоритмических задач. В первой части лекции мы узнаем причины этого: за доказательство существования или отсутствия эффективного алгоритма для этой задачи положен приз в миллион долларов; в терминах этой задачи легко формулируются многие возникающие на практике задачи; она находит применения в самых разных областях компьютерных наук; ей посвящена ежегодная международная конференция, каждый год проводится соревнование программ для решения задачи выполнимости; самый длинный раздел в "Искусстве программирования" Кнута посвящён задаче выполнимости.

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

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

В четвёртой части увидим, что выполнимость — самая трудная задача: если для неё есть эффективные алгоритмы, то они есть и для всех других трудных задач.

В пятой части поговорим о том, как именно задача выполнимости используется в формальной верификации. Познакомимся с простейшими системами доказательств, позволяющими убедиться, что данная формула невыполнима.

Лекция может быть интересна студентам и старшеклассникам.

[alexeykholodkov]

Большое спасибо за освещение такой интересной темы.
Хочется больше узнать о том как сейчас пишутся sat-солверы. Есть ли русскоязычные сообщества которые этим занимаются?
В частности хочется узнать как солверы тестируются - предположу что должны быть библиотеки для генерации различных 3кнф (для последующей проверки на них) для которых заранее известно выполнимы ли они, только самому не получилось такие найти.

[AnatoliiSviridenkov]

Миллион дают, если доказать решаемость. За доказательство нерешаемости миллион не дают.

[falafel]

Спасибо за видео. Позвольте высказать критику. Александра на видео слишком много, непонятно зачем. Если бы изображение было в одном из углов, воспринималось бы лучше. Сопровождение постоянно переключается на Александра и обратно, невозможно сосредоточиться. И оговорки режут слух