Поиск поддерева в дереве

From
Dmitriy Krylov ()
To
All
Date
2002-10-25T07:13:39Z
Area
RU.ALGORITHMS
From: "Dmitriy Krylov" <krylov@mail.primorye.ru>

Привет всем!

  Вот, занимаюсь подсистемой вывода для одной программки.

  Подсистема делает следующее: есть куча формул (в простейшем случае это
математико-логические выажения), есть правила преобразования. Преобразования
применяются к формулам.

Например, есть две формулы:

  (z + 2 > sqrt(v)) => (x | y)  // здесь | обозначает бул. опер. "или",
  not(x & not(y | v)) | z       //  а => - "импликация"


и такие три правила:

  1. x => y      -->   x | not(y)
  2. not(x & y)  -->   not(x) | not(y)
  3. not(x | y)  -->   not(x) & not(y)

После их (частичного) применения может получиться следующее:

  (z + 2 > sqrt(v)) | (not(x) & not(y)) // преобразование первой
                                        // формулы (правила 1, 3)

  not(x & (not(y) & not(v))) | z       // преобразование второй формулы



Возникает проблема применения правила к формулам, и (!) определения
применимости
того или иного правила преобразования к формулам.

Причем, перед применением правила
к формуле, необходимо сначала обнаружить возможность применимости. "Мест", в
которых может применяться одно и то же правило в пределах одной формулы -
несколько (например, для второй формулы правило 3 может применяться и для
подформулы not(y | v) [получиться not(y) & not(v)] и для подформулы not(x &
not(y | v)) [получиться not(x) | not(not(y | v))]). Полученные "места"
используются в других модулях проги для выбора способа наиболее оптимального
преобразования выражений.

Я решал эту проблему просто представлением формул в виде деревьев, а
правил - в виде двух деревьев. Это очевидно - вот пример представления
второй формулы:

                     |(или)
                    / \
                 not  z
                  |
                  &
                 / \
                x  not
                    |
                    | (или)
                    /\
                   y  v


Деревья представлены были в виде ссылочных структур, типа такой:

type
  TBinaryTree = class(TAbstractTree) // пример для би
    ...
    Left: TAbstractTree;
    Right: TAbstractTree;
    ...
  end;

В формулах попадаются более сложные подформулы - напр., кванторы по
нескольким переменным, так что деревья могут иметь много (больше, чем два)
потомков.

Нужно отметить, что значения формул (но не подформул) - логические. Всё
множество формул называется "моделью" и истинно (если хоть одна формула
оказывается ложной - модель считается противоречивой и дальнейшая обработка
прекращается). Поэтому формулы всех деревьев можно объеденить в одно дерево,
связав их операцией "и". То есть задача преобразования деревьев сводится к
преобразованию одного дерева.

Поиск "места" применения правила сводиля к поиску подходящего для правила
части формулы. Или поддерева (части формулы) в дереве (формулы) по
шаблонному дереву (правилу).

Поиск производился простым спуском по дереву модели и сверкой с _выбранным_
шаблоном (т.е. правилом). Если корень текущего поддерева совпадал с корнем
шаблона, происходило дальнейшее сравнение шаблона и поддерева (и, в случае
успеха, унификация - т.е. замена переменных шаблона на подформулы), если же
сравнение было неудачным - происходил переход к другому (не "обойденному")
поддереву в дереве моделей. Нужны все возможные вхождения.

Очевидно, что такой алгоритм - линейный (O(n*m) ~ O(n), где n - количество
узлов в дереве модели, m - количество узлов в дереве правила).

-------------------------------------------

Ну вот.

Пока модели (набор формул) и правила были маленькие (50-100 формул, в каждой
из них 10-20 подформул (узлов в дереве)), все было хорошо и быстро.

Но сейчас ситуация изменилась. Количество формул возросло до 5000 - 10000,
увеличилась их длина, правил стало тоже больше. Былая быстрота прошла.

All!! Посоветуйте:

1) лучшую структу для формул и правил - для более быстрого поиска (на память
можно забить - с условием, что деревья поместяться в ~128Mb, т.е. не будет
своппинга на многих системах)

2) лучший алгоритм обхода дерева и поиска применимости правила. Критерий -
скорость.

3) пункт 2 + для _всех_ правил.

4) пункты 2 и 3 с поиском не всех поддеревьев, а первого попавшегося.

Мои соображения следующие:

1) С каждым узлом поддерева можно связать множество операций (типов узлов),
встречающихся в поддереве, например, для той же второй формулы:


                        |(или)            [not, |, &]
                  /                \
                 not [&, not, |]    z []
                  |
                  &  [&, not, |]
                /  \
              x[]  not [not, |]
                    |
                    | (или) [|]
                   / \
                 y[]  v[]

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

Плохо, что количество операций может быть тоже велико - и эффективное
представление множества битовоми массивами приводит к большому потреблению
памяти.

Этот подход здорово ускорил подсистему вывода (например, при рассмотрении
правила 1 вообще не понадобится обход дерева - нужно лишь взглянуть на
первый элемент), но скорость все равно осталась маленькой (например, правила
2 и 3 приведут к полному обходу дерева). Тут интересно отметить, что у
дерева моделей множество, связанное с корнем оказывается почти полным, а
ближе к листьям начинает "редеть", так что при проверке правила всё равно
приходится обойти часть дерева (ту, что ближе к корню).

Интересно, есть ли какая-либо характеристическая функция - H(формула,
правило), -  которая бы __очень__ эффективно определяла, стоит ли
_пробовать_ искать "место" применения правила. Если эта функция выдает
false - искать вхождения не нужно, если true - Ok, ищем (можно даже старыми
методами).

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

Например (для формулы 2),

|   - <указатель1, ур.1>, <указатель2, ур. 5>
&   - <указатель3, ур.3>
not - <указатель4, ур.2>, <указатель5, ур. 4>


                     |(или)            уровень 1
                    / \
                 not  z                уровень 2
                  |
                  &                    уровень 3
                 / \
                x  not                 уровень 4
                    |
                    | (или)            уровень 5
                    /\
                   y  v                уровень 6

У каждого правила тоже есть такой список операций, указателей и уровней.

Можно попытаться выбрать порядок следования операций такой, чтобы он
совпадал с порядком в шаблоне. Если не удается - ну, что ж, не судба..., но
если удается, то можно продолжить дальнейшие раскопки. Причем найденный
порядок следования примерно указывает, где искать.

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

-------------------------------------------

Заранее спасибо.

P.S. Приношу извинения за столь длинный текст.

__________________________________________________
--{ Dmitriy Krylov aka "Abulafia"   }-------------
--{ mailto: krylov@mail.primorye.ru }-------------


--- ifmail v.2.15dev5
 * Origin: Demos online service (2:5020/400)