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

Дано: формула 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>, выглядят следующим образом.

Для получения границы <math>|F|^{O(1)} \cdot 2^{0,10299l}</math> достаточно использовать пару <math>F[\neg a], F[I(a, F)]</math> подзадач (см. лемму 2(2)), обеспечивающую необходимое рекуррентное неравенство <math>t_l \le t_{l - 5} + t_{l + 17}</math>, и перейти к алгоритму с временем выполнения <math>|F|^{O(1)} \cdot 2^{0,30897m}</math>, если таковой нет. Недавнее и намного более технически сложное улучшение этого алгоритма [16] обеспечивает границу <math>|F|^{O(1)} \cdot 2^{0,0926l}.</math>

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

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

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