Синтаксическое дерево и допустимое дерево

Приведённое выше доказательство полноты метода резолюций становится нагляднее, если рассмотреть синтаксическое дерево.

Пусть в КНФ С входит п переменных …, х_п. Рассмотрим дизъюнкты вида {^1,…, ?*.}, где к ^ 0, а литерал.

ii — это переменная х или её отрицание. Совокупность таких дизъюнктов образует полное корневое бинарное дерево глубины п, которое и называется синтаксическим деревом. Корнем является пустой дизъюнкт, а у вершины {^?1,…, (^} есть два потомка: {fi,…, 4"*fc+i} и {?,…, 4," laifc+i};

Вершинами допустимого дерева для КНФ Т> являются те дизъюнкты указанного выше вида, которые не включают как множество ни одного дизъюнкта из V.

Чтобы наглядно представить себе эту конструкцию, нужно считать, что в каждой вершине ложен соответствующий ей дизъюнкт. Тогда недопустимые вершины — это те вершины, в которых мы можем утверждать ложность КНФ. На рис. 1.4 показаны примеры. Тонкими линиями на этих рисунках нарисованы ребра полного бинарного дерева, а толстыми — рёбра допустимых деревьев для указанных КНФ, вершины допустимых деревьев помечены точками.

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

Лемма 1.46. КНФ выполнима тогда и только тогда, когда допустимое дерево имеет, глубину п.

Доказательство. Пусть КНФ выполнима на наборе (од, 02, о_п). Тогда вершина, помеченная.

допустима, так как в каждом дизъюнкте КНФ должен найтись литерал х**^г. И в обратную сторону: если вершина.

допустима, то ни один дизъюнкт КНФ не содержится в множестве (1.15), следовательно, содержит хотя бы один литерал х¹?'. Это и означает выполнимость КНФ на наборе (1о_ь…, 1а_п). ?

Рис. 1.4. Примеры допустимых деревьев.

В доказательстве леммы 1.44 мы фактически строили самый левый путь глубины п для полного непротиворечивого множества дизъюнктов.