Содержание к диссертации
Введение
ГЛАВА 1. Виды параллелизма в дедуктивном выводе 11
1.1. Последовательные стратегии в доказательстве теорем 12
1.2. Принципы распараллеливания 17
1.3. План поиска и параллелизм на уровне термов 21
1.4. План поиска и параллелизм на уровне дизъюнктов 22
1.5. Параллелизм и план поиска на уровне поиска 25
1.5.1. Параллельный поиск с использованием подхода «главный -подчиненный» 25
1.5.2. Параллельный поиск с использованием равноправных процессов.. 27
1.5.3. Распределенный план поиска 29
1.5.4 Применение стратегий распараллеливания к процедурам вывода... 30
ГЛАВА 2. Унификация в процедурах параллельного дедуктивного вывода 34
2.1. Структуры представления данных в системах дедуктивного вывода 36
2.1.1. Определения 36
2.1.2. Строковое представление терма и представление терма в виде дерева 38
2.1.3. DAG-представление термов 39
2.1.4. Плоские термы 40
2.1.5. Prolog-представление термов 41
2.2. Структуры представления индексов для термов ; 42
2.2.1. Позиционные строки (position strings) 44
2.2.1.1. Основные определения 44
2.2.1.2. Совместимость позиционных строк.. 45
2.2.1.3. Характеристическое множество строк. 45
2.2.2. Индексация путей (path indexing) 47
2.2.2.1. Построение индекса „ 47
2.2.2.2. Алгоритм нахождения множества унифицируемых термов .49
2.2.2.3. Преимущества и недостатки подхода, основанного на использовании строковых путей. 50
2.2.3. Различающие деревья (discrimination trees) 50
2.2.3.1. Построение индекса 51
2.2.3.2. Операции просмотра терма 53
2.2.3.3. Алгоритм нахождения унифицируемых термов 54
2.2.3.4. Преимущества и недостатки подхода, основанного на использовании различающих деревьев... 55
2.2.4. Деревья подстановок (substitution trees) 56
2.2.4. L Основные определения 56
2.2.4.2. Построение индекса 57
2.2.4.3. Нахождение унифицируемых термов 58
2.2.5. Выводы к разделу 2.2 60
2.3. Предлагаемый способ представления термов в логиісе предикатов первого порядка 61
2.3.1. Основные определения 61
2.3.2. Установление связей между путями 63
2.3.3 Решение задачи унификации 69
2.3.4. Распараллеливание алгоритма унификации 74
Выводы к главе 2 82
ГЛАВА 3. Параллелизм на уровне дизъюнктов. процедура вывода на графах связей. 84
3.1. Последовательная процедура доказательства методом графа связей 85
3.2. Стратегии поиска в графе связей 91
3.3. Достоинства процедуры дедуктивного вывода на графе связей 94
3.3.1. Проблема нахождения контрарной пары 94
3.3.2. Проблема вычисления унификаторов для связи 94
3.3.3 Проблема удаления дизъюнктов, которые не могут быть
использованы в дальнейшем пространстве поиска 95
3.4. Параллельный вывод на графе связей 95
3.4.1. Метод OR-параллельной резолюции 95
3.4.2. DCDP-параллельный вывод 97
3.4.3. AND-параллельная резолюция 102
3.5. Модификация процедур параллельного вывода 106
3.5.1. Принципы создания эвристических функций 106
3.5.2 Эвристическая функция №1 108
3.5.3 Эвристическая функция №2 109
3.5.4.Эвристическая функция HI Ill
3.5.4.1. Вычисление эвристической оценки дизъюнкта... 112
3.5.4.2. Вычисление эвристической оценки унификатора 113
3.5.4.3. Вычисление эвристической оценки предикатной литеры 113
3.5.4.4. Выбор коэффициентов 113
3.5.4.5. Применение эвристической функции HI при решении задачи «Стимроллер» 115
Выводы к главе 3 120
ГЛАВА 4. Анализ эффективности представленных алгоритмов вывода 121
4.1 Основные понятия 121
4.2 Сравнение эффективности на тестовой задаче «стимроллер» 123
Выводы к главе 4 129
Заключение 130
Список литературы.
- Последовательные стратегии в доказательстве теорем
- Структуры представления данных в системах дедуктивного вывода
- Последовательная процедура доказательства методом графа связей
- Сравнение эффективности на тестовой задаче «стимроллер»
Введение к работе
Диссертационная работа посвящена исследованию и разработке эффективных алгоритмов параллельного дедуктивного вывода. В настоящее время алгоритмы дедуктивного вывода находят свое применение в системах принятия решений, дедуктивных базах данных, информационно-поисковых системах. В числе других областей применения дедуктивного вывода можно назвать верификацию спецификаций компьютерного оборудования (процедуры дедуктивного вывода были использованы при верификации процессоров компании AMD), проверку корректности систем безопасности, анализ корректности протоколов передачи данных. В условиях постоянно растущих объемов обрабатываемых данных, особое значение приобретает проблема создания процедур дедуктивного вывода, способных эффективно работать с большими множествами дизъюнктов.
Использование графовых структур в качестве основы для построения процедур дедуктивного вывода является одним из способов повышения эффективности процесса вывода. Создан ряд алгоритмов дедуктивного вывода на графовых структурах [4, 9, 12, 40, 54, 62, 63]. Однако при решении задач практической сложности, которые характеризуются экспоненциальным ростом числа дизъюнктов, данные алгоритмы не всегда показывали удовлетворительные результаты, что привело к дальнейшим исследованиям в области повышения эффективности процедур вывода. Одним из способов повышения эффективности является распараллеливание процесса вывода.
В работах целого ряда авторов [3, 37, 44, 45, 46, 55] было показано, что использование параллелизма в алгоритмах вывода, основанных на графовых структурах, позволяет существенно повысить эффективность работы алгоритмов. Таким образом, исследование и разработка алгоритмов параллельного дедуктивного вывода на графовых структурах является актуальной задачей. Объектом исследования работы являются системы искусственного интеллекта, использующие дедуктивный вывод. Предметом исследования — процедуры параллельного дедуктивного вывода на графовых структурах.
Цель работы заключается в разработке алгоритмов параллельного дедуктивного вывода, способных решать задачи практической сложности и использующих в качестве основной структуры представления графовые структуры. Необходимо отметить, что создание эффективной процедуры дедуктивного вывода требует решения ряда проблем, многие из которых являются взаимосвязанными. Основными задачами, стоящими перед разработчиком процедуры параллельного дедуктивного вывода, являются:
1) Использование эффективного способа представления термов. Термы логики предикатов первого порядка являются основной структурой обработки в процедурах вывода, и их неэффективное представление ведет к неэффективной работе доказателя в целом.
2) Использование эффективного способа представления множества дизъюнктов. Множество дизъюнктов является объектом работы процедуры дедуктивного вывода, и выбор способа представления множества дизъюнктов крайне важен для создания эффективных процедур вывода.
3) Использование эффективной стратегии поиска. Резольвирование дизъюнктов является основной операцией в процедурах дедуктивного вывода, и неэффективный выбор дизъюнктов для резольвирования приводит к практической непригодности процедуры вывода.
4) Использование эффективной стратегии, распараллеливания. Данную проблему необходимо решать совместно с проблемой выбора эффективной стратегии поиска. Выделяется три основных вида параллелизма: параллелизм на уровне термов, параллелизм на уровне дизъюнктов и параллелизм на уровне поиска (более подробная классификация видов параллелизма рассматривается в первой главе работы). При создании эффективных параллельных проце 7 дур вывода, необходимо уделять внимание всем трем разновидностям параллелизма.
В диссертационной работе предлагается комплексный подход к решению задачи создания эффективной процедуры дедуктивного вывода. В качестве основной структуры представления дизъюнктов выбраны графы связей Ковальского. Графы связей могут быть рассмотрены и как эффективный способ представления множества дизъюнктов, так и как основа для построения процедур вывода. Использование графов связей позволяет решить целый ряд проблем, с которыми сталкиваются процедуры дедуктивного вывода, таких как проблема поиска контрарной пары и проблема удаления дизъюнктов, которые не могут быть использованы в процессе доказательства.
Как было показано выше, использование эффективной структуры представления дизъюнктов требует использования эффективных алгоритмов обработки термов. В работе представлена структура представления термов логики предикатов и алгоритм параллельной унификации, использующий данное представление. Основными достоинствами представленной структуры представления и алгоритма являются высокая эффективность в сочетании с возможностью их использования в параллельных процедурах вывода, основанных на использовании графовых структур.
Графы связей Ковальского являются основой для построения алгоритмов параллельного дедуктивного вывода. В настоящее время существует несколько способов распараллеливания процедур вывода на графе связей. В работе рассматриваются алгоритмы 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г., доклад на английском языке).
Рассмотрим структуру диссертационной работы подробнее.
В первой, обзорной, главе работы рассматривается классификация параллельных стратегий в дедуктивном выводе, представлены основные способы использования параллелизма, рассматриваются наиболее широко распространенные способы представления термов в логике предикатов первого порядка, проводится анализ достоинств и недостатков существующих методов. Вторая глава работы посвящена разработке структуры представления термов логики предикатов первого порядка. Представлены алгоритмы последовательной и параллельной унификации, использующие данное представление. Представлены результаты работы алгоритмов унификации, приведено сравнение эффективности разработанных алгоритмов с алгоритмами других авторов.
В третьей главе рассматривается граф связей как основа построения процедур параллельного дедуктивного вывода. Приводится определение графа связей, дается описание алгоритмов последовательного и параллельного дедуктивного вывода. Анализируются недостатки классического алгоритма вывода на графе связей, которые не позволяют использовать данный подход при решении задач практической сложности. Рассматриваются модификации алгоритма дедуктивного вывода на графе связей. Предлагается структура создания эвристических функций, рассмотрена эвристическая функция, созданная на основе данной структуры.
В четвертой главе представлены результаты сравнения эффективности разработанного алгоритма с алгоритмами других авторов. Предложены подходы для решения задачи сравнения эффективности процедур параллельного дедуктивного вывода. Глава 1. Виды параллелизма в дедуктивном выводе
При решении проблем практической сложности особое значение приобретает задача повышения эффективности процедур дедуктивного вывода. Одним из способов повышения эффективности является распараллеливание процесса вывода. Как было показано в [14,18], особое внимание следует уделить применяемой стратегии распараллеливания (под понятием стратегии распараллеливания в дедуктивном выводе понимается управляющая компонента параллельных дедуктивных методов, которая, с помощью стратегий поиска, производит поиск решения).
В настоящее время создан ряд процедур дедуктивного вывода, наиболее известными среди которых являются метод резолюций Робинсона [57], метод инверсий Маслова [5], процедура вывода с использованием аналитических таблиц, алгоритм Дэвиса-Патнэма [26] и их модификации. Несмотря на существенные различия этих алгоритмов, ко всем из них применимы различные стратегии распараллеливания. В главе рассмотрены основные виды стратегий распараллеливания и возможность их использования для распараллеливания последовательных алгоритмов дедуктивного вывода.
Говоря о распараллеливании последовательных алгоритмов дедуктивного вывода стоит отметить, что, вообще говоря, распараллеливание не сводится к простому одновременному выполнению шагов последовательного алгоритма. При использовании параллелизма возможно изменение стратегии поиска последовательного алгоритма. Таким образом, если последовательная стратегия поиска не является оптимальной, при использовании параллельного поиска мы можем получить сверхлинейное ускорение. Примером этого может служить распределенный доказатель Peers-mcd, который представляет собой распараллеливание доказателя EQP [18]. При запуске Peers-mcd на теореме «Роббин-совские алгебры являются булевыми» (которая была ранее доказана с помощью EQP), бьшо показано сверхлинейное ускорение, тогда как все остальные факторы (используемое аппаратное обеспечение, версия EQPt системы вывода) оставались неизменными.
Перед тем как перейти к анализу параллельных стратегий, следует рассмотреть основные понятия и терминологию, используемые при рассмотрении последовательных стратегий в дедуктивном выводе
Последовательные стратегии в доказательстве теорем
Упорядочивающие стратегии включают в себя стратегии, основанные на принципе резолюции/парамодуляции, использующие перезапись термов {term rewriting) и принцип Кнута-Бендикса, а также стратегии, основанные на процедуре выводе на графах связей Ковальского, которые будут подробно разобраны в третьей главе работы. Эти стратегии называют упорядочивающими, так как они работают с множеством дизъюнктов, используя состоятельное упорядочивание на этом множестве и (возможно) удаляя дизъюнкты, которые или больше других дизъюнктов (согласно введенному упорядочиванию), или являются следствиями других дизъюнктов. Подобные стратегии могут или добавлять дизъюнкты во множество дизъюнктов (для выводов расширения — таких как резолюция или парамодуляция), или удалять дизъюнкты (заменять их на меньшие) - для выводов сокращения (например, для перезаписи термов). Состояние вывода содержит множество дизъюнктов, которые были получены
и сохранены (то есть, не были удалены в результате операции сокращения). Так как это множество обычно приобретает большие размеры, используются различные способы индексирования, для извлечения элементов из множества. Эти способы будут подробно рассмотрены во второй главе работы.
Стратегии, которые используют только расширяющие правила, или которые применяют сокращающие правила только для нормализации сгенерированных данных относительно существующего множества (подобный подход называют прямым сокращением), называются расширяющими стратегиями. Стратегии, использующие как прямое, так и обратное сокращение (то есть нормализацию данных, уже находящихся во множестве, относительно сгенерированных данных), называются сокращающими стратегиями. Упорядочивающие стратегии, вообще говоря, не являются чувствительными к цели, хотя семантические стратегии или стратегии множества поддержки используют семантику для отображения некоторой чувствительности к цели.
Стратегии, основанные на сведении к подцелям, включают в себя стратегии, основанные на принципе линейной резолюции, удалении моделей (model elimination) и табличных методах. Название этого подкласса стратегий отражает тот факт, что каждый шаг в доказательстве представляет собой разбиение цели на подцели (то есть текущего центрального дизъюнкта в линейной резолюции, текущей цепочки в удалении моделей, выбранного листа в таблице). Из этого следует, что эти стратегии являются чувствительными к цели. Состояние вывода содержит текущую попытку вывода (например, в линейной дедукции, в табличных методах). Так как подцели могут повторяться и приводить к избыточным выводам, применяются различные формы леммализации или кэширования, которые сохраняют уже полученные результаты и устраняют повторы в выводах.
В стратегиях, основанных на примерах, напрямую реализуется теорема Эр-брана: производится генерация множеств фундаментальных примеров дизъюнктов и производится проверка выполнимости этих множеств с помощью методов логики исчисления высказываний. Данный класс стратегий размещен на рисунке между упорядочивающими стратегиями и стратегиями, основанными на сведении к подцелям, так как стратегии основанные на примерах имеют общие черты с каждой из вышеуказанных стратегий. С одной стороны, стратегии, основанные на примерах, подобно стратегиям, основанным на упорядочивании, являются синтетическими (так как в них производится генерация примеров). С другой стороны, они имеют сходство со стратегиями, основанными на сведении подцелям, в способе закрытия таблиц путем означивания формул.
Рассмотрим планы поиска, обычно используемые в рассмотренных стратегиях. Упорядочивающие стратегии обычно применяют поиск «первый - лучший» с использованием различных эвристических функций. Так как они аккумулируют все сгенерированные неизбыточные данные, эти стратегии не являются чувствительными к порядку вывода (proof-confluent), то есть, если система вывода является полной, а план поиска.- справедливым, порядок выводов не влияет на полноту. Эти стратегии не нуждаются в операции бэктрекинга, и все их действия могут стать в дальнейшем одной из попыток вывода. В качестве примера, рассмотрим типичный управляющий алгоритм, который используется в доказателях, применяющих стратегии, основанные на упорядочивании (например Otter [50]). В этих алгоритмах рассматривается множество дизъюнктов, которые могут быть выбраны (как бы «граница» поиска) и список дизъюнктов уже выбранных. Предположим, что план поиска осуществляет поиск в глубину, следовательно список дизъюнктов, которые могут быть выбраны, может быть реализованы в виде стека. Таким образом, даже при использовании поиска в глубину, этот вид стратегии не нуждается в бэктрекинге, так как при выборе дизъюнкта р, который не порождает потомков, достаточно просто переместить этот дизъюнкт в список уже выбранных и продолжить работу алгоритма выбрав другой дизъюнкт.
Стратегии, основанные на сведении к подцелям, обычно используют планы поиска в глубину с бэктрекингом и итеративным углублением. В принципе, возможен поиск линейного опровержения или закрытой таблицы с помощью любого плана поиска, например поиска в ширину или стратегии «первый 17 лучший». Однако подобные планы поиска требуют от стратегии порождения и
сохранения в памяти множества попыток доказательства (линейных дедукций или таблиц), которые представляют собой границу поиска. Поиск в глубину с итеративным углублением, как правило, является более предпочтительным, так как он требует сохранения только одной попытки вывода в данный момент времени, в то время как остальные будут рассмотрены во время выполнения операции бэктрекинга. Если ни один шаг доказательства не является применимым к текущему линейному дедуктивному выводу или таблице, план поиска выполняет операцию возврата (бэктрекинга).
Нами были рассмотрены основные стратегии, использующиеся в последовательных процедурах дедуктивного вывода. Перейдем к рассмотрению основных принципов распараллеливания последовательных процедур. В рассмотренной ниже классификации основным критерием является различие между параллелизмом на уровне термов, параллелизмом на уровне дизъюнктов и параллелизмом на уровне поиска.резолюции/парамодуляции, использующие перезапись термов {term rewriting) и принцип Кнута-Бендикса, а также стратегии, основанные на процедуре выводе на графах связей Ковальского, которые будут подробно разобраны в третьей главе работы. Эти стратегии называют упорядочивающими, так как они работают с множеством дизъюнктов, используя состоятельное упорядочивание на этом множестве и (возможно) удаляя дизъюнкты, которые или больше других дизъюнктов (согласно введенному упорядочиванию), или являются следствиями других дизъюнктов. Подобные стратегии могут или добавлять дизъюнкты во множество дизъюнктов (для выводов расширения — таких как резолюция или парамодуляция), или удалять дизъюнкты (заменять их на меньшие) - для выводов сокращения (например, для перезаписи термов). Состояние вывода содержит множество дизъюнктов, которые были получены и сохранены (то есть, не были удалены в результате операции сокращения). Так как это множество обычно приобретает большие размеры, используются различные способы индексирования, для извлечения элементов из множества. Эти способы будут подробно рассмотрены во второй главе работы.
Стратегии, которые используют только расширяющие правила, или которые применяют сокращающие правила только для нормализации сгенерированных данных относительно существующего множества (подобный подход называют прямым сокращением), называются расширяющими стратегиями. Стратегии, использующие как прямое, так и обратное сокращение (то есть нормализацию данных, уже находящихся во множестве, относительно сгенерированных данных), называются сокращающими стратегиями. Упорядочивающие стратегии, вообще говоря, не являются чувствительными к цели, хотя семантические стратегии или стратегии множества поддержки используют семантику для отображения некоторой чувствительности к цели.
Стратегии, основанные на сведении к подцелям, включают в себя стратегии, основанные на принципе линейной резолюции, удалении моделей (model elimination) и табличных методах. Название этого подкласса стратегий отражает тот факт, что каждый шаг в доказательстве представляет собой разбиение цели на подцели (то есть текущего центрального дизъюнкта в линейной резолюции, текущей цепочки в удалении моделей, выбранного листа в таблице). Из этого следует, что эти стратегии являются чувствительными к цели. Состояние вывода содержит текущую попытку вывода (например, в линейной дедукции, в табличных методах). Так как подцели могут повторяться и приводить к избыточным выводам, применяются различные формы леммализации или кэширования, которые сохраняют уже полученные результаты и устраняют повторы в выводах.
Структуры представления данных в системах дедуктивного вывода
Наиболее часто выполняемой операцией в системах дедуктивного вывода (как последовательных, так и параллельных) является операция унификации. Таким образом, при реализации эффективных процедур вывода унификации следует уделить особое внимание, так как неэффективная реализация унификации приводит к неэффективной реализации системы вывода в целом. Классический алгоритм унификации, предложенный в [57] не может быть использован для задач практической сложности, так как он требует экспоненциальных затрат времени и памяти. В [58] было показано, что для создания более эффективных процедур унификации необходимо использование специальных структур для представления термов и создание эффективных алгоритмов для их обработки.
В настоящее время существует целый ряд алгоритмов унификации, которые использующих различные представления термов. Наиболее известными являются алгоритмы предложенные Мартелли и Монтанари [48], Юэ [36], Корби-ном и Бидуа [25]. Эти алгоритмы значительно более эффективны, чем алгоритм Робинсона (временная сложность алгоритма Мартелли и Монтанари составляет 0(n+hgm), где п — число термов, т - число различных переменных в термах, Хью - 0(па(п)) — где а(п)- крайне медленно растущая функция, Кор-бина и Бидуа — 0(п2)).
Однако как было показано в [10], эти алгоритмы редко используются на практике, так как используемые структуры данных слишком сложны и плохо соответствуют структурам данных, обычно используемых в алгоритмах вывода, что приводит к дополнительным накладным расходам на перекодировку одного представления термов в другое. Таким образом, при разработке процедуры унификации необходимо учитывать как пригодность используемых структур данных для непосредственно алгоритма унификации, так и возможность их использования в процедурах дедуктивного вывода. В современных доказателях теорем, таких как Otter (W. McCune, 1994), SETHEO, SPASS, Vampire [68], Waldmeister обычно используется следующая схема: используемые структуры представления термов достаточно просты (чаще всего это представление терма в виде плоского терма или в виде направленного ациклического графа). Подобные представления, во-первых, хорошо подходят для использования в процедурах дедуктивного вывода, и, во-вторых, могут быть использованы в алгоритмах унификации, которые обладают относительно высокой эффективностью (например, алгоритм, предложенный в [20], обладает сложностью 0(п2)). Для повышения эффективности процесса поиска унифицируемых дизъюнктов используются различные методы индексации множества дизъюнктов. Таким образом, работу алгоритма унификации можно разбить на два этапа. Первый этап заключается в поиске термов, которые потенциально могут быть унифицированы. Этот этап выполняется с помощью одного из методов индексации термов. На втором этапе производится непосредственно нахождение унификатора с помощью одного из алгоритмов унификации. Данный подход продемонстрировал высокую эффективность при использовании в последовательных доказателях теорем.
При разработке параллельных доказателей теорем, реализации алгоритма унификации также стоит уделить самое пристальное внимание. Одним из способов повышения эффективности процесса унификации является ее распараллеливание. И, хотя, в [28] было показано, что унификация не принадлежит к классу JVC алгоритмов (то есть алгоритм унификации не может иметь вычислительную сложность 0(log п) при полиномиальном числе процессоров), в работах [11, 66, 67] были выделены классы задач унификации, для которых сложность может быть оценена как 0(Е/Р + V log Р), где Р - число процессоров, - число ребер в графовом представлении терма, V - число вершин в графовом представлении. Многие проблемы, которые возникают в области автоматического доказательства теорем, относятся к этим классам. Таким образом, использование алгоритмов параллельной унификации может привести к повышению производительности алгоритмов параллельного дедуктивного вы 36 вода. Для достижения этой цели необходимо создание структуры представления термов, которая будет одинаково хорошо подходить как для реализации процедуры параллельного дедуктивного вывода, так и для реализации процедуры параллельной унификации.
В главе приводится обзор наиболее известных способов представления термов и методов построения индексов на термах. В третьей части главы представлен способ представления термов, основным достоинством которого является простота распараллеливания, что позволяет использовать данный способ в алгоритмах параллельной унификации. В четвертой части главы рассмотрены разработанные алгоритмы параллельной и последовательной унификации, использующие данное представление.
Последовательная процедура доказательства методом графа связей
Поставим в соответствие каждому предикату вершину в графе связей. Два узла соединяются ненаправленным ребром, называемым связью, если соответствующие предикаты потенциально образуют контрарную пару (что означает возможность резольвирования данных предикатов после применения к ним унификатора и переименования соответствующих переменных). Узлы, соответствующие предикатам, принадлежащим одному дизъюнкту, группируются вместе в графе связей. При построении графа при определении предикатов — потенциальных кандидатов на резольвирование - следует (хотя это потребует дополнительных вычислительных затрат) пометить каждую связь соответствующим наиболее общим унификатором (НОУ).
Будем обозначать граф связей, соответствующий исходному множеству дизъюнктов S как CG(S), а множество связей графа связей как CGUNK(S).
С каждой связью в графе связей ассоциируется единственная резольвента, являющаяся результатом резольвирования предикатов, соединенных данной связью. После генерации резольвенты не составляет особого труда добавить её в граф. Новые связи дизъюнкта-резольвенты могут быть вычислены с использованием имеющейся информации о наследуемых связях дизъюнктов — потомков. НОУ для новых связей будет представлять собой композицию унификатора резольвированной связи и связи дизъюнкта-предка.
Таким образом, процесс резольвирования для данной связи представляет собой получение резольвенты, добавление резольвенты в граф связей, добавле 86
ниє связей резольвенты в граф связей и удаление «старых» связей и дизъюнктов из графа связей.
Удаление «старых» связей и дизъюнктов производится по следующей схеме: 1) когда резольвента сгенерирована и добавлена в граф, связь, которая породила резольвенту, удаляется из графа связей; 2) если вершина не имеет связей, то дизъюнкт, которому эта вершина (предикатная литера) принадлежит, удаляется из графа вместе со всеми связями; 3) если дизъюнкт является тавтологией, то он удаляется со всеми принадлежащими ему предикатными литерами и связями. В значительной мере гибкость и мощь процедуры вывода являются следствием её недетерминизма, так как на каждом шаге алгоритма может быть выбрана любая связь для резольвирования.
Для точного определения процедуры вывода необходимо обратить внимание на детали, особенно на вопросы, связанные с факторизацией, поглощением дизъюнктов, удалением дизъюнктов-тавтологий и чистых дизъюнктов.
Таким образом, последовательный алгоритм вывода на графе связей имеет следующий вид. 1. Выбор связи из множества связей. 2. Резольвирование связи и получение резольвенты. Удаление связи, по которой производилось резольвирование, 3. Если получена пустая резольвента, то успешное завершение, иначе помещение резольвенты в граф, добавление ее связей, удаление дизъюнктов-тавтологий и чистых дизъюнктов, выполнение операций факторизации и поглощения дизъюнктов. 4. Если граф не содержит ни одного дизъюнкта, то неуспешное завершение алгоритма, иначе переход к пункту 1. Рассмотрим работу алгоритма дедуктивного вывода на примере
Данный граф связей не содержит дизъюнктов-тавтологий и чистых дизъюнктов, подлежащих удалению. Операции факторизации и поглощения дизъюнктов также являются неприменимыми к данному множеству дизъюнктов, поэтому переходим к шагу 4 алгоритма.
Граф связей, изображенный на рис. 26, не содержит пустого дизъюнкта, поэтому переходим к шагу 1.
Выберем для резольвирования связь 5. После резольвирования по этой связи получаем дизъюнкт 7: —L(a,b). Удаляем связь 5 и переходим к шагу 4 алгоритма.
Дизъюнкт 7 не является пустым дизъюнктомсвязей, изображенный на рис. 30, содержит дизъюнкты, поэтому переходим к шагу 1.
Выберем для резольвирования связь 8. После резольвирования по этой связи получаем дизъюнкт 9: D . Удаляем связь 8 и переходим к шагу 3 алгоритма.
Дизъюнкт 9 является пустым дизъюнктом, следовательно, исходное множество дизъюнктов является невыполнимым. Завершение работы алгоритма.
Доказана полнота и состоятельность процедуры вывода на графе связей [29, 71].
Нижеприведенный алгоритм является недетерминированным. Для реализации его на детерминированной машине он нуждается в детерминированной процедуре выбора резольвируемой связи. В данном вопросе возможно использование нескольких основных методик, одной из которых является выбор связи, активация которой приведет к уменьшению количества дизъюнктов в гра 91 фе, количества связей или количества вхождений предикатных литер в дизъюнкты. Идеальная ситуация возникает в случае когда связь соединяет пару предикатных литер, не имеющих никаких других связей (так как в этом случае резольвирование приведет к удалению родительских дизъюнктов и всех связей родительских дизъюнктов). Также к упрощению графа приводит слияние одинаковых предикатных литер из дизъюнктов-родителей. Еще одним фактором, влияющим выбор связи, является единственность связи для предикатной литеры, что приводит, как сказано ранее, к удалению дизъюнкта, содержащего эту предикатную литеру после резольвирования. В случае, когда упрощения графа добиться не удается, следует выбрать связь, резольвирование которой приведет к минимальному усложнению графа связей. В этой ситуации следует отдавать предпочтение связям, резольвенты которых содержат наименьшее количество предикатных литер.
Сравнение эффективности на тестовой задаче «стимроллер»
Анализ вычислительной эффективности алгоритмов дедуктивного вывода
является непростой задачей. Обычно анализ производится в виде сравнения результатов работы алгоритма с результатами работы других алгоритмов на некотором подмножестве тестовых задач. К таким задачам относятся задачи «Стимроллер», «Ханойские башни», задачи из множества тестовых примеров ТРТР [60,69] и другие. Однако даже наличие подобных тестовых задач не всегда позволяет сделать вывод о большей или меньшей эффективности алгоритма по сравнению с алгоритмами, разработанными другими исследователями. Во-первых, основными объектами анализа являются такие, достаточно общие, характеристики как количество промежуточных дизъюнктов и количество успешных унификаций. Обычно не учитываются такие параметры как требования к памяти и время работы алгоритма (в связи с различиями в архитектуре и производительности вычислительных средств, использованных при реализации алгоритмов). Количество промежуточных дизъюнктов и успешных унификаций, несомненно, связано с используемой памятью и временными характеристиками алгоритма, но данная зависимость не является прямой. Например, алгоритмы, основанные на использовании графовых структур, обычно производят меньшее количество унификаций, но более требовательны к памяти. Небольшое количество промежуточных дизъюнктов, в свою очередь, может быть вызвано сложными механизмами направленными на удаление дизъюнктов, которые не могут быть использованы при дальнейшем выводе. Однако временная сложность этих механизмов может превышать выгоду от их использования. Таким образом, алгоритм, генерирующий во время своей работы меньшее количество промежуточных дизъюнктов и производящий меньше унификаций, может оказаться не самым эффективным.
Вторым фактором, затрудняющим анализ, является качественные отличия в самих алгоритмах вывода. Например, для доказателей, использующих такие механизмы как множество поддержки (SOS) или теоретических связей (Theory Links) результаты сравнения всегда будут лучше, чем для доказателен, эти механизмы не использующих. Тем не менее, это не говорит, о более высокой эффективности алгоритмов, использующих множества поддержки и теоретические связи, так как применение этих механизмов требует вмешательства человека (эксперта) или, как минимум, наличие какой-либо априорной информации о решаемой проблеме, тогда как представленные в работе алгоритмы подобных требований не предъявляют.
Третьим, затрудняющим анализ эффективности, фактором является различие в подмножестве выбираемых задач для анализа. Так как выбор тестовых задач, из-за отсутствия сложившихся стандартов, во многом остается на усмотрение автора, чаще всего выбираются те задачи, на которых разработанный алгоритм показывает наилучшие результаты. Для решения этой проблемы, в последнее время предпринимаются попытки ввести стандарты для тестирования алгоритмов, самым известным из которых является библиотека ТРТР [60, 69J. Однако данная библиотека является лишь множеством задач, которые могут быть решены с помощью автоматических доказателен теорем, в ней отсутствуют какие-либо тестовые наборы задач, позволяющие оценить производительность алгоритмов.
Трудности вызывает и анализ параллельных алгоритмов дедуктивного вывода. Главной проблемой является практически полное отсутствие (даже по сравнению с последовательными алгоритмами) тестовых примеров и исследований, посвященных сравнению параллельных алгоритмов. Таким образом, исследователю приходится проводить сравнение параллельных алгоритмов с последовательными, причем сравнение производится на тестовых задачах, предназначенных для анализа эффективности последовательных алгоритмов. Подобные тестовые задачи, как правило, отличаются высоким уровнем связности между дизъюнктами, что, естественно, уменьшает выгоду от распараллеливания. В то же время, при одновременном запуске я независимых задач при наличии п свободных процессоров мы можем получить степень распараллеливания близкую к п, что также не будет в полной мере отражать реальную эффективность распараллеливания процедуры вывода.
Однако все перечисленные выше проблемы не означают того, что анализ эффективности алгоритмов дедуктивного вывода невозможен в принципе. Они лишь свидетельствуют о сложности этой задачи и о необходимости критического отношения к результатам сравнения.
В работе рассматривается следующий подход к анализу эффективности. В первой части главы приводятся результаты сравнения работы последовательного алгоритма вывода на графе связей с последовательным алгоритмом предложенным Стикелем в [64]. Данный алгоритм выбран для сравнения вследствие схожести характеристик (оба алгоритма используют граф связей), а также из-за наличия подробного анализа характеристик этого алгоритма в работе М. Стикеля [64]. Сравнение производится на тестовой задаче Стимроллер. Далее, на этой же задаче, мы приводим сравнение параллельной версии алгоритма с последовательной версией.
В следующем разделе приводятся результаты сравнения разработанных алгоритмов с алгоритмами других авторов. В данном сравнении рассматриваются как алгоритмы не использующие априорную информацию, так и алгоритмы которые эту информацию используют. Наилучшие результаты демонстрируют именно алгоритмы второго типа, однако это не позволяет, как было указано выше, сделать однозначное заключение об их более высокой эффективности.
Особое внимание уделено анализу эффективности разработанных эвристик. Ниже приводятся таблицы, демонстрирующие результаты работы алгоритма при использовании разработанных эвристик (результаты работы алгоритма с использованием менее мощных эвристических функций рассмотрены в предыдущей главе).
