Сложность пропозициональных систем доказательств, оперирующих неравенствами тема автореферата и диссертации по математике, 01.01.06 ВАК РФ

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

На ггоавах рукописи ииаОБООЭБ

Кожевников Арист Александрович

СЛОЖНОСТЬ ПРОПОЗИЦИОНАЛЬНЫХ СИСТЕМ ДОКАЗАТЕЛЬСТВ, ОПЕРИРУЮЩИХ НЕРАВЕНСТВАМИ

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

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

2 4 МАЙ 2007

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

003060095

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

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

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

Пономаренко Илья Николаевич — кандидат физико-математических наук, доцент Тишков Артем Валерьевич Ведущая организация — Институт математики им С Л Соболева

Сибирского отделения Российской академии наук

Защита диссертации состоится " ^ " Я 4 Я 2007 года

в 11 О'Ь часов на заседании Диссертационного совета Д 212 232 29 по защите диссертаций на соискание ученой степени доктора наук при Санкт-Петербургском государственном университете по адресу 19В504, Санкт-Петербург Старый Петергоф, Университетский пр , 28, математико-меха-нический факультет Санкт-Петербургского государственного университета

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

Защита будет проходить в Санкт-Петербургском отделении Математического института им В А Стеклова РАН по адресу Санкт-Петербург, наб реки Фонтанки, д 27, ауд 311

Автореферат разослан "2?" 2007 года

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

профессор

Нежинский В М

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

Актуальность темы Необходимость математического изучения понятия доказахельства была сформулирована и обоснована Д Гильбертом совместно с П Бернайсом в "Основаниях математики" Д Гильберта интересовала непротиворечивость всей математики и, в частности, непротиворечивость доказательств основных теорем Для того, чтобы проверить корректность доказательства за разумное время, необходимо, чтобы само доказательство было разумного размера Отсюда возникает важный вопрос о сложности систем доказательств, изучение которого было инициировано работой С А Кука и Р А Рекхоу 1979 г в естественном предположении, что каждый шаг доказательства проверяется за полиномиальное время, требуется оценить количество шагов доказательства

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

Исторически сложилась более естественная, похожая на обычное математическое доказательство, терминология для описания сисгем доказательств В ней в качестве L используется один из естественных языков математических объектов, например, язык пропозициональных тавтологий в нормальной форме Доказательством в аакои системе называется конечная последовательность строк, заканчивающейся строкой, которую мы хотим доказать Каждая строка в доказательстве получается из предыдущих строк по правилу вывода Если правило не имеет посылки, оно называется аксиомой

Пропозициональной системой доказательств называется система доказательств для языка TAUT пропозициональных тавтологий в дизъюнктивной нормальной форме (ДНФ) Поскольку такой язык содержится в co-NP, то любую систему доказательств для co-NP-трудного языка L мож-

ио считать пропозициональной системой доказательств, для этого необходимо лишь зафиксировать конкретное сведение

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

V V V-У. - + > 1

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

Первая полуалгебраическая система доказательств, "секущие плоскости" (CP), оперирующая только линейными неравенствами, была введена в работах Р Е Гомори 1963 г и В Хватала 1973 г Доказательство нижнеи экспоненциальной оценки для системы "секущие плоскости" долгое время оставалось важным открытым вопросом В работе А Гердта 1991 г была доказана нижняя экспоненциальная оценка для CP с oí раниченной степенью ложности, в работах М Боне и др 1995 г и Я Крайчека 1997 г для CP с унарными коэффициентами, в работах Р Импалияццо и др 1995 г и Я Крайчека 1998 г для древовидных "секущих плоскостей" Для системы без ограничении нижняя экспоненциальная оценка была доказана П Пуд-лаком в 1997 г Нижняя экспоненциальная оценка для другой изучаемой в диссертации системы "поднять и спроецировать" была доказана аналогичной техникой С Дашем в 2002 г

Для системы Ловаса-Схрайвера, оперирующей квадратичными неравенствами, нижние экспоненциальные оценки были известны только для древовидных доказательств систем неравенств, не обладающих корохкой записью в виде булевой формулы (один из результатов работы Д Ю Григорьева и др 2002 г) Также было известно несколько условных нижних оценок для системы, объединенной с СР, П Пудлака 1997 г , и для древовидной версии системы, П Бима и др 2005 г

Цели работы 1 Доказать нижние экспоненциальные оценки на размер вывода в полуалгебраических системах доказательств, для которых они были не известны Предложить новые методы доказательства таких оценок

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

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

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

Основные результаты работы 1 Получены нижние экспоненциальные оценки на размер статических и древовидных доказательств в системе Ловаса-Схрайвера для цейтинских тавтологии Доказана моделируемость системы доказательств "поднять и спроецировать" с унарными коэффициентами в системе "секущие плоскости"

2 Доказана верхняя полиномиальная оценка па размер доказательства цейтинских тавтологий в краичековском расширении генценовского типа системы "поднять и спроецировать" Улучшены нижние экспоненциальные оценки на размер древовидного доказательства в рассматриваемом системе доказательств устранена зависимость от максимального размера коэффициентов

