Методы и инструментальные средства программирования в булевых ограничениях тема диссертации и автореферата по ВАК РФ 05.13.11, кандидат технических наук Богданова, Вера Геннадьевна

• Богданова, Вера Геннадьевна
• кандидат технических наук
• 2005

Оглавление диссертации кандидат технических наук Богданова, Вера Геннадьевна

введение.

глава 1. методы и программные средства решения задач удовлетворения ограничений с конечными областями значений переменных (обзор).

1 1.1. Основные понятия и определения.и

J 1.2. Классификация задач удовлетворения ограничений с конечными областями и алгоритмов их решения.

1.3. Оценка эффективности алгоритмов.

1.4. Инструментальные средства автоматизации программирования в булевых ограничениях.

глава 2. алгоритмы решения задачи выполнимости булевых ограничений.

2.1. Базовый алгоритм.зз

2.2. Усовершенствованный алгоритм.

2.3. Гибридный алгоритм.

2.4. Сравнительный анализ разработанных алгоритмов.

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

3.1. Средства спецификации булевых ограничений в международном формате DIMACS и его расширениях.

3.2. Булевы модели некоторых дискретных задач.

3.3. Технология булева моделирования дискретных задач.

1 3.4. Высокоуровневые языковые средства задания булевых ограничений в инструментальном комплексе РЕБУС.

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

4.1. Постановка задачи и основные функциональные требования к инструментальному комплексу РЕБУС.

4.2. концептуальная модель, принципы организации и архитектура инструментального комплекса РЕБУС.

4.3. Архитектура и функциональные возможности подсистем инструментального комплекса РЕБУС.

4.4. Визуальный пользовательский интерфейс и основные аспекты программной реализации РЖ РЕБУС.

Введение диссертации (часть автореферата) на тему «Методы и инструментальные средства программирования в булевых ограничениях»

Одним из перспективных направлений исследований в современном программировании [1,2] является направление, связанное с программированием в ограничениях (Constraint Programming — CP). Теоретическую основу этого направления составляют методы решения задач удовлетворения ограничений (Constraint Satisfaction Problem - CSP). Задачи удовлетворения ограничений представляются в виде множества переменных и системы ограничений над ними. Решением задачи является такой набор значений этих переменных (из области допустимых значений), который удовлетворяет всем заданным ограничениям. Многие задачи науки и техники формулируются или могут быть сформулированы как задачи удовлетворения ограничений.

К важному классу ограничений относятся булевы ограничения, представляемые в виде систем булевых уравнений, и связанные с этим классом задача выполнимости булевых ограничений (Boolean Constraint Satisfaction Problem - BCSP) и задача программирования в булевых ограничениях (Constraint Boolean Programming - СВР).

В [3,4] отмечается, что булевы уравнения естественным образом возникают при исследованиях, имеющих дело с отображениями, области определения и значений которых лежат в пространствах векторов с двоичными компонентами (Z?2={0,l}). Таковы, например, уравнения алгебры логики; соотношения, описывающие бинарные отношения со свойствами типа транзитивности, связности, асимметрии и т.д.; булевы неравенства; задачи, описывающие нахождение оптимальных переключательных схем; задачи проверки специальных свойств булевых функций, таких как линейность, монотонность, самодвойственность, существенная зависимость булевой функции от переменной и т.д.

Задача булевой выполнимости является фундаментальной проблемой в математической логике и теории вычислений. Следует отметить, что многие практические задачи могут быть сформулированы как задачи булевой выполнимости (или решение системы булевых уравнений). К ним относятся [5] задачи криптографии, логического программирования, доказательства теорем, дедуктивного и абдуктивного вывода, нейросетевых вычислений, машинного зрения, планирования действий роботов, планирования вычислений в системах синтеза программ, оптимального проектирования, разработки систем баз знаний, компьютерной графики, моделирования цепей, разработки СБИС, создания новых компьютерных архитектур и сетей вычислительных машин, коммуникации, безопасности, составления расписаний, интеллектного управления, различные задачи на графах, шахматной доске и многие другие.

Формально задача решения булевых уравнений формулируется следующим образом [3]: пусть X = {xv.1xn) — упорядоченное множество булевых переменных (х{еВ2 для всех i = l,n; Z?2 = {0,1}). Задано т булевых соотношений (система уравнений) вида где yj(/ = l,7«) - произвольные булевы функции своих аргументов. Требуется найти одно, несколько или все решения системы (1) или установить ее несовместность.

Следует заметить, что первая NP-полная задача - задача "выполнимости КНФ" (задача булевой выполнимости или SAT задача) есть, по существу, задача распознавания совместности систем уравнений [6] fiih^K „) = 0'

1)

Х°К V . V =1 (/ = 1,.,/и), l '*(/) 4 где переменная

X, при сг, =0, р >р х, при сг =1.

V р p = \,k(i)

Двойственная к (2) система уравнений вида (1) записывается следующим образом: хк л .a XiHi) =0 (i = l,.,m). (3)

