4446
правок
Точные алгоритмы решения задачи о выполнимости формулы в КНФ общего вида: различия между версиями
Перейти к навигации
Перейти к поиску
Точные алгоритмы решения задачи о выполнимости формулы в КНФ общего вида (посмотреть исходный код)
Версия от 11:20, 24 июля 2020
, 24 июля 2020→Основные результаты
Irina (обсуждение | вклад) |
Irina (обсуждение | вклад) |
||
| Строка 65: | Строка 65: | ||
'''''Резолюция с категоризацией''''' | '''''Резолюция с категоризацией''''' | ||
Пусть имеются литерал a и дизъюнкты C и D, такие, что a является единственным литералом, удовлетворяющим обоим условиям a | Пусть имеются литерал <math>a</math> и дизъюнкты C и D, такие, что <math>a</math> является единственным литералом, удовлетворяющим обоим условиям <math>a\in C</math> и <math>\neg a \in D</math>. В этом случае дизъюнкция <math>(C \cup D) \backslash \{ a, \neg a \}</math> называется ''резольвентой с литералом <math>a</math>'' дизъюнктов C и D и обозначается R(C, D). | ||
Правило: если R(C | Правило: если <math>R(C, D) \subseteq D</math>, заменить <math>F</math> на (F \ {D}) <math>\cup</math> {R(C, D)}. | ||
'''''Исключение переменной путем резолюции [ ]''''' | == '''''Исключение переменной путем резолюции [7]''''' == | ||
Пусть имеется литерал a. Построить формулу DPa(F) следующим образом | Пусть имеется литерал a. Построить формулу DPa(F) следующим образом | ||