3. Изучена сложность систем Ловаса-Схрайвера старших степеней с ограничением на свободный член рассматриваемые системы экспоненциально отделены от системы 'секущие плоскости" и обобщения революционной системы доказательств, оперирующего формулами в &-ДНФ Получена нижняя экспоненциальная оценка на размер доказательств цейтинских тавтологий

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

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

Апробация работы. Результаты диссертации докладывались на семинаре по дискретной махематике ПОМИ РАН, а также на международных конференциях "Вторые дни логики и вычислимости в Санкг-Петербурге", посвященной столетию А А Маркова (август 2003, Санкт-Петербург, Россия), "Международном коллоквиуме по автоматам, языкам и программированию", ICALP (июль 2006, Венеция, Италия) и "Международной конференции по теории и практическому применению задачи выполнимости', SAT (август 2006, Сиэтл, США)

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

Структура и объем диссертации. Диссертация состоит из введения и четырех глав Нумерация разделов, формул, примеров, лемм и теорем ведется отдельно для каждой главы Текст диссертации изложен на 96 страницах (исключая список литературы) Список литературы содержит 57 наименований

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

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

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

Основные понятия теории сложности доказательств определяются в первой главе Система доказательств А полиномиально моделируется

в системе доказательств В, если для любою доказательства р в А существует доказательство полиномиальной от |р| длины того же факта в В Доказательство нижних экспоненциальных оценок для системы II обычно заключается в предоставлении такой последовательности хп 6 L,n £ N, в которой длина каждого хп полиномиально зависит от п и любое П-доказательство хп имеет экспоненциальный от п размер

Полуалгебраические системы доказательств преобразовывают каждый дизъюнкт отрицания исходной тавтологии F, содержащий переменные t>i, ,vt, в неравенство

h+ +lt> 1, (1)

где 1г — уг, если переменная уг входит положительно в исходный дизъюнкт, и 1г = 1 — vt, если vl входит отрицательно Далее из полученной системы выводится противоречие 0 > 1 при помощи естественных правил работы с неравенствами и правил, использующих факт булевости переменных Следовательно, если таким образом может быть выведено противоречие, формула F действительно является тавтологией

В работе изучается сложность нескольких полуалгебраических систем доказательств Первые две из них, системы "секущие плоскости" (CP Cutting Planes) и "поднять и спроецировать" (L&P, Lift and Project) оперируют только линеиными неравенствами Обе системы используют аксиомы

Mil + А2/2 > о

а 12га'Х> - С

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

Система CP использует правила (где Аг е N), (3)

для каждой переменной х Система CP использует правила /1 > 0 /2> О

^ Га1

В системе L&P последнее правило заменяется на

/>0 д> О

(где а€Й,с,в,£2,а х, — переменные) (4)

(3)

/2+5(1-1) + с(х2 - х) > 0' где константа с выбирается таким образом, чтобы заключение правила бы ло линеиным

Система Лооаса-Схрайвера (ЬБ, Ьоуазг-БсЬгууег) оперирует квадратичными неравенствами, использует правило сложения (3) и правило умножения на литерал

Ш- <■*» и

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

х2 - х > 0 (7)

Систему можно расширить до следующем множеством аксиом

/2>0 (гдсаеё/ = 1) (8)

Описанные выше системы можно усилить, позволив им оперировать неравенствами старших степеней В частности, в ЬБ^ в правиле (6) неравенство / может быть любой степени, меньшей к Различные системы доказательств можно комбинировать между собой, разрешая одной системе использовать правила вывода из другой Таким образом определяется система ЬЭ^Ч-СР^, оперирующая правилами ЬБ'1 и СРЛ

Полуалгебраическая система генценовского типа Щб) представляет собой естественное усиление 6 — любой из определенных выше систем, позволяющее работать с предположениями в частности, можно предположить, что линейная сумма с целочисленными коэффициентами / больше чем целое с или, наоборот, / не больше чем с и вывести в каждом предположении противоречие Запишем правила вывода 11(6) (мы будем обозначать через Г произвольную дизъюнкцию неравенств)

/1 > О V Г, /2 > о V г Л > о /2 > о

-, ^ . . . --—, если -——- — правило вывода ©,

п>0 у I п>О

_г_ />оу/>оуг

г V / > о' / > о V г

и множеством аксиом

/ > 1 V / — 0 где / — линейная сумма с коэффициентами из Ъ

Отметим, что мы можем удалять из дизъюнкций противоречие 0 > 1, поскольку из него можно легко вывести любое неравенство

Поскольку длина доказательства измеряется количеством битов, используемых в доказательстве, на ней сказывается способ записи коэффициентов В СР и Ь&Р для записи коэффициентов используется двоичная система счисления В диссертации рассматриваются их ослабления СРх и Ь&Р1, отличающиеся от исходных тем, что оперируют целочисленными коэффициентами в унарной записи

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

такие, что

г

з

где йг — исходные неравенства (включая аксиомы)

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