Известно, что любая система вида (1) может быть представлена одним т эквивалентным уравнением /(jc,,.,jc„) = [J/(x/i,.,jc/t(()) = 0. Поэтому далее 1 будем рассматривать в основном одно стандартное уравнение = 0. (4)

Известные подходы к решению булевых уравнений. Можно выделить три основных подхода к решению систем булевых уравнений — это аналитический, дискретный и непрерывный.

Истоки аналитического метода можно найти еще у самого Дж. Буля (см., например [7]), который получил решение уравнения с одним неизвестным. Дальнейшее развитие аналитического метода связано с именами его ближайших последователей, таких как У. Джевонс, Э. Шредер и в особенности казанский математик П.С. Порецкий [7]. Уточнение метода Буля-Порецкого выполнено Н.П. Брусенцовым [8]. Систематическое изложение проблемы аналитического решения булевых уравнений к концу 70-х годов представлено в объемной монографии [9]. Акерс [10] использовал в 1959 г. для решения уравнений булевы производные и сформировал основы для развития булевого дифференциального исчисления. В [4] подход Акерса нашел свое дальнейшее развитие. Условия существования решения и вид решений для некоторых специальных важных классов систем булевых уравнений можно найти в работах Чистова В.П. [11] и Пандефа Е. [12]. Из работ последних лет следует выделить исследования B.C. Левченкова [3], в которых получен общий вид решения булева уравнения со многими неизвестными, даны условия единственности решения, а также рассмотрены вопросы решения неявных булевых уравнений. Обсуждение проблемы аналитического решения 'задачи "выполнимости КНФ" с использованием средств компьютерной алгебры системы MAPLE (специализированный пакет математической логики) представлен на сайте [13].

В дискретных методах задача решения булева уравнения рассматривается как частный случай задачи удовлетворения ограничений, когда домены, на которых определены переменные, являются бинарными. Поисковое пространство является дискретным, в котором реализуются разнообразные стратегии перебора. Самый простой способ — это полный перебор. С целью сокращения поискового пространства предложено много улучшенных методов, таких как алгоритмы с хронологическим возвратом, распространением ограничений, интеллектуальным возвратом, метод резолюций, алгоритмы с применением многозначной логики, алгоритм Дэвиса-Патнема, жадный алгоритм и целый ряд других алгоритмов и их комбинаций (см., например, [6,14,15]). Список комбинаторных SAT-решателей можно найти на сайте [16]. Все предлагаемые методы ориентированы на представление левой части булевого уравнения (4) в одной из нормальных форм (конъюнктивной, дизъюнктивной или разностной). Разработка методов и алгоритмов решения булевых уравнений (4) с произвольной левой частью считается [5] перспективным направлением исследований в силу того, что такие уравнения часто возникают в практических задачах.

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

Пионерским в этом направлении решения булевых уравнений является итеративный метод С.Ю.Маслова [17], который сочетает механизм расширения области поиска (с целочисленной до рациональной) с принципом глобальности обработки информации и итеративной схемой уточнения решения. В [18] приведено три варианта семантики итеративного метода С.Ю.Маслова: это импликативная семантика, экстремальная семантика и химико-кинетическая семантика. Интересный подход к погружению задачи решения булевых уравнений из В^ в R", основанный на физических аналогиях и дифференциальных моделях, предложен в [19] — это модель химической кинетики, модель «сотворения мира» и модель резонанса. Из зарубежных работ следует выделить исследования Jun Gu [5], который сводит задачу решения булева уравнения в к задаче безусловной глобальной параметрической оптимизации некоторой целевой функции в R".

Актуальность темы. Существует достаточно большое количество программ решения задач выполнимости. Список зарубежных систем можно найти на сайте [16]. В качестве входного языка этих программ используется фрагмент международного формата DIMACS [20] представления булевых ограничений в виде конъюнктивной нормальной формы пропозициональной логики (системы булевых ограничений вида (2)). Программы, решающие системы булевых ограничений общего вида (1), автору неизвестны. Средства автоматизации построения булевых моделей (в формате DIMACS) по содержательной (ориентированной на конечного пользователя) постановке задачи в этих программах отсутствуют, взаимодействие с программой возможно только в режиме командной строки (визуальный пользовательский интерфейс отсутствует). Из числа отечественных систем следует выделить решатели UNICL [21], UniCalc [2,22] и интегрированный программный вычислительный комплекс SibCalc [22, 23], предназначенные для решения задач, представленных системами алгебраических уравнений, неравенств и логических выражений и реализованные на основе интервальных методов и 8 методов распространения ограничений. Эти системы имеют кроме арифметического логический блок для прямого решения булевых уравнений и визуальный пользовательский интерфейс, но в основном применяются для решения численных задач удовлетворения ограничений. Таким образом, актуальной является проблема разработки эффективного, ориентированного на конечного пользователя инструментария автоматизации программирования в булевых ограничениях (включая высокоуровневые средства построения булевых моделей для различных классов дискретных задач).

Цель работы. Основная цель диссертации состоит в исследовании существующих на данный момент достижений в области решения систем булевых ограничений; разработка специализированных алгоритмов и программ для решения булевых уравнений; создании принципиально новой интегрированной инструментальной среды, объединяющей решатели комбинаторных задач большой размерности в единую систему, позволяющую автоматизировать процесс построения булевой модели решаемой дискретной задачи, выбирать из базы знаний (исходя из свойств полученной модели и накопленной статистики решения задач) подходящий алгоритм решения, проводить вычислительный эксперимент, сохранять результаты расчетов в пользовательской базе данных, осуществлять тестирование алгоритмов с использованием эталонных тестовых задач и тестов из библиотеки SATLIB [24], включать в базу знаний инструментальной среды новые модели и алгоритмы.

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

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

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

Практическая значимость. Применение разработанных в диссертации методов и инструментальных средств автоматизации программирования в булевых ограничениях позволяет сократить трудозатраты на разработку, отладку и исследование булевых моделей, повышает качество и сокращает сроки выполнения необходимых многовариантных расчетов. Решатели ИК РЕБУС зарегистрированы в Российском агентстве по патентам и товарным знакам (РОСПАТЕНТ) и используются для проведения экспериментальных расчетов по плановым темам НИР в ИДСТУ СО РАН. Применение ИК РЕБУС в учебных целях в качестве программного инструмента решения задач дискретной математики позволяет обучить студентов основным навыкам булева моделирования, наглядно ознакомить их с существующими комбинаторными методами решения классических задач искусственного интеллекта.

Реализация. Исследование, разработка и применение рассматриваемых в диссертации программных средств выполнялись в рамках плановых тем ИДСТУ СО РАН "Методы автоматизации исследования и разработки интеллектных систем" (№ гос. per. 01.99.00 07820, 1999-2001 гг.), "Методы и инструментальные средства организации распределенных вычислений в сети Интернет" (№ гос. per. 01.20.01 11785, 2002-2003 гг.), "Интегрированные информационно-вычислительные и коммуникационные ресурсы: интеллектные методы организации, автоматизации разработки и применения" (2004-2006 гг.), в рамках комплексного интеграционного проекта СО РАН "Методы, технологии и инструментальные средства создания вычислительной инфраструктуры в Internet" (2003-2005 гг.), в рамках проектов РФФИ №98-01-00160 "Численное решение больших разреженных систем булевых уравнений", №01-07-90220 "Разработка инструментальной среды для создания и поддержки функционирования распределенных пакетов знаний в сети Интернет" и №04-07-90358 "Разработка и реализация распределенной вычислительной системы решения булевых уравнений большой размерности", в процессе реализации программы президиума РАН №21 "Разработка фундаментальных основ создания научной распределенной информационно-вычислительной среды на основе технологий GRID" (проект №6 "Планирование и оптимизация схем решения задач в распределенной мультиагентной вычислительной среде ").

Результаты исследований используются в Иркутском государственном университете путей сообщения при проведении практических занятий по дисциплине «Теория дискретных устройств автоматики и телемеханики», а так же в Информационно-вычислительном центре Восточно-Сибирской железной дороги филиала ОАО РЖД для разработки системы поддержки принятия решений при решении задач составления плана ремонта электропоездов и оперативного плана отправления локомотивных бригад в условиях отсутствия жесткого расписания движения грузовых поездов.

Апробация. Основные результаты работы докладывались на следующих конференциях: I Международной научно-практической конференции "Интеллектуальные электромеханические устройства, системы и комплексы" (Новочеркасск, 2000), II Международной научно-практической конференции "Развивающиеся интеллектуальные системы автоматизированного проектирования и управления" (Новочеркасск, 2002), V Международной научно-практической конференции "Моделирование. Теория, методы и средства" (Новочеркасск, 2005), на XII Байкальской международной школе-семинаре "Методы оптимизации и их приложения" (Иркутск, 2001), на конференциях "Ляпуновские чтения & Презентация информационных технологий" (Иркутск, 2001, 2002, 2003) , на VII международной конференции "Проблемы управления и моделирования в сложных системах "(Самара, 2005).

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

Заключение диссертации по теме «Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей», Богданова, Вера Геннадьевна

8) результаты работы сохраняются в БД пользователя.

Действия 1)-5) являются обязательными, действия 6)-8) выполняются по желанию пользователя. Выбор программы-решателя основывается на запросе пользователя, в котором в качестве условий отбора могут быть указаны метод, алгоритм, вид модели, вычислитель, вид постановки задачи. Вычислитель включается в запрос, если модель задана в программном виде. Программы-решатели представляют собой исполняемый файл и хранятся в определенном каталоге ИК РЕБУС. Решатели условно можно разделить на две группы:

1) булевы ограничения для одних представлены в виде модели в формате DIMACS;

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

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

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

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

Таким образом, в концептуальной модели ИК РЕБУС можно выделить следующие основные понятия:

Вид Модели - форма представления булевых ограничений.

Метод — конструктивный подход к решению дискретной задачи, имеющий математическое обоснование.

Алгоритм - конкретизация метода решения для определенного класса ЭВМ.

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

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

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

Постпроцессор - программа, обрабатывающая результат работы решателя.

Формат параметров решателя - спецификация входных параметров решателя.

Параметры вычислителя — спецификация формальных параметров программы-вычислителя.

Вид ПЗ — перечень возможных видов постановок задач.

Вид Статистики — перечень возможных критериев оценки работы решателя.

Результат — результаты работы решателя, обработанные постпроцессором и снабженные информацией о прохождении процесса решения: дата, имя решателя, размерность модели и т.д. Модель - компьютерный вариант булевой модели конкретной дискретной задачи. На рис. 3 представлена архитектура ИК РЕБУС в виде структурной модели, отображающей на самом общем уровне связь между следующими тремя основными подсистемами: . подсистемой моделирования;

ВИЗУАЛЬНЫЙ ПОЛЬЗОВАТЕЛЬСКИЙ ИНТЕРФЕЙС

