Алгоритмы локального поиска для 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], можно получить вышеупомянутую границу).

Основные результаты

В длинном списке алгоритмов для k-SAT алгоритм Шонинга [11] стал революционным прорывом. Это стандартный подход с использованием локального поиска, и сам по себе алгоритм не был новинкой (см., например, [7]). Предположим, что y – текущее присваивание (его начальное значение равномерно выбирается случайным образом). Если присваивание y обеспечивает выполнимость формулы, алгоритм выдает ответ «Да» и завершает работу. В противном случае имеется по меньшей мере один дизъюнкт, литералы которого на присваивании y имеют значение «ложь». Выберем такой произвольный дизъюнкт и выберем случайным образом один из трех литералов. Затем изменим значение этой переменной на противоположное («истина» на «ложь» и наоборот), заменим y этим новым присваиванием и повторим ту же процедуру. Более формально алгоритм выглядит следующим образом:

  SCH(КНФ-формула F, целое I)
     repeat I раз
        y = равномерно выбранный случайный вектор [math]\displaystyle{ \in \{ 0, 1 \}^n \; }[/math]
        z = RandomWalk(F, y);
        if z приводит к выполнимости F
           then output(z); exit;
     end
     output(«Невыполнима»);
  RandomWalk(КНФ-формула [math]\displaystyle{ G(x_1, x_2, ..., x_n) \; }[/math], присваивание y);
     y' = y;
     for 3n раза
        if y' приводит к выполнимости G
           then return y'; exit;
     C [math]\displaystyle{ \to }[/math] произвольный дизъюнкт G, невыполнимый на y';
     Изменить y' следующим образом:
        равномерным случайным образом выбрать один из литералов C и поменять присваивание этому литералу на противоложное;
  end
  return y'