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

Материал из WEGA
Перейти к навигации Перейти к поиску

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

Задача о выполнимости КНФ заключается в следующем. Для данной формулы 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{ \gets }[/math] произвольный дизъюнкт G, невыполнимый на y';
     изменить y' следующим образом:
        равномерным случайным образом выбрать один из литералов C и поменять присваивание этому литералу на противоположное;
  end
  return y'


Шонинг выполнил очень изящный анализ этого алгоритма. Обозначим за d(a, b) расстояние Хэмминга между двумя бинарными векторами (присваиваниями) a и b. Для простоты будем считать, что формула F оказывается выполнимой только на одном присваивании y* и что текущее присваивание y находится от y* на расстоянии Хэмминга d. Предположим также, что ложный в настоящий момент дизъюнкт C включает три переменные – [math]\displaystyle{ x_i, x_j \; }[/math] и [math]\displaystyle{ x_k \; }[/math]. Тогда y и y* должны различаться по меньшей мере в одной из этих переменных. Это значит, что если поменять значение [math]\displaystyle{ x_i, x_j \; }[/math] или [math]\displaystyle{ x_k \; }[/math] на противоположное, то новое присваивание будет ближе к y* согласно расстоянию Хэмминга с вероятностью не ниже 1/3 – и дальше от него с вероятностью не более 2/3. Это рассуждение можно распространить на случай, когда формула F оказывается выполнимой на нескольких присваиваниях. Отсюда следует важная лемма.


Лемма 1. Пусть F – выполнимая формула, а y* – присваивание, на котором она оказывается выполнимой. Для любого присваивания y вероятность того, что присваивание, на котором формула оказывается выполнимой (и которое может быть отличным от y*), найдено алгоритмом RandomWalk(F, y), составляет не менее [math]\displaystyle{ (1/(k - 1))^{d(y, y*)}/p(n) \; }[/math], где p(n) – полином от n.


Взяв среднее значение по случайным начальным присваиваниям, получим следующую теорему.


Теорема 2. Для любой выполнимой формулы F с n переменными вероятность успеха алгоритма RandomWalk(F, y) составляет не менее [math]\displaystyle{ (k/2(k - 1))^n /p(n) '; }[/math] для некоторого полиномиального p. Таким образом, положив [math]\displaystyle{ I = (2(k - 1)/k)^n \cdot p(n) \; }[/math], алгоритм SCH с высокой вероятностью находит присваивание, на котором формула выполняется. При k = 3 значение I составляет [math]\displaystyle{ O(1,334^n) \; }[/math].

Применение

Результат Шонинга был улучшен в серии статей [1, 3, 9], основанных на идее из [3]. В частности, сочетание алгоритма RandomWalk с алгоритмом 2-КНФ с полиномиальным временем выполнения позволило выбирать более подходящие начальные присваивания. Дерандомизация алгоритма SCH описана в работе [2]. В работе [4] была предложена нетривиальная комбинация SCH с еще одним известным представителем семейства алгоритмов с возвратом [8], что позволило ускорить выполнение алгоритма до показателя [math]\displaystyle{ O(1,324^n) \; }[/math]. Самый быстрый известный на данный момент алгоритм представлен в [10], он основан на том же подходе, что и алгоритм из работы [4], и выполняется за время [math]\displaystyle{ O(1,32216^n) \; }[/math].

Открытые вопросы

Задача k-КНФ остается, вероятно, самой популярной NP-полной задачей, над поиском самого быстрого алгоритма решения которой бьется множество исследователей. Улучшение его временной границы представляет собой значимую цель исследований.

Экспериментальные результаты

Исследователи искусственного интеллекта также активно изучали алгоритм КНФ, включая локальный поиск – см., например, [5].

См. также

Литература

1. Baumer, S., Schuler, R.: Improving a probabilistic 3-SAT algorithm by dynamic search and independent clause pairs. ECCC TR03-010, (2003) Also presented at SAT (2003)

2. Dantsin, E., Goerdt, A., Hirsch, E.A., Kannan, R., Kleinberg, J., Papadimitriou, C., Raghavan, P., Schöning, U.: A deterministic (2 - 2/(k +1))n algorithm for k-SAT based on local search. Theor. Comput. Sci. 289(1), 69–83 (2002)

3. Hofmeister, T., Schöning, U., Schuler, R., Watanabe, O.: Probabilistic 3-SAT algorithm further improved. Proceedings 19th Symposiumon Theoretical Aspects of Computer Science. LNCS 2285, 193–202 (2002)

4. Iwama, K., Tamaki, S.: Improved upper bounds for 3-SA T. In: Proceedings 15th Annual ACM-SIAM Symposium on Discrete Algorithms, pp. 321–322. New Orleans, USA (2004)

5. Kautz, H., Selman, B.: Ten Challenges Redux: Recent Progress in Propositional Reasoning and Search. Proceedings 9th International Conference on Principles and Practice of Constraint Programming, pp. 1–18. Kinsale, Ireland (2003)

6. Monien, B., Speckenmeyer, E.: Solving satisfiability in less than 2n steps. Discret. Appl.Math. 10, 287–295 (1985)

7. Papadimitriou, C.H.: On selecting a satisfying truth assignment. Proceedings 32nd Annual Symposium on Foundations of Computer Science, pp. 163–169. San Juan, Puerto Rico (1991)

8. Paturi, R., Pudlák, P., Saks, M.E., Zane, F.: An improved exponential-time algorithm for k-SAT. Proceedings 39th Annual Symposium on Foundations of Computer Science, pp. 628–637. Palo Alto, USA (1998) Also, J. ACM52(3), 337–364 (2006)

9. Rolf, D.: 3-SAT 2 RTIME(O(1.32793n)). ECCC TR03–054. (2003)

10. Rolf, D.: Improved Bound for the PPSZ/Schöning-Algorithm for 3-SAT. J. Satisf. Boolean Model. Comput. 1, 111–122 (2006)

11. Schöning, U.: A probabilistic algorithm for k-SAT and constraint satisfaction problems. Proceedings 40th Annual Symposium on Foundations of Computer Science, pp. 410–414. New York, USA (1999)