5.1.7. Алгоритмы распознавания невыполнимости формулы

а) Алгоритмы, основанные на использовании дерева частичных интерпретаций

Некоторые алгоритмы анализа невыполнимости формулы используют семантическое дерево. Если задано конечное множество элементарных высказываний P = { ,…, }, входящих в формулу, то семантическое дерево – это бинарное дерево, удовлетворяющее следующим условиям:

1. Каждая дуга помечена позитивной или негативной литерой из P.

2. Литеры, помечающие дуги, инцидентные одной и той же вершине, противоположны.

3. Простая цепь, соединяющая корень дерева с его листом, не содержит более одного вхождения каждой литеры.

4. Простая цепь, соединяющая корень дерева с его листом, не содержит противоположных литер и представляет одну из полных интерпретаций i формулы.

Каждой вершине v семантического дерева сопоставляется частичная интерпретация. Если в простой цепи, соединяющей эту вершину с корнем дерева, присутствует дуга, помеченная символом p (p), то в частичной интерпретации этой вершины элементарному высказыванию p (p) приписывается значение и (л). Считается, что частичная интерпретация не определена на p, если ни одна дуга рассматриваемой простой цепи не помечена литерами p (p).

Семантическое дерево является полным, если каждой простой цепи, соединяющей его корень с листом, соответствует всюду определенная интерпретация i. Иначе семантическое дерево является неполным.

Полное семантическое дерево представляет всевозможные интерпретации формулы А, содержащей множество P элементарных высказываний.

Для проверки невыполнимости формулы А можно построить для нее полное семантическое дерево и подсчитать значение истинности для каждой интерпретации. Эта процедура аналогична построению таблицы истинности для формулы А.

Однако совсем не обязательно просматривать все полные интерпретации для проверки невыполнимости формулы.

КАДР

Алгоритм Квайна

Идея алгоритма заключается в следующем. Если при всех возможных расширениях частичной интерпретации до полных формула А принимает одно и то же значение истинности, то нет необходимости перебирать эти полные интерпретации. Вершина, которой сопоставляется рассматриваемая частичная интерпретация, объявляется листом дерева и ей приписывается соответствующее значение истинности.

Алгоритм.

1. Элементарные высказывания некоторым образом упорядочиваются.

2. Выполняется раскрытие очередной вершины, начиная с корня, с целью построения дерева частичных интерпретаций в соответствии с выбранным порядком элементарных высказываний.

3. Для каждой вновь полученной вершины и соответствующей ей частичной интерпретации проверяется, принимает ли формула А значение л (и). Если формула А принимает значение и, переходим к п. 4 алгоритма. Если формула А принимает значение л, вершину объявляем концевой и переходим к раскрытию оставшихся вершин. Если все вершины раскрыты, переходим к п. 5 алгоритма. Если формула на рассматриваемой частичной интерпретации не принимает значения л (и), переходим к п. 2.

4. Формула А выполнима, переходим к п. 6.

5. Формула А не выполнима.

6. Работа алгоритма закончена.

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

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

1. Исключить связки , , воспользовавшись тождествами:

p  q = p  q, p  q = pq  pq.

2. Применить многократно правила Де Моргана с тем, чтобы опустить инверсии со скобок на символы элементарных высказываний.

3. Применить многократно дистрибутивный закон:

p  (q  r) = (p  q)(p  r).

4. Исключить дизъюнкты, содержащие противоположные литеры, так как они общезначимы.

5. Заменить повторяющиеся в дизъюнкте литеры одной литерой.

Проиллюстрируем сказанное примером:

(p  (q  r))  ((p  s)  r),

(p  (q  r))  ((p  s)  r),

 (p  (q  r))  ( (p  s)  r),

 (p  (q  r))  ( (p  s)  r),

(p   (q  r))  (p  s  r),

p  q  r  p  s  r,

(p  p  s  r)(q  p  s  r)( r  p  s  r),

q  p  s  r.

Итак, исходная формула ложна на единственной интерпретации:

q, r = л, p, s = и.

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

КНФ в дальнейшем будем рассматривать как множество дизъюнктов S = ={ ,…, }.

Опишем раскрытие вершины в алгоритме Квайна, используя КНФ.

Выберем некоторое элементарное высказывание p формулы А. Множество S разбивается на три подмножества:

– множество дизъюнктов, содержащих p,

– множество дизъюнктов, содержащих p,

= S /{  },

получается из вычеркиванием литеры p,

получается из вычеркиванием литеры p.

Теорема 5.1. Множество S не выполнимо, если и только если не выполнимы два множества:  и  .

Доказательство следует из того факта, что рассматриваемые множества получаются из S фиксированием значения p (p = и, p = л соответственно).

При раскрытии вершины, двигаясь по дуге p, сопоставляем новой вершине выражение  , двигаясь по дуге p, сопоставляем новой вершине выражение  .

Дерево частичных интерпретаций можно сократить в следующих ситуациях:

1. При наличии в множестве дизъюнктов, сопоставляемом внутренней вершине (в том числе корню), однобуквенных дизъюнктов p (p).

2. В случае однородности множества дизъюнктов по литере p (p). Множество дизъюнктов однородно по литере p (p), если дизъюнкты не содержат литеру p (p).

В обоих случаях при раскрытии вершины из нее исходит единственная дуга, помеченная литерой p (p). Напомним, что речь идет о проверке КНФ на невыполнимость.

КАДР

б) Резольвентный метод проверки невыполнимости КНФ

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

Пусть А, В, С – формулы исчисления высказываний. Предположим, что две формулы (А  С) и (В  С) истинны на одних и тех же интерпретациях. Если С тоже истинна на этих интерпретациях, то В истинна на них. Если С – ложна, то – А истинна. Формально имеем

{ А  С, В  С} |= A  B. (3)

В частном случае, когда А и В – дизъюнкты, а С – элементарное высказывание, правило (3) называется правилом резолюций.

Теорема 5.2. Пусть , – дизъюнкты КНФ, представленной множеством S, а l – литера. Если l из , а l из , то дизъюнкт r =( / {l})  ( / {l}) есть логическое следствие множества S дизъюнктов.

Доказательство следует из введенного ранее определения резольвенты.

Следствие. КНФ, представленные множествами S и S  r, эквивалентны.

Дизъюнкт r называется резольвентой дизъюнктов и .

Заметим, что операция резолюции двойственна операции обобщенного склеивания, выполняемой над элементарными дизъюнкциями. Это значит, что выполнив всевозможные поглощения дизъюнктов в множестве S, мы можем далее воспользоваться методом Блейка, с той лишь разницей, что операция обобщенного склеивания заменяется на операцию резолюции.

Проиллюстрируем сказанное примером:

S = {p, p  q, p  r, q  r}. Выполнив операцию резолюции для первого и второго дизъюнктов с одновременным поглощением одного из них, имеем

{p, q, p  r, q  r}.

Выполнив операцию резолюции для первого и третьего дизъюнктов в новом множестве, получим

{p, q, r, q  r}.

Выполнив операцию резолюции для второго и четвертого дизъюнктов в полученном выражении, имеем

{p, q, r, r}.

Операция резолюции над r, r порождает пустой дизъюнкт, то есть л.

Напомним, что объем вычислений при реализации метода Блейка растет экспоненциально с ростом числа переменных, то есть в нашем случае числа элементарных высказываний, составляющих формулу, и, следовательно, далеко не всегда может быть применен на практике. Однако резольвентный подход оказывается эффективным при описании предметной области хорновскими дизъюнктами.

КАДР