Сложность пропозициональной логики тема автореферата и диссертации по математике, 01.01.06 ВАК РФ

Санкт-Петербургский государственный университет

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

005004339

ГИРШ Эдуард Алексеевич

ЛОЖНОСТЬ ПРОПОЗИЦИОНАЛЬНОЙ логики

01.01.06 — математическая логика, алгебра и теория чисел

АВТОРЕФЕРАТ

диссертации на соискание ученой степени доктора физико-математических наук

- 1 ДЕК 2011

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

005004339

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

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

профессор ВЕРЕЩАГИН Николай Константинович (Московский государственный университет им. М.В.Ломоносова)

доктор физико-математических наук, чл.-корр. РАН РАЗБОРОВ Александр Александрович (Учреждение Российской академии наук Математический институт им. В.А.Стеклова РАН)

доктор физико-математических наук ПОНОМАРЕНКО Илья Николаевич (Учреждение Российской академии наук Санкт-Петербургское отделение Математического института им. В.А.Стеклова РАН, лаборатория теории представлений и вычислительной математики)

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

Защита состоится <2$> 20// г. в /6> часов на заседании совета

Д 212.232.29 по защите докторских и кандидатских диссертаций при Санкт-Петербургском государственном университете по адресу: 191023, Санкт-Петербург, наб. р. Фонтанки, 27, ауд. 311.

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

Автореферат разослан </У> 2011 г.

Ученый секретарь

диссертационного совета Д 212.232.29 доктор физ.-мат. наук, профессор

В. М. Нежинский

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ Актуальность темы. Сложность задач пропозициональной логики является важной тематикой в теории сложности вычислений и доказательств, составляющей важную область математической логики. Более сорока лет назад независимо СА.Куком и Л.А.Левиным было предложено понятие ИР-полноты, оказавшееся ключевым для современной теории сложности. В 1971 г. С.А.Куком была доказана Ш3-полнота задачи выполнимости формул логики высказываний, а затем С.А.Кук и Р.А.Рекхоу определили понятие пропозициональной системы доказательств. Последние несколько десятилетий теоретические исследования по оценкам сложности этой задачи велись в двух основных направлениях:

(1) построение новых систем пропозициональных доказательств, анализ отношений моделируемости между ними, построение в них эффективных доказательств важных семейств тавтологий, доказательство нижних оценок сложности для этих систем (первой была работа Г.С.Цейтина 1968 года, затем работы А.Хакена и А.Уркхарта и, наконец, многочисленные работы С.Басса, П.Бима, Я.Крайчека, П.Пудлака, А.А.Разборова и др.);

(2) построение новых алгоритмов для задачи выполнимости пропозициональных формул и связанных с ней задач, доказательство верхних оценок на время их работы (первыми были независимые работы Е.Я.Данцина и Б.Мониена и Э.Шпекенмейера начала 1980-х гг., а затем многочисленные работы О.Кульмана, М.Патури, У.Шонинга и др.).

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

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

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

Наиболее привычными системами доказательств являются системы Фре-ге, названные в честь Готлоба Фреге, который, однако, в своей монографии 1879 года использовал более общие системы, включающие правило подстановки; считается, что первым такие системы без правила подстановки использовал Джон фон Нейман. Экспоненциальных нижних оценок для них не известно и по сей день; однако известны такие оценки для систем, промежуточных между системами Фреге и резолюций: систем Фреге ограниченной глубины (работы Я.Крайчека, П.Пудлака и А.Вудса, Т.Питасси, П.Бима и Р.Импальяццо) и обобщения метода резолюций для формул, являющихся конъюнкциями формул в fc-ДНФ (работа М.Алехновича). Все системы Фреге

эквивалентны, как доказано в диссертации Р.А.Рекхоу 1976 года, и эквивалентны (по их определению) пропозициональному фрагменту генценовского секвенциального исчисления (с правилом сечения). Они обладают определёнными возможностями рассуждений о целых числах (представленных при помощи векторов пропозициональных переменных) — например, имеют полиномиального размера (хоть и технически непростые) доказательства пропозиционального принципа Дирихле, как показано С.Бассом.

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

