Задача выполнимости булевых формул (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.
В процессе работы была построена программа, позволяющая автоматически генерировать экспоненциальные алгоритмы для задачи MaxSAT. Как и в работе [12], на вход даётся формула с желаемой константой ветвления и строится дерево доказательство похожей структуры. Отличия нашей программы:
• модель описания формул предполагает наличие необлитированных переменных: если покрытие означивает литералы, соседствующие с какой-то переменной, то для получения хорошего вектора ветвления зачастую неважно, облитерована она или нет. При этом наличие возможности не облитеровывать переменных существенно уменьшает размеры получаемых деревьев доказательств;
• правила упрощения также построены на основе анализа таблицы выигрышей, но упрощаемые формулы подбираются не за счёт подстановок в литералы значений (e.g. x =1) или других литералов (e.g. x = y), а за счёт перебора возможных формул, имеющих те же мажорирующие выигрыши. Это позволяет чаще находить упрощения, что также сказывается на размере доказательств.
На основе подхода была построена программа, генерирующая точный алгоритм для задачи (п, 3) — MaxSAT, параметризированной относительно количества переменных, со временем работы O*(1.175n), что является улучшением алгоритма, предложенного в [5], со временем работы O*(1.191n).
Также был исследован подход, позволяющий проверять корректность правил ветвления с помощью SMT-солверов, что может быть полезно не только для автоматических доказательств.
