автореферат диссертации по информатике, вычислительной технике и управлению, 05.13.11, диссертация на тему:Исследование и разработка алгоритмов параллельного дедуктивного вывода на графовых структурах

На правах рукописи

Аверин Андрей Игоревич

ИССЛЕДОВАНИЕ И РАЗРАБОТКА АЛГОРИТМОВ ПАРАЛЛЕЛЬНОГО ДЕДУКТИВНОГО ВЫВОДА НА ГРАФОВЫХ СТРУКТУРАХ

Специальность 05.13.11 - Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей

АВТОРЕФЕРАТ

диссертации на соискание ученой степени кандидата технических наук

Москва-2004

Работа выполнена на кафедре Прикладной математики Московского энергетического института (Технического университета)

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

Вадим Николаевич Вагин

Официальные оппоненты:

доктор технических наук, профессор

Эдуард Викторович Попов

кандидат физико-математических наук, профессор

Геральд Станиславович Плесневич

Ведущая организация: Институт программных систем РАН

Защита состоится «24» декабря 2004 г. в {$ час. 00 мин. на заседании диссертационного совета Д 212.157.01 при Московском энергетическом институте (Техническом университете) по адресу: 111250, Москва, Красноказарменная ул., 17 (ауд. Г-306).

С диссертацией можно ознакомиться в библиотеке Московского энергетического института (Технического университета).

Отзывы в двух экземплярах, заверенные печатью, просьба направлять по адресу: 111250, г. Москва, Красноказарменная улица, д. 14, Ученый Совет МЭИ (ТУ).

Автореферат разослан «23» ноября 2004 г.

Ученый секретарь

диссертационного совета Д 212.157.01 кандидат технических наук, профессор

И.И. Ладыгин

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ Актуальность темы исследований. В настоящее время алгоритмы дедуктивного вывода находят широкое применение в системах принятия решений, дедуктивных базах данных, информационно-поисковых системах. В числе других областей использования дедуктивного вывода можно также назвать верификацию спецификаций компьютерного оборудования (процедуры дедуктивного вывода использовались, например, при верификации процессоров компании AMD), проверку корректности систем безопасности, анализ корректности протоколов передачи данных.

Значительный вклад в разработку и исследование алгоритмов дедуктивного вывода внесли Дж. Робинсон (J.A. Robinson), М. Дэвис (М. Davis), X. Патнэм (Н. Putnam), Р. Ковальски (R. Kowalski), А. Кольмрауэр (A. Colmerauer), В Бибель (W. Bibel), А. Банди (A. Bundy), У. Бледсоу (W. Bledsoe), Л. Воc (L Wos), П. Гилмор (P. Gilmore), Д. Лавлэнд (D. Loveland), У. МакКьюн (W McCune), X. Ольбах (Н. Ollbach), М. Стикель (М. Stickel), P. Шостак (R Shostak), Э. Эдер (Е. Eder), Н. Эйзингер (N. Eisinger), А.Воронков, СЮ Маслов, В.Н. Вагин.

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

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

В работах Д. Паурса (D. Powers) и Р. Логанантхараджа (R. Loganantharaj) было показано, что использование параллелизма в алгоритмах вывода, основанных на графовых структурах, позволяет существенно повысить эффективность работы алгоритмов. Таким образом, исследование и разработка алгоритмов параллельного дедуктивного вывода на графовых структурах является актуальной задачей.

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

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

БИблмотекА J

структуры. Необходимо отметить, что

6Я

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

Основными требованиями, предъявляемыми к процедуре параллельного дедуктивного вывода, являются:

1. Использование эффективного способа представления термов. Термы логики предикатов первого порядка являются основной структурой обработки в процедурах вывода, и их неэффективное представление ведет к неэффективной работе процедуры в целом.

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

3. Использование эффективной стратегии поиска. Резольвирование дизъюнктов является основной операцией в процедурах дедуктивного вывода, и неэффективный выбор дизъюнктов для резольвирования приводит к практической непригодности процедуры вывода.

4. Использование эффективной стратегии распараллеливания. Данную проблему необходимо решать совместно с проблемой выбора эффективной стратегии поиска.

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

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

Научная новизна. Новыми являются:

1. Способ представления термов логики предикатов первого порядка, предназначенный для использования в процедурах параллельного вывода на графовых структурах.

2. Метод построения множества связей для DCDP-параллельного вывода, позволяющий повысить эффективность DCDP-параллельного вывода.

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

4. Комплексный подход к распараллеливанию процесса вывода, объединяющий в себе OR, AND и DCDP параллелизм.

Практическая значимость. Практическая значимость работы заключается в создании программной системы, в рамках которой реализованы алгоритмы OR, AND и DCDP параллельного вывода на графовых структурах.

Практическая значимость работы подтверждается использованием разработанных алгоритмов в системе диагностики, реализованной в рамках интегрированной системы управления предприятием SAP R/3, о чем имеетсч

акт о внедрении, а также результатами работы алгоритма при решении тестовой задачи «Стимроллер».

Реализация результатов. Разработанный алгоритм был реализован в рамках системы диагностики, представляющей собой надстройку над стандартной функциональностью интегрированной системы управления предприятием SAP R/3 и используемой для ускорения процесса диагностики и устранения неисправностей, возникающих во время работ по инсталляции, системной настройке и системному администрированию системы в НПО «Мекомп».

Результаты диссертационной работы Аверина А.И. вошли в отчеты по НИР, выполняемым кафедрой ПМ по грантам РФФИ № 99-01-00049, № 02-07-90042 по теме «Исследование и разработка инструментальных средств создания экспертных систем семиотического типа», а также в учебном процессе при изучении дисциплины «Математическая логика».

Апробация работы. Основные положения и результаты диссертации докладывались и обсуждались на 6-й, 7-ой, 8-ой, 9-ой и 10-ой научных конференциях аспирантов и студентов «Радиотехника, электроника, энергетика» в МЭИ (ТУ) (г. Москва, 2000 - 2004 г.г.), на 4-ой международной летней школе-семинаре по искусственному интеллекту для студентов и аспирантов (Браславская школа) (Беларусь, г. Браслав, 1999 г.), на «Научных сессиях МИФИ» (г. Москва, 2000 - 2004 г.г.), на 7-й национальной конференции по искусственному интеллекту с международным участием КИИ'2000 (г. Переславль-Залесский, 2000 г.), международном форуме МФИ-2003 (Международные конференции «Информационные средства и технологии») (г. Москва, 2003), на Международной научно-технической конференции «Интеллектуальные системы» AIS'03 (Россия, п. Дивноморское, 2003 г.) и международной конференции JCKBSE - 2004 (Россия, г. Переславль-Залесский, 2004г., доклад на английском языке).

Публикации. Основные результаты, полученные при выполнении диссертационной работы, опубликованы в 18 печатных работах.

Структура и объем работы. Диссертация состоит из введения, четырех глав, заключения, списка использованной литературы (72 наименования) и приложений. Диссертация содержит 139 страниц машинописного текста (без приложений).

Содержание работы

Во введении обоснована актуальность темы, сформулирована цель работы, рассмотрена структура и краткое содержание диссертации по главам.

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

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

последовательных алгоритмов дедуктивного вывода. Представлена предложенная М.П. Боначиной (М.Р. Bonacina) классификация стратегий распараллеливания, основным критерием которой является различие между параллелизмом на уровне термов, параллелизмом на уровне дизъюнктов и параллелизмом на уровне поиска.

На рис. 1 показано текущее состояние исследований в области параллельного доказательства теорем (пунктирными линиями показаны связи между видами параллелизма и классами стратегий, к которым эти виды параллелизма были применены).

Рис. 1. Применение стратегий распараллеливания к стратегиям последовательного дедуктивного вывода.

Как показано на рис.1, существуют недостаточно исследованные способы использования параллельных стратегий в дедуктивном выводе. Среди них можно отметить использование AND- и OR-параллелизма для упорядочивающих стратегий, что объясняется неудобством использования большинства упорядочивающих стратегий для одновременной обработки всех литер одного дизъюнкта (в случае AND-параллелизма) или одной литеры дизъюнкта (в случае OR-параллелизма). Однако это несправедливо для

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

Во второй главе рассматриваются вопросы, связанные с реализацией операции унификации в процедурах параллельного дедуктивного вывода. Операция унификации является наиболее часто выполняемой операцией в процедурах дедуктивного вывода. Таким образом, при реализации эффективных процедур вывода унификации следует уделить особое внимание. Классический алгоритм унификации, предложенный Дж. Робинсоном не может быть использован для задач практической сложности, так как он требует экспоненциальных затрат времени и памяти. Дж. Робинсоном было показано, что для создания более эффективных процедур унификации необходимо использование специальных структур для представления термов и создание эффективных алгоритмов для их обработки.

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

В настоящее время существует целый ряд алгоритмов унификации, которые используют различные представления термов. Наиболее известными являются алгоритмы, предложенные Мартелли и Монтанари (A. MartelU & U.Montanari), Юэ (G. Huet), Корбином и Бидуа (J. Corbin & М. Bidoit). Эти алгоритмы значительно более эффективны, чем алгоритм Робинсона (временная сложность алгоритма Мартелли и Монтанари составляет O(n+logm), где п - число термов, m - число различных переменных в термах, Хью — 0(па(п)) — где а(п)- крайне медленно растущая функция, Корбина и Бидуа -

Однако данные алгоритмы редко используются на практике, так как используемые структуры данных слишком сложны и плохо соответствуют структурам данных, обычно используемых в алгоритмах вывода, что приводит к дополнительным накладным расходам на перекодировку одного представления термов в другое. В современных доказателях теорем, таких как: Otter, SETHEO, SPASS, Vampire, Waldmeister, обычно используется следующий подход: используемые структуры представления термов достаточно просты (чаще всего это представление терма в виде плоского терма или в виде направленного ациклического графа), что объясняется удобством их применения в процедурах дедуктивного вывода. Для повышения эффективности процесса поиска унифицируемых дизъюнктов используются различные методы индексации множества дизъюнктов. Таким образом, работу алгоритма унификации можно разбить на два этапа. Первый этап заключается в

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

Одним из способов повышения эффективности процесса унификации является его распараллеливание. И хотя С. Дуорк (S. Dwork) было показано, что унификация не принадлежит к классу NC алгоритмов (то есть алгоритм унификации не может иметь вычислительную сложность 0(log nf при полиномиальном числе процессоров), в работах Дж. Виттера (J. Vitter) и М. Беллья (М. ВеШа) были выделены классы задач унификации, для которых сложность может быть оценена как - число

процессоров, Е — число ребер в графовом представлении терма, V - число вершин в графовом представлении. Многие проблемы, которые возникают в области автоматического доказательства теорем, относятся к этим классам. Таким образом, использование алгоритмов параллельной унификации может привести к повышению производительности алгоритмов параллельного дедуктивного вывода. Для достижения этой цели необходимо создание структуры представления термов, которая будет одинаково хорошо подходить как для реализации процедуры параллельного дедуктивного вывода, так и для реализации процедуры параллельной унификации.

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

таблицы, установки связей между строками таблицы и обработки полученного графа по определенным правилам. Пример построения таблицы для задачи унификации 8~{/(а,Ь)—г,/(г,Ь)=/([(а,Ь),х)} приведен на рис. 2.

Рис. 2. Представление задачи унификации с использованием предложенного способа представления термов.

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

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

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

При построении графа связей для последовательности дизъюнктов состоящих из предикатов каждому предикату

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

На рис. 3 представлен пример построения графа связей для множества дизъюнктов:

Рис. 3. Пример построения графа связей.

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

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

В работе рассмотрено три метода вывода: ОИ-параллельный вывод, ЛКВ-параллельный вывод и ВСВР-параллельный вывод.

В случае ОЯ-параллелизма производится одновременное резольвирование всех связей одной из литер дизъюнкта. При сопоставлении осуществляется унификация литер и генерация новых дизъюнктов по методу резолюции для предикатов первого порядка.

Для графа связей, изображенного на рис.3, допустимыми множествами OR-связей являются, например, {1',2'} и {Ю',1]'}.

Алгоритм OR-иараллельной резолюции включает в себя следующие этапы:

1. Выбор множества связей для OR-параллелъного резольвирования.

2. Параллельное резольвирование всех связей из выбранного множества. Удаление выбранных связей.

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

4. Если граф не содержит ни одного дизъюнкта, то неуспешное завершение алгоритма, иначе переход к пункту 1.

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

Одной из разновидностей параллельного вывода на графе связей Ковальского является DC-параллелизм (distinct clause parallelism). В случае DC-параллелизма резольвируются те связи, для которых дизъюнкты, соединенные этими связями, различны. В работе рассматривается ограниченный DC-параллелизм, сохраняющий логическую непротиворечивость. Такой параллелизм называется DCDP-параллелизмом (parallelism for distinct clauses, edge distinct pair).

Определение 1. Дизъюнкты называются смежными, если существует одна или несколько связей, соединяющих литеры одного с литерами другого.

Определение 2. Множеством DCDP-связей называется множество связей, которые соединяют пары различных дизъюнктов, если дизъюнкты каждой пары не являются смежными со всеми дизъюнктами остальных пар.

Для графа связей, изображенного на рис. 3, допустимыми множествами DCDP-связейявляются, например, {!', б', 9'}, {2', б', 12'}, {4\ 12'}, {1\б\ 10'}.

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

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

В работе представлена модификация процедуры нахождения множества DCDP-связей. Рассмотрим множество дизъюнктов S. Построим граф связей CG(S). Обозначим множество связей графа связей как CGusk(S).

Обозначим множество DCDP-связей графа как SETDcdp, & множество связсй, которые могут быть потенциально добавлены во множество как

SET avail-

Пусть SETavail = CGum(S); SETocdp = {}■

На первом шаге работы алгоритма производится оценка связей из множества связей SET avail по выбранному эвристическому критерию.

После оценивания связей производится сортировка по степени убывания значения оценки. Связь с наибольшим значением оценки - обозначим ее L -удаляется из множества связей SETavail и добавляется во множество связей SETDCDP- ИЗ множества связей SETavail также удаляются и все связи, соединяющие дизъюнкты, являющиеся смежными с дизъюнктами, которые соединяет связь L. Если множество SETavail не пусто, то происходит переход на шаг 1.

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

В случае AND-параллелизма одновременно резольвируются все связи одного дизъюнкта, называемого SUN-дизъюнктом. Доказана корректность AND-параллельной резолюции.

Для графа связей, изображенного на рис.3, допустимыми множествами AND-связей являются, например, {5', 4', 7'} (SUN-дизъюнкт - дизъюнкт 5) и {5', б'} (SUN-дизъюнкт - дизъюнкт 6).

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

Далее в главе рассмотрена задача создания эвристических функций оценки связи.

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

Этими принципами являются:

1) число литер в резольвируемых дизъюнктах должно быть по возможности минимальным;

2) число связей у резольвируемых дизъюнктов должно быть минимальным;

3) число связей у литер, по которым резольвируются дизъюнкты, должно быть минимальным;

4) НОУ резольвируемой связи должны иметь подстановки вида х—>с, где с -константный или функциональный терм, х - переменная.

Поясним смысл каждого из принципов.

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

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

Принцип (3) отдает предпочтение связям, резольвирование которых позволяет получить «чистые» дизъюнкты, удаление которых позволяет значительно упростить структуру графа связей.

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

Кроме того, при создании эвристической функции следует учитывать, что для обеспечения полноты вывода необходимо гарантировать, что любая связь графа должна быть, в конце концов, прорезольвирована. Для этого нужно увеличивать вес не резольвированных связей. Данный принцип было предложен К. Мюнхом (К. Munch) и называется принципом отсечения.

При разработке процедур вывода было проанализировано и испытано несколько возможных эвристических функций. В работе представлены результаты, полученные при использовании различных функций, проведено их сравнение. Разработана эвристическая функция H1, в которой учитываются все принципы (1)-(4), а также производится корректировка значений коэффициентов в процессе вывода. При создании эвристической функции H1 функция оценки связи была представлена как линейная комбинация функций оценки объектов, входящих в связь (унификатор связи, дизъюнкты и предикатные литеры, участвующие в связи).

Пусть WeightLink - значение эвристической оценки для связи. Тогда: WeightLink=kdame-(ClauseiHeur+Clause2HeJ+UniHem-kum+kpred-(PrediHeur+Pred2Heur),

где:

Clauseweur~ значение эвристической оценки первого дизъюнкта;

значение эвристической оценки второго дизъюнкта; значение эвристической оценки унификатора связи;

Ргес1шеиг — значение эвристической оценки предикатной литеры из первого дизъюнкта, участвующей в связи;

значение эвристической оценки предикатной литеры из второго дизъюнкта, участвующей в связи;

Кт, Кьша кргеЛ е[1;100] - произвольные коэффициенты.

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

аашвнеиг ~ к/ • СЬшеМитЬегО/ЬНегаЬ + к^ ■ С1аичеА'итЪегО/Ыпкх,

ОашеМитЬегО]Ыпкх — число связей дизъюнкта;

С1сшеМитЪег01Ьиега1$ - число предикатных литер дизъюнкта;

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

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

этом случае оба принципа (1) и (2) учитываются в одинаковой степени. Однако в процессе вывода значения характеристик могут изменяться. В этом случае первоначально выбранные значения коэффициентов «устаревают», и один из принципов получает больший вес, чем другой. Для того чтобы избежать подобной ситуации, необходимо изменять значения коэффициентов в процессе вывода. Введем следующие обозначения:

AverageLinkCount - среднее число связей для дизъюнкта;

AverageClauseLength - среднее число предикатных литер в дизъюнкте.

Тогда можно предложить следующие значения коэффициентов к/ и

В этом случае оба

принципа (1) и (2) учитываются в равной степени на протяжении всего процесса вывода. Окончательный вид эвристической функции оценки дизъюнкта:

Clauseнem-(ЛverageLinkCount/AverageClauseLength)■ClauseNumberOfLiterals+

Эвристическая оценка унификатора должна учитывать принцип (4) (унификаторы резольвируемой связи должны иметь подстановки вида где

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

Пусть - значение эвристической оценки для унификатора. Тогда

вычисляем значение {/иг«„.. следующим образом:

Uni|leur=AverageLinkCount/(l+NumberOfConstaníSubsí+NumberOfFuncSubst),

где МитЬегО/СоП51ап1зЗиЬ51 - число подстановок в унификаторе вида {х—> с}, где с - константный терм, а х- переменная;

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

Эвристическая оценка предикатной литеры должна учитывать принцип (3) и изменение характеристик графа.

Пусть Ргес1неиг - значение эвристической оценки для предикатной литеры. Тогда вычисляем значение Ргес1иеигследующим образом: Ргес1Неш. — Рге(ШитЪегОА-тЪ ■ AverageClauseLength, где - число связей предикатной литеры.

Коэффициенты кащ, кС1аи5е, крге!{ выбираются опытным путем. В работе были выбраны следующие отношения коэффициентов: к„т = (1/10)-кС!аше. При

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

Принцип отсечения учитывается в эвристической функции следующим образом: через каждые 20 шагов резольвирования происходит увеличение значений связей, созданных ранее, чем за 20 шагов резольвирования, и еще не прорезольвированных. На рис. 4 и рис. 5 представлены результаты сравнения результатов работы алгоритмов OR, AND и DCDP параллельного вывода при использовании рассмотренных в работе эвристических функций №1, №2 и Ш (функции №1 и №2 учитывают первые два принципа, корректировка значений коэффициентов в процессе вывода не производится).

Рис. 4. Изменение количества промежуточных дизъюнктов в зависимости от использованной функции оценки.

Рис.5. Изменение количества промежуточных унификаций в зависимости от использованной функции оценки.

Результаты сравнения показывают, что наилучшие результаты были показаны алгоритмом, использующим БСБР-параллелизм. Это объясняется структурой БСБР-параллельного вывода, при котором производится поиск доказательства сразу по нескольким направлениям, в различных областях пространства поиска, в то время как АКБ- и ОК параллелизм обрабатывают в текущий момент времени один дизъюнкт и одну литеру соответственно. Так как для сложных задач без использования помощи эксперта трудно определить направление вывода, то подход, используемый в БСБР-параллелиЗме, представляется более перспективным.

Разработанная функция H1 была реализована в рамках программного комплекса, способного осуществлять процесс ОЯ-, БСБР- и АКБ-параллелыюго вывода на графе связей В рамках комплекса реализована также процедура последовательного вывода и алгоритм параллельной унификации, представленный во второй главе работы. Для контроля над процессом эффективности вывода используется блок мониторинга, собирающий информацию об эффективности процесса вывода. Схема программного комплекса изображена на рис. 6.

Рис. 6. Схема программного комплекса

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

1) сложность математического анализа эффективности;

2) отсутствие эталонного набора примеров для тестирования и сравнения параллельных алгоритмов вывода;

3) различия в понимании исследователями анализируемых показателей эффективности (что считать шагом вывода, промежуточным дизъюнктом, успешной унификацией);

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

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

В работе рассматривается следующий подход к анализу эффективности: в первой части главы приводятся результаты сравнения работы параллельного алгоритма вывода на графе связей с алгоритмом, предложенным М. Стикелем. Данный алгоритм выбран для сравнения вследствие схожести характеристик (оба алгоритма используют граф связей). Сравнение производится на тестовой задаче Стимроллер. Задача «Стимроллер» характеризуется экспоненциальным ростом пространства поиска, поэтому для эффективной работы при решении данной задачи, процедура вывода должна, во-первых, по возможности сокращать множество дизъюнктов и, во-вторых, выбирать наилучшие, или близкие к наилучшим, связи для резольвирования. (Под наилучшими связями мы понимаем связи, резольвирование по которым приближает нас к решению задачи). Далее, на задаче «Стимроллер», приводится сравнение параллельной версии алгоритма с наиболее эффективными алгоритмами других авторов.

Таблица 1

Сравнение результатов работы параллельных алгоритмов вывода с __алгоритмом Стикеля__

Вид параллелизма Кол-во полученных дизъюнктов Кол-во успешных унификаций Длина доказательства

Алгоритм Стикеля 4518 245829 205

DCDP 2320 2200 110

AND 2545 11000 165

OR 2600 3500 135

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

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

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

Таблица 2

Сравнение результатов работы алгоритмов параллельного вывода на графе

связей с наиболее эффективными алгоритмами других исследователей

Процедура вывода Количество успешных унификаций Количество шагов вывода

Stickel/CG-SOS-TR 2494 160

Stickel/CG-TR 477 25

McCune/UR 6050 38

McCune/LUR 1106 23

DCDP вывод на графе связей 2195 110

AND вывод на графе связей 11061 135

OR вывод на графе связей 3523 165

Последовательный вывод на графе связей 8034 181

(CG - стратегия вывода с использованием графа связей

SOS - вывод на графе связей с использованием целевого утверждения, как множества поддержки.

TR - вывод с использованием теории связей (Theory Links) - расширения стандартного метода резолюции.

UR - Вывод с использованием юнитной резолюции - модификации метода резолюции

LUR - Вывод с использованием связанной юнитной резолюции - модификации метода UR -резолюции)

Результаты сравнения показывают, что наилучшие результаты были получены при использовании процедуры McCune/LUR. Процедуры параллельного вывода на графе связей показали, что их эффективность

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

В заключении приведены основные результаты, полученные в диссертационной работе.

Основные результаты работы

1. Разработан комплексный подход к решению задачи создания эффективной процедуры вывода, основанного на применении параллелизма на уровне термов и параллелизма на уровне дизъюнктов (OR-, AND- и DCDP параллелизм).

2. Представлена структура представления термов, которая может быть использована в параллельных процедурах вывода.

3. Разработан алгоритм параллельной унификации, использующий представленную структуру представления термов.

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

5. Разработана эвристическая функция, позволяющая повысить эффективность параллельной процедуры вывода.

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

СПИСОК РАБОТ, ОПУБЛИКОВАННЫХ ПО ТЕМЕ ДИССЕРТАЦИИ

1. Аверин А.И. Алгоритмы дедуктивного вывода на графе связей. Параллельный вывод на графе связей//Третья международная школа-семинар по искусственному интеллекту для студентов и аспирантов (Браславская школа - 1999): Сборник научных трудов. -Минск: БГУИР, 1999. - С.155-157.

2. Аверин А.И., Вагин В.Н. Разработка алгоритмов дедуктивного вывода в системах принятия решений//Радиоэлектроника, электротехника и энергетика. Шестая Междунар. науч.-техн.конф. студентов и аспирантов; Тезисы докл. В 3-х т.~ Т. 1.-М.:МЭИ,2000.-С.214.

3. Аверин А.И., Вагин В.Н., Хамидулов М.К. Исследование алгоритмов параллельного вывода на задаче "Стимроллер'7/Известия Академии Наук. Теория и системы управления. - 2000. - №5. - С. 92-100.

4. Аверин А.И., Вагин В.Н., Хамидулов М.К. Исследование алгоритмов параллельного вывода на задаче "Стимроллер"//Международный журнал вычислительной техники и системотехники, Перевод журнала «Известия РАН. Теория и системы управления». — 2000. - Т. 39, №. 5 - С. 758-766-(на англ. яз.).

5. Аверин А.И., Вагин В.Н., Хамидулов М.К. Методы параллельного вывода на графовых структурах//Седьмая национальная конференция по искусственному интеллекту с международным участием (КИИ 2000). - Т.1. -М.: ФизМатЛит, 2000. - С.181-189.

6. Аверин А.И., Вагин В.Н. Методы параллельного дедуктивного вывода на графах связей//Научная сессия МИФИ - 2001. Сборник научных трудов. В 14 томах. -Т.З. -М.:МИФИ, 2001. - С. 200-201.

7. Аверин А.И., Вагин В.Н. Реализация алгоритмов дедуктивного вывода на графах связей//Радиоэлектроника, электротехника и энергетика. Седьмая

N222 7 0 3

Междунар. науч.-техн.конф. студентов и аспирантов; Тезисы докл. В 3-х т. -Т.1.-М.:МЭИ,2001. -С. 386.

8. Аверин А.И., Вагин В.Н. Параллелизм в дедуктивном выводе на графовых структурах/УАвтоматика и телемеханика. - 2001. - №10. - С. 54-64.

9. Аверин А.И., Вагин В.Н. Параллелизм в дедуктивном выводе на графовых структурах//Автоматика и телемеханика, перевод журнала «Известия РАН. Автоматика и телемеханика».- 2001. - Т.62,№. 10 - С.1588-1596. - (на англ. яз.).

10. Аверин А.И., Вагин В.Н. Методы параллельного дедуктивного вывода на графах связей//Научная сессия МИФИ - 2002. Сборник научных трудов. В 14 томах. - Т.З. - Банки данных. Интеллектуальные системы. Программное обеспечение.М.МИФИ2001., с. 200-201.

11. Аверин А.И. Разработка алгоритмов дедуктивного вывода в системах принятия решений//Радиоэлектроника, электротехника и энергетика. Восьмая Междунар. науч.-техн.конф. студентов и аспирантов; Тезисы докл. В 3-х т. М. МЭИ,2002. Том 1.с. 255-256.

12. Аверин А.И. Способ представления термов в логике предикатов первого порядка. Задача унификации/УРадиоэлектроника, электротехника и энергетика. Девятая междунар. науч.-техн. конф. студентов и аспирантов; Тез. докл. В 3-х т. Т.1. - М.: МЭИ, 2003. - С. 282-283.

13. Аверин А.И. Алгоритм параллельной унификации с использованием усовершенствованной структуры термов//Научная сессия МИФИ - 2003. Сборник научных трудов. В 14 томах. Т.З -М.:МИФИ,2003. - С. 154-156.

14. Аверин А.И. Разработка алгоритмов параллельной унифика-ции//Радиоэлектроника, электротехника и энергетика. Десятая международная научно-техническая конференция студентов и аспирантов; Тез. докл. В 3-х т. -Т.1. - М.: МЭИ, 2004. - С. 307-308.

15. Аверин А.И. Использование агентов в распределенном доказательстве теорем//Международный форум информатизации - 2003: Доклады международной конференции «Информационные средства и технологии» в 3-х т. -Т.1.-М.:Янус-К, 2003 -С. 178-181.

16. Аверин А.И., Вагин В.Н. Разработка высокоэффективных алгоритмов параллельного дедуктивного вывода с использованием графа связей//Программное обеспечение основанное на знаниях: материалы шестой объединенной конференции по программному обеспечению, основанному на знаниях/под ред. В. Стефанюка и К. Каджири - IOS Press, 2004. - С.253-260. -(на англ. яз.)

17. Аверин А.И., Вагин В.Н. Использование параллелизма в дедуктивном методе//Известия РАН. Теория и системы управления. - 2004.-№4.- С. 114-126.

18. Аверин А. И., Вагин В.Н. Использование параллелизма в дедуктивном методе//Международный журнал вычислительной техники и системотехники, Перевод журнала «Известия РАН. Теория и системы управления». - 2004. - Т. 43, № 4. - С.603-615. - (на англ. яз).

Подписано в печать Я \{'-1СС1(Г ЗакТир. \i(' П.л. \,%í)

Полиграфический центр МЭИ (ТУ)

Красноказарменная ул. д.13

ВВЕДЕНИЕ.

ГЛАВА 1. ВИДЫ ПАРАЛЛЕЛИЗМА В ДЕДУКТИВНОМ ВЫВОДЕИ

1.1. Последовательные стратегии в доказательстве теорем.

1.2. Принципы распараллеливания

1.3. План поиска и параллелизм на уровне термов. ф, 1.4. План поиска и параллелизм на уровне дизъюнктов.

1.5. Параллелизм и план поиска на уровне поиска.

1.5.1. Параллельный поиск с использованием подхода «главный -подчиненный».

1.5.2. Параллельный поиск с использованием равноправных процессов.

1.5.3. Распределенный план поиска.

1.5.4 Применение стратегий распараллеливания к процедурам вывода.

ГЛАВА 2. УНИФИКАЦИЯ В ПРОЦЕДУРАХ ПАРАЛЛЕЛЬНОГО ДЕДУКТИВНОГО ВЫВОДА.

2.1. Структуры представления данных в системах дедуктивного вывода

1Ц 2.1.1. Определения.

2.1.2. Строковое представление терма и представление терма в виде дерева

2.1.3. DAG-представление термов.

2.1.4. Плоские термы.

2.1.5. Prolog-представление термов.

2.2. Структуры представления индексов для термов.:.

2.2.1. Позиционные строки (position strings).

2.2.1.1. Основные определения.

2.2.1.2. Совместимость позиционных строк.

2.2.1.3. Характеристическое множество строк.ч

2.2.2. Индексация путей (path indexing).

2.2.2.1. Построение индекса.

2.2.2.2. Алгоритм нахождения множества унифицируемых термов.

2.2.2.3. Преимущества и недостатки подхода, основанного на использовании строковых путей.

2.2.3. Различающие деревья (discrimination trees).

2.2.3.1. Построение индекса.

2.2.3.2. Операции просмотра терма.

2.2.3.3. Алгоритм нахождения унифицируемых термов.

2.2.3.4. Преимущества и недостатки подхода, основанного на использовании различающих деревьев.

2.2.4. Деревья подстановок (substitution trees).

2.2.4.1. Основные определения.

2.2.4.2. Построение индекса.

2.2.4.3. Нахождение унифицируемых термов.

2.2.5. Выводы к разделу 2.2.

2.3. Предлагаемый способ представления термов в логике предикатов первого порядка.

2.3.1. Основные определения.

2.3.2. Установление связей между путями.

2.3.3 Решение задачи унификации.

2.3.4. Распараллеливание алгоритма унификации.

• Выводы к главе 2.

3. ПАРАЛЛЕЛИЗМ НА УРОВНЕ ДИЗЪЮНКТОВ. ПРОЦЕДУРА ВЫВОДА НА ГРАФАХ СВЯЗЕЙ.

3.1. Последовательная процедура доказательства методом графа связей

3.2. Стратегии поиска в графе связей.

3.3. Достоинства процедуры дедуктивного вывода на графе связей.

3.3.1. Проблема нахождения контрарной пары.

3.3.2. Проблема вычисления унификаторов для связи.

3.3.3 Проблема удаления дизъюнктов, которые не могут быть использованы в дальнейшем пространстве поиска.

3.4. Параллельный вывод на графе связей.

3.4.1. Метод OR-параллельной резолюции.

3.4.2. DCDP-параллельный вывод.

3.4.3. AND-параллельная резолюция.

3.5. Модификация процедур параллельного вывода.

3.5.1. Принципы создания эвристических функций.

3.5.2 Эвристическая функция №1.

3.5.3 Эвристическая функция №2.

3.5.4. Эвристическая функция HI.Ill

3.5.4.1. Вычисление эвристической оценки дизъюнкта.

3.5.4.2. Вычисление эвристической оценки унификатора.

3.5.4.3. Вычисление эвристической оценки предикатной литеры.

3.5.4.4. Выбор коэффициентов.

3.5.4.5. Применение эвристической функции HI при решении задачи «Стимроллер».

Ф Выводы к главе 3.

4. АНАЛИЗ ЭФФЕКТИВНОСТИ ПРЕДСТАВЛЕННЫХ АЛГОРИТМОВ ВЫВОДА.

4.1 Основные понятия.

4.2 Сравнение эффективности на тестовой задаче «Стимроллер».

Выводы к главе 4.

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

Использование графовых структур в качестве основы для построения процедур дедуктивного вывода является одним из способов повышения эффективности процесса вывода. Создан ряд алгоритмов дедуктивного вывода на графовых структурах [4, 9, 12, 40, 54, 62, 63]. Однако при решении задач практической сложности, которые характеризуются экспоненциальным ростом числа дизъюнктов, данные алгоритмы не всегда показывали удовлетворительные результаты, что привело к дальнейшим исследованиям в области повышения эффективности процедур вывода. Одним из способов повышения эффективности является распараллеливание процесса вывода.

В работах целого ряда авторов [3, 37, 44, 45, 46, 55] было показано, что использование параллелизма в алгоритмах вывода, основанных на графовых структурах, позволяет существенно повысить эффективность работы алгоритмов. Таким образом, исследование и разработка алгоритмов параллельного дедуктивного вывода на графовых структурах является актуальной задачей.

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

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

1) Использование эффективного способа представления термов. Термы логики предикатов первого порядка являются основной структурой обработки в процедурах вывода, и их неэффективное представление ведет к неэффективной работе доказателя в целом.

2) Использование эффективного способа представления множества дизъюнктов. Множество дизъюнктов является объектом работы процедуры дедуктивного вывода, и выбор способа представления множества дизъюнктов крайне важен для создания эффективных процедур вывода.

