Теоретические оценки времени работы алгоритмов для задачи выполнимости булевых формул тема диссертации и автореферата по ВАК РФ 05.13.17, кандидат физико-математических наук Гирш, Эдуард Алексеевич

• Гирш, Эдуард Алексеевич
• кандидат физико-математических наук
• 1998

Оглавление диссертации кандидат физико-математических наук Гирш, Эдуард Алексеевич

Оглавление

Введение

Метод расщеплений

Метод поиска локального максимума

Структура диссертации

1 Основные понятия

1.1 Формулы и наборы

1.2 Классы формул в КНФ

1.3 Вычислительные задачи

1.4 Модели вычислений

2 Общая схема алгоритма расщепления для ВЫП

2.1 Дерево расщепления

2.2 Оценка количества вершин в дереве расщепления

2.3 Описание общей схемы

2.4 Правила преобразования, сохраняющие выполнимость

3 Алгоритм расщепления для произвольных формул в КНФ

3.1 Правило черных и белых литералов

3.2 Верхняя оценка относительно количества дизъюнкций

3.3 Верхняя оценка относительно длины формулы

4 Алгоритм расщепления для формул в КНФ-(1,оо)

4.1 Дополнительные правила преобразования

4.2 Процедура Reduce для формул в КНФ-(1,сю)

4.3 Верхняя оценка относительно количества дизъюнкций

4.4 Верхняя оценка относительно длины формулы

4.5 Верхняя оценка относительно количества переменных

5 Алгоритм расщепления для формул в к-КНФ, имеющих много выполняющих наборов

5.1 Описание алгоритма

5.2 Формулировки основных результатов

5.3 Анализ алгоритма

5.4 Формулы в КНФ без "коротких" выполняющих наборов

6 Алгоритмы расщепления для задачи максимальной выполнимости

6.1 Общая схема алгоритма для МАКС-ВЫП, основанного на методе расщеплений

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

6.3 Верхние оценки для МАКС-ВЫП и МАКС-2-ВЫП

6.4 Верхняя оценка для МАКС-З-ВЫП

7 Алгоритмы поиска локального максимума

7.1 Верхняя оценка

7.2 Нижняя оценка

Литература

150

Введение диссертации (часть автореферата) на тему «Теоретические оценки времени работы алгоритмов для задачи выполнимости булевых формул»

Введение

Язык булевых формул является удобным языком для кодирования многих важных алгоритмических задач, например, встречающихся в теории расписаний, верификации программ, потоковых задач. Любая задача, решаемая на недетерминированной машине Тьюринга за полиномиальное время, сводится к задаче выполнимости булевых формул (см., например, [1, 30]). Задача о выполнимости булевой формулы остается КР-полной, даже если рассматривать формулы в конъюнктивной нормальной форме (КНФ), состоящие из дизъюнкций, длины которых не превосходят трех; можно также считать, что каждая переменная входит в формулу не более трех раз. Все известные алгоритмы для задачи о выполнимости формулы в КНФ и ее подзадач с указанными ограничениями имеют экспоненциальные верхние оценки времени исполнения "в наихудшем случае", причем все эта оценки имеют вид с", где с — некоторая константа, а п — либо длина формулы, либо количество дизъюнкций, либо количество входящих в формулу переменных.

Чаще всего задача выполнимости формулы в КНФ (ВЫЛ) определяется как задача распознавания: требуется выяснить, существует ли набор истинностных значений переменных, при котором формула становится истинной (выполняющий набор). В качестве результата выдается один из двух ответов: "Выполнима" или "Невыполнима". Поскольку все рассматриваемые в данной диссертации алгоритмы для задачи ВЫП находят выполняющий набор, будем рассматривать ВЫП как задачу поиска: алгоритм, решающий ее, выдает для выполнимой формулы выполняющий набор, а для невыполнимой — ответ "Невыполнима" . С задачей выполнимости также тесно связана задача максимальной выполнимости формулы в КНФ (МАКС-ВЫП), в которой

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

Исследования по алгоритмам для задачи выполнимости булевых формул велись по следующим основных направлениям:

— поиск классов формул, для которых задача выполнимости разрешима за полиномиальное время (см., например, обзор в [4]);

— понижение основания экспоненты в верхних оценках для ВЫП и ее NP-полных подзадач [27, 28, 2, 3, 29, 40, 32, 23, 24];

— оценка сложности доказательств невыполнимости в различных системах доказательств [39];

— создание приближенных алгоритмов для МАКС-ВЫП [41, 18, 14, 26, 38, 7, 21],

— компьютерные эксперименты, проясняющие эффективность алгоритмов для ВЫП и МАКС-ВЫП на определенных классах формул, там, где не доказаны хорошие верхние оценки [11, 37, 16].

Экспериментальные исследования наиболее широко проводились для алгоритмов, основанных на методе поиска локального максимума и методе расщеплений. Большая часть "экспоненциальных" алгоритмов для ВЫП и ее подзадач также основана на методе расщеплений. Два этих основных метода будут рассмотрены ниже подробнее.

В приближенных алгоритмах, предлагавшихся для МАКС-ВЫП, используются совершенно иные методы, чем в (точных) алгоритмах для ВЫП. Эти алгоритмы преобразуют МАКС-ВЫП в задачу полуопределенного программирования и находят за полиномиальное время приближенное решение. В общем случае полученный набор значений переменных выполняет долю 0.770 от максимального числа выполненных дизъюнкций [7]. Для формул в &-КНФ при к = 2,3 существуют более точные алгоритмы (формула находится в &-КНФ, если каждая ее дизъюнкция содержит не более к литералов). Алгоритм для фор-

мул в 3-КНФ [21] выполняет долю 7/8, алгоритм для формул в 2-КНФ [14] выполняет долю 0.931. Все указанные алгоритмы являются вероятностными, некоторые из них могут быть дерандомизированы (т.е. в них можно избавиться от случайного выбора). С другой стороны, исследования, касающиеся вероятностно проверяемых доказательств (см., например, [6]), привели к тому, что была показана невозможность при условии Р ф NP построения полиномиального по времени алгоритма, находящего приближение с долей, большей некоторой константы. Для формул, состоящих из дизъюнкций, содержащих не более, чем по два литерала, эта константа составляет 0.955 [20]. Если же разрешены дизъюнкции хотя бы из трех литералов, константа равна 7/8. Таким образом, в предположении Р ф NP, невозможно построение полиномиального алгоритма, который давал бы ответ со степенью приближения лишь на произвольное е большей, чем алгоритм X. Карлоффа и У. Цвика. Алгоритмы, дающие ответ с такой степенью приближения и имеющие экспоненциальную сложность, меньшую, чем сложность алгоритма, находящего точное решение, неизвестны.

