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

РГО Oil

2 0 пне 1RS7

Мальмов "усилий Юрьеьич

Дг:Д;/К";ЙНиГО ЛОГИЧЕСКОГО

А п Г ? ? Г. ¿ г.: г- А т якс'^ертчттми на ?o''C!'<in::o ученой степей;1 из i:1";!-'на та технических наук

счннт -"р i'ep.^/pr

- 1996

Работа выполнена в Санкт-Петербургском Государственном электротехническом университете имени В.И.Ульянова (Ленина).

Научные руководители :

доктор технических наук, профессор ВОДЯХО А.И. кандидат технических наук, доцент СТРАБЫКШ Д. А.

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

доктор технических наук, профессор ЯКОВЛЕВ В.В. кандидат технических наук, доцент КИЗУБ В.А.

Ведущая организация - Санкт-Петербургский институт информатики РАН (СПИИРАН).

Защита состоится " ;/У " 199& г. в _ часов на

заседании диссертационного совета К 063.36.12 Санкт-Петербургского Государственного электротехнического университета имени В.И.Ульянова (Ленина) по адресу: 197376, Санкт-Петербург, ул, Проф. Попова, 5.

С диссертацией можно ознакомиться в библиотеке университета.

Автореферат разослан " ЗУ" Рр 1996 г.

Ученый секретарь диссертационного совета

Маркин А.С.

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

Актуальность темы. В начале 80-х годов в ряде ведущих стран мира было объявлено о начале работ над национальными проектами создания ЭВМ пятого поколения. В наиболее известном из них, японском проекте, предполагалось, что ЭВМ нового поколения должна содержать: машину баз знаний (МБЗ), машину логического вывода (MJIB) и "дружественный" интерфейс пользователя. Основное внимание при этом уделялось разработке машины логического вывода. Базовым языком проекта был выбран язь:к логического программирования Пролог.

Практика показала, что характеристики, полученные в результате исследований, оказались несколько ниве ожидаемых, и практического варианта машины пятого поколения (из отдельных более или менее удачных проектов МБЗ и ШШ) так и не было создано. Однако, некоторая "экологическая шжа" для данного направления имеется, и проблема создания мощных систем логического вывода (СЛВ) по-прежнему остается актуальной

Одной из причин недостаточного распространения ОБ)Д нового поколения явилась низкая производительность машин логического вывода. Действительно, для решения реальных задач обработки знаний необходимо быстродействие порядка 1 GLIPG, а существующие MJIB, большинство из которых спроектированы на базе Пролог-процессоров, обладают производительностью 1-10 1ILIPS, и имеются принципиальные ограничения производительности, заложенные в стандартной (фон-неймановской) архитектуре машин, приспособленной, в основном, под нужды процедурных языков, и в последовательном, по своей сути, методе SLD-резолюций, на котором основан язык Пролог.

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

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

В соответствии с поставленной целью в работе решаются следующие основные задачи:

- разработка метода ускоренного логического вывода (МУЛВ);

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

- разработка архитектуры процессора логического вывода (ПЛВ) с сокращенным набором команд;

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

- разработка системы моделирования машины логического вывода .

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

Научная новизна. В результате проведенных исследований получены следующие научные результаты;

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

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

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

Практическая ценность работы заключается в следующем:

- проанализированы базовые архитектурно-структурные решения потоковых ПЛВ, и сформулированы принципы построения ПЛВ и его основных подсистем - процессора команд и исполнительного процессора;

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

- разработана диалоговая система моделирования однопроцес-сороной системы логического вывода.

Внедрение результатов работы. Полученные в диссертационной работе теоретические и практические результаты используются в рамках курсов "Системы искусственного интеллекта" и "Вычислительные системы и комплексы" ВятГТУ.

Апробация работы. Основные положения и результата диссертационной работы докладывались на научно-технических конференциях профессорско-преподавательского состава ЛЭТИ им, В.И Ульянова (Ленина) в 1991-1994 гг., а так же на международной научно-технической конференции "Исскуственный интеллект - 94" в городе Рыбинске.

Публикации. По теме диссертация опубликовано 6 печатных работ: 5 статей и 1 депонированная рукопись.

