Точные алгоритмы решения задачи о выполнимости формулы в КНФ общего вида: различия между версиями

Дано: формула F в КНФ, содержащая n переменных, m дизъюнктов clauses и l литералов.

Требуется: выдать «Да», если F содержит присваивание, обеспечивающее выполнимость формулы, т. е. подстановку булевых значений переменных, с которой значение F становится истинным, и «Нет» в противном случае.

Границы времени выполнения алгоритмов SAT, таким образом, можно выразить в форме <math>|F|^{O(1)} \cdot \alpha^n, |F|^{O(1)} \cdot \beta^m</math> или <math>|F|^O(1) \cdot \gamma^l</math>, где |F| – длина удовлетворительного битового представления F (т. е. формальных входных данных алгоритма). Фактически для существущих алгоритмов базы <math>\beta</math> и <math>\gamma</math> являются константами, а <math>\alpha</math> – функцией <math>\alpha(n, m)</math> от параметров формулы (поскольку не известно лучшей константы, чем <math>\alpha = 2</math>).

Формула в конъюнктивно-нормальной форме представляет собой набор дизъюнктов (понимаемый как конъюнкция этих дизъюнктов), дизъюнкт – набор литералов (понимаемый как дизъюнкция этих литералов), а литерал – либо булеву переменную, либо отрицание булевой переменной. Истинностное присваивание присваивает булевы значения ('''false''' или '''true''') одной или нескольким переменным. Сокращенное присваивание представляет собой список литералов, которые при данном присваивании получают значение '''true''' (например, присваивание значения '''false''' переменной x и значения '''true''' – переменной y обозначается <math>\lnot x, y</math>). Результатом применения присваивания A к формуле F (обозначаемым F[A]) является формула, полученная удалением дизъюнктов, содержащих истинные литералы из F, и удалением ставших ложными литералов из оставшихся дизъюнктов. К примеру, если <math>F = (x \lor \lnot y \lor z) \land (y \lor \lnot z)</math>, то <math>F[ \lnot x, y] = (z)</math>. Присваиванием, обеспечивающим выполнимость формулы F, называется присваивание A, такое, что F[A] = true. Если такое присваивание существует, формула F называется ''выполнимой''.

Тривиальный алгоритм перебора, перечисляющий все возможные присваивания n переменным, выполняется за <math>2^n</math> шагов с полиномиальным временем. Таким образом, <math>\alpha \le 2</math>; по тривиальной причине <math>\beta, \gamma \le 2</math>. В начале 80-х Мониен и Спекенмейер заметили, что <math>\beta</math> можно сделать меньше. ''//И они, и другие исследователи также отметили, что a можно сделать меньше для специального случая задачи, в котором длина каждого дизъюнкта ограничена константой; соответствующие ссылки и алгоритмы см. в статье «Алгоритмы локального поиска для k-КНФ».//''

Затем Куллманн и Лукхардт [12] разработали схему для алгоритмов SAT типа «разделяй и властвуй» ''//также называемых DPLL в связи со статьями Дэвиса и Патнем [7] и Дэвиса, Логемана и Лавленда [6]//'', которая разбивала исходную задачу на несколько (как правило, постоянное число) подзадач, подставляя значения некоторых переменных и упрощая полученные формулы. В результате этого исследования были получены следующие верхние пределы для <math>\beta</math> и <math>\gamma</math>:

давало желаемую верхнюю границу по количеству листьев в дереве рекуррентности и, следовательно, по времени работы алгоритма. В частности, для получения границы <math>|F|^{O(1)} \cdot 2^{0,30897m};</math> необходимо решить либо две подзадачи F[x], F[<math>\lnot</math>x] с рекуррентным неравенством

где <math>t_i = max_{m(G)\le i} T(G)</math>. Правила упрощения, используемые в алгоритмах со временем выполнения <math>|F|^{O(1)} \cdot 2^{0,30897m};</math> и <math>|F|^{O(1)} \cdot 2^{0,10299l}.</math>, выглядят следующим образом.

== '''''Исключение переменной путем резолюции [7]''''' ==

(1) Если дизъюнкт C заблокирован для литерала a относительно F, то F и F nfCg являются в равной мере выполнимыми.