АСТРОЙКА ПАРАМЕТРОВ СИСТЕМЫ

УСТАНОВКА СВОЙСТВ ОБЪЕКТОВ ИК РЕБУС

ПОДСИСТЕМА МОДЕЛИРОВАНИЕ

КОНСТРУКТОР

РКПАКТОР

ГЕНЕРАТОР

KOHRRPTOP |

АНАЛИЗАТОР j

1 nPRnPOITRCCOP |

Входные дшшые 1

Модели

ZL

ДАННЫЕ

Решатели

Вычислители

ПОДСИСТЕМА ВЫЧИСЛИТЕЛЬНЫЙ ЭКСПЕРИМЕНТ

ПЛАНИРОВЩИК ИСПОЛНИТЕЛЬ

ВИЗУАЛИЗАТОР

БАЗА ЗНАНИЙ

БД

ПОЛЬЗОВАТЕЛЯ обозначение каталога (папки) обозначение области оперативной памяти

ПОДСИСТЕМА РАБОТА С ДАННЫМИ

СПРАВОЧНИК

ПОЛЬЗОВАТЕЛЬ

АДМИНИСТРАТОР

Объекты ИК

Параметры среды

Рис. 3. Структурная модель архитектуры ИК РЕБУС. подсистемой вычислительного эксперимента; подсистемой работы с базой знаний.

Обмен информацией между подсистемами организован следующим образом. Вся совместно используемая информация о предметной области хранится в общей базе знаний РЖ РЕБУС, доступной всем подсистемам. Промежуточные результаты обработки информации на всех этапах работы ИК, являющиеся входными для других этапов работы, передаются в виде файлов, сохраняющихся в каталогах ИК РЕБУС. Конечные результаты работы сохраняются в файлах и БД пользователя. Данные, представляющие собой значение свойств объектов ИК, служащих для настройки интерфейса, и параметры среды хранятся в оперативной памяти. Модель потоков данных приведена на рис. 4.

Рис. 4. Модель потоков данных ИК РЕБУС при прохождении всех этапов работы

В качестве модели управления инструментального комплекса РЕБУС была выбрана модель управления, основанная на событиях [116] , которая позволяет относительно легко проводить последующую модернизацию. Новую подсистему можно интегрировать в систему, регистрируя ее события в обработчике событий. Модульная декомпозиция системы была проведена в соответствии с объектно-ориентированным подходом, преимущества которого хорошо известны [117-119]. Система структурирована в виде совокупности слабо связанных объектов с четко определенными интерфейсами. Объекты вызывают сервисы, предоставляемые другими объектами. Поскольку объекты слабо связаны между собой, можно изменять реализацию того или иного объекта, не воздействуя на остальные объекты.

В соответствии с описанным выше подходом и учетом функциональных требований был разработан и реализован инструментальный комплекс РЕБУС [30,35], позволяющий объединить и автоматизировать в рамках одной инструментальной среды средства представления и обработки знаний при решении задач удовлетворения булевых ограничений. В следующем разделе описывается архитектура подсистем ИК РЕБУС.

4.3. Архитектура и функциональные возможности подсистем инструментального комплекса РЕБУС.

4.3.1. Подсистема моделирования. Подсистема моделирования предназначена для автоматизации построения булевой модели дискретной задачи. В эту подсистему входят следующие основные компоненты: Конструктор модели; Редактор модели; конвертор; генератор; препроцессор.

Общая схема подсистемы моделирования приведена на рис. 5. К основным функциям подсистемы моделирования относятся следующие: задание системы ограничений на входном языке ИК РЕБУС, генерация булевой модели в одном из выходных форматов, преобразование булевой модели, перевод булевой модели из одного формата в другой.

Задание системы ограничений в ИК РЕБУС осуществляется с помощью двух программных компонентов: конструктора модели и редактора модели. Конструктор позволяет задать ограничения в диалоговом

ПОДСИСТЕМА МОДЕЛИРОВАНИЯ

ВБФ - вычислитель булевой функции

Рис. 5. Архитектура подсистемы моделирования. режиме с помощью графического пользовательского интерфейса. В пакетном режиме можно явно записать эти ограничения на языке ЯСФОР в текстовом файле и перевести их конвертором в формат DIMACS. Редактор модели предоставляет средства для ввода ограничений в виде математических формул.

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