3) Использование эффективной стратегии поиска. Резольвирование дизъюнктов является основной операцией в процедурах дедуктивного вывода, и неэффективный выбор дизъюнктов для резольвирования приводит к практической непригодности процедуры вывода.

4) Использование эффективной стратегии распараллеливания. Данную проблему необходимо решать совместно с проблемой выбора эффективной стратегии поиска. Выделяется три основных вида параллелизма: параллелизм на уровне термов, параллелизм на уровне дизъюнктов и параллелизм на уровне поиска (более подробная классификация видов параллелизма рассматривается в первой главе работы). При создании эффективных параллельных процедур вывода, необходимо уделять внимание всем трем разновидностям параллелизма.

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

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

Графы связей Ковальского являются основой для построения алгоритмов параллельного дедуктивного вывода. В настоящее время существует несколько способов распараллеливания процедур вывода на графе связей. В работе рассматриваются алгоритмы OR, DCDP и AND параллельного вывода на графах связей Ковальского. В данных алгоритмах реализован как параллелизм на уровне дизъюнктов (в случае OR и AND параллелизма), так и на уровне поиска (DCDP параллелизм). Для повышения эффективности процесса вывода предлагаются эвристические критерии оценки множества связей для параллельного резольвирования.

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

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

Научная новизна. Новыми являются:

