Авторефераты по всем темам >>
Авторефераты по техническим специальностям
На правах рукописи
Зо Мьо Хтет
Исследование и разработка параллельнЫх МЕТОДОВ вывода на АНАЛИТИЧЕСКИХ ТАБЛИЦах
Специальность 05.13.11 - Математическое и программное обеспечение вычислительных машин, комплексов
и компьютерных сетей
А В Т О Р Е Ф Е Р А Т
диссертации на соискание ученой степени
кандидата технических наук
Москва - 2012
Работа выполнена на кафедре Прикладной математики Института автоматики и вычислительной техники НИУ МЭИ.
Научный руководитель: Лауреат премии Президента РФ в области образования, доктор технических наук, профессор Вадим Николаевич Вагин
Официальные оппоненты: доктор технических наук,
профессор
Дзегелёнок Игорь Игоревич
кандидат физико-математических наук,
ведущий научный сотрудник
Аверкин Алексей Николаевич
Ведущая организация: Российский научно-исследовательский институт информационных технологий
и систем автоматизированного проектирования
(ФГБУ РосНИИ ИТ и АП), г. Москва
Защита состоится 12 октября 2012 г. в 16 час. 00 мин. на заседании диссертационного совета Д 212.157.01 при НИУ МЭИ по адресу: 111250, Москва, Красноказарменная ул., 17 (ауд. Г 306).
С диссертацией можно ознакомиться в библиотеке НИУ МЭИ.
Автореферат разослан л сентября 2012 г.
Ученый секретарь
диссертационного совета Д 212.157.01
кандидат технических наук, доцент Фомина М.В.
ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ
Актуальность темы исследований. В настоящее время алгоритмы дедуктивного вывода находят широкое применение в системах принятия решений, дедуктивных базах данных, информационно-поисковых системах. В числе других областей использования дедуктивного вывода можно также назвать верификацию спецификаций компьютерного оборудования (процедуры дедуктивного вывода использовались, например, при верификации процессоров компании AMD), проверку корректности систем безопасности, анализ корректности протоколов передачи данных.
Значительный вклад в разработку и исследование алгоритмов дедуктивного вывода внесли Д. Хинтикка (Jaakko Hintikka), Э.Бет (Evert W. Beth), Д. Правитц (Dag Prawitz), Дж. Робинсон (J.A. Robinson), Р.Смаллиан (R.V. Smullan), Мелвин Фиттинг (Melvin Fitting), Стив Ривс (Steve Reeves), М. Дэвис (M. Davis), Х. Патнэм (H. Putnam), Р. Ковальски (R. Kowalski), В. Бибель (W. Bibel), Л. Вос (L. Wos), П. Гилмор (P. Gilmore), Д. Лавлэнд (D. Loveland), Н. Эйзингер (N. Eisinger) , С.Ю. Маслов, В.К.Финн, В.Н. Вагин.
Одной из основных проблем, встающих перед разработчиками процедур дедуктивного вывода, является экспоненциальный рост пространства поиска. В условиях постоянно растущих объемов обрабатываемых данных особое значение приобретает проблема создания процедур дедуктивного вывода, способных эффективно работать с большими множествами дизъюнктов.
Использование аналитических таблиц в качестве основы для построения процедур дедуктивного вывода является одним из способов повышения эффективности процесса вывода. Был создан ряд алгоритмов дедуктивного вывода на аналитических таблицах. Однако при решении задач практической сложности, которые характеризуются экспоненциальным ростом числа дизъюнктов, данные алгоритмы не всегда показывали удовлетворительные результаты, что привело к дальнейшим исследованиям в области повышения эффективности процедур вывода. Одним из способов повышения эффективности является распараллеливание процесса вывода.
В работах Р. Джонсона (Robert Johnson) было показано, что использование параллелизма методов вывода, основанных на аналитических таблицах, позволяет существенно повысить эффективность работы алгоритмов. Таким образом, исследование и разработка параллельных методов вывода на аналитических таблицах является актуальной задачей.
Объектом исследования работы являются системы искусственного интеллекта, использующие дедуктивный вывод. Предметом исследования - процедуры параллельного дедуктивного вывода на аналитических таблицах.
Целью диссертационной работы является исследование, разработка методов, алгоритмов и соответствующих программных средств, реализующих параллельный дедуктивный вывод на аналитических таблицах и способных решать задачи практической сложности. Для достижения поставленной цели необходимо решить следующие задачи:
- изучить имеющиеся алгоритмы вывода на аналитических таблицах для пропозициональной логики и логики предикатов первого порядка;
- исследовать возможности внесения параллелизма вывода на аналитических таблицах для пропозициональной логики и безфункциональной логики предикатов первого порядка;
- изучить имеющиеся алгоритмы унификации для безфункциональной логики предикатов первого порядка и предложить наиболее эффективный метод унификации для параллельных систем;
- предложить усовершенствования для выбранного метода унификации;
-предложить эвристики, повышающие эффективность вывода на аналитических таблицах;
-предложить параллельные методы аналитических таблиц для пропозициональной логики и логики предикатов первого порядка, использующие две стратегии поиска: Ув ширинуФ и Ув глубинуФ;
- выполнить программную реализацию исследованных методов для многоядерных машин с общей памятью;
- произвести сравнение результатов, полученных на тестовых примерах.
Для достижения поставленной в работе цели использовались следующие методы исследования: методы дискретной математики, математической логики, искусственного интеллекта.
Достоверность научных результатов подтверждена теоретическими выкладками, данными компьютерного моделирования, а также сравнением полученных результатов с результатами, приведенными в научной литературе.
Научная новизна полученных в диссертации результатов состоит в том, что
1) проведен анализ преимущества параллельного вывода на аналитических таблицах по сравнению с последовательным методом в задачах практической сложности.
2) разработан и реализован параллельный метод с фиктивными переменными для логики предикатов первого порядка, использующий стратегию Ув ширинуФ.
3) разработан и реализован параллельный метод с фиктивными переменными для логики предикатов первого порядка, использующий стратегию Ув глубинуФ.
Практическая значимость результатов диссертационной работы заключается в создании программной системы, в рамках которой реализованы алгоритмы последовательного и параллельного вывода на аналитических таблицах, использующие две стратегии поиска: Ув ширинуФ и Ув глубинуФ. Программы реализованы в среде Microsoft Visual Studio 2010 на языке C#. Реализованные алгоритмы были также использованы для решения тестовой задачи Стимроллер, а также в учебном процессе при изучении дисциплин У Математическая логика Ф и У Экспертные системы Ф (на английском языке).
Апробация работы. Основные положения и результаты диссертации докладывались и обсуждались на 40-й юбилейной международной конференции, 10-й международной конференции молодых учёных УИнформационные технологии в науке, образовании, телекоммуникации и бизнесеФ, IT + S&EТ 2012. Украина, Крым, ЯлтаЦГурзуф, 25.05 - 04. 06. 2012, на 17-ой и 18-ой научных конференциях аспирантов и студентов Радиотехника, электроника, энергетика в НИУ МЭИ (г. Москва, 2010 - 2012 г.г.).
Публикации. Основные результаты, полученные при выполнении диссертационной работы, опубликованы в 5 печатных работах, включая 2 статьи в изданиях из перечня ВАК.
Структура и объем работы. Диссертация состоит из введения, четырех глав, заключения, списка использованной литературы и приложений. Диссертация содержит 137 страниц машинописного текста (без приложений).
Содержание работы
Во введении обоснована актуальность темы, сформулирована цель работы, рассмотрена структура и краткое содержание диссертации по главам.
В первой главе анализируется задача использования различных видов параллелизма в дедуктивном выводе.
В настоящее время создан ряд процедур дедуктивного вывода, наиболее известными среди которых являются метод резолюций Робинсона, метод обратного вывода Маслова, процедура вывода с использованием аналитических таблиц, алгоритм Дэвиса-Патнэма и их модификации. Несмотря на различия этих алгоритмов, ко всем из них применимы различные стратегии распараллеливания. В главе рассматриваются основные виды стратегий распараллеливания и возможность их использования для распараллеливания последовательных алгоритмов дедуктивного вывода. Представлена предложенная М. Боначина (M.P. Bonacina) классификация стратегий распараллеливания, основным критерием которой является различие между параллелизмом на уровне термов, параллелизмом на уровне дизъюнктов и параллелизмом на уровне поиска.
В параллелизме на уровне термов данными, над которыми может быть произведена параллельная обработка, являются термы или литеры. В методах доказательства теорем имеет место параллельное сопоставление литер и параллельная унификация, когда термы подставляются параллельно вместо переменных. В системах переписывания имеет место параллельное переписывание термов. Этот вид параллелизма относится к параллелизму низшего уровня и отличается довольно большой связностью между данными.
В параллелизме на уровне дизъюнктов данными, над которыми производится параллельная обработка, являются формулы некоторого языка. В системах, основанных на языке Пролог, имеет место AND-параллелизм и OR-параллелизм.
В параллелизме на уровне поиска различают распределенный поиск и мультипоиск. Ключевой фактор в классификации методов с параллельным поиском заключается в дифференциации и комбинировании активности дедуктивных процессов. Принцип разделения пространства поиска на ряд подпространств положен в основу распределенного поиска, в котором существенную роль играет организация связи между порциями пространства.
Другая возможность организации параллельного поиска заключается в обработке всего пространства поиска различными планами поиска, что осуществляется мультипоиском. Чтобы каждый процесс мог воспользоваться результатами других процессов, здесь также необходима связь между ними.
Еще одна возможность параллелизма на уровне поиска представляется в допущении процессам иметь разные или одну и ту же систему вывода. В первом случае такую систему вывода назовем гетерогенной, а в последнем- гомогенной.
Рассматриваемый нами метод аналитических таблиц имеет одну и ту же систему вывода (так называемую гомогенную систему) и осуществляет параллелизм на уровне распределенного поиска.
Во второй главе рассматриваются вопросы, связанные с методом аналитических таблиц для пропозициональной логики и для логики предикатов первого порядка. Одной из конкретных реализаций разрешающей или полуразрешающей процедуры для логических систем является метод аналитических таблиц. Он, как и метод резолюции, относится к методам опровержения, т.е. для доказательства общезначимости формулы A доказывается ее противоречие (мA). Но если метод резолюции работает с формулами, представленными в конъюнктивной нормальной форме (КНФ), то метод аналитических таблиц оперирует с формулами, представленными в дизъюнктивной нормальной форме (ДНФ). Представлены четыре правила расширения таблицы, два из которых относятся к логике высказываний (, ), а два - для логики предикатов первого порядка (, ).
В общем случае правила расширения таблицы недетерминированы, т.е. они говорят, что можно сделать, а не то, что нужно сделать. Для уменьшения недетерминированности выбора правил сначала будем использовать все - и -правила (нет ветвления). Затем применим - правила и только после этого -правила. Доказано, что метод аналитических таблиц обладает непротиворечивостью, т.е. невозможно доказать этим методом формулу и её отрицание одновременно. Также метод полон, т.е. если формула Х общезначима, то она доказуема (выводима) методом аналитических таблиц.
Далее в работе предложены эвристики и усовершенствования для повышения эффективности вывода на аналитических таблицах. Целью приводимых улучшений является уменьшение затрат на хранение данных и увеличение скорости вывода. Обычно увеличение скорости вывода ведет к увеличению затрат на хранение данных, поэтому улучшение обоих показателей - это всегда компромисс между желанием максимально улучшить каждый из показателей.
В работе дан алгоритм последовательного метода таблиц для пропозициональной логики (STMp) и алгоритм последовательного метода полного перебора (STMe) для логики предикатов первого порядка.
Все остальные методы, описанные здесь, выведены из STMP. В процессе вывода мы двигаемся по таблице сверху вниз, слева направо. Это гарантирует минимальное использование памяти, необходимой для хранения таблицы в процессе вывода т.к. таблица расширяется по одному пути до тех пор, пока он не будет либо замкнут, либо не будет определено, что он открыт. При расширении формулы, когда применяется -правило, происходит расщепление и правая ветвь помещается в стек (по ней не ведется расширение таблицы) до тех пор пока все пути, использующие левую ветвь не будут замкнуты. Только после этого правая ветвь извлекается из стека и по ней начинается расширение. Для эффективной реализации все пути проверяются на немедленное константное замыкание до того, как они будут помещены в стек. Если контрарные формулы будут найдены, тогда путь не помещается в стек, а удаляется из таблицы, тем самым не занимая лишнее место, и ожидая своей очереди быть расширенным.
Метод полного перебора (STMe) конструирует таблицу сверху вниз слева направо, немедленно замыкая путь, на котором найдена контрарная пара формул. В каждой точке расщепления генерируются два пути 1 и 2. 2 помещается в стек, в то время как STMe продолжает вычислять 1, пока замыкание не будет найдено. Все дальнейшие незамкнутые пути, получившиеся в результате расщеплений, помещаются в стек перед 2. Таким образом, проверка таблицы сверху вниз, слева направо обеспечена. В STMe новая копия любой -формулы может быть добавлена к пути для каждой константы. Система квот вводится для преодоления проблем, вызванных применением -правила к единичной формуле бесконечное множество раз. Пусть имеется универсально квантифицированная формула на ветви таблицы и переменная-ограничитель n. Тогда универсально квантифицированная формула может быть использована максимум n раз для введения новых имен на пути, после чего она отмечается как использованная.
В третьей главе рассматриваются вопросы метода с фиктивными переменными для избежания комбинаторных проблем, вызванных многократным добавлением к пути экземпляров универсальных формул. Метод с фиктивными переменными отличается от метода полного перебора в способах работы с универсальными формулами. Если метод полного перебора добавляет новую копию формулы для каждой новой константы, которая появляется на пути, метод фиктивных переменных просто помещает фиктивную переменную на место всех вхождений универсально квантифицированной переменной, т.е. вместо фиктивной переменной может быть подставлена любая константа, находящаяся на пути. Эта подстановка может создать контрарную пару и тем самым замкнуть путь.
Мы будем обозначать фиктивные переменные как dx или dx, где х Цположительное целое число.
Описывается метод, который параллельно пытается построить подстановки, способные замкнуть таблицу. Отметим, что в таблице могут существовать пути, которые не требуют унификации, т.е. когда контрарная пара F и F не нуждается в унификации. Если на пути существуют две формулы, которые замыкают его без унификации, то это называется константным замыканием. Однако, если на пути присутствуют формулы типа F(a, x) и F(y, b), где a и b - константы, x и y - фиктивные переменные, то эти формулы необходимо унифицировать, т.е. применить к ним подстановку {<x, b>, <y, a>} и получить контрарную пару F(a, b) и ¬F(a, b).
Главная проблема, на которую нужно обратить внимание в параллельном случае, состоит в поддержании непротиворечивости подстановок, так как многие фиктивные переменные разделяются между нитями и могут связываться с различными константами, что недопустимо.
Две или более редукций являются противоречивыми, если они пытаются связать одну и ту же фиктивную переменную с различными константами. Противоречивая подстановка - это подстановка, содержащая одну или более пар противоречивых редукций. Рассмотрим два пути Р1, Р2 таблицы Т, где Р1 может быть замкнут после унификации формул F(a, x) и F(y, b), и Р2 может быть замкнут после унификации формул G(a, x) и G(y, c). Р1 требует подстановку {<x, b>, <y, a>} для замыкания, в то время как Р2 требует {<x,c>, <y,a>}. Очевидно, что эти подстановки противоречивы. Поэтому замыкание путей с такими подстановками несостоятельно и невозможно.
Возможное унифицирующее множество (П-множество) П для подтаблицы Т таблицы Т содержит редукции, требующиеся для замыкания всех путей в Т. Каждое П-множество состоит из непротиворечивых идемпотентных подстановок. Необходимое унифицирующее множество (N-множество) N является множеством из П-множеств.
В работе представлен процесс согласования. Во время унификации конструируются подстановки и осуществляется согласование различными таблицами. Каждое N-множество содержит множество П-множеств, каждое из которых унифицирует, по крайней мере, одну пару контрарных формул на всех путях конкретной таблицы. Операция согласования объединяет N- множества N1 и N2, соответствующие паре таблиц, выводя единственное N- множество, содержащее П-множества, которые замыкают обе таблицы. Унификация N-множеств называется согласованием.
Подход, который принимается нами по отношению к каждому -расщеплению называется "порождением процессов" (process spawning). В результате, когда мы доходим до точки ветвления то мы можем далее расширять обе ветви независимо, т.е. параллельно.
При применении -правила новый процесс "порождается" для обработки появившейся правой ветви. Левая ветвь продолжает обрабатываться текущим процессом. Когда все подтаблицы, обрабатываемые порожденными процессами, будут замкнуты, можно считать всю таблицу замкнутой.
Рис 1. иллюстрирует работу с аналитической таблицей с фиктивными переменными на 3 узлах Р0, P1 и Р2.
Прокомментируем полученное решение. Первые 14 шагов проходят в соответствии с последовательным алгоритмом метода аналитических таблиц с фиктивными переменными. В универсальных формулах с кванторами x или мx осуществляются подстановки фиктивных переменных вместо x, y и z, т.е. x = d1, x = d2, x = d3, y = d4 и z = d5. Затем в экзистенциональных формулах с кванторами x или мx реализуются подстановки констант вместо переменных, т.е. y = a (для F(d1,y)), y = b ( для G (d2,y ) ) и x = c (для H(x,y)).
После этого идёт разветвление. Применение результатов композиции подстановок даёт следующее: {{F(d1,a), мF(d3,a)},{G(d2,b), мG(d3,b)}}. Отсюда N1= {{<d1/d3>},{<d2/d3>}}.
В отличие от левого пути правый путь ещё раз разветвляется. Имеем:{{F(d1,a), мF(a,d5)},{ G(d2,b), мG(b,d5)}}, N2 = {{<d1/a>,<d5/a>}, {<d2/b>,<d5/b>}}.{{мH(c,d4), H(d3,d5) }}, N3 = {{<d3/c>,<d4/d5>}}.
Применяем операцию согласования, которая объединяет N2 и N3, получая N-множество N4.
N4 = {{<d1/a>,<d5/a>}, {<d2/b>,<d5/b>}} {{<d3/c>,<d4/d5>}}.
xy F(x,y), xy G(x,y), xy (F(x,y) G(x,y) z(F(y,z) G(y,z) H(x,z))) xy H(x,y). 1. м[xy F(x,y) & xy G(x,y) & xy (F(x,y) G(x,y) z(F(y,z) G(y,z) H(x,z))) xy H(x,y)] 2. xy F(x,y) (1) 3. xy G(x,y) (1) 4. xy (F(x,y) G(x,y) z(F(y,z) G(y,z) H(x,z))) (1) 5. м xy H(x,y) (1) 6. y F(d1,y) (2) 7. y G(d2,y) (3) 8. y (F(d3,y) G(d3,y) z(F(y,z) G(y,z) H(d3,z))) (4) 9. F(d1,a) (6) 10. G(d2,b) (7) 11. F(d3,a) G(d3,b) z(F(a,z) G(b,z) H(d3,z)) (8) 12. мy H(c,y) (5) 13. м H(c,d4) (12) 14. F(d3,a) G(d3,b) (F(a,d5) G(b,d5) H(d3,d5)) (11) P0 P1 15. м(F(d3,a) G(d3,b)) (14) 15Т. F(a,d5) G(b,d5) H(d3,d5) (14) 16. мF(d3,a) (15) 17.м G(d3,b) (15) P1 P2 16Т. м(F(a,d5) G(b,d5)) (15Т) 16ТТ. H(d3,d5) (15Т) {<d1/d3>} [9:16] 17Т. мF(a,d5) (16Т) {<d2/d3>} [10:17] 18Т. мG(b,d5) (16Т) {<d3/c>,<d4/d5>}[13:16ТТ]
{<d1/a>,<d5/a>}[9:17Т] {<d2/b>,<d5/b>}[10 :18Т] Здесь P0,P1,P2 - номер узла выполняющего вычисления. Nитог = {{<d1/c>,<d2/b>,<d3/c>,<d4/b>,<d5/b>},{<d1/a>,<d2/c>,<d3/c>,<d4/a>,<d5/a>}}. |
Рис.1. Пример параллельного метода с фиктивными переменными.
Процесс согласования N-множеств, как уже упоминалось, требует создания всех перестановок пар П-множеств из двух N-множеств, причём несогласованные подстановки или экземпляры любых П-множеств из одного и того же N-множества, будут исключены.
N4={{<d1/a>,<d5/a>},{<d3/c>,<d4/d5>}}{{<d2/b>,<d5/b>},{<d3/c>,<d4/d5>}}={{<d1/a>,<d3/c>,<d4/a>,<d5/a>},{<d2/b>,<d3/c>,<d4/b>,<d5/b>}}.
Теперь выполняем согласование между левой и правой ветвями:
N1 = {{<d1/d3>},{<d2/d3>}};
N4 = {{<d1/a>, <d3/c>,<d4/a>,<d5/a>},{<d2/b>,<d3/c>,<d4/b>,<d5/b>}}.
N1 N4 = {{<d1/d3>},{<d1/a>, <d3/c>,<d4/a>,<d5/a>}}
{{<d1/d3>},{<d2/b>, <d3/c>,<d4/b>,<d5/b>}}
{{<d2/d3>},{<d1/a>, <d3/c>,<d4/a>,<d5/a>}}
{{<d2/d3>},{<d2/b>, <d3/c>,<d4/b>,<d5/b>}} =
= {{<d1/a>, <d3/a>,<d3/c>,<d4/a>,<d5/a>}
{<d1/c>,<d2/b>, <d3/c>,<d4/b>,<d5/b>}
{<d1/a>,<d2/c>,<d3/c>,<d4/a>,<d5/a>}
{<d2/b>,<d3/b>, <d3/c>,<d4/b>,<d5/b>}}
В итоговом согласовании первое и четвертое N-множества являются противоречивыми (подчеркнуто), поэтому их следует исключить. Nитог = {{<d1/c>,<d2/b>,<d3/c>,<d4/b>,<d5/b>},{<d1/a>,<d2/c>,<d3/c>,<d4/a>,<d5/a>}}.
Предложено использовать подход Ривса (Reeves) к затенению, когда конфликтующие подстановки обнаруживаются. Ривс добавляет экземпляр - формулы, содержащей новую переменную к таблице, только если константное замыкание не смогло выполниться с текущим множеством фиктивных переменных и констант. Для метода с фиктивными переменными, затенение заменяет процесс, принятый переборным методом для сохранения полноты. Затенение происходит после согласования. Переборный метод добавляет экземпляр для каждой универсально квантифицированной формулы к концу пути, всякий раз, когда вводится новая константа. Если различные пути требуют различных подстановок для определенной фиктивной переменной, тогда тень добавляется к каждому пути с требуемой константой (или новой фиктивной переменной), подставленной вместо фиктивной переменной, которая вовлечена в конфликтующую подстановку. Например, имеем четыре пути Р1, Р2, Р3 и Р4, которые требуют подстановки ({x, a}, {x, b}, {x, c} и {x, d}) соответственно, тогда гранула х найдена (назовем её S) и результирующие пути P2 {S{<x, b>}}, P3 {S{<x, c>}}, и P4 {S{<x, d>}} расширены и произведен поиск на замыкание. Отметим, что мы позволим P1 замкнуться с подстановкой {<х, a>} и затеним только остающееся дерево.
В четвертой главе введены и описаны модификации параллельного метода с фиктивными переменными, которые программно реализованы, проведен анализ вычислительной эффективности разработанных параллельных методов дедуктивного вывода.
Разработаныа следующие параллельные методы аналитических таблиц для логики предикатов первого порядка :
- параллельный метод полного перебора, использующий стратегию поиска Ув ширинуФ (PTMеbd);
- параллельный метод полного перебора, использующий стратегию поиска Ув глубинуФ (PTMеdd);
- параллельный метод с фиктивными переменными, использующий стратегию поиска Ув ширинуФ (PTMdbd);
- параллельный метод с фиктивными переменными, использующий стратегию поиска Ув глубинуФ. (PTMddd);
PTMebd расширяет все открытые ветви таблицы параллельно до тех пор, пока ограничитель порождения не будет превышен. Вне (за пределом) этого момента подтаблицы конструируются локально. Расширение Ув ширинуФ с отдельным порождением процессов стремится распределить пути вокруг доступных процессоров.
Механизм поиска Ув ширинуФ становится проблематичным, когда все пространство поиска (в нашем случае таблица) необходимо хранить целиком. Однако, поскольку метод полного перебора не требует унификации, являющейся дорогой операцией по затратам процессорного времени, он будет полезен (и далее мы это покажем) для малых проблем, так как замыкание пути требует только простой операции сопоставления. Однако, требуется эффективная эвристика, для предсказания, какую из -формул нужно исследовать первой, и этот выбор является довольно непростой эвристической проблемой. Схема поиска Ув ширинуФ диктует, чтобы вся таблица поддерживалась при установлении замыкания. К сожалению, экспоненциальная природа таблиц ограничивает доступное хранение порождаемых дизъюнктов.
PTMedd применяет ту же самую политику порождения процессов для табличного разбиения, что и PTMebd. Однако, как только счётчик порождения становится равным вычисленному значению ограничителя порождения процессов, PTMedd переходит в режим Ув глубинуФ, и Услева-направоФ.
Параллельный метод с фиктивными переменными, использующий стратегию поиска Ув ширинуФ (PTMdbd) расширяет все пути параллельно, распределяя пути тем же самым образом, что и PTMebd. Это расширение происходит асинхронно до тех пор, пока не потребуется унификация. Унификация требуется, когда путь завершен (полностью расширен) и константное замыкание потерпело неудачу. Во время унификации строятся подстановки, и осуществляется согласование различными таблицами (желательно смежными). Этот процесс требует синхронизации. Если N-множество для всей таблицы не может быть сконструировано, выбирается N-множество, которое замыкает больше всего путей. Эти пути замыкаются, и начинается затенение для оставшихся путей. Затенение может происходить асинхронно до тех пор, пока снова не понадобится унификация. На рис.2 приведен пример параллельного метода с фиктивными переменными, использующий стратегию Ув ширинуФ.
(1) ¬x(S(x) & Q(x)) (2) x(¬P(x) Q(x) R(x)) (3) x(P(x)) x (Q(x)) (4) x(¬(Q(x) R(x)) S(x)) (5) ¬x(P(x) R(x)) P1 P2 (6) x(P(x)) [3] (7) x (Q(x)) [3] (8) P(a) [6] (8Т) Q(b) [7] (9) ¬(P(d1) & R(d1)) [5] (9Т) ¬(S(d2) & Q(d2)) [1] P1 P1 P2 P2 (10) ¬P(d1) [9] (11) ¬R(d1) [9] (10Т) ¬S(d2) [9Т] (11Т) ¬Q(d2) [9Т]
[8:10 ;{d1/a}] (12) ¬P(d4) Q(d4) R(d4) [2] (12Т) ¬(Q(d3) R(d3)) S(d3) [4] [8Т:11Т;{d2/b}] P1 P1 P1 P2 P2 (13) ¬P(d4) [12] (14) Q(d4) [12] (15) R(d4) [12] (13Т) ¬(Q(d3) v R(d3)) [12Т] (14Т)S(d3) [12Т]
[8;13;{d4/a}] (16) ¬(S(d5) & Q(d5)) [1] [11:15;{d1/d4}] (15Т) ¬Q(d3) [13Т] [10Т:14Т;{d2/d3}] P1 P1 (16Т) ¬R(d3) [13Т]
(17) ¬S(d5) [16] (18) ¬Q(d5) [16] [8Т:15Т;{d3/b}]
(19) ¬(Q(d6) R(d6)) S(d6) [4] [14:18;{d4/d5}] P1 P1 (20) ¬(Q(d6) v R(d6)) [19] (21) S(d6) [19] (22) ¬Q(d6) [20] (23) ¬R(d6) [20] [17:21;{d5/d6}]
[14:22;{d4/d6}] Px - ( x = номер процессора) Nитог = {<d1/a>, <d2/b>, <d3/b>, <d4/a>, <d5/a>, <d6/a>}. |
Рис.2. Пример параллельного метода с фиктивными переменными для логики предикатов первого порядка, использующий стратегию Ув ширинуФ (с использованием 2 ядер).
(1) ¬x(S(x) & Q(x)) (2) x(¬P(x) Q(x) R(x)) (3) x(P(x)) x (Q(x)) (4) x(¬(Q(x) R(x)) S(x)) (5) ¬x(P(x) & R(x)) 1.P1 1.P2 (6) x(P(x)) [3] (7) x (Q(x)) [3] (8) P(a) [6] (12) Q(b) [7] (9) ¬(P(d1) & R(d1)) [5] (13) ¬(S(d2) & Q(d2)) [1] 1.P1 2.P1 1.P2 5.P1 (10) ¬P(d1) [9] (11) ¬R(d1) [9] (14) ¬S(d2) [13] (15) ¬Q(d2) [13]
[8:10 ;{d1/a}] (21) ¬P(d4) Q(d4) R(d4) [22] (16) ¬(Q(d3) R(d3)) S(d3) [4] [12:15;{d2/b}] 2.P1 3.P1 4.P2 1.P1 2.P2 (22) ¬P(d4) [21] (23) Q(d4) [21] (24) R(d4) [21] (17) ¬(Q(d3) R(d3)) [16] (18) S(d3) [16]
[8;22;{d4/a}] (25) ¬(S(d5) & Q(d5)) [1] [11:24;{d1/d4}] (19) ¬Q(d3) [17] [14:18;{d2/d3}] 3.P1 4.P1 (20) ¬R(d3) [17]
(26) ¬S(d5) [25] (27) ¬Q(d5) [25] [12:19;{d3/b}]
(28) ¬(Q(d6) R(d6)) S(d6) [4] [23:27;{d4/d5}] 3.P1 3.P2
(29) ¬(Q(d6) R(d6)) [28] (30) S(d6) [28] (31) ¬Q(d6) [29] (32) ¬R(d6) [29] [26:30;{d5/d6}]
[23:31;{d4/d6}] Y.Px Ц ( Y = число прохождений процессора ; x = номер процессора) Nитог = {<d1/a>, <d2/b>, <d3/b>, <d4/a>, <d5/a>, <d6/a>}. |
Рис.3. Пример параллельного метода с фиктивными переменными для логики предикатов первого порядка, использующий стратегию Ув глубинуФ(с использованием 2 ядер).
PTMddd следует другой схеме параллелизма чем та, которая была в PTMdbd. Стек неполных задач (незамкнутые пути) поддерживается централизовано. Сеть из n процессоров дает возможность PTMddd исследовать n путей параллельно. При каждом раздвоении создаются два пути. Вычисление одного пути продолжается, в то время как другой путь помещается в стек Tasks (задачи) активных открытых путей вместе с уникальным идентификатором и данными управления. Если процессор УmasterФ (главный) осуществляет хранение Tasks, то расширение и замыкание путей выполняется процессорами УslaveФ (подчиненный). Когда процессор становится свободным, находящийся в стеке путь повторно активируется. Каждый из n активированных путей решается параллельно и одновременно происходит согласование. Когда происходит замыкание пути, берется новый путь из Tasks. Процесс продолжается до тех пор, пока Tasks не станет пустым, и никакой другой процессор не работает на незамкнутом пути. Тогда в этот момент таблица объявляется замкнутой. Если какой - либо процессор находит открытый путь, все вычисления заканчиваются сообщением из центрального пункта распределения сообщений (процессор УmasterФ).
На рис.3 приведен пример параллельного метода с фиктивными переменными, использующий стратегию Ув глубинуФ.
Так как все процессоры должны быть доступны стеку Tasks, возникает узкое место для их связи. Если стратегия Ув ширинуФ нуждается только в синхронизации всех путей при каждом согласовании (перед добавлением тени), подход Ув глубинуФ должен синхронизировать каждое активированное подмножество путей таблицы, ожидая пока унификатор для замыкания этого подмножества не будет сконструирован, перед тем как работать со следующим подмножеством путей из стека. Этот унификатор должен быть также непротиворечив с любыми замыкающими унификаторами, сконструированными до этого.
В работе программно реализованы описанные параллельные методы вывода, приводятся результаты сравнения работ параллельных методов дедуктивного вывода. Сравнения производятся на тестовых задачах (3 легкие задачи, проблема Гилмора и задача Стимроллер) .
егкие задачи
1) x[C(x)&{y(P(y) →L(x,y))}],
x(C(x) →{y(H(y) → ¬L(x,y))})
y(P(y) → ¬H(y))
2) xy[F(x,y)],
xy[G(x,y)],
xy[{F(x,y) ∨ G(x,y)} →{z{{F(y,z) ∨ G(y,z)} →H(x,z)}}]
xyH(x,y)
3) ¬x(S(x) & Q(x)),
x(¬P(x) ∨ Q(x) ∨ R(x)),
x(P(x)) ∨ x (Q(x)),
x(¬(Q(x) ∨ R(x)) ∨ S(x))
x(P(x) ∨ R(x))
Проблемы посложнее
4) Проблема Гилмора ( Gilmore problem)
xy[[{F(y) →G(y)} ↔F(x)]&[{F(y)→H(y)}↔G(x)]&[[{F(y)→G(y)} →H(y)] ↔H(x)]]→z{F(z)&G(z)&H(z)}
5) Задача УСтимроллерФ
xW(x),
xF(x),
xB(x),
xC(x),
xS(x),
x(W(x) →A(x)),
x(F(x) →A(x)),
x(B(x) →A(x)),
x(C(x) →A(x)),
x(S(x) →A(x)),
xG(x),
x(G(x) →P(x)),
xyzv[[{A(x)&P(y)}→E(x,y)]∨[{A(z)&P(v)&M(z,x)&E(z,v)} →E(x,z)]],
[xy[{C(x)&B(y)} →M(x,y)]]& xy[{S(x)&B(y)} →M(x,y)],
xy[{B(x)&F(y)} →M(x,y)],
xy[{F(x)&W(y)} →M(x,y)],
xy[{W(x)&F(y)} → ¬E(x,y)],
xy[{W(x)&G(y)} → ¬E(x,y)],
xy[{B(x)&C(y)} →E(x,y)],
xy[{B(x)&S(y)} → ¬E(x,y)],
xy[C(x) →{P(y)&E(x,y)}],
xy[S(x) →{P(y)&E(x,y)}]
xy[{A(x)&A(y)}&[{E(x,y)}&z{G(z)&E(y,z)}]]
Условия эксперимента:
Windows 7 Professional.
Processor: Intel ( R ) Core (TM) 2 Quad CPU Q 8300 @2.50 GHz 2.50 GHz.
Installed memory (RAM) 4.00 GB (3.25 GB usable)
Задача 1.
Таблица.1.
Количество процессоров | PTMebd (секунды) | PTMedd (секунды) | PTMdbd (секунды) | PTMddd (секунды) |
1 | 0,0725197 | 0,1427895 | 0,2794677 | 0,3583594 |
2 | 0,0437943 | 0,1754636 | 0,2350575 | 0,3016914 |
3 | 0,0832202 | 0,2022179 | 0,2263397 | 0,3402666 |
4 | 0,0428872 | 0,2266498 | 0,3400607 | 0,3224897 |
Рис.4.Результаты для задачи 1.
Задача 2.
Таблица.2.
Количество процессоров | PTMebd (секунды) | PTMedd (секунды) | PTMdbd (секунды) | PTMddd (секунды) |
1 | 0,7119277 | 2,5705974 | 3,6946656 | 4,3583594 |
2 | 0,8037942 | 2,0187224 | 2,8899844 | 3,9016914 |
3 | 1,5032202 | 2,9725663 | 3,1684812 | 3,3402666 |
4 | 1,6029728 | 3,05746163 | 3,3306021 | 3,3224897 |
Рис.5.Результаты для задачи 2.
Задача 3.
Таблица.3.
Количество процессоров | PTMebd (секунды) | PTMedd (секунды) | PTMdbd (секунды) | PTMddd (секунды) |
1 | 1,3942722 | 1,9888753 | 2,5168543 | 3,6140641 |
2 | 1,2747713 | 0,8674326 | 2,2937031 | 3,0785893 |
3 | 1,0032787 | 1,5236543 | 1,8846743 | 2,5698716 |
4 | 1,4555136 | 1,1543278 | 1,7849632 | 2,3890925 |
Рис.6.Результаты для задачи 3.
Проблема Гилмора
Таблица.4.
Количество процессоров | PTMebd (секунды) | PTMedd (секунды) | PTMdbd (секунды) | PTMddd (секунды) |
1 | 70,3954222 | 56,8865531 | 24,7752692 | 22,7325742 |
2 | 61,3982791 | 40,5974336 | 21,2426667 | 19,9661091 |
3 | 54,0022787 | 45,9221543 | 18,6692931 | 14,4931026 |
4 | 53,4555136 | 37,9983258 | 16,4895347 | 14,171059 |
Рис.7.Результаты для проблемы Гилмора.
Задача УСтимроллерФ
Таблица.5.
Количество процессоров | PTMebd (секунды) | PTMedd (секунды) | PTMdbd (секунды) | PTMddd (секунды) |
1 | неудача | неудача | 140,802268 | 72,6130082 |
2 | неудача | неудача | 125,8395874 | 58,8022019 |
3 | неудача | неудача | 110,138551 | 48,8022019 |
4 | неудача | неудача | 107,2166469 | 48,29333 |
Рис.8.Результаты для задачи УСтимроллерФ.
Системы, основанные на методе полного перебора, не пригодны для решения больших проблем, поскольку они сталкиваются с огромным ростом числа промежуточных дизъюнктов, как только многократные -формулы (и экземпляры -формул) появляются на пути. Когда сложность проблемы возрастает, метод с фиктивными переменными становится очень привлекательным, в то время как эффективность метода полного перебора уменьшается. Однако там где переборная система способна завершить доказательство, она, в общем, стремится сделать его быстрее, чем система с методом с фиктивными переменными. Поскольку метод с фиктивными переменными включает унификацию, он имеет естественно, более сложный алгоритм и имеет вычислительные, накладные расходы, связанные с ним. Успех метода полного перебора для параллельного автоматического доказательства теорем на таких малых проблемах должен быть ожидаемым, поскольку не требуется никакой связи между процессами. Процессы полностью независимы до момента, когда они выдают результат. В противоположность этому системы метода с фиктивными переменными требуют связи между процессами с целью поддержки непротиворечивой подстановки для таблицы.
Метод полного перебора лучше справляется с задачами малой сложности, но плохо справляется со сложными задачами. Так, для лёгких задач 1,2,3 (см. первую строку (1 процессор) табл. 1, 2, 3) методы полного перебора (PTMebd и PTMedd) тратят меньше времени, чем методы с фиктивными переменными (PTMdbd и PTMddd).(см. также рис.4,5,6)
Метод с фиктивными переменными, наоборот, лучше справляется со средними и сложными задачами (сравним результаты, данные в таблицах 4 и 5 и рис.7), даже если метод потребует связь между процессами. Недостатки, связанные с этой связью, перевешивают многократное применение -экземпляров. Так, для задачи 4 (проблема Гилмора) в таблице 4 методы с фиктивными переменными ( PTMdbd и PTMddd) тратят меньше времени чем методы полного перебора ( PTMebd и PTMedd). Что касается задачи УСтимроллерФ (см. табл. 5) алгоритмы полного перебора потерпели неудачу при её решении (слишком большой перебор), в то время как алгоритмы с фиктивными переменными ( PTMdbd и PTMddd) успешно её решили (см. также рис. 8).
Поскольку системы, использующие стратегию поиска Ув глубинуФ, доказали своё преимущество, имеется искушение отменить выбор стратегии поиска Ув ширинуФ сразу и навсегда. Однако системы, использующие подход Ув ширинуФ возможно, найдут своё применение для доказательства следствий, содержащих равенство. Если системы, использующие стратегию поиска Ув ширинуФ ограничены размерами памяти, то в системах со стратегией поиска Ув глубинуФ на первый план выдвигается ограничение по времени.
Отметим также, что при решении задач 4 (проблема Гилмора) и 5 (задача УСтимроллерФ) мы видим, что с ростом числа вершин положительный эффект от применения параллелизма будет сказываться по сравнению с методом полного перебора ввиду ускорения процесса вычислений. Хотя сам параллельный метод с фиктивными переменными не учитывает стоимость связи между процессами, он предлагает более эффективное распределение загрузки процессоров, нежели метод полного перебора.
В заключении приведены основные результаты, полученные в диссертационной работе.
Основные результаты работы
- Представлена классификация видов параллелизма в процедурах дедуктивного вывода, основанная на различиях в степени распараллеливания.
- Предложено использовать параллелизм на уровне распределенного поиска для метода аналитических таблиц.
- Рассмотрено формализованное описание классического метода аналитических таблиц для пропозициональной логики и логики предикатов первого порядка, даны основные стратегии выбора следующей формулы на очередном шаге.
- Для метода унификаций предложен более эффективный способ работы с подстановками.
- Предложены эвристики, повышающие эффективность вывода, как для пропозициональной логики, так и для логики предикатов первого порядка.
- Разработаны последовательные и параллельные методы с фиктивными переменными, использующие стратегии Ув глубинуФ и Ув ширинуФ для аналитических таблиц, и разработаны алгоритмы, реализующие эти методы.
- Программно реализованы параллельные алгоритмы полного перебора, использующие стратегии поиска Ув ширинуФ (PTMebd) и Ув глубинуФ (PTMedd), а также параллельные алгоритмы с фиктивными переменными, использующие те же самые стратегии поиска (PTMdbd и PTMddd).
- Произведено сравнение методов на тестовых примерах и показано преимущество параллельного метода аналитических таблиц с фиктивными переменными над параллельным методом полного перебора. Эксперименты на тестовых задачах показали преимущество параллельного метода, использующего стратегию поиска Ув глубинуФ над параллельным методам, реализующим поиск Ув ширинуФ. Сравнительный анализ результатов показал, что метод полного перебора лучше справляется с задачами малой сложности, но плохо справляется с задачами большой размерности. Метод с фиктивными переменными, наоборот, лучше справляется со средними и сложными задачами. Сравнение эффективности разработанных алгоритмов показало, что алгоритмы параллельного вывода на аналитических таблицах являются эффективными.
СПИСОК РАБОТ, ОПУБЛИКОВАННЫХ ПО ТЕМЕ ДИССЕРТАЦИИ
- Вагин В.Н, Зо Мьо Хтет. Параллельный вывод в методе аналитических таблиц, Программные продукты и системы, № 3(95), 2011, с. 8Ц13.
- Вагин В.Н, Зо Мьо Хтет. аМодификации параллельного метода аналитических таблиц. Журнал Открытое образование. № 1(90) 2012. с. 60Ц70.а
- Вагин В.Н, Зо Мьо Хтет. О параллельном методе аналитических таблиц с фиктивными переменными //Матералы 40-й юбилейной международной конференции, 10-й международной конференции молодых учёных УИнформационные технологии в науке, образовании, телекоммуникации и бизнесеФ, IT + S&EТ 2012. Украина, Крым, ЯлтаЦГурзуф 25.05 - 04. 06. 2012, с. 102Ц105.
- Вагин В.Н, Зо Мьо Хтет. Стратегии вывода в параллельном методе аналитических таблиц //Радиоэлектроника, электротехника и энергетика. Восемнадцатая международная научно-техническая конференция студентов и аспирантов; Тезисы докладов. В 4 т. - Т.2. - М.: НИУ МЭИ, 2012. - С. 42Ц43.
- Вагин В.Н, Зо Мьо Хтет. Параллельный вывод в методе аналитических таблиц с фиктивными переменными //Радиоэлектроника, электротехника и энергетика. Восемнадцатая международная научно-техническая конференция студентов и аспирантов; Тезисы докладов. В 4 т. - Т.2. - М.: НИУ МЭИ, 2012. - С. 44.
Авторефераты по всем темам >>
Авторефераты по техническим специальностям