Структура и обьем работы. Диссертационная работа состоит из введения, четырех глаз с выводами, заключения, списка литературы, включавшего 105 наименований, списка сокращений и трех приложений . Основная часть работы изложена на 150 страницах машинописного текста. Работа содоряат 51 рисунок и 7 таблиц

СОДЕРНАНЙЕ PAB0TU

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

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

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

- форме представления празил;

- направленности вывода;

- основным применяемым законам логики;

- принципам доказательства теорем;

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

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

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

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

Во второй главе описаны формальные система (ФС) для логики высказываний и логики предикатов, в рамках которых

удобно исследовать различные методы логического вывода. ФС определяется множеством < Т.Н.А.Я >, где:

- Т - множество констант, переменных и оператороз;

- Н - множество правил конструирования формул;

- А - множество аксиом;

- й - множество правил вывода.

Различные наборы множеств Т, Н, А, й определяют различные формальные системы. Описанные ФС отличаются от известных аксиоматических систем наличием двух дополнительных правил вывода:

1. Правило поглощения:

X 1- О, 1 1- X V V Р и У ;

Х-2 I- О, ЬПТ, и ИТ в 1 ь У ;

1 к й, 1 I- з V г, 1 1- I V т, ь г V у ь 1 >- у.

2. Празило упрощения:

1>-х, у-г 1-0 >= (х V у)-г I- о

Кроме этого, выражение (X V У) -Ъ 0 истинно, если г ь 0 или X V У 1- 0 : г н о р (х V у)-г I- о или х V у >- о с (х V у)-г н о

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

12 п

жение (заключение) В.

В рамках ФС для логики высказываний разработан.метод ускоренного логического вывода (МУЛВ), в основу которого положены:

- двунаправленный вывод;

- использование принципа остатков для доказательства теорем;

- применение стратегии "сначала вширь" и тактики упрощения на каждом шаге ЛВ;

- использование эвристических оценок для предотвращения комбинаторного взрыва.

Для описания сути метода введем следующие обозначения : V = < М, г, Q, мТ г*> - процедура вывода, где:

М = < Ri,R2,...,R ,...,R > - множество исходных правил ;

Rj- Lj v L* V ... V L' V ... Vi/ - i-e правило, состоящее

из литералов L* ;

г = г^Л гзЛ...л Гкл...л г - выводимое правило, состоящее из дизъюнктов г , причем каждый дизъюнкт состоит из литералов Lk :

k s

г = Ll V Lk V...V Lkv.,.v Ll ;

к 1 2 s S

Q - признак окончания вывода.принимающий одно из трех значений:

Y - вывод успешно завершен (правило г следует из множества правил М);

N - вывод завершен неудачно (празило г не выводимо из множества правил Ц) ;

G - требуется продолжение вывода для нового выводимого правила ;

М - новое множество исходных правил ; -г - новое множество выводимых правил.

Обозначим также :

Ri= íbj , í/ , . . . , L^,..., L^] - множество литералов, входящих в

исходное правило R^

г = {Lk, Lk,..., Lk,..., Lk} - множество литералов, входящих в

1с 1 2 s S

дизъюнкт г выводимого правила г;

г = I) г - множество литералов, входящих в выводимое k = 1 к

правило г,

Процедура

ускоренного логического вывода применима, если

М * и и г * 0, где а - пустое множество.

На каждом шаге ЛВ выполняются следующие действия : 1. Проверяется основное условие осуществимости вывода правила г из множества М :

U R п г * а для каждого k =» 1,К.

2. Для каждого дизъюнкта г правила г формируется множество Мв базовых правил :

к

Мв = {RBk, RBk..... RBÍ..., RBk] , где

k 12 q Q

M8 e И и RBk П Г * 0 •

k q 1 1 k

3. Для каждого дизъюнкта г формируется множество дМв oc-

ie к

татков базовых правил и проверяется частное условие успешного завершения вывода :

лм = 1дИ , дН , . .., лк , .. . , дк J , где

к 1 2 q О

¿Rsk- остаток правила R по дизъюнкту г ; q q k

д~вк= ~Вк / ("Skn " ) q = Y7q q q q к

Если при определении остатков для какого-либо правила

М® выполняется условие:

-

означающее совпадение дизъюнкта г с исходным правилом йв. то

к и