В редакторе модели система ограничений может быть введена в виде формул на математическом языке. Для ввода формул предусмотрены следующие возможности: ввод формулы в формате Latex [120] средствами ИС РЕБУС; импорт формулы в формате Latex из внешнего файла; ввод формулы с помощью математического редактора Mathtype в среде ИК РЕБУС; импорт формулы в формате математического редактора Mathtype. Система ограничений в формате DIMACS может быть также создана или отредактирована по стандартной технологии работы с документом в многооконном текстовом редакторе, встроенном в ИК РЕБУС.

Конвертор, генератор и препроцессор представляют собой библиотеки динамической компоновки. Конвертор включает следующие функции преобразования форматов булевой модели: перевод из формата Latex в DIMACS; перевод с языка ЯСФОР в формат DIMACS; перевод из ДНФ в КНФ и обратно.

Заключение.

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

1. Новые алгоритмы полного поиска с возвратом для решения больших «> разреженных систем булевых уравнений.

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

3. Декларативный язык описания булевых ограничений ЯСФОР.

4. Инструментальный комплекс РЕБУС, автоматизирующий все этапы проведения вычислительного эксперимента при решении задачи удовлетворения булевых ограничений.

5. Булевы модели ряда классических и практических дискретных задач, разработанные с применением технологии моделирования ИК РЕБУС.

Список литературы диссертационного исследования кандидат технических наук Богданова, Вера Геннадьевна, 2005 год

1. Яхно Т.М. Программирование в ограничениях: обзор и классификация подходов и методов. Системная информатика: Сб. науч. тр. -Новосибирск: Наука, 1995. Вып. 4: Методы теоретического и системного программирования. - С.160-192.

2. Ушаков Д.М., Телерман В.В. Системы программирования в ограничениях. Системная информатика: Сб. науч. тр. Новосибирск: Наука, 2000. - Вып. 7: Проблемы теории и методологии создания параллельных и распределенных систем. — С.275-310.

3. Левченков B.C. Булевы уравнения. М.: ДИАЛОГ МГУ, 1999. - 72 с.

4. Бохманн Д., Постхофф X. Двоичные динамические системы. М.: Энергоатомиздат. - 1986. - 401 с.

5. J.Gu, P.W.Purdom, J. Franco, and В. Wah. Algorithms for the Satisfability problem:a survay. DIMACS Series on Discrete Mathematics and Theoretical Computer Science, American Mathematical Society. 1997. - V. 35. -РЛ9-151.

6. Горшков С.П. Применение теории NP-полных задач для оценки сложности решения систем булевых уравнений// Обозрение прикладной и промышленной математики, серия дискретной математики. — 1995. — Т.2. — Вып.З.-С. 325-398.

7. Стяжкин Н.И. Формирование математической логики. — М.: Наука. — 1967.-508 с.

8. Брусенцов Н.П., Владимирова Ю.С. Решение булевых уравнений. В кн.: «Методы математического моделирования» (под. ред. А.А. Самарского и В.И. Дмитриева). М.: Диалог МГУ. - 1998. - С.59-68.

9. S. Rudeanu. Boolean Function and Equations. North-Holland publishing Сотр., Amsterdam-London. 1974.-442 p.

10. S.B. Akers. On a theory of Boolean functions// J. Soc. Ind. Appl. Math. 1959. — V.7. — №4.

11. Чистов В.П. Аналитические решения логических уравнений// Техническая кибернетика. 1994. — №2. - С.219-224.

12. Пандеф Е. Булевы матрицы// Булева алгебра и конечные автоматы.1. М.:Мир.- 1969.-С. 53-61.13. http://www.mapleapps.com/List.asp?Author= 15

13. Закревский А.Д. Логические уравнения. Минск: Наука и техника.- 1975.-94 с.

14. Катериночкина Н.М., Королева З.Е., Мизатиян Х.А., Платоненко Н.М. Методы решения булевых уравнений. -М.: ВЦ АН СССР, 1988. — 21 с.16. http://www.lri.fr/~simon/satex/satex.php3.

15. Маслов С.Ю. Итеративные методы в переборной задаче как модель интуитивных// Тезисы IX Всесоюзного симпозиума по кибернетике. 1981. -С. 26-28.

16. Крейнович В.Я. Семантика итеративного метода С.Ю.Маслова// Вопросы кибернетики. Проблемы сокращения перебора. — М.: АН СССР. — 1987.-С. 30-62.

17. Опарин Г.А., Богданова В.Г. Решение больших разреженных систем булевых уравнений// Информационные технологии контроля и управления на транспорте. Иркутск: ИРИИТ. - 2001. - Вып.9. - С. 87-95.

18. Опарин Г.А., Богданова В.Г. Алгоритмы решения больших разреженных систем булевых уравнений// Методы оптимизации и их приложения (Иркутск, июнь 2001). Труды XII Байкальской межд. конф. — Иркутск. 2001.-Т. 5.-С. 114-118.

