Точные алгоритмы решения задачи о выполнимости формулы в КНФ общего вида
Ключевые слова и синонимы
Задача выполнимости булевых формул (SAT)
Постановка задачи
Задача выполнимости (SAT) булевых формул в конъюнктивной нормальной форме (КНФ) является одной из первых NP-полных задач [2,13]. Поскольку NP-полнота в настоящее время не оставляет надежды на использование алгоритмов с полиномиальным временем выполнения, прогресс достигается за счет уменьшения показателя степени. Существует несколько версий этой параметризованной задачи, которые различаются параметром, используемым для оценки времени выполнения.
Задача 1 (SAT).
Дано: формула F в КНФ, содержащая n переменных, m дизъюнктов и l литералов.
Требуется: выдать «Да», если для F имеется присваивание, обеспечивающее выполнимость формулы, т. е. подстановку булевых значений переменных, с которой значение F становится истинным, и «Нет» в противном случае.
Границы времени выполнения алгоритмов SAT, таким образом, можно выразить в форме [math]\displaystyle{ |F|^{O(1)} \cdot \alpha^n, |F|^{O(1)} \cdot \beta^m }[/math] или [math]\displaystyle{ |F|^O(1) \cdot \gamma^l }[/math], где |F| – длина удовлетворительного битового представления F (т. е. формальных входных данных алгоритма). Фактически для существущих алгоритмов базы [math]\displaystyle{ \beta }[/math] и [math]\displaystyle{ \gamma }[/math] являются константами, а [math]\displaystyle{ \alpha }[/math] – функцией [math]\displaystyle{ \alpha(n, m) }[/math] от параметров формулы (поскольку не известно константы лучше [math]\displaystyle{ \alpha = 2 }[/math]).
Нотация
Формула в конъюнктивно-нормальной форме представляет собой набор дизъюнктов (понимаемый как конъюнкция этих дизъюнктов), дизъюнкт – набор литералов (понимаемый как дизъюнкция этих литералов), а литерал – либо булеву переменную, либо отрицание булевой переменной. Истинностное присваивание присваивает булевы значения (false или true) одной или нескольким переменным. Сокращенное присваивание представляет собой список литералов, которые при данном присваивании получают значение true (например, присваивание значения false переменной x и значения true – переменной y обозначается [math]\displaystyle{ \lnot x, y }[/math]). Результатом применения присваивания A к формуле F (обозначаемым F[A]) является формула, полученная удалением из F дизъюнктов, содержащих истинные литералы, и удалением ставших ложными литералов из оставшихся дизъюнктов. К примеру, если [math]\displaystyle{ F = (x \lor \lnot y \lor z) \land (y \lor \lnot z) }[/math], то [math]\displaystyle{ F[ \lnot x, y] = (z) }[/math]. Присваиванием, обеспечивающим выполнимость формулы F, называется присваивание A, такое, что F[A] = true. Если такое присваивание существует, формула F называется выполнимой.
Основные результаты
Границы для [math]\displaystyle{ \beta }[/math] и [math]\displaystyle{ \gamma }[/math]
Общий подход и граница для [math]\displaystyle{ \gamma }[/math]
Тривиальный алгоритм перебора, перечисляющий все возможные присваивания n переменным, выполняется за [math]\displaystyle{ 2^n }[/math] шагов с полиномиальным временем. Таким образом, [math]\displaystyle{ \alpha \le 2 }[/math]; по тривиальной причине [math]\displaystyle{ \beta, \gamma \le 2 }[/math]. В начале 80-х Мониен и Спекенмейер заметили, что [math]\displaystyle{ \beta }[/math] можно сделать меньше. //И они, и другие исследователи также отметили, что [math]\displaystyle{ \alpha }[/math] можно сделать меньше для специального случая задачи, в котором длина каждого дизъюнкта ограничена константой; соответствующие ссылки и алгоритмы см. в статье «Алгоритмы локального поиска для k-КНФ».//
Затем Куллманн и Лукхардт [12] разработали схему для алгоритмов SAT типа «разделяй и властвуй» //также называемых DPLL в силу его связи со статьями Дэвиса и Патнем [7] и Дэвиса, Логемана и Лавленда [6]//, которая разбивала исходную задачу на несколько (как правило, постоянное число) подзадач, подставляя значения некоторых переменных и упрощая полученные формулы. В результате этого исследования были получены следующие верхние пределы для [math]\displaystyle{ \beta }[/math] и [math]\displaystyle{ \gamma }[/math]:
Теорема 1 (Хирш [8]). Задачу SAT можно решить за время
1. [math]\displaystyle{ |F|^{O(1)} \cdot 2^{0,30897m}; }[/math]
2. [math]\displaystyle{ |F|^{O(1)} \cdot 2^{0,10299l}. }[/math]
Типичный алгоритм «разделяй и властвуй» для задачи SAT состоит из двух этапов: разбиение исходной задачи на несколько подзадач (например, редукция SAT(F) до SAT(F[x]) и SAT(F[[math]\displaystyle{ \lnot }[/math]x])) и упрощение полученных подзадач при помощи правил преобразования с полиномиальным временем работы, не влияющих на выполнимость подзадач (т.е. заменяющих формулу другой формулой, в равной мере выполнимой). Подзадачи [math]\displaystyle{ F_1, ..., F_k }[/math] для разбиения выбираются таким образом, чтобы соответствующее рекуррентное неравенство с упрощенными задачами [math]\displaystyle{ F'_1, ..., F'_k }[/math],
[math]\displaystyle{ T(F) \le \sum_{i=1}^k T(F'_i) + const, }[/math]
давало желаемую верхнюю границу по количеству листьев в дереве рекуррентности и, следовательно, по времени работы алгоритма. В частности, для получения границы [math]\displaystyle{ |F|^{O(1)} \cdot 2^{0,30897m} }[/math] необходимо решить либо две подзадачи F[x], F[[math]\displaystyle{ \lnot }[/math]x] с рекуррентным неравенством
[math]\displaystyle{ t_m \le t_{m - 3} + t_{m - 4} }[/math]
либо четыре подзадачи F[x, y], F[x, [math]\displaystyle{ \lnot }[/math]y], F[[math]\displaystyle{ \lnot }[/math]x, y], F[[math]\displaystyle{ \lnot }[/math]x, [math]\displaystyle{ \lnot }[/math]y] с рекуррентным неравенством
[math]\displaystyle{ t_m \le 2t_{m - 6} + 2t_{m - 7}, }[/math]
где [math]\displaystyle{ t_i = max_{m(G)\le i} T(G) }[/math]. Правила упрощения, используемые в алгоритмах со временем выполнения [math]\displaystyle{ |F|^{O(1)} \cdot 2^{0,30897m} }[/math] и [math]\displaystyle{ |F|^{O(1)} \cdot 2^{0,10299l} }[/math], выглядят следующим образом.
Правила упрощения
Исключение дизъюнктивных одночленов
Если F содержит дизъюнктивный одночлен (a), заменить F на F[a].
Категоризация
Если F содержит два дизъюнкта C и D, таких, что [math]\displaystyle{ C \subseteq D }[/math],заменить F на F \ {D}.
Резолюция с категоризацией
Пусть имеются литерал [math]\displaystyle{ a }[/math] и дизъюнкты C и D, такие, что [math]\displaystyle{ a }[/math] является единственным литералом, удовлетворяющим обоим условиям [math]\displaystyle{ a\in C }[/math] и [math]\displaystyle{ \neg a \in D }[/math]. В этом случае дизъюнкция [math]\displaystyle{ (C \cup D) \backslash \{ a, \neg a \} }[/math] называется резольвентой с литералом [math]\displaystyle{ a }[/math] дизъюнктов C и D и обозначается R(C, D).
Правило: если [math]\displaystyle{ R(C, D) \subseteq D }[/math], заменить [math]\displaystyle{ F }[/math] на (F \ {D}) [math]\displaystyle{ \cup }[/math] {R(C, D)}.
Исключение переменной путем резолюции [7]
Пусть имеется литерал [math]\displaystyle{ a }[/math]. Построить формулу [math]\displaystyle{ DP_a(F) }[/math] следующим образом:
1. добавить к F все резольвенты с [math]\displaystyle{ a }[/math];
2. удалить из F все дизъюнкты, содержащие [math]\displaystyle{ a }[/math] или [math]\displaystyle{ \neg a }[/math].
Правило: если [math]\displaystyle{ DP_a(F) }[/math] не больше в [math]\displaystyle{ m }[/math] (соответственно, в [math]\displaystyle{ l }[/math]), чем F, заменить F на [math]\displaystyle{ DP_a(F) }[/math].
Исключение заблокированных дизъюнктов
Дизъюнкт C является заблокированным для литерала [math]\displaystyle{ a }[/math] относительно F, если C содержит литерал [math]\displaystyle{ a }[/math], а литерал [math]\displaystyle{ \neg a }[/math] встречается только в дизъюнктах F, содержащих отрицание по меньшей мере одного из литералов, встречающихся в C \ {[math]\displaystyle{ a }[/math]}. Для КНФ-формулы F и встречающегося в ней литерала [math]\displaystyle{ a }[/math] присваивание [math]\displaystyle{ I(a, F) }[/math] определяется как
[math]\displaystyle{ \{ a \} \cup \{ }[/math] литералы [math]\displaystyle{ x \notin \{ a, \neg a \} | }[/math] дизъюнкт [math]\displaystyle{ \{ \neg a, x \} }[/math] заблокирован для [math]\displaystyle{ \neg a }[/math] относительно [math]\displaystyle{ F \} }[/math].
Лемма 2 (Куллман [11])
(1) Если дизъюнкт C заблокирован для литерала a относительно F, то F и F \ {C} являются в равной мере выполнимыми.
(2) Пусть имеется литерал [math]\displaystyle{ a }[/math]. Формула F является выполнимой в том и только том случае, если по меньшей мере одна из формул [math]\displaystyle{ F [ \neg a ] }[/math] и [math]\displaystyle{ F[I(a, F)] }[/math] является выполнимой.
Первое утверждение леммы применяется в качестве правила упрощения.
Применение принципа «черного и белого литералов»
Пусть P – бинарное отношение между литералами и формулами в КНФ, такое, что для переменной v и формулы F выполняется не более чем одно из выражений P(v, F) и P([math]\displaystyle{ \neg }[/math] v, F).
Лемма 3. Предположим, что каждый дизъюнкт F, содержащий литерал w, удовлетворяющий P(w, F), также содержит по меньшей мере один литерал [math]\displaystyle{ b }[/math], удовлетворяющий [math]\displaystyle{ P(\neg b, F) }[/math]. Тогда [math]\displaystyle{ F }[/math] и [math]\displaystyle{ F[ \{ l | P( \neg l, F) \} ] }[/math] являются в равной мере выполнимыми.
Граница для [math]\displaystyle{ \gamma }[/math]
Для получения границы [math]\displaystyle{ |F|^{O(1)} \cdot 2^{0,10299l} }[/math] достаточно использовать пару [math]\displaystyle{ F[\neg a], F[I(a, F)] }[/math] подзадач (см. лемму 2(2)), обеспечивающую необходимое рекуррентное неравенство [math]\displaystyle{ t_l \le t_{l - 5} + t_{l - 17} }[/math], и перейти к алгоритму с временем выполнения [math]\displaystyle{ |F|^{O(1)} \cdot 2^{0,30897m} }[/math], если таковой пары нет. Недавнее и намного более технически сложное улучшение этого алгоритма [16] обеспечивает границу [math]\displaystyle{ |F|^{O(1)} \cdot 2^{0,0926l}. }[/math]
Граница для [math]\displaystyle{ \alpha }[/math]
В настоящее время нетривиальная константная верхняя граница для [math]\displaystyle{ \alpha }[/math] неизвестна. Однако, начиная с работы [14], были предложены любопытные неконстантные границы. Был разработан ряд рандомизированных и детерминированных алгоритмов, демонстрирующих последовательные улучшения. Лучшая на данный момент возможная граница достигается при помощи детерминированного алгоритма «разделяй и властвуй», применяющего следующую рекурсивную процедуру. Его идея заключается в дихотомии: либо каждый дизъюнкт входной формулы можно сократить до первых k литералов (тогда можно применить алгоритм k-КНФ), либо все эти литералы в одном из дизъюнктов можно считать ложными. Такой подход к сокращению дизъюнктов можно приписать Шулеру [15], который использовал его в рандомизированной форме. Следующая версия детерминированного алгоритма, достигающего лучшей известной границы как для детерминированных, так и для рандомизированных алгоритмов, приведена в [5]).
Процедура S
Дано: КНФ-формула F и положительное целое число k.
1. Предположим, формула F состоит из дизъюнктов [math]\displaystyle{ C_1, ..., C_m }[/math]. Заменим каждый дизъюнкт [math]\displaystyle{ C_i }[/math] дизъюнктом [math]\displaystyle{ D_i }[/math] следующим образом: если [math]\displaystyle{ |C_i| \gt k }[/math], выбрать любые k литералов в [math]\displaystyle{ C_i }[/math] и отбросить все остальные литералы; в противном случае оставить [math]\displaystyle{ C_i }[/math] неизменным, т. е. [math]\displaystyle{ D_i = C_i }[/math]. Обозначить полученную формулу как F'.
2. Проверить выполнимость формулы F' с помощью алгоритма k-КНФ с временем выполнения [math]\displaystyle{ m \cdot poly(n) \cdot (2 - 2/(k + 1))^n }[/math], определенного в работе [3].
3. Если формула F' является выполнимой, вывести «Формула выполнима» и остановить выполнение. В противном случае для каждого значения i выполнить следующее:
(а) Преобразовать F в [math]\displaystyle{ F_i }[/math] следующим образом:
11. Заменить [math]\displaystyle{ C_j }[/math] на [math]\displaystyle{ D_j }[/math] для всех j < i;
12. Присвоить всем литералам [math]\displaystyle{ D_i }[/math] значение false.
(б) Рекурсивно вызвать процедуру S для значений ([math]\displaystyle{ F_i }[/math], k).
4. Вернуть «Формула невыполнима».
Алгоритм вызывает процедуру S для исходной формулы и целочисленного параметра k = k * (m, n). Из наиболее точного анализа данного семейства алгоритмов, выполненного Калабро, Импальяццо и Патури [1], следует, что, предполагая, что m > n, можно получить следующую границу, приняв k(m, n) = 2 log(m/n) + const. (Эта явная граница не задана в [1] и выводится в [4].)
Теорема 4 (Данцин, Хирш [4]). Предполагая, что m > n, задачу SAT можно решить за время [math]\displaystyle{ |F|^{O(1)} \cdot 2^{n \big (1 - \frac{1}{O(log(m/n))} \big ) }. }[/math]
Применение
У задачи SAT множество приложений, однако упомянутые алгоритмы к ним не применимы напрямую.
Открытые вопросы
Основными нерешенными вопросами в данной области остаются доказательство наличия постоянной верхней границы на [math]\displaystyle{ \alpha \lt 2 }[/math], а также гипотетическое существование алгоритмов с временем выполнения [math]\displaystyle{ (1 + \varepsilon)^l }[/math] для произвольного малого [math]\displaystyle{ \varepsilon \gt 0 }[/math].
Можно провести анализ алгоритма «разделяй и властвуй» и даже автоматически генерировать правила упрощения [10]. Однако пока такой подход позволил получить новые границы только для (NP-полной) версии оптимизации 2-КНФ [9].
Экспериментальные результаты
Ван Цзюнь реализовал алгоритм, дающий границу для [math]\displaystyle{ \beta }[/math], и собрал некоторую статистику по количеству применений правил упрощения [17].
См. также
Литература
1. Calabro, C., Impagliazzo, R., Paturi, R.: A duality between clause width and clause density for SAT. In: Proceedings of the 21st Annual IEEE Conference on Computational Complexity (CCC 2006), pp. 252-260. IEEE Computer Society (2006)
2. Cook, S.A.: The Complexity of Theorem Proving Procedures. Proceedings of the Third Annual ACM Symposium on Theory of Computing, May 1971, pp. 151-158. ACM (2006)
3. Dantsin, E., Goerdt, A., Hirsch, E.A., Kannan, R., Kleinberg, J., Papadimitriou, C., Raghavan, P., Schoning, U.: A deterministic (2-2/(k+1))n algorithm for k-SAT based on local search. Theor. Comput. Sci. 289(1), 69-83 (2002)
4. Dantsin, E., Hirsch, E.A.: Worst-Case Upper Bounds. In: Biere, A., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. IOS Press (2008) To appear
5. Dantsin, E., Hirsch, E.A., Wolpert, A.: Clause shortening combined with pruning yields a new upper bound for deterministic SAT algorithms. In: Proceedings of CIAC-2006. Lecture Notes in Computer Science, vol. 3998, pp. 60-68. Springer, Berlin (2006)
6. Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Commun. ACM 5, 394-397 (1962)
7. Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7, 201 -215 (1960)
8. Hirsch, E.A.: New worst-case upper bounds for SAT. J. Autom. Reason. 24(4), 397-420 (2000)
9. Kojevnikov, A., Kulikov, A.: A New Approach to Proving Upper Bounds for MAX-2-SAT. Proceedings of the Seventeenth Annual ACM-SIAM Symposium on Discrete Algorithms (SODA 2006), pp. 11 -17. ACM, SIAM (2006)
10. Kulikov, A.: Automated Generation of Simplification Rules for SAT and MAXSAT. Proceedings of the Eighth International Conference on Theory and Applications of Satisfiability Testing (SAT 2005). Lecture Notes in Computer Science, vol. 3569, pp. 430^36. Springer, Berlin (2005)
11. Kullmann, O.: New methods for 3-{SAT} decision and worst-case analysis. Theor. Comput. Sci. 223(1 -2):1 -72 (1999)
12. Kullmann, O., Luckhardt, H.: Algorithms for SAT/TAUT decision based on various measures, preprint, 71 pages, http://cs-svr1. swan.ac.uk/csoliver/papers.html (1998)
13. Levin, L.A.: Universal Search Problems. Проблемы передачи информации 9(3), 265-266, (1973). In Russian. English translation in:Trakhtenbrot, B.A.: A Survey of Russian Approaches to Perebor (Brute-force Search) Algorithms. Annals of the History of Computing 6(4), 384-400 (1984)
14. Pudlak, P.: Satisfiability - algorithms and logic. In: Proceedings of the 23rd International Symposium on Mathematical Foundations of Computer Science, MFCS'98. Lecture Notes in Computer Science, vol. 1450, pp. 129-141. Springer, Berlin (1998)
15. Schuler, R.: An algorithm for the satisfiability problem of formulas in conjunctive normal form. J. Algorithms 54(1), 40-44 (2005)
16. Wahlstrom, M.: An algorithm for the SAT problem for formulae of linear length. In: Proceedings of the 13th Annual European Symposium on Algorithms, ESA 2005. Lecture Notes in Computer Science, vol. 3669, pp. 107-118. Springer, Berlin (2005)
17. Wang, J.: Generating and solving 3-SAT, MSc Thesis. Rochester Institute of Technology, Rochester (2002)