Сложность пропозициональной логики

Основные определения и обозначения.

Определение 1. Формулы логики высказываний (пропозициональной логики) — это элементы минимального множества, удовлетворяющего следующим условиям:

• логические константы false и true — формулы,.

• пропозициональные переменные — формулы,.

• результат применения логической связки к формулам — формула.

Формулы могут быть построены для различных наборов логических связокнабор логических связок, используемый для построения формул, называется базисом. В данной диссертации в основном используются два базиса: базис, составленный из унарной операции отрицанияп и бинарных дизъюнкции V и конъюнкции Л, и базис, составленный из отрицания и бинарной операции импликации D. Мы будем придерживаться стандартных обозначений и опускать скобки, когда приоритет операций ясен или порядок операций несуществен.

Определение 2. Формула в конъюнктивной нормальной форме (КНФ) представляет собой конъюнкцию, каждый из членов которой является дизъюнкцией литераловвсякий литерал является либо пропозициональной переменной, либо отрицанием таковой.

Дизъюнкция, состоящая ровно из к литералов, называется к-дизъюнщией. Формулой в к-КНФ называется формула, все дизъюнкции которой являются г-дизъюнкциями при г ^ к.

Определение 3. Формула в дизъюнктивной нормальной форме (ДНФ) представляет собой дизъюнкцию, каждый из членов которой является конъюнкцией литералов.

Конъюнкция, состоящая ровно из к литералов, называется к-конъюнкцией. В этом случае к называется длиной конъюнкции. Формулой в к-ДНФ называется формула, все конъюнкции которой являются г-конъюнкциями при г ^ к.

Определение 4. Набором значений переменных (или, для краткости, па-бором) называется множество пар вида (v, b), где v — пропозициональная переменная, b € {false, true} — логическое значение (иногда false обозначается как 0, a true — как 1) — в этом множестве пар одна и та же переменная не может встречаться дважды.

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

Определение 5. Результат подстановки набора, А в формулу F обозначается как F [А] и представляет собой формулу, полученную из формулы F присваиванием значений из набора соответствующим переменным. Если набор даёт значения нескольким переменным, все они могут быть перечислены в квадратных скобках как F[v = &i, vi = ?"2, • • •]• Иногда мы будем писать в наборе присваивание I = b для литерала I, имея в виду, что если I — переменная, то она получает значение b, а если отрицание переменной — то соответствующая переменная получает значениеФ.

В случае, когда нам будет важно представление формулы в КНФ, подстановка значения true переменной х производится удалением всех дизъюнкций. содержащих х без отрицания, и удалением литерала -*х из оставшихся дизъюнкций. Аналогично подстановка значения false производится удалением всех дизъюнкций, содержащих ->х, и удалением положительного литерала х из оставшихся дизъюнкций.

Определение 6. Набор, в результате подстановки которого формула (в частности, дизъюнкция литералов) обращается в тождественно истинную, называется выполняющимнабор, в результате подстановки которого формула обращается в тождественно ложную формулу, называется опровергающим.

Формула, для которой существует хотя бы один выполняющий набор, называется выполнимойязык, состоящий из всех выполнимых формул в конъюнктивной нормальной форме, обозначается SATязык, состоящий из всех выполнимых формул в /с-КНФ, обозначается /c-SAT.

Формула, для которой не существует ни одного опровергающего набора, называется тавтологией.

Определение 7. Результат подстановки одного набора В в другой набор, А обозначается через А[5]- он представляет собой набор А, в котором значения переменных, имеющихся только в В, добавлены к Л, а значения переменных, имеющихся в обоих наборах, заменены на те, что имеются в В. Формальное определение таково:

А[В] = {О, b) (v, b) eBv (0, b) е, А л (v, -.Ь)? в))}.

При необходимости наборы и формулы кодируются каким угодно разумным образом в виде битовых строк.

Актуальность темы

и исторический обзор

Сложность задач пропозициональной логики является важной тематикой в теории сложности вычислений и доказательств, составляющей важную область математической логики. Более сорока лет назад независимо С. А. Куком и Л. А. Левиным [22, 3] было предложено понятие NP-полноты, оказавшееся ключевым для современной теории сложности. В 1971 г. С. А. Куком [22] была доказана NP-полнота задачи выполнимости формул логики высказываний, а затем С. А. Кук и Р. А. Рекхоу [23] определили понятие пропозициональной системы доказательств. Последние несколько десятилетий теоретические исследования по оценкам сложности этой задачи велись в двух основных направлениях:

1) построение новых систем пропозициональных доказательств, анализ отношений моделируемости между ними, построение в них эффективных доказательств важных семейств тавтологий, доказательство нижних оценок сложности для этих систем (см. [5, 4, 9, 16, 43, 61, 63, 78, 77, 89] и др-);

2) построение новых алгоритмов для задачи выполнимости пропозициональных формул и связанных с ней задач, доказательство верхних оценок на время их работы (см. [2, 46, 64, 74, 75, 83, 84] и другие ссылки в обзорах [29, 49]).

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

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

