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

Смирнов Петр Юрьевич
Бесплатно
В избранное
Работа доступна по лицензии Creative Commons:«Attribution» 4.0

Мы изучаем сложность цейтинских формул T(G, c), построенных на графах G(V, E). Основной рассматриваемой моделью вычислений в работе является однопроходная ветвящаяся программа (1-BP). Мы описываем структуру 1-BP, решающих задачу SearchVertex(G, c) поиска вершины с нарушенным условием чётности для невыполнимой T(G, c). По такой программе размера S мы строим:
(1) 1-BP размера S^O(log |V|), вычисляющую значение выполнимой T(G, c’);
(2) вывод отрицания формулы T(G, c) в системе Фреге константной глубины размера S * poly(|T(G, c)|).
Из (1) следует, что если размер регулярного резолюционного опровержения T(G, c) равен S, то размер 1-BP, вычисляющей значение выполнимой T(G, c’), не больше S^O(log |V|).

1. Введение 4
1.1. Пропозициональные доказательства . . . . . . . . . . . . 4
1.2. ЗадачаSearchφ ……………………. 6
1.3. Цейтинскиеформулы………………… 6
1.4. Древовидная резолюция и дерево решений . . . . . . . . 7
1.5. Регулярнаярезолюцияи1-BP……………. 8
1.6. Постановказадачи …………………. 10
1.7. Результатыиструктураработы…………… 10
2. Основные определения 12
2.1. Резолюционные системы доказательств . . . . . . . . . . 12
2.2. Диаграммыпринятиярешений …………… 13
2.3. Цейтинскиеформулы………………… 13
3. Структура 1-BP, вычисляющих SearchVertex(G, c) 16
3.1. Структурированные ветвящиеся программы . . . . . . . 16 3.2. Структурнаятеорема………………… 20
4. Построение 1-BP для T(G, c′) по 1-BP для SearchVertex(G, c) 29
5. Построение вывода ¬T(G, c) в системе Фреге константной глубины по 1-BP для SearchVertex(G, c) 35 5.1. СистемыФреге …………………… 35 5.2. Вспомогательныеутверждения …………… 36 5.3. Построениевывода …………………. 42
Заключение Список литературы
49 50

В этой работе мы изучаем сложность цейтинских формул T(G,c), построенных на графах G(V , E ). Основной рассматриваемой моде- лью вычислений будет однопроходная ветвящаяся программа (1-BP). Мы описываем структуру 1-BP, решающих задачу SearchVertex(G,c) поиска вершины с нарушенным условием чётности для невыполни- мой T(G,c). По программе размера S мы строим: (1) 1-BP размера SO(log |V |), вычисляющую значение выполнимой T(G, c′); (2) вывод фор- мулы ¬T(G, c) размера S · poly(|T(G, c)|) в системе Фреге константной глубины. Из (1) следует, что если размер регулярного резолюционного опровержения T(G, c) равен S, то размер 1-BP, вычисляющей значение выполнимой T(G, c′), не больше SO(log |V |).
1.1. Пропозициональные доказательства
Булевы функции f : {0, 1}n → {0, 1} (0 и 1 здесь и далее будем отож-
дествлять со значениями лжи и истины соответственно) можно запи-
сывать с помощью пропозициональных формул –– пропозициональных
переменных, соединённых логическими связками (конъюнкцией, дизъ-
юнкцией, отрицанием и другими). Конъюктивная нормальная форма
(КНФ) –– формула φ, записанная в виде m ( ni li,j ), где li,j –– литерал i=1 j=1
(пропозициональная переменная или её отрицание), а каждая скобка ( ni li,j) называется дизъюнктом φ.
j=1
Рассмотрим задачу проверки формулы в КНФ на выполнимость ––
то есть задачу проверки существования набора значений переменных, при подстановке которых формула обращается в истину. По теореме Кука-Левина [7, 16], эта задача является NP-полной.
Пусть мы каким-то образом узнали, выполнима ли формула, и те- перь хотим предъявить доказательство того, что ответ действительно такой. Если формула выполнима, достаточно предъявить выполняю- щий набор переменных.
Будем называть пропозициональной системой доказательств поли- номиальный алгоритм V (φ, w), который принимает формулу φ в КНФ
4
и строку w, возвращает 0 или 1 и обладает свойствами:
• Корректность: если V (φ, w) = 1, то φ невыполнима; w в этом слу-
чае называется доказательством φ.
• Полнота: если φ невыполнима, то существует строка w такая, что
V (φ, w) = 1.
Существует ли пропозициональная система доказательств, в кото- рой для любой невыполнимой формулы φ существует доказательство полиномиального от длины φ размера? В [6] было показано, что такая система доказательств существует тогда и только тогда, когда клас- сы сложности NP и coNP совпадают. В частности, если такой системы доказательств не существует, то классы P и NP различаются.
Основная программа исследований в теории сложности доказа- тельств заключается в доказательстве суперполиномиальных нижних оценок для как можно более сильных систем доказательств. Для мно- гих интересных из них неизвестны нетривиальные нижние оценки (для систем Фреге, для полуалгебраических систем высокой степени и пр.).
Нижние оценки на системы доказательств позволяют получать сложные примеры для алгоритмов, которые решают задачу выполни- мости. Так, алгоритмы расщепления (DPLL) эквивалентны древовид- ным резолюционным доказательствам, а современные используемые на практике алгоритмы, запоминающие конфликты (CDCL), соответству- ют резолюционным доказательствам общего вида.
Резолюционная система доказательств –– классическая система, ис- пользующая правило резолюции. Правило резолюции позволяет из дизъюнктов x∨A и ¬x∨B вывести дизъюнкт A∨B. Доказательством φ в резолюционной системе является вывод с помощью правила резолюции пустого дизъюнкта (то есть тождественно ложного) из дизъюнктов ис- ходной формулы. Размер доказательства –– это количество дизъюнктов в нём.
Доказательство называется древовидным, если любой выведенный дизъюнкт используется затем не более одного раза (чтобы использо- вать повторно, необходимо вывести его ещё раз). Доказательство на-
5

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

