авторефераты диссертаций БЕСПЛАТНАЯ РОССИЙСКАЯ БИБЛИОТЕКА - WWW.DISLIB.RU

АВТОРЕФЕРАТЫ, ДИССЕРТАЦИИ, МОНОГРАФИИ, НАУЧНЫЕ СТАТЬИ, КНИГИ

 
<< ГЛАВНАЯ
АГРОИНЖЕНЕРИЯ
АСТРОНОМИЯ
БЕЗОПАСНОСТЬ
БИОЛОГИЯ
ЗЕМЛЯ
ИНФОРМАТИКА
ИСКУССТВОВЕДЕНИЕ
ИСТОРИЯ
КУЛЬТУРОЛОГИЯ
МАШИНОСТРОЕНИЕ
МЕДИЦИНА
МЕТАЛЛУРГИЯ
МЕХАНИКА
ПЕДАГОГИКА
ПОЛИТИКА
ПРИБОРОСТРОЕНИЕ
ПРОДОВОЛЬСТВИЕ
ПСИХОЛОГИЯ
РАДИОТЕХНИКА
СЕЛЬСКОЕ ХОЗЯЙСТВО
СОЦИОЛОГИЯ
СТРОИТЕЛЬСТВО
ТЕХНИЧЕСКИЕ НАУКИ
ТРАНСПОРТ
ФАРМАЦЕВТИКА
ФИЗИКА
ФИЗИОЛОГИЯ
ФИЛОЛОГИЯ
ФИЛОСОФИЯ
ХИМИЯ
ЭКОНОМИКА
ЭЛЕКТРОТЕХНИКА
ЭНЕРГЕТИКА
ЮРИСПРУДЕНЦИЯ
ЯЗЫКОЗНАНИЕ
РАЗНОЕ
КОНТАКТЫ


Pages:   || 2 | 3 |

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

-- [ Страница 1 ] --

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

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

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

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

и компьютерных сетей

А В Т О Р Е Ф Е Р А Т

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

кандидата технических наук

Москва – 2004

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

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

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

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

профессор

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

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

профессор

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

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

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

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

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

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

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

диссертационного совета Д 212.157.01

кандидат технических наук,

профессор

И.И. Ладыгин

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ

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

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

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

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

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

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

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

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

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 страниц машинописного текста (без приложений).

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

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

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

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

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

 Применение стратегий-0

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

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

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

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

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

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

Одним из способов повышения эффективности процесса унификации является его распараллеливание. И хотя С. Дуорк (S. Dwork) было показано, что унификация не принадлежит к классу NC алгоритмов (то есть алгоритм унификации не может иметь вычислительную сложность O(log n)k при полиномиальном числе процессоров), в работах Дж. Виттера (J. Vitter) и М. Беллья (M. Bellia) были выделены классы задач унификации, для которых сложность может быть оценена как O(E/P + V log P), где P – число процессоров, E – число ребер в графовом представлении терма, V - число вершин в графовом представлении. Многие проблемы, которые возникают в области автоматического доказательства теорем, относятся к этим классам. Таким образом, использование алгоритмов параллельной унификации может привести к повышению производительности алгоритмов параллельного дедуктивного вывода. Для достижения этой цели необходимо создание структуры представления термов, которая будет одинаково хорошо подходить как для реализации процедуры параллельного дедуктивного вывода, так и для реализации процедуры параллельной унификации.

В главе приводится обзор наиболее известных способов представления термов и методов индексации термов. Показано, что в системах, использующих графовые структуры представления термов (таких как графы связей), использование методов индексации только для поиска потенциально унифицируемых термов не совсем оправданно, так как потенциально унифицируемые термы или уже соединены ребром в графе, или нахождение этой связи требует просмотра только небольшого подмножества всего множества дизъюнктов. Таким образом, распространенные подходы, основанные на использовании индексации путей или различающих деревьев (то есть осуществляющие поиск потенциально унифицируемых термов без нахождения унифицирующей подстановки), не могут быть использованы при разработке доказателя теорем (последовательного или параллельного), использующего графовые структуры. Таким образом, для разработки параллельного доказателя теорем, основанного на использовании графовых структур, необходимо создание новых структур представления и индексации термов. В третьей части главы представлен подобный способ представления термов, основным достоинством которого является простота распараллеливания, что позволяет использовать данный способ в алгоритмах параллельной унификации. В четвертой части главы рассмотрены разработанные алгоритмы параллельной и последовательной унификации, использующие данное представление. Решение задачи унификации с использованием предложенного способа представления термов основывается на записи представления термов, участвующих в задаче унификации, в виде таблицы, установки связей между строками таблицы и обработки полученного графа по определенным правилам. Пример построения таблицы для задачи унификации S={f(a,b)=z, f(z,b)=f(f(a,b),x)} приведен на рис. 2.

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

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

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

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



Pages:   || 2 | 3 |
 





 
© 2013 www.dislib.ru - «Авторефераты диссертаций - бесплатно»

Материалы этого сайта размещены для ознакомления, все права принадлежат их авторам.
Если Вы не согласны с тем, что Ваш материал размещён на этом сайте, пожалуйста, напишите нам, мы в течении 1-2 рабочих дней удалим его.