📄Работа №141619
Тема: Алгоритмы для частных случаев задачи максимальной выполнимости
Тип работы
Магистерская диссертация
Предмет
Школьная математика
Объем:
30 листов
Год:
2022
Просмотров:
87
4650
руб.
🛒 Купить работу
Не подходит эта работа?
Закажите новую по вашим требованиям
Узнать цену на написание
Закажите новую по вашим требованиям
Представленный материал является образцом учебного исследования, примером структуры и содержания учебного исследования по заявленной теме. Размещён исключительно в информационных и ознакомительных целях.
Workspay.ru оказывает информационные услуги по сбору, обработке и структурированию материалов в соответствии с требованиями заказчика.
Размещение материала не означает публикацию произведения впервые и не предполагает передачу исключительных авторских прав третьим лицам.
Материал не предназначен для дословной сдачи в образовательные организации и требует самостоятельной переработки с соблюдением законодательства Российской Федерации об авторском праве и принципов академической добросовестности.
Авторские права на исходные материалы принадлежат их законным правообладателям. В случае возникновения вопросов, связанных с размещённым материалом, просим направить обращение через форму обратной связи.
Настоящий учебно-методический информационный материал размещён в ознакомительных и исследовательских целях и представляет собой пример учебного исследования. Не является готовым научным трудом и требует самостоятельной переработки.
📋 Содержание
1 Введение 2
2 Предварительные сведения 4
3 Алгоритм 6
4 Автоматически доказанные верхние оценки 22
5 Дальнейшие направления 24
6 Заключение 26
2 Предварительные сведения 4
3 Алгоритм 6
4 Автоматически доказанные верхние оценки 22
5 Дальнейшие направления 24
6 Заключение 26
📖 Введение
Задача выполнимости булевых формул (SAT) - одна из самых известных NP-трудных задач. В задаче требуется определить, существуют ли такие значения переменных, при которых эта формула выполняется. Её обобщение, задача максимальной выполнимости (MaxSAT), в которой требуется максимизировать количество выполненных клозов, также известна и поиск эффективных алгоритмов для неё и связанных с ней подзадач представляет большой интерес, как в теории, так и на практике ([1], [2], [3]).
Это одна из первых задач, для которой была показана NP-трудность. Помимо прочего исследовались подходы к
• различным подвидам MaxSAT ([4], [5])
• построению вероятностных и приближённых алгоритмов ([6], [7]),
• построению алгоритмов, использующих эвристики ([1]),
• построению точных алгоритмов ([8], [9], [10]), а также
• автоматическому построению доказательств верхних оценок на время работы точных алгоритмов ([11], [12], [13]).
Нас интересует последнее, а именно автоматическое построение точных алгоритмов. Типичный точный алгоритм, принимая на вход формулу F, на каждом шаге, покуда возможно, упрощает формулу правилами упрощения, а потом применяет правило расщепления: делает два рекурсивных вызова на подформулах полученных из F присваиваниями l = true и l = false, где l - переменная формулы F. После чего алгоритм возвращает ответ, исходя из ответов на подформулах. В общем случае в расщеплении может рассматриваться большее количество подформул и присваиваний.
Автоматическое построение точного алгоритма подразумевает построение
• алгоритма упрощения формулы;
• алгоритма поиска наилучшего расщепления;
• уточнения вида формулы (если не нашлось подходящих упрощений и расщеплений).
В последних двух работах именно такой метод автоматического построения алгоритмов и рассматривается:
• в работе [12] описывается программа, которая на основе заданного списка правил упрощения и ветвления строит для заданной формулы и константы расщепления точный алгоритм;
• в работе [13] исследуется подход к автоматической генерации правил упрощения.
На основе этих работ были получены новые оценки для SAT и MaxSAT.
Это одна из первых задач, для которой была показана NP-трудность. Помимо прочего исследовались подходы к
• различным подвидам MaxSAT ([4], [5])
• построению вероятностных и приближённых алгоритмов ([6], [7]),
• построению алгоритмов, использующих эвристики ([1]),
• построению точных алгоритмов ([8], [9], [10]), а также
• автоматическому построению доказательств верхних оценок на время работы точных алгоритмов ([11], [12], [13]).
Нас интересует последнее, а именно автоматическое построение точных алгоритмов. Типичный точный алгоритм, принимая на вход формулу F, на каждом шаге, покуда возможно, упрощает формулу правилами упрощения, а потом применяет правило расщепления: делает два рекурсивных вызова на подформулах полученных из F присваиваниями l = true и l = false, где l - переменная формулы F. После чего алгоритм возвращает ответ, исходя из ответов на подформулах. В общем случае в расщеплении может рассматриваться большее количество подформул и присваиваний.
Автоматическое построение точного алгоритма подразумевает построение
• алгоритма упрощения формулы;
• алгоритма поиска наилучшего расщепления;
• уточнения вида формулы (если не нашлось подходящих упрощений и расщеплений).
В последних двух работах именно такой метод автоматического построения алгоритмов и рассматривается:
• в работе [12] описывается программа, которая на основе заданного списка правил упрощения и ветвления строит для заданной формулы и константы расщепления точный алгоритм;
• в работе [13] исследуется подход к автоматической генерации правил упрощения.
На основе этих работ были получены новые оценки для SAT и MaxSAT.
✅ Заключение
В процессе работы была построена программа, позволяющая автоматически генерировать экспоненциальные алгоритмы для задачи MaxSAT. Как и в работе [12], на вход даётся формула с желаемой константой ветвления и строится дерево доказательство похожей структуры. Отличия нашей программы:
• модель описания формул предполагает наличие необлитированных переменных: если покрытие означивает литералы, соседствующие с какой-то переменной, то для получения хорошего вектора ветвления зачастую неважно, облитерована она или нет. При этом наличие возможности не облитеровывать переменных существенно уменьшает размеры получаемых деревьев доказательств;
• правила упрощения также построены на основе анализа таблицы выигрышей, но упрощаемые формулы подбираются не за счёт подстановок в литералы значений (e.g. x =1) или других литералов (e.g. x = y), а за счёт перебора возможных формул, имеющих те же мажорирующие выигрыши. Это позволяет чаще находить упрощения, что также сказывается на размере доказательств.
На основе подхода была построена программа, генерирующая точный алгоритм для задачи (п, 3) — MaxSAT, параметризированной относительно количества переменных, со временем работы O*(1.175n), что является улучшением алгоритма, предложенного в [5], со временем работы O*(1.191n).
Также был исследован подход, позволяющий проверять корректность правил ветвления с помощью SMT-солверов, что может быть полезно не только для автоматических доказательств.
• модель описания формул предполагает наличие необлитированных переменных: если покрытие означивает литералы, соседствующие с какой-то переменной, то для получения хорошего вектора ветвления зачастую неважно, облитерована она или нет. При этом наличие возможности не облитеровывать переменных существенно уменьшает размеры получаемых деревьев доказательств;
• правила упрощения также построены на основе анализа таблицы выигрышей, но упрощаемые формулы подбираются не за счёт подстановок в литералы значений (e.g. x =1) или других литералов (e.g. x = y), а за счёт перебора возможных формул, имеющих те же мажорирующие выигрыши. Это позволяет чаще находить упрощения, что также сказывается на размере доказательств.
На основе подхода была построена программа, генерирующая точный алгоритм для задачи (п, 3) — MaxSAT, параметризированной относительно количества переменных, со временем работы O*(1.175n), что является улучшением алгоритма, предложенного в [5], со временем работы O*(1.191n).
Также был исследован подход, позволяющий проверять корректность правил ветвления с помощью SMT-солверов, что может быть полезно не только для автоматических доказательств.
ИЛИ
Поиск аналога
📕 Список литературы
🖼 Скриншоты
🛒 Оформить заказ
⚡ Работу высылаем в течении 5 минут после оплаты.