WWW.DISSERS.RU

БЕСПЛАТНАЯ ЭЛЕКТРОННАЯ БИБЛИОТЕКА

загрузка...
   Добро пожаловать!

Pages:     | 1 ||

Пусть F формула в КНФ, v переменная F, набор переменным F. Наборы {v} и {¬v} мы будем записывать просто как v и ¬v. Через F [] мы обозначаем формулу, полученную из F заменой каждого выполненного набором дизъюнкта на дизъюнкт T и удалением всех вхождений литералов l, таких что ¬l, из оставшихся дизъюнктов.

Задачи выполнимости и максимальной выполнимости. Задача SAT заключается в проверке существования набора, выполняющего все дизъюнкты данной формулы F в КНФ, а задача MAX-SAT в нахождении набора, выполняющего MCl(F ) дизъюнктов. Под решением для SAT мы подразумеваем выполняющий набор, в то время как решением для MAXSAT мы называем набор, выполняющий максимальное количество дизъюнктов.

Приведем два очень простых примера. Формула F1 = (x y) (¬x) (x ¬y) содержит две переменные и три дизъюнкта и является невыполнимой. Набор {x, ¬y} выполняет MCl(F1) = 2 дизъюнкта формулы F1.

Формула же F2 = (x y) (x ¬y), очевидно, выполнима.

Анализ алгоритмов расщепления. Получив на вход некоторую формулу F, типичный алгоритм расщепления сначала некоторым образом упрощает ее, потратив на это полиномиальное от размера F время, после чего производит рекурсивные вызовы для нескольких формул вида F [1],..., F [r], где 1,..., r суть наборы значений переменным F. Таким образом, работу алгоритма расщепления можно рассматривать как дерево, вершины которого помечены формулами в КНФ. Каждой формуле F такого дерева мы приписываем неотрицательное вещественное число µ(F ), обозначающее сложность F. Стандартными мерами сложности формул являются следующие: µ(F ) = N(F ) количество переменных F ; µ(F ) = K(F ) количество дизъюнктов F ; µ(F ) = L(F ) длина (то -11есть общее количество литералов) F. Дерево является деревом расщепления, если сложность формулы каждой вершины строго больше сложности каждой из формул, которыми помечены сыновья этой вершины.

Рассмотрим вершину дерева расщепления, помеченную формулой F0. Пусть ее сыновья помечены формулами F1, F2,..., Fr. Вектор (t1, t2,..., tr) Rr называется вектором расщепления данной вершины, >если ti µ(F0) - µ(Fi) для всех i = 1,..., r. Характеристический многочлен данного вектора расщепления определяется следующим образом:

r i h(x) = 1 - x-t. Единственный положительный корень этого многоi=члена называется числом расщепления и обозначается через (t1, t2,..., tr) (несложно видеть, что при положительных x функция h(x) монотонно возрастает от - к 1). Числом расщепления дерева называется максимальное из чисел расщепления всех его вершин.

Следующая лемма доказана Кульманном и Люкхардтом.

Лемма 1. Количество листьев в дереве расщепления, корень которого помечен формулой F и число расщепления которого равно, не превосходит µ(F ).

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

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

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

Теорема 1. Существует алгоритм, решающий задачу (n, 3)-MAX-SAT за время 1.272021N в наихудшем случае.

Данное правило также используется в программе автоматического анализа алгоритмов, описанной далее.

Рассмотрим правило доминирующий единичный дизъюнкт для задачи MAX-SAT, введенное впервые Нидермайером и Росмани: если формула F содержит литерал l, такой что F содержит хотя бы столько же единичных дизъюнктов (l), сколько и дизъюнктов, содержащих литерал ¬l, то заменить F на F [l]. Корректность такой замены очевидна. Действительно, для любого полного набора переменным формулы F, содержащего литерал ¬l, набор \ {¬l} {l} выполняет хотя бы столько же дизъюнктов. Поэтому при поиске набора, выполняющего максимальное количество дизъюнктов, нет смысла рассматривать наборы, содержащие ¬l. В такой ситуации мы говорим, что {l} сильнее {¬l}. Мы обобщаем данную идею и представляем некоторое общее правило упрощения, содержащее в качестве частных случаев многие известные правила.

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

Анализ алгоритма расщепления состоит из длинного списка случаев. В каждом случае показывается, что соответствующее число расщепления не превосходит требуемой константы. Разработанная программа осуществляет такой разбор случаев автоматически. Данной программой были доказаны несколько нетривиальных оценок для задач SAT и MAX-SAT.

Некоторые из них до сих пор остаются наилучшими из известных.

-13Пятая глава посвящена идеям использования нестандартных мер сложности и запоминания дизъюнктов. С использованием данных идей доказываются две следующие теоремы.

