Упорядоченные бинарные диаграммы решений

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

Таблица 1

п/п	Фамилия	Имя	Отчество	Пол	ID-код
1	Дериев	Игорь	Сергеевич	М	1246
2	Егорова	Елена	Дмитриевна	Ж	7133
3	Ермак	Станислав	Олегович	М	6588
4	Зорянский	Виктор	Николаевич	М	3972
5	Карманова	Екатерина	Геннадьевна	Ж	783
6	Матюшенко	Татьяна	Станиславовна	Ж	2854
7	Пиваев	Геннадий	Петрович	М	1769
8	Чутов	Валерий	Семенович	М	4087

Таблица №1 состоит из 6 полей:

“№ п/п” - номер записи в порядке возрастания. Тип - счётчик.

“Фамилия” - фамилия сотрудника. Тип - текстовый.

“Имя” - имя сотрудника. Тип - текстовый.

“Отчество” - отчество сотрудника. Тип - текстовый.

“Пол” - пол сотрудника. Тип - текстовый.

“ID код” - уникальный идентификационный номер, присвоенный каждому сотруднику. Тип - числовой. Ключевое поле базы данных. С его помощью осуществляется связь таблиц между собой.

Таблица №2.

№ п/п	Дата рождения	Дата отпуска	Образование	Стаж	ID-код
1	11.09.1981	12.03.2005	Высшее	2 года	1246
2	01.03.1967	27.07.2005	Среднее	18 лет	7133
3	30.11.1980	23.08.2005	Среднее	6 лет	6588
4	22.03.1951	11.12.2004	Высшее	34 года	3972
5	07.10.1973	19.11.2005	Высшее	11 лет	783
6	12.12.1978	07.02.2005	Среднее	8 лет	2854
7	20.06.1969	30.04.2005	Высшее	15 лет	1769
8	03.08.1979	09.11.2005	Среднее	16 лет	4087

Таблица №2.

Таблица №2 состоит из полей:

“№ п/п” - поле аналогичное первой таблице.

“Дата рождения” - дата рождения. Тип - числовой. Формат - дата.

“Дата отпуска” - дата последнего отпуска, взятого сотрудником.

“Образование” - степень законченного образования.

“Стаж” - общий трудовой стаж, не зависимо от места работы.

“ID код” - поле аналогичное первой таблице.

Запрос к базе данных осуществляется в SQL и УБДР режимах. Программная реализация осуществлена в среде Borland C++ Builder 6.0 и состоит в описании событий, которые являются результатом определенного воздействия на одну из компонент формы, так как Borland C++ Builder 6.0 дает возможность использовать готовые формы с добавлением необходимых компонент. Выбирая запрос1 (SQL - режим) и запрос2 (УБДР - режим), реализуется пошаговое выполнение соответствующего запроса и результат выдается в виде графической информации.

Эксперименты проводились при использовании компьютера с одной и той же конфигурацией. За единицу скорости выполнения взято значение 1000000 операций в секунду. Ясно, что в зависимости от размера базы данных меняется и скорость выполнения различных операций при её использовании. Чем больше размер БД, тем медленнее они выполняются и тем мощнее должна быть конфигурация компьютера для обеспечения приемлемой скорости выполнения различных действий. В ходе экспериментов измерялось количество времени, затрачиваемое на выполнение запросов различной сложности в БД отличных размеров в SQL и УБДР режимах.

В таблице 4.1 показана зависимость времени выполнения запроса от количества информации, содержащейся в базе данных при выполнении стандартного SQL-запроса. Количество записей в каждой следующей строке увеличивается от 10 тыс. до 100000 тыс.

Таблица 4.1. Время выполнения стандартного SQL запроса.

	Количество переменных в запросе 1 2 3 4 5
Время выполнения запроса (секунд)	0,1	0,4	0,9	1,6	2,5
	1	4	9	16	25
	10	40	90	160	250
	100	400	900	1600	2500
	1000	4000	9000	16000	25000

Учитывая данные таблицы легко заметить экспоненциальный рост времени выполнения запроса в зависимости от количества записей и переменных в запросе. Рассмотрим выполнение аналогичных запросов, но при использовании УБДР для их реализации.

Таблица 4.2. Время выполнения запроса с УБДР реализацией.

	Количество переменных в запросе 1 2 3 4 5
Время выполнения запроса (секунд)	0,1	0,1-0,4	0,1-0,9	0,1-1,6	0,1-2,5
	1	0,2-4	0,3-9	0,4-16	0,5-25
	10	2-40	3-90	4-160	5-250
	100	20-400	30-900	40-1600	50-2500
	1000	200-4000	240-9000	400-16000	500-25000

В таблице 4.2 указано 2 значения времени выполнения запроса - минимальное и максимальное. При сравнении результатов из таблицы 4.1 видно, что максимальное время выполнения осталось прежним, а значит, использование УБДР не влияет отрицательно на скорость выполнения запросов, а минимальное время показывает насколько можно сократить время выполнения запроса при УБДР реализации. Например, при выполнении запроса, содержащего 1000 тыс. записей и 5 переменных минимальное время выполнения составило 5 секунд вместо 250 - выигрыш во времени в 50 раз!

Заключение

В данной работе сформулированы основные понятия УБДР и операции на УБДР, которые помогают привести УБДР к наиболее удобному виду, показана зависимость размера дерева решений от заданного порядка переменных.