1. Способ представления термов логики предикатов первого порядка, предназначенный для использования в процедурах параллельного вывода на графовых структурах.

2. Метод построения множества связей для DCDP-параллельного вывода, позволяющий повысить эффективность DCDP-параллельного вывода.

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

4. Комплексный подход к распараллеливанию процесса вывода, объединяющий в себе OR-, AND- и DCDP- параллелизм.

Практическая значимость. Практическая значимость работы заключается в создании программной системы, в рамках которой реализованы алгоритмы OR, AND и DCDP параллельного вывода на графовых структурах.

Практическая значимость работы подтверждается использованием разработанных алгоритмов в системе диагностики, реализованной в рамках интегрированной системы управления предприятием SAP R/3 , о чем имеется акт о внедрении.

Реализация результатов. Результаты диссертационной работы Аверина А.И. вошли в отчеты по НИР, выполняемым кафедрой ПМ по по грантам РФФИ № 99-01-00049, № 02-07-90042 по теме «Исследование и разработка инструментальных средств создания экспертных систем семиотического типа», а также в учебном процессе при изучении дисциплины «Математическая логика».

Произведена реализация представленного алгоритма вывода в рамках системы диагностики, представляющей собой надстройку над стандартной функциональностью интегрированной системы управления предприятием SAP R/3 и используемой для ускорения процесса диагностики и устранения неисправностей, возникающих во время работ по инсталляции, системной настройке и системному администрированию системы в НПО «Мекомп».