все остатки, соответствующие данному дизъюнкту, из дальнейшего рассмотрения исключаются. В случае, если данное условие выполняется для всех к = 1,К , то вывод считается успешно завершенным (С2=У) и переходим к п.7, иначе к п.4.

4. Проверяется общее условие завершения вывода. Для этого для каждого г составляется функция Г , равная конъюнкции аРВ11:

к к q

Гк= А дн®к , С! = ГТЧ .

Далее каждая функция Г^ упрощается в соответствии с законами логики высказываний.

Формируется и анализируется функция F = V F^, k = l,K. :

а) если F = О, то вызод успешно завершен (Q=Y) и переходим к п.7;

б) если F = 1, то вывод невозможен (Q=N) и переходим к п.7;

в) если F = f, где f - логическая формула, отличная от О и 1, то требуется продолжение вывода (Q=G), поэтому переходим к п.5;

5. Формируется новое множество исходных правил :

К в

М = и / п м 1 1 к к = 1

Если U. = и, то Q = N и переходим к п.7, иначе к п.б

6. Формируется и упрощается новое выводимое правило. Функция F инвертируется и представляется в виде :

F = f Л f Л A f Л A f

12 J J

После упрощения получаем новое выводимое правило г* = F = г*Л г*л. . .А г-*л. . .л г* , где г - дизъюнкт.

12 V ' " v "

и формируем признак продолжения JIB (Q = G) .

7. Фиксируются выходные параметры Q, М* г . На этом шаг JIB заканчивается и, в зависимости от значения признака Q, выдается ответ или производится переход к следующему шагу вывода, но уже с новой системой правил.

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

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

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

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

- на уровна систем;

- на уровне правил;

- на уровне матриц остатков;

- на уровне предикатов.

Выполнен анализ схемы потока логических вычислений. Активация процессов происходит недетерминированно и асинхронно, под воздействием сообщений (пакетов данных), передаваемых от других процессов, причем все вершины могут обрабатываться параллельно (за исключением связи родитель-наследник). На уровне систем (V-лроцессов) отсутствует необходимость сохранения внутреннего состояния вершин. Используя особенности МУЛВ удалось сократить количество типов сообщений в формальной модели до двух: CREATE и END,

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

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

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

Переход от АМ к тому или иному техническому проекту разработки Ш1В базируется на современной концепции абстрактной машина , отражая общую идеологию реализации логического вывода в высокопроизводительных прикладных системах. В рамках этого направления разрабатываются как специализированные системы (например, Пролог-процессоры), так и системы на базе универсальных ЭВМ. В данной работе выбран вариант создания специализированной СЛВ.

Далее проанализированы базовые архитектурно-структурные решения (АСР) потоковых ПЛВ и сформулированы принципы построения ПЛВ и его основных подсистем - процессора команд (ПК) и исполнительного процессора (ИП). На уровне структуры обосновано решение объединить в единый модуль исполнительный процессор к блок рабочей памяти (РП). Система команд ПЛВ ориентирована на обработку тегированных данных, путем включения команд установки, проверки и перехода по значению тега. Использование ассоциативной памяти пакетов позволяет упростить определение готовности команд. Выбранная структура ПЛВ (с мультиплексированием ИП), позволяет ввести еще два типа параллелизма:

- параллельную выборку и исполнение команд;

- параллельную обработку нескольких команд на исполнительных процессорах.

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

Основываясь на современных тенденциях проектирования вычислительных систем, ориентированных на высокоскоростную параллельную обработку, предлагается обобщенная многоуровневая структура мультипроцессорной СЛВ для аппаратной поддержки ускоренного метода (МПСЛВ МУЛВ). Особенностью данной системы является распределенная конфигурация с локальным адресным пространством на верхнем уровне обработки (обработки систем правил) и конфигурация с

общей памятью на уровне обработки правил и матриц остатков. Данная структура СЛВ наиболее полно соответствует особенностям МУЛВ и организации вычислительного процесса в АМ и позволяет реализовать следующие типа параллелизма:

- параллельнун обработку систем правил на У-процессорах;

- параллельную обработку правил на ПЛВ;

- параллельную обработку матриц остатков и предикатов на исполнительных процессорах;

- параллелизм при обращении к общей памяти и кэш-памяти;

