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

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

Задача о выполнимости КНФ заключается в следующем. Для данной формулы F с n переменными в конъюнктивной нормальной форме необходимо определить, существует ли присваивание, обеспечивающее выполнимость формулы F. Если все дизъюнкты F содержат не более литералов, то F называется формулой в k-КНФ, а задача носит название задачи выполнимости k-КНФ (k-SAT) и является одной из самых фундаментальных NP-полных задач. Тривиальный алгоритм выполняет поиск среди [math]\displaystyle{ 2^n \; }[/math] присваиваний значений 0 и 1 для n переменных. Однако с момента выхода работы [6] были разработаны алгоритмы, скорость выполнения которых значительно превышает [math]\displaystyle{ O(2^n) \; }[/math] тривиального подхода. В качестве простого примера рассмотрим следующий прямолинейный алгоритм для задачи 3-КНФ, обеспечивающий верхнюю границу [math]\displaystyle{ 1,913^n \; }[/math]. Выберем произвольный дизъюнкт из F, скажем, [math]\displaystyle{ (x_1 \lor \bar{x_2} \lor x_3) }[/math]. Затем сгенерируем семь новых формул путем подстановки в [math]\displaystyle{ x_1, x_2, x_3 \; }[/math] всех возможных значений, кроме [math]\displaystyle{ (x_1, x_2, x_3) = (0, 1, 0) \; }[/math], при котором, очевидно, формула F не выполняется. Теперь можно проверить выполнимость этих семи формул и сделать вывод, что F является выполнимой, в том случае, если хотя бы одна из этих формул выполнима. (Обозначим за T(n) временную сложность этого алгоритма. После этого, учитывая рекуррентность [math]\displaystyle{ T(n) \le 7 \times T(n - 3) \; }[/math], можно получить вышеупомянутую границу).