Алгебраические системы основаны на слабой теореме Гильберта о нулях. Эти системы были предложены в работах Бима и др. и М.Клегга, Дж.Эдмондса и Р.Импальяццо. Экспоненциальные нижние оценки для этих двух систем были доказаны в серии работ С.Басса, Р.Импальяццо, А.А.Разборова и др. Обобщения алгебраических систем, в которых полиномы могут быть записаны произвольными алгебраическими формулами, были кратко рассмотрены в работах Т.Питасси (с вероятностной проверкой корректности доказательства) и П.Бима и др. , Полуалгебраические системы оперируют неравенствами: формулы в конъюнктивной нормальной форме естественным образом записываются в виде системы линейных неравенств в переменных, принимающих значения О и 1. Одно из важных различий между ними — способ, при помощи которого гарантируется, что решения системы принимают только значения 0 и 1.

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

неравенство х > [г]); её полнота была доказана Е.Гомори, далее она подробно изучалась В.Хваталом в контексте целочисленного линейного программирования, а как пропозициональная система она была впервые использована в работе У.Кука, К.Р.Кулларда и Г.Турана. Экспоненциальная нижняя оценка для неё была доказана П.Пудлаком. Другой способ обеспечить принадлежность решений множеству {0,1} — использовать квадратичные неравенства; такие системы берут начало из работы Л.Ловаса и А.Схрайвера 1991 года (полнота более простой системы доказательств, использующей правило "поднять-и-спроектировать", доказана в работе Е.Баласа, С.Кериа и Г.Корнуеолса 1993 года). Во всех этих системах пропозициональный принцип Дирихле имеет короткие доказательства.

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

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

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

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

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

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

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

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

Алгоритмы, основанные на лемме о кодировании выполняющего набора, были предложены М.Патури, П.Пудлаком, М.Саксом и Ф.Зейном. Главное отличие этих алгоритмов от DPLL-алгоритмов заключается в том, что для них важен порядок, в котором переменные выбираются для присваивания, и этот порядок не может быть определён по формуле, как для DPLL-алгоритмов; поэтому либо упорядочение переменных, выбираемых для присваивания, берётся случайным образом, либо (для детерминированного варианта) перебираются все перестановки из некоторого семейства с подходящими свойствами (не зависящими от конкретной формулы). Анализ основан не на локальных (как для DPLL-алгоритмов), а на глобальных рассуждениях, например оценке количества переменных, которые никогда не используются для рекурсивных вызовов, поскольку удаляются во время упрощения. Для этих алгоритмов более простыми являются их вероятностные варианты, когда и упорядочение переменных, и значение переменной на каждом шаге выбираются случайным образом, а вместо возврата из рекурсии используется новый запуск алгоритма с самого начала.

Метод локального поиска используется как в экспериментальных алгоритмах, так и для доказательства верхних оценок (работы Х.Пападимитриу и У.Шонинга). В частности, У.Шонингом доказано, что задача fc-SAT может быть решена алгоритмом, основанным на случайных блужданиях, за время (2 — 2/А;)п с точностью до полиномиального сомножителя.

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

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

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

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

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

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

Научная новизна. В диссертации получены следующие новые научные результаты:

• Предложен ряд полуалгебраических систем доказательств, в том числе статических (представляемых одной формулой без вывода); доказаны

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

- экспоненциальная нижняя оценка на размер статических доказательств,

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

• Предложены алгебраические системы доказательств Р-ЫБ и Р-РС, оперирующие формулами; доказана эквивалентность ^N8 и древесного варианта Р-РС.

• Доказано, что задача максимальной выполнимости для булевых формул в 2-КНФ, состоящих из К дизъюнкций, может быть решена за время

