K-КНФ-алгоритмы на основе поиска с возвратом

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

Широко известна задача определения сложности алгоритма выполнимости формул, записанных в форме k-КНФ. Пусть дана булева формула в конъюнктивной нормальной форме, имеющая не более k литералов на дизъюнкт. Необходимо найти такое присваивание переменным, при котором выполняются все дизъюнкты, или дать ответ об отсутствии такого присваивания. Хорошо известно, что проблема разрешимости для задачи выполнимости k-КНФ является NP-полной для [math]\displaystyle{ k \ge 3 \; }[/math]. Далее будут рассмотрены алгоритмы, позволяющие значительно улучшить время выполнения в наихудшем случае, ассоциированное с алгоритмом поиска полным перебором и составляющее [math]\displaystyle{ poly(n)2^n \; }[/math] для формулы с n переменными. Мониен и Шпекенмейер [8] впервые улучшили границу, предложив простой алгоритм с временем выполнения [math]\displaystyle{ O(2^{(1 - \varepsilon_k)n}) }[/math], где [math]\displaystyle{ \varepsilon_k \gt 0 \; }[/math] для всех k. В последующих работах [1, 3, 5, 6, 7, 9, 10, 11, 12] были предложены и проанализированы алгоритмы со все более приемлемым временем выполнения (для больших значений [math]\displaystyle{ \varepsilon_k \; }[/math]).

Эти алгоритмы обычно применяют один из двух подходов к поиску решения задачи выполнимости. Первый класс составляют алгоритмы поиска с возвратом. Эти алгоритмы, изначально предложенные Дэвисом, Логеманом и Лавлендом [4], иногда называют процедурами Дэвиса-Патнем. Подобные алгоритмы пытаются найти присваивание, на котором формула оказывается выполнимой, назначая в некотором порядке значения каждой переменной и выполняя возврат в случае, если дизъюнкт оказался ложным. Другой класс алгоритмов построен на использовании локального поиска (первые результаты с гарантированной эффективностью были получены Шонингом [12]). Алгоритм начинает работу со случайно или стратегически выбранного присваивания и выполняет локальный поиск присваиваний, результатом которых является выполнимость формулы, ориентируясь на невыполняющиеся дизъюнкты.

Далее будет представлен ResolveSat, рандомизированный алгоритм проверки выполнимости k-КНФ с одними из лучших известных на данный момент верхних границ. Он основан на более раннем алгоритме, предложенном Патури, Пудлаком и Зейном [10] и представляющим собой алгоритм поиска с возвратом, который проверяет переменные в случайно выбранном порядке. Анализ алгоритма основывается на следующем наблюдении: до тех пор пока у формулы имеется присваивание, на котором она оказывается выполнимой, изолированное от других аналогичных присваиваний, треть переменных встречается в виде единичных дизъюнктов, поскольку переменные присваиваются в случайном порядке. Таким образом, алгоритму нужно правильно угадать значения не более чем 2/3 переменных. Этот анализ был расширен для общего случая благодаря следующему наблюдению: либо существует изолированное присваивание, на котором формула выполнима, либо существует много решений, так что вероятность угадать подходящее достаточно высока.

ResolveSat объединяет эти идеи и стремление значительно улучшить границы [9]. На данный момент алгоритму ResolveSat удается обеспечить наилучшие известные верхние границы для задачи выполнимости k-КНФ для всех [math]\displaystyle{ k \ge 5 \; }[/math]. Для k = 3 и k = 4 Ивама и Таками [6] получили наилучшую известную верхнюю границу при помощи рандомизированного алгоритма, сочетающего идеи алгоритма локального поиска Шонинга и ResolveSat. Более того, для задачи с предусловием о существовании единственного решения задачи выполнимости k-КНФ, считающейся одной из самых трудных вариаций задачи о выполнимости k-КНФ [2], ResolveSat достигает рекордных значений для всех [math]\displaystyle{ k \ge 3 \; }[/math]. Границы, полученные ResolveSat для задачи с единственным решением и задачи общего вида для значений k = 3, 4, 5, 6, представлены в таблице. Эти границы сравниваются с границами алгоритма Шонинга [12], последовательно улучшенными результатами на базе локального поиска [1, 5, 11] и недавними изменениями, предложенными Ивамой и Таками [6]. Полученные для этих алгоритмов верхние границы выражаются в форме [math]\displaystyle{ 2^{cn - o(n)} \; }[/math], а значения в таблице отражают показатель c. Это сравнение охватывает только лучшие границы вне зависимости от типа алгоритма (рандомизированного или детерминированного).

