4446
правок
Точные алгоритмы решения задачи о выполнимости формулы в КНФ общего вида: различия между версиями
Материал из WEGA
Точные алгоритмы решения задачи о выполнимости формулы в КНФ общего вида (посмотреть исходный код)
Версия от 11:34, 24 июля 2020
, 24 июля 2020→Исключение переменной путем резолюции [7]
Irina (обсуждение | вклад) |
Irina (обсуждение | вклад) |
||
| Строка 70: | Строка 70: | ||
'''''Исключение переменной путем резолюции [7]''''' | |||
Пусть имеется литерал <math>a</math>. Построить формулу <math>DP_a(F)</math> следующим образом: | Пусть имеется литерал <math>a</math>. Построить формулу <math>DP_a(F)</math> следующим образом: | ||
| Строка 90: | Строка 90: | ||
'''Лемма 2''' (Куллман [11]) | '''Лемма 2''' (Куллман [11]) | ||
(1) Если дизъюнкт C заблокирован для литерала a относительно F, то F и F | (1) Если дизъюнкт C заблокирован для литерала a относительно F, то F и F \ {C} являются в равной мере выполнимыми. | ||
(2) Пусть имеется литерал a. Формула F является выполнимой в том и только том случае, если по меньшей мере одна из формул F[ | (2) Пусть имеется литерал <math>a</math>. Формула F является выполнимой в том и только том случае, если по меньшей мере одна из формул <math>F [ \neg a ]</math> и <math>F[I(a, F)]</math> является выполнимой. | ||
Первое утверждение леммы применяется в качестве правила упрощения. | Первое утверждение леммы применяется в качестве правила упрощения. | ||
| Строка 99: | Строка 99: | ||
'''''Применение принципа «черного и белого литералов»''''' | '''''Применение принципа «черного и белого литералов»''''' | ||
Пусть P – бинарное отношение между литералами и формулами в КНФ, такое, что для переменной v и формулы F выполняется не более чем одно из выражений P(v | Пусть P – бинарное отношение между литералами и формулами в КНФ, такое, что для переменной v и формулы F выполняется не более чем одно из выражений P(v, F) и P(<math>\neg</math> v, F). | ||
'''Лемма 3.''' Предположим, что каждый дизъюнкт F, содержащий литерал w, удовлетворяющий P(w | '''Лемма 3.''' Предположим, что каждый дизъюнкт F, содержащий литерал w, удовлетворяющий P(w, F), также содержит по меньшей мере один литерал <math>b</math>, удовлетворяющий <math>P(\neg b, F)</math>. Тогда <math>F</math> и <math>F[ \{ l | P( \neg l, F) \} ]</math> являются в равной мере выполнимыми. | ||
'''''Граница для <<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. | ||
