Точные алгоритмы решения задачи о выполнимости формулы в КНФ общего вида
Ключевые слова и синонимы
Задача выполнимости булевых формул (SAT)
Постановка задачи
Задача выполнимости (SAT) булевых формул в конъюнктивной нормальной форме (КНФ) является одной из первых NP-полных задач [2,13]. Поскольку NP-полнота в настоящее время не оставляет надежды на использование алгоритмов с полиномиальным временем выполнения, прогресс достигается за счет уменьшения показателя степени. Существует несколько версий этой параметризованной задачи, которые различаются параметром, используемым для оценки времени выполнения.
Задача 1 (SAT).
Дано: формула F в КНФ, содержащая n переменных, m дизъюнктов clauses и 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 переменным, выполняется за 2n шагов с полиномиальным временем. Таким образом, a < 2, а по тривиальным причинам и f$,y < 2. В начале 1980-х Мониен и Спекенмейер заметили, что /3 можно сделать меньше1. Затем Куллманн и Лукхардт [12] разработали схему для алгоритмов SAT типа «разделяй и властвуй2», которая разбивала исходную задачу на несколько (как правило, постоянное число) подзадач, подставляя значения некоторых переменных и упрощая полученные формулы. В результате этого исследования были получены следующие верхние пределы для f$ и y.
1 И они, и другие исследователи также заметили, что a можно сделать меньше для специального случая задачи, в котором длина каждого дизъюнкта ограничена константой; соответствующие ссылки и алгоритмы см. в статье «Алгоритмы локального поиска для k-КНФ».
2 Этот алгоритм также носит название DPLL в связи со статьями Дэвиса и Патнем [7] и Дэвиса, Логемана и Лавленда [6].
Теорема 1 (Хирш [ ]). Задачу SAT можно решить за время
1. jFjO(1). 2°:30897m;
2. jFjO(1) • 20:10299
Типичный алгоритм «разделяй и властвуй» для задачи SAT состоит из двух этапов: разбиение исходной задачи на несколько подзадач (например, редукция SAT(F) до SAT(F[x]) и SAT(F[:x])) и упрощение полученных подзадач при помощи правил преобразования с полиномиальным временем работы, не влияющих на выполнимость подзадач (т.е. заменяющих формулу другой формулой, в равной мере выполнимой). Подзадачи F1, ..., Fk для разбиения выбираются таким образом, чтобы соответствующее рекуррентное неравенство с упрощенными задачами F[,..., Fk0, к T(F) < X T(Fi0) + const ;
давало желаемую верхнюю границу по количеству листьев в дереве рекуррентности и, следовательно, по времени работы алгоритма. В частности, для получения границы jFjO(1) • 2°:30897m необходимо решить либо две подзадачи F[x]; F[:x] с рекуррентным неравенством
tm < tm-3 + fm-4 ]; F[:x;
либо четыре подзадачи F[x;y]; F[x; :y] с рекуррентным неравенством
tm < 2fm_6 + 2fm_7
где ti = maxm(G)<; T(G). Правила упрощения, используемые в алгоритмах со временем выполнения |F|°«.20-30897m и |F|o«.20-10299/, выглядят следующим образом.
Правила упрощения