Символьные алгоритмы и программы вычисления булевых базисов Грёбнера

• Автор: Зинин, Михаил Владимирович
• Шифр специальности: 05.13.11
• Научная степень: Кандидатская
• Год защиты: 2013
• Место защиты: Москва
• Количество страниц: 114 с. : ил.

Содержание
Введение .

Глава 1. Булевы базисы Грбнера и инволютивные базисы

1.1. Основные обозначения

1.2. Булевы функции, многочлены и кольцо.

1.3. Булевы базисы Грбнера

1.4. Булевы инволютивные базисы

Глава 2. Алгоритмы вычисления булевых базисов

2.1. Некоторые существующие алгоритмы построения базисов Грсбнера

2.1.1. Алгоритм Бухбергера

2.1.2. Инволютивный алгоритм

2.1.3. Вычисление булевых базисов в кольце В2Х
2.2. Инволютивный алгоритм на основе деления Жане.
2.2.1. Подробное описание алгоритма.
2.3. Инволютивный алгоритм на основе деления Поммаре
2.3.1. Вычисление базиса Поммаре в кольце Х.
2.3.2. Вычисление базиса Поммаре в кольце В X
2.3.3. Подробное описание алгоритма
Глава 3. Программная реализация
3.1. Реализация утилит ВЛВ и ВРВ на языке программирования
3.1.1. Преимущества и недостатки векторизации в представлении мономов
3.1.2. Представление мономов односвязным списком .
3.1.3. Представление многочленов Об
3.1.4. Выбор мономиального упорядочения.
3.2. Реализация пакета Ii в системе 2.
3.2.1. Реализация и представление данных
3.2.2. Пользовательский интерфейс.
3.2.3. Примеры использования
3.3. Реализация пакета Ii в системе
3.3.1. Реализация и представление данных
3.3.2. Пользовательский интерфейс.
3.3.3. Примеры использования
Глава 4. Результаты компьютерных экспериментов.
4.1. Выбор тестовых примеров.
4.2. Сравнение делений Жане и Поммарс
4.3. Сравнение с пакетами i и i
4.4. Система компьютерной алгебры 2, сравнение пакета Ii и встроенного пакета .
4.5. Система компьютерной алгебры , сравнение пакетов
Ii и
4.6. Выводы.
Заключение
Литература


Задача булевой выполнимости SAT (Boolean Satisfiability) — очень распространенная и, в общем случае, MV—полная [] задача, которая возникает, в частности, при проверке корректности работы оборудования и программ, в робототехнике, при создании экспертных систем и т. Для решения этой задачи разработан ряд успешных и широко применяемых специализированных алгоритмов. В настоящее время уже известен ряд примеров [] успешного применения техники булевых базисов Грёбнера к решению задачи булевой выполнимости. Через лет после теоретического обоснования [] применимости таких базисов для решения задач SAT был создан программный пакет PolyBoRi [], использующий метод базисов Грёбнера и способный конкурировать с лучшими современными программами решения задач булевой выполнимости (SAT-solvers). Приведем простой пример задачи булевой выполнимости, иллюстрирующий применение метода базисов Грёбнера для её решения, т. В терминах базисов Грёбнера данный вопрос формулируется следующим образом: состоит ли соответствующий базис Грёбнера из одного многочлена, который, в свою очередь, является единичным булевым мономом {1}) или нет? В последнем случае рассматриваемая задача является выполнимой. Вычисление базиса Грёбнера для данной системы многочленов показывает, что этот базис равен {1}, т. Ещё одним интересным применением булевых базисов Грёбнера может стать моделирование квантовых вычислений, т. Тоффоли и Адамара (они образуют универсальный базис вентилей) её цепная матрица однозначно определяется числом общих корней (когда все переменные принимают значения в ? В работе [] описан пакет для системы Ма-ЪЬета^са [], позволяющий пользователю по введенной квантовой цепи строить её цепную унитарную матрицу стандартными методами линейной алгебры, а также автоматически создавать систему определяющих её булевых многочленов. На практике, в силу ограниченности памяти компьютера, методами линейной алгебры удается промоделировать лишь - кубитиые схемы. И хотя задача построения базисов Грёбнера в булевых кольцах имеет экспоненциальную сложность [], уже сейчас эта задача решается для некоторых систем многочленов от 0 и более переменных [], что дает реальную надежду на то, что базисы Грёбнера, по крайне мере в отдельных случаях, позволят сильно продвинуться в моделировании квантовых вычислений. Стоит отметить, что случай полиномиальных систем с коэффициентами из конечного поля F2 интересен не только тем, что имеет огромное количество практических приложений, но и простотой арифметики коэффициентов. Если рассматривать многочлены с коэффициентами из конечных полей большего размера или из ноля рациональных чисел, то эффективность реализации операций с такими многочленами в значительной степени определяется эффективностью реализации операций над самими коэффициентами. Обеспечение же последней является отдельной и очень важной темой исследования []. К таковым можно отнести уже упоминавшиеся алгоритмы Ра и F5 французского математика Фожера, целый ряд модификаций алгоритма _Р5, например, алгоритмы в2У и СУДУ [] — результат работы китайских и американских исследователей, а также инволютивный алгоритм [, ] Блинкова и Гердта. Булевой версии последнего и посвящена данная работа. Цель диссертационной работы. Целью настоящей работы является разработка эффективного алгоритма построения булевых базисов Грёб-нера для идеала в булевом кольце, порождаемого заданной системой булевых многочленов, а также реализация разработанного алгоритма в виде специализированных пакетов и их встраивание в системы компьютерной алгебры с открытым кодом. Исследование современных алгоритмов построения базисов Грёбнера в полиномиальных кольцах и условий их применимости для вычисления булевых базисов Грёбнера. Разработка специализированного алгоритма, способного строить булев базис Грёбнера путем вычислений непосредственно в булевом кольце. Реализация разработанного алгоритма на языке С++ и ее оптимизация на основе эмпирических данных, полученных с помощью компьютерных экспериментов. Разработка программных пакетов, реализующих предложенный алгоритм в среде систем компьютерной алгебры с открытым исходным кодом.