Из алгоритмов для ВЫП, не использующих ни метод расщепления, ни метод поиска локального максимума, стоит отметить новый результат Р. Патури, П.Пудлака и Ф. Зейна [31]: доказано, что выполнимость формулы в &-КНФ можно выяснить вероятностным алгоритмом за время, не превосходящее p(L)2(l~l/k)N, а детерминированным алгоритмом — за время, приближающееся к p(L)с ростом к (здесь и далее р — некоторый полином, L — длина входной формулы, К — количество дизъюнкций в ней, N — количество переменных). Эти алгоритмы дают наилучшие известные на данный момент оценки относительно количества переменных: вероятностный — для к > 4, а детерминированный — для к > 5.

Решение алгоритмических задач тесно связано с системами до-

казательств. Из существования системы доказательств, в которой имелись бы полиномиальные доказательства невыполнимости булевых формул, следовало бы NP = coNP [39]. Экспоненциальная нижняя оценка на длину таких доказательств была впервые доказана Г. С. Цейтиным [5] для регулярных резолюций. Впоследствии эта оценка неоднократно улучшалась и была обобщена на случай обычных резолюций. Этот результат представляется особенно важным, поскольку метод расщепления тесно связан с резолюционными доказательствами [10]. Позднее были доказаны экспоненциальные нижние оценки для некоторых других систем, например, резолюций и систем Фреге ограниченной глубины. Обзор таких результатов имеется в [39].

Метод расщеплений

Наиболее широко в литературе по задаче выполнимости булевых формул представлены алгоритмы, основанные на методе расщеплений, восходящем к [13] и [12]. Этот метод состоит в том, что задача выполнимости для исходной формулы сводится к задаче выполнимости для нескольких более простых формул; в простейшем случае задача выполнимости для формулы F сводится к задаче выполнимости для формул F[x] и F[x] для некоторой переменной х (для литерала /, формула F[l] получается из формулы F удалением всех дизъюнкций, в которые входит литерал Z, и удалением его отрицания из всех остальных дизъюнкций). Каждая из полученных формул подвергается некоторым не изменяющим ее выполнимости преобразованиям, производимым за полиномиальное время, таким как удаление 1-дизъюнкций (дизъюнкций, содержащих ровно по одному литералу) и чистых литералов (литерал является чистым, если его отрицание не входит в формулу). Таким образом, алгоритм строит некоторое дерево расщепления, каждый лист которого помечен либо пустой (т.е. тождественно истинной) формулой,

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

Алгоритмы из [13] и [12] имеют сложность р{Ь)2м. В начале 80х годов было замечено [27, 2, 3, 29], что выполнимость формул в /г-КНФ можно выяснить быстрее, если переменные для расщепления выбирать из самых коротких дизъюнкций. Таким образом, задача выполнимости для формулы в &-КНФ с N переменными сводится к задаче выполнимости для формул с N — 1, N — 2, ..., N — к + 2 и N — к переменными. Решение соответствующего рекуррентного уравнения дает оценку1 р(Ь)ф{к)н на время работы алгоритма, где ф(к) — единственный положительный корень полинома хк — хк~1 — ... — 1. Впоследствии для формул в 3-КНФ были созданы алгоритмы, работающие время р(Ь)1.579ж [32], р(£)1.571^ [42], р(1,)1.5045* [23]. И.Шиермейер анонсировал оценку р(Ь) 1.497^ [33], но полное доказательство пока не опубликовано. Имеются и работы по понижению экспоненциальных верхних оценок для других КР-полных задач, в частности, для задачи 3-раскрашиваемости графа [8].

В начале 80х годов появились также алгоритмы, для которых приводились верхние оценки относительно количества дизъюнкций в исходной формуле и ее длины. Это алгоритм Б. Мониена и Э. Шпекенмей-ера [28], затрачивающий время р(Ь) 1.2600х, и алгоритм X. Люкхардта [25], затрачивающий время Впоследствии эти алгоритмы

были улучшены О. Кулльманном и X. Люкхардтом [24]: первый алгоритм был значительно упрощен, а вторая оценка была снижена до р(Ь)1.08011. Основная

идея этих алгоритмов — использование расширенного принципа знака. Пусть Р — некоторое свойство, которым может обладать пара из литерала и формулы в КНФ, такое что Р(1, Г)

*В указанных статьях доказывается лучшая оценка, см. табл. I.

выполняется хотя бы для одного из литералов I = V или I = V для каждой переменной г>, встречающейся в формуле Р. Например, Р(1, Р) может означать "литерал I входит в формулу Р не более одного раза".

Расширенный принцип знака. Если в формулу Р не входит ни одной дизъюнкции, состоящей только из литералов, для которых выполняется свойство Р (относительно формулы Р), то формула Р выполнима.

Наиболее простой пример применения этого принципа продемонстрировал X. Люкхардт в [25]. Он рассматривал формулы в КНФ-(1,оо): формула принадлежит этому классу, если для каждой пары противоположных литералов по крайней мере один из них входит в формулу не более одного раза1. В этом случае, если положить Р(/,Р) ="литерал I входит в формулу Р не более одного раза", то расширенный принцип знака позволяет найти в формуле дизъюнкцию {/ь/г, • • ■ состоящую только из литералов, которые не входят более ни в какие дизъюнкции. Задача выполнимости исходной формулы Р таким образом сводится к задаче выполнимости формул з], ь^Дз] и \J21h] (пусть, для простоты, к = 3). В самом деле, не умаляя общности, можно считать, что ровно один из литералов ¿ь/г^з является истинным в выполняющем наборе: в формуле Р[1\] литералы /2 и /3 становятся чистыми и могут быть легко удалены, и т.д. В итоге получается, что задача выполнимости формулы с N переменными сводится к задаче выполнимости к формул с N — к переменными, т.е. время работы этого алгоритма не превосходит

8пр(к1/к)мр{ь) = г^рЩ. к> 1

В статье [24] расширенный принцип знака используется для по-

*В настоящей диссертации используется другое определение: см. раздел 1.2 и сноску на стр. 78.