Нотация

Далее булева формула в КНФ [math]\displaystyle{ F(x_1, x_2, ..., x_n) \; }[/math] будет рассматриваться и как булева функция, и как множество дизъюнктов. Булева формула F является формулой в k-КНФ, если все дизъюнкты имеют величину не более k. Для дизъюнкта C обозначим за var(C) множество переменных, встречающихся в C. Если [math]\displaystyle{ v \in var(C) \; }[/math], то ориентация [math]\displaystyle{ v \; }[/math] является положительной, если литерал v принадлежит к C, и отрицательной, если литерал [math]\displaystyle{ \bar{v} \; }[/math] принадлежит к C. Вспомним, что если F является булевой формулой в КНФ над переменными [math]\displaystyle{ (x_1, x_2, ..., x_n) \; }[/math], а [math]\displaystyle{ a \; }[/math] – частичным присваиванием переменным, то ограничение F согласно [math]\displaystyle{ a \; }[/math] определяется как формула [math]\displaystyle{ F' = F \lceil_a \; }[/math] на множестве переменных, значения которых задаются без использования [math]\displaystyle{ a \; }[/math], получаемая в результате обработки каждого дизъюнкта C формулы F следующим образом: если значение C в результате присваивания [math]\displaystyle{ a \; }[/math] становится равным 1, то C следует удалить; в противном случае заменить C дизъюнктом C’, полученным в результате удаления из C любых литералов, значения которых в результате присваивания [math]\displaystyle{ a \; }[/math] становятся равными 0. Единичным дизъюнктом называется дизъюнкт, содержащий ровно один литерал.

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

Алгоритм ResolveSat

Алгоритм ResolveSat по сути очень прост. Получив на вход формулу в k-КНФ, он вначале генерирует дизъюнкты, которые могут быть получены путем разложения, длина которых не превышает некоторой величины. Затем он устанавливает некоторый случайный порядок переменных и последовательно присваивает им значения согласно этому порядку. Если рассматриваемая в текущий момент переменная встречается в виде единичного дизъюнкта, ей присваивается единственное значение, при котором этот дизъюнкт выполним. Если она встречается в двух противоречащих друг другу единичных дизъюнктах, алгоритм начинает работу заново. На каждом этапе алгоритм также проверяет, выполнима ли формула. Если выполнима, то входной набор принимается. Процедура повторяется до тех пор, пока не будет найдено присваивание, приводящее к выполнимости формулы, либо пока не истечет выделенное время.

Алгоритм ResolveSat использует следующую процедуру, которая принимает на вход произвольное присваивание y, КНФ-формулу F и перестановку [math]\displaystyle{ \pi \; }[/math] и выполняет присваивание u. Присваивание u получается путем рассмотрения переменных y в порядке, заданном [math]\displaystyle{ \pi \; }[/math], и изменении их значений в попытке обеспечить выполнимость формулы F.

Функция Modify(КНФ-формула [math]\displaystyle{ G(x_1, x_2, ..., x_n) \; }[/math], перестановка [math]\displaystyle{ \pi \; }[/math] = ({1, 2, ..., n}, присваивание y) [math]\displaystyle{ \to }[/math] (присваивание u)

  [math]\displaystyle{ G_0 = G }[/math].
  for i = 1 to n
     if [math]\displaystyle{ G_{i - 1} }[/math] содержит единичный дизъюнкт [math]\displaystyle{ x_{\pi (i)} }[/math]
        then [math]\displaystyle{ u_{\pi(i)} = 1 }[/math]
     else if [math]\displaystyle{ G_{i - 1} }[/math] содержит единичный дизъюнкт [math]\displaystyle{ \bar{x}_{\pi (i)} }[/math]
        then [math]\displaystyle{ u_{\pi(i)} = 0 }[/math]
     else [math]\displaystyle{ u_{\pi(i)} = y_{\pi(i)} }[/math]
     [math]\displaystyle{ G_i = G_{i - 1} \lceil_{x_{\pi (i)} = u_{\pi (i)}} \; }[/math]
  end /* конец цикла for */ 
  return u;

Алгоритм Search получается в результате выполнения алгоритма Modify[math]\displaystyle{ (G, \pi, y) \; }[/math] на нескольких парах [math]\displaystyle{ (\pi, y) \; }[/math], где [math]\displaystyle{ \pi \; }[/math] – случайная перестановка, а y – случайное присваивание.

Search(КНФ-формула F, целое число I)

  repeat I раз
     [math]\displaystyle{ \pi }[/math] = равномерно распределенная случайная перестановка 1, ..., n
     у = равномерно распределенный случайный вектор [math]\displaystyle{ \in \{ 0, 1 \}^n \; }[/math]
     u = Modify[math]\displaystyle{ (F, \pi, у) }[/math];
     if при u формула F выполнима
        then output(u); exit;
     end /* конец цикла repeat */
  output("Невыполнима");

Алгоритм ResolveSat получается в результате сочетания Search с шагом предварительной обработки, заключающейся в ограниченном разложении формулы. Между дизъюнктами [math]\displaystyle{ C_1 \; }[/math] и [math]\displaystyle{ C_2 \; }[/math] возникает конфликт на переменной v, если один из них содержит v, а другой – [math]\displaystyle{ \bar{v} }[/math]. [math]\displaystyle{ C_1 \; }[/math] и [math]\displaystyle{ C_2 \; }[/math] представляют собой разложимую пару, если они конфликтуют точно на одной переменной v. Для таких пар их резольвентой, обозначаемой [math]\displaystyle{ R(C_1, C_2) \; }[/math], будет являться дизъюнкт [math]\displaystyle{ C = D_1 \vee D_2 \; }[/math], где [math]\displaystyle{ D_1 \; }[/math] и [math]\displaystyle{ D_2 \; }[/math] получаются удалением v и [math]\displaystyle{ \bar{v} }[/math] из [math]\displaystyle{ C_1 \; }[/math] и [math]\displaystyle{ C_2 \; }[/math], соответственно. Легко заметить, что любое присваивание, при котором [math]\displaystyle{ C_1 \; }[/math] и [math]\displaystyle{ C_2 \; }[/math] выполнимы, влечет также и выполнимость C. Следовательно, если F является выполнимой КНФ-формулой, содержащей разложимую пару [math]\displaystyle{ C_1 \; }[/math], [math]\displaystyle{ C_2 \; }[/math], то формула [math]\displaystyle{ F' = F \wedge R(C_1, C_2) }[/math] будет иметь те же удовлетворяющие условию выполнимости присваивания, что и F. Разложимая пара [math]\displaystyle{ C_1, C_2 \; }[/math] является s-ограниченной, если [math]\displaystyle{ |C_1|, |C_2| \le s }[/math] и [math]\displaystyle{ |R(C_1, C_2)| \le s }[/math]. Следующая процедура расширяет формулу [math]\displaystyle{ F \; }[/math] до формулы [math]\displaystyle{ F_s \; }[/math], применяя s-ограниченное разложение максимально возможное количество раз.

Resolve(КНФ-формула F, целое число s)

  [math]\displaystyle{ F_s = F }[/math].
  while [math]\displaystyle{ F_s }[/math] содержит s-ограниченную разложимую пару [math]\displaystyle{ C_1, C_2 }[/math], такую, что [math]\displaystyle{ R(C_1, C_2) \notin F_s }[/math]
        [math]\displaystyle{ F_s = F_s \wedge R(C_1, C_2) }[/math].
  return ([math]\displaystyle{ F_s }[/math]).

Алгоритм для формулы k-КНФ представляет собой простую комбинацию Resolve и Search:

ResolveSat(КНФ-формула F, целое число s, целое положительное число I)

  [math]\displaystyle{ F_s }[/math] = Resolve(F, s).
  Search([math]\displaystyle{ F_s }[/math], I).

Анализ алгоритма ResolveSat

Время выполнения ResolveSat(F, s, I) можно ограничить следующим образом. Resolve(F, s) добавляет не более [math]\displaystyle{ O(n^s) \; }[/math] дизъюнктов к F за счет сравнения пар дизъюнктов, так что прямолинейная реализация будет выполняться за время [math]\displaystyle{ n^{3s}poly(n) \; }[/math] (эту границу можно улучшить, однако ее улучшение не повлияет на асимптотику основного результата). Search([math]\displaystyle{ F_s, \; I }[/math]) требует [math]\displaystyle{ I(|F| + n^s)poly(n) \; }[/math] времени. Следовательно, полное время выполнения ResolveSat(F, s, I) можно грубо ограничить сверху значением [math]\displaystyle{ (n^{3s} + I(|F| + n^s))poly(n) \; }[/math]. If s = O(n/log n), общее время выполнения можно ограничить значением [math]\displaystyle{ I|F|2^{O(n)} \; }[/math], поскольку [math]\displaystyle{ n^s = 2^{O(n)} \; }[/math]. Для этого нужно взять в качестве s некоторую константу достаточно большой величины или медленно растущую функцию от n. Таким образом, s(n) будет стремиться к бесконечности с n, но будет оставаться в пределах O(log n).

В случае, если функция F оказывается невыполнимой, алгоритм Search(F, I) всегда выдает результат «невыполнима». Таким образом, единственной проблемой остается нахождение верхней границы в случае, когда F выполнима. Обозначим за [math]\displaystyle{ \tau(F) \; }[/math] вероятность того, что Modify([math]\displaystyle{ F, \pi, y \; }[/math]) найдет некоторое присваивание, обеспечивающее выполнимость. Тогда для выполнимой функции F вероятность ошибки Search(F, I) равна [math]\displaystyle{ (1 - \tau(F))^I \le e^{-I \tau(F)} }[/math], что не превышает [math]\displaystyle{ e^{-n} \; }[/math] при условии [math]\displaystyle{ I \ge n / \tau(F) }[/math]. Следовательно, достаточно получить хорошую верхнюю границу для [math]\displaystyle{ \tau(F) \; }[/math].

Анализ сложности алгоритма ResolveSat требует введения ряда констант [math]\displaystyle{ \mu_k \; }[/math] для [math]\displaystyle{ k \ge 2 \; }[/math]:

[math]\displaystyle{ \mu_k = \sum_{j=1}^{\infty} \frac{1}{j (j + \frac{1}{k - 1})} }[/math].

Легко показать, что [math]\displaystyle{ \mu_3 = 4 - 4 \; ln \; 2 \gt 1,226 }[/math], используя разложение функции ln 2 в ряд Тейлора. Используя стандартные способы, также легко показать, что [math]\displaystyle{ \mu_k \; }[/math] представляет собой возрастающую функцию от k с пределом [math]\displaystyle{ \sum_{j=1}^{\infty} (1 / j^2) = (\pi^2 / 6) = 1,644 }[/math].

Результаты работы алгоритма ResolveSat можно изложить в следующих трех теоремах.

Теорема 1 (i). Пусть [math]\displaystyle{ k \ge 5 \; }[/math], а s(n) – функция, стремящаяся к бесконечности. Тогда для любой выполнимой формулы F в k-КНФ с n переменными верно соотношение:

[math]\displaystyle{ \tau(F_s) \ge 2^{-(1 - \frac{mu_k}{k - 1})n - o(n)} }[/math].

Следовательно, ResolveSat(F, s, I) при [math]\displaystyle{ I = 2^{(1 - \frac{mu_k}{k - 1})n - O(n)} }[/math] имеет вероятность ошибок O(1) и время выполнения [math]\displaystyle{ 2^{(1 - \frac{mu_k}{k - 1})n - O(n)} }[/math] на любой выполнимой формуле в k-КНФ при условии, что s(n) стремится к бесконечности достаточно медленно.

(ii) Для [math]\displaystyle{ k \ge 3 \; }[/math] те же границы действительны для случая, когда формула F является уникально выполнимой.

Для доказательства теоремы 1 вначале рассмотрим случай уникальной выполнимости, а затем свяжем с ним задачу общего вида. При [math]\displaystyle{ k \ge 5 \; }[/math] из анализа следует, что асимптотика для общего случая оказывается не хуже асимптотики для случая уникальной выполнимости. При k = 3 и k = 4 границы в общем случае оказываются несколько более худшими по сравнению с уникальным.

Теорема 2. Пусть s = s(n) – медленно растущая функция. Для любой выполнимой 3-КНФ-формулы с n переменными верно [math]\displaystyle{ \tau(F_s) \ge 2^{-0,521^n} }[/math], в силу чего ResolveSat(F, s, I) с [math]\displaystyle{ I = n \; 2^{0,521n} }[/math] имеет вероятность ошибок O(1) и время выполнения [math]\displaystyle{ 2^{0,521 n + O(n)} \; }[/math].

Теорема 3. Пусть s = s(n) – медленно растущая функция. Для любой выполнимой 4-КНФ-формулы с n переменными верно [math]\displaystyle{ \tau(F_s) \ge 2^{-0,5625n} }[/math], в силу чего ResolveSat(F, s, I) с [math]\displaystyle{ I = n \; 2^{0,5625n} \; }[/math] имеет вероятность ошибок O(1) и время выполнения [math]\displaystyle{ 2^{0,5625n + O(n)} \; }[/math].

Применение

Различные эвристики применялись для создания алгоритмов выполнимости формул в 3-КНФ, значительно превосходящих эффективностью алгоритмы перебора. Алгоритм ResolveSat и его анализ представляют строгое объяснение этой эффективности и обозначают структурные параметры (к примеру, длину дизъюнктов и количество решений), влияющие на сложность.

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

Разрыв между границами для общего случая и для случая уникальной выполнимости при [math]\displaystyle{ k \in \{ 3, 4 \} }[/math] связан со слабостью анализа; было высказано предположение, что асимптотические границы для случая уникальной выполнимости выполняются в общем случае для всех k. Если это предположение верно, из него следует, что ResolveSat оказывается быстрее любого существующего алгоритма и в случае k = 3.

к uniquek-SAT [ ] k-SAT [ ] k-SAT [ ] k-SAT [1 , , 11] k-SAT [6] 3 0,386... 0,521 ... 0,415... 0,409... 0,404... 4 0,554... 0,562... 0,584... 0,559... 5 0,650... 0,678... 6 0,711 ... 0,736...

Таблица 1

В таблице представлен показатель c, используемый в значении границы 2c"~oW для уникального и общего случаев задачи k-КНФ, решаемой при помощи алгоритма ResolveSat, границы для k-КНФ и алгоритма Шонинга [12], его улучшенной версии для 3-КНФ [1, 5, 11] и гибридной версии из работы [6]

Еще одной любопытной задачей было бы более четкое понимание связи между количеством присваиваний, приводящих к выполнимости, и сложностью поиска такого присваивания [2]. Сильная гипотеза заключается в том, что выполнимость формул с большим количеством подходящих присваиваний доказать намного проще, чем в случае формул с меньшим числом решений.

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

См. также

• Алгоритмы локального поиска для k-КНФ
• Задача максимальной выполнимости формул в 2-КНФ
• Параметризованная задача выполнимости КНФ
• Пороги в задаче выполнимости случайной k-КНФ

Литература

1. Baumer, S., Schuler, R.: Improving a Probabilistic 3-SAT Algorithm by Dynamic Search and Independent Clause Pairs. In: SAT 2003, pp. 150-161

2. Calabro, C., Impagliazzo, R., Kabanets, V., Paturi, R.: The Complexity of Unique k-SAT: An Isolation Lemma for k-CNFs. In: Proceedings of the Eighteenth IEEE Conference on Computational Complexity, 2003

3. Dantsin, E., Goerdt, A., Hirsch, E.A., Kannan, R., Kleinberg, J., Papadimitriou, C., Raghavan, P., Schoning, U.: A deterministic (2 — k+12)n algorithm for k-SAT based on local search. Theor. Comp. Sci. 289(1), 69-83 (2002)

4. Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. Commun.ACM 5, 394-397 (1962)

5. Hofmeister, T., Schoning, U., Schuler, R., Watanabe, O.: A probabilistic 3-SAT algorithm further improved. In: STACS 2002. LNCS, vol. 2285, pp. 192-202. Springer, Berlin (2002)

6. Iwama, K., Tamaki, S.: Improved upper bounds for 3-SAT. In: Proceedings of the fifteenth annual ACM-SIAM symposium on Discrete algorithms, 2004, pp. 328-329

7. Kullmann,O.: New methods for 3-SAT decision and worst-case analysis. Theor. Comp. Sci. 223(1-2), 1 -72 (1999)

8. Monien, B., Speckenmeyer, E.: Solving Satisfiability In Less Than 2n Steps. Discret. Appl. Math. 10,287-295 (1985)

9. Paturi, R., Pudlak, P., Saks, M., Zane, F.: An Improved Exponential-time Algorithm for k-SAT. J. ACM 52(3), 337-364 (2005) (более ранняя версия публиковалась в источнике "39th Annual IEEE Symposium on Foundations of Computer Science, 1998, pp. 628-637")

10. Paturi, R., Pudlak, P., Zane, F.: Satisfiability Coding Lemma. In: Proceedings of the 38th Annual IEEE Symposium on Foundations of Computer Science, 1997, pp. 566-574. Chicago J. Theor. Comput. Sci. (1999), http://cjtcs.cs.uchicago.edu/

11. Rolf, D.: 3-SAT 2 RTIME(1 :32971n). In: ECCC TR03-054, 2003

12. Schoning, U.: A probabilistic algorithm fork-SAT based on limited local search and restart. Algorithmica 32, 615-623 (2002) (более ранняя версия публиковалась в источнике "40th Annual Symposium on Foundations of Computer Science (FOCS '99), pp. 410-414")