Задача выполнимости

Александр Куликов
Александр Куликов
ПОМИ РАН, Computer Science Center
Кандидат физико-математических наук. Научный сотрудник лаборатории математической логики ПОМИ РАН, координатор и преподаватель Computer Science центра и Computer Science клуба при ПОМИ РАН, преподаватель Академического университета. Научные интересы: алгоритмы для NP-трудных задач, схемная сложность.
Лекция посвящена одной из самых известных алгоритмических задач — задаче выполнимости булевых формул. Это каноническая трудная задача, по которой проводится огромное количество исследований — как практических, так и теоретических. В частности, этой задаче посвящена ежегодная международная конференция. Каждый год также проводятся соревнования программ для данной задачи (так называемых сат-солверов). Такие программы активно используются во многих прикладных областях. Буквально несколько месяцев назад Дональд Кнут дописал том 4B монографии «Искусство программирования», треть которого посвящена задаче выполнимости. В лекции рассказано, в частности, о следующем:
  • Почему за алгоритм, решающий данную задачу за полиномиальное время, положен миллион долларов.
  • Как жадные алгоритмы, перебор с возвратами, локальный поиск, случайные блуждания и другие техники используются для разработки алгоритмов для задачи выполнимости.
  • Как именно сат-солверы используются на практике. В частности, воспользуемся сат-солверами для решения какой-нибудь комбинаторной задачи.