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

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