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

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

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

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

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

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

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

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

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