Диссертация (1150569), страница 10

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

Текст из файла (страница 10)

Строим δ-членный F-набор, формулы в котором не повторяются. Тоесть переписываем без конъюнкций все дизъюнкты вида  S    Pki x1,..., xniпри i  1,..., . Создаем популяцию из δ процессоров.КаждойпареPki  a j1 ,..., a j  ,ni потенциальновходящихвконтрарныходинF-набор,формулназначаемPki x1,..., xniприоритетиихотождествления равным 1. Остальные приоритеты назначаем равными 0.2. Копируем δ-членный F-набор δ – 1 раз. Получаем ровно δ одинаковыхF-наборов. Назначаем i-му процессору i  1,...,   свою начальную формулуPki x1,..., xni– формулу, с которой данный процессор начинает свойитерационный цикл, и потенциально контрарную ей формулу изS   ,имеющую приоритет, равный 1.

Если каким-то двум процессорам назначеныформулы, начинающиеся с одного и того же предикатного символа (таких формулне более δ), то назначаем для них разные формулы изконтрарные данной.S   , потенциально60Если для каких-то двух процессоров не существует разных потенциальноконтрарных формул, то формула не выводима4. Алгоритм заканчивает работу.Иначе, переходим к п. 3.3.3. Параллельно работают δ процессоров; i-й процессор i  1,...,  осуществляет присвоение значений переменным.3.1. Если в рабочей формуле данного процессора нет переменных, то вкачестве рабочей для этого процессора выбираем формулу из следующейэлементарной дизъюнкции, содержащую хоть одну переменную.3.2.

Ищем среди формул вS   формулу Pki  a j1 ,..., a j n  , имеющуюiприоритет, равный 1, и потенциально контрарную формуле Pki t1,..., tni , скоторой работает этот процессор5. Если какие-то два процессора работают содной и той же дизъюнкцией, ищем для них разные потенциально контрарныеатомарные формулы. Если найти разные формулы не удалось, один изпроцессоров «засыпает» до тех пор, пока не будет отменено присвоение,приведшее к одинаковой работе двух процессоров. Если нашли подходящуюформулу, то переходим к п. 3.3.

Если ее нет, то переходим к п. 4.3.3. Решаем систему уравнений вида tl  a jl l  1,..., ni  , унифицирующуюсписок переменных и констант со списком констант. В случае, если эта системаимеет решение, то переходим к п. 3.4. Если система решений не имеет, топонизить приоритет этого действия до 0 и переходим к п. 3.2.3.4. Записываем результаты, полученные разными процессорами, ипроверяем их на непротиворечивость следующим образом. Если процессорыодновременно присваивают одним и тем же переменным разные значения, тотакие результаты считаются противоречивыми.

Если результаты действий двух4Невозможно подобрать такой набор значений переменных, чтобы вывести пустой F-набор, так как в нем будеткак минимум одна формула, в которой останутся переменные, которым будет невозможно присвоить значение.5Первоначальноt1 ,...,tni– список переменных изx1 ,..., xni .При последующих итерациях это списокпеременных и констант, подставленных вместо переменных после процедуры унификации.61процессоров не противоречат друг другу, то присвоение полученных значенийпеременных осуществляется в формулах обоих процессоров.3.5. Заменяем в F-наборе каждого процессора вхождения переменных изсписка на их значения, полученные в п.

3.3 и 3.4, если успешно пройденапроверка на непротиворечивость.3.6. Если для какого-либо процессора получился пустой F-набор, тоалгоритм заканчивает работу. Формула выводима и найден набор значенийпеременных, существование которых утверждалось в формуле.3.7. Если получился тупиковый F-набор, то переходим к п. 4.3.8. Если для всех процессоров приоритеты всех действий равны 0, тоформула не выводима. Алгоритм заканчивает работу.3.9. Если в F-наборе какого-либо процессора существуют формулы,имеющие переменные, которым еще не присвоено значение, то переходим к п.3.1.4.

Возвратная часть алгоритма.4.1. Отменяем последнее действие п. 3.5, если это возможно, и переходим кп. 3.2.4.2. Если для какого-либо процессора отмена последнего действия п. 3.5невозможна, то алгоритм заканчивает работу.4.3. Если все процессоры закончили работу, но пустой F-набор не получен,то алгоритм заканчивает работу.

Формула не выводима.На рис. 3.1.1 представлена краткая схема этого алгоритма.62Рис. 3.1.1. Краткая схема работы алгоритма IAPTA.633.2. Оценка числа шагов работы алгоритма IAPTAТеорема 3.2.1. (Нижняя оценка числа шагов работы алгоритмаIAPTA)Количество шагов доказательства логического следования видаS    x Ak  x и нахождения значений переменных, для которых это следование имеет место,при использовании алгоритма IAPTA, не менее 2δ(s + 2) + 2.Доказательство. Нижняя оценка достигается в том случае, когда алгоритм11заканчивает работу в п. 2. То есть существуют две формулы Pki t1 ,..., tniиPki t12 ,..., tn2i , имеющие различные переменные, и всего одна формулаPki a j1 ,...,a jn , потенциально контрарная Pki t11,..., t1ni и Pki t12 ,..., tn2i .iНа выполнение соответствующих пунктов алгоритма уходитв п.