19. Опарин Г.А., Богданова В.Г. Гибридные методы возврата в решении больших разреженных систем булевых уравнений// Ляпуновские чтения & презентация информационных технологий (Иркутск, ноябрь 2001). Материалы конф. Иркутск: ИДСТУ СО РАН. - 2001. - С.23.

20. Опарин Г.А., Богданова В.Г., Новопашин А.П. Булевы модели некоторых дискретных задач// Ляпуновские чтения & Презентация информационных технологий (Иркутск, декабрь 2002). Материалы конф-Иркутск: ИДСТУ СО РАН. 2002. - С.28.

21. Опарин Г.А., Богданова В.Г., Инструментальная среда РЕБУС для решения систем булевых уравнений// Ляпуновские чтения & Презентация информационных технологий (Иркутск, декабрь 2003 г.). Материалы конф. -Иркутск: ИДСТУ СО РАН. 2003. - С. 57-58.

22. Опарин Г.А., Феоктистов А.Г., Богданова В.Г. Программа BULEQ1 для решения больших разреженных систем булевых уравнений (BULEQ1).

23. Свидетельство об официальной регистрации программы для ЭВМ № 980494. Москва: РосАПО. 1998.

24. Опарин Г.А., Феоктистов А.Г., Богданова В.Г. Программа BULEQ2 для решения больших разреженных систем булевых уравнений (BULEQ2). Свидетельство об официальной регистрации программы для ЭВМ № 990557. Москва: РОСПАТЕНТ. 1999.

25. Опарин Г.А., Богданова В.Г. Программа для решения больших разреженных систем булевых уравнений (BULEQ3). Свидетельство об официальной регистрации программы для ЭВМ №2000610609. Москва: РОСПАТЕНТ. 2000.

26. Лорьер Ж.-Л. Системы искусственного интеллекта: Пер. с франц. -М.: Мир. 1991.-568 с.

27. Zsofla Ruttkay. Constraint Satisfaction a Survey/ CWI Quarterly. -1998.- V.l. — №2-3. — P. 123-161.

28. Dechter R., Pearl J. Tree Clustering for Constraint Network// Artificial Intelligence. 1989. - Vol.38. - P. 353-366.

29. Freuder E. Synthesizing Constraint Expressions// Comm. jf the ACM, 1978. V. 21. — № 11.-P. 958-966.

30. Dechter R., Pearl J. Network-based heuristics for constraint-satisfaction problems// Artificial Intelligence. 1998. - V.34. - №1. - P. 1-38.

31. Bitner J.R., Reingold E.M. Backtrack programming techniques// Commun. ACM. 1975. - V.l8. -P.651-656.

32. Montanari U. Networks of constraints: Fundamental properties and applications to picture processing// Information Science, 1974. V.7. - №66. -P.95-132.

33. Mackworth A.K. Consistency in networks of relations// Artificial Intelligence. 1977. -V.8. -№1. - P. 99-118.

34. Freuder E. A sufficient condition of backtrack-free search// J.ACM. -1982. V. 29. - № 1. - P. 24-32.

35. Mohr R., Henderson T. Arc-consistency and path-consistency revisited// Artificial Intelligence. 1986. - № 28. - P. 225-233.

36. Deville Y., Van Hentenryck P. An Efficient Arc Consistency Algorithm for a Class of CSP Problems// Proc. IJCAI. 1991. - P. 325-330.

37. Bessiere C. Arc-consistency and arc-consistency again// Artificial Intelligence. 1994. -№ 65. - P. 179-190.

38. Bessiere C., Freuder E.C., Regin J.-C. Using inference to reduce arc consistency computation// Proc. 14th IJCAI. 1996. - V. 1. - P. 592-598.

39. Haralick R.M., Elliott G.L. Increasing tree search efficiency for constraint satisfaction problem// Artificial Intelligence. 1980. - № 14 . - P. 263313.

40. McGregor J.J. Relational consistency algorithms and their applications to picture processing// Infotrm. Sci. 1979. - V. 19. - P. 229-250.

41. Tsang E. Foundations of Constraint Satisfaction// Academic Press. -1993.

42. Dechter R., Rossi F. Constraint Satisfaction. Survey ECS. March. -2000.- 15 p.

43. Dechter R., Meiri I. Experimental evaluation of processing algorithms for constraint satisfaction problem// Artificial Intelligence. 1994. - № 68. - P. 211-241.

44. Dechter R., Pearl J. Network-based heuristics for constraint-satisfaction problems// Artificial Intelligence. 1998. - V.34. - №1. - P. 1-38.

45. Dechter R. Enhancement schemes for constraint processing: backjumping, learning, and cutset decomposition// Artificial Intelligence. 1990. — V. 41. — № 3 — P. 273-312.

46. Roberto J. Bayardo, Daniel P. Miranker. An optimal backtrack algorithm for tree-structured constraint satisfaction problems// Artificial Intelligence. — 1994. -№71.-P. 159-181.

47. Van Hentenryck P. Constraint Satisfaction in Logic Programming// Logic Progr. Series, MIT Press. Cambridge, MA. - 1989.