~ тг) с> где аг — положительные константы, а тг — мономы Для неравенства г., определим ее степень лоэюности как правую часть литеральной формы I Степень ложности доказательства в ЬЗ^'+СР** определим как максимальную степень ложности всех возникающих в доказательстве неравенств

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

Принцип Дирихле с то кроликами и п клетками формализует невозможность предоставить каждому кролику собственную клетку при т > п Данный факт может быть выражен формулой РНР™ с топ булевыми переменными xtJ, 1 < г < т, 1 < j < п, равными 1, если г-ыи кролик сидит в jj-ой клетке

Пусть дан граф Gen вершинами Булева формула WQC™, кодирующая два факта, первый о том, что G содержит клику размера т, второй о том, что все вершины G можно раскрасить в т — 1 цвет таким образом, что соседние вершины имеют разные цвета, является невыполнимой Зафиксируем некоторый порядок на вершинах графа Наличие ребра, соединяющего вершины ! и j, задается булевой переменной рг] Переменной qh кодируется факт о том, что г-ая вершина является к-ой вершиной клики Наконец, переменная гг( обозначает то, что г-ая вершина покрашена в £-ый цвет Таким образом булева формула будет содержать п2 -f то п + (т — 1) п = (п + 2т — 1) п переменных

Впервые формулы Tsg, основанные на противоречии, заключающемся в том, что в графе G количество ребер вокруг всех вершин не может быть нечетным, были использованы в работе Г С Цейтина 1968 г для получения нижней оценки для ретулярной резолюции Позднее эти оценки были расширены для общей резолюции и улучшены до экспоненциальных для графов-расширителеи

Для графа G и подмножества вершин X через д(Х) мы будем обозначать множество соседей X Назовем (г d, с)-расширителем граф G с максимальной степенью d, такой, что для любого множества X С V, |Х| < г выполняется |9(ЛГ)| > с \Х\

Вторая глава посвящена сложности статических полуалгебраических систем доказательств Она содержит короткое статическое ЬБ+-дока-зательство формулы, кодирующей ослабленный принцип нераскрашивае-мости графа, содержащего клику и нижнюю экспоненциальную оценку на размер статического Ь8+-доказательства цейтинских формул

Теорема 2 15 системе доказательств ¿5+ существует короткое статическое доказательство четвертой степени формулы

Короткий вывод опровержения формулы \¥<ЗС™, кодирующей ослабленный принцип нераскрашиваемости в (гга — 1) цветов графа с п вершинами, содержащего клику размера т, был найден путем моделирования вывода формулы, кодирующий принцип Дирихле

В последнем разделе второй главы доказываются нижние экспоненциальные оценки на длину вывода цейтинских формул в статической полуалгебраической системе доказательств Ловаса-Схраивсра Доказательство основано на идеях из работы Д Ю Григорьева и др 2002 г и разделено на четыре основные части В первом подразделе мы показываем, что если граф С является "хорошим" расширителем, то он остается "хорошим'' расширителем после выкидывания линейного числа ребер Для этого мы пользуемся техникой из статьи М Алехновича и др 2005 г Далее, мы вводим систему Туэ преобразования мономов и доказываем некоторые ее свойства (в частности, связь со степенями вывода в алгебраической системе доказательств РозгШзЬеИепзаЬг) В следующем подразделе мы расширяем результат из работы Д Ю Григорьева 2001 г , доказывая нижнюю линейную оценку на булеву степень вывода в РовгЬпзЬеИепваЬг биномиальной записи цейтинских формул Далее мы сводим доказательство в ^'£lsг¿гг^síe//ensafe биномиальной записи цейтинских формул к доказательству в статической Ь8+ их булевой формы Наконец, в последнем подразделе мы показываем, как из результатов предыдущих частей, используя идеи Д Ю Григорьева и др 2002 г , получить нижнюю экспоненциальную оценку на размер доказательства в статической булевой формы цеитинских формул

Теорема 2 4 Пусть граф С является (г = п/2, с1, с)-расширителем, где й > 4, с > 1, а п — количество вершин Любое статическое доказательство цейтииской формулы Тес с имеет размер ехр(Г2(п))

В третьей главе изучается сложность генценовских расширений полуалгебраических систем доказательств Через ЩЬР) мы будем обозначать генценовское расширение системы, оперирующей единственным правилом сложения (3) В разделе 3 1 доказывается полиномиальная эквивалентность систем Г1(ЬР) и 11(Ь&Р), ЩЬРх) и ЩСР^, в следующем разделе показывается полиномиальное моделирование Ь&Р с унарными коэффициентами, 1^1, в СРх

В разделе 3 3 приводится доказательство верхней полиномиальной оценки на размер 11(ЬР)-доказательств цейтинских тавтологии

Теорема 3 4 Для любого целого числа д, > 1 и для любого д-регулярного графа в с нечетным количеством вершин п, существует вывод Тбс в Я(ЬР) полиномиального от п размера

