Содержание к диссертации
Введение
1 Определения 10
1.1 Задачи булевой логики 10
1.1.1 Формулы в КНФ 10
1.1.2 Задачи выполнимости и максимальной выполнимости 12
1.2 Алгоритм расщепления 14
1.3 Анализ алгоритмов расщепления 17
1.4 Класс формул 19
2 Методы доказательства верхних оценок, использующиеся в работе 23
2.1 Пример простого алгоритма расщепления 24
2.2 Общее правило упрощения 26
2.3 Автоматический анализ сложности алгоритмов расщепления 28
2.4 Комбинированные меры сложности 29
2.5 Запоминание дизъюнктов 33
3 Автоматическое порождение правил упрощения 35
3.1 Известные правила упрощения для SAT и MAX-SAT 35
3.2 Общее правило упрощения 37
3.3 Алгоритм для (n, 3)-MAX-SAT 44
4 Автоматический анализ времени работы 50
4.1 Описание программы 50
4.1.1 Входные и выходные данные 51
4.1.2 Алгоритм построения доказательства 54
4.1.3 Детали реализации 57
4.1.4 Правила упрощения 60
4.1.5 Правило расщепления 60
4.1.6 Мера сложности 61
4.1.7 Инвариант 61
4.2 Автоматически доказанные верхние оценки 62
4.3 Подобные работы 64
5 Комбинированные меры сломсности и запоминание дизъюнктов 67
5.1 Решение MAX-SAT на формулах константной плотности быстрее, чем за 2N 67
5.2 Алгоритм для MAX-2-SAT 71
5.2.1 Правила упрощения 72
5.2.2 Правила расщепления 76
5.2.3 Алгоритм для MAX-2-SAT 78
5.2.4 (n, 3)-М AX-2-SAT 83
- Автоматический анализ сложности алгоритмов расщепления
- Общее правило упрощения
- Автоматически доказанные верхние оценки
- Решение MAX-SAT на формулах константной плотности быстрее, чем за 2N
Введение к работе
Интерес к доказательству экспоненциальных верхних оценок для NP-трудных задач в последние несколько десятилетий остается на стабильно высоком уровне. Одним из наиболее хорошо изученных подходов к доказательству таких оценок является метод расщепления. Впервые данный метод был предложен в 1960-м году Дэвисом и Патнемом [19] и сформулирован в более современном виде Дэвисом, Лоджеманном и Лавлэндом [18] в 1962-м году. Его основная идея заключается в расщеплении входного примера задачи на несколько более простых примеров (упрощаемых в дальнейшем некоторыми правилами упрощения), таких что, построив решение для каждого из них, возможно за полиномиальное время построить решение для исходного примера. В списке ниже мы приводим некоторые верхние оценки на время решения NP-трудных задач в наихудшем случае, доказанные методом расщепления и являющиеся наилучшими из известных (здесь и на протяжении всей работы мы опускаем полиномиальные от размера входа множители в оценках, указывая только экспоненциальную составляющую):
1. 1.0741, для задачи пропозициональной выполнимости формул в КНФ, где L — длина (то есть общее количество литералов) входной
формулы [23];
1.341294^ для задачи максимальной выполнимости, где К — количество дизъюнктов входной формулы [14];
1.122463771 для задачи о максимальном разрезе, где т — количество ребер входного графа [36];
1.328971 для задачи о 3-раскрашиваемости графа, где п — количество вершин входного графа [12].
В диссертации рассматриваются алгоритмы расщепления в применении к задачам выполнимости и максимальной выполнимости. Обе задачи формулируются на языке булевых формул, являющемся очень удобным для кодирования многих алгоритмических задач (таких, например, как автоматическое доказательство теорем, составление расписаний, оптимизационные задачи на графах). Задача пропозициональной выполнимости (satisfiability problem, SAT) является одной из наиболее известных NP-полных задач (см., например, [1]). Данной задаче посвящена международная ежегодная конференция (The International Conference on Theory and Applications of Satisfiability Testing), проводящаяся уже более десяти лет, а также научный журнал (Journal on Satisfiability, Boolean Modeling and Computation). Поскольку NP-трудные задачи часто возникают в практических приложениях (например, при разработке микросхем, в распознавании образов), важное место в исследовании задачи выполнимости занимает разработка программ, решающих SAT (такие программы называются SAT-солверами). Ежегодно проводятся соревнования таких программ.
Современные SAT-солверы способны быстро решать многие задачи, считавшиеся нерешаемыми несколько лет назад.
Важным оптимизационным обобщением задачи выполнимости является задача максимальной выполнимости (maximum satisfiability problem, MAX-SAT). В терминах задачи MAX-SAT могут быть естественным образом переформулированы многие оптимизационные NP-трудные задачи, к примеру, такие оптимизационные задачи на графах, как задача о максимальном разрезе (maximum cut problem, MAX-CUT), задача о минимальном вершинном покрытии (minumum vertex cover problem), задача о максимальном независимом множестве (maximum independent set problem). Задача MAX-SAT возникает также в задачах искусственного интеллекта и комбинаторной оптимизации [37, 22]. В статье Кресензи и Канна [15] перечислены 15 самых популярных задач комбинаторной оптимизации, в число которых входит и задача MAX-SAT.
Для задачи MAX-SAT существуют приближенные алгоритмы, находящие за полиномиальное время решение с некоторой гарантированной точностью. Например, алгоритм Асано и др. [8] выдает набор, выполняющий хотя бы долю 0.77 количества дизъюнктов, выполненных оптимальным набором. В то же время известно, что в предположении P^NP не существует полиномиального по времени алгоритма, находящего приближенное решение, сколь угодно близкое к оптимальному. Алгоритм Данцина и др. [17] находит такое приближение, но за экспоненциальное время. Известно также много алгоритмов, решающих практические примеры задачи максимальной выполнимости (см., например, [13, 10, 39]). Для данных алгоритмов,
однако, неизвестно никаких оценок (кроме тривиальных) на время работы в наихудшем случае.
Наряду с общей задачей максимальной выполнимости мы рассматриваем следующие ее частные случаи:
(n, 3)-MAX-SAT — вариант задачи MAX-SAT для формул, в которых каждая переменная содержится не более, чем в трех дизъюнктах;
MAX-2-SAT — вариант задачи MAX-SAT, где каждый дизъюнкт входной формулы содержит не более двух литералов;
(n, 3)-MAX-2-SAT — вариант задачи MAX-SAT, где каждый дизъюнкт входной формулы содержит не более двух литералов и каждая переменная входит не более, чем в три дизъюнкта.
Известно, что все перечисленные выше задачи являются NP-трудными (доказательство NP-трудности задачи (n, 3)-MAX-2-SAT см., например, в [34]). Таким образом, в предположении P^NP не существует полиномиальных по времени алгоритмов для данных задач. Тем не менее, поскольку подобные задачи часто возникают в практических приложениях, важно понять, какое время требуется для их решения, даже если это время экспоненциально.
Как сказано выше, лучшие известные оценки для многих NP-трудных задач получены именно методом расщепления. Простейший алгоритм расщепления для задачи выполнимости на формуле с N переменными имеет время работы порядка 2N. Первые улучшения данной оценки были получены в начале 1980-х годов Мониеном и Шпекенмейером [30] и Данциным [2] для формул, длины дизъюнктов
которых ограничены некоторой константой. Позднее было получено много оценок, улучшающих тривиальную для некоторых NP-полных подклассов задач выполнимости и максимальной выполнимости. Вопрос о том, могут ли данные две задачи быть решены за время cN, где с < 2 — константа, до сих пор остается открытым и является одним из самых знаменитых вопросов современной теоретической информатики. Однако недавно были разработаны алгоритмы, решающие задачи выполнимости и максимальной выполнимости быстрее, чем за 2-^, для формул константной плотности, то есть формул, у которых отношение количества дизъюнктов к количеству переменных ограничено сверху некоторой константой [7, 16].
Типичный алгоритм расщепления сначала некоторым образом расщепляет формулу, после чего производит рекурсивные вызовы для формул меньшей сложности. Анализ такого алгоритма содержит разбор большого количества случаев, в каждом из которых показывается, что алгоритм всегда производит рекурсивные вызовы для формул, сложность которых меньше сложности исходной формулы хотя бы на некоторую константу. Для улучшения оценки на время работы алгоритма можно добавлять в алгоритм новые правила упрощения либо же проводить более детальный разбор случаев.
Основные результаты работы перечислены ниже.
Реализована программа, автоматически доказывающая верхние оценки на время работы алгоритмов расщепления путем анализа случаев. При помощи данной программы получено несколько новых оценок.
Разработано правило упрощения для задач выполнимости и
максимальной выполнимости, обобщающее известные правила упрощения, присваивающие значения переменным формулы.
Разработан алгоритм, решающий задачу MAX-SAT на формулах константной плотности А за время cN, где с = с(Л) < 2 — константа, с использованием лишь полиномиальной памяти.
Доказаны следующие новые верхние оценки на время работы алгоритмов расщепления:
2к/61 где К — количество дизъюнктов входной формулы, для MAX-2-SAT;
2N/6-7, где N — количество дизъюнктов входной формулы, для (n, 3)-MAX-2-SAT.
Алгоритмы для (n, 3)-MAX-SAT и MAX-2-SAT являются самыми быстрыми из известных. Алгоритм для MAX-SAT, работающий на формулах константной плотности быстрее, чем 2^, является первым известным алгоритмом для данной задачи, улучшающим тривиальную оценку и при этом пользующимся лишь полиномиальной памятью. Реализованная программа для автоматического анализа алгоритмов расщепления и обобщенное правило упрощения являются первыми в своем роде.
Основные результаты диссертации опубликованы в семи работах [3, 5, 6, 25, 24, 26, 4].
Автоматический анализ сложности алгоритмов расщепления
Как правило, анализ алгоритма расщепления состоит из длинного списка случаев. В каждом случае показывается, что соответствующее число расщепления не превосходит требуемой константы. В главе 4 мы представляем программу, осуществляющую такой разбор случаев автоматически. Данной программой были доказаны несколько нетривиальных оценок для задач SAT и MAX-SAT. Некоторые из них до сих пор остаются наилучшими из известных.
Покажем, как такая программа доказывает оценку 1.619 - на время работы алгоритма SATALGI, рассмотренного в разделе 2.1. Итак, программа знает, что алгоритм использует правила единичный дизъюнкт и чистый литерал, и ей требуется доказать, что алгоритм может расщепить любую формулу, к которой не применимы эти правила, так, чтобы соответствующее число расщепления относительно количества дизъюнктов не превосходило 1.619. Сначала программа находит все такие i,j, для которых наличие (г, -литерала в формуле мгновенно влечет существование необходимого расщепления. Поскольку (1,2) 1.619, таким оказываются все пары (i,j), где і l,j 2 или г 2, j 1. Ясно также, что упрощенная формула не содержит чистых литералов. Таким образом, программа может считать, что формула состоит только из (1,1)-литералов. С этого момента начинается разбор случаев, см. рис. 2.1. Выбирается произвольный литерал х и рассматривается класс формул
Поскольку для такого класса формул (1,2)-расщепление найти не удается, программа начинает разбирать под случаи. Именно, первый дизъюнкт текущего класса формул может либо не содержать больше литералов, либо содержать еще хотя бы один. Если больше литералов в нем нет, то этот дизъюнкт является единичным, что противоречит тому, что формула упрощена. Значит, этот дизъюнкт содержит еще хотя бы один литерал. Назовем его у. Мы знаем, что у является (1,1)-литералом. Есть два случая оставшегося вхождения литерала -iy. В каждом из этих случаев при расщеплении по х удаляется хотя бы одно вхождение переменной var(y), после чего правила упрощения удаляют и все оставшиеся вхождения этой переменной, что дает число расщепления не хуже т(1, 2).
Как правило, для доказательства верхних оценок на время работы алгоритма расщепления сперва фиксируется некоторая мера сложности формул, после чего показывается, что алгоритм всегда расщепляет входную формулу на несколько формул, сложности которых меньше сложности исходной формулы. Естественными мерами сложности формул являются количество переменных N, количество дизъюнктов К и длина формулы L. Известно большое количество верхних оценок относительно этих мер для задач SAT и MAX-SAT и их частных случаев. Иногда, однако, можно использовать нестандартную меру сложности для доказательства оценок относительно стандартной меры. Такой подход используется, например, Граммом и др. [21] для доказательства оценки 2К1Ъ для MAX-2-SAT и Кульманом [27] для доказательства оценки 1.5045 для 3-SAT. В данной работе мы также используем комбинированные меры сложности для доказательства новых оценок для MAX-SAT и MAX-2-SAT. Наша мера сложности для задачи MAX-SAT выглядит следующим образом: где w — некоторая константа. Мы показываем, что для любой формулы найдётся достаточно хорошее расщепление либо относительно количества переменных, либо относительно количества дизъюнктов. После этого мы подбираем константу w, зависящую от плотности формулы, так, чтобы соотвествующая оценка была меньше 2 . Ниже мы также описываем вид меры для MAX-2-SAT.
Пусть F — формула в 2-КНФ. Через Ni(F) мы обозначаем количество переменных F, входящих в ровно і 2-дизъюнктов формулы F. Легко видеть, что общее количество 2-дизъюнктов формулы K2{F) может быть выражено следующим образом:
В работе [24] мы доказываем оценку 2К1ЪЬ для MAX-2-SAT, используя следующую меру сложности для формул в 2-КНФ:
Поясним (неформально), как именно такое изменение коэффициентов может помочь доказать более сильные оценки для MAX-2-SAT. Заметим, что расщепление по переменной веса w (весом переменной 2-КНФ формулы называется количество 2-дизъюнктов формулы, в которые входит эта переменная) в общем случае является (го, гі )-расщеплением относительно Кч (поскольку в обеих ветках все 2-дизъюнкты, содержащие рассматриваемую переменную, либо выполняются, либо становятся единичными). Рассмотрим теперь переменную х веса 5. Если все соседи х различны и имеют вес не более 5, то расщепление по х является (5.5,5.5)-расщеплением относительно 7о, поскольку в обеих ветках х удаляется (70 уменьшается на 2.5) и веса всех ее соседей уменьшаются (70 уменьшается на 0.6 5). Если же х имеет вес 4 и все остальные переменные имеют вес не более 4, то при присваивании х булева значения 70 снова уменьшается хотя бы на 1.9 4- 4 0.6 = 5.5. Ясно также, что для любой формулы F в 2-КНФ выполняется неравенство 7о( ) (- ) поэтому любая оценка относительно 7о остаётся верной и при замене 7о на К. Таким образом, меньшая по значению мера позволила нам найти лучшее расщепление.
Общее правило упрощения
Основная часть программы реализована в процедуре ANALYZECASE (СМ. алг. 6). Говоря неформально, эта процедура пытается найти подходящее расщепление для входного класса формул. Если такое расщепление найдено, программа возвращает, в противном случае она строит несколько новых классов, объединение которых содержит исходный класс, и рекурсивно вызывает себя на этих классах. Легко видеть, что если эта процедура останавливается на данном классе формул, то для каждой формулы этого класса есть подходящее расщепление.
На первом шаге процедура ANALYZECASE проверяет, применимо ли к Т хотя бы одно правило множества S, и возвращает, если такое правило есть. Этот шаг мотивируется тем фактом, что алгоритм расщепления расщепляет только упрощенные формулы. На втором шаге процедура пытается найти подходящее расщепление (то есть расщепление, которому соответствует число расщепления, не превосходящее с) для входного класса формул и возвращает, если такое расщепление есть.
На третьем шаге процедура просто выбирает дизъюнкт с неопределенной длиной. Отметим, что можно не рассматривать ситуацию, когда таких дизъюнктов нет, поскольку в противном случае формула состоит из двух не пересекающихся по переменным формул, для которых задача может быть решена независимо.
На четвертом и пятом шагах процедура рассматривает два случая: когда выбранный дизъюнкт содержит еще хотя бы один литерал и когда не содержит. Другими словами, она расщепляет класс формул, для которого не может найти подходящее расщепление, на несколько
Алгоритм 6 ANALYZECASE Вход: класс формул Т
Параметры: множество правил упрощения S, множество правил расщепления 1Z, число с 1, мера сложности /І, эвристика выбора дизъюнкта е
Метод:і. построить множество всех возможных классов формул, получающихся из Т добавлением вхождений переменной и, при которых и становится (г, -переменной
іі. произвести рекурсивный вызов на каждом построенном классе формул
более мелких классов и рекурсивно вызывает себя на них. Целью данных двух шагов является построение классов формул, объединение которых содержит Т.
Мы используем отношение а на пятом шаге процедуры для обозначения множества пар (i,j), таких что (і, -литерал не предоставляет немедленно подходящего расщепления. Легко видеть, что для любой задачи это отношение может быть определено следующим образом: где К — количество дизъюнктов входной формулы, L — ее длина. Эти множества конечны вследствие свойств чисел расщепления (см. раздел 1.3). К сожалению, мы не можем определить такое конечное отношение, когда работаем с числом переменных, как с мерой сложности. Тем не менее, в случае задачи (n, 3)-MAX-SAT возможно написать следующее: где N — число переменных формулы.
Отметим, что на третьем шаге рассматриваемая процедура может выбрать любой дизъюнкт с неопределенной длиной, на практике же размер получающегося анализа случаев (когда мы записываем все классы формул, обработанные процедурой) сильно зависит от выбранного дизъюнкта. Текущая версия программы по умолчанию выбирает дизъюнкт следующим образом: для каждого дизъюнкта с неопределенной длиной строятся классы формул, как это делается на четвертом и пятом шагах процедуры, и считается количество плохих классов среди них (здесь мы называем класс плохим, если он не удовлетворяет условиям первых двух шагов процедуры). В итоге выбирается дизъюнкт, которому соответствует минимальное количество плохих классов. В подавляющем большинстве ситуаций эта эвристика выбора дизъюнкта позволяла получать доказательства меньшего размера, чем при использовании других эвристик. Более того, с некоторыми эвристиками программа не может доказать оценку, в то время как эту оценку можно доказать с другой эвристикой. Таким образом, эвристика выбора дизъюнкта является очень важной частью алгоритма. Основные классы программы перечислены ниже.
Содержит всю необходимую для разбора случаев информацию (такую как списки правил упрощения и расщепления, инварианты, эвристика выбора дизъюнкта). Анализ случаев производится вызовом метода StartCaseAnalysis (). Данный метод инициализирует все внутренние поля и вызывает метод AnalyzeCase ( CFormula к ) для класса дизъюнктов, состоящего из одного пустого дизъюнкта.
Как правило, используется для определения подкласса NP-трудной задачи. К примеру, мы унаследовали класс CMax2SatProblem от класса CMaxSatProblem и добавили экземпляр класса CClauseLengthRestriction в список инвариантов в конструкторе. Это, однако, не единственная возможность использования данного класса. Он может быть также использован для рассмотрения алгоритмов, поддерживающих некоторый инвариант входных формул. Такое ограничение иногда помогает избежать некоторых трудных случаев. Пример такого алгоритма можно найти в [14].
Отвечает за итерирование по всем возможным классам формул, получающимся из данного класса формул добавлением новой переменной. Используется при рассмотрении подслучаев процедурой ANALYZECASE.
Автоматически доказанные верхние оценки
Верхние оценки, доказанные нашей программой, представлены в таблице 4.1. Выходные файлы с доказательствами доступны по адресу (там же представлено несколько доказательств более простых оценок). Структура доказательств позволяет проверять каждый шаг программы. Отметим здесь, что большое количество случаев во всех представленных доказательствах не означает, что соответствующие алгоритмы сложны для реализации (на самом деле, форма таких алгоритмов дана в первой главе). Таблица 4.2 содержит статистику рассматриваемых доказательств. Ниже мы вводим обозначения, использующиеся в таблице. найденное число расщепления соответствует как раз ожидаемой верхней оценке). d: Максимальная глубина рекурсии процедуры ANALYZECASE. Несмотря на то, что лучшие известные на данный момент алгоритмы для SAT и MAXSAT используют метод расщепления, наша программа не смогла доказать их оценки. Причиной тому является то, что эти алгоритмы содержат некоторые нестандартные шаги, которые трудно добавить в нашу программу (равно как и во все известные на данный момент подобные программы). Ниже мы кратко описываем эти шаги: Алгоритм Гирша для SAT ([23]) использует следующее правило упрощения: если каждый дизъюнкт формулы, который содержит (2, 3+)-литерал, содержит также и (3+, 2)-литерал, то всем (3+, 2)-литералам может быть присвоено значение True.
Понятно, что такое правило невозможно добавить в нашу программу, поскольку программа может рассматривать только константное количество литералов. Алгоритм Чена и Кана для MAXSAT ([14]) сохраняет некоторый инвариант входной формулы. То есть он применяет правила упрощения или расщепляет входную формулу, только если все получающиеся формулы удовлетворяют этому инварианту. Это делается для того, чтобы избежать некоторых "узких" случаев. Приведенные оценки являются наилучшими из доказанных нашей программой для рассматриваемых задач. Как мы уже отмечали выше, невозможно заранее сказать, остановится ли наша программа на конкретных входных данных. Таким образом, мы были вынуждены прервать программу, когда она пыталась доказать более сильные оценки. Независимо от нас были написаны две программы для автоматических доказательств верхних оценок. Первая из них, написанная Николенко и Сироткиным [33], была разработана для доказательства верхних оценок для SAT и использует только одно правило упрощения, а именно: правило удаления чистых литералов. Этой программой было доказано, что задача SAT может быть решена за время 0(1.56639 ) алгоритмом расщепления, использующим только правило удаления чистых литералов. Другая программа была разработана Граммом и др. [20]. Этой программой было доказано несколько новых оценок для сложных задач модификации графов. Например, верхняя оценка для задачи Cluster Editing была улучшена до 0(1.92fe) (где к обозначает количество допустимых модификаций ребер). Программа Грамма и др. позволяет работать с различными правилами упрощения. Все современные программы (включая нашу) основаны на следующем простом замечании: возможно доказать верхнюю оценку для задачи, просто рассматривая все возможные подформулы размера, ограниченного некоторой константой.
Программа Грамма и др. является, в некотором смысле, непосредственной реализацией этого факта: программа, получив на вход число s, строит множество S графов на s вершинах, такое что любой возможный граф содержит в качестве подграфа хотя бы один элемент множества S. Для каждого графа множества S перебираются все возможные расщепления и выбирается то, которому соответствует наименьшее число расщепления. Наконец, как результат, выдается оценка, соответствующая максимальному из рассмотренных чисел расщепления. Ясно, что итоговая оценка тем лучше, чем больше входное число 5. Тем не менее, с увеличением числа s очень сильно растет количество возможных расщеплений графа на s вершинах (равно как и размер самого множества S). Ниже мы приводим отличия нашей программы от программы, написанной Граммом и др. 1. Наша программа сначала получает на вход оценку и после этого пытается ее доказать, в то время как программа Грамма и др. по данному числу s пытается доказать как можно лучшую оценку, рассматривая графы на s вершинах. 2. Множество возможных подформул в нашей программе строится в процессе поиска доказательства, построение же аналогичного множества в программе Грамма и др. делается на первом шаге.
Таким образом, мы никогда не знаем, остановится ли (то есть докажет ли) наша программа данную оценку. Аналогично, невозможно сказать заранее, для какого числа s (и существует ли такое s вообще) программа Грамма и др. сможет доказать данную оценку. 3. Наша программа не рассматривает все возможные расщепления для каждого класса формул (она рассматривает лишь расщепления по наборам, содержащим не более, чем две переменные), как это делает программа Грамма и др.
Решение MAX-SAT на формулах константной плотности быстрее, чем за 2N
В данном разделе мы показываем, что MAX-SAT для формул с не более чем AN дизъюнктами, где А — константа, может быть решена за время cN, где с 2 — константа. Формальное описание алгоритма для МАХ SAT приведено в алг. 7. Алгоритм сначала применяет правило чистый литерал до тех пор, пока это возможно.
После этого он расщепляет по 1)+-литералу, если такой литерал есть. Если же такого нет, алгоритм берет произвольный литерал и находит оптимальные наборы аа и а-,а для Fa и F-,a, соответственно. Поскольку Fa и F a содержат менее D дизъюнктов, это может быть сделано за полиномиальное время. Более того, можно считать, что аа и ог-,а содержат менее D литералов. Наконец, алгоритм расщепляет формулу, используя литералы одного из найденных наборов. Теорема 5.1.1. Для любой константы Л 0 найдутся константы D 0 и с 2, такие что MAXSATALG(D) выдает MC1(F) для любой формулы F с не более чем AN(F) дизъюнктами за время cN F . Доказательство. Если текущая формула F содержит 1)+-литерал, алгоритм просто расщепляет по нему. При этом в одной из веток удаляется хотя бы одна переменная и хотя бы один дизъюнкт, в другой — хотя бы одна переменная и хотя бы D дизъюнктов (напомним, что F не содержит чистых литералов). Рассмотрим теперь случай, когда F состоит только из -литералов. Н.У.О., допустим, что % + fc_,a І + a (напомним, что а является (г, -литералом). Мы утверждаем, что а- а U a ZF Qj- o U ""О- Действительно, рассмотрим произвольный полный набор (3 переменным формулы F. Из (1.6) заключаем, что в то время как из (1.7) следует, что 1. Присвоить значение True всем чистым литералам формулы F. 2. Если F содержит только дизъюнкты Т, вернуть их количество. 3. Если F содержит 1)+-литерал а, то произвести рекурсивные вызовы для F[a] и F[-ia] и вернуть максимум из полученных ответов. 4.
Пусть а — произвольный литерал F. Пусть і = d(a), j = d(- a). 5. Построить оптимальные наборы для Fa и F-,a. Обозначим их через &а = {Х\, . . . , Хр\ И а-,а = ІУІ, і Уд}, СООТВЄТСТВЄННО, И ПуСТЬ 6. Если і + fc-,a j 4- fca, то произвести рекурсивные вызовы для вернуть максимум из полученных ответов. 7. В противном случае произвести рекурсивные вызовы для вернуть максимум из полученных ответов. Таким образом, (3a--Ua выполняет хотя бы столько же дизъюнктов формулы F, сколько выполняет набор /а-аи_,а (для любого /?), из чего мы делаем вывод, что а_,а U a ZF СК-Ю U -1 . Значит, нет необходимости рассматривать расширения набора а-,0 в -ia-ветке. Тогда алгоритм может расщепить следующим образом: Если же i + fc-,0 j + ka, то аналогичным образом показывается, что aaU a b 1 оса U a- Из этого следует, что алгоритм находит верное решение. Теперь необходимо оценить время работы алгоритма. Для оценки мы используем следующую меру сложности (w — w{A) будет определено позднее): Если формула содержит D+-литерал, алгоритм расщепляет с числом расщепления не более т(1 + w, 1 + wD). В противном случае число расщепления не превосходит Г = т(1, 2,..., Z)+l) (поскольку р, q D). Возьмем теперь произвольную константу d, большую А. Допустим, что существуют константы w и Z), такие что Тогда время работы алгоритма ограничено сверху выражением где с = 2 І+Ч" 2 — константа. Ниже мы показываем, что такие константы w и D существуют. Легко видеть, что для любой константы D 1 существует константа WD 0, такая что т(1,..., D + 1) — 2T+V d (так как т(1,..., D + 1) 2). Таким образом, достаточно подобрать целое D, такое что т(1 + WD, 1 + wpD) 21+wod. Для этого достаточно показать, что (1 + wr d)2 (1 + гу )(1 + WDD) (так как т(а,Ь) 2 ). Последнее неравенство эквивалентно неравенству wDd?+2d D+l+wDD, которое, очевидно, выполнено для достаточно большого D.
