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

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

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

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

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

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

Рассмотрим два преобразования кодового дерева (рис. 4.2).

1. Удаление ребра, исходящего из вершины с порядком ветвления один.

Пусть в кодовом дереве, порожденном схемой Σ, содержится вершина порядка 1, из которой исходит ровно одна дуга, заканчивающаяся концевой вершиной дерева (листом), и пусть концевой вершине приписана вероятность ρ.

a) Удалим это ребро.

b) Припишем величину ρ вершине, из которой оно исходило. Получим новое кодовое дерево, представляющее схему кодирования .Новое кодовое дерево имеет меньшую избыточность. Действительно, = – ρ.

2. Перемещение ребра в ненасыщенную вершину более близкого к корню яруса по сравнению с вершиной, из которой это ребро исходило, или в вершину того же яруса.

Рассмотрим некоторую вершину дерева кодирования, порожденного схемой Σ, из которой исходит ребро, заканчивающееся в концевой вершине. Концевой вершине приписана величина ρ и соответствует кодовое слово B.

a) Перенесем это ребро вместе с концевой вершиной в ненасыщенную вершину того же яруса или более близкого к корню яруса.

b) Припишем концевой вершине величину ρ. Получим новое кодовое дерево, представляющее схему .

Новое кодовое дерево имеет не большую избыточность. Действительн, при перенесении ребра в ненасыщенную вершину того же яруса избыточность кодового дерева сохраняется. При перенесении ребра в ненасыщенную вершину, расположен ближе к корню, избыточность нового кодового дерева уменьшается.

Определение. Конечное дерево называется насыщенным, если порядки ветвления всех его вершин, за исключением, быть может, одной, лежащей в предпоследнем ярусе, равны 0 или q. Порядок ветвления этой исключительной вершины равен , где 2 £ £ q.