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

Содержание к диссертации

Введение

1 Основные понятия 20

1.1 Основные обозначения 20

1.2 Классы сложности 21

1.3 Системы доказательств

1.3.1 Язык UNSAT 23

1.3.2 Резолюционная система доказательств 24

1.3.3 Система доказательств секущих плоскостей 25

1.3.4 Система доказательств полиномиального исчисления 26

1.3.5 Резолюционная система доказательств с резолюцией по линейным формам Res-Lin 27

1.4 Алгоритмы для SAT и деревья расщеплений 27

1.4.1 DPLL алгоритм 27

1.4.2 Алгоритм линейных расщеплений 29

1.5 Задача выполнения ограничений 30

1.6 Графы 33

2 Верхние оценки для резолюционных систем доказательств 34

2.1 Формулы для принципов Дирихле и совершенного паросо четания 35

2.1.1 Принцип Дирихле 35

2.1.2 Принцип совершенного паросочетания

2.2 Верхняя оценка на принцип совершенного паросочетания в общей резолюции 37

2.3 Верхние оценки на древовидные доказательства в системе Res-Lin

2.3.1 Принцип Дирихле 41

2.3.2 Принцип совершенного паросочетания 46

3 Резолюционные системы доказательств над произвольным алфавитом 50

3.1 Нижняя оценка на минимальную ширину доказательств в системе NG-Res 51

3.2 Обобщенные цейтинские формулы 53

3.3 Нижняя оценка на обобщенные цейтинские формулы

3.3.1 Сокращенное дерево расщеплений 56

3.3.2 Нижняя оценка 58

3.4 Верхняя оценка на древовидные резолюционные доказа тельства 60

4 Доказательствасправилом сдвига 64

4.1 Подвижные формулы и системы доказательств с правилом сдвига 65

4.2 Нижние оценки на размер доказательств с правилом сдвига

4.2.1 Кодировка 68

4.2.2 Нижние оценки для систем, устойчивых к замене переменных 70

4.2.3 Устойчивость к замене переменных 75

4.3 Разделение систем доказательств с правилом сдвига и без

него 79

4.3.1 Формула–счетчик 79

4.3.2 Верхняя и нижняя оценки 81

Заключение 87

Литература

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

Введение к работе

Актуальность темы. Теория сложности доказательств — одна из активно развиваемых областей математической логики. В рамках теории изучаются формальные системы доказательств.

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

Резолюционная система доказательств (Res) — одна из наиболее изученных систем. Впервые система была введена Блэком в 1938 г. и позднее популяризована в работах Дэвиса и Путнама в 1960 г. и Робинсона в 1965 г.

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

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

В 1968 г. Цейтин получил первые суперполиномиальные нижние оценки для резолюционных систем доказательств регулярного вида. Трудные формулы кодировали утверждение, что сумма степеней вершин графа нечетна; такие формулы называют цейтинскими. В 1987 г. Уркухарт показал для цей-

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

Первые экспоненциальные нижние оценки для резолюций в общем виде получил Хакен в 1985 г. В качестве трудных формул использовался принцип Дирихле. Формула PHP кодирует утверждение, что можно посадить т кроликов в п клеток так, чтобы в каждой клетке сидело не более одного кролика. При т > п формула невыполнима. Хакен показал, что формула PHP^_₁ имеет резолюционное доказательство размера 2^^п>. В 1988 г. Басс и Туран показали нижнюю оценку 2^^п '^т> для формулы PHP. В 1999 г. Басс и Пи-

тасси показали, что формула PHP имеет доказательство размера 2^^п> при

т = 2v^nlogn. Также Басс и Питасси показали, что для любых т > п формула PHP имеет резолюционное доказательство размера 2^^п, что показало точность уже полученных нижних оценок.

В 2004 г. Разборов рассмотрел формулу для принципа совершенного па-росочетания PMP^. Формула PMPс выполнима тогда и только тогда, когда в графе G есть совершенное паросочетание.