Апробация работы. Основные положения и результаты диссертации докладывались и обсуждались на 6-й, 7-ой, 8-ой, 9-ой и 10-ой научных конференциях аспирантов и студентов «Радиотехника, электроника, энергетика» в МЭИ (ТУ) (г. Москва, 2000 - 2004 г.г.), на 4-ой международной летней школе-семинаре по искусственному интеллекту для студентов и аспирантов (Бра-славская школа) (Беларусь, г. Браслав, 1999 г.), на «Научных сессиях МИФИ» (г. Москва, 2000 - 2004 г.г.), на 7-й национальной конференции по искусственному интеллекту с международным участием КИИ'2000 (г. Переславль-Залесский, 2000 г.), международном форуме МФИ-2003 (Международные конференции «Информационные средства и технологии») (г. Москва, 2003), на Международной научно-технической конференции «Интеллектуальные системы» AIS'03 (Россия, п. Дивноморское, 2003 г.) и международной конференции JCKBSE - 2004 (Россия, г. Переславль-Залесский, 2004г., доклад на английском языке).

Рассмотрим структуру диссертационной работы подробнее.

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

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

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

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

Выводы к главе 4

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

2. Проведенный анализ показал, что применение эвристик позволило значительно повысить эффективность процедуры вывода. Продемонстрировано, что наиболее чувствительными к выбору эвристики являются процедуры ЭСЭР параллельного вывода.

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

