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

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

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

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

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

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

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

— исследовать возможности внесения параллелизма вывода на аналитических таблицах для пропозициональной логики и безфункциональной логики предикатов первого порядка;

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

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

— выполнить программную реализацию исследованных методов для многоядерных машин с общей памятью;

— произвести сравнение результатов, полученных на тестовых примерах.

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

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

Научная новизна полученных в диссертации результатов состоит в том, что.

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

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

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

Практическая значимость результатов диссертационной работы заключается в создании программной системы, в рамках которой реализованы алгоритмы последовательного и параллельного вывода на аналитических таблицах, использующие две стратегии поиска: «в ширину» и «в глубину». Программы реализованы в среде Microsoft Visual Studio 2010 на языке С#.

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

Апробация работы. Основные положения и результаты диссертации докладывались и обсуждались на 40-й юбилейной международной конференции, 10-й международной конференции молодых учёных «Информационные технологии в науке, образовании, телекоммуникации и бизнесе», IT + S&E' 2012. Украина, Крым, Ялта-Гурзуф, 25.05 — 04. 06. 2012, на 17-ой и 18-ой научных конференциях аспирантов и студентов «Радиотехника, электроника, энергетика» в НИУ «МЭИ» (г. Москва, 2010 — 2012 г. г.).

Публикации. Основные результаты, полученные при выполнении диссертационной работы, опубликованы в 5 печатных работах, включая 2 статьи в изданиях из перечня ВАК.

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

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

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

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

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

Выводы.

В настоящей главе получены следующие выводы.

1. Представлены параллельный метод с фиктивными переменными, использующий стратегию поиска «в ширину», и параллельный метод с фиктивными переменными,. использующий стратегию поиска «в глубину» .

Заключение

.

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

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

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

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

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

4) Для метода унификаций предложен более эффективный способ работы с подстановками.

5) Предложены эвристики, повышающие эффективность вывода, как для пропозициональной логики, так и для логики предикатов первого порядка.

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

7) Программно реализованы параллельные алгоритмы полного перебора, использующие стратегии поиска «в ширину» (РТМеМ) и «в глубину» (РТМе?/Д, а также параллельные алгоритмы с фиктивными переменными, использующие те же самые стратегии поиска (РТМ^м и РТМ Мс1).

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