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

, 4 ^ «98

На правах рукописи

Абдрахимов Илья Сабитович

Процедурная семантика и стратегии поиска решения в системе Флэнг

05.13.16- применение вычислительной техники, математического моделирования и математических методов в научных исследованиях

АВТОРЕФЕРАТ диссертации на соискание ученой степени кандидата физико-математических наук

Иркутск - 1998

Работа выполнена в Иркутском государственном университете

Научный руководитель: доктор физико-математических наук,

профессор Манцивода A.B.

Официальные оппоненты: доктор физико-математических наук

Пальчунов Д. Е.;

кандидат физико-математических наук, доцент Дулатова З.А.

Ведущая организация: Красноярский государственный

университет.

Защита состоится 25 декабря 1998 г. в 14 часов на заседании диссертационного совета Д 063.32.04 в Иркутском государственном университете по адресу: 664003, г. Иркутск, бульвар Гагарина, 20.

С диссертацией можно ознакомиться в библиотеке Иркутского государственного университета (бульвар Гагарина, 24).

Автореферат разослан 24 ноября 1998 г.

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

Бельтюков Н.Б.

Общая характеристика работы

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

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

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

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

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

Научная новизна работы.

Построение процедурной семантики на основе Е-программирования1 и параллельного программирования в ограничениях (сс - программирование2) позволило:

• оперировать широким классом логических формул, допускающих эффективную процедурную семантику;

• использовать ограниченные кванторы для реализации методов работы с дизъюнктивными ограничениями;

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

В диссертации рассматривается наиболее важный случай работы с равенством, а именно, когда отношение равенства удовлетворяет теории равенства Кларка. Именно этот вариант отношения равенства наиболее распространен в логическом программировании.

'Гончаров С.С., Свириденко Д.И. ^-программирование// Вычислительные системы, 107, Новосибирск, 1985, с.24-51.

2V. Sarasvat. Concurrent Constraint Programming// the MIT Press, 1993, 486p.

Исследовано поведение различных стратегий поиска решения комбинаторных задач. Сформулированы и доказаны теоремы о полноте и корректности -машины на моделях теории равенства Кларка.

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

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

Структура и объем дисертации. Диссертация состоит из введения, четырех глав, заключения и списка литературы. Объем диссертации 110 страниц, список литературы содержит 93 пункта, включая работы автора.

Содержание работы

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

Первая глава посвящена построению процедурной семантики для систем удовлетворения ограничений посредством описания £ и Е+-машин.

В первом параграфе определяется понятие системы ограничений как частного случая информационной системы 3.

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

В данной работе рассматривается вариант Е-исчисления, в котором равенство удовлетворяет теории Кларка, имеющей следующие аксиомы:

• с ф d для всех пар различных констант;

• f(xli • • • i хп) ф g[yii Уп), если / и д различные функциональные символы;

• f(x i,..., х„) ф с, где п > 0, а с - нуль-местный функциональный символ (константа) ;

• f{x 1 ,...,хп)фх, если х е Var(f(xiхп));

• xi ф у\ V... Vxn фуп-± f(xi,...,xn) ф f{yi,...,yn) для каждого функционального символа /;

• х — xj

• xi = yi к ... к хп = уп ->/(xi....,x„) = f(yi, ...,у„);

• Xi - Ух к ... к х„ - уп к p(xi,...,xn) -» р(у1,...,уп) для каждого предикатного символа р.

Пусть С — множество функциональных и предикатных символов {С содержит нульместные предикатные символы true и false) и 3? - конструктивная модель языка С. Предикатные и функциональные символы, входящие в С, будут обозначать базовые или "встроенные ограничения" (в качестве одного из встроенных отношений должно выступать равенство). Расширим £ множеством новых предикатных символов {pi,... ,рк} и обозначим С* — С U {pi,...,рк}- Новые предикатные символы будут обозначать так называемые определяемые

3Dana S. Scott. Domains for denotational semantics.// In Proceedings of ICALP, 1982.

ограничения, которые определяются через встроенные ограничения с помощью Е-программ.

