4446
правок
Точные алгоритмы решения задачи о выполнимости формулы в КНФ общего вида: различия между версиями
Перейти к навигации
Перейти к поиску
Точные алгоритмы решения задачи о выполнимости формулы в КНФ общего вида (посмотреть исходный код)
Версия от 11:27, 24 июля 2020
, 24 июля 2020→Исключение переменной путем резолюции [7]
Irina (обсуждение | вклад) |
Irina (обсуждение | вклад) |
||
| Строка 72: | Строка 72: | ||
== '''''Исключение переменной путем резолюции [7]''''' == | == '''''Исключение переменной путем резолюции [7]''''' == | ||
Пусть имеется литерал a. Построить формулу | Пусть имеется литерал <math>a</math>. Построить формулу <math>DP_a(F)</math> следующим образом: | ||
1. добавить к F все резольвенты с a; | 1. добавить к F все резольвенты с <math>a</math>; | ||
2. удалить из F все дизъюнкты, содержащие a или | 2. удалить из F все дизъюнкты, содержащие <math>a</math> или <math>\neg a</math>. | ||
Правило: если | Правило: если <math>DP_a(F)</math> не больше в <math>m</math> (соответственно, в <math>l</math>), чем F, заменить F на <math>DP_a(F)</math>. | ||
'''''Исключение заблокированных дизъюнктов''''' | '''''Исключение заблокированных дизъюнктов''''' | ||
Дизъюнкт C является заблокированным для литерала a относительно F, если C содержит литерал a, а литерал | Дизъюнкт C является ''заблокированным'' для литерала <math>a</math> относительно F, если C содержит литерал <math>a</math>, а литерал <math>\neg a</math> встречается только в дизъюнктах F, содержащих отрицание по меньшей мере одного из литералов, встречающихся в C \ {<math>a</math>}. Для КНФ-формулы F и встречающегося в ней литерала <math>a</math> присваивание <math>I(a, F)</math> определяется как | ||
<math>\{ a \} \cup \{</math> литералы <math> x \notin \{ a, \neg a \} | </math> дизъюнкт <math>\{ \neg a, x \}</math> заблокирован для <math>\neg a</math> относительно <math>F \}</math>. | |||