Открытая лекция: задача выполнимости булевых формул

(Скриншот из презентации: slideplayer.com/slide/3238789 ^[1])

Приглашаем всех на открытую лекцию Computer Science центра ^[2], посвященную задаче выполнимости булевых формул — одной из самых известных и важных алгоритмических задач. Лекция пройдёт в рамках встречи со слушателями онлайн-курса «Алгоритмы: теория и практика. Методы» ^[3]. Время и место проведения: 25 декабря, 19:00, БЦ Таймс (г. Санкт-Петербург, ул. Кантемировская 2А, 4 этаж). Участие бесплатное, но требуется регистрация: goo.gl/IiNvV8 ^[4]

Задача выполнимости — каноническая трудная задача, по которой проводится огромное количество исследований: как практических, так и теоретических. В частности, этой задаче посвящена ежегодная международная конференция. Каждый год проходят соревнования программ для данной задачи (так называемых сат-солверов). Такие программы активно используются во многих прикладных областях. Буквально несколько месяцев назад Дональд Кнут дописал том 4B монографии «Искусство программирования», треть которого посвящена задаче выполнимости.

В лекции будут рассмотрены, в частности, следующие вопросы:
— почему за алгоритм, решающий данную задачу за полиномиальное время, положен миллион долларов;
— как жадные алгоритмы, перебор с возвратами, локальный поиск, случайные блуждания и другие техники используются для разработки алгоритмов для задачи выполнимости;
— как именно сат-солверы используются на практике (воспользуемся сат-солверами для решения какой-нибудь комбинаторной задачи).

Автор: СПБАУ

Источник ^[5]