Атомарная формула — выражение вида р(<1,... ,tn), где р есть п-местный предикатный символ языка С, а термы - является Е-формулой. Если Р и £? - Е-формулы, Н - формула сигнатуры С, не содержащая неограниченный квантор существования, то Р & (?, Р V в, Н Р, (Зх € у)Р, (Ух б у) .Г, (3х)Р - также Е-формулы. Обозначим через Уаг(Р) множество свободных переменных Р. Определением ограничения будем называть выражение вида:

р(хь...,х„) О Р,

если р(х1,..., хп) — атомарная формула с определяемым предикатным символом р, а Г — Е-формула языка £*, такая что Уаг(-Р) С {х1,..., х„} и XI,..., х„ есть различные переменные.

Е-программа есть множество {£>1,..., Дь, Рх,..., Рт}, где Д, есть определения ограничений (не более одного для каждого определяемого предикатного символа), а ^ есть Е-формулы. Е-программу можно понимать как запрос: выполняется ли конъюнкция ограничений Р,-, и если выполняется, то при каких значениях переменных. Механизм вычисления Е-программы описывается с помощью Е-исчисления4. Выводимость формулы Р в Е-исчислении из множества исходных формул Д и программы Г обозначим Л и Г Ьд Р.

Третий параграф посвящен изложению основных принципов параллельного программирования в ограничениях.

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

4А.В. Манцивода. И-программирование и проблемы дискретной оптимизации// Иркутск, Иркутский университет, 1994, 245с.

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

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

В дальнейшем большими буквами греческого алфавита будем обозначать некоторую совокупность ограничений и определений ограничений. Большими буквами латинского алфавита будем обозначать ограничения. Под записью будем понимать память Е-машины, состоящую из множества ограничений и определений Г, и ограничения Г. Под записью {б11Г) {| Г} будем понимать преобразование памяти машины по одному из правил преобразования, от состояния {С|Г} к состоянию {/-'¡Г}. Подстановочными равенствами будем называть формулы вида х — I, где х - переменная, а { - терм.

Будем называть множество подстановочных равенств разрешимым, если каждая переменная встречается не более чем один раз в левой части равенств. Если множество равенств Л совместно в теории Кларка, то мы можем сконструировать разрешимое множество Л', которое эквивалентно Л с точки зрения теории Кларка. Разрешимое множество Л' определяет подстановку г|х = г£Л'> которая

производит одновременную замену переменных термами. Результат

применения подстановки, определяемой подстановочными равенствами содержащимися в множестве формул Л, будем обозначать ¿Л (FA) Приведем примеры правил замыкания S-машины: (V-удаление)

{(V* е {¿1,...,«*}№) I г} {F(h),...,F(tk) |г}

{(V* б 0№) | г} и- г

(З-удаленне)

{(3x)F | Г} ^ {F | Г}

если х не входит в Г (в противном случае переменную нужно переименовать)

{(За: 6 {гь • ■ ..it})*1 I Г} н. {(х = h V ... V х = tk), F | Г}

{(Зг е 9)F{x) | Г} Н> {false} (применение определения)

^ {F', x[=h,...ix'k = tk, P{Xl,.. .хк) F 1 Г}

где х[ £ 'jar(Г) и F' получено из F заменой вхождений переменных

ж, на х'{.

(JJ-оценка)

{P(xi,...,atn) |Г}^{У1 =h,...,ym =tm | Г}, (1)

если

зг И (Э'Й) • ■ - (зы^!)... (Vzt)P(<ei,. • •, <».)

где

• tXi - значения переменных xt- вычисленные на множестве подстановочных равенств содержащихся в памяти Г.

• ti - единственные значения переменных ¡/,, и выполняется: 3f?H(^i)...(Vzi)P(i:ri,...(ij:n) <yi <r-tu...ym <r-tm>

• Var(tXl,.. ,,tXn) = {yi,...ym,zi,---,zk},

* yi Í Var{tj)¡ где ¡ = l,mij = 1 ,m

• P не содержит определяемых символов и все вхождения переменных в Р свободны.

В дальнейшем замыкание множества ограничений посредством правил замыкания будем обозначать >-?.

Секвенция

Fx, ...,Fm\rF

истинна тогда и только тогда, когда F выводится из Fi,..., Fm с помощью последовательности применений правил замыкания, или

3Í Направило выбора (V-удаление):

{Fi V ... V Ft | Г} {F¿ I Г} 1 < г < к

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

Пусть Ai,.. ,Ап - последовательность множеств E-формул (состояний памяти E-машины) такая, что A¿+i получается из Ai применением некоторого правила преобразования. Назовем такую последовательность корректной, если правило выбора применяется в ней только к тем множествам, к которым невозможно применить ни одно из правил замыкания.

Пусть Г = {Gi,..., Gk, Di,..., Drn} - память S-машины, где Gi - E-формулы, аД - определения предикатов. Будем говорить, что Г является S-реализуемой, если существует корректная последовательность преобразований £-машины с памятью Г, приводящая к машине с памятью {xi = t\,...,Xk = Di,. ■., Dm}, где x-¡ = ti,... ,Xk = i* — подстановочные равенства, причем не более одного на каждую переменную. Формула F E-реализуема в £-программе Г, если множество {F | Г} Е-реализуемо.

Если в памяти E-машины появилось ограничение false, то будем считать, что получено противоречивое состояние памяти Е-машины.

Поскольку применение правила выбора допускает несколько вариантов (в зависимости от выбираемого дизъюнкта), то каждое применение такого правила определяет в последовательности преобра-

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

В пятом параграфе описывается абстрактная Е+-машина, в которой в отличии от Е-машины, имеются правила преобразования, оптимизирующие работу с дизъюнктивными ограничениями.

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

(правило локальной совместности)

ДСГ {F | A} h false {FV G | Г} м- {G | Г}

Доменовой дизъюнкцией (доменом) будем называть выражение вида х — ti W .. .У х — t„, где х = t, — подстановочные равенства. Обозначим Dx доменовую дизъюнкцию, соответствующую переменной х.

Обозначим через Ai,..., Д„ такую последовательность множеств ограничений, что Ai+i получена из Д, с помощью одного из определенных выше преобразований Е-машины.

Пусть Ai и Аг — множества доменовых дизъюнкций. Пересечением информации, содержащейся в множествах Aj и Аг, называется множество формул Aj П А2 = {D\ V D\ | Пхх € A ], [Д Е Л2}.

Введем бинарную операцию Д, определенную на множестве пар дизъюнкций (Df, DJ), ее результатом является дизъюнкция, составленная из дизъюнктов входящих, как в дизъюнкцию Df, так и в дизъюнкцию D*. Объединение информации, содержащейся в множествах Ai и Л2 называется множество Л) U A-j = {D | D — Df Д Df} где Df ель dx2 ел2. (конструктивная дизъюнкция)

{F | A} A (Qf U \F) {G | A} A (Sig U Ад) {FVG | r)}^{FV(? | (Г \ Л) U (Л U (Лг П Ag))}

где Л — множество доменовых дизъюнкций соответствующих переменным входящим в формулу F V G; Qf и Qg — потомки формул F и G, а Ар и Ас — потомки формул из Л в результате замыкания множеств {F | Л} и {G | Л}, соответственно. Правило конструктивной дизъюнкции позволяет получить из дизъюнкции информацию, общую для всех ее дизъюнктов. Это дает возможность работать с данными, спрятанными в дизъюнкции еще до того, как выбрана некоторая ее альтернатива.

(правило истинного дизъюнкта)

{Д'> -Pi V ... V Pi | Г) i-> {Р,- | Г} 1<г<*

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

В шестом параграфе рассматривается стратегия глубокого возврата, оптимизирующая механизм возврата в Е+-машине.

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

Во второй главе рассмотрены вопросы полноты и корректности Е+ -машины.

Пусть Дь..., Д„ — последовательность состояний памяти Е-машины. Обозначим через Ti(Ai,R,,Fi) преобразование (применение Е-правила) такое, что к памяти А,- применяется правило Я, с посылкой Fi. Под записью Т,(Д,, R,,Fi) = Д;+[ будем понимать то, что состояние Е-машины Ai+i получено из состояния А,- преобразованием Ti(Ai,Ri, Fi).

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

Теорема 1. Пусть возможны последовательности непротиворечивых преобразований Е(£+)-машины.

Тг(Ах, Ии Г) = Л2, Т2(Л3) Я2, С) = Л3

и

Т° (Ль Я3,0) = Л$, Г2° (Л2, Кг, Е) = Л^

Тогда: или для всех х € шг(Лх) выполняется гЛз = £Лз ила существует одна из следующих последовательностей преобразований, применением правила 5? оценки:

Гз(ЛЗ) = А4,...>ГГ1_1(ЛП_1)=ЛП

или

такая, что хАз = хЛ" или гЛз =

Теорема 2. Пусть Г - множество определений предикатов (программа), а Е - И-формула. Тогда если {Р | Г} £+-реализуемо, то Г Не Р.

В Е+-машине принята стратегия поиска в глубину с хронологическим возвратом. В случае поиска в глубину проблема полноты может быть сформулирована следующим образом: будет ли система полна в случае, если всегда выбирается правильная альтернатива? Формально полнота Е+-машины определяется так: Е+-машина полна, если для любой Е-программы Г = {0},..., <гт, ..., I?*} выполняется: если С?!,..., Ст - выводимы из {.От,..., О*} в Е-исчислении, то программа Г Е+-реализуема.

Учитывая это определение, формулируется следующая теорема. Теорема 3. Пусть 3? - конечная модель, Е - замкнутая Е-формула, Тогда, если Г Е, то Е £+ -реализуема в программе Г.

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

пользованию глубокого возврата в функционально логическом языке программирования в ограничениях Флэнг5.

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

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

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

Для оценки были выбраны задача планирования организационно-технических мероприятий (ОТМ) для АСУ иерархической структуры и задача о строительстве моста. Нами получены решение этих задач с использованием метода удовлетворения ограничений на конечных областях, реализованного в функционально-логическом языке Флэнг. Как показали наши исследования, предложенные в работе методы локальной совместности и глубокого возврата позволяют значительно повысить эффективность языка Флэнг.

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

Основными результатами настоящей работы можно считать следующие:

• Развитие идей ^-программирования, построение эффективной процедурной семантики для Е-языков в случае теории равенства Кларка.

• Адаптация понятия активной дизъюнкции для Е-языков в случае теории равенства Кларка. Теоретическое обоснование метода решения комбинаторных проблем, основанного на активной дизъюнкции. Доказательство базовых свойств, а также полноты и корректности Е и Е+-машин.

5А.В. Манцивода. Флэнг - язык искусственного интеллекта// Кибернетика, 1993, N0. 5. С.350-367

• Разработка метода глубокого возврата, позволяющего более эффективно решать комбинаторные задачи.

• Апробация вышеперечисленных результатов на сложных индустриальных задачах.

Публикации по теме дисертации

1. Абдрахимов И.С., Манцивода A.B. Полнота и корректность Сигм а- машины. //Сб. Алгебра, логика и приложения. - Иркутск, 1994. - С. 156-181.

2. Абдрахимов И.С., Манцивода A.B. Активные дизъюнкции во Флэнге. //Всерос. школа Компьютерная логика, алгебра и ин-теллектное управление, (под. ред. С.Н. Васильева, М.В. Почта-ренко), Сб. докладов. Т.1 - Иркутск, 1993. - С. 158-174.

3. Абдрахимов И.С., Манцивода A.B. Полнота стратегии локальной совместности. //Межд. конф. по матем. логике. Тез. сообщений. - Новосибирск, 1994. - С. 3-5.

4. Абдрахимов И.С., Манцивода A.B. Сигма-программирование и теория равенства Кларка. - ИНПРИМ. Тезисы докладов, часть IV. - Новосибирск: Изд-во Института математики СОР АН, 1998. - С. 36-37.

5. Абдрахимов И.С., Манцивода A.B. Глубокий возврат в Е-машияе. // Международная конференция по прикладной логике: Тезисы сообщений.- Иркутск, 1995 - С. 3-4.

6. Abdrakhimov I. and Mantsivoda A. Intelligent Backtracking in Fiang. //International Workshop on Constraint Processing at CSAM'93, St. Petersburg (ed. M. Meyer), DFKI Document D-93-14, p.215-221 DFKI Kaiserslautern, P.O. Box 2080, 67608 Kaiserslautern, Germany

7. Abdrakhimov I. and Mantsivoda A. The E-machine, its Soundness

and Completeness. /Department of Computing Science, K.U.Leuven. Report CW234, June 1996 p. 31

Редакционно-издательский отдел Иркутского государственного университета Лицензия ЛР N020592 от 9.07.97г. 664000, Иркутск, бульвар Гагарина, 36

Подписано в печать 21.11.1998г. Формат бумаги 60x84 1/16. Объем 1,0 п.л. План 1998 г. Заказ 43. Тираж 100 экз.

Отпечатано в ОПВЦ ИГУ 664003, Иркутск, б. Гагарина, 20