• Доказано существование вероятностного (1 — е)-приближённого алгоритма для задачи максимальной выполнимости формул в fc-КНФ, использующего время 0(n°W • (2 - k^fklT) (Для произвольного е > 0).

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

• Доказано, что задача выполнимости булевых формул в fc-КНФ, использующих п переменных, может быть решена детерминированным алгоритмом, использующим время 0((2 - щ + е)в) и память полиномиального размера (для произвольного е > 0).

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

Апробация работы. Результаты работы докладывались и обсуждались, в частности, на следующих конференциях и семинарах: 27-й международный коллоквиум по автоматам, языкам и программированию (ICALP 2000, Женева, Швейцария, 9-15 июля 2000 г.), 29-й международный коллоквиум по автоматам, языкам и программированию (ICALP 2002, Малага, Испания, 8-13 июля 2002 г.), 17-м ежегодный симпозиум по теоретическим аспектам информатики (STACS 2000, Лилль, Франция, 17-19 февраля 2000 г.), 19-м ежегодный симпозиум по теоретическим аспектам информатики (STACS 2002, Жуан ле Пен, Франция, 14-16 марта 2002 г.), международный ворк-

шоп по логике и сложности в информатике (Университет Париж-12, Франция, 3-5 сентября 2001 г.), 7-й международная конференция по принципам и практике программирования с использованием условий (CP 2001, Пафос, Кипр, 26 ноября - 1 декабря 2001 г.), городской семинар Санкт-Петербурга по математической логике под руководством акад. Ю.В.Матиясевича, общеинститутский математический семинар ПОМИ РАН под руководством проф., д.ф.-м.н. А. М. Вершика.

Публикация результатов. Результаты исследований отражены в 19 работах [1]—[19], в том числе 11 работах в изданиях, входящих в Перечень ведущих научных журналов и изданий, в которых должны быть опубликованы основные научные результаты диссертаций на соискание учёной степени доктора наук (издания [1, 3, 8] входили в Перечень на момент публикации; журналы [2, 4, 5, 6, 7, 9, 10, 11] входят в систему цитирования ISI Web of Knowledge).

Совместная работа [2] является объединением трёх независимых работ: работы [3] (а также [12]) и двух работ коллективов соавторов; диссертанту принадлежат в ней алгоритм для fc-SAT, использующий память полиномиального размера, улучшенный алгоритм для 3-SAT и доказательства верхних оценок для этих алгоритмов (леммы 7-10, теорема 2 и следствие 2). Эти же принадлежащие диссертанту результаты приводятся в пятом разделе совместной работы [1] и третьем разделе работы [13].

В работе [4] диссертанту принадлежит алгоритм для MAX-2-SAT и доказательство верхней оценки для него (теорема 10). В работе [5] диссертанту принадлежит доказательство эквивалентности системы F-NS и системы древесного вывода F-PC (теорема 6), доказательство моделируемости систем Фреге в F-PC (теорема 3) и короткое доказательство принципа Дирихле в системе F-NS константной глубины (раздел 6). В работе [6] диссертанту принадлежат утверждения о возможности эффективных рассуждений о целых

числах в системах третьей степени (теоремы 5.1 и 5.2, леммы 5.1 и 5.2), теорема о существовании доказательств полиномиального размера для тавтологий о раскраске графа, содержащего клику (теорема 4.1), и цейтинских тавтологий в системах ограниченной степени (теорема 6.1), экспоненциальная нижняя оценка на размер статических доказательств (теоремы 9.1-9.3, следствие 9.1; необходимые для доказательства леммы о нижних оценках на степень доказательств (раздел 8) получены в неразрывном соавторстве). Эти результаты диссертанта также приводятся в совместных работах [14] (разделы 4-6) и [15] (разделы 3 и 4). В работах [8, 9, 18] диссертанту принадлежит алгоритм и доказательство его вероятностной приближённой полноты, соавтору — реализация алгоритма и экспериментальная часть. В работе [11] диссертанту принадлежит методика оценивания, соавторам — реализация системы оценивания. В работе [10] диссертанту принадлежит доказательство эквивалентности алгебраических и полуалгебраических систем доказательств ген-ценовского типа (результаты раздела 2). В работе [19] диссертанту принадлежит доказательство моделирования системы СР с ограниченной степенью ложности методом резолюций (теорема 3).

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

Структура и объем диссертации. Диссертация изложена на 152 страницах и состоит из введения и двух глав, разбитых на 5 основных разделов, и списка использованной литературы. Библиография включает 91 наименование.

СОДЕРЖАНИЕ ДИССЕРТАЦИИ

Введение начинается с основных определений и обозначений, необходимых для понимания диссертации.

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

условиям:

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

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

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

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

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

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

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

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

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

не может встречаться дважды.

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

Определение 5. Результат подстановки набора А в формулу F обозначается как F[A] и представляет собой формулу, полученную из формулы F присваиванием значений из набора соответствующим переменным. Если набор даёт значения нескольким переменным, все они могут быть перечислены в квадратных скобках как F[vi = h,v2 = b2,...]. Иногда мы будем писать в наборе присваивание I = Ь для литерала I, имея в виду, что если I - переменная, то она получает значение Ь, а если отрицание переменной - то соответствующая

переменная получает значение Ч>.

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

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

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

выполнимых формул в А:-КНФ, обозначается /с-БАТ.

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

Определение 7. Результат подстановки одного набора В в другой набор А обозначается через А[В]; он представляет собой набор А, в котором значения переменных, имеющихся только в В, добавлены к Л, а значения переменных, имеющихся в обоих наборах, заменены на те, что имеются в В. Формальное определение таково: А[В] = {(V, Ь) | (и, Ь) £ В V ((г», Ь) е А А (V, ~>Ь) £ В))}.

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

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

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