Самая известная система доказательств — метод резолюций, восходящий к работам П. С. Порецкого конца XIX века, — имеет непосредственное отношение к алгоритмам, использующим метод расщепления задачи. Хотя большинство применяемых на практике алгоритмов принадлежит к этому классу, первые суперполиномиальные нижние оценки на размер вывода для различных вариантов метода резолюций (из которых следуют нижние оценки на время работы таких алгоритмов) были получены Г. С. Цейтиным [4] для формул, основанных на раскраске рёбер графа в два цвета, ещё в 1960;х гг. (затем они были обобщены и усилены А. Хакеном [43] для пропозиционального принципа Дирихле и А. Уркхартом [89] для формул, аналогичных [4], но построенных на графах-расширителях). Поэтому построение систем доказательств и алгоритмов, основанных на других принципах, является актуальной задачей, важной не только в контексте поиска новых подходов к доказательству нижних оценок сложности, но и для расширения круга задач, которые могут быть решены реализациями алгоритмов на практике.

Наиболее привычными системами доказательств являются системы Фре-ге, названные в честь Готлоба Фреге, который, однако, в своей монографии [32] использовал более общие системы, включающие правило подстановкисчитается, что первым такие системы без правила подстановки использовал Джон фон Нейман [90]. Экспоненциальных нижних оценок для них не известно и по сей деньоднако известны такие оценки для систем, промежуточных между системами Фреге и резолюций: систем Фреге ограниченной глубины [63. 77] и обобщения метода резолюций для формул, являющихся конъюнкциями формул в &—ДНФ [5]. Все системы Фреге эквивалентны, как доказано в диссертации Р. А. Рекхоу [81], и эквивалентны (по их определению) пропозициональному фрагменту генценовского секвенциального исчисления (с правилом сечения). Они обладают определёнными возможностями рассуждений о целых числах (представленных при помощи векторов пропозициональных переменных) — например, имеют полиномиального размера (хоть и технически непростые) доказательства пропозиционального принципа Дирихле [14].

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

Алгебраические системы. Эти системы основаны на слабой теореме Гильберта о нулях: переведём исходную формулу в систему полиномов, не имеющих общих корней в алгебраически замкнутом поле, если исходная формула была тавтологиейтогда доказать тавтологичность формулы можно, показав, что единица лежит в идеале, порождённом этими полиномами. Эти системы были предложены в работах [9, 20], где приводятся система Nullstellensatz и полиномиальное исчисление. Экспоненциальные нижние оценки для этих двух систем были показаны в серии работ [80, 15, 57]. Обобщения алгебраических систем, в которых полиномы могут быть записаны произвольными алгебраическими формулами, были кратко рассмотрены в работах Т. Питасси [76] (с вероятностной проверкой корректности доказательства) и П. Бима и др. [16] (под названием «equational logic»).

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

Первые такие системы берут начало из исследований по целочисленной линейной оптимизации. Система секущих плоскостей использует правило округления (тот факт, что для целого числа х неравенство х ^ г влечёт неравенство х ^ [г]) — её полнота была доказана Е. Гомори [34], далее она подробно изучалась В. Хваталом [19] в контексте целочисленного линейного программирования, а как пропозициональная система она была впервые использована в работе У. Кука, К. Р. Кулларда и Г. Турана [24]. Экспоненциальная нижняя оценка для неё была доказана П. Пудлаком [78]. Другой способ обеспечить принадлежность решений множеству {0,1} — использовать квадратичные неравенстватакие системы берут начало из работы Л. Ловаса и А. Схрайвера [68] (полнота более простой системы доказательств, использующей правило «поднять-и-спроектировать», доказана в работе Е. Баласа, С. Кериа и Г. Корнуеолса [8]). Во всех этих системах пропозициональный принцип Дирихле имеет короткие доказательства [79]. В данной диссертации рассматриваются обобщения систем Ловаса-Схрайвера на многочлены большей степениэти обобщения были введены в работе [38].

К другому типу полуалгебраических систем относятся система Positivstellensatz и РозШу81е11еп8а1г-исчисление, берущие начало от работы Х. Ломбарди, Н. Мнёва и М.-Ф.Руа [66] и введённые как пропозициональные системы в работе Д. Григорьева и Н. Воробьёва [41]. Хотя фактически для полноты их пропозиционального варианта достаточно слабой теоремы Гильберта о нулях, размер вывода существенно уменьшается за счёт использования неравенств и аксиом, постулирующих неотрицательность квадрата любого полинома. Нижние оценки на степень вывода в этих системах доказаны Д. Григорьевым в [36], однако они не приводят непосредственно к экспоненциальным нижним оценкам на размер вывода.

Наконец, Я. Крайчеком [61] были предложены системы, комбинирующие секвенциальный вывод с использованием неравенств.

Алгоритмы для задач пропозициональной логики.

Поскольку задача пропозициональной выполнимости NP-полна, маловероятно, что она может быть решена за полиномиальное время. Тем не менее, важно понять, какое время требуется для её решения, даже если это время экспоненциально: алгоритм, решающий SAT, скажем, за время 2П/1000. был бы весьма полезен для многих приложений, например для современных задач разработки микросхем.

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

Алгоритмы, использующие метод расщепления. Многие алгоритмы для SAT используют расщепление. Такой алгоритм сводит задачу для входной формулы F к задаче для полиномиального числа формул F,., Fp. Это сведение может быть детерминированным (рекурсивно вызывать алгоритм для каждой из формул Fi) или вероятностным (случайно выбирать одну из формул Fi). Естественно разделить современные расщепляющие алгоритмы на два семейства: классические (DPLL) алгоритмы и алгоритмы, основанные на лемме о кодировании случайного набора.