В последнем разделе третьей главы мы вводим понятие вещественной коммуникационной сложности и показываем, как переделать доказательство в 11(СР)-110добной системе доказательств (что может использовать в качестве правил вывода все допустимые двухпосылоч7ше правила вывода) в протокол вещественной игры (в котором два игрока, обмениваясь вещественными числами, должны найти решение поставленной задачи, отметим, что сложность протокола равна количеству переданных чисел) Понятие вещественной коммуникационной шры напрямую связано с понятием вещественной схемы и используемая техника представляет собой частный случай интерполяции схемой Нижняя экспоненциальная оценка для древовидных 11(СР)-подобных систем получается из оценки на размер древовидного протокола вещественной игры, решающей известную теорему Холла (записываемую при помощи формулы На11п, где 2п — размер соответствующего двудольного графа)

Теорема 3 8 Пусть тг — древовидное доказательств множества неравенств На11„ в некоторой 11(СР)-подобной системе доказательств Тогда \тх\ > где VV — максимальный размер дизъюнк-

ции в тг

Четвертая глава поевящеяа сложности полуалгебраических систем доказательств старших степеней с ограниченной степенью ложности В первом разделе мы доказываем верхние полиномиальные оценки в Ь32+СР2 на размер доказательств со степенью ложности, ограниченной корнем от количества переменных, формул, кодирующих принцип Дирихле, и ослабленный принцип нераскрашиваемости графа, содержащего клику Для этого мы переделываем короткие ЬБ2+СР2-доказательства, описанные в работе Д Ю Григорьева и др 2002 г, в доказательства с ограниченной степенью ложности

В разделе 4 2 мы показываем, как доказательство в ЬБ^+СР'1 можно переделать в доказательство в Пеэ(А;) (обобщение резолюционнои системы доказательств, оперирующей формулами в А;-ДНФ) Получаемый результат представляет собой обобщение результата Э А Гирша и С И Нико-ленко 2005 г

Объединяя результат из предыдущею раздела с нижней экспоненциальной оценкой для Ыез(/;), доказанной М Алехновичем в 2005 г, в разделе 4 3 мы доказываем нижнюю экспоненциальную оценку для ЬЗ^+СР*-со степенью ложности, ограниченной линейной от количества переменных функцией, для цейтинских формул построенных по матрицам-расширителям (обобщениях графов-расширителеи)

Для множества строк I матрицы А £ {0,1}тхп мы определим его границу 81 как множество всех столбцов J матрицы А, таких что существует в точности одна строка г £ / для которой аг} — 1, для некоторого 7 £ 3, в то время как для всех остальных г' £ г' ф г, выполняется а%'у] = 0 Мы будем говорить, что А является (г, 5, с)-гранучным расширителем, если 1 любая строка содержит по крайней мере й единиц, 2 дтя любого множества строк

I размера по крайней мерс г выполняется \д1\ > с |/| Пусть Ь обозначает некоторый вектор из {0,1}" Тогда Ф(А,Ь) будет обозначать равенство Ах = b по модулю 2, где каждое равенство ®,^1а1Нх]1 = Ьг представляется в виде 2s эквивалентных дизъюнкций на переменных x3l, ,хи

Теорема 4 3 Существует такая положительная постоянная 5, что формула Ф(Л, b) для (Г2(п/Д), 3, с)-расширителя А, в котором любой столбец содержгт по крайней мере Д единиц, имеет в LSfc+CPfc со степенью ложности, ограниченной 6п, доказательство только размера exp(f](n))

Работы автора по теме диссертации

1 Кожевников, А А Нижние оценки на длину вывода цейтинских формул в статической системе доказатепьств Ловаса-Схрайвера

/ДМ Ицыксон, А А Кожевников // Записки научных семинаров ПОМИ

- СПб 2006 - Т 340 - С 10-32

2 Kojevnikov, A Several notes on the power of Gomory-Chvatal cuts / E A Hirsch, A Kojevnikov // Annals of Pure and Applied Logic — Elsevier 2006 - Vol 411, №3 - P 429-436

3 Kojevnikov, A Several notes on the powei of Gomory-Chvatal cuts / E A Husch, A Kojevnikov — Electronic Colloquium on Computational Complexity - 2003, January - TR012 - 10 p

4 Kojevnikov, A Improved Lower Bounds for Resolution over Linear Inequalities / A Kojevnikov — Electronic Colloquium on Computational Complexity - 2007, January - TR010 - 10 p

5 Kojevnikov, A Exponential Lower Bound on the Size of Static Lovasz-Schrijver Calculus / A Kojevnikov, D Itsykson // Proceedings of the 33rd International Colloquium on Automata, Languages and Programming — Springer 2006 ~ LNCS 4052 - P 323-334

6 Kojevnikov, A Complexity of Semialgebraic Proofs with Restricted Degree of Falsity / A Kojevnikov, A S Kulikov /,' Proceedings of the 9th International Conference on Theory and Applications of Satisfiability Testing

- Springer 2006 - LNCS 4121 - P 11-21

Подписано в печать с оригинал-макета 10 04 07 Формат 60x84/16 Бумага офсетная Печать ризографическая Уел печ л 0,8 Тираж 100 экз Заказ №1004/01-Р