Поскольку любая строка над конечным алфавитом может быть очевидным образом закодирована битовой строкой, в данной главе рассматриваются строки из {0,1}*, то есть множества всех конечных битовых строк.

Определение 1.1 (С.А.Кук, Р.А.Рекхоу, 1979). Системой доказательств для языка Ь С {0,1}* называется любая сюръективная функция / : {0,1}* Ь, вычислимая за полиномиальное время.

Определение 1.2. Пропозициональной системой доказательств называется любая система доказательств для некоторого заранее фиксированного со-КР-полного языка пропозициональных тавтологий (например тавтологий в дизъюнктивной нормальной форме).

Аргументы функции f, используемой в определении, можно назвать "кандидатами на роль доказательств", а элементы языка Ь — теоремами. Если /(7г) = х, будем говорить, что 7Г является /-доказательством х.

Определение 1.3. Система Щ полиномиально моделирует систему Пг, если существует такая функция д: {0,1}* -4 {0,1}*, сопоставляющая "кандидатам на роль доказательств" для Пг "кандидаты" для Пь что для любой строки 7Г П1(р(7г)) = Пг(7г), и длина д(тг) ограничена полиномом от длины тг. В частности, для каждой строки языка Ь длина её кратчайшего доказательства в П1 ограничена полиномом от длины её кратчайшего доказательства в Пг-

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

Система доказательств Щ экспоненциально отделена от системы Пг, если существует бесконечная последовательность таких строк ••• € что длина кратчайшего Пх-доказательства строки и ограничена полиномом от длины и, а длина кратчайшего Пг-доказательства строки и экспоненциальна.

Система доказательств Пх экспоненциально сильнее системы Пг, если система Пг полиномиально моделирует Пг и экспоненциально отделена от неё.

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

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

Пусть ^ — формула в А>ДНФ, — её отрицание (которое будет формулой в /с-КНФ). Определим перевод каждой дизъюнкции, входящей в конъюнкцию -тР, в полиномиальное равенство. Дизъюнкция, содержащая пере-

менные ... (< < &), переводится в равенство

(1 — ¿1) ■ — • (1 — = 0, (1.2)

где 1, = Чм если переменная входит в дизъюнкцию положительно (без отрицания), и к = (1 - у]%), если она входит с отрицанием. Для каждой переменной входящей в формулу, добавляется также равенство V? - ы = О в систему полиномиальных равенств.