строения алгоритмов для произвольных формул в КНФ; полученные алгоритмы имеют хорошие оценки на время исполнения относительно длины формулы и количества дизъюнкций в ней. Поясним метод, с помощью которого получена вторая оценка, поскольку сходная техника используется и в данной диссертации. Эта оценка составляет р(Ь)2к/3 « р(Ь) 1.2600х. В качестве преобразований, упрощающих формулу, выбираем удаление 1-дизъюнкций и замену на резольвенты: для некоторой переменной добавляем в формулу все резольвенты по этой переменной и удаляем из формулы дизъюнкции, в которые эта переменная входила. Такое преобразование применяем только в случае, если оно не увеличивает количества дизъюнкций в формуле, в частности, если переменная входит ровно два раза положительно и ровно два раза отрицательно или входит не более одного раза положительно (или отрицательно). Каждая из переменных, остающихся в формуле после этих преобразований, входит в формулу по крайней мере пять раз, причем не менее двух раз положительно и не менее двух раз отрицательно. Если для расщепления каждый раз выбирать переменную, входящую в формулу по крайней мере три раза положительно и по крайней мере три раза отрицательно, каждая из полученных формул будет иметь по крайней мере на три дизъюнкции меньше; соответствующее рекуррентное уравнение имеет решение 21/3, т.е. как раз то, что фигурирует в искомой оценке. В результате остается разобрать случай, когда формула содержит только переменные, входящие ровно два раза положительно и по крайней мере три раза отрицательно (или наоборот). В этом случае расширенный принцип знака гарантирует наличие дизъюнкции, состоящей исключительно из литералов, входящих в формулу ровно два раза. Расщепление по одному из них оказывается также выгодным: если мы полагаем его значение истинным, оставшиеся литералы будут удалены при замене на резольвенты (они теперь встречаются только

один раз в формуле). Можно показать, что корень соответствующего рекуррентного уравнения будет также 21/3.

Последние известные оценки для метода расщеплений на момент написания данной диссертации указаны в табл. I. Все они, кроме результата для формул в &-КНФ, являются наилучшими из известных верхних оценок не только для метода расщеплений, но и для других алгоритмов для задачи выполнимости. Экспериментальные данные указывают на возможность дальнейшего улучшения этих оценок, например, Дж. М. Кроуфорд и Л. Д. Аутон [11] утверждают, что время работы их алгоритма растет приблизительно как 2м!11. Алгоритмы, решающие МАКС-ВЫП при помощи метода расщеплений, также изучались экспериментально: Б. Борчерс и Дж. Фурман [9] показали, что комбинация метода расщеплений с эвристикой поиска локального максимума оказывается довольно эффективной для случайно порожденных формул в 2-КНФ и 3-КНФ.

В данной диссертации предлагается ряд новых алгоритмов для ВЫП, использующих метод расщеплений, и доказываются верхние оценки на время их исполнения "в наихудшем случае". Оценки для задачи выполнимости формулы в КНФ без ограничений оказываются лучше известных ранее, оценки для других классов формул улучшаются за счет сужения этих классов.

В главе 5 показано, что с помощью алгоритма, использующего метод расщеплений, можно за линейное время найти выполняющий набор для формулы в &-КНФ, имеющей много выполняющих наборов (доля выполняющих наборов среди всех наборов — не меньше некоторой константы). Выполняющий набор для такой формулы может быть легко найден с помощью простого вероятностного алгоритма, который вы-

количество дизъюнкций К длина формулы Ь количество переменных ЛГ

КНФ 1.2600^ [28] 1.08011, [24]

к-ШФ ф(к - 1)* [27, 3]

3-КНФ 1.5045^ [23]

КНФ-(1,оо) 1.4423* [25]

КНФ-(1,2) 1.0416х' [24] 1.1299* [24]

3-КНФ-(1,2) 1.1299Л [24]

Таблица I: Наилучшие известные верхние оценки для алгоритмов для задачи ВЫП, использующих метод расщепления (исключая оценки, полученные в данной диссертации). Оценки приведены с точностью до полиномиального сомножителя р(Ь). Величина ф(к) — единственный положительный корень многочлена хк — хк~1 — ... — 1.

бирает значения переменных случайным образом2 и проверяет истинность формулы при этих значениях (эта операция повторяется несколько раз). В данной диссертации строится детерминированный алгоритм для этой задачи. Выполняющий набор, который находит этот алгоритм, оказывается "коротким", т.е. количество литералов, содержащихся в нем, ограничено константой. Алгоритм работает полиномиальное время и в случае, когда формула имеет долю ^у выполняющих наборов. Несмотря на кажущуюся естественность наличия "короткого" выполняющего набора, оказывается, что существуют формулы в КНФ без ограничения на длины дизъюнкций, имеющие много выполняющих наборов, но не имеющие при этом "коротких" выполняющих наборов.

В главе 3 на основе алгоритмов из [24] с оценками р(Ь) 1.2600х и р(£)1.0801ь строятся новые алгоритмы, имеющие лучшие оценки. Основой для этого улучшения является замена расширенного принципа знака на более общее правило черных и белых литералов (раздел 3.1). Это правило является развитием принципа автаркности (см., например, [29]): если присваивание значения некоторым переменным не приводит к появлению новых дизъюнкций, то оно не изменяет выполнимости формулы. Использование этого правила приводит к алгоритмам для ВЫП, работающим время р(Ь) 1.2389х и р(Ь)1.0758ь. Неформально говоря, правило черных и белых литералов состоит в следующем. Пусть некоторые литералы, встречающиеся в формуле окрашены в черный цвет, их отрицания окрашены в белый цвет.

Правило черных и белых литералов. Для любой раскраски существует только две возможности:

— формула .Р содержит дизъюнкцию, содержащую черный ли-

2Всякий раз, когда будем говорить "выбирает случайно", будем иметь в виду "в соответствии с равномерным распределением".

терал и не содержащую белых литералов;

— удаление всех дизъюнкций, содержащих окрашенные литералы, не изменяет выполнимости формулы Р.

Основная идея улучшения алгоритма для ВЫП, имеющего хорошую оценку относительно количества дизъюнкций, состоит в следующем. Если в формуле есть литерал, входящий по крайней мере четыре раза, такой что его отрицание входит по крайней мере три раза, то расщепление относительно такого литерала приводит к рекуррентному уравнению с корнем, не превосходящим 1.2208. Если такого литерала нет, покрасим литералы, входящие в формулу Р ровно два раза, в черный цвет. Правило черных и белых литералов гарантирует наличие в формуле Р дизъюнкции, в которую входят черный и неокрашенный литералы (в этом случае произведем расщепление по неокрашенному литералу и удалим черный литерал с помощью резолюции), либо дизъюнкции, состоящей только из черных литералов. Можно показать, что в обоих случаях корень рекуррентного уравнения будет тот же самый. Если указанных дизъюнкций нет в формуле, значит, из нее можно удалить все дизъюнкции, кроме тех, что состоят только из неокрашенных, то есть входящих в формулу ровно три раза, литералов. Можно показать, что после расщепления по любому из них в формуле вновь появляются литералы, по которым можно произвести "выгодное" расщепление. Рассмотрение этих двух уровней, т.е. расщепление на четыре подзадачи с рекуррентным уравнением t(x) — 2Ь{х — 6) + 2Ь(х — 7), приводит к оценке р(Ь) 1.2389л.