Мшш-типография «Знак» издательства «Знак» 191025, Санкт-Петербург, ул Восстания, д 6 тел (812) 579-0891, 579-38-50

Введение

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

Статические полуалгебраические системы доказательств.

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

Полуалгебраические системы с ограниченной степенью ложности

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

1 Используемые системы доказательств и семейства тавтологий

1.1 Пропозициональные системы доказательств.

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

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

1.4 Статические полуалгебраические системы доказательств

1.5 Полуалгебраические системы доказательств генценовского типа.

1.6 Понятие степени ложности.

1.7 Понятия и обозначения теории графов.

1.8 Формулы, кодирующие принцип Дирихле.

1.9 Формулы, кодирующие принцип нераскрашиваемости графа, содержащего клику.

1.10 Цейтинские формулы на графах-расширителях.

2 Сложность статических полуалгебраических систем

2.1 Короткое статическое доказательство тавтологии о нераскрашиваемости графа, содержащего клику.

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

2.2.1 Процедура очищения расширителей.

2.2.2 Линейная нижняя оценка на булеву степень вывода биномиальных цейтипских формул в системе доказательств PS

2.2.3 Нижние оценки на булеву степень PS-доказательства биномиальных цейтинских формул.

2.2.4 Преобразование доказательства цейтинских формул в статической LS+ в доказательство в PS.

2.2.5 Нижняя экспоненциальная оценка на размер доказательства в статической LS+

3 Сложность полуалгебраических систем генценовского типа

3.1 Полиномиальная эквивалентность R(L&P) и R(LP), связь R(CP) и R(LP).

3.2 Полиномиальное моделирование L&Pi в CPi.

3.3 Доказательство полиномиального размера цейтинских формул в R(LP).

3.4 Вещественная коммуникационная сложность и нижние экспоненциальные оценки для R(CP).

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

4.1 Верхние полиномиальные оценки на размер доказательств принципа Дирихле и принципа нераскрашиваемости графа, содержащего клику.

4.2 Полиномиальное моделирование LS^'+CP^ с ограниченной степенью ложности в Res (к).

4.3 Нижние экспоненциальные оценки для LSfc+CPfc с линейной от количества переменных степенью ложности.

Необходимость математического изучеиия понятия доказательства была сформулирована и обоснована Д. Гильбертом совместно с П. Бер-найсом в "Основаниях математики". Д. Гильберта интересовала непротиворечивость всей математики и, в частности, непротиворечивость доказательств основных теорем. Для того, чтобы проверить корректность доказательства за разумное время, необходимо, чтобы само доказательство было разумного размера. Отсюда возникает важный вопрос о сложности систем доказательств, изучение которого было инициировано работой [21]: в естественном предположении, что каждый шаг доказательства проверяется за полиномиальное время, требуется оценить количество шагов доказательства.

Пропозициональной системой доказательств называется система доказательств для языка TAUT пропозициональных тавтологий в ДНФ. Поскольку такой язык содержится в co-NP, то любую систему доказательств для co-NP-трудного языка L можно считать пропозициональной системой доказательств, для этого необходимо лишь зафиксировать конкретное сведение.

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

Одними из самых известных системам доказательств являются системы Фреге, к которым, например, относятся системы гильбертовского типа и генцсновская система с правилом сечения. С. А. Кук и Р. А. Рекхоу в [21] доказали, что различные системы Фреге полиномиально моделируются друг в друге. Для них, в частности, известны верхние полиномиальные оценки для семейств формул, кодирующих принцип Дирихле [1G] и нераскрашиваемость графа, содержащего клику [54], имеющих экспоненциальную сложность, например, в резолюционной системе доказательств.

Для частного случая систем Фреге, систем Фреге ограниченной глубины, доказано несколько экспоненциальных нижних оценок [52,12,13,18, 45]. Эти системы отличаются от исходных константными ограничениями на глубину промежуточных формул.

Многие системы доказательств не имеют коротких выводов простых фактов, например, известная резолюционная система доказательств, введённая в [55], не имеет короткого доказательства принципа Дирихле. С другой стороны, можно естественным образом переписать данную формулу в виде системы линейных неравенств, например, записав каждую дизъюнкцию следующем образом:

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

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

Первая полуалгебраическая система доказательств, "секущие плоскости" (CP), оперирующая только линейными неравенствами, была введена в 6070 годах прошлого века в работах [26,19, 22]. Система основана на простом соображении о том, что сумма целых чисел также должна быть целым числом. Доказательство нижней экспоненциальной оценки для системы "секущие плоскости" долгое время оставалось важным открытым вопросом. В работе [25] была доказана нижняя экспоненциальная оценка для CP с ограниченной степенью ложности (т.е. с ограничением на свободный член неравенства), в работах [15, 41] для CP с унарными (полиномиально ограниченными) коэффициентами, в работах [36, 43] для древовидных "секущих плоскостей", в которых мы не имеем возможности использовать уже доказанные факты многократно и обязаны выводить их каждый раз заново. Для системы без ограничений нижняя экспоненциальная оценка была доказана в [53] для формул, кодирующих ослабленный принцип нераскрашиваемости графа, содержащего клику. Нижняя экспоненциальная оценка для системы "поднять и спроецировать" (L&P) [9], что также оперирует только линейными неравенствами, была доказана техникой, аналогичной технике доказательства вышеупомянутых нижних оценок для CP, в работе [24].