Разборов показал, что формула PMPс имеет минимальное резолюционное доказательство размера 2ⁿ^^^G''^{log п}, где п — число вершин в графе, а 8(G) — минимальная степень графа. Данчев и Риис в 2001 г. и Алекнович в 2004 г. рассмотрели задачу замощения домино шахматной доски с двумя выколотыми угловыми клетками. Для доски размера 2п х 2п соответствующие формулы содержат (п²) переменных и эквивалентны PMP^. Авторы показали нижнюю оценку 2^^п> на размер резолюционного доказательства.

В 2015 г. Ицыксон, Слабодкин и Соколов показали, что если взять специальный двудольный граф c п и т = 0(п) вершинами в долях при т > п, и степень каждой вершины будет ограничена константой, то любое резолюционное доказательство формулы PMPс будет иметь размер хотя бы 2^^п>.

Как следствие, авторы получили нижнюю оценку 2^^п> для двудольной клики К_щт при т = 0(п) и клики i^n+i.

Для произвольного графа G на п вершинах известна тривиальная верхняя оценка 2(^nlogn) для формул РМР^.

Вопрос 1. Является ли нижняя оценка 2^^п> для формулы РМР^ точной или ее можно улучшить?

В 2014 г. Ицыксон и Соколов рассмотрели расширение DPLL алгоритма — алгоритм линейных расщеплений. Алгоритм линейных расщеплений ищет выполняющий набор для пропозициональной формулы ф. Алгоритм поддерживает систему линейных уравнений Ф над полем F2, изначально пустую. Выполняющий набор ищется среди решений системы Ф. Алгоритм работает рекурсивно; на каждом шаге выбирается линейная комбинация ф_іє/ Хі для некоторого множества индексов /ив одном рекурсивном запуске в систему добавляется уравнение ф_іє/ Хі = 0, в другом — ф^_є/ Хі = 1. Если система оказывается несовместна или какой-либо дизъюнкт не имеет выполняющего набора среди решений Ф, алгоритм откатывается на шаг назад.

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

Фі_є/ Хі = 0 V Сі ф_іє/ Хі = 1 V С<і С\ V С2

Сами линейные уравнения появляются в результате правила ослабления:

С D'

где дизъюнкция линейных уравнений D семантически следует из С.

В своей работе авторы показали, что древовидное доказательство в системе Res-Lin эквивалентно протоколу работы алгоритма линейных расщеп-

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

Примеры, основанные на системах линейных уравнений, оказываются простыми для Res-Lin. В 2014 г. Ицыксон и Соколов доказали экспоненциальную нижнюю оценку 2^^п> на размер древовидного доказательства Res-Lin для формулы PHP⁺¹. В 1999 г. Ивама и Миязаки показали, что минимальное древовидное доказательство в системе Res для PHP⁺¹ имеет размер 2^e>^^nlogn'.

Вопрос 2. Является ли нижняя оценка 2^^п> на размер древовидного доказательства формулы PHP в системе Res-Lin точной или ее можно улучшить?

Резолюционные системы доказательств не ограничиваются пропозициональными формулами. В 2002 г. Митчелл рассмотрел резолюционную систему доказательств NG-Res для задачи выполнения ограничений (CSP). CSP состоит из множества переменных X и набора ограничений S, которые зависят от этих переменных. Переменные X принимают значения из некоторого фиксированного алфавита D. Размер D может быть больше двух. Задача состоит в поиске подстановки р : X —> D, которая бы выполнила все ограничения.