48. Kondrak G., Van Beek P. A theoretical evaluation of selected backtracking algorithms// Artificial Intelligence. 1997. - V.89. - №(1-2) - P. 365-387.

49. Gasching J. A general backtracking algorithm that eliminates most redundant tests// Proceedings IJCAI-77. Cambridge, MA. - 1977. - P. 457.

50. Haralick R.M., Elliott G.L. Increasing tree search efficiency for constraint satisfaction problem// Artificial Intelligence. 1980. - V. 14. - P. 263313.

51. McGregor J.J. Relational consistency algorithms and their applications to picture processing// Infotrm. Sci. 1979. -№ 19. - P. 229-250.

52. Prosser P. Hybrid algorithms for the constraints satisfaction problem// Comput. Intell. 1993. - № 9. - P. 268-299.

53. Minton S., Johnston M., Philips A., Laird P. Solving large-scale constraint satisfaction and scheduling problems using heuristic repair method// Proc. Of AAAI. 1990. - P. 17-24.

54. Selman В., Levesque H., Mitchell D. A new method for solving hard satisfiability problems// Proc. Of AAAI- 1992. - P. 440-446.

55. Eiben G., Ruttkay Zs. Constraint Satisfaction problems and evolutionary algorithms, In: T.B. Bark, D. Fogel, Z. Michalewicz (eds.)// Handbook of Evolutionary Algorithms. Oxford University Press. - 1997.

56. Tsang E., Wang C. A generic neural network approach for constraint satisfaction problems// Taylor J. (ed.). Neural Network Applications. Springer-Verlag. -1992.

57. Kask K., Dechter R. GSAT and local consistency// Proc. Of IJCAI. -1995.-P. 616-622.

58. Robinson J.A. A machine oriented logic based on the resolution principle// J. of the ACM. 1965. - V.12. - P. 25-41.

59. Данцин Е.Я. Алгоритмы задачи выполнимости// Вопросы кибернетики. Проблемы сокращения перебора. М.: АН СССР. - 1987. — С.7-30.

60. Davis М., Putnum Н. A computing procedure for quantification theory// J. of the ACM.- 1960. -P.201-215,.

61. Davis M., Logemann G., and Loveland D. A mashine program for theorem proving// Communications of the ACM. 1962 V.5. -№7 . - P. 394-397.

62. A.E. Литвиненко. Определение класса истинности логических формул методом направленного перебора. Кибернетика и системный анализ. — 2000. — № 5. — С.23-31.

63. Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем. М.: Наука, 1983. - 358 с.

64. Пападимитриу X., Стайглиц К. Комбинаторная оптимизация. Алгоритмы и сложность. М.:Мир, 1985. - 512 с.

65. Семенов А.А. Технологии решения многомерных задач логического поиска. Вестник Томского государственного университета. Приложение. 2005. -№ 14. - С. 61-73.

66. Dechter R., Meiri I. Experimental evaluation of processing algorithms for constraint satisfaction problem// Artificial Intelligence. 1994. - V.68. — P. 211-241.

67. Purdom P. Search rearrangement back tracking and polynomial average time//Artificial Intelligence. 1983.-V. 21(1-2) .-P. 117-133.

68. Purdom P.W., Robertson E.L., Brown C.A. Backtracking with multilevel dynamic search rearrangement// Artificial Intelligence — 1981. V. 15(2) . — P. 99-114.

69. J. Gashing. Performance measurement and analysis of certain search algorithms// Tech. Report CMU-CS-124, Computer Department, Carnegie Mello University, Pittsburgh, PA. 1979.

70. Nadel В. Consistent-labeling problems and their algorithms: expected-complexities and theory-based heuristics// Artificial Intelligence — 1983. —V. 21. — P. 135-178. *

71. Benhamou F., McAllester D., Van Hentenryck P. CLP (Interval) Revisited //Proc. 1994 Intern. Logic Progr. Symp. MIT Press, 1994. - P. 124-138.

72. Van Hentenryck P., Michel L., Deville Y. Numerica: a Modeling Language for Global Optimization. The MIT Press, Cambridge, Mass, 1997.88. http://www.ilog.com/product/solvers/.

73. Алефельд Г., Херцбергер Ю. Введение в интервальные вычисления.1. М.: Мир. 1987.-260 с.

74. Колмероэ А., Кануи А., ван Канегем М. Пролог теоретические основы и современное развитие // Логическое программирование. - М.: Мир.- 1988.-С. 27-133.

75. Van Hentenryck P. Constraint Satisfaction Using Constraint Logic Programming// Artifical Intelligence. 1992. - V.58. - P.l 13-159.

76. Jaffar J., Maher MJ. Constraint Logic Programming: A Survey // J.Logic Progr. 1994. -V. 19. -№20. - P. 503-581.

77. Colmerauer A. An introduction to Prolog III// Communications of the ACM.- 1990.-V. 33.-№7.

78. Benhamou F., Older W.J. Applying Interval-Arithmetic to Real, Integer and Boolean Constraint// J.Logic Progr. 1997. - V. 32. - № 1. - P. 1-24.