В разделе 3.2 данной диссертации приводится способ преобразования Ь&Р-доказательства в доказательство в CP размера, полиномиально зависящего от размера исходного доказательства и коэффициентов в нём, из которого следует, например, альтернативный метод доказательства нижней экспоненциальной оценки для системы L&Pi с унарными коэффициентами.

Для системы Ловаса-Схрайвера (LS) [48, 47], оперирующей квадратичными неравенствами, нижние экспоненциальные оценки были известны только для древовидных доказательств систем неравенств, не обладающих короткой записью в виде булевой формулы (один из результатов работы [30]). Также было известно несколько условных нижних оценок: для системы, объединённой с CP [54], и для древовидной версии системы [И]. Описанные выше системы можно усилить, позволив им оперировать неравенствами старших степеней [30].

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

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

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

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

Вторая глава диссертации также содержит короткое статическое доказательство в LS+ четвёртой степени формулы, кодирующей ослабленный принцип нераскрашиваемости графа, содержащего клику. Из этого следует, что статическая система LS+ экспоненциально сильнее системы СР. Данный результат можно рассматривать, как усиление полиномиальной верхней оценки для системы LS+, оперирующей неравенствами четвёртой степени, для аналогичных тавтологий, предложенный в [30].

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

Полуалгебраическая система генценовского типа R(6) [42] представляет собой естественное усиление 6 — любой из известных ранее полуалгебраических систем — позволяющее работать с предположениями: можно предположить, что сумма мономов с целочисленными коэффициентами / больше чем целое с или, наоборот, / не больше чем с и вывести в каждом предположении противоречие. Через R(LP) мы будем обозначать генце-новское расширение системы, оперирующей исключительно правилом сложения с неотрицательными коэффициентами. Хотя LP не является полной пропозициональной системой (в ней нельзя вывести все тавтологии из TAUT) и для неё существуют эффективные алгоритмы поиска доказательства (первый из которых был предложен JI. Г. Хачияном), её ген-ценовское расширение является полной системой доказательств.

Третья глава целиком посвящена исследованию полуалгебраических систем генценовского типа: в первом разделе доказывается полиномиальная эквивалентность систем R(LP) и R(L&P), а так же R(LPi) и R(CPi) с унарными коэффициентами, в следующем разделе приводится доказательство верхней полиномиальной оценки на размер R(LP)-дoкaзaтeльeтв цейтинских тавтологий. Идея последнего доказательства взята из работы [30], где аналогичная верхняя оценка доказывалась для систем LS больших степеней.

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

Я. Крайчек в [42] доказал экспоненциальную нижнюю оценку на размер ЩСР^-доказательств при условии, что каждая дизъюнкция содержит не более, чем 0(пе) неравенств, где п — количество переменных в выводимой формуле. С. Даш в [23, 24] приводит доказательства нижних экспоненциальных оценок на размер доказательств в ограниченной версии древовидной R(L&P). Мы расширяем его оценку для всех древовидных R(6), оперирующих дизъюнкциями линейных неравенств при помощи правил с константным количеством посылок.

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

Полуалгебраические системы с ограниченной степенью ложности

В работе [25] было введено естественное ограничение на количество дизъюнкций, при помощи которых можно записать данное линейное неравенство, называемое степень ложности линейного неравенства. Неформально, если d — степень ложности данного линейного неравенства с п переменными, то его можно эквивалентно записать при помощи (^Д) дизъюнкций.

В настоящей диссертации мы обобщаем понятие степени ложности на случай неравенств больших степеней и исследуем сложность систем LSfc+CPfc, оперирующих неравенствами степени не превосходящей к с ограниченной степенью ложности при помощи правил LS и СР. В первом разделе четвёртой главы мы доказываем верхние полиномиальные оценки на размер Ь82+СР2-доказательств со степенью ложности, ограниченной корнем от количества переменных, формул, кодирующих принцип Дирихле, и ослабленный принцип нераскрашиваемости графа, содержащего клику. Для этого мы переделываем короткие Ь82+СР2-доказательства, описанные в работе [30], в доказательства с ограниченной степенью ложности.

В разделе 4.2 показано как доказательство в LSfc+CPfc с ограничением на степень ложности можно переделать в доказательство в Res (к) (обобщение резолюционной системы доказательств, оперирующей формулами в fc-ДНФ). Получаемый результат представляет собой обобщение результата [34].

Объединяя результат из предыдущего раздела с нижней экспоненциальной оценкой для Res (к), доказанной в [4], в разделе 4.3 мы показываем нижнюю экспоненциальную оценку для LS^'-f СРА со степенью ложности, ограниченной линейной от количества переменных функцией, для цейтинских формул, построенных по графам-расширителям.

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

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

