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

003467455

САНКТ-ПЕТЕРБУРГСКИЙ ГОСУДАРСТВЕННЫЙ УНИВЕРСИТЕТ

На правах рукописи

Куликов Александр Сергеевич

ПОСТРОЕНИЕ АЛГОРИТМОВ ДЛЯ ЗАДАЧ БУЛЕВОЙ ЛОГИКИ ПРИ ПОМОЩИ АВТОМАТИЗАЦИИ, КОМБИНИРОВАННЫХ МЕР СЛОЖНОСТИ И ЗАПОМИНАНИЯ ДИЗЪЮНКТОВ

05.13.17 — теоретические основы информатики

АВТОРЕФЕРАТ диссертации на соискание ученой степени кандидата физико-математических наук

Санкт-Петербург — 2009

003467455

Работа выполнена в Учреждении Российской академии наук Санкт-Петербургском отделении Математического института им. В. А. Стеклова РАН

Научный руководитель: кандидат физико-математических наук,

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

профессор Гимади Эдуард Хайрутдинович (Институт математики им. С. Л. Соболева Сибирского отделения РАН) кандидат физико-математических наук, доцент Соловьев Игорь Павлович (Санкт-Петербургский государственный университет)

Ведущая организация: Уральский государственный университет

Зо

час.

Защита диссертации состоится "7^" 2009 г. в

на заседании совета Д 212.232.51 по защите докторских и кандидатских диссертаций при Санкт-Петербургском государственном университете по адресу: 198504, Санкт-Петербург, Старый Петергоф, Университетский пр., 28.

С диссертацией можно ознакомиться в Научной библиотеке им. М. Горького Санкт-Петербургского государственного университета по адресу: 199034, Санкт-Петербург, Университетская наб., 7/9.

Автореферат разослан " " 2009 г.

Ученый секретарь диссертационного совета, доктор физ.-мат. наук,

профессор Даугавет И. К.

Общая характеристика работы

Актуальность темы. Интерес к доказательству экспоненциальных верхних оценок для №-трудных задач в последние несколько десятилетий остается на стабильно высоком уровне. Одним из наиболее хорошо изученных подходов к доказательству таких оценок является метод расщепления. Впервые данный метод был предложен в 1960-м году Дэвисом и Патнемом и сформулирован в более современном виде Дэвисом, Лоджеманном и Лавлэндом в 1962-м году. Его основная идея заключается в расщеплении входного примера задачи на несколько более простых примеров (упрощаемых в дальнейшем некоторыми правилами упрощения), таких что, построив решение для каждого из них, возможно за полиномиальное время построить решение для исходного примера. В списке ниже мы приводим некоторые верхние оценки на время решения ИР-трудных задач в наихудшем случае, доказанные методом расщепления и являющиеся наилучшими из известных (здесь и на протяжении всей работы мы опускаем полиномиальные от размера входа множители в оценках, указывая только экспоненциальную составляющую):

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

2. 1.341294к для задачи максимальной выполнимости, где К — количество дизъюнктов входной формулы (Чен и Канж, 2002);

3. 1.122463"1 для задачи о максимальном разрезе, где т — количество ребер входного графа (Скотт и Соркин, 2003);

4. 1.3289" для задачи о 3-раскрашиваемое™ графа, где п — количество вершин входного графа (Бейгель и Эпштейн, 2005).

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

