4446
правок
Точные алгоритмы решения задачи о выполнимости формулы в КНФ общего вида: различия между версиями
Материал из WEGA
Точные алгоритмы решения задачи о выполнимости формулы в КНФ общего вида (посмотреть исходный код)
Версия от 12:11, 9 июля 2020
, 9 июля 2020→Основные результаты
Irina (обсуждение | вклад) Нет описания правки |
Irina (обсуждение | вклад) |
||
| Строка 23: | Строка 23: | ||
Общий подход и граница для <math>\gamma</math> | Общий подход и граница для <math>\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/, выглядят следующим образом. | |||
'''Правила упрощения''' | |||