Таким образом, мы решили поставленные задачи: построили верхнюю оценку на 1-BP(T(G, c′)) по 1-BP(SearchVertex(G, c)), а значит и по SReg(T(G,c)); построили верхнюю оценку на ми- нимальный размер вывода ¬T(G,c) в системе Фреге констант- ной глубины по 1-BP(SearchVertex(G,c)). В частности, мы полу- чили два способа доказательства нижних оценок на сложность SearchVertex(G, c) для 1-BP: достаточно получить нижнюю оценку на размер 1-BP(SearchVertex(G, c)), либо на размер вывода ¬T(G, c) в си- стеме Фреге константной глубины.
Структурная теорема и теорема о построении 1-BP для T(G,c′) по 1-BP для SearchVertex(G,c) включены в статью [13]. Во второй части этой статьи для всех графов G доказывается нижняя оценка 1-BP(T(G, c′)) ⩾ 2Ω(tw(G)), где tw(G) –– древесная ширина графа G. Вме- сте с теоремой о перестроении, это даёт нижнюю оценку на минималь- ный размер регулярного резолюционного доказательства цейтинской формулы для любого графа G: SReg(T(G, c)) ⩾ 2Ω(tw(G)/ log |V |). Для гра- фов константной степени эта оценка оказывается почти точной: для них известна верхняя оценка SReg(T(G, c)) ⩽ 2O(tw(G))poly(|V |) [1].
Кроме того, в статье [13] строится семейство выполнимых цейтин- ских формул T(Gn, c′n) на графах Gn(Vn, En) константной степени, для которых 1-BP(T(Gn, c′n)) ⩾ 2Ω(tw(Gn) log |Vn|). При этом по [1] нам известно, что 1-BP(SearchVertex(Gn,cn)) ⩽ SReg(T(Gn,cn)) ⩽ 2O(tw(Gn))poly(|Vn|). Из этого следует, что при перестроении 1-BP для SearchVertex(G, c) в 1-BP для T(G, c′) нельзя избавиться от показателя степени log |V |.