Правило черных и белых литералов оказывается полезным и для задачи выполнимости формул в КНФ-(1,оо), рассматриваемой в главе 4. Являющееся его следствием правило разделения знаков позволяет построить алгоритмы, проверяющие выполнимость таких формул за время р(Ь) 1.0644х и р(Ь)1Л939к. Выполнимость формул в 3-КНФ-(1,оо)

проверяется за время p(L) 1.3581я; для формул в &-КНФ-(1,оо) верхняя оценка составляет для вероятностного алгоритма и p(L)(21-£fe/fc -f l)jV/3 для детерминированного € [0; 0.5] — решение уравнения ek/k - 1 = ек log2 £к + (1 - £*) bg2 (1 - £*))•

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

В данной диссертации метод расщеплений применяется и для решения (как точного, так и приближенного) задачи максимальной выполнимости. В ряде работ МАКС-ВЫП рассматривается как задача с весами — каждой дизъюнкции входной формулы приписан вес, и требуется найти набор, выполняющий дизъюнкции с как можно большим суммарным весом. В данной диссертации рассматривается случай, когда все веса равны единице; однако задача остается MAXSNP-полной и в такой формулировке (см., например, [30]). В главе 6 строится алгоритм, время работы которого зависит от необходимой степени приближения; он находит точное решение МАКС-ВЫП за время р(Ь)фК (где ф = (\/5 + 1)/2 — "золотое сечение"), а (0.770 + £)-приближенное решение (т.е. набор, выполняющий долю (0.770 +г) от количества дизъюнкций, выполняемых оптимальным набором) — за время р{Ь)фАЛШК. Похожие оценки доказываются для вероятностных и детерминированных алгоритмов для задач МАКС-ВЫП, МАКС-2-ВЫП, МАКС-З-ВЫП. В частности, строится вероятностный алгоритм, находящий (7/8 -I- s)-приближенное решение задачи МАКС-З-ВЫП за время p(L)2SsK. Полиномиальный по времени детерминированный алгоритм для этой задачи может существовать только если Р = NP [20].

количество дизъюнкций К длина формулы Ь количество переменных N

КНФ 1.2389^ 1.0758х

КНФ-(1,ос) 1.1939к 1.0644х

