Построение алгоритмов для задач булевой логики при помощи автоматизации, комбинированных мер сложности и запоминания дизъюнктов

• Автор: Куликов, Александр Сергеевич
• Шифр специальности: 05.13.17
• Научная степень: Кандидатская
• Год защиты: 2009
• Место защиты: Санкт-Петербург
• Количество страниц: 94 с.

Введение

1 Определения

1.1 Задачи булевой логики

1.1.1 Формулы в КНФ.

1Л.2 Задачи выполнимости и максимальной выполнимости

1.2 Алгоритм расщепления.

1.3 Анализ алгоритмов расщепления

1.4 Класс формул.

2 Методы доказательства верхних оценок,

использующиеся в работе

2.1 Пример простого алгоритма расщепления

2.2 Общее правило упрощения
2.3 Автоматический аначиз сложности алгоритмов расщепления
2.4 Комбинированные меры сложности
2.5 Запоминание дизъюнктов.
3 Автоматическое порождение правил упрощения
3.1 Известные правила упрощения для и X .
3.2 Общее правило упрощения.
3.3 Алгоритм для п, 3МАХ8АТ.
4 Автоматический анализ времени работы
4.1 Описание программы .
4.1.1 Входные и выходиые данн ые
4.1.2 Алгоритм построения доказательства
4.1.3 Детали реализации.
4.1.4 Правила упрощения.
4.1.5 Правило расщепления.
4.1.6 Мера сложности
4.1.7 Инвариант.
4.2 Автоматически доказанные верхние оценки.
4.3 Подобные работы.
5 Комбинированные меры сложности и запоминание дизъюнктов
5.1 Решение МАХЭЛТ на формулах константной плотности
быстрее, чем за 2ДГ.
5.2 Алгоритм для МАХАТ
5.2.1 Правила упрощения.
5.2.2 Правила расщепления.
5.2.3 Алгоритм для МАХАТ
5.2.4 п, 3М АХАТ.
Введение


Общее правило упрощения. Алгоритм для п, 3МАХ8АТ. Описание программы . Детали реализации. Правила упрощения. Правило расщепления. Инвариант. Автоматически доказанные верхние оценки. Подобные работы. ДГ. Правила упрощения. Правила расщепления. М АХАТ. Интерес к доказательству экспоненциальных верхних оценок для КРтрудных задач в последние несколько десятилетий остается на стабильно высоком уровне. Одним из наиболее хорошо изученных подходов к доказательству таких оценок является метод расщепления. Впервые данный метод был предложен в м году Дэвисом и Патнемом и сформулирован в более современном виде Дэвисом, Лоджеманном и Лавлэндом в м году. Его основная идея заключается в расщеплении входного примера задачи на несколько более простых примеров упрощаемых в дальнейшем некоторыми правилами упрощения, таких что, построив решение для каждого из них, возможно за полиномиальное время построить решение для исходного примера. Зраскрашиваемости графа, где п количество вершин входного графа . В диссертации рассматриваются алгоритмы расщепления в применении к задачам выполнимости и максимальной выполнимости. Обе задачи формулируются ка языке булевых формул, являющемся очень удобным для кодирования многих алгоритмических задач таких, например, как автоматическое доказательство теорем, составление расписаний, оптимизационные задачи на графах. Задача пропозициональной выполнимости iiii , является одной из наиболее известных полных задач см. Данной задаче посвящена международная ежегодная конференция Ii ii iiii i, проводящаяся уже более десяти лет, а также научный журнал iiii, i i. Поскольку трудные задачи часто возникают в практических приложениях например, при разработке микросхем, в распознавании образов, важное место в исследовании задачи выполнимости занимает разработка программ, решающих такие программы называются солверами. Ежегодно проводятся соревнования таких программ. Современные солверы способны быстро решать многие задачи, считавшиеся нерешаемыми несколько лет назад. Важным оптимизационным обобщением задачи выполнимости является задача максимальной выполнимости xi iiii , X. В терминах задачи X могут быть естественным образом переформулированы многие оптимизационные трудные задачи, к примеру, такие оптимизационные задачи на графах, как задача о максимальном разрезе xi , X, задача о минимальном вершинном покрытии i vx v , задача о максимальном независимом множестве xi i . Задача X возникает также в задачах искусственного интеллекта и комбинаторной оптимизации , . В статье Кресеизи и Канна перечислены самых популярных задач комбинаторной оптимизации, в число которых входит и задача X. Для задачи X существуют приближенные алгоритмы, находящие за полиномиальное время решение с некоторой гарантированной точностью. Например, алгоритм Асано и др. В то же время известно, что в предположении не существует полиномиального по времени алгоритма, находящего приближенное решение, сколь угодно близкое к оптимальному. Алгоритм Данцина и др. Известно также много алгоритмов, решающих практические примеры задачи максимальной выполнимости см. Для данных алгоритмов,
однако, неизвестно никаких оценок кроме тривиальных на время работы в наихудшем случае. X2 вариант задачи X, где каждый дизъюнкт входной формулы содержит не более двух литералов и каждая переменная входит не более, чем в три дизъюнкта. Известно, что все перечисленные выше задачи являются трудными доказательство трудности задачи тг, 3X2 см. Таким образом, в предположении не существует полиномиальных по времени алгоритмов для данных задач. Тем не менее, поскольку подобные задачи часто возникают в практических приложениях, важно понять, какое время требуется для их решения, даже если это время экспоненциально. Как сказано выше, лучшие известные оценки для многих трудных задач получены именно методом расщепления. Простейший алгоритм расщепления для задачи выполнимости на формуле с переменными имеет время работы порядка 2iV. Первые улучшения данной оценки были получены в начале х годов Мониеном и Шпекен.