1. Кожевников, А. А. Нижние оценки на длину вывода цейтинских формул в статической системе доказательств Ловаса-Схрайвера / Д. М.Ицыксон, А.А.Кожевников // Записки научных семинаров ПОМИ. - СПб.: 2006.- Т. 340.- С. 10-23.

2. Маргулис, Г. А. Явные конструкции расширителей / Г. А. Мар-гулис // Проблемы передачи информации. — 1973. — Т. 9, № 4. — С. 71-80.

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

4. Alekhnovich, М. Lower bounds for k-DNF resolution on random 3-CNFs / M. Alekhnovich // Proceedings of the 37th annual ACM symposium on Theory of computing. — ACM Press: 2005. — P. 251-256.

5. Alekhnovich, M. Pseudorandom generators in propositional proof complexity / M. Alekhnovich, E. Ben-Sasson, A. A. Razborov and A. Wigderson // SIAM Journal on Computing. 2004. - Vol.34 № 1. - P. 67-88.

6. Alekhnovich, M. Exponential lower bounds for the running time of DPLL algorithms on satisfiable formulas / M. Alekhnovich, E. A. Hirsch and D. Itsykson // Journal of Automated Reasoning. — Springer: 2005. Vol. 35 № 1-3. - P. 51-72.

7. Alekhnovich, M. Resolution is not automatizable unless WP] is tractable / M. Alekhnovich and A. A. Razborov // Proceedings of the 42nd Annual IEEE Symposium on Foundations of Computer Science. — 2001. P. 210-219.

8. Atserias, A. On the automatizability of resolution and related propositional proof systems / A. Atserias and M. L. Bonet // Informationand Computation. 2004. - Vol. 189 № 2. - P. 182-201.

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

10. Beame, P. Lower bounds on Hilbert's Nullstellensatz and propositional proofs / P. Beame, R. Impagliazzo, J. Krajicek, T. Pitassi and P. Pudlak. Proc. London Math. Soc. 1996. - Vol. 73 № 3. - P. 1-26.

11. Ben-Sasson, E. Hard examples for bounded depth Frege / E. Ben-Sasson // Proceedings of the 34th Annual ACM Symposium on Theory of Computing. 2002. - P. 563-572.

12. Ben-Sasson, E. Lower bounds for bounded depth Frege proofs via Buss-Pudlak games / E. Ben-Sasson and P. Harsha. — Electronic Colloquium on Computational Complexity. 2003. - TR004. - 16 p.

13. Ben-Sasson, E. Short proofs are narrow — resolution made simple / E. Ben-Sasson and A. Wigderson // Journal of ACM. 2001. - Vol. 48 № 2. - P. 149-169.

14. Bonet, M. Lower Bounds for Cutting Planes Proofs with Small Coefficients / M. Bonet, T. Pitassi and R. Raz // The Journal of Symbolic Logic. 1997. - Vol. 62 № 3. - P. 708-728.

15. Buss, S. R. Polynomial size proofs of the propositional pigeonhole principle / S. R. Buss // The Journal of Symbolic Logic. — 1987. — Vol. 52 № 4. P. 916-927.

16. Buss, S. R. Linear gaps between degrees for the polynomial calculus modulo distinct primes / S. R. Buss, D. Grigoriev, R. Impagliazzo, andT. Pitassi // JCSS. 2001. - Vol. 62. - P. 267-289.

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

18. Chvatal, V. Edmonds polytopes and a hierarchy of combinatorial problems / V. Chvatal // Discrete Mathematics. — 1973. — Vol. 4. — P. 305-337.

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

20. Cook, S. A. The relative efficiency of propositional proof systems / S. A. Cook and R. A. Reckhow // The Journal of Symbolic Logic. — 1979. Vol. 44 № 1. - P. 36-50.

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

22. Dash, S. On the Matrix Cuts of Lovasz and Schrijver and their use in Integer Programming : PhD thesis / S. Dash. — 2001. Rice University Technical Report 01-08.

23. Dash, S. An exponential lower bound on the length of some classes of branch-and-cut proofs / S. Dash // Proceedings of IPCO 2002. — Springer: 2002. LNCS 2337. - P. 145-160.

24. Goerdt, A. The Cutting Plane Proof System with Bounded Degree of Falsity / A. Goerdt // Proceedings of CSL 1991. Springer: 1991. -LNCS 626. - P. 119-133.

25. Gomory, R.E. An algorithm for integer solutions of linear programs / Ralph E. Gomory; Editors R. L. Graves and P. Wolfe. — Recent Advancesin Mathematical Programming. McGraw-Hill: 1963. - P. 269-302.

26. Grigoriev, D. Linear lower bound on degrees of Positivstellensatz Calculus proofs for the Parity / D. Grigoriev // TCS. 2001. - Vol. 259. - P. 613-622.

27. Grigoriev, D. Complexity of Null- and Positivstellensatz Proofs /D. Grigoriev and N. Vorobjov// APAL. 2001. - Vol. 113 № 1-3. -P. 153-160.

