Алгоритмы локального поиска для k-КНФ: различия между версиями

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