[1] Michael Alekhnovich and Alexander A. Razborov. Satisfiability, branch-width and tseitin tautologies. Comput. Complex., 20(4):649– 678, 2011.
[2] Eli Ben-Sasson. Size space tradeoffs for resolution. In Proceedings of the Thiry-fourth Annual ACM Symposium on Theory of Computing, STOC ’02, pages 457–464, New York, NY, USA, 2002. ACM.
[3] Eli Ben-Sasson and Avi Wigderson. Short proofs are narrow – resolution made simple. J. ACM, 48(2):149–169, 2001.
[4] Sam Buss, Dmitry Itsykson, Alexander Knop, and Dmitry Sokolov. Reordering rule makes OBDD proof systems stronger. In Computational Complexity Conference, volume 102 of LIPIcs, pages 16:1–16:24. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2018.
[5] Samuel R. Buss, Dima Grigoriev, Russell Impagliazzo, and Toniann Pitassi. Linear gaps between degrees for the polynomial calculus modulo distinct primes. In STOC, pages 547–556. ACM, 1999.
[6] Stephen Cook and Robert Reckhow. On the lengths of proofs in the propositional calculus (preliminary version). In Proceedings of the Sixth Annual ACM Symposium on Theory of Computing, STOC ’74, pages 135–148, New York, NY, USA, 1974. ACM.
[7] Stephen A. Cook. The complexity of theorem-proving procedures. In Proceedings of the Third Annual ACM Symposium on Theory of Computing, STOC ’71, pages 151–158, New York, NY, USA, 1971. ACM.
[8] Ludmila Glinskih and Dmitry Itsykson. Satisfiable tseitin formulas are hard for nondeterministic read-once branching programs. In MFCS, volume 83 of LIPIcs, pages 26:1–26:12. Schloss Dagstuhl – Leibniz- Zentrum für Informatik, 2017.
[9] Ludmila Glinskih and Dmitry Itsykson. On tseitin formulas, read-once branching programs and treewidth. In CSR, volume 11532 of Lecture Notes in Computer Science, pages 143–155. Springer, 2019.
[10] Dima Grigoriev. Linear lower bound on degrees of positivstellensatz calculus proofs for the parity. Theor. Comput. Sci., 259(1-2):613–622, 2001.
[11] Johan Håstad. On small-depth frege proofs for tseitin for grids. In FOCS, pages 97–108. IEEE Computer Society, 2017.
[12] Dmitry Itsykson, Alexander Knop, Andrei E. Romashchenko, and Dmitry Sokolov. On obdd-based algorithms and proof systems that dynamically change order of variables. In STACS, volume 66 of LIPIcs, pages 43:1–43:14. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2017.
[13] Dmitry Itsykson, Artur Riazanov, Danil Sagunov, and Petr Smirnov. Almost tight lower bounds on regular resolution refutations of tseitin formulas for all constant-degree graphs. Electronic Colloquium on Computational Complexity (ECCC), 26:178, 2019.
[14] Arist Kojevnikov and Dmitry Itsykson. Lower bounds of static lovász- schrijver calculus proofs for tseitin tautologies. In ICALP (1), volume 4051 of Lecture Notes in Computer Science, pages 323–334. Springer, 2006.
[15] Jan Krajícek. Lower bounds to the size of constant-depth propositional proofs. J. Symb. Log., 59(1):73–86, 1994.
[16] L.A. Levin. Universal problems of full search. Probl. Peredachi Inf., 9(3):115–116, 1973.
[17] László Lovász, Moni Naor, Ilan Newman, and Avi Wigderson. Search problems in the decision tree model. SIAM J. Discret. Math., 8(1):119– 132, 1995.
[18] Toniann Pitassi, Benjamin Rossman, Rocco A. Servedio, and Li-Yang Tan. Poly-logarithmic frege depth lower bounds via an expander switching lemma. In STOC, pages 644–657. ACM, 2016.
[19] G.S. Tseitin. On the complexity of derivation in the propositional calculus. In Studies in Constructive Mathematics and Mathematical Logic Part II. A. O. Slisenko, editor, a968.
[20] Alasdair Urquhart. Hard examples for resolution. J. ACM, 34(1):209– 219, January 1987.

Заказать новую

Лучшие эксперты сервиса ждут твоего задания

от 5 000 ₽