Определяются алгебраические системы доказательств Nullstellensatz (N8), полиномиальное исчисление (РС) и системы, основанные на Positivstellensatz.

Ро8ИлУ81е11еп8а1г (Д.Ю.Григорьев и Н.Н.Воробьёв). Доказательство в этой системе состоит из таких полиномов д\,... ,дт и ..., Ы, что

» 3

Роз^Ь^еПег^х-исчисление (Д.Ю.Григорьев и Н.Н.Воробьёв).

Доказательство в этой системе состоит из полиномов /и,..., Ы и вывода равенства 1 + Щ = 0 из исходных равенств при помощи правил (1.3).

Полуалгебраические системы доказательств. Для этих систем используется следующий перевод формулы -пГ в конъюнктивной нормальной форме в систему 5 линейных неравенств. Дизъюнкция, содержащая переменные .'.., и,',, переводится в неравенство

к + + С1-5)

где и = если переменная ^ входит в дизъюнкцию положительно, и = 1 - если она входит отрицательно. Для каждой переменной х в систему

5 также добавляются неравенства

х ^ О,

(1.6)

1.

(1.7)

"Предсистема" ЬР. Рассмотрим единственное правило взятия линейной комбинации

(Здесь и в дальнейшем /, и д обозначают линейные функции с рациональными коэффициентами.)

Система вывода, основанная лишь на этом правиле, не является системой доказательств, так как она не является полной: из некоторых систем не имеющих 0/1-решений неравенств при помощи этих правил нельзя вывести противоречия, и поэтому при помощи неё нельзя доказать некоторые тавтологии. Будем называть эту "предсистему" ЬР; добавление в неё новых правил позволит получать (полные) пропозициональные системы доказательств.

Система секущих плоскостей (СР) (Е.Гомори). В этой системе доказательств противоречие 0 > 1 из системы 5 должно быть выведено при помощи правила (1.8) и правила округления

(где а; € Z, а а^ — переменная). Потребуем, чтобы все коэффициенты в выводимых неравенствах кроме свободного члена были целочисленными.

Система "поднять-и-спроектировать" (Ь&Р) (Е.Балас и др.)

19

£*= о

^ а^зг,- > с

(1.9)

> ГС1

содержит два правила: правило (1.8) и правило

_Ь.-i- (если заключение линейно). (1-Ю)

(fx + д( 1 - х)) mod(x2 - х)

Исчисление Ловаса-Схрайвера (LS). В этой системе промежуточные неравенства могут быть квадратичными. Противоречие должно быть выведено при помощи правила (1.8), которое теперь может быть применено и к квадратичным неравенствам, и правил

/>0 />0

(где / — линейная функция, х — переменная).

/х>0' /(1 — ж) > О Кроме того, к системе 5 добавляются неравенства

х2-х>0, х-х2>0 (1.12)

для каждой переменной х.

Ь8+ (Л.Ловас, А.Схрайвер). Эта система получается добавлением к ЬБ аксиом

г2 > 0 (1.13)

для любых линейных функций I.

ЬЭ* (Л.Ловас, А.Схрайвер). Эта система получается добавлением к системе ЬБ правила вывода

^ ° и, 9 линейны). (1.14)

/5 > О

1,3+,». Эта система объединяет Ь3+ и ЬБ».

ЬБ + СР1 (П.Пудлак). Эта система состоит из тех же аксиом и правил вывода, что и система 1Д а также правила округления (1.9) системы СР,

20

которое разрешается применять лишь к линейным неравенствам.

ЬЭ + СР2 содержит те же аксиомы и правила вывода, что и система ЬБ, а также правило округления (1.9) системы СР, которое теперь разрешается применять и к квадратичным неравенствам:

Эта система расширяет систему ЬБ, а именно, правило (1.11) разрешается применять к неравенствам / > 0 степени вплоть до ¿— 1, а не только к линейным неравенствам. Правило (1.8) разрешается применять к любому набору неравенств степени вплоть до степени <1.

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