Заключение

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

Произведенное в первой главе работы исследование стратегий распараллеливания показало, что существуют недостаточно изученные способы использования параллельных стратегий в дедуктивном выводе. Среди них можно отметить использование АМ> и (Ж- параллелизма для упорядочивающих стратегий, а также применение в дедуктивном выводе параллельной унификации. Это обусловлено объективными причинами. Если говорить о параллельной унификации и параллельном сопоставлении, то это объясняется структурой параллелизма на уровне термов, применение которого, без использования параллелизма на других уровнях, не приводит к заметному увеличению производительности процедуры вывода. Недостаточные исследования в области А№> и ОЙ.- параллелизма применительно к упорядочивающим стратегиям объясняются неудобством применения большинства упорядочивающих стратегий для одновременной обработки всех литер одного дизъюнкта (в случае АЬЮ-параллелизма) или одной литеры дизъюнкта (в случае (Ж-параллелизма).

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

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

В качестве структуры представления дизъюнктов и основы для построения процедуры параллельного вывода были выбраны графы связей Ковальского. Было показано, что процедура вывода на графе связей удовлетворяет основным принципам создания эффективной процедуры параллельного дедуктивного вывода. Процедура вывода использует рассмотренную во второй главе структуру представления термов, которая позволяет повысить эффективность процедуры параллельной унификации. Структура представления дизъюнктов в виде графа связей позволяет производить быстрый поиск контрарной пары, предъявляет не слишком высокие требования к памяти и позволяет удалять дизъюнкты, которые не могут быть эффективно использованы в процессе вывода.

Процедура вывода на графе связей служит основой для разработки алгоритмов параллельной резолюции. В работе представлены три стратегии распараллеливания (OR, AND и DCDP параллелизм). Для повышения эффективности стратегии поиска были разработаны эвристические функции выбора связи. Сравнение результатов работы процедуры вывода при использовании этих функций и без использования эвристических функций, показали заметное повышение эффективности процедуры вывода при использовании эвристических функций оценки связи.

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

Основными полученными результатами являются:

1) разработка комплексного подхода к решению задачи создания эффективной процедуры вывода, основанного на применении параллелизма на уровне термов и параллелизма на уровне дизъюнктов;

2) исследование задачи представления термов в процедурах дедуктивного вывода. Разработка структуры представления термов, которая может быть использована в параллельных процедурах вывода на графовых структурах.

