4446
правок
Точные алгоритмы решения задачи о выполнимости формулы в КНФ общего вида: различия между версиями
Перейти к навигации
Перейти к поиску
м
Точные алгоритмы решения задачи о выполнимости формулы в КНФ общего вида (посмотреть исходный код)
Версия от 11:13, 24 июля 2020
, 24 июля 2020→Основные результаты
Irina (обсуждение | вклад) |
Irina (обсуждение | вклад) |
||
| Строка 20: | Строка 20: | ||
== Основные результаты == | == Основные результаты == | ||
Границы для <math>\beta</math> и <math>\gamma</math> | '''''Границы для <math>\beta</math> и <math>\gamma</math>''''' | ||
Общий подход и граница для <math>\gamma</math> | '''''Общий подход и граница для <math>\gamma</math>''''' | ||
| Строка 29: | Строка 29: | ||
Теорема 1 (Хирш [8]). Задачу SAT можно решить за время | '''Теорема 1 (Хирш [8]). Задачу SAT можно решить за время''' | ||
1. <math>|F|^{O(1)} \cdot 2^{0,30897m};</math> | 1. <math>|F|^{O(1)} \cdot 2^{0,30897m};</math> | ||
| Строка 53: | Строка 53: | ||
'''Правила упрощения''' | '''Правила упрощения''' | ||
'''Исключение дизъюнктивных одночленов''' | '''''Исключение дизъюнктивных одночленов''''' | ||
Если F содержит дизъюнктивный одночлен (a), заменить F на F[a] | Если F содержит дизъюнктивный одночлен (a), заменить F на F[a]. | ||
'''Категоризация''' | '''''Категоризация''''' | ||
Если F содержит два дизъюнкта C и D, таких, что | Если F содержит два дизъюнкта C и D, таких, что <math>C \subseteq D</math>,заменить F на F \ {D}. | ||
'''Резолюция с категоризацией''' | '''''Резолюция с категоризацией''''' | ||
Пусть имеются литерал a и дизъюнкты C и D, такие, что a является единственным литералом, удовлетворяющим обоим условиям a 2 C и :a 2 D. В этом случае дизъюнкция (C [ D) \ a; :ag называется резольвентой с литералом a дизъюнктов C и D и обозначается R(C; D). | Пусть имеются литерал a и дизъюнкты C и D, такие, что a является единственным литералом, удовлетворяющим обоим условиям a 2 C и :a 2 D. В этом случае дизъюнкция (C [ D) \ a; :ag называется резольвентой с литералом a дизъюнктов C и D и обозначается R(C; D). | ||
| Строка 70: | Строка 70: | ||
'''Исключение переменной путем резолюции [ ]''' | '''''Исключение переменной путем резолюции [ ]''''' | ||
Пусть имеется литерал a. Построить формулу DPa(F) следующим образом | Пусть имеется литерал a. Построить формулу DPa(F) следующим образом | ||
| Строка 81: | Строка 81: | ||
'''Исключение заблокированных дизъюнктов''' | '''''Исключение заблокированных дизъюнктов''''' | ||
Дизъюнкт C является заблокированным для литерала a относительно F, если C содержит литерал a, а литерал -43 встречается только в дизъюнктах F, содержащих отрицание по меньшей мере одного из литералов, встречающихся в C n fag. Для КНФ-формулы F и встречающегося в ней литерала a присваивание I(a;F) определяется как fa U {literals x <£ a; :agj the clause f:a;xg is blocked for :a wrt Fg : | Дизъюнкт C является заблокированным для литерала a относительно F, если C содержит литерал a, а литерал -43 встречается только в дизъюнктах F, содержащих отрицание по меньшей мере одного из литералов, встречающихся в C n fag. Для КНФ-формулы F и встречающегося в ней литерала a присваивание I(a;F) определяется как fa U {literals x <£ a; :agj the clause f:a;xg is blocked for :a wrt Fg : | ||
| Строка 95: | Строка 95: | ||
'''Применение принципа «черного и белого литералов»''' | '''''Применение принципа «черного и белого литералов»''''' | ||
Пусть P – бинарное отношение между литералами и формулами в КНФ, такое, что для переменной v и формулы F выполняется не более чем одно из выражений P(v; F) и P(:v; F). | Пусть P – бинарное отношение между литералами и формулами в КНФ, такое, что для переменной v и формулы F выполняется не более чем одно из выражений P(v; F) и P(:v; F). | ||
| Строка 103: | Строка 103: | ||
Граница для <<math>\gamma</math> | '''''Граница для <<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. | Для получения границы 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. | ||
Граница для <math>\alpha</math> | '''''Граница для <math>\alpha</math>''''' | ||
В настоящее время нетривиальная константная верхняя граница для a неизвестна. Однако, начиная с работы [ ], были предложены любопытные неконстнатнеы границы. Был разработан ряд рандомизированных и детерминированных алгоритмов, демонстрирующих последовательные улучшения. Лучшая на данный момент возможная граница достигается при помощи детерминированного алгоритма «разделяй и властвуй», применяющего следующую рекурсивную процедуру. Его заключается в дихотомии: либо каждый дизъюнкт входной формулы можно сократить до первых k литералов (тогда можно применить алгоритм k-КНФ), либо все эти литералы в одном из дизъюнктов можно считать ложными. Такой подход к сокращению дизъюнктов можно приписать Шулеру [ ], который использовал его в рандомизированной форме. Следующая версия детерминированного алгоритма, достигающего лучшей известной границы как для детерминированных, так и для рандомизированных алгоритмов, приведена в [5]). | В настоящее время нетривиальная константная верхняя граница для a неизвестна. Однако, начиная с работы [ ], были предложены любопытные неконстнатнеы границы. Был разработан ряд рандомизированных и детерминированных алгоритмов, демонстрирующих последовательные улучшения. Лучшая на данный момент возможная граница достигается при помощи детерминированного алгоритма «разделяй и властвуй», применяющего следующую рекурсивную процедуру. Его заключается в дихотомии: либо каждый дизъюнкт входной формулы можно сократить до первых k литералов (тогда можно применить алгоритм k-КНФ), либо все эти литералы в одном из дизъюнктов можно считать ложными. Такой подход к сокращению дизъюнктов можно приписать Шулеру [ ], который использовал его в рандомизированной форме. Следующая версия детерминированного алгоритма, достигающего лучшей известной границы как для детерминированных, так и для рандомизированных алгоритмов, приведена в [5]). | ||
| Строка 137: | Строка 137: | ||
Теорема 4 (Данцин, Хирш [ ]). Предполагая, что m > n, задачу SAT можно решить за время | '''Теорема 4 (Данцин, Хирш [ ]). Предполагая, что m > n, задачу SAT можно решить за время''' | ||
== Применение == | == Применение == | ||