DPLL-алгоритмы основаны на процедурах, описанных в работах Дэвиса и Патнема [31] и Дэвиса, Лоджмана и Лавлэнда [30]. Грубо говоря, такой алгоритм заменяет входную формулу F двумя формулами F[x] и F[-ix], полученными присваиванием некоторой переменной х значений true и false соответственно. Затем алгоритм упрощает каждую из полученных формул и рекурсивно вызывает процедуру для каждой из упрощенных формул. Переменная для расщепления на каждом шаге выбирается обычно с учётом лишь локальных" свойств формулы. В разных ветвях дерева расщепления переменные выбираются независимо (исключением являются экспериментальные алгоритмы, использующие метод запоминания конфликтов [69]). Основным методом анализа таких алгоритмов являются рекуррентные соотношения для количества листьев в дереве рекурсии. Используя этот метод, Е. Я. Данцин [2] и Б. Мониен и Э. Шпекенмейер [70] получили первые нетривиальные верхние оценки для /с-БАТ.

В настоящее время методом, близким к данному, получены наилучшие оценки для задачи выполнимости формул в конъюнктивной нормальной форме [17] (см. также [29]). Также этот метод является наиболее популярным среди методов, используемых для построения экспериментальных алгоритмов (см., например, обзор в [87]).

Алгоритмы, основанные на лемме о кодировании выполняющего набора были предложены Патури, Пудлаком, Саксом и Зейном [75, 74]. Главное отличие этих алгоритмов от БРЬЪ-алгоритмов заключается в том, что для них важен порядок, в котором переменные выбираются для присваивания, и этот порядок не может быть определён по формуле, как для БРЬЬ-алгоритмовпоэтому либо упорядочение переменных, выбираемых для присваивания, берётся случайным образом, либо (для детерминированного варианта) перебираются все перестановки из некоторого семейства с подходящими свойствами (не зависящими от конкретной формулы). Анализ основан не на локальных (как для ОРЬЬ-алгоритмов), а на глобальных рассуждениях, например оценке количества переменных, которые никогда не используются для рекурсивных вызовов, поскольку удаляются во время упрощения. Для этих алгоритмов более простыми являются их вероятностные варианты, когда и упорядочение переменных, и значение переменной на каждом шаге выбираются случайным образом, а вместо возврата из рекурсии используется новый запуск алгоритма с самого начала.

Алгоритмы, основанные на локальном поиске. Другим методом решения задачи выполнимости является метод локального поиска, использованный У. Шонингом в [83].

Имеется большое семейство алгоритмов, решающих эту задачу при помощи локального поиска (обзор см., например, в [42]). Типичный алгоритм, основанный на локальном поиске, берет начальный набор и изменяет его шаг за шагом, пытаясь приблизиться к выполняющему набору, то есть сократить количество переменных, значения которых в текущем наборе и в выполняющем различаются. Если после определенного количества шагов выполняющий набор не найден, алгоритм порождает другой начальный набор и опять изменяет его шаг за шагом. Число таких попыток ограниченоесли ни в одной из них не удается найти выполняющий набор, алгоритм заканчивает работу, с ответом «не найдено» .

Методы изменения наборов разнообразны. Например, э/садные алгоритмы (напр. [60, 86]) выбирают переменную и изменяют ее значение в текущем наборе на противоположное, так чтобы значение некоторой функции от набора (например, число дизъюнкций, которые он выполняет) возрастало как можно сильнее. Другой метод используется в алгоритмах, основанных на случайных блуоюданиях [73]. Такой алгоритм изменяет на противоположное значение переменной, выбранной случайно из невыполненной дизъюнкции. Сложность алгоритмов, основанных на случайных блужданиях, можно оценить, используя их связь с одномерными случайными блужданиями. Основные результаты в области верхних оценок для этих алгоритмов принадлежат Пападимитриу [73] и Шонингу [83]. Как показано в [73], 2-БАТ может быть решена алгоритмом, основанным на случайных блужданиях, за полиномиальное время. В работе [83] показано, что /с-БАТ может быть решена алгоритмом, основанным на случайных блужданиях, за время (2 — 2/к)п с точностью до полиномиального сомножителя.

Алгоритмы для других задач пропозициональной логики. Исследования в области верхних оценок в наихудшем случае для трудных задач не ограничиваются SAT. В частности, обобщением SAT является задача максимальной выполнимости, в которой требуется не только найти набор, выполняющий все дизъюнкции входной формулы, если он имеется, но и набор, выполняющий максимально возможное количество дизъюнкций, если выполняющего набора нет. Для этой задачи применяются методы, похожие на методы для задачи SAT. В особенности популярны DPLL-алгоритмы (см., например, [72]), однако специфика задачи требует соответствующей модификации этих методов (в частности, правил эквивалентных преобразований формул).