3) разработка алгоритма параллельной унификации, использующего представленную структуру представления термов и направленного на применение в процедурах параллельного вывода;

4) исследование алгоритмов параллельного дедуктивного вывода на графовых структурах, разработка эвристической функции, позволяющей повысить эффективность параллельной процедуры вывода;

5) разработка программного комплекса, в котором реализованы основные теоретические результаты, представленные в работе.

1. Аверин А.И., Вагин В.Н., Хамидулов М.К. Исследование алгоритмов параллельного вывода на задаче "Стимроллер" //Известия Академии Наук. Теория и системы управления, 2000. №5. - С. 92-100.

2. Аверин А.И., Вагин В.Н. Параллелизм в дедуктивном выводе на графовых структурах //Автоматика и телемеханика. №10. - 2001. - С. 54-64.

3. Вагин В.Н., Салапина Н.О. Система параллельного вывода с использованием графа связи // Известия Академии Наук. Теория и системы управления, №5,1998.-С.39-48.

4. Вагин В. Н. Дедукция и обобщение в системах принятия решений. — М.: Наука.-1988.-384с.

5. Маслов С.Ю. Обратный метод установления выводимости для логических исчислений //Труды математического института им. В.А. Стеклова АН СССР, т.98, стр. 26-87,1968 г.