1 – δ шагов на построение F-набора и δs шагов на назначение приоритетов;в п. 2 – (δ − 1) шаг на копирование F-набора;δ шагов на создание популяции процессоров;δ шагов на назначение каждому процессору своего F-набора, своей начальнойформулы с переменными;111 шаг на назначение процессору, начинающему работу с формулы Pki t1 ,..., tniформулы Pki a j1 ,..., a jn ;i111 шаг на проверку на совпадение имен предикатов в формулах Pki t1 ,..., tniиPki t12 ,..., tn2i ;1 шаг на поиск среди формул с единичными приоритетами формулы видаPki a j1 ,..., a jn .iИтого получаем 4δ + 2δs − 1 + 3 = 2δ(s + 2) + 2 шагов.■64Теорема 3.2.2.

(Верхняя оценка числа шагов работы алгоритмаIAPTA)Количество шагов доказательства логического следования видаS    x Ak  x и нахождения значений переменных, для которых это следование имеет место, при использовании алгоритма IAPTAсоставляет O l   max sk   k.Доказательство. Верхняя оценка будет достигнута, если ответ на вопрос,выводима ли формула, будет получен на последнем шаге работы алгоритма, т. е.,если каждому процессору придется перебрать все постоянные формулы из S   ,потенциально контрарные своей атомарной формуле.Каждому процессору придется решить не более чем max sk систем из lkуравнений на первой итерации, не более чем max sk  1 систем из l уравнений наkвторой итерации и не более чем max sk   систем l уравнений на δ-й итерации,kна которой происходит присвоение значений последним переменным.С учетом возвратов назад получаем оценку O l   max sk  max sk  max sk  1    max sk  max sk  1     max sk      kk k k k  k  O l   max sk    k ■Замечание.

Алгоритм IAPTA разработан для идеального варианта, когдаколичество процессоров не ограничено. В этом случае верхняя оценка числашаговалгоритма,использующеготактикимуравьиныхалгоритмовипараллельных вычислений IAPTA имеет порядок, в δ раз меньший, чем верхняяоценка числа шагов работы алгоритма IMA. В реальности количествопроцессоров ограничено, например, числом d(при больших δ,d<δ).65Работает ровно d процессоров.

Каждый из них может провести полныйперебор всех унификаций. Поэтому при ограниченном количестве процессоров валгоритме IAPTA следует изменить п. 2 следующим образом:2. Копируем δ-членный F-набор d – 1 раз. Назначаем i-му процессору i  1,..., d  свою группу из m6( m    ) формул, для остальных   m формул i-гоd процессора назначаем нулевой приоритет. Таким образом добьемся, что никакиедва процессора не могут начинать работу с одной и той же формулы Pki x1,..., xni, имеющей переменные.

Далее из каждой группы m начальных формулPki x1,..., xni i-го процессора назначаем этому процессору первую начальнуюформулу, с которой данный процессор начинает свой итерационный цикл, ипотенциально контрарную ей формулу изS   , имеющую приоритет, равный 1.Если каким-то двум процессорам назначены формулы, начинающиеся с одного итого же предикатного символа (таких формул не более δ), то назначаем для нихразные формулы изS   , потенциально контрарные данной.

Если для каких-тодвух процессоров не существует разных потенциально контрарных формул, тоформула не выводима. Алгоритм заканчивает работу. Иначе, переходим к п. 3.3.После этой модификации каждому процессору придется обойти все ветвидерева представленного на рис. 3.2.1.6Для одного из процессоров может быть назначено меньшее, чем m число начальных рабочих формул, так как δ,вообще говоря, не делится нацело на d.66Рис. 3.2.1.

Вид дерева доказательства поиска вывода для каждого процессора при ограниченномколичестве процессоров.Тогда верхняя оценка числа шагов работы алгоритма IAPTAсоставляет  O    l   max sk  d   k.В приложении Б алгоритм IAPTA применен к примеру, который вприложении А решается посредством алгоритма IMA, что иллюстрирующийсокращение перебора при применении алгоритма IAPTA.Пусть имеется множество контурных изображений, составленных изотрезков прямых, задаваемых своими концами.

Заданы два предиката V и L,определяемых так, как представлено на рис. 3.3.1.Рис. 3.3.1. Предикаты V и L.Задан класс объектов Ω1 – класс контурных изображений «троек».Схематическое изображение эталонного объекта имеет вид (см. рис. 3.3.2):Рис. 3.3.2. Контурное изображение «тройка».Описание класса задается следующей формулой:A x1,..., x6   V  x2 , x1, x4  & V  x4 , x2 , x3  & V  x4 , x3 , x6  & V  x6 , x4 , x5  & L x4 , x2 , x6 .67Пусть задано контурное изображение, представленное на рис. 3.3.3, вкотором требуется найти хотя бы один объект, принадлежащий классу «троек».Рис.

3.3.3. Контурное изображение.Это изображение имеет описание:S a1,, a6   {V a1, a2 , a3  & V a2 , a1, a4  & V a3 , a1, a4  & V a3 , a4 , a5  & La3 , a1, a5 & V a4 , a2 , a3  & V a4 , a3 , a6  & La4 , a2 , a6  & V a5 , a3 , a6  & V a6 , a4 , a5 }Для того чтобы выделить объект, принадлежащий классу «троек»,необходимо доказать справедливость логического следованияS a1,, a6   x1,..., x6 Ax1,..., x6 Для рассматриваемого примера количество формул в F-наборе δ=5,количество атомарных формул в S a1, , a6  с одним и тем же предикатнымсимволом s1  8 и s2  2 для предикатов V и L соответственно ( s1  8 ),наибольшее количество аргументов в атомарной формуле l  3 .

Характеристики

Список файлов диссертации