Известно, что степень полиномиального по времени приближения для некоторых трудных задач имеет некоторые границы в предположении, что Р ^ NP (см., например, [6]). В частности, для задачи максимальной выполнимости для формул в 3-КНФ не существует полиномиального алгоритма (если Р NP), который находил бы набор, выполняющий ^ (| + е) М клозов, где М — максимально возможное число одновременно выполнимых клозов, а б > 0 — сколь угодно малое число. Однако существуют алгоритмы [25], которые находят такие приближенные решения быстрее, чем наилучшие на данный момент алгоритмы находят точные решения.

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

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

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

Алгебраические системы. В диссертации рассматриваются две формульные алгебраические системы: вариант полиномиального исчисления Р-РС и вариант системы Ми1^е11епза1г Р-^, допускающие запись полиномов произвольными алгебраическими формулами. Для проверки эквивалентности различных записей одного и того же полинома используются правила упрощения, повторяющие аксиомы кольца. Система, аналогичная системе Р-РС ранее кратко рассматривалась в [16]- система Р-^ ранее не рассматривалась. Доказывается следующая теорема о полиномиальной эквивалентности системы Р-МЭ и древесного вывода в системе Р-РС.

Теорема 1.2. Система Р-^ полиномиально моделирует древесный вариант системы Р-РС.

Также приводится короткое и простое доказательство пропозиционального принципа Дирихле (в Р-РС или Р-^), использующее лишь формулы ограниченной степени (в отличие от систем Фреге, где короткое и технически трудное доказательство этих тавтологий [14] использует формулы неограниченной степени).

Приводимые в диссертации результаты об алгебраических системах опубликованы в работе [37]. После того, как эта работа была опубликована, И. Цамерет [88] предложил ослабить систему Р-РС, ограничив её строки некоммутативными формуламикак показано в его работе, в результате получается система, полиномиально эквивалентная системе Р-РС.

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

В частности, доказаны экспоненциальные нижние оценки на размер доказательств системы неравенств, известной как симметричная задача о рюкзаке, или задача о сумме подмножества т — Х — Х2 — ¦ ¦. — хп = 0 (где т? 2,), (1−57) в статических вариантах систем доказательств Ловаса-Схрайвера и в Positivstellensatz-иcчиcлeнии (точные определения выводов в этих и других полуалгебраических системах приводятся в разделе 1.1.4).

Теорема 1.9. При т = (2п + 1)/4 количество мономов в любом доказательстве (1.57) в Positivstellensatz-иcчиcлeнии составляет (следовательно, размер такого доказательства экспоненциален).

Следствие 1.7. При т = (2п + 1)/4 размер всякого статического доказательства в для системы неравенств (1−57) составляет.

Следствием последнего результата является также экспоненциальная оценка на размер древесного вывода противоречия из этой системы неравенств в двух нестатических системах — системе Ловаса-Схрайвера с использованием неотрицательности квадратов и обобщении системы Ловаса-Схрайвера на полиномы произвольной степени ЬЭ00.

С другой стороны, система неравенств (1.57) имеет короткие доказательства в системах ЬБ3 и Ь8зрщэтот факт является простым следствием следующей леммы.

Лемма 1.7. Пусть.

•У = ЕГ= 1 агхг,.