- параллелизм между выполнением логического вывода ка ЙП и обработкой сообщений на ПК.

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

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

Т, = (1-а) • Р

1 а

(3 • N

8 апс!

t + « • N • t

( к-! >/Я а г ( к - 1 > /К

т = (1-е) • — • ь + 1~ (1—а) N • г

К I. Jv.rH

N + 1 N

Т = 1/2 и

2К N • (К-1)

о г -

+ 1/2

I- 2Я -1

N

где: - Я - количество процессоров в системе;

~ '^и ~ среднее время выполнения одной операции

(время обработки одной вершины) на соответствующей СЛБ;

- N - общее число вершин в графе задачи;

- N - число обрабатываемых вершин для МУЛВ;

- N - число ИЛИ-вершин;

впй

- Н - число И-вершин;

ог

-И - число И-вершин со связанными переценными;

- а - вероятность отказа ветви;

- к - средний коэффициент связности переменных;

- (5 - средняя длина ветви в графе.

Проведенный анализ позволяет утверждать, что:

- информационная сложность МПСЛВ МУЛВ меньше других систем логического вывода;

- обменная сложность МПСЛВ МУЛВ меньше других многопроцессорных (в том числе потоковых) СЛВ;

- по производительности МПСЛВ МУЛВ на определенных классах

к'

задач имеет преимущество до 2Й • ^- раз;

V аг

- с увеличением объема задачи (увеличением количества вершин в графе) преимущество МПСЛВ МУЛВ над остальными системами возрастает.

Для доказательства корректности алгоритмов функционирования основных элементов абстрактной машины и проверки полноты ее системы команд была разработана диалоговая система моделирования (ДСМ) однопроцессорной потоковой машины логического вывода, реализующей ускоренный метод. ДСМ позволяет проверить работоспособность ускоренного метода ЛВ, безопасность динамической модели МУЛВ, провести анализ эффективности сокращения количества типов сообщений в АМ и организации буфера готовности команд в виде ЬХГО-стека. Развитый дружественный интерфейс пользователя делает систему моделирования пригодной для применения в учебном процессе .

ОСНОВНЫЕ РЕЗУЛЬТАТЫ РАБОТЫ

В диссертационной работе получены следующие основные науч-

ные и практические результаты:

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

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

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

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

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

6. Разработана диалоговая система моделирования абстрактной машины логического вывода.

СПИСОК ПУБЛИКАЦИЙ ПО ТЕМЕ ДИССЕРТАЦИИ

1. Мельцов В.Ю. , Страбыкин Д.А. Метод параллельного логического вывода/ НирПИ,- М.,1992,- Деп. в ВИНИТИ 12.06.92 N 3240-В92. 27с .

2. Баталов Д.И., Водяхо А.И., Мельцов В.Ю., Солдатов В В. Процессор векторной унификации для высокопроизводительных систем логического вывода/ Известия С.-Пб. ЭТИ. Сборник научных трудов, вып 444 - С.-Пб. ЭТИ, 1992, с.19-24

3. Водяхо А.И., Мельцов В.Ю., Страбыкин Д. А. Солдатов В.В. Формальная система дедуктивного логического вывода в рамках логики высказываний/ Известия ТЭТУ. Сборник научных трудов, вкп. 458 - С.-Пб. ТЭТУ, 1993, с.7-13.

4. Водяхо А,И., Иванов C.B., Мельцов В.Ю. Солдатов В.В. Организация памяти транспьютерной системы логического вывода/ Известия ТЭТУ. Сборник научных трудов, вып. 458 - С.-Пб. ТЭТУ,

1993, с 47-50.

5. Водяхо А.И. , Мельцов В.Ю., Страбыкин Д.А. Система параллельного логического вывода/ Известия ПЭТУ. Сборник научных трудов, вып. 476. Структуры и математическое обеспечение специализированных вычислительных средств. - С.-Пб. ТЭТУ, 1994, с.60-64.

6. Страбыкин Д.А., Мельцов В.Ю., Рыков О.В. Логический вывод методом параллельной редукции и его аппаратная поддержка/ IV Национальная конференция с международным участием "Искусственный интеллект - 94". Сборник научных трудов, том II. - Рыбинск,

1994, с.300-314.