6. Astrachan O.L., Loveland D.W. METEORs: high performance theorem provers using model elimination/Robert S. Boyer, editor, Automated Reasoning: Essays in Honor of Woody Bledsoe, Kluwer AcademiaPublisher^l991^— pp. 31-60.

7. Avenhaus J., Denzinger J., Fuchs M. DISCOUNT: a system for distributed equational deduction. In Jieh Hsiang, editor, Proceedings of the 6th RTA, volume 914 of LNCS, Springer Verlag, 1995. pp. 397-402.

8. Baader F., Snyder W. Unification Theory //Handbook of Automated Reasoning/ A. Robinson, A. Voronkov eds. Elsevier Science. - 2001. - pp. 445532.

9. Barklund, J., Hagner, N., Wafin, M. Condition Graphs // Proceedings of the Fifth International Conference and Symposium on Logic Programming/ Kowalski, R. Bowen K.A. Seattle: The MIT Press. - 1988. - pp. 435-446

10. Bellia M., Occhuito M.E., Combinatorial lazy unification. Journal of Symbolic Computation. № 27 - 1999. - pp. 185-206.

11. Bellia M., Occhiuto M.E. New Bounds in Parallel Unification: Proc. of CSP'2002. pp. 53-64.

12. Bibel W. On Matrices with Connections // Journal of the ACM. № 28(4). -1981.- pp. 633-645.

13. Bibel W. Automated Theorem Proving. Friedr. Vieweg & Sohn, 2nd edition, 1987.-289 pp.

14. Bonacina M.P., Hsiang J. Parallelization of deduction strategies: an analytical study // Journal of Automated Reasoning. №13. — 1994. - pp. 1-33.

15. Bonacina M.P., Hsiang J. The Clause—Diffusion methodology for distributed deduction//Fundamenta Informaticae. №24. — 1995. - pp.177—207.

16. Bonacina M.P. On the reconstruction of proofs in distributed theorem proving: a modified Clause-Diffusion method // Journal of Symbolic Computation. — 1996. — №21.- pp. 507-522.

17. Bonacina M.P., Hsiang J., Zhang H. PSATO: a distributed propositional prover and its application to quasigroup problems//Journal of Symbolic Computation. №21.-1996. - pp. 543-560.

18. Bonacina M.P., Hsiang J. Ten years of parallel theorem proving: a perspective /Notes of the Workshop on Strategies m Automated Deduction, Federated Logic Conference/Gramlich B., Kirchner H., Pfenning F. eds. — Trento, Italy, 1999. pp. 3-15.

19. Bose S., Clarke E. M., Long D. E., Michaylov S. Parthenon: a parallel theorem prover for non-Horn clauses//Journal of Automated Reasoning, 8(2). — 1992.-pp. 153-182.

20. Ciprietti G., EC-expressions:linear unification and lazy narrowing, Thesis, Universita di Pisa, 1995.

21. Chaiyin G.J., Auslnder M.A., Chandra A.K., Cocke J., Hopkins M.E., Markstein P.W. Register allocation via coloring. // Computer Languages, 6:4757,1981.

22. Christian J. Fast Knuth-Bendix completion: A summary/ Proceedings of the 3rd International Conference on Rewriting Techniques and Applications./ N. Dershowitz, ed., Vol.355 of Lecture Notes in Computer Science, Springer Verlag, 1989.-pp. 551-555.

23. Christian J. Flatterais, discrimination nets, and fast term rewriting//Journal of Automated Reasoning. № 10(1). - 1993. - pp. 95-113.

24. Corny S.E., Macintosh D.J., Meyer D.J. DARES: A Distributed Automated Reasoning System: Proc. 8th National Conf. on Artificial Intelligence (AAAI-90, July 29-August 3, 1990). AAAI Press/MIT Press, 1990. - pp. 78-85.

25. Corbin J., Bidoit M. A Rehabilitation of Robinson's Unification Algorithm /Information Processing 83/R.E.A. Mason (ed.). Elsevier Science Publisher B.V (North-Holland), IFIP, 1983. - pp. 909-914.

26. Davis M., Putnam H. A computing procedure for quantification theory // Journal of the ACM. -№7. 1960. - pp. 201-215.

27. Denzinger J., Lind J. Twlib: a library for distributed search applications/Proceedings of ICS-96/Chu-Sing Yang, editor, 1996 pp. 101-108.

28. Dwork C., Kannelakis P.C., Mitchell J.C. On the sequential nature of unification// J. Logic Programming. № 1. - 1984. - pp.35-50

29. N. Eisinger. Completeness, Confluence, and Related Properties of Clause Graph Resolution//Research Notes in Artificial Intelligence. Pitman Ltd., London, 1991.

30. Fuchs D. Requirement-based cooperative theorem proving/Proceedings of the 6th JELIA/ Jurgen Dix, Luis Farinas del Cerro, Ulrich Furbach, editors,, volume 1489 ofLNAI, Springer, 1998.-pp. 139-153.

31. Graf P., Substitution tree indexing /Rewriting Techniques and Applications/ J. Hsiang, ed., Vol. 914 of Lecture Notes in Computer Science, 1995. pp. 117-131.

32. Graf P., Term Indexing, Vol. 1053 of Lecture Notes in Computer Science, Springer Verlag.

33. Hillenbrand Th., Buch A., Vogt R., Löchner B., Waldmeister: HighPerformance Equational Deduction//Journal of Automated Reasoning. № 18(2). -1997. - pp. 265-270.

34. Hornung G., Knapp A., Knapp U. A parallel connection graph proof procedure / J. H. Siekmann, ed // German Workshop on Artificial Intelligence, Springer-Verlag, Berlin. 1981. pp. 160-167.

35. Huet G., Resolution d'équations dans les language d'ordre 1,2,.,w, Ph.D dissertation, Univ. de Paris VII, France, 1976.