• МУ) = (У-((1−1)){У-.

• аг — целочисленные константы,.

• Х{ — переменные.

Тогда существует вывод неравенства ¡-¿-(У) ^ 0 (из аксиом) размера, полиномиального от с?, п и тах^ |аг|, в системах.

1. ЬБ3,.

2. ЬБдр!^, причём правило введения отрицания применяется только к переменным.

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

Д Д (1-же) = 0, (1.59) где V пробегает все вершины некоторого графа, а пробегает все подмножества чётной мощности множества рёбер, инцидентных V.

Теорема 1.7. Для каждой константы ^ 1 и каждого ¿—регулярного графа С в системе ЬБ^" 1″ 2 имеется полиномиального размера вывод противоречия из формул (1.59).

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

Теорема 1.4. Существует множество неравенств, для которого имеется полиномиального размера вывод противоречия в системах ЬБ4 и ЬЭ + СР2, но любой вывод противоречия в системе СР содержит экспоненциальное количество шагов.

Системы, использующие линейные неравенства, также рассматриваются в диссертации. Показано, что система секущих плоскостей с ограничением на степень ложности неравенств полиномиально моделируется методом резолюций. Также рассматриваются секвенциальные расширения этих систем. (Секвенциальное расширение системы X обозначается Я (Х).) Именно, для системы секущих плоскостей СР, системы «поднять-и-спроектировать» Ъ&Р и их общей неполной подсистемы ЬР, основанной на линейном программировании, доказывается эквивалентность в случае, когда коэффициенты записываются в унарной системе счисления (соответствующие системы обозначаются индексом 1, например Я (СР1)).

Теорема 1.11. Я (ЬР) полиномиально моделирует ЩЬ&Р). Это моделирование также имеет место, если коэффициенты записываются в унарной системе счисления.

Теорема 1.12. Если имеется вывод полиномиального размера в системе ЩСРх) строки доказательства Р из множества строк {Сдг}1£1, то имеется и вывод полиномиального размера в системе ЩЬРх) строки Р/ Г из множества строк {(2г V Г}ге1.

Приводимые в диссертации результаты о полуалгебраических системах опубликованы в работах [38] и [53], а также в работах [39, 40, 54]. После того, как эти работы были опубликованы, П. Бим, Т. Питасси и Н. Сегерлинд [10] нашли пропозициональную формулу, для которой экспоненциальная нижняя оценка имеет место для всех древесных систем доказательств, строки которых являются полиномиальными неравенствами ограниченной степениони доказали этот результат в предположении о коммуникационной сложности с несколькими участниками для задачи дизъюнктности множеств, их предположение было затем доказано в работах А. Чаттопадхяя и А. Ада [18] и Т. Ли и А. Шрайбмана [65].

Алгоритмы для задач пропозициональной логики.

Алгоритмы для задачи выполнимости формул в конъюнктивной нормальной форме. В диссертации предлагается детерминированный алгоритм, решающий задачу выполнимости для формул в /с-КНФ за время 0((2 — -щ + е) п) с использованием памяти полиномиального размера.

Теорема 2.1. Для любого е > 0 существует алгоритм, который для любого целого числа к и любой входной формулы I71 в /с-КНФ от п переменных он корректно решает задачу выполнимости для формулы заканчивает свою работу за время О ((2 — + е) п) и использует память полиномиального размера.

Этот алгоритм является частичной дерандомизацией алгоритма локального поиска, предложенного У. Шонингом [83]. Он состоит из конструкции множества начальных наборов и алгоритма, частично дерандомизирующего случайное блуждание по множеству наборов, начинающееся с конкретного набора. Последний алгоритм улучшен для случая формул в 3-КНФ.

Теорема 2.2. Существует алгоритм, который для любой входной формулы ^ в 3-КНФ от п переменных корректно решает задачу выполнимости, заканчивает свою работу за время 0(1.481п) и использует память полиномиального размера.

Константы, используемые в асимптотических оценках этих алгоритмов, весьма велики и делают алгоритмы непригодными для практической реализации. С практической точки зрения исходный вероятностный алгоритм Шо-нинга более привлекателен, хоть он и ошибается с некоторой вероятностью. В диссертации предложена комбинация использующейся в этом алгоритме идеи вероятностного локального поиска с другой идеей, принадлежащей Р.Патури. П. Пудлаку и Ф. Зейну [75] — использованием случайного упорядочения переменных и дальнейшего устранения единичных дизъюнкций (этот метод также называется методом кодирования выполняющего набора). Хотя на первый взгляд эти методы не могут быть скомбинированы в одном алгоритме, в диссертации делается именно это. Вычислительные эксперименты (в том числе проведённые независимо другими исследователями) показали перспективность полученного экспериментального алгоритма, названного UnitWalk. Для него также было доказано свойство вероятностной приближённой полноты, которое отсутствует у многих других экспериментальных алгоритмов, основанных на методе вероятностного локального поиска. Это свойство, определённое Х. Хоосом [55], состоит в том, что независимо от начального набора алгоритм всегда имеет положительную вероятность найти выполняющий набор (с другими алгоритмами локального поиска часто случается, что случайное блуждание приводит их в локальный максимум целевой функции, из которого им не удаётся выбраться без того, чтобы начать случайное блуждание заново).

Теорема 2.3. Алгоритм UnitWalk обладает свойством вероятностной приближённой полноты.

Приводимые в диссертации результаты об алгоритмах для задачи выполнимости пропозициональных формул опубликованы в двух главных работах [26] и [52], а также работах [1, 27, 28, 50, 51, 87]. После того, как эти работы были опубликованы, Р. А. Мозеру и Д. Шедеру [71] удалось улучшить детерминированный алгоритм для к-SAT: воспользовавшись той же конструкцией множества начальных наборов, что излагается в разделе 2.1.2.2, и другой дерандомизацией случайного блуждания, они достигли верхней оценки 0((2 — | + б) п). Также в серии работ К. Ивама и др. методы локального поиска и кодирования выполняющего набора были объединены иным (отличным от приводимого в настоящей диссертации) методом, что в конечном итоге привело к вероятностному алгоритму для 3-SAT, работающему время 0(1.32 113п) [58].

Реализация алгоритма UnitWalk была доработана А. А. Кожевниковым и оказалась лучшей для случайно сгенерированных выполнимых формул на соревновании программ для задачи SAT в 2003 году[11]. Также М. Хейле и X. ван Маарен использовали алгоритм UnitWalk, реализовав его другим способом в солвере UnitMarch [44].

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

Теорема 2.4. Существует алгоритм, который выдаёт набор, выполняющий не менее (1-е)-OptVal (-F) дизъюнкций входной формулы F от N переменных с вероятностью не менее 1 — где е = 2.171 828. Время его работы в наихудшем случае составляет poly (|F|) • ске, где = 2 — к+2ее+ке < 2, a |F| обозначает длину битового представления входной формулы F.

Здесь poly (|F|) означает функцию, ограниченную сверху некоторым полиномом от F, т. е.

Приводится также детерминированный алгоритм для точного решения задачи MAX-2-SAT, заканчивающий работу за время 2К2//5 с точностью до полиномиального сомножителя.

Теорема 2.7. Существует алгоритм, находящий для входной формулы F в 2-КНФ оптимальное значение OptVal (F) за время poly (|F|) • 2К2//5, где К2 ~ суммарный вес всех 2-дизъюнкций формулы F, a |F| обозначает длину битового представления входной формулы.

Приводимые в диссертации результаты об алгоритмах для задачи максимальной выполнимости опубликованы в двух главных работах [48] и [35], а также работах [47, 45]. После того, как эти работы были опубликованы, сначала А. Кожевников и А. С. Куликов [59], а затем Д. Бинкеле-Ребле и Х. Фернау [12] доработали алгоритм для максимальной 2-выполнимости, приводимый в этой диссертации, и им удалось получить оценку 0(2²//6 22).

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

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

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

1. Всемирное М. А., Гирш Э. А., Данцин Е. Я., Иванов С. В. Алгоритмы для пропозициональной выполнимости и верхние оценки их сложности // Записки научных семинаров ПОМИ. 2001. Т. 277. С. 14−46.

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

3. Левин Л. А. Универсальные задачи перебора // Проблемы передачи информации. 1973. Vol. 9, N. 3. Р. 115−116.

4. Цейтин Г. С. О сложности вывода в исчислении высказываний // Записки научных семинаров ЛОМИ. 1968. Т. 8. С. 234−259.

5. Alekhnovich М. Lower bounds for k-DNF resolution on random 3-CNFs // Proceedings of the 37th Annual ACM Symposium on Theory of Computing, STOC'05. 2005. P. 251−256.

6. Arora S., Lund C. Hardness of approximation // Approximation algorithms for NP-hard problems / Ed. by D. Hochbaum. Boston: PWS Publishing Company, 1997. P. 399−446.

7. Ash R. B. Information Theory. Dover, 1965.

8. Balas E., Ceria S., Cornuejols G. A lift-and-project cutting plane algorithm for mixed 0−1 programs // Mathematical Programming. 1993. Vol. 58. P. 295 324.

9. Beame P., Impagliazzo R., Krajicek J., Pitassi T., Pudlak P. Lower bounds on Hilbert’s Nullstellensatz and prepositional proofs // Proc. London Math. Soc. 1996. Vol. 73, N. 3. P. 1−26.

10. Beame P., Pitassi T., Segerlind N. Lower bounds for Lovasz-Schrijver systems and beyond follow from multiparty communication complexity // SIAM Journal on Computing. 2007. Vol. 37, N. 3. P. 845−869.

11. Berre D. L., Simon L. The essentials of the SAT 2003 competition // Proceedings of the 6th International Conference on Theory and Applications of Satisfiability Testing, SAT 2003. Vol. 2919 of Lecture Notes in Computer Science. 2003. P. 452−467.

12. Binkele-Raible D., Fernau H. A new upper bound for Max-2-SAT: A graph-theoretic approach // Journal of Discrete Algorithms. 2010. Vol. 8. P. 388 401.

13. Bonet M., Pitassi T., Raz R. Lower bounds for Cutting Planes proofs with small coefficients // Proceedings of the 27th Annual ACM Symposium on Theory of Computing, STOC'95. ACM, 1995. P. 575−584.

14. Buss S. Polynomial size proofs of the propositional pigeonhole principle // Journal of Symbolic Logic. 1987. Vol. 52. P. 916−927.

15. Buss S., Grigoriev D., Impagliazzo R., Pitassi T. Linear gaps between degrees for the polynomial calculus modulo distinct primes // Journal of Computing and System Sciences. 2001. Vol. 62. P. 267−289.

16. Buss S., Impagliazzo R., Krajicek J., Pudlak P., Razborov A. A. Sgall J. Proof complexity in algebraic systems and bounded depth Frege systems with modular counting // Computational Complexity. 1996/97. Vol. 6, N. 3. P. 256−298.

17. Calabro C., Impagliazzo R., Paturi R. A Duality between Clause Width and Clause Density for SAT // Proceedings of the 21st Annual IEEE Conference on Computational Complexity, CCC 2006. 2006. P. 252−260.

18. Chattopadhyay AAda A. Multiparty communication complexity of disjoint-ness // Electronic Colloquium on Computational Complexity. 2008. Vol. 15, N. 002.

19. Chvdtal V. Edmonds polytopes and a hierarchy of combinatorial problems // Discrete Mathematics. 1973. Vol. 4. P. 305−337.

20. Clegg M., Edmonds J., Impagliazzo R. Using the Groebner basis algorithm to find proofs of unsatisfiability // Proceedings of the 28th Annual ACM Symposium on Theory of Computing, STOC'96. ACM, 1996. P. 174−183.

21. Cohen G., Honkala I., Litsyn S., Lobstein A. Covering Codes. Elsevier, 1997. Vol. 54 of Mathematical Library.

22. Cook S. A. The complexity of theorem-proving procedure // Proc. 3rd Annual ACM Symposium on the Theory of Computing. 1971. P. 151−159.

23. Cook S. A., Reckhow R. A. The relative efficiency of propositional proof systems // Journal of Symbolic Logic. 1979. Vol. 44, N. 1. P. 36−50.

24. Cook W., Coullard C. R., Turan G. On the complexity of cutting-plane proofs // Discrete Applied Mathematics. 1987. Vol. 18, N. 1. P. 25−38.

25. Dantsin E., Gavrilovich M., Hirsch E. A., Konev B. 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.

26. Dantsin E., Goerdt A., Hirsch E. A., Kannan R., Kleinberg J., Papadimitri-ou C., Raghavan P., Schoning U. A deterministic (2 — 2/(k + l))n algorithmfor к-SAT based on local search // Theoretical Computer Science. 2002. Vol. 289, N. 1. P. 69−83.

27. Dantsin E., Hirsch E. A. Algorithms for k-SAT based on covering codes // Препринты ПОМИ PAH. 2000. N. 1/2000. P. 1−12.

28. Dantsin E., Hirsch E. A. Worst-case upper bounds // Handbook of Satisfiability / Ed. by A. Biere, M. Heule, H. van Maaren, Т. Walsh. IOS Press, 2009. Vol. 185 of Frontiers in Artificial Intelligence and Applications. P. 403−424.

29. Davis M., Logemann G., Loveland D. A machine program for theoremproving // Communications of the ACM. 1962. Vol. 5, N. 7. P. 394−397.

30. Davis M., Putnam H. A computing procedure for quantification theory // Journal of the ACM. 1960. Vol. 7, N. 3. P. 201−215.

31. Frege G. Begriffsschrift: eine der arithmetischen nachgebildete Formelsprache des reinen Denkens. Halle, 1879.

32. Goerdt A. The Cutting Plane proof system with bounded degree of falsity // Proceedings of CSL 1991. Vol. 626 of Lecture Notes in Computer Science. Springer, 1991. P. 119−133.

33. Gomory R. E. An algorithm for integer solutions of linear programs // Recent Advances in Mathematical Programming / Ed. by R. L. Graves, P. Wolfe. McGraw-Hill, 1963. P. 269−302.

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

35. Grigoriev D. Complexity of Positivstellensatz proofs for the knapsack // Computational Complexity. 2001. Vol. 10. P. 139−154.

36. Grigoriev D., Hirsch E. A. Algebraic proof systems over formulas // Theoretical Computer Science. 2003. Vol. 1, N. 303. P. 83−102.

37. Grigoriev D., Hirsch E. A., Pasechnik D. V. Complexity of semi-algebraic proofs // Moscow Mathematical Journal. 2002. Vol. 2, N. 4. P. 647−679.

38. Grigoriev D., Vorobjov N. Complexity of Nulland Positivstellensatz Proofs // Annals of Pure and Applied Logic. 2001. Vol. 113, N. 1−3. P. 153 160.

39. Gu J., Purdom P., Franco JWah B. W. Algorithms for the Satisfiability Problem. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2000.

40. Haken A. The intractability of resolution // Theoretical Computer Science. 1985. Vol. 39. P. 297−308.

41. Hirsch E. A. A new algorithm for MAX-2-SAT // Proceedings of the 17th Annual Symposium on Theoretical Aspects of Computer Science, STACS 2000. Vol. 1770 of Lecture Notes in Computer Science. Springer, 2000. P. 6573.

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

43. Hirsch E. A. Worst-case study of local search for MAX-/c-SAT // Discrete Applied Mathematics. 2003. Vol. 130, N. 2. P. 173−184.

44. Hirsch E. A. Exact Algorithms for General CNF SAT // Encyclopedia of Algorithms. Springer, 2008. P. 286−288.

45. Hirsch E. A., Kojevnikov A. UnitWalk: A new SAT solver that uses local search guided by unit clause elimination // Препринты ПОМИ PAH. 2001. N. 9/2001. P. 1−25.

46. Hirsch E. A., Kojevnikov A. Unit Walk: A new SAT solver that uses local search guided by unit clause elimination // Annals of Mathematics and Artificial Intelligence. 2005. Vol. 43, N. 1. P. 91−111.

47. Hirsch E. A., Kojevnikov A. Several notes on the power of Gomory-Chvatal cuts // Annals of Pure and Applied Logic. 2006. Vol. 141, N. 3. P. 429−436.

48. Hirsch E. A., Kojevnikov A., Kulikov A. S., Nikolenko S. I. Complexity of semialgebraic proofs with restricted degree of falsity // Journal on Satisfiability, Boolean Modeling and Computation. 2009. Vol. 6, N. 1−3. P. 53−69.

49. Hoos H. H. On the run-time behaviour of stochastic local search algorithms for SAT // Proceedings of the 16th National Conference on Artificial Intelligence, AAAI'99. 1999. P. 661−666.

50. Hoos H. H., Stiitzle T. SATLIB: An Online Resource for Research on SAT // Highlights of Satisfiability Research in the Year 2000. IOS Press, 2000. Vol. 63 of Frontiers in Artijicial Intelligence and Applications. P. 283−292.

51. Impagliazzo R., Pudlak P., Sgall J. Lower bounds for the polynomial calculus // Computational Complexity. 1999. Vol. 8, N. 2. P. 127−144.

52. Kojevnikov A., Kulikov A. S. A new approach to proving upper bounds for MAX-2-SAT // Proceedings of the 17th Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2006. 2006. P. 11−17.

53. Koutsoupias E., Papadimitriou C. H. On the greedy algorithm for satisfiability // Information Processing Letters. 1992. Vol. 43, N. 1. P. 53−55.

54. Krajicek J. Bounded Arithmetic, Propositional Logic, and Complexity Theory. Cambridge University Press, 1995. Vol. 60 of Encyclopedia of Mathematics and its Applications.

55. Krajicek J. Discretely ordered modules as a first-order extension of the cutting planes proof system // Journal of Symbolic Logic. 1998. Vol. 63, N. 4. P. 1582−1596.

56. Krajicek J., Pudlak P., Woods A. Exponential lower bound to the size of bounded depth Frege proofs of the pigeonhole principle // Random Structures and Algorithms. 1995. Vol. 7. P. 15−39.

57. Kullmann 0. New methods for 3-SAT decision and worst-case analysis // Theoretical Computer Science. 1999. Vol. 223, N. 1−2. P. 1−72.

58. Lee T., Shraibman A. Disjointness is hard in the multi-party number-on-the-forehead model // Proceedings of the 23rd Annual IEEE Conference on Computational Complexity, CCC'08. 2008. P. 81−91.

59. Lombardi H., Mnev N., Roy M.-F. The Positivstellensatz and small deduction rules for systems of inequalities // Mathematische Nachrichten. 1996. Vol. 181. P. 245−259.

60. Lovasz L. Stable sets and polynomials // Discrete Mathematics. 1994. Vol. 124. P. 137−153.

61. Lovasz L., Schrijver A. Cones of matrices and set-functions and 0−1 optimization // SIAM Journal on Optimization. 1991. Vol. 1. P. 166−190.

62. Marques-Silva J., Sakallah K. A. GRASP: a search algorithm for propositional satisfiability // IEEE Transactions on Computers. 1999. Vol. 48, N. 5. P. 506−521.

63. Monien B., Speckenmeyer E. Solving satisfiability in less then 2n steps // Discrete Applied Mathematics. 1985. Vol. 10. P. 287−295.

64. Moser R. A., Scheder D. A full derandomization of Schoning’s k-SAT algorithm // Proceedings of the 43rd Annual ACM symposium on Theory of Computing, STOC’ll. 2011. P. 242−252.

65. Niedermeier R., Rossmanith P. New upper bounds for MaxSat // Journal of Algorithms. 2000. Vol. 36. P. 63−88.

66. Papadimitriou C. H. On selecting a satisfying truth assignment // Proceedings of the 32nd Annual IEEE Symposium on Foundations of Computer Science, FOCS'91. 1991. P. 163−169.

67. Paturi R., Pudlak P., Saks M. E., Zane F. An improved exponential-time algorithm for fc-SAT // Proceedings of the 39th Annual IEEE Symposium on Foundations of Computer Science, FOCS'98. 1998. P. 628−637.

68. Paturi R., Pudlak P., Zane F. Satisfiability coding lemma // Proceedings of the 38th Annual IEEE Symposium on Foundations of Computer Science. FOCS'97. 1997. P. 566−574.

69. Pitassi T., Beame P., Impagliazzo R. Exponential lower bounds for the pigeonhole principle // Computational Complexity. 1993. Vol. 3. P. 97−140.

70. Pudlak P. Lower bounds for resolution and cutting plane proofs and monotone computations // Journal of Symbolic Logic. 1997. Vol. 62, N. 3. P. 981−998.

71. Pudlak P. On the complexity of prepositional calculus // Sets and Proofs: Invited papers from Logic Colloquium'97. Cambridge University Press, 1999. P. 197−218.

72. Razborov A. A. Lower bounds for the polynomial calculus // Computational Complexity. 1998. Vol. 7. P. 291−324.

73. Reckhow R. A. On the lengths of proofs in the prepositional calculus. PhD Thesis. University of Toronto. 1976.

74. Robinson J. A. Generalized resolution principle // Machine Intelligence. 1968. Vol. 3. P. 77−94.

75. Schoning U. A probabilistic algorithm for k-SAT and constraint satisfaction problems // Proceedings of the 40th Annual IEEE Symposium on Foundations of Computer Science, FOCS'99. 1999. P. 410−414.

76. Schuler R. An algorithm for the satisfiability problem of formulas in conjunctive normal form // Journal of Algorithms. 2005. Vol. 54, N. 1. P. 40−44.

77. Selman B., Kautz H. A., Cohen B. Noise strategies for improving local search // Proceedings of the 12th National Conference on Artificial Intelligence, AAAI'94. 1994. P. 337−343.

78. Selman B., Levesque H., Mitchell D. A new method for solving hard satisfiability problems // Proceedings of the 10th National Conference on Artificial Intelligence, AAAI'92. 1992. P. 440−446.

79. Simon L., Le Berre D., Hirsch E. A. The SAT2002 competition // Annals of Mathematics and Artificial Intelligence. 2005. Vol. 43, N. 1. P. 307−342.

80. Tzameret L Algebraic proofs over noncommutative formulas // Proceedings of the 7th Annual Conference on Theory and Applications of Models of Computation. Vol. 6108 of Lecture Notes in Computer Science. Springer, 2010. P. 60−71.

81. Urquhart A. Hard examples for resolution // JACM. 1987. Vol. 34, N. 1. P. 209−219.90. von Neumann J. Zur Hilbertschen Beweistheorie // Mathematische Zeitschrift. 1926. Vol. 26. P. 1−46.

82. Yannakakis M. On the approximation of maximum satisfiability // Journal of Algorithms. 1994. Vol. 17, N. 3. P. 457−502.