В работе рассматривается знаменитая шахматная задача о восьми ферзях (задача Гаусса). Производится анализ всевозможных комбинаций фигур, являющихся решением задачи, предлагается необходимая формализация условий, результатом которой является булева функция. Она является конъюнкцией всех необходимых условий. Значение “истина” полученной функции соответствует искомой комбинации расположения шахматных фигур на доске. В приложении к диплому описаны программные модули на языке Pascal, позволяющие построить БДР для этой задачи, редуцировать её - получить УБДР.

В дипломной работе демонстрируется пример сжатия чёрно-белого изображения при помощи УБДР. Производится формализация условий, строится УБДР. Данный пример возможно перенести и для сжатия цветных изображений. Для этого надо:

Осуществить усреднение интенсивностей пикселей в изображении.

Для каждого цвета ввести свой идентификатор - построить карту цветов.

Карту цветов разбить на сектора по цветам так, чтобы каждый сектор имел свой идентификатор.

Каждый сектор сжать по аналогии с чёрно-белым изображением.

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

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

Список литературы

1. Евстигнеев В.А., Касьянов В.Н. Теория графов (алгоритмы обработки деревьев) // Новосибирск Наука -1994.-250с.

2. Капитонов Ю. В., Кривой С.Л., Летичевский О. А., Луцкий Г.М., Печурин М. К. Основы дискретной математики // Киев Наукова Думка -2002.-180с.

3. Виноградов А.А. Математическая энциклопедия // М. Наука -1985.-С.220-235

4. Новиков П.С. Элементы математической логики // М. Наука -1973.-С.28-45

5. Bryant R.E. Symbolic Boolean Manipulation wiht Odered Binary Decision Diagrams // Scool of Computer Science Carnegi Mellon University -1992.-P.145-148

6. Burch J.R., Clarke E. M., McMillan K. I. Symbolic model checking: state and beyond // Fifth Annual IEEE Symposium on Logic in Computer Science (Philodelphia, June). IEEE, New York. -1990.-P.12-19

7. McMilan K. I. Symbolyc Model Checking: an approach to state explosion problem // PhD thesis, Scool of Computer Science, Carnegi Melonn University, -1992.-P.28-30

Приложение

Реализация создания УБДР и операции над ними на языке Pascal

Создание дерева решений

uses crt;

type

pnode=^node;

node=record

one:pnode;

zero:pnode;

prev:pnode;

index:integer;

zn:integer;

end;

var

q,z,p:pnode;

i,n:integer;

function build(i,t:integer):pnode;

begin

if i>n then

begin

new(q);

q^.one:=nil;

q^.zero:=nil;

q^.index:=i;

q^.zn:=t;

q^.prev:=p;

{Теперь необходимо подсчитать значение полученной терминальной вершины}

end

else

begin

new(q);

q^.prev:=p; p:=q;

q^.index:=i;

q^.zn:=t;

q^.one:=build(i+1,1);

q^.zero:=build(i+1,0);

end;

end;

begin

clrscr;

new(q);

q^.index:=1;

q^.prev:=nil;

p:=q;

q^.one:=build(1,1);

q^.zero:=build(1,0);

readkey;

end.

Подсчитав значения терминальных вершин, можно осуществить СЛД (склеивание листков дубликатов).

Пусть q - это текущая терминальная вершина:

Term1^.one:=nil; Term1^.zero:=nil;

Term0^.one:=nil; Term0^.zero:=nil;

Term1^.func:=1;Term0^.func:=0;

If q^.zn=1 then

{Терминальная вершина является правым сыном}

If q^.func =1 then

Begin

q:=q^.prev;

dispose(q^.one);

q^.one:=term1;

term1^.prev:=q;

end

Else

begin

q:=q^.prev;

dispose(q^.one);

q^.one:=term0;

term0^.prev:=q;

end

Else {Терминальная вершина является левым сыном}

If q^.func =1 then

Begin

q:=q^.prev;

dispose(q^.zero);

q^.zero:=term1;

end

Else

begin

q:=q^.prev;

dispose(q^.zero);

q^.zero:=term0;

end

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

Склеивание внутренних вершин дубликатов (СВВД): если внутренние вершин z1 и z2 дерева решений такие, что , то исключаем одну из этих вершин и переориентируем все входящие дуги на вторую вершину, которая осталась.

Z - текущая переменная;

If (q1^.index= q2^.index) and (q1^.one=q2^.one) and(q1^.zero=q2^.zero) then

begin

Z:=q2^.prev;

If q2^.zn=1 then

Z^.one:=q1

Else

Z^.zero:=q1;

End;

Исключение лишних тестов (ИЛТ): если внутренняя вершина v такая, что , то исключаем вершину v и переориентируем все входящие дуги на вершину .

Пусть z - текущая переменная ;

If z^.one=z^.zero then

Begin

R:=z^.prev

If z^.zn:=1 then

begin

R^.one:=z^.zero;

Z^.one^.prev:=r;

Dispose(z);

End;

Else

begin

R^.zero:=z^.zero;

Z^.one^.prev:=r;

Dispose(z);

End;

End;

Сужение функции.

q - текущая переменная

Сужение функции относительно переменной q для q=1

q^.zero:=q^.one;

z:=q^.one;

dispose(q);

Сужение функции относительно переменной q для q=0

q^.one:=q^.zero;

z:=q^.zero;

dispose(q);