Теорема 2. Для любой константы > 0 найдутся константы D > и c < 2, такие что MaxSatAlg(D) выдает MCl(F ) для любой формулы F с не более чем N(F ) дизъюнктами за время cN(F ).

Алгоритм 1 MaxSatAlg Вход: КНФ формула F Параметры: положительное целое число D Метод:

1. Присвоить значение True всем чистым литералам формулы F.

2. Если F содержит только дизъюнкты T, вернуть их количество.

3. Если F содержит D+-литерал a, то произвести рекурсивные вызовы для F [a] и F [¬a] и вернуть максимум из полученных ответов.

4. Пусть a произвольный литерал F. Пусть i = d(a), j = d(¬a).

5. Построить оптимальные наборы для Fa и F¬a. Обозначим их через a = {x1,..., xp} и ¬a = {y1,..., yq}, соответственно, и пусть ka = MCl(Fa) = Cl(F, a), k¬a = MCl(F¬a) = Cl(F, ¬a).

6. Если i + k¬a j + ka, то произвести рекурсивные вызовы для F [a], F [¬a, ¬y1], F [¬a, y1, ¬y2],..., F [¬a, y1,..., yq-1, ¬yq] и вернуть максимум из полученных ответов.

7. В противном случае произвести рекурсивные вызовы для F [¬a], F [a, ¬x1], F [a, x1, ¬x2],..., F [a, x1,..., xp-1, ¬xp] и вернуть максимум из полученных ответов.

Теорема 3. Существуют алгоритмы, решающие задачи MAX-2-SAT и (n, 3)-MAX-2-SAT за время 2K/6 и 2N/6.7, соответственно, в наихудшем случае.

-14Для доказательства верхних оценок на время работы алгоритма расщепления сперва фиксируется некоторая мера сложности формул, после чего показывается, что алгоритм всегда расщепляет входную формулу на несколько формул, сложности которых меньше сложности исходной формулы. Естественными мерами сложности формул являются количество переменных N, количество дизъюнктов K и длина формулы L. Известно большое количество верхних оценок относительно этих мер для задач SAT и MAX-SAT и их частных случаев. В данной работе мы используем комбинированные меры сложности для доказательства новых оценок для MAX-SAT и MAX-2-SAT. Наша мера сложности для задачи MAX-SAT выглядит следующим образом: (F ) = N(F ) + wK(F ), где w некоторая константа. Мы показываем, что для любой формулы найдется достаточно хорошее расщепление либо относительно количества переменных, либо относительно количества дизъюнктов. После этого мы подбираем константу w, зависящую от плотности формулы, так, чтобы соответствующая оценка была меньше 2N.

Идея запоминания дизъюнктов используется во многих современных SAT-солверах. Программа запоминает найденные частичные наборы, делающие формулу невыполнимой. Например, набор {x, ¬y} делает невыполнимой формулу (¬y z) (z ¬x) (x) (¬z y). Для того, чтобы учесть этот факт, программа добавляет к рассматриваемой формуле дизъюнкт (¬x y). Сама по себе идея довольно естественна и не является новой: она используется, например, в теоретических алгоритмах, практических программах и даже в системах доказательств. Мы приводим обобщение этой простой идеи для задачи MAX-SAT.

Список литературы [1] Куликов А. С. Верхняя оценка O(20.16254n) для точной 3-выполнимости:

более простое доказательство // Записки научных семинаров ПОМИ.

2002. Т. 293. С. 118–128.

[2] Куликов А. С., Куцков К. Новые верхние оценки для задачи максимальной выполнимости // Дискретная математика. 2009. Т. 21, № 1.

С. 139–157.

[3] Куликов А. С., Федин С. С. Решение задачи о максимальном разрезе за время 2|E|/4 // Записки научных семинаров ПОМИ. 2002. Т. 293.

С. 129–138.

[4] Куликов А. С., Федин С. С. Автоматические доказательства верхних оценок на время работы алгоритмов расщепления // Записки научных семинаров ПОМИ. 2004. Т. 316. С. 111–128.

[5] Kojevnikov A., Kulikov A. S. A New Approach to Proving Upper Bounds for MAX-2-SAT // Proceedings of the Seventeenth Annual ACM-SIAM Symposium on Discrete Algorithms. 2006. P. 11–17.

[6] Kulikov A. S. Automated Generation of Simplification Rules for SAT and MAXSAT // Proceedings of the Eighth International Conference on Theory and Applications of Satisfiability Testing. Vol. 3569 of Lecture Notes in Computer Science. 2005. P. 430–436.

[7] Kulikov A. S., Kutzkov K. New Bounds for MAX-SAT by Clause Learning // Proceedings of the 2nd International Computer Science Symposium in Russia. Vol. 4649 of Lecture Notes in Computer Science. 2007. P. 194– 204.

Pages:     | 1 ||






© 2011 www.dissers.ru - «Бесплатная электронная библиотека»