ЬКНФ-(1,оо) детерминированный -£к/к + вероятностный (21~1 /* + ^/3

3-КНФ-(1,оо) 1.3581*

Таблица И: Верхние оценки для алгоритмов для задачи ВЫП, использующих метод расщепления, полученные в данной диссертации. Оценки приведены с точностью до полиномиального сомножителя р(Ь). Величина £к Е [0;0.5] — решение уравнения £к/к — 1 = £к\о%2£к + (1 — - £к).

Алгоритм СБАТ. Вход:

Формула Р в КНФ. Вспомогательные данные:

Функции МАХРЫРБ и МАХТШЕБ, выдающие по формуле целое число. Выход:

Выполняющий набор для либо ответ "Невыполнима". Метод.

(1) Повторять МАХТШЕБ^) раз:

— Выбрать набор Л для формулы Р случайным образом.

— Повторять МАХРЫРЗ(Р) раз:

— — Если набор А выполняет формулу Р, то выдать А.

— — Выбрать переменную V в формуле Р, так чтобы

набор А с измененным значением V выполнял как можно больше дизъюнкций формулы Р.

— — Изменить значение переменной V в наборе А.

(2) Выдать ответ "Невыполнима".

Рис. I: Алгоритм СБАТ

Метод поиска локального максимума

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

Li ^

оценок времени исполнения в наихудшем случае , в то время как экспериментальные исследования были весьма широкими, и в результате них были получены данные в пользу эффективности таких алгоритмов. Единственные известные теоретические результаты касаются времени работы таких алгоритмов "в среднем" [22, 19, 15]. Б. Селман, Г. Левек и Д.Митчелл показали в [37], что простой "жадный" алгоритм, использующий поиск локального максимума, способен найти выполняющий набор для некоторых "трудных" булевых формул. Их алгоритм GSAT ("Greedy SAT", см. рис. I) показал обнадеживающие результаты для формул, получающихся при кодировании задачи о п ферзях и задачи о раскраске графа. Алгоритм GSAT начинает свою работу с набора для входной формулы, выбранного случайным образом (начального набора). В дальнейшем GSAT на каждом шаге изменяет значение одной из переменных так, чтобы как можно сильнее увеличить количество выполнившихся дизъюнкций ("увеличение" может быть нулевым или отрицательным). Если за определенное число шагов выполняющий набор не найден, GSAT начинает свою работу заново, выбрав другой случайный набор для входной формулы. Позднее было получено много экспериментальных результатов, касающихся различных модификаций GSAT [34, 36, 16, 17]. Б. Селман и Г. Кауц представили в [35] экспериментальные результаты, показывающие, что различные варианты GSAT могут решать задачи, возникающие при синтезе схем и плани-

ровании. Однако, ни для одного из упомянутых алгоритмов не было доказано никаких нетривиальных оценок на время исполнения "в наихудшем случае", даже если рассматривать только входные формулы, относящиеся к какому-либо конкретному классу.

В данной диссертации впервые приводится нетривиальная оценка времени исполнения "в наихудшем случае" для алгоритма поиска локального максимума. Именно, оценивается время работы алгоритма CSAT ("Cautious SAT", см. рис. II). Этот алгоритм был предложен Я.П.Гентом и Т. Уэлшем, которые привели в [16] экспериментальные данные, показывающие, что этот алгоритм ведет себя не хуже, чем GSAT.

Верхняя оценка доказывается для формул в к-ККФ-d: каждая дизъюнкция имеет длину не более к, каждая переменная входит в формулу не более d раз. (Как уже отмечалось выше, задача выполнимости для таких формул NP-полна даже при к — d = 3.) В отличие от алгоритма GSAT, алгоритм CSAT выбирает не переменную, приводящую к самому большому росту количества выполненных дизъюнкций, а любую из переменных, приводящих хоть к какому-нибудь росту, и делает это случайным образом. Если переменных, приводящих к росту, нет, алгоритм CSAT выбирает переменную, не изменяющую количества выполненных дизъюнкций, а если нет и таких, то произвольную переменную. Я.П.Гент и Т. Уэлш опубликовали результаты экспериментов, показывающих, что этот алгоритм имеет сходное время исполнения с алгоритмом GSAT. Для простоты доказательства, в данной диссертации рассмотрен ослабленный вариант алгоритма CSAT, который способен делать только "ходы вверх" (т.е. выбирать переменные, приводящие к росту количества выполненных дизъюнкций). Оказывается, что даже в таком варианте алгоритм CSAT решает задачу о выполнимости формулы в к-КНФ-d за время p(N)2lN с вероятностью ошибки не

Алгоритм CSAT. Вход:

Формула F в КНФ. Вспомогательные данные:

Функции MAXFLIPS и MAXTRIES, выдающие по формуле целое число. Выход:

Выполняющий набор для F, либо ответ "Невыполнима". Метод.

(1) Повторять MAXTRIES(F) раз:

— Выбрать набор А для формулы F случайным образом.

— Повторять MAXFLIPS (F) раз:

— — Если набор А выполняет формулу F, то выдать А. ■— — Выбрать случайным образом переменную v в формуле F, такую что набор, полученный из А заменой значения переменной v, выполняет больше дизъюнкций формулы F, чем набор А.

Если таких переменных нет, выбрать случайным образом переменную v, которая не приводит к изменению количества выполненных дизъюнкций.

Если нет и таких переменных, выбрать случайным образом переменную v из множества всех переменных, встречающихся в формуле F.

— — Изменить значение переменной v в наборе А.

(2) Выдать ответ "Невыполнима".

Рис. II: Алгоритм CSAT

более 1/е (здесь е — основание натуральных логарифмов, 7 = 1 — т.е. значительно быстрее, чем алгоритм, просто перебирающий случайные наборы. Этот результат остается справедливым и для исходного алгоритма CSAT.

В той же главе доказывается и нижняя оценка на время работы алгоритмов CSAT и GSAT в общем случае, т.е. когда на вход им подается произвольная формула в КНФ. Строится последовательность выполнимых формул Fn от N переменных, таких что алгоритм CSAT (или GSAT) может найти выполняющий набор для формулы Fn, только если он случайно начнет очередную итерацию с этого набора либо с одного из наборов, отличающихся от него значением ровно одной переменной. Таким образом, математическое ожидание времени работы каждого из этих алгоритмов не может быть менее Q(2N/(N -f- 1)) при условии, что вероятность ошибки (т.е. ответа "Невыполнима" для выполнимой формулы) ограничена снизу константой.

Структура диссертации

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

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

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

преобразования.

Во третьей главе приводятся алгоритмы для ВЫП, дающие новые верхние оценки для этой задачи. Эти алгоритмы используют метод расщеплений. Улучшение оценок достигается за счет вводимого здесь нового правила преобразования формул — правила черных и белых литералов. Алгоритмы, построенные на основе этого правила, решают задачу выполнимости за время, не превосходящее р(Ь) 1.2389^ и р(Ь) 1.07581.

В четвертой главе аналогичная техника применяется к формулам в КНФ-(1,оо). Все приводимые в ней алгоритмы используют метод расщеплений, а также правило черных и белых литералов. Полученные алгоритмы для формул в КНФ-(1,оо) заканчивают свою работу за время, не превосходящее р(£)1.1939А и р(Ь) 1.06442'. Для формул в 3-КНФ-(1,оо) доказывается верхняя оценкар(Ь)1.3581*, а для формул в &-КНФ — оценка р(Ь)(21~1/к 4- для вероятностного алгоритма и р(Ь)(21~£к/к + для детерминированного £ [0; 0.5] — решение уравнения ек/к- 1 = ек log2 ^ + (1 - ек) log2 (1-е*)).

Как уже отмечалось выше, существует простой вероятностный алгоритм, быстро находящий выполняющий набор для формулы в &-КНФ, доля выполняющих наборов для которой ограничена снизу константой. В пятой главе приводится детерминированный алгоритм, решающий эту задачу за линейное время. Этот алгоритм использует метод расщеплений, однако обходит дерево расщепления не в глубину, а в ширину. Выполняющий набор, выдаваемый этим алгоритмом, является "коротким", т.е. количество переменных, которым он присваивает значения, ограничено константой. В конце главы показывается, что, в отличие от формул в &-КНФ, формула в КНФ без ограничения на длину дизъюнкций может не иметь "коротких" выполняющих наборов, даже если половина всех наборов для нее — выполняющие.

В шестой главе метод расщеплений переносится на задачу максимальной выполнимости. Общая схема алгоритма, использующего метод расщеплений, дополняется для решения МАКС-ВЫП. Доказывается, что с помощью этой схемы можно находить как точные, так и приближенные (с произвольной степенью точности) решения. Приводятся правила преобразования формул, которые можно использовать при решении задачи максимальной выполнимости; показывается, как по точному или приближенному решению для преобразованной формулы найти решение для исходной. Общая схема применяется последовательно к формулам в КНФ, 2-КНФ, 3-КНФ и выполнимым формулам, в каждом из этих разделов доказывается верхняя оценка для соответствующего класса формул. Для нахождения точного решения МАКС-ВЫП доказывается верхняя оценка р(Ь)фк, где ф — "золотое сечение". Для нахождения а-приближенного решения, доказываются оценка рЩф^^1^ в случае задач МАКС-ВЫП и МАКС-2-ВЫП, и

Га-арjA

оценка p{L)2 \ I в случае задачи МАКС-З-ВЫП, в предположении, что существует полиномиальный по времени алгоритм для соответствующей задачи, находящий ао-пРиближение. Полученные оценки применяются для конкретных известных полиномиальных по времени приближенных алгоритмов для этих задач. Результаты пятой главы получены совместно с М. Р. Гавриловичем, Е. Я. Данциным и Б. Ю. Коневым.

В седьмой главе изучаются алгоритмы, использующие метод поиска локального максимума. Доказывается верхняя оценка q(N)2jN (при 7 = 1 - -L) для алгоритма CSAT в случае, если на вход ему подана формула в &-КНФ-<1 Для случая произвольных формул в КНФ доказывается нижняя оценка порядка 2N. Эта оценка справедлива как для алгоритма CSAT, так и для алгоритма GSAT.

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

Заключение диссертации по теме «Теоретические основы информатики», Гирш, Эдуард Алексеевич

Выход:

Выполняющий набор для F, либо ответ "Невыполнима".

Метод.

1) Если в формуле F имеется положительная 3-дизъюнкция С = {щ,и2,щ}, применить алгоритм 4.2 для каждой из формул F[ui] и F\u\\. Если для формулы F[u\] был получен выполняющий набор А\, выдать набор A\U {щ}. В противном случае, если для формулы F\W[] был получен выполняющий набор А2, выдать набор А2 U {гГГ}. Если для обеих формул был получен ответ "Невыполнима", выдать "Невыполнима".

2) Положить формулу G равной результату применения процедуры 4.2 к формуле F.

Рис. 4.4: Алгоритм 4.2: начало.

3) Положить Р+ равным множеству всех положительных дизъюнкций формулы Ст.

4) Для каждой дизъюнкции С = {^1,^2} £ Р+ проделать следующую операцию: удалить С из формулы С, а затем заменить в £ каждое вхождение литерала Щ на литерал щ.

5) Положить набор А равным результату применения к формуле й алгоритма А.

6) Для каждой переменной «2, удаленной на шаге (4), добавить литерал Щ к набору А, если щ £ А, в противном случае добавить литерал щ к набору А (где щ — литерал, входящий в ту же самую дизъюнкцию множества Р+, что и литерал щ).

7) Выдать набор А.

Рис. 4.5: Алгоритм 4.2: окончание. только ветвь дерева расщепления, ведущая к какому-нибудь одному конкретному выполняющему набору).

Формально, вместо алгоритма 4.2 следовало описать несколько алгоритмов (так как для разных значений к следует использовать разные алгоритмы Л). Вместо этого опишем один алгоритм 4.2 и будем каждый раз упоминать, какой именно алгоритм используется в нем в качестве алгоритма Л (когда это будет существенно).

Замечание 4.1 На данный момент наилучшим алгоритмом для задачи 3-ВЫП является алгоритм О. Кулльманна [23], находящий ответ2 за время ро1у(Ь) 1.5045*. (Верхнюю оценку ро1у(Ь) 1.497*, анонсированную И. Шиермейером [33], пока нельзя считать доказанной.) Для формул в &-КНФ при к > 4 имеется вероятностный алгоритм Р. Патури, П. Пудлака и Ф. Зейна [31], находящий ответ за время 2(1~1/^лгро1у(£). Наилучший детерминированный алгоритм для этой задачи для к > 5 приводится в той же статье, время его работы составляет , где £ £ [0; 0.5] — решение уравнения (4.5). Для к = 4 наилучший алгоритм [3, 29, 4] находит выполняющий набор за время ро1у(£)г(1,2,3)*. Некоторые из упомянутых алгоритмов сформулированы в слегка других терминах, но каждый из них может быть легко приведен к виду, принятому в данной диссертации, т.е. перестраивается в алгоритм, находящий выполняющий набор для формулы в &-КНФ.

Лемма 4.5 Процедура 4.2 выдает ответ за время, полиномиальное от длины входной формулы. Количество входящих в нее переменных не превосходит количества переменных, входящих в исходную формулу. Если для некоторого к, входная формула является формулой в

2Этот алгоритм сформулирован в терминах двойственной задачи: задачи выполнимости формулы в дизъюнктивной нормальной форме; кроме того, он решает задачу распознавания, но легко может быть преобразован к необходимому нам виду.

-КНФ-(1,оо), выходная формула также является формулой в &-КНФ-(1,оо).

Доказательство. Время работы каждого из шагов процедуры 4.2 не превосходит некоторого полинома от длины обрабатываемой формулы. На каждой итерации, заключенной между двумя последовательными исполнениями шага (1), удаляется по крайней мере одна переменная. С другой стороны, легко заметить, что количество переменных, входящих в формулу, не увеличивается. Кроме того, в выходную формулу входят только дизъюнкции, входящие во входную, либо их подмножества, поэтому максимум длин дизъюнкций выходной формулы не превосходит максимума длин дизъюнкций входной формулы. □

Лемма 4.6 Пусть к > 3. Предположим, что время работы алгоритма Л, который используется в алгоритме 4.2, не превосходит р1(Ь)(м для формулы в &-КНФ длины Ь, в которую входят N переменных (1 < ( < 2, р1 — некоторый полином). Алгоритм 4.2 корректно решает задачу о выполнимости формулы в &-КНФ-(1,оо)-(+/-), обработанной процедурой 4.2 и не содержащей положительных 4+-дизъюнкций. Время его работы для входной формулы Р составляет ро1у(£(Р))(£ + 1)Л/'(-р)/3.

Доказательство. Корректность. Аналогично лемме 4.4. Ясно, что если формула в КНФ-(1,оо)-(4-/-), обработанная процедурой 4.2, не содержит положительных 4+-дизъюнкций, то каждая ее положительная дизъюнкция имеет длину 2 либо 3.

Время работы. Пусть Л^ — количество переменных во входной формуле. Пусть входная формула содержит £ < Л^/З положительных 3-дизъюнкций. Рассмотрим дерево Г, образованное естественным образом формулами, расщепляемыми на шаге (1) алгоритма 4.2. Из каждой его внутренней вершины выходит два ребра, соответствующих формулам Р[щ] и Р[гГ[]. Будем называть эти ребра соответственно ребрами типа 1 и типа 2. Листьями дерева Т будут формулы, которые алгоритм 4.2 не расщепляет, а передает алгоритму А. При этом перед тем, как передать формулу алгоритму А, на шаге (4) алгоритм 4.2 сокращает количество переменных в два раза.

При проходе по ребру типа 2 удаляется одна переменная, при проходе по ребру типа 1 удаляется одна переменная и удаляются единственные положительные вхождения еще двух переменных, отрицательные вхождения которых удаляются затем на шаге (2) процедуры 4.2, вызванной на шаге (2) алгоритма 4.2. Поэтому если путь из корня дерева Т до некоторого листа проходит ровно через ребер типа 1 и ровно через г2 ребер типа 2, то в формуле, находящейся в этом листе, имеется не более (Д^ — 3«1 — ¿2)/2 переменных. Заметим, что %\ + %2 = так как в результате расщепления не могут исчезать положительные 3-дизъюнкции, отличные от непосредственно расщепляемой, и не могут появляться новые. Для данных ¿1 и г2 в дереве Т имеется не более ) различных листьев с подобным путем из корня. Следовательно, алгоритм 4.2 должен выдать ответ, затратив время, не превосходящее

Р2(1) £ (*\с("°-3;'-;')/2р1(Ь) < й=0 \!2/

3=0 \г2/ ¡,=0 у < = рз(£)(С + 1)""/3, где р2(Ь) — некоторый подходящий полином, рз = р\р2. Справедливость второго неравенства вытекает из того, что для 1 < С < 2 верно, что С + 1 > С3/2, a t < No/3. □

Теорема 4.3 Пусть к > 3. Предположим, что время работы алгоритма Л, который используется в алгоритме 4.2, составляет poly(L)CJV для формулы в к-КНФ длины L, в которую входят N переменных (1 < ( < 2). Рассмотрим алгоритм 2.1, в котором в качестве процедуры Reduce используется процедура 4.2, в качестве процедуры Lift — соответствующая процедура, полученная на основе описания процедуры reduce и материала разделов 2.4 и 4.1, в качестве условия DONE — условие "формула принадлежит классу КНФ-(1,оо)-(+/-) и не содержит положительных 4+-дизъюнк-ций", в качестве алгоритма Leaf — алгоритм 4.2, в качестве числа s — единица, в качестве меры сложности // — количество дизъюнкций N в формуле, в качестве числа расщепления Л — число г(1,4). Тогда алгоритм 2.1 корректно решает задачу &-ВЫП-(1,оо) и время его работы для формулы F составляетpoly(£(F)) max(r(l,4), (C+l)1/3)^^. Доказательство. Учитывая теорему 2.1 и леммы 4.5 и 4.6, достаточно показать, что для всякой формулы F в КНФ-(1,оо), обработанной процедурой 4.2, но не удовлетворяющей условию Done, алгоритм 2.1 может найти на шаге (2) процедуры 2.1 подходящее расщепление. В зависимости от того, является ли F формулой в КНФ-(1,оо)-(+/-), возможны два случая.

Случай 1. F является формулой в КНФ-(1,оо)-(+/-).

Формула F не удовлетворяет условию Done, и поэтому содержит положительную 4+-дизъюнкцию С = {wi,m2, w3,w4,. ,wm}. Рассмотрим расщепление типа (2.1) по литералу щ. При переходе от формулы

Р к формуле исчезает переменная щ; затем не позднее шага (2) процедуры 4.2 исчезают и переменные щ, щ и И4, так как литералы Щ, Щ и Щ становятся чистыми в формуле Р[мх]. С другой стороны, при переходе от формулы Р к формуле Р[«Г] переменная щ также исчезает. Таким образом, этому случаю соответствует число расщепления г(1,4).

Случай 2. Р не является формулой в КНФ-(1,оо)-(+/-).

Докажем, что этому случаю соответствует даже меньшее число расщепления г(2,3) (это понадобится нам при доказательстве теоремы 4.4). Поскольку формула Р не удовлетворяет условию шага (4) процедуры 4.2, в ней имеются положительная дизъюнкция С = {щ,и2,., ит} и дизъюнкция в которую входят литерал Щ и некоторый положительный литерал V. Рассмотрим расщепление типа (2.1) по литералу щ. Возможны два подслучая: т = 2 и га > 3.

Случай 2.1. га = 2.

Покажем, что Л/"(Р) — Л/"((Р)и1) > 2. Действительно, переменная щ удаляется сразу при переходе от формулы Р к формуле Р[мх], а переменная и2 удаляется не позднее шага (2) процедуры 4.2, так как литерал Щ становится чистым литералом в формуле Р[их].

С другой стороны, Л/"(Р) -ЛГ((Г)щ) > 3. Действительно, переменная щ удаляется при переходе к формуле Р[йх]. Дизъюнкция С становится 1-дизъюнкцией {г^} в формуле Р[мГ]5 поэтому переменная щ удаляется на шаге (1) процедуры 4.2. Литерал V становится чистым литералом в формуле Р[«Т], поэтому переменная V удаляется не позднее шага (2) процедуры 4.2.

Таким образом, этому случаю соответствует число расщепления г(2,3) < г(1,4).

Случай 2.2. га = 3.

Покажем, что Л/^Р) — Л/'ЦР)^) > 3. Действительно, переменная и\ удаляется сразу при переходе от формулы F к формуле F[ui], а переменные щ и щ удаляются не позднее шага (2) процедуры 4.2, так как литералы Щ и Щ становятся чистыми литералами в формуле F[mi].

С другой стороны, J\f(F) — Af((F)st) > 2. Действительно, переменная щ удаляется при переходе к формуле F[iЦ). Литерал v становится чистым литералом в формуле поэтому переменная v удаляется не позднее шага (2) процедуры 4.2.

Таким образом, этому случаю соответствует число расщепления г(2,3) < т(1,4).

Теорема 4.4 Пусть, в условиях теоремы 4.3, к = 3. Рассмотрим алгоритм 2.1, в котором в качестве числа расщепления А используется число г(2,3), а остальные вспомогательные процедуры и параметры — такие же, как и в теореме 4.3. Тогда алгоритм 2.1 корректно решает задачу 3-ВЫП-(1,оо) и время его работы для формулы F составляет poly(£(F)) max(r(2,3), (С + l)1/3)^ в условиях теоремы 4.3.

Доказательство. Доказательство аналогично доказательству теоремы 4.3. Единственное отличие заключается в том, что, в условиях настоящей теоремы, формула F, расщепляемая на шаге (2) процедуры 2.1, не может быть формулой в КНФ-(1,оо)-(+/-) (иначе по лемме 4.5 она была бы формулой в 3-КНФ-(1,оо)-(+/-) и, следовательно, удовлетворяла бы условию Done). Поэтому достаточно рассмотреть только случаи 2.1 и 2.2, а им соответствует число расщепления т(2,3). □

Конкретизируем теперь результаты теорем 4.3 и 4.4, подставляя в качестве алгоритма Л, используемого в алгоритме 4.2, различные известные алгоритмы.

Следствие 4.1 Пусть к > 4. С помощью алгоритма, описанного в теореме 4.3, можно решить задачу &-ВЫП-(1,оо) для формулы F верок 3 4 5 6 7 детерминированный 1.3581 1.4161 1.4271 1.4292 1.4308 вероятностный — 1.3894 1.3996 1.4064 1.4114

Список литературы диссертационного исследования кандидат физико-математических наук Гирш, Эдуард Алексеевич, 1998 год

Литература

[1] Гэри М., Джонсон Д. Вычислительные машины и труднорешаемые задачи. Пер. с англ.— М.: Мир, 1982.— 416 с.

[2] Данцин Е. Я. Две системы доказательства тавтологичности, основанные на методе расщеплений // Записки научных семинаров ЛОМИ.— Л., 1981.— Т. 105.— С. 24-44.

[3] Данцин Е. Я. Системы доказательства тавтологичности, основанные на методе расщеплений.— Диссертация на соискание степени канд. ф.-м. н.— Ленинград, ЛОМИ, 1983.— 98 с.

[4] Данцин Е. Я. Алгоритмика задачи выполнимости //В сб.: Вопросы кибернетики.— РАН, 1987 — №131.— С. 7-29.

[5] Цейтин Г. С. О сложности вывода в исчислении высказываний // Записки научных семинаров ЛОМИ.— Л., 1968.— Т. 8.— С. 234259.

[6] Arora S., Lund С. Hardness of approximation // In: Approximation algorithms for NP-hard problems / D.Hochbaum, editor.— Boston, PWS Publishing Company, 1997.— Ch. 10.

[7] Asano T. Approximation algorithms for MAX SAT: Yannakakis vs. Goemans-Williamson // Proceedings of the 5th Israel Symposium on Theory and Computing Systems.— 1997.— P. 24-37.

[8] Beigel R., Eppstein D. 3-coloring in time 0(1.3446"): a no-MIS algorithm // Proceedings of the 36th Symposium on Foundations of Computer Science.— 1995.— P. 444-452.

[9] Borchers В., Fuhrman J. A Two-Phase Exact Algorithm for MAXSAT and Weighted MAX-SAT Problems //To appear in Journal of Combinatorial Optimization.— 1997.

[10] Cook S., Reckhow R. On the lengths of proofs in the propositional calculus (preliminary version) // Conference Record of Sixth Annual

ACM Symposium on Theory of Computing.— 1974.— P. 135-148.

[11] Crawford J. M., Auton L. D. Experimental Results on the Crossover Point in Satisfiability Problems // Proceedings of the 11th National Conference on Artificial Intelligence.— AAAI Press, 1993.— P. 21-27.

[12] Davis M., Logemann G., Loveland D. A machine program for theoremproving // Comm. ACM.— 1962.— №5.— P. 394-397.

[13] Davis M., Putnam H. A computing procedure for quantification theory // J. Assoc. Comp. Mach.— I960.— №7.— P. 201-215.

[14] Feige U., Goemans M. X. Approximating the value of two proper proof systems, with applications to MAX-2SAT and MAX-DICUT // Proceedings of the 3rd Israel Symposium on Theory and Computing Systems.— 1995.— P. 182-189.

[15] Franco, J., Swaminathan, R. Average case results for satisfiability algorithms under the random clause model //To appear in Annals of Mathematics and Artificial Intelligence.— 1998.

[16] Gent I. P., Walsh T. Towards an understanding of hill-climbing procedures for SAT // Proceedings of the 11th National Conference on Artificial Intelligence.— AAAI Press, 1993.— P. 28-33.

[17] Gent I. P., Walsh T. Unsatisfied Variables in Local Search // Hybrid Problems, Hybrid Solutions (AISB-95).— Amsterdam, IOS Press.— 1995.

[18] Goemans M. X., Williamson D. P. Improved approximation algorithms for maximum cut and satisfiability problems using semidefinite programming // Journal of the ACM— 1995 — Vol. 42, №6.— P. 11151145.

[19] Gu, J., Gu, Q.-P. Average Time Complexity of The SAT1.2 Algorithm // Proceedings of the 5th Annual International Symposium on Algorithms and Computation.— 1994.— P. 147-155.

[20] Hastad J. Some optimal inapproximability results // Proceedings of

the 29th Annual ACM Symposium on Theory of Computing.— 1997.— P. 1-10.

[21] Karloff H., Zwick U. A 7/8-approximation algorithm for MAX 3SAT? // Proceedings of the 38th Annual IEEE Symposium on Foundations of Computer Science— 1997.— P. 406-415.

[22] Koutsoupias, E., Papadimitriou, C. H. On the greedy algorithm for satisfiability // Information Processing Letters.— 1992.— Vol.43, №1.— P. 53-55.

[23] Kullmann 0. Worst-case Analysis, 3-SAT Decision and Lower Bounds: Approaches for Improved SAT Algorithms // DIM ACS Proceedings SAT Workshop 1996.— American Mathematical Society, 1996.— P. 261-313.

[24] Kullmann O., Luckhardt H. Deciding propositional tautologies: Algorithms and their complexity // Submitted to Information and Computation.— 1997.

[25] Luckhardt H. Obere Komplexitätsschranken für TAUT-Entscheidungen // Proceedings of Frege Conference.— Schwerine, Akademie-Verlag Berline, 1984.— P. 331-337.

[26] Mahajan S., Ramesh H. Derandomizing semidefinite programming based approximation algorithms // Proceedings of the 36th Annual IEEE Symposium on Foundations of Computer Science.— 1995.— P. 162-169.

[27] Monien B., Speckenmeyer E. 3-satisfiability is testable in 0(1.62r) steps.— Bericht Nr. 3/1979.— Reihe Theoretische Informatik, Universität-Gesamthochschule-Paderborn.

[28] Monien B., Speckenmeyer E. Upper bounds for covering problems.— Bericht Nr. 7/1980.— Reihe Theoretische Informatik, UniversitätGesamthochschule-Paderborn.

[29] Monien B., Speckenmeyer E. Solving satisfiability in less than 2" steps

// Discrete Applied Mathematics— 1985 — Vol. 10 — P. 287-295.

[30] Papadimitriou Ch.H. Computational Complexity.— Addison-Wesley, 1994.— 532 p.

[31] Paturi R., Pudlak P., Zane F. Satisfiability Coding Lemma // Proceedings of the 38th Annual Symposium on Foundations of Computer Science.— 1997.— P. 566-574.

[32] Schiermeyer I. Solving 3-satisfiability in less than 1.579" steps // Lecture Notes in Computer Science.— Springer-Verlag, 1993.— Vol.702.— P. 379-394.

[33] Schiermeyer I. Pure literal look ahead: An 0(1.497") 3-Satisfiability algorithm // In: Workshop on the Satisfiability Problem, Technical Report.— Siena, April, 29 - May, 3, 1996.— University Koln, Report No. 96-230.

[34] Selman, B., Kautz, H. An Empirical Study of Greedy Local Search for Satisfiability Testing // Proceedings of the 11th National Conference on Artificial Intelligence.— AAAI Press, 1993.— P. 46-53.

[35] Selman B., Kautz H. Pushing the Envelope: Planning, Propositional Logic and Stochastic Search // Proceedings of the 13th National Conference on Artificial Intelligence and the 8th Innovative Applications of Artificial Intelligence Conference.— AAAI Press/MIT Press, 1996.— Vol.2.— P. 1194-1201.

[36] Selman, B., Kautz, H., Cohen, B.: Noise strategies for improving local search // Proceedings of the 12th National Conference on Artificial Intelligence — AAAI Press, 1994.— Vol. 1 — P. 337-343.

[37] Selman B., Levesque H., Mitchell D. A New Method for Solving Hard Satisfiability Problems // Proceedings of the 10th National Conference on Artificial Intelligence.— MIT Press, 1992.— P. 440-446.

[38] Trevisan L., Sorkin G. B., Sudan M., Williamson D.P. Gadgets, approximation, and linear programming // Proceedings of the 37th

Annual IEEE Symposium on Foundations of Computer Science.— 1996.— P. 617-626.

[39] Urquhart A. The Complexity of Propositional Proofs // Bulletin of Symbolic Logic.— 1995 — Vol. 1, №4.— P. 425-467.

[40] Van Gelder A. A satisfiability tester for non-clausual proposition calculus // Information and Computation.— 1988.— P. 1-21.

[41] Yannakakis M. On the approximation of maximum satisfiability // Journal of Algorithms.— 1994 — №17 — P. 475-502.

[42] Zhang, W. Number of models and satisfiability of sets of clauses // Theoretical Somputer Science — 1996 — №155.— P. 277-288.