79. Манцивода A.B. Программирование в ограничениях на Флэнге. Системная информатика: Сб. науч. тр. Новосибирск: Наука, 1995. — Вып. 4: Методы теоретического и системного программирования. - С. 118-159.

80. Freeman-Benson B.N., Borning A. Integrating Constraints with on Object-Oriented Language// Proc. Of ECOOP'92. 1992. - P. 268-286.

81. Швецов И.Е. Основные положения технологии активных объектов. Новосибирск, 1995. - 26с. - (Препр./НФ РосНИИ ИИ).

82. Логический подход к искусственному интеллекту: от классической логики к логическому программированию: Пер. с франц./ Тейз А., Грибомон П., Луи Ж. и др. М.: Мир. - 1990. - 432 с.

83. Карпенко А.С. Логика и компьютер. Вып. 4. Многозначные логики. М.: Наука, 1997. - 233 с.

84. Опарин Г.А. Алгоритм решения больших разреженных систем булевых уравнений// Новые информационные технологии в исследовании дискретных структур. Доклады Всероссийской конференции. -Екатеринбург: Уро РАН, 1996. С.137-142.

85. A.V. Gelder. A satisfiability tester for non-clausal propositional calculus//Information and Computation. Oct. 1988. - V. 79. -№ 1. -P. 1-21.

86. J. Peysakh. A fast algorithm to convert Boolean expression into CNF// IBM Computer Science RC 12913. T.J. Watson, New York. - 1987.

87. Ines Lynce, Marques-Silva J.P. Efficient Data Structures for Backtrack Search SAT Solvers// 5th International Symposium on the Theory and Applications of Satisfiability Testing (SAT'02), May 2002.

88. Доморяд А.П. Математические игры и развлечения. М.: Физматлит. 1961. - 267 с.

89. Окунев Л.Я. Комбинаторные задачи на шахматной доске. М.: НКТП.- 1935.-87 с.

90. Гэри М., Джонсон Д. Вычислительные машины и труднорешаемые задачи. М.: Мир. - 1882.- 416 с.

91. Асанов М.О., Баранский В.А., Расин В.В. Дискретная математика: графы, матроиды, алгоритмы. Ижевск: НИЦ "Регулярная и хаотическая динамика".- 2001.- 288с.

92. Хакен А. Труднорешаемость резолюций. Кибернетический сборник. Новая серия. Сб. статей за 1988-1990 г.г. Пер. с англ. (сост. О.Б. Лупанов, Д.М. Касим-Заде). М.: Мир. - 1991. - Вып.28. - 206 с.

93. Сигал И.Х., Иванова А.П. Введение в прикладное дискретное программирование: модели и вычислительные алгоритмы. М.: ФИЗМАТЛИТ. - 2002. - 240 с.

94. Бартеньев О.В. Современный Фортран. 2-е изд., испр. - М. «Диалог-МИФИ» . - 1998. - 397 с.

95. Соммервил, Иан. Инженерия программного обеспечения, 6-е издание.: Пер. с англ. М.: Издательский дом «Вильяме» . - 2002. — 624 с.

96. Буч Г. Объектно-ориентированное проектирование с примерами применения: Пер. с англ. М.: Конкорд. - 1992. - 519 с.

97. Бадд Т. Объектно-ориентированное программирование в действии/ Пер. с англ. СПб.: Питер. - 1997.-464 с.

98. Гуссенс М., Ратц С. Путеводитель по пакету Latex и его Web-приложениям: Пер. с англ. М.: Мир. - 2001. - 604 с.

99. С.М. Львовский. Набор и верстка в пакете Latex. М.: Космоинформ. 1994. - 328 с.

100. Д. Грис. Конструирование компиляторов для цифровых вычислительных машин: Пер. с англ. — М.: Мир. — 1975. — 544 с.

101. Программные системы: Пер. с нем./ Под ред. П.Бахманна. — М.: Мир.- 1988.-288 с.

102. Евангелос Петрусос. Visual Basic 6. Руководство разработчика: в 2 т.: Пер. с англ. К.: Издательская группа BHV. - 2000. - 1072 с.

103. Дженнингс, Роджер. Руководство разработчика баз данных на Visual Basic 6.: Пер. с англ. К.; М.; СПб.: Издательский дом «Вильяме» . -2001.-976 с.

104. Клюшин Д.А. Полный курс С++. Профессиональная работа. М.: Издательский дом «Вильяме» . - 2004. - 672 с.

105. Бьярн Страуструп. Язык программирования С++. Специальное издание. Пер. с англ. М.: ООО «Бином-Пресс» . — 2005 г. - 1104 с.

106. Уильям Топп, Уильям Форд. Структуры данных в С++: Пер. с англ. М.: ЗАО «Издательство Бином» . - 1999. - 816 с.

107. Лоуренс Харрис. Программирование OLE: Пер. с англ. М.: БИНОМ.- 1995.-464 с.

108. Праг, Керри, Н., Ирвин, Майкл, P. Access 2000. Библия пользователя.: Пер. с англ. М.: Издательский дом «Вильяме». — 2001 — 1040 с.