Выполнимость: задача на миллион. 5. Системы доказательств, формальная верификация

Александр Куликов, доктор физ.-мат. наук, старший научный сотрудник ПОМИ РАН, профессор МКН СПбГУ, член совета Computer Science центра, руководитель образовательных проектов JetBrains. Задача выполнимости — одна из самых популярных трудных алгоритмических задач. В первой части лекции мы узнаем причины этого: за доказательство существования или отсутствия эффективного алгоритма для этой задачи положен приз в миллион долларов; в терминах этой задачи легко формулируются многие возникающие на практике задачи; она находит применения в самых разных областях компьютерных наук; ей посвящена ежегодная международная конференция, каждый год проводится соревнование программ для решения задачи выполнимости; самый длинный раздел в “Искусстве программирования“ Кнута посвящён задаче выполнимости. Во второй части мы познакомимся с программами для решения задачи выполнимости. Чтобы продемонстрировать, как просто ими пользоваться, мы вместе напишем программу, которая мгновенно решает любой Судоку.