Алгоритмы локального поиска для k-КНФ

Постановка задачи

Задача выполнимости КНФ выглядит следующим образом. Для данной формулы F с n переменными в конъюнктивной нормальной форме необходимо определить, существует ли присваивание, обеспечивающее выполнимость формулы F. Если все дизъюнкты F содержат не более литералов, то F называется формулой в k-КНФ, а задача носит название задачи выполнимости k-КНФ (k-SAT) и является одной из самых фундаментальных NP-полных задач. Тривиальный алгоритм выполняет поиск среди 2n присваиваний значений 0 и 1 для n переменных. Однако с момента выхода работы [6] были разработаны алгоритмы, скорость выполнения которых значительно превышает O(2n) тривиального подхода. В качестве простого примера рассмотрим следующий прямолинейный алгоритм для задачи 3-КНФ, обеспечивающий верхнюю границу 1,913n. Выберем произвольный дизъюнкт из F, скажем, (x1_x2_x3). Затем сгенерируем семь новых формул путем замены x1, x2 и x3 всеми возможными значениями, кроме (x1, x2, x3) = (0, 1, 0), при котором, очевидно, формула F не выполняется. Теперь можно проверить выполнимость этих семи формул и сделать вывод, что F является выполнимой, в том случае, если хотя бы одна из этих формул выполнима. (Обозначим за T(n) временную сложность этого алгоритма. После этого, учитывая рекуррентность T(n) _ 7 _ T(n - 3), можно получить вышеупомянутую границу).