Не подошла эта работа?
Закажи новую работу, сделанную по твоим требованиям

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

    Хочешь уникальную работу?

    Больше 3 000 экспертов уже готовы начать работу над твоим проектом!

    Мария М. УГНТУ 2017, ТФ, преподаватель
    5 (14 отзывов)
    Имею 3 высших образования в сфере Экологии и техносферной безопасности (бакалавриат, магистратура, аспирантура), работаю на кафедре экологии одного из опорных ВУЗов РФ... Читать все
    Имею 3 высших образования в сфере Экологии и техносферной безопасности (бакалавриат, магистратура, аспирантура), работаю на кафедре экологии одного из опорных ВУЗов РФ. Большой опыт в написании курсовых, дипломов, диссертаций.
    #Кандидатские #Магистерские
    27 Выполненных работ
    Анастасия Б.
    5 (145 отзывов)
    Опыт в написании студенческих работ (дипломные работы, магистерские диссертации, повышение уникальности текста, курсовые работы, научные статьи и т.д.) по экономическо... Читать все
    Опыт в написании студенческих работ (дипломные работы, магистерские диссертации, повышение уникальности текста, курсовые работы, научные статьи и т.д.) по экономическому и гуманитарному направлениях свыше 8 лет на различных площадках.
    #Кандидатские #Магистерские
    224 Выполненных работы
    Дмитрий Л. КНЭУ 2015, Экономики и управления, выпускник
    4.8 (2878 отзывов)
    Занимаю 1 место в рейтинге исполнителей по категориям работ "Научные статьи" и "Эссе". Пишу дипломные работы и магистерские диссертации.
    Занимаю 1 место в рейтинге исполнителей по категориям работ "Научные статьи" и "Эссе". Пишу дипломные работы и магистерские диссертации.
    #Кандидатские #Магистерские
    5125 Выполненных работ
    Ксения М. Курганский Государственный Университет 2009, Юридический...
    4.8 (105 отзывов)
    Работаю только по книгам, учебникам, статьям и диссертациям. Никогда не использую технические способы поднятия оригинальности. Только авторские работы. Стараюсь учитыв... Читать все
    Работаю только по книгам, учебникам, статьям и диссертациям. Никогда не использую технические способы поднятия оригинальности. Только авторские работы. Стараюсь учитывать все требования и пожелания.
    #Кандидатские #Магистерские
    213 Выполненных работ
    Екатерина Д.
    4.8 (37 отзывов)
    Более 5 лет помогаю в написании работ от простых учебных заданий и магистерских диссертаций до реальных бизнес-планов и проектов для открытия своего дела. Имею два об... Читать все
    Более 5 лет помогаю в написании работ от простых учебных заданий и магистерских диссертаций до реальных бизнес-планов и проектов для открытия своего дела. Имею два образования: экономист-менеджер и маркетолог. Буду рада помочь и Вам.
    #Кандидатские #Магистерские
    55 Выполненных работ
    Вирсавия А. медицинский 1981, стоматологический, преподаватель, канди...
    4.5 (9 отзывов)
    руководитель успешно защищенных диссертаций, автор около 150 работ, в активе - оппонирование, рецензирование, написание и подготовка диссертационных работ; интересы - ... Читать все
    руководитель успешно защищенных диссертаций, автор около 150 работ, в активе - оппонирование, рецензирование, написание и подготовка диссертационных работ; интересы - медицина, биология, антропология, биогидродинамика
    #Кандидатские #Магистерские
    12 Выполненных работ
    Екатерина С. кандидат наук, доцент
    4.6 (522 отзыва)
    Практически всегда онлайн, доработки делаю бесплатно. Дипломные работы и Магистерские диссертации сопровождаю до защиты.
    Практически всегда онлайн, доработки делаю бесплатно. Дипломные работы и Магистерские диссертации сопровождаю до защиты.
    #Кандидатские #Магистерские
    1077 Выполненных работ
    Анастасия Л. аспирант
    5 (8 отзывов)
    Работаю в сфере метрологического обеспечения. Защищаю кандидатскую диссертацию. Основной профиль: Метрология, стандартизация и сертификация. Оптико-электронное прибост... Читать все
    Работаю в сфере метрологического обеспечения. Защищаю кандидатскую диссертацию. Основной профиль: Метрология, стандартизация и сертификация. Оптико-электронное прибостроение, управление качеством
    #Кандидатские #Магистерские
    10 Выполненных работ
    Ольга Б. кандидат наук, доцент
    4.8 (373 отзыва)
    Работаю на сайте четвертый год. Действующий преподаватель вуза. Основные направления: микробиология, биология и медицина. Написано несколько кандидатских, магистерских... Читать все
    Работаю на сайте четвертый год. Действующий преподаватель вуза. Основные направления: микробиология, биология и медицина. Написано несколько кандидатских, магистерских диссертаций, дипломных и курсовых работ. Слежу за новинками в медицине.
    #Кандидатские #Магистерские
    566 Выполненных работ