Ограничения, имеющие вид (xi = (Т\ Л Х2 = о"2 Л Л Xt = (Jt), где (Ті Є D для і Є [і\, будем называть запрещающими наборами. Запрещающий набор N соответствует ограничению / Є S, если (1) множества переменных, от которых зависят / и N, совпадают; (2) любая подстановка выполняющая /, выполняет N.

Доказательство в системе NG-Res — это последовательность запрещающих наборов, каждый из которых соответствует ограничению из S, выводится по правилу резолюции (принимает к = \D\ посылок в отличии от Res):

(x = а\ Л а,\) (х = a,k Л ak) («і Л «2 Л Л а^

или по правилу ослабления:

(а Л х = а)

Последний запрещающий набор — тождественно ложный.

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

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

Теорема 1 (Митчелл, 2002). Для CSP 0, зависящей от п переменных, выполняются следующие неравенства:

5т() > 2^ww^>^w№\ (1)

3(ф) > ехр ( Q (—^—^ )) , (2)

где 5 и St — размеры минимальных доказательств в NG-Res общего вида и древовидного соответственно.

Для получения нижней оценки на минимальную ширину доказательства используют расширительную способность CSP. Пусть F — множество ограничений; обозначим dF множество переменных, от каждой из которых зависит ровно одно ограничение в F. Расширительная способность CSP ф

еЛФ) = min \dF\ ,

где минимум берется по всем множествам F таким, что ттт|5| < 1^1 < ттт15|.

t-\-i і і — і і — t-\-i і

Прямой перенос техники Бен-Сассона и Вигдерсона на CSP дает нижнюю оценку \(ф \- 0) > Єк{ф), где к — размер алфавита. Можно заметить,

что чем больше к, тем больше вариантов для подмножества F. Соответственно, с увеличением размера алфавита, значение Єк{ф) уменьшается.

Вопрос 3. Можно ли улучшить нижнюю оценку на ширину так, чтобы она не зависела от размера алфавита?

Для CSP 0, чувствительной к подстановкам, можно получить нижнюю оценку \(ф \- 0) > Є2(ф) — 1.

Расширительная способность цейтинской формулы Ts(G), построенной на графе G, совпадает с расширительной способностью графа G. Теорема Митчелла для расширенной версии формул дает нижнюю оценку 2^e2^^G>~^d~^l на размер древовидного доказательства в системе NG-Res, где d — максимальная степень графа. Кажется естественным, чтобы в основании степени стояло значение размер алфавита к, а не 2. Возможно, детальный анализ конкретной формулы может дать такую оценку.

Вопрос 4. Верно ли, что для невыполнимой цейтинской формулы Ts(G) можно показать нижнюю оценку k^e2^^G'~^d на размер древовидных доказательств в системе NG-Res?

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

Вопрос 5. Является ли расширительная способность формулы необходимым свойством, хотя бы на примере древовидных доказательств NG-Res?

Резолюционные системы доказательств находят свое применение в комбинаторике слов.

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

Задачу избегаемости можно переформулировать в терминах выполнимости пропозициональной формулы на бесконечном числе переменных

X-\XqX\ . Сопоставим каждой строке s Є Р счетное число дизъюнктов, каждый из которых запрещает подстроку s на конкретной позиции в бесконечной строке. Такие формулы будем называть подвижными, поскольку дизъюнкт как бы двигается вдоль строки.

Известно, что если запрещенные строки не содержат пропусков, то задача избегаемости решается за полиномиальное время методом Ахо-Корасика. В 2002 г. Лотар предложил систему вывода над строками: если бесконечная строка избегает строки хуО и у\ (или ху\ и г/0), где х и у — некоторые конечные строки, то она же избегает строку ху. Бесконечной строки не существует тогда и только тогда, когда можно вывести пустую строку.

В 2009 г. Бланше с соавторами показали, что задача избегаемости с пропусками NP-труда, Блэкели показал принадлежность PSPACE. В работе [1] мои соавторы Ицыксон и Охотин показали PSPACE-полноту задачи избегаемости и то, что отсутствие строки можно доказать в резолюционной системе доказательств с выводом размера 2^^п , где п — размер задачи.

Структура подвижной формулы позволяет расширить систему доказательств дополнительным правилом сдвига. Если есть вывод дизъюнкта х^а-^х V V х, то можно вывести сдвиг на j позиций х^₊- V V х*₊ для любого j Є Z.

Вопрос 6. Может ли правило сдвига существенно сократить размер доказательства подвижной формулы?

Аналогичное правило сдвига можно добавить в систему секущих плоскостей, полиномиального исчисления и другие

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

Цели работы.

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

2. Получить верхнюю оценку на принцип Дирихле для древовидных доказательств в системе Res-Lin, которая совпадает с нижней с точностью до константы в экспоненте.

3. Доказать нижнюю оценку на минимальную ширину доказательства в NG-Res, не зависящую от размера алфавита.

4. Показать, что для невыполнимой цейтинской формулы Ts(), построенной на графе с максимальной степенью , древовидное доказательство в системе NG-Res имеет нижнюю оценку ^2()-.

5. Построить верхнюю оценку на древовидные доказательства в системе NG-Res через расширительную способность CSP.

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

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

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

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

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

Основные результаты.

8. Доказано, что формула РМР^ для любого графа G на п вершинах без совершенного паросочетания имеет доказательство в системе Res размера 0(п² 2^П). Оценка совпадает с ранее известной нижней с точностью до константы в показателе экспоненты.

9. Доказано, что формула РНР при т > п имеет древовидное доказательство размера 2(^п> в системе Res-Lin. Оценка совпадает с нижней с точностью до константы в показателе экспоненты.

10. Доказано, что минимальная ширина доказательства чувствительных к подстановкам CSP ф ограничена снизу Є2(ф) — 1. Нижняя оценка не зависит от размера алфавита.

11. Доказано, что обобщенные цейтинские формулы Ts(G, /), построенные на основе графа G с максимальной степенью d и расширительной способностью Є2(С) над алфавитом размера к, имеют древовидные доказательства в NG-Res размера как минимум k^G2^~^d.

12. Показана формально необходимость расширительной способности графа для нижних оценок на древовидные доказательства в системе NG-Res. По CSP ф над алфавитом размера к можно построить граф зависимостей G = (V, Е), который описывает сколько общих переменных имеет каждая пара ограничений. Показано, что в графе G существует подграф Н такой, что древовидная сложность CSP ф в системе NG-Res не больше fce(tf)-iog_3/2N.

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

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

Апробация работы. Результаты диссертационной работы были изложены на следующих конференциях и семинарах.

14. Международная конференция “First Russian-Finnish Symposium on Discrete Mathematics” (Турку, RuFiDim 2012).

15. Международная конференция “The 8th International Computer Science Symposium in Russia” (Екатеринбург, CSR 2013).

16. Международная конференция “19th International Conference on Theory and Applications of Satisfability Testing” (Бордо, SAT 2016).

17. Международная конференция “41st International Symposium on Mathematical Foundations of Computer Science” (Краков, MFCS 2016)

18. Научный семинар в LIRMM, Университет Монпелье 2, 2016.

Публикации. Основные результаты диссертации опубликованы в рецензируемых научных изданиях — [1, , , ]. Работы [1, , ] написаны в соавторстве.

В работе [1] PSPACE–полнота задачи избегаемости принадлежит соавторам; диссертанту принадлежит доказательство теоремы о разделении систем доказательств с правилом сдвига и без него. При этом разделяющие формулы предложил Д.М. Ицыксон. Нижние оценки на системы доказательств с правилом сдвига получены диссертантом.

Работа [] написана в соавторстве с научным руководителем. Научному руководителю принадлежит постановка задачи, диссертанту принадлежит техническая часть всех доказательств.

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

Структура и объем работы. Диссертация состоит из введения, четырех глав, заключения и списка литературы. Общий объем диссертации — 95 страниц. Список литературы включает 45 наименования на 6 страницах.

Резолюционная система доказательств

Алгоритм линейных расщеплений, DPLL/ n, принимает на вход пропозициональную формулу ф в КНФ и систему линейных уравнений Ф над полем F2, изначально пустую; ищет выполняющую подстановку для формулы ф среди всех решений системы Ф. Если система Ф пуста, алгоритм решает задачу SAT. Алгоритм линейных расщеплений параметризуется двумя эвристиками А и В. Эвристика А по формуле ф и системе Ф выбирает множество индексов переменных /. Эвристика В по формуле 0, системе Ф и множеству индексов / выбирает значение а Є {0,1}.

Псевдокод алгоритма приведен на описании 2. Отметим, что проверки на совместность в строках 1 и 5 и на единственность решения в строке 9 осуществляются за полиномиальное время. Будем говорить, что система Ф нарушает дизъюнкт С, если любое решение Ф не выполняет дизъюнкт С. В строках 4-8 алгоритм проверяет, не нарушает ли система Ф хотя бы один дизъюнкт формулы ф.

Рассмотрим протокол работы алгоритма на невыполнимой формуле ф. Протокол можно представить в виде дерева. В каждом внутреннем узле записана линейная форма / = @ІЄІХІ. Каждое ребро помечено уравнением вида / = 0 или / = 1.

Мы сделаем допущение, что эвристика А(ф, Ф) всегда выбирает форму, линейно независимую от форм в системе Ф. Это значит, что алгоритм никогда не попадает внутрь условия на строке 1. Потому все листья дерева помечены дизъюнктами формулы ф. При этом система уравнений, составленная на пути от корня до листа, нарушает дизъюнкт в листе.

Описанное выше дерево назовем деревом линейных расщеплений. Минимальное дерево линейных расщеплений совпадает с минимальным древовидным доказательством в Res-Lin и совпадает с точностью до константы с минимальным временем работы алгоритма линейных расщеплений на невыполнимой формуле [25].

Пусть есть конечный алфавит D размера к и множество переменных X = {xi, Х2-, , жп}, которые принимают значения из алфавита. Пусть также есть множество предикатов (ограничений) S, которые зависят от переменных из X. Определение 1.5. Задача выполнения ограничений (consraint satisfaction problem, CSP) ф = (X,D,S) состоит в поиске подстановки р : X — D, выполняющей каждое ограничений из S.

В случае, когда алфавит бинарный, CSP совпадает с задачей выполнимости пропозициональной формулы. CSP невыполнима, если не существует подстановки р, выполняющей все ограничения одновременно. Определим запрещающий набор как ограничение, имеющее вид геї где / С [п] — подмножество индексов переменных, а,і Є D. Набор с / = 0 будем обозначать (True).

Пусть ограничение / Є S зависит от множества переменных Xf. Будем говорить, что запрещающий набор N соответствует ограничению /, если он использует все переменные Xf и подстановка, нарушающая N, нарушает /.

Определим резолюционную систему доказательств NG-Res для CSP. Пусть, для простоты, D = [к]. Система NG-Res оперирует запрещающими наборами. Доказательство в NG-Res определяется аналогично пропозициональной системе Res. Каждый запрещающий набор либо соответствует ограничению из S, либо выводится из предыдущих по следующим правилам вывода. Правило ослабления: ,сг (х = а Л а) Из запрещающего набора (о) можно вывести запрещающий набор (х = а Л а) при условии, что х не лежит в а. Правило резолюции: (х = 1 Л а і) (х = 2 Л о ) (х = к Л о ) (AaeDaa) Последний набор в доказательстве — пустой: (True). Кроме размера доказательства мы будем использовать понятие ширины. Ширина CSP ф — это максимальное число переменных от которых зависит ограничения ф. Ширина доказательства 7Г в системе NG-Res для CSP ф определяется как максимальное число переменных в отдельном запрещающем наборе N доказательства тт. Минимальная ширина доказательства \(ф \- 0) для СSP ф — это минимальная ширина по всем возможным доказательствам CSP ф.

Теорема 1.4 ([27]). Пусть CSP ф = (X, D, S) зависит от п переменных, каждое ограничение д Є S зависит не более чем от d переменных. Тогда 8т(Ф) 2W d1 3(ф) ехр Q - — где Зт{ф) — размер минимального древовидного доказательства в системе NG-Res для CSP 0, а 3(ф) — размер минимального доказательства общего вида в системе NG-Res для CSP ф. Определение 1.6. Пусть CSP ф = (X, D, S) невыполнима. Мы скажем, что CSP ф минимально невыполнима, если для любого ограничения / Є S CSP ф-f = (X, D,S — f) выполнима.

Пусть F С S — подмножество ограничений CSP ф = (X,D,S). Будем говорить, что переменная х лежит на границе F, если существует ровно одно ограничение / Є F, которое формально зависит от х. Множество всех переменных, которые лежат на границе F, обозначим dF.

Алгоритмы для SAT и деревья расщеплений

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

Теорема 2.4 ([25]). Пусть граф С содержит п вершин и п нечетно. Тогда формула РМР имеет дерево линейных расщеплений полиномиального от п размера.

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

Теорема 2.5. Пусть граф С = (V,E) связен, содержит п вершин и не имеет совершенного паросочетания. Тогда формула РМР имеет дерево линейных расщеплений размера 2 п .

Идея доказательства — свести принцип совершенного паросочетания к принципу Дирихле. Используя критерий Татта, мы можем выделить множество вершин S размера / в графе Gиm компонент связности Сь 2? Ст нечетного размера в графе G — S. При этом

Каждую компоненту мы отождествим с кроликом. Каждую вершину S — с клеткой. Кролик СІ отправляется в клетку Sj в случае, если число ребер в паросочетании между компонентой связности СІ и вершиной Sj нечетно.

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

Второй случай распадается на два подслучая.

Есть вершина Sj Є S такая, что вершину Sj и компоненту СІ соединяет ненулевое четное число ребер, лежащих в паросочетании. В этом подслучае мы обнаруживаем ребра, используя дерево полиномиального размера.

Ни одно ребро между СІ и S не лежит в паросочетании. В этом случае, мы используем дерево из теоремы 2.4, чтобы найти нарушенный дизъюнкт на компоненте связности Cj, как на графе нечетного размера.

Доказательство. Для доказательства теоремы 2.5 мы воспользуемся теоремой 2.1. Поскольку в графе С нет совершенного паросочетания, значит, есть подмножество 5 С У, такое, что число компонент связности нечетного размера в графе С — S больше, чем размер S.

Обозначим вершины множества S как si, S2, s/, а соответствующие компоненты как Сі, С -, Сто Для каждой компоненты связности СІ и вершины Sj, мы введем переменную m l. Рассмотрим формулу PHP, основанную на переменных yij, и дерево линейных расщеплений Ту размера 2", как это было сделано в Теореме 2.3. Поскольку / = 0(п), то размер дерева будет 2 .

Мы построим дерево линейных расщеплений Тх для формулы PMPс, используя структуру дерева Ту для формулы PHP. Заменим все переменные типа у на линейные формы соответствующих переменных типа х. В некоторых вершинах дерева Тх мы можем получить пустые линейные формы. Если в вершине v записана пустая форма, то на двух исходящих ребрах будут записаны два уравнения 0 = 1 и 0 = 0. Первое уравнение делает систему несовместной, потому соответствующая ветвь может быть обрезана. Ребро со вторым уравнением может быть стянуто, объединяя родителя и ребенка.

Рассмотрим произвольный лист / дерева Ту, помеченный дизъюнктом D\. Каждый лист / мы заменим на поддерево Т/ полиномиального от п размера. Каждое дерево Т/ находит нарушенные дизъюнкты формулы PKPQ. Структура дерева зависит от дизъюнкта D\. Возможны два случая.

Верхняя оценка на принцип совершенного паросочетания в общей резолюции

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

Мы будем работать с системами доказательств определенной формы, которые будем называть классическими. Классическая система доказательств П оперирует некоторым видом предикатов (дизъюнкты, неравенства, уравнения) и правилами вывода над ними. Будем называть такие предикаты заключениями. Доказательство формулы ф в системе П это последовательность заключений Pi, Р , PS. Каждое заключение либо равносильно дизъюнкту формулы 0, либо аксиома, либо следует по правилам вывода из предыдущих заключений. Правила вывода гарантируют семантическое следствие и проверяемы за полиномиальное время. Последнее заключение доказательства — тождественно ложный предикат.

Для примера, система секущих плоскостей оперирует неравенствами с целочисленными коэффициентами. Каждому дизъюнкту сопоставляется эквивалентное неравенство. Для каждой переменной определяются аксиомы х 0 и —х — 1. Также мы используем аксиому 0 — 1. Система использует три правила вывода: сложение неравенств, умножение на константу и деление с округлением. Полиномиальная проверяемость и семантическое следствие для правил очевидны. Последнее неравенство, 0 1, тождественно ложный предикат.

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

Рассмотрим отображение т:—) и{0,1}. Будем называть г заменой переменных, если любая переменная у которую заменили на другую переменную или константу (т(уі) = уі), сама не участвует в качестве замены (уІ ф т()).

Определим предикат Р(г/і15--- іУік)[т] после замены как Р(т(уі1) т(уік)). Определим формулу ф после замены как ФМ = с =фСЬ ]. Определение 4.1. Система является f -устойчивой к замене переменных, если для любой замены г и любого заключения системы такого, что Р[т] ф 1, соблюдаются три условия. 1. Предикат Р[т] является заключением в системе . 2. Если заключение Р — аксиома в системе , то и Р[т] — аксиома в системе . 3. Пусть заключение Р является результатом правила вывода из заключений Pi,--- , Р&, тогда заключение Р[т] имеет вывод размера не более чем / из нетривиальной части предикатов Рі[т],

Отметим, что если Р[т] ф 1, то хотя бы одно из заключений Рі[т], Рк[т] тоже нетривиально. Также отметим, что если предикат Р равносилен дизъюнкту С, то после любой замены г, предикат Р[т] равносилен дизъюнкту С[т]. Лемма 4.1. Если классическая система доказательств /-устойчива, то из доказательства 7Г формулы ф размера s можно построить доказательство 7г формулы ф[т] размера / s. Доказательство. Пусть 7Г = Pi, Р2, Ps — доказательство формулы ф в классической системе доказательств П, и г замена переменных.

Рассмотрим последовательность предикатов ТТ[Т] = PI[T],--- , PS[T]. Опустим все тривиальные предикаты. Получим последовательность 7г . По определению 4.1 каждый предикат последовательности 7г — заключение системы П. Пусть РІ[Т] ф 1. Если заключение Pi равносильно некоторому дизъюнкту С формулы 0, то РІ[Т] равносильно С[т]. Если заключение Д — аксиома системы П, то и РІ[Т] — тоже аксиома системы П. Если заключение Р{ — результат правила вывода в системе П, то заключение Р%\т\ имеет вывод размера не более чем / из предыдущих заключений в последовательности 7г . После замены переменных, тождественно ложное заключение остается тождественно ложным.

Таким образом, по последовательности ті можно построить доказа тельство тт" для формулы ф[т] размера не более / s.

Теорема 4.1. Пусть П — классическая система доказательств, /-устойчивая к замене переменных. Пусть формула фп имеет кратчайшее доказательство в системе П размера 5п ( / ). Тогда длина кратчайшего доказательства формулы W„ в системе bniit-11 как минимум \1 Л .

План доказательства. Мы докажем теорему следующим образом. Сначала мы возьмем доказательство формулы Фп и сделаем из него m = 4- (п+1) параллельных копий со всем возможными сдвигами на j для j Є [О, га — 1]. Затем, мы заменим каждую переменную уі в формуле и выводе на 2/imodm. За счет того, что у нас есть m параллельных копий, нам не потребуется использовать правило сдвига: для каждого дизъюнкта мы выводим одновременно все возможные сдвиги по модулю т.

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

Нижние оценки на размер доказательств с правилом сдвига

В этом разделе мы определим семейство невыполнимых подвижных формул {Фп}п 1. Формула Фп будет содержать полиномиальное от п число подвижных дизъюнктов. Размер любого классического доказательства без правила сдвига для формулы Фп составит Q(2n). При этом размер доказательства в системе Shift-Res будет всего лишь полиномиального от п размера.

Мы воспользуемся кодировкой, описанной в разделе 4.2.1. Каждая формула Фп будет содержать подформулу Shifts(Encn), выполнимую бесконечной строкой W-i$Wo$Wi, где Wi — блок из п цифр О и 1, задающий n-битный счетчик.

В формуле Фп мы определим дополнительную подформулу-инкремент, гарантирующую, что каждый блок больше предыдущего ровно на единицу. Кроме того, мы запретим старшему разряду любого блока быть равным единице. Очевидно, последовательность из 2n_1 + 1 бло ков не сможет выполнить все ограничения. Таким образом, формула Фп будет невыполнима.

Нам потребуется вспомогательная формула. Для каждого п 1 и каждого к Є [0, п — 1] определим формулу Step (a;o, жі, , хп-і, уо,Уі, ,2/п-і), которая принимает бинарное представление чисел х и у. При этом хо и уо — это младшие биты. Формула Step (a;o, Жі, , хп-і,уо,уі, ,2/n-i) будет выполнима тогда и только тогда, когда у = х + 2к по модулю 2П. Формула Step определяется конъюнкцией следующих условий. ХІ = УІ Уі Є {0,1, , к — 1}; Хк Ф У к] хг = уг - хг+і = уг+і Уі Є {к + 1, , п - 2}; а;8 ,Ла;, = 1 - хг+і ф уг+і Уі Є {к, ,n - 2}; жг уг Л жг = О - жг+і = уг+і Уі Є {/с, , п - 2}. Заметим, что каждое ограничение зависит не более, чем от четырех переменных, и формула Step имеет представление в КНФ размера 0(п). Введем дополнительное обозначение. Пусть есть формула ф = С\ Л С2 Л Л С к и дизъюнкт D. Припишем дизъюнкт D к каждому дизъюнкту ф и обозначим полученную формулу как OR(D, ф) = {С\ V D) Л (О2 V D) Л Л (С& V D). Мы определим формулу Фп как подвижное расширение конъюнкции четырех подформул. 1. Формула Encп из раздела 4.2.1; задает кодировку. 2. Формула OR(D$, Stepo( 8, Жі2, -jX n+A-, 4n+12, , #8n+8)), где D$ = x\ V Ж2 V Ж3 V Ж4 — дизъюнкт для выравнивания по сепаратору; задает инкремент между двумя соседними блоками. 3. Формула Vn; посимвольно задает следующий сепаратор относитель но предыдущего. Формула выводима из Encп, но нам удобнее запи сать ее в явном виде. Определяется следующими дизъюнктами: D$ V Ж4п+55 D$ V 4n+6, D$ V Ж4п+75 D$ V 4n+8 4. Формула Overn; запрещает единицу в старшем разряде: Overn = D$ V ж4п+4 Определим формулу Фп как Shifts(Encn Л OR(L $, Step) Л К Л Overn). 4.3.2 Верхняя и нижняя оценки Лемма 4.5. Пусть П — классическая система доказательств без правила сдвига. Минимальный вывод формулы Фп в системе П имеет размер Q(2n). Доказательство. Пусть вывод использует t дизъюнктов формулы Фп и опровергает соответствующую подформулу фп. Разобьем бесконечную строку на блоки пот = 4(п + 1) переменной в каждом. Скажем, что дизъюнкт затрагивает отрезок переменных, задаваемый минимальным и максимальным индексами переменных в дизъюнкте. Дизъюнкт затрагивает блок, если хотя бы одна переменная блока лежит внутри этого отрезка. По построению, каждый дизъюнкт формулы Фп затрагивает не более трех блоков. Разобьем все затрагиваемые блоки на последовательности без разрывов. Формулу фп можно разбить на независимые подформулы, каждая из которых соответствует такой последовательности. Пусть последовательность s = bob\ bk-i имеет длину к 2n_1, и ей соответствует формула ф8. Запишем в блоке ЬІ число І в двоичном виде. Очевидно, формула i/js будет выполнена.

Поскольку фп невыполнима, то существует последовательность дли ны хотя бы 2n_1 + 1. Значит, t 2n_1, и доказательство имеет размер Q(2n). Покажем верхнюю оценку для резолюционных доказательств с правилом сдвига. Нам потребуется следующая лемма. Лемма 4.6. Для любого п 1 и любого к Є [0,п — 2] из конъюнкции формул Step іУп—l) Step к(Уо іУіі іУп—іі а-і іі і Zn—і) можно вывести все дизъюнкты формулы Step +1(a;o, жі, , xn-i] zo, zi, , zn-i) с выводом размера 0(n). Доказательство. Пусть две формулы А и В, представленные в КНФ, зависят от константного числа переменных. Пусть формула А семантически следует из формула , тогда каждый дизъюнкт формулы А семантически следует из формулы В. По лемме 1.1 каждый дизъюнкт формулы А имеет вывод в резолюционной системе доказательств. Поскольку формула В зависит от константного числа переменных, вывод имеет константный размер.