Статический вариант ЬБ00. Рассмотрим систему неравенств 5, состоящую из неравенств Si > 0 для г = 1, ...,£, где каждое неравенство ^ О либо получено в результате перевода (1.5), либо является неравенством вида х^ > 0 или 1 - X] > 0, либо является неравенством вида х] —х^ > 0. Опровержение такой системы состоит из положительных вещественных констант и мультимножеств 11ц и и~р определяющих такие полиномы

а^х{х3 4- > с

(где а;, ау 6 2,1; - переменная). (1.15)

Еи <ь]Х<Х1 + Ег а'Х> ^ ГС1

Аналогичным образом определяются системы ЬБ^, ЬЭ» и ЬБ'

и«',/ = • Д Хк П (1 - Хк),

Ш+, кеи-,

что

(1.16)

Статический вариант LS~ Отличие от предыдущей системы состоит в том, что в систему S добавляются неравенства st+1 > 0,..., st- ^ О, где каждый из полиномов Sj (j G {t +1,..., f}) представляет собой квадрат другого полинома Условие (1.16) заменяется условием

«=1 i

Статический вариант LS+. Аналогичен статическому варианту LS+, но полиномы s- должны быть линейными.

Секвенциальные системы, основанные на неравенствах. В общем случае секвенциальный вариант R(6) можно определить для любой системы вывода 6. Строками новой системы являются множества строк {/¡}Ц системы 6, обозначаемые как дизъюнкции Л V • • • V Л- Правила вывода в новой системе таковы (ниже Г обозначает произвольную дизъюнкцию строк системы б): два структурных правила

Г (1.20) ТУГ

ШУЕ (1.21)

/V г '

правило для введения отрицания, которое мы сразу запишем для неравенств:

х - 1 > 0 У -х ^ 0 (где х - переменная), (1.22)

и главное правило: если h получено из fU---,fk согласно правилу вывода системы 6, то .

/1УГ,...,ДУГ (123)

h\JT

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

LSfpj;t. Эта система включает в себя систему LSd, причём правила (1.8) и (1.11) обобщаются естественным образом для использования строгих неравенств; также вводится правило ослабления строгого неравенства / > 0 до нестрогого / > 0. Вводится аксиома 1 > 0. Система содержит все правила системы R(LS<i), но правило введения отрицания (1.22) заменяется на другое:

/>оу-/>о- (1'24)

Иначе говоря, мы разрешаем делать предположения вида / > 0 и заключать, что / ^ 0, если в LSjfpIit можно вывести противоречие из сделанного предположения.

LS^ определяется аналогично. Добавляется также правило

луо>о

Д

LS/ — система LSd, расширенная строгими неравенствами и правилом деления

fg > 0, / > 0 9> 0 '

LSSpiit, LS»iSpi,t и т.д. — сокращения для соответствующих систем, ограниченных использованием только полиномов степени d= 2.

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

Формульные алгебраические системы. Строками системы F-PC являются алгебраические формулы.

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

23

вилам могут получаться только формулы большего размера, то, чтобы вывести формулу 1 (означающую противоречие 1 = 0), введём также (обратимые) правила упрощения, выражающие ассоциативность, коммутативность, дистрибутивность и т.д. Эти правила упрощения перечисляются далее в диссертации. Они могут быть применены к любым подформулам (подтермам)

выводимых формул.

Доказательство в системе для множества алгебраических формул ..., Рт} состоит из двух частей:

• мультимножества {Сь..., <Зт} алгебраических формул;

• вывода единицы из алгебраической формулы

т ¡=1

при помощи правил упрощения системы Р-РС.

Наконец, определяются системы Р-РС и Р-ИЗ константной глубины. В разделе 1.2 рассматриваются формульные алгебраические системы. Доказывается следующая теорема о полиномиальной эквивалентности системы Р-ЫБ и древесного вывода в системе Р-РС.

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

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

В разделе 1.3 рассматриваются полуалгебраические системы. Эти системы рассматриваются не только как пропозициональные системы доказа-

24

тельств, но и как системы доказательств для других co-NP-трудных языков, языков несовместных систем равенств или неравенств.

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