Обе задачи формулируются на языке булевых формул, являющемся очень удобным для кодирования многих алгоритмических задач (таких, например, как автоматическое доказательство теорем, составление расписаний, оптимизационные задачи на графах). Задача пропозициональной выполнимости (satisfiability problem, SAT) является одной из наиболее известных NP-полных задач. Данной задаче посвящена международная ежегодная конференция (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 возникает также в задачах искусственного интеллекта и комбинаторной оптимизации.

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

выполненных оптимальным набором. В то же время известно, что в предположении P=^NP не существует полиномиального по времени алгоритма; находящего приближенное решение, сколь угодно близкое к оптимальному. Алгоритм Дандина и др. находит такое приближение, но за экспоненциальное время. Известно также много алгоритмов, решающих практические примеры задачи максимальной выполнимости. Для данных алгоритмов, однако, неизвестно никаких оценок (кроме тривиальных) на время работы в наихудшем случае.

Наряду с общей задачей максимальной выполнимости мы рассматриваем следующие ее частные случаи:

• (n,3)-MAX-SAT — вариант задачи MAX-SAT для формул, в которых каждая переменная содержится не более, чем в трех дизъюнктах;

• MAX-2-SAT — вариант задачи MAX-SAT, где каждый дизъюнкт входной формулы содержит не более двух литералов;

• (n, 3)-MAX-2-SAT — вариант задачи MAX-SAT, где каждый дизъюнкт входной формулы содержит не более двух литералов и каждая переменная входит не более, чем в три дизъюнкта.

Известно, что все перечисленные выше задачи являются NP-трудными. Таким образом, в предположении P^NP не существует полиномиальных по времени алгоритмов для данных задач. Тем не менее, поскольку подобные задачи часто возникают в практических приложениях, важно понять, какое время требуется для их решения, даже если это время экспоненциально.

Как сказано выше, лучшие известные оценки для многих NP-трудных задач получены именно методом расщепления. Простейший алгоритм расщепления для задачи выполнимости на формуле с N переменными имеет время работы порядка 2N. Первые улучшения данной оценки были получены в начале 1980-х годов Мониеном и Шпекенмейером

и Данциным для формул, длины дизъюнктов которых ограничены некоторой константой. Позднее было получено много оценок, улучшающих тривиальную для некоторых NP-полных подклассов задач выполнимости и максимальной выполнимости. Вопрос о том, могут ли данные две задачи быть решены за время с", где с < 2 — константа, до сих пор остается открытым и является одним из самых знаменитых вопросов современной теоретической информатики. Однако недавно были разработаны алгоритмы, решающие задачи выполнимости и максимальной выполнимости быстрее, чем за для формул константной плотности, то есть формул, у которых отношение количества дизъюнктов к количеству переменных ограничено сверху некоторой константой (Арвинд и Шулер, 2003; Данцин и Вольперт, 2006).

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

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

2. Разработать правило упрощения, обобщающее известные правила.

3. Построить алгоритм, решающий задачу MAX-SAT на формулах константной плотности Д в худшем случае за время с^, где с =

с(Д) < 2 — константа, с использованием лишь полиномиальной памяти.

4. Доказать новые верхние оценки для задач MAX-2-SAT и (п, 3)-MAX-2-SAT.

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

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

2. Разработано правило упрощения для задач выполнимости и максимальной выполнимости, обобщающее известные правила упрощения, присваивающие значения переменным формулы.

3. Разработан алгоритм, решающий задачу MAX-SAT на формулах константной плотности Д за время с", где с = с(Д) < 2 — константа, с использованием лишь полиномиальной памяти.

4. Доказаны следующие новые верхние оценки на время работы алгоритмов расщепления:

• где К — количество дизъюнктов входной формулы, для MAX-2-SAT;

• 2n/6-7, где N — количество дизъюнктов входной формулы, для (n, 3)-М AX-2-S AT.

Научная новизна. Алгоритмы для (п, 3)-М AX-SAT и МАХ-2-SAT являются самыми быстрыми из известных. Алгоритм для MAX-SAT, работающий на формулах константной плотности быстрее, чем 2n, является первым известным алгоритмом для данной задачи, улучшающим тривиальную оценку и при этом пользующимся лишь полиномиальной памятью. Реализованная программа для автоматического анализа алгоритмов расщепления и обобщенное правило упрощения являются первыми в своем роде.

Практическая и теоретическая ценность. Новые идеи доказательства верхних оценок на время работы алгоритмов расщепления имеют, скорее, теоретическую ценность. В то же время идеи, использующиеся для сокращения перебора случаев, могут быть применены и на практике (к примеру, в SAT-солверах).

Апробация работы. Основные результаты обсуждались на следующих конференциях и семинарах: Международная студенческая школа Estonian Winter School in Computer Science (EWSCS 2004), Эстония, 2004; Международная студенческая школа Summer School on Experimental Algorithmics, Дания, 2004; Международная конференция International Workshop on Parameterized and Exact Computation (IWPEC

2004), Норвегия, 2004; Международная конференция Eighth International Conference on Theory and Applications of Satisfiability Testing (SAT

2005), Шотландия, 2005; Международный семинар Dagstuhl Seminar on Exact Algorithms and Fixed-Parameter Tractability, Германия, 2005; Международный симпозиум Seventeenth Annual ACM-SIAM Symposium on Discrete Algorithms (SODA 2006), США, 2006; Международный симпозиум Second International Computer Science Symposium in Russia (CSR 2007), Россия, 2007; Международный семинар Dagstuhl Seminar on Moderately Exponential Algorithms, Германия, 2008; Результаты, лежащие в основе диссертации, также были доложены в Университете Торонто (Univeristy of Toronto), Университете Нью-Йорка (City University of New York) и Чешской академии наук (Czech Academy of Sciences), а также на семинаре ПОМИ

РАН. Доклад на студенческой школе в Эстонии занял первое место.

Публикации. Основные результаты диссертации опубликованы в семи работах [1, 3, 4, 6, 5, 7, 2]. Работы [1, 3, 4, 2] опубликованы в изданиях, входящих в список рекомендованных Высшей аттестационной комиссией на момент публикации. В работах [7, 2] диссертанту принадлежит новая идея использования нестандартной меры сложности для оценки времени работы алгоритмов, доказательства получены совместно с соавтором К. Куцковым. Описанные в работах [3, 4] алгоритмы и результаты принадлежат диссертанту. В работе [5] диссертантом доказана основная оценка на время работы алгоритма, сам же алгоритм разработан совместно с соавтором А. Кожевниковым.

Структура и объем диссертации. Диссертация объемом 94 страницы состоит из введения и пяти основных глав, разбитых на разделы и подразделы. Список цитируемой литературы состоит из сорока наименований.

Содержание работы

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

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

Формулы в КНФ. Пусть V — множество булевых переменных, то есть переменных, принимающих значения True и False (константы TVue и False обозначаются также 1 и 0, соответственно). Отрицание переменной v 6 V обозначается через г;. Литералом называется переменная или ее отрицание. Через var{l) мы обозначаем переменную, соответствующую литералу I. Дизъюнктом и набором называются множества литералов, не содержащие одновременно переменной и ее отрицания. Длиной дизвкжкпга называется количество содержащихся в нем литералов, ¿-дизъюнкт — это дизъюнкт длины ровно к. Формулой в конъюнктивной нормальной форме

(КНФ) называется мультимножество дизъюнктов. Формулой в Л-КНФ называется формула, содержащая только дизъюнкты длины не более к. Плотностью формулы называется отношение количества дизъюнктов к количеству переменных. Мы считаем, что формула может содержать также специальный дизъюнкт Т, который выполняется любым набором.

Полный набор — это набор значений всем переменным формулы. Мы говорим, что дизъюнкт С выполняется набором а, если С п а ф 0; дизъюнкт С опровергается набором а, если V7 б С, ->1 б а. С помощью V{a) мы обозначаем множество переменных набора а. Через C1(F, а) обозначается количество дизъюнктов формулы F, выполненных набором а, а через MC1(F) — максимальное количество одновременно выполнимых дизъюнктов (таким образом, MC1(F) = maxc C1(F, а)).

Пусть F — формула в КНФ, v — переменная F, а — набор переменным F. Наборы {«} и {->г>} мы будем записывать просто как v и -ч?. Через F[a] мы обозначаем формулу, полученную из F заменой каждого выполненного набором а дизъюнкта на дизъюнкт Т и удалением всех вхождений литералов I, таких что ->i 6 а, из оставшихся дизъюнктов.

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

Приведем два очень простых примера. Формула Fi = (х v у) Л (-а) Л (х v содержит две переменные и три дизъюнкта и является невыполнимой. Набор выполняет MC^Fj) = 2 дизъюнкта

формулы F\. Формула же Fi = (х v у) А (х v -ту), очевидно, выполнима.

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

после чего производит рекурсивные вызовы для нескольких формул вида F[ai], ..., jF[ar], где ai,...,aT суть наборы значений переменным F. Таким образом, работу алгоритма расщепления можно рассматривать как дерево, вершины которого помечены формулами в КНФ. Каждой формуле F такого дерева мы приписываем неотрицательное вещественное число p{F), обозначающее сложность F. Стандартными мерами сложности формул являются следующие: /x(F) = N{F) — количество переменных F\ /i(F) = K(F) — количество дизъюнктов F; fi(F) = L(F) — длина (то есть общее количество литералов) F. Дерево является деревом расщепления, если сложность формулы каждой вершины строго больше сложности каждой из формул, которыми помечены сыновья этой вершины.

Рассмотрим вершину дерева расщепления, помеченную формулой Fo. Пусть ее сыновья помечены формулами Fu F2, ■.., FT. Вектор (¿x, ¿2, ■ • •, tr) € R>0 называется вектором расщепления данной вершины, если ti > /i(Fo) — n(F{) для всех i — 1,...,г. Характеристический многочлен данного вектора расщепления определяется следующим образом: h(x) = 1 — Yll=i х~и ■ Единственный положительный корень этого многочлена называется числом расщепления и обозначается через r(íi, ¿2,..., tr) (несложно видеть, что при положительных х функция h(x) монотонно возрастает от —оо к 1). Числом расщепления дерева называется максимальное из чисел расщепления всех его вершин.

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

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

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

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

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

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

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

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

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

В четвертой главе представляется программа для автоматического

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

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

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

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

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

Для доказательства верхних оценок на время работы алгоритма расщепления сперва фиксируется некоторая мера сложности формул, после чего показывается, что алгоритм всегда расщепляет входную •формулу на несколько формул, сложности которых меньше сложности исходной формулы. Естественными мерами сложности формул являются количество переменных N, количество дизъюнктов К и длина формулы L. Известно большое количество верхних оценок относительно этих мер для задач SAT и MAX-SAT и их частных случаев. В данной работе мы используем комбинированные меры сложности для доказательства новых оценок для MAX-SAT и MAX-2-SAT. Наша мера сложности для

Алгоритм 1 MaxSatAlg

Вход: КНФ формула F

Параметры: положительное целое число D

Метод:

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

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

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

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

5. Построить оптимальные наборы для Fa и F~,a. Обозначим их через аа = {xi,..., хр} и а-,а " {уь ■ • •, Уд}, соответственно, и пусть

ка = МС1(Р„) = C1 (F, о»), к^ = MCI(F^) = C1 (F, а^) .

6. Если i + к~,а > j + ка, то произвести рекурсивные вызовы для

F[a], F[-ia, Fb<x, yu • • •, ^ba, yu..., yq-1, ->y?] и вернуть максимум из полученных ответов.

7. В противном случае произвести рекурсивные вызовы для

F[-ia], F[a, -.xi], F[a, xu ->x2],..., F[a, xu..., xp_b mp] и вернуть максимум из полученных ответов.

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

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

Публикации автора по теме диссертации

[1] Куликов А. С. Верхняя оценка 0(2°-16254п) для точной 3-выполнимости: более простое доказательство // Записки научных семинаров ПОМИ. 2002. Т. 293. С. 118-128.

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

[3] Куликов А. С., Федин С. С. Решение задачи о максимальном разрезе за время 2'£1/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. 194204.

Тиражирование и брошюровка выполнены в учреждении

«Университетские телекоммуникации»

197101, Санкт-Петербург, Саблинская ул., 14

Тел. (812) 233 4669 объем 1 п.л.

Тираж 100 экз.

Введение

1 Определения

1.1 Задачи булевой логики.

1.1.1 Формулы в КНФ.

1.1.2 Задачи выполнимости и максимальной выполнимости

1.2 Алгоритм расщепления.

1.3 Анализ алгоритмов расщепления.

1.4 Класс формул.

2 Методы доказательства верхних оценок, использующиеся в работе

2.1 Пример простого алгоритма расщепления.

2.2 Общее правило упрощения.

2.3 Автоматический анализ сложности алгоритмов расщепления

2.4 Комбинированные меры сложности

2.5 Запоминание дизъюнктов.

3 Автоматическое порождение правил упрощения

3.1 Известные правила упрощения для SAT и MAX-SAT

3.2 Общее правило упрощения.

3.3 Алгоритм для (n, 3)-MAX-SAT.

4 Автоматический анализ времени работы

4.1 Описание программы

4.1.1 Входные и выходные данные.

4.1.2 Алгоритм построения доказательства.

4.1.3 Детали реализации.

4.1.4 Правила упрощения.

4.1.5 Правило расщепления.

4.1.6 Мера сложности.

4.1.7 Инвариант.

4.2 Автоматически доказанные верхние оценки.

4.3 Подобные работы.

5 Комбинированные меры сложности и запоминание дизъюнктов

5.1 Решение MAX-SAT на формулах константной плотности быстрее, чем за 2м.

5.2 Алгоритм для MAX-2-SAT.

5.2.1 Правила упрощения.

5.2.2 Правила расщепления.

5.2.3 Алгоритм для MAX-2-SAT.

5.2.4 (n, 3)-М AX-2-SAT.

Интерес к доказательству экспоненциальных верхних оценок для КР-трудных задач в последние несколько десятилетий остается на стабильно высоком уровне. Одним из наиболее хорошо изученных подходов к доказательству таких оценок является метод расщепления. Впервые данный метод был предложен в 1960-м году Дэвисом и Патнемом [19] и сформулирован в более современном виде Дэвисом, Лоджеманном и Лавлэндом [18] в 1962-м году. Его основная идея заключается в расщеплении входного примера задачи на несколько более простых примеров (упрощаемых в дальнейшем некоторыми правилами упрощения), таких что, построив решение для каждого из них, возможно за полиномиальное время построить решение для исходного примера. В списке ниже мы приводим некоторые верхние оценки на время решения ЫР-трудных задач в наихудшем случае, доказанные методом расщепления и являющиеся наилучшими из известных (здесь и на протяжении всей работы мы опускаем полиномиальные от размера входа множители в оценках, указывая только экспоненциальную составляющую):

1. 1.0741, для задачи пропозициональной выполнимости формул в КНФ, где Ь — длина (то есть общее количество литералов) входной формулы [23];

2. 1.341294^ для задачи максимальной выполнимости, где К — количество дизъюнктов входной формулы [14];

3. 1.122463™ для задачи о максимальном разрезе, где т — количество ребер входного графа [36];

4. 1.328971 для задачи о З-раскрашиваемости графа, где п — количество вершин входного графа [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, где каждый дизъюнкт входной формулы содержит не более двух литералов;

• (п, 3)-MAX-2-SAT — вариант задачи MAX-SAT, где каждый дизъюнкт входной формулы содержит не более двух литералов и каждая переменная входит не более, чем в три дизъюнкта.

Известно, что все перечисленные выше задачи являются NP-трудными (доказательство NP-трудности задачи (п, 3)-MAX-2-SAT см., например, в [34]). Таким образом, в предположении P^NP не существует полиномиальных по времени алгоритмов для данных задач. Тем не менее, поскольку подобные задачи часто возникают в практических приложениях, важно понять, какое время требуется для их решения, даже если это время экспоненциально.

Как сказано выше, лучшие известные оценки для многих NP-трудных задач получены именно методом расщепления. Простейший алгоритм расщепления для задачи выполнимости на формуле с N переменными имеет время работы порядка 2N. Первые улучшения данной оценки были получены в начале 1980-х годов Мониеном и Шпекенмейером [30] и Данциным [2] для формул, длины дизъюнктов которых ограничены некоторой константой. Позднее было получено много оценок, улучшающих тривиальную для некоторых МР-полных подклассов задач выполнимости и максимальной выполнимости. Вопрос о том, могут ли данные две задачи быть решены за время с^, где с < 2 — константа, до сих пор остается открытым и является одним из самых знаменитых вопросов современной теоретической информатики. Однако недавно были разработаны алгоритмы, решающие задачи выполнимости и максимальной выполнимости быстрее, чем за для формул константной плотности, то есть формул, у которых отношение количества дизъюнктов к количеству переменных ограничено сверху некоторой константой [7, 16].

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

Основные результаты работы перечислены ниже.

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

2. Разработано правило упрощения для задач выполнимости и максимальной выполнимости, обобщающее известные правила упрощения, присваивающие значения переменным формулы.

3. Разработан алгоритм, решающий задачу MAX-SAT на формулах константной плотности А за время cN, где с = с(Д) < 2 — константа, с использованием лишь полиномиальной памяти.

4. Доказаны следующие новые верхние оценки на время работы алгоритмов расщепления:

• 2к/61 где К — количество дизъюнктов входной формулы, для MAX-2-SAT;

• 2ЛГ/6"7, где N — количество дизъюнктов входной формулы, для (n, 3)-MAX-2-SAT.

Алгоритмы для (n, 3)-MAX-SAT и MAX-2-SAT являются самыми быстрыми из известных. Алгоритм для MAX-SAT, работающий на формулах константной плотности быстрее, чем 2N, является первым известным алгоритмом для данной задачи, улучшающим тривиальную оценку и при этом пользующимся лишь полиномиальной памятью. Реализованная программа для автоматического анализа алгоритмов расщепления и обобщенное правило упрощения являются первыми в своем роде.

Основные результаты диссертации опубликованы в семи работах [3, 5, 6, 25, 24, 26, 4].

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

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

3. Куликов А. С. Верхняя оценка О(20 16254п) для точной 3-выполнимости: более простое доказательство // Записки научных семинаров ПОМИ. 2002. Т. 293. С. 118-128.

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

5. Куликов А. С., Федин С. С. Решение задачи о максимальном разрезе за время 21-Б1/4 // Записки научных семинаров ПОМИ. 2002. Т. 293. С. 129-138.

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

7. Arvind V., Schuler R. The quantum query complexity of 0-1 knapsack and associated claw problems // Proceedings of the 14th Annual International Symposium on Algorithms and Computation. Vol. 2906 of Lecture Notes in Computer Science. 2003. P. 168-177.

8. Asano T., Hori K., Ono T., Hirata T. A theoretical framework for hybrid approaches to MAX SAT // Proceedings of the 8th International Symposium on Algorithms and Computation. Vol. 1350 of Lecture Notes in Computer Science. 1997. P. 153-162.

9. Bansal N., Raman V. Upper Bounds for MaxSat: Further Improved // Proceedings of ISAAC'99. Vol. 1741 of Lecture Notes in Computer Science. 1999. P. 247-258.

10. Battiti R., Protasi M. Reactive search, a history-base heuristic for MAXSAT // ACM Journal of Experimental Algorithmics. 1997. Vol. 2.

11. Beame P., Impagliazzo R., Pitassi T., Segerlind N. Memoization and DPLL: formula caching proof systems // Proceedings of 18th IEEE Annual Conference on Computational Complexity. 2003. P. 248-259.

12. Beigel R., Eppstein D. 3-coloring in time 0(1.3289n) // Journal of Algorithms. 2005. Vol. 54, N. 2. P. 168-204.

13. Borchers B., Furman J. A two-phase exact algroithm for MAX-SAT and weighted MAX-SAT problems // Journal of Combinatorial Optimization. 1999. Vol. 2, N. 4. P. 299-306.

14. Chen J., Kanj I. Improved exact algorithms for MAX-SAT // Proceedings of the 5th LATIN. Vol. 2286 of Lecture Notes in Computer Science. 2002. P. 341-355.

15. Crescenzi P., Kann V. How to find the best approximation results — a follow-up to Garey and Johnson // ACM SIGACT News. 1998. Vol. 29, N. 4. P. 90-97.

16. Dantsin E. Y., Hirsch E. A., Gavrilovich M. R., Konev B. Y. MAX SAT approximation beyond the limits of polynomial-time approximation // Annals of Pure and Applied Logic. 2001. Vol. 113, N. 1-3. P. 81-94.

17. Davis M., Logemann G., Loveland D. A machine program for theorem proving 11 Comm. ACM. 1962. Vol. 5. P. 394-397.

18. Davis M., Putnam H. A computing procedure for quantification theory // J. Assoc. Comp. Mach. 1960. Vol. 7. P. 201-215.

19. Gramm J., Guo J., Hiiffner F., Niedermeier B. Automated Generation of Search Tree Algorithms for Hard Graph Modification Problems // Algorithmica. 2002. Vol. 39, N. 4. P. 321-347.

20. Gramm J., Hirsch E. A., Niedermeier R., Rossmanith P. Worst-case upper bounds for MAX-2-SAT with an application to MAX-CUT // Discrete Applied Mathematics. 2003. Vol. 130, N. 2. P. 139-155.

21. Hansen P., Jaumard B. Algorithms for the maximum satisfiability problem 11 Computing. 1990. Vol. 44. P. 279-303.

22. Hirsch E. A. New Worst-Case Upper Bounds for SAT // Journal of Automated Reasoning. 2000. Vol. 24, N. 4. P. 397-420.

23. 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.

24. 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.

25. 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.

26. Kullmann 0. New methods for 3-SAT decision and worst-case analysis // Theoretical Computer Science. 1997. Vol. 223. P. 1-72.

27. Kullmann O., Luckhardt H. Algorithms for SAT/TAUT decision based on various measures. Preprint. 1998.

28. Marques-Silva J., Sakallah K. GRASP: a search algorithm for prepositional satisfiability // IEEE Transactionon Computers. 1999. Vol. 48, N. 5. P. 506-521.

29. Monien B., Speckenmeyer E. Solving satisfiability in less than 2n steps // Discrete Applied Mathematics. 1985. Vol. 10. P. 287-295.

30. Moskewicz M., Madigan C., Zhao Y., Zhang L., Malik S. Chaff: engineering- an efficient SAT solver // Proceedings of the 38th Design Automation Conference. 2001. P. 530-535.

31. Niedermeier R., Rossmanith P. New upper bounds for Maximum Satisfiability // Journal of Algorithms. 2000. Vol. 36. P. 63-88.

32. Nikolenko S. I., Sirotkin A. V. Worst-case upper bounds for SAT: automated proof // Proceedings of the 8th ESSLLI Student Session. 2003. P. 225-232.

33. Raman V., Ravikumar B., Srinivasa Rao S. A simplified NP-complete MAXSAT problem // Information Processing Letters. 1998. Vol. 65, N. 1. P. 1-6.

34. Robson J. Algorithms for maximum independent sets // Journal of Algorithms. 1986. Vol. 7, N. 3. P. 425-440.

35. Wallace R. J. Enhancing maximum satisfiability algorithms with pure literal strategies // Proceedings of the 11th Canadian Conference on Artificial Intelligence. Vol. 1081 of Lecture Notes in Computer Science. 1996. P. 388-401.

36. Williams R. On Computing A;-CNF Formula Properties // Proceedings of the 6th International Conference on Theory and Applications of Satisfiability Testing. Vol. 2919 of Lecture Notes in Computer Science. 2003. P. 330-340.

37. Yagiura M., Ibaraki T. Efficient 2 and 3-flip neighborhood search algorithms for MAX SAT // Proceedings of the Fourth Annual International Computing and Combinatorics Conference. Vol. 1449 of Lecture Notes in Computer Science. 1998. P. 105-116.

38. Zhang H. SATO: An Efficient Propositional Prover // Proceedings of the 14th International Conference on Automated Deduction. Vol. 1249 of Lecture Notes in Computer Science. 1997. P. 272-275.