5.7.2. Алгоритм Куайна для днф

Алгоритм Куайна для ДНФ позволяет проверить выполнимость и общезначимость приведенной дизъюнктивной нормальной формы.

Пусть р – элементарное высказывание, а S – приведенная ДНФ, которая может быть представлена в виде:

S= S_p S_{ p}  (S_р\ S^_p),

где S_p – дизъюнкты, содержащие высказывание р;

S_{ p} – дизъюнкты, содержащие р;

S^_p = (S\(S_p S_{ p})).

Алгоритм

1. Если S = , то S – выполнима.

2. Если S = F, то S – невыполнима.

3. Иначе:

а) выбирается p, входящее в S;

б) определяются множества S_p, S_{ p}, S^_p;

в) получение S^_p из S_p удалением р;

г) получение S^ _{ p} из S_{ p} удалением  p .

S – невыполнимо тогда и только тогда, когда невыполнимы два множества (S^_pS^_р) и (S^_{ p} S^_р). Если р – Т, то S  (S^_{ p}  S^_р), если р – F, то S  (S^_p S^_р).

{F, r}- не выполняется.

5.7.3. Принцип резолюций

В исчислении высказываний не существует общего, по-настоящему эффективного критерия для проверки выполнимости КНФ, однако есть удобный метод для выявления невыполнимости множества дизъюнктов.

Множество дизъюнктов S не выполнимо тогда и только тогда, когда логическое следствие из него есть пустой дизъюнкт, т. е. дизъюнкт, всегда принимающий значение F. Таким образом, невыполнимость множества дизъюнктов S можно проверить, порождая логические следствия из него до тех пор, пока не получится пустой дизъюнкт.

Для порождения логических следствий используется следующая схема рассуждений. Пусть A, B, X – формулы. Предположим, что (АХ) и (ВХ) – истинны. Если Х принимает значение Т, то В также принимает значение Т. Если Х принимает значение F, то А принимает значение Т. Следовательно, АВ принимает значение Т.

То есть, {А Х, ВХ} ├ АВ, или {Х А, Х В}├ АВ, где Х – высказывание, а А и В – дизъюнкты. Это правило резолюций.

Лемма. Пусть S₁, S₂ – дизъюнкты нормальной формы S, l – литера. Если l S₁ и  l S₂, то r = (S₁\{l})  (S₂\{l}), называется резольвентой дизъюнктов S₁ и S₂ и является логическим следствием нормальной формы S.

Следствие. Нормальные формы S и S{r} логически эквивалентны.

Алгоритм доказательства невыполнимости логической формулы

1. Если в формуле нет невыполнимых дизъюнктов, то выбираются l, S₁ и S₂, такие, что l S₁ и  l S₂.

2. Строится резольвента r.

3. Заменяется S на S{r}.

4. Процесс повторяется до порождения пустого дизъюнкта, это означает, что формула невыполнима.

Пример. Доказать невыполнимость следующего множества дизъюнктов S={pq, pr, qr, p}.

Упорядочим множество S: S={pq, pr, qr, p}.

1 2 3 4

Строим резольвенты для дизъюнктов, допускающих построение резольвенты:

5. (1, 3) pr;

6. (1, 4)  q;

7. (2, 3) p q;

8. (2, 4) r;

9. (2, 5) p;

10. (4, 5) r;

11. (4, 9) F.

Замечания:

1. Если множество S не содержит ни одной пары дизъюнктов, допускающих резольвенту, то оно выполнимо.

2. Если выполнение алгоритма закончилось порождением пустого дизъюнкта, то установлена невыполнимость исходного S.

3. Может случиться, что выполнение алгоритма не завершится.

Применение метода резолюций означает построение соответствующего семантического дерева снизу вверх.