28. Grigoriev, D. Algebraic proof systems over formulas / D. Grigoriev andE. A. Hirsch // TCS. 2003. - Vol. 303 № 1. - P. 83-102.

29. Grigoriev, D. Complexity of semi-algebraic proofs / D. Grigoriev, E. A. Hirsch, and D. V. Pasechnik // Moscow Mathematical Journal.- M., 2002. Vol. 2 № 4. - P. 647-679.

30. Haken, A. The intractability of resolution / A. Haken // TCS. 1985.- Vol. 39. P. 297-308.

31. Hirsch, E. A. Several notes on the power of Gomory-Chvatal cuts / E. A. Hirsch and A. Kojevnikov // Electronic Colloquium on Computational Complexity. — 2003, January. — TR012. — 10 p.

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

33. Hirsch, E. A. Simulating Cutting Plane proofs with restricted degree of falsity by Resolution / E. A. Hirsch and S. I. Nikolenko // Proceedings of SAT 2005. Springer-Verlag: 2005. - LNCS 3569. - P. 135-142.

34. Impagliazzo, R. Lower Bounds for the Polynomial Calculus and the Groebner Basis Algorithm / R. Impagliazzo, P. Pudlak and J. Sgall // Computational Complexity. 1999. - Vol. 3 № 2. - P. 127-144.

35. Impagliazzo, R. Upper and Lower Bounds for Tree-like Cutting Planes Proofs / R. Impagliazzo, T. Pitassi and A. Urquhart // Proceedings of Symposium on Logic in Computer Science. — IEEE: 1994. — P. 220-228.

36. Karchmer, M. Monotone circuits for connectivity require super-logarithmic depth / M. Karchmer and A. Wigderson // SIAM Journal on Discrete Mathematics. 1990. - Vol. 3 № 2. - P. 255-265.

37. Kojevnikov, A. Exponential Lower Bound on the Size of Static Lovasz-Schrijver Calculus / A. Kojevnikov, D. Itsykson // Proceedings of the 33rd International Colloquium on Automata, Languages and Programming. — Springer: 2006. LNCS 4052. - P. 323-334.

38. Kojevnikov, A. Improved Lower Bounds for Resolution over Linear Inequalities / A. Kojevnikov. — Electronic Colloquium on Computational Complexity. 2007, January. - TR010. - 10 p.

39. Kraji'Cek, J. Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic / J. Krajicek // Journal of Symbolic Logic. 1997. - Vol. 62 № 2. - P. 457-486.

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

41. Krajicek, J. Interpolation by a game / J. Krajicek // Mathematical Logic Quarterly. 1998. - Vol. 44 № 4. - P. 450-458.

42. Krajicek, J. On the weak pigeonhole principle / J. Krajicek // Fundamenta Mathematicae. 2001. -Vol. 170 № 1-3. - P 123-140.

43. Krajicek, J. An exponential lower bound to the size of bounded depth Frege proofs of the pigeonhole principle / J. Krajicek, P. Pudlak and A. Woods // Random Structures and Algorithms. — 1995. — Vol. 7 № 1.- P. 15-39.

44. Kushilevitz, E. Communication Complexity / E. Kushilevitz andN. Nisan. — 1997. — Cambridge University Press. — p. 189.

45. Lovasz, L. Stable sets and polynomials / L. Lovasz // Discrete Mathematics. 1994. - Vol. 124. - P. 137-153.

46. Lovasz, L. Cones of matrices and set-functions and 0-1 optimization / L. Lovasz and A. Schrijver // SIAM J. Optimization. 1991. - Vol. 1 № 2. - P. 166-190.

47. Lubotzky, A. Ramanujan graphs / A. Lubotzky, R. Phillips and P. Sarnak // Combinatorica. 1988. - Vol. 8 № 3. - P. 261-277.

48. Murty, R. Ramanujan graphs / R. Murty // Journal of the Ramanujan Math. Society. 2003. - Vol. 18 № 1. - P. 1-20.

49. Pitassi, T. Algebraic propositional proof systems / T. Pitassi // Descriptive complexity and finite models (Princeton, NJ, 1996); DIMACS Series in Discrete Mathematics and TCS. — Amer. Math. Soc., Providence: 1997. Vol. 31. - P. 215-244.

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

51. Pudlak, P. Lower bounds for resolution and cutting plane proofs and monotone computations / P. Pudlak // Journal of Symbolic Logic. — 1997. Vol. 62 № 3. - P. 981-998.

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

53. Robinson, J. A. The generalized resolution principle / J. A. Robinson // Machine Intelligence. — American Elsevier: 1968. — Vol 3. — P. 77-94.

54. Segerlind, N. A Switching Lemma for Small Restrictions and Lower Bounds for k-DNF Resolution / N. Segerlind, S. R. Buss, and R. Impagliazzo // SIAM Journal on Computing. 2004. - Vol. 33 № 5.- P. 1171-1200.

55. Urquhart, A. Hard examples for resolution / A. Urquhart // Journal of ACM. 1987. - Vol. 34 № 1. - P. 209-219.