(2) Пусть имеется литерал a. Формула F является выполнимой в том и только том случае, если по меньшей мере одна из формул F[:a] и F[I(a; F)] является выполнимой.

Пусть P – бинарное отношение между литералами и формулами в КНФ, такое, что для переменной v и формулы F выполняется не более чем одно из выражений P(v; F) и P(:v; F).

'''Лемма 3.''' Предположим, что каждый дизъюнкт F, содержащий литерал w, удовлетворяющий P(w; F), также содержит по меньшей мере один литерал b, удовлетворяющий P(:b;F). Тогда F и F[fljP(:l;F)g] являются в равной мере выполнимыми.

'''''Граница для <<math>\gamma</math>'''''

Для получения границы jFjO(1) • 20:10299l достаточно использовать пару F[:a]; F[I(a; F)] подзадач (см. лемму 2(2)), обеспечивающую необходимое рекуррентное неравенство tl < f,_5 + f;_17, и перейти к алгоритму с временем выполнения jFjO(1) • 2°:30897m, если таковой нет. Недавнее и намного более технически сложное улучшение этого алгоритма [16] обеспечивает границу jFjO(1) • 2°:0926l.

В настоящее время нетривиальная константная верхняя граница для a неизвестна. Однако, начиная с работы [ ], были предложены любопытные неконстнатнеы границы. Был разработан ряд рандомизированных и детерминированных алгоритмов, демонстрирующих последовательные улучшения. Лучшая на данный момент возможная граница достигается при помощи детерминированного алгоритма «разделяй и властвуй», применяющего следующую рекурсивную процедуру. Его заключается в дихотомии: либо каждый дизъюнкт входной формулы можно сократить до первых k литералов (тогда можно применить алгоритм k-КНФ), либо все эти литералы в одном из дизъюнктов можно считать ложными. Такой подход к сокращению дизъюнктов можно приписать Шулеру [ ], который использовал его в рандомизированной форме. Следующая версия детерминированного алгоритма, достигающего лучшей известной границы как для детерминированных, так и для рандомизированных алгоритмов, приведена в [5]).

1. Предположим, формула F состоит из дизъюнктов C1, ..., Cm. Заменим каждый дизъюнкт Ci дизъюнктом Д следующим образом: если j C i j  > k, выбрать любые k литералов в Ci и отбросить все остальные литералы; в противном случае оставить Ci неизменным, т. е. Di = Ci. Обозначить полученную формулу как F0.

2. Проверить выполнимость формулы F0 с помощью алгоритма k-КНФ с времерем выполнения m ■ poly(n) • (2 — 2/ (k + 1))n, определенного в работе [3].

3. Если формула F0 является выполнимой, вывести «Формула выполнима» и остановить выполнение. В противном случае для каждого значения i выполнить следующее:

(а) Преобразовать F в Fi следующим образом:

11.  Заменить Cj на Dj для всех j < i;

12. Присвоить всем литералам Д значение false.

(б) Рекурсовно вызвать процедуру S на (Fi, k).

Алгоритм вызывает процедуру S для исходной формулы и целочисленного параметра k = k * (m, n). Из наиболее точного анализа данного семейства алгоритмов, выполненного Калабро, Импальяццо и Патури [ ], следует, что, предполагая, что m > n, можно получить следующую границу, приняв k(m; n) = 2log(m/n) + const. (Эта явная граница не задана в [ ] и выводится в [4].)

'''Теорема 4 (Данцин, Хирш [ ]). Предполагая, что m > n, задачу SAT можно решить за время'''

Основными нерешенными вопросами в данной области остаются доказательство наличия постоянной верхней границы на a < 2, а также гипотетическое существование алгоритмов с временем выполнения (1 + ") для произвольного малого " > 0. Можно провести анализ алгоритма «разделяй и властвуй» и даже автоматически генерировать правила упрощения [10]. Однако пока такой подход позволил получить новые границы только для (NP-полной) версии оптимизации 3-КНФ [9].

Ван Цзюнь реализовал алгоритм, дающий границу для f$, и собрал некоторую статистику по количеству применений правил упрощения [17].