Задача выполнимости: теория и практика. Лекция 1

Мы познакомимся с задачей выполнимости — одной из самых важных трудно решаемых задач. Разберём основные методы решения задачи выполнимости (как в теории, так и на практике): метод расщепления, локальный поиск, случайные блуждания. Узнаем, как эта задача связана с другими известными вычислительными задачами: например, ускорить классический квадратичный по времени алгоритм для расстояния редактирования не проще, чем ускорить полный перебор для задачи выполнимости. Наконец, увидим, насколько эффективны SAT-солверы (задачи для решения задачи выполнимости) на практике: вместе решим несколько сложных комбинаторных задач при помощи таких программ.