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