тп-х i - х2 — ... - хп = 0 (где тп £ Z), (1-57)

в статических вариантах систем доказательств Ловаса-Схрайвера и в Positivstellensatz-исчислении.

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

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

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

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

Лемма 1.7. Пусть У = а,хи fd{Y) = {Y-{d- 1))(У - d), <ц - целочисленные константы, Xi — переменные. Тогда существует вывод неравенства fd{Y) ^ 0 (из аксиом) размера, полиномиального от d, п и maxi |а;|, в системах LS3 и LSspHt, причём правило введения отрицания применяется только к переменным.

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

П®е-П(1-Х«)=0' (1'59)

где V пробегает все вершины некоторого графа, а пробегает все подмножества чётной мощности множества рёбер, инцидентных V.

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

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

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

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

ются в унарной системе счисления (соответствующие системы обозначаются индексом 1, например ЩСРх)).

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

Теорема 1.12. Если имеется вывод полиномиального размера в системе ЩСРх) строки доказательства Р из множества строк {ф]че/, то имеется и вывод полиномиального размера в системе ЩЬРх) строки Р V Г из множества строк {<5* \/ Г},е/.

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

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

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

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

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

чивает свою работу за время 0(1.481") и использует память полиномиального размера.

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

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

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

Теорема 2.4. Существует алгоритм, который выдаёт набор, выполняющий не менее (1-е) -Ор1;Уа1(Г) дизъюнкций входной формулы FoтЛг переменных

с вероятностью не менее 1 — где е = 2.171828____Время его работы в

наихудшем случае составляет poly(|F|) ■ где c*iC = 2 — < 2, a |F|

обозначает длину битового представления входной формулы F.

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

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

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

Статьи в журналах и изданиях, входящих в Перечень ВАК.

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

[2] Dantsin Е., GoerdtA., Hirsch Е. А., Каппап R., Kleinberg J., Papadimitri-ои С., Raghavan Р., Schöning U. A deterministic (2 —2/(fc + l))n algorithm for k-SAT based on local search // Theoretical Computer Science. 2002. Vol. 289, N. 1. P. 69-83.

[3] Dantsin E., Hirsch E. A. Algorithms for k-SAT based on covering codes // Препринты ПОМИ РАН. 2000. № 1/2000. С. 1-12.

[4] 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.

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

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

[7] Hirsch E. A. Worst-case study of local search for MAX-fc-SAT // Discrete Applied Mathematics. 2003. Vol. 130, N. 2. P. 173-184.

[8] Hirsch E. A., Kojevnikov A. UnitWalk: A new SAT solver that uses local search guided by unit clause elimination // Препринты ПОМИ PAH. 2001. № 9/2001. C. 1-25.

[9] Hirsch E. A., Kojevnikov A. UnitWalk: 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.

[10] Hirsch E. A., Kojevnikov A. Several notes on the power of Gomory-Chvätal cuts // Annals of Pure and Applied Logic. 2006. Vol. 141, N. 3. P. 429-436.

[11] 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.

Другие публикации.

[12] Dantsin E., Goerdt A., Hirsch E. A., Schöning U. Deterministic algorithms for fc-SAT based on covering codes and local search // Proceedings of the 27th International Colloquium on Automata, Languages and Programming (ICALP 2000). Vol. 1853 of Lecture Notes in Computer Science. Springer, 2000. P. 236-247.

[13] 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.

[14] Grigoriev D., Hirsch E. A., Pasechnik D. V. Complexity of semi-algebraic proofs // Proceedings of the 19th Annual Symposium on Theoretical Aspects of Computer Science (STACS 2002). Vol. 2285 of Lecture Notes in Computer Science. Springer, 2002. P. 419-130.

[15] Grigoriev D., Hirsch E. A., Pasechnik D. V. Exponential lower bound for static semi-algebraic proofs // Proceedings of the 29th International Colloquium on Automata, Languages and Programming (1СALP 2002). Vol. 2380 of Lecture Notes in Computer Science. Springer, 2002. P. 257-268.

[16] 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. 65-73.

[17] Hirsch E. A. Worst-case time bounds for MAX-&-SAT w.r.t. the number of variables using local search // Proceedings of the 4th International Workshop on Randomization and Approximation Techniques in Computer Science (RANDOM 2000), ICALP Workshops 2000. Vol. 8 of Proceedings in Informatics. Carleton Scientific, 2000. P. 69-76.

[18] Hirsch E. A., Kojevnikov A. Solving Boolean satisfiability using local search guided by unit clause elimination // Proceedings of the 7th International Conference on Principles and Practice of Constraint Programming (CP 2001). Vol. 2239 of Lecture Notes in Computer Science. Springer, 2001. P. 605-609.

[19] 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.

Подписано к печати 05.09.2011.

Формат бумаги 60 х 84 Vie. Бумага офсетная.

Печать цифровая. Усл. печ. л. 2,00. Тираж 100 экз. Заказ 5244.

Отпечатано в отделе оперативной полиграфии Химического факультета СПбГУ.

198504, Санкт-Петербург, Петродворец, Университетский пр. 26

Введение

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

Актуальность темы и исторический обзор.

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

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

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

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

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

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

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

1.1 Определения, связанные с системами доказательств.

1.1.1 Понятие системы доказательств

1.1.2 Традиционные системы доказательств.

1.1.3 Алгебраические системы доказательств.

1.1.4 Полуалгебраические системы доказательств

1.1.5 Секвенциальные системы, основанные на неравенствах

1.1.6 Системы, использующие строгие неравенства.

1.1.7 Формульные алгебраические системы.

1.2 Формульные алгебраические системы.

1.2.1 Моделирование систем Фреге в системе Р-РС.

1.2.2 Полиномиальная эквивалентность системы Р-ИБ и древесного вывода в системе Р-РС.

1.2.3 Короткие доказательства пропозиционального принципа Дирихле в системах ограниченной глубины.

1.3 Полуалгебраические системы.

1.3.1 Способы перевода пропозициональных формул для использования в ЬБ^ и верхние оценки на степень доказательств

1.3.2 Короткие доказательства тавтологий, кодирующих нераскрашиваемость графа, содержащего клику, в системах ЬБ + СР2 и ЬЯ

1.3.3 Рассуждения о целых числах в полуалгебраических системах

1.3.4 Короткие доказательства цейтинских тавтологий в системе

1.3.5 Линейная нижняя оценка на "булеву степень" опровержения симметричной задачи о рюкзаке в Positivstellensatz-иcчиcлeнии

1.3.6 Экспоненциальная нижняя оценка на размер вывода в статическом варианте Ь8+ и в Positivstellensatz-исчислении.

1.3.7 Секвенциальные системы, основанные на линейных неравенствах

1.3.8 Система секущих плоскостей с ограниченной степенью ложности.

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

2.1 Алгоритмы для задачи выполнимости пропозициональных формул

2.1.1 Обозначения и соглашения.

2.1.2 Детерминированные алгоритмы, основанные на методе локального поиска.

2.1.3 Экспериментальный вероятностный алгоритм, основанный на комбинации методов локального поиска и кодирования выполняющего набора.

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

2.2.1 Определения, связанные с задачей максимальной выполнимости

2.2.2 Вероятностный алгоритм для задачи MAX-Zc-SAT, основанный на методе локального поиска.

2.2.3 Детерминированный алгоритм для задачи MAX-2-SAT, основанный на методе расщепления.

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

Определение 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.32113п) [58].

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

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

Теорема 2.4. Существует алгоритм, который выдаёт набор, выполняющий не менее (1-е)-OptVal(-F) дизъюнкций входной формулы F от N переменных с вероятностью не менее 1 — где е = 2.171828. Время его работы в наихудшем случае составляет 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^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. 295324.

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

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., Turän 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., Schöning 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 Null- and Positivstellensatz Proofs // Annals of Pure and Applied Logic. 2001. Vol. 113, N. 1-3. P. 153160.

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. Schöning 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.