36. Kerber M., Choi S. The semantic clause graph procedure// In proceedings of the CADE-17 Workshop on Model Computation-Principles, Algorithms, and Applications/ P. Baumgartner et al., eds., Pittsburgh, PA, USA. June 2000. pp. 2937.

37. Kirchner C., Viry P. Implementing parallel rewriting /Parallelization in Infërence Systems / Bertram Fronhofer and GrahamWrightson, Eds. № 590, LNAI. Springer-Verlag. 1990. - pp. 123-138

38. Knight K. Unification: a multidisciplinary survey //ACM Computing Surveys. №21. - 1989. -pp. 93—124

39. Kowalski.R. A Proof Procedure Using Connection Graphs. // Journal of the ACM, 22(4), October 1975, p.595-599.

40. Letz R., Schumann J., Bayerl S., Bibel W. SETHEO: A high-performance theorem prover//Journal of Automated Reasoning. №8(2). — 1992.- pp. 183-212.

41. Loganantharaj R., Mueller R.A. Parallel Theorem Proving with Connection Graphs// CADE 1986. pp. 337-352

42. Loganantharaj R. Parallel Link Resolution of Connection Graph Refutation and Its Implementation //International Conference on Parallel Processing (ICPP '87),

43. University Park, PA, USA, August 1987. Pennsylvania State Univ. Press, 1987-pp.154-157

44. Loganantharaj R., Liou A.A. Parallel Deduction of Connection Graphs // Advances in Logic Programming and Automated Reasoning /R.W. Wilkerson ed. -Ablex, 1990.-pp. 1-48.

45. R.Loganantharaj and A. A. Liou, Experience with Extended DC Parallelism of Connection Graphs //International Journal of Mini and Microcomputers.- vol 16(2).- 1994. pp. 33-47.

46. Loganantharaj R., Liou A.A.Experience with Or-Parallelism of Connection Graphs Proceedings of the 19th annual conference on Computer Science, ACM -1991.-pp. 381-390

47. Lusk E.L., McCune W., Slaney J. ROO: a parallel theorem prover /Proceedings of the 11th CADE/ Deepak Kapur, editor, volume 607 of LNAI, Springer Verlag, 1992.-pp. 731-734.

48. Martelli A., Montanari U. An Efficient Unification Algorithm//ACM Trans, on Progr. Lang, and Sys., 4, 2, 1982.- pp. 259-282.

49. McCune W. Experiments with discrimination-tree indexing and path indexing for term retrieval//Journal of Automated Reasoning. № 9(2). - 1992. - pp. 147167.

50. McCune W. Otter 3.0 reference manual and guide, Technical Report 94/6, MCS Division, Argonne National Laboratory, 1994.-57 pp.

51. De Nivelle H., Datastructures for Resolution pjieiapoHHbiH pecypc. — 2000.- http://www.mpi-sb.mpg.de/~nivelle/software/bliksem/

52. Nieuwenhuis R., Rivero J., Vallejo M. //The Barcelona prcver, Journal of Automated Reasoning. №18(2). - pp. 171-176.

53. Ohlbach H. Abstraction tree indexing for terms: in proceedings of the 9th European Conference on Artificial Intelligence. Pitman Publishing, London, 1990.- pp. 479-484.

54. Ohlbach H. J., Siekmann J.H. The Markgraf Karl Refutation Procedure //Computional Logic Essays in Honor of Alan Robinson / Jean Louis Lassez and GordonPlotkin(ed.).-MITPress.- 1991.- ISBN0-262-12156-5.- pp. 41-112

55. Powers D. M. V. Parallel and Efficient Implementation of the Compartmentalized Connection Graph Proof Procedure// Parallelism in Inference Systems. Springer-Verlag, 1991. - pp. 210-233.

56. Ramesh R., Ramakrishnan I., Warren D. 1995., Automata-driven indexing of Prolog clauses// Journal ofLogic Programming. № 23(2). — 1995.- pp.151-202.

57. Robinson J. A machine-oriented logic based on the resolution principle// Journal of the ACM. №12(1). - 1965. - pp. 23-41.

58. Robinson J. New directions in mechanical theorem proving // Information Processing 68, Proceedings of IFIP Congress 1968, Edinburgh, UK, 510 August 1968, Volume 1 Mathematics, Software - 1968. - pp. 63-69.

59. Schulz, S. E A Brainiac Theorem Prover // Journal of AI Communications № 15(2/3).- 2002.-pp.111-126.

60. Schumann J., Letz R. PARTHEO: a high-performance parallel theorem prover/ Proceedings of the 10th CADE/Mark E. Stickel, editor, volume 449 of LNAI, Springer Verlag, 1990.-pp. 28-39.

61. Sekar R., Ramakrishnan I.V., Voronkov A. Term indexing /Handbook of Automated Reasoning/A. Voronkov, A.Robinson eds, Elsiever Science Publishers, 2001.-pp. 1853-1954.

62. Sickel S. A search technique for clause interconnectivity graphs // IEEE Transactions on Computers, G25(8). 1976. — pp. 823- 835.

63. Shostak R.E. Refutation graphs //Artificial Intelligence.- №7. pp.51-64.

64. Stickel M. E. Schubert's steamroller problem: Formulations and solutions // Journal of Automated Reasoning, 2.- 1986. pp. 89-101.

65. Stickel M. E. The path-indexing method for indexing terms, Technical Report 473, SRI International, Menlo Park, California, USA 1989.

66. Vitter J.S., Simons R.A. Parallel algorithms for unification and other complete problems in P: in ACM'84 Conference Proceedings (San Francisco, California, Oct. 8-10). ACM, New York, 1984.

67. Vitter, J. S. and Simons, R. A. (1986). New classes for parallel complexity: A study of unification and other complete problems for P/IEEE Transactions on Computers, C-35(5):23.- pp.403-418.

68. Voronkov A. The Anatomy of Vampyre, Implementing BottomUp Procedures with Code Trees//Journal of Automated Reasoning.- №15. 1995. - pp. 237-265.

69. Weidenbach C., Gaede B., Rock G. SPASS & FLOTTERProceedings of the 13th CADE/ McRobbie M., Slaney J. editors, volume 1104 ofLNAI, Springer, 1996.-pp. 141-145.

70. Weidenbach, C., 1999, Combining Superposition, Sorts and Splitting /A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, Elsevier,2001. pp. 1965-2013.

71. Werner S., Siekmann J.H. Completeness and Soundness of the Connection Graph Proof. AISB/GI (ECAI). 1978. - pp. 340-344.

72. Wos L. Note on McCune Discrimination trees//Journal of Automated Reasoning. №9 (2). - 1992. - pp. 145-146.1. ОГ- -Г/39-/ т. 2.

73. Московский энергетический институт (технический университет)1. На правах рукописи1. Аверин Андрей Игоревич

74. Исследование и разработка алгоритмов параллельного дедуктивного вывода на графовых структурах

75. Специальность 05.13.11 Математическое и программное обеспечение вычислительных машин,комплексов и компьютерных сетей

76. Диссертация на соискание ученой степеникандидата технических наук