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

Смирнов Петр Юрьевич
Бесплатно
В избранное
Работа доступна по лицензии 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 экспертов уже готовы начать работу над твоим проектом!

    Кормчий В.
    4.3 (248 отзывов)
    Специализация: диссертации; дипломные и курсовые работы; научные статьи.
    Специализация: диссертации; дипломные и курсовые работы; научные статьи.
    #Кандидатские #Магистерские
    335 Выполненных работ
    Дарья П. кандидат наук, доцент
    4.9 (20 отзывов)
    Профессиональный журналист, филолог со стажем более 10 лет. Имею профильную диссертацию по специализации "Радиовещание". Подробно и серьезно разрабатываю темы научных... Читать все
    Профессиональный журналист, филолог со стажем более 10 лет. Имею профильную диссертацию по специализации "Радиовещание". Подробно и серьезно разрабатываю темы научных исследований, связанных с журналистикой, филологией и литературой
    #Кандидатские #Магистерские
    33 Выполненных работы
    Дмитрий М. БГАТУ 2001, электрификации, выпускник
    4.8 (17 отзывов)
    Помогаю с выполнением курсовых проектов и контрольных работ по электроснабжению, электроосвещению, электрическим машинам, электротехнике. Занимался наукой, писал стать... Читать все
    Помогаю с выполнением курсовых проектов и контрольных работ по электроснабжению, электроосвещению, электрическим машинам, электротехнике. Занимался наукой, писал статьи, патенты, кандидатскую диссертацию, преподавал. Занимаюсь этим с 2003.
    #Кандидатские #Магистерские
    19 Выполненных работ
    Анна Н. Государственный университет управления 2021, Экономика и ...
    0 (13 отзывов)
    Закончила ГУУ с отличием "Бухгалтерский учет, анализ и аудит". Выполнить разные работы: от рефератов до диссертаций. Также пишу доклады, делаю презентации, повышаю уни... Читать все
    Закончила ГУУ с отличием "Бухгалтерский учет, анализ и аудит". Выполнить разные работы: от рефератов до диссертаций. Также пишу доклады, делаю презентации, повышаю уникальности с нуля. Все работы оформляю в соответствии с ГОСТ.
    #Кандидатские #Магистерские
    0 Выполненных работ
    Вики Р.
    5 (44 отзыва)
    Наличие красного диплома УрГЮУ по специальности юрист. Опыт работы в профессии - сфера банкротства. Уровень выполняемых работ - до магистерских диссертаций. Написан... Читать все
    Наличие красного диплома УрГЮУ по специальности юрист. Опыт работы в профессии - сфера банкротства. Уровень выполняемых работ - до магистерских диссертаций. Написание письменных работ для меня в удовольствие.Всегда качественно.
    #Кандидатские #Магистерские
    60 Выполненных работ
    Шагали Е. УрГЭУ 2007, Экономика, преподаватель
    4.4 (59 отзывов)
    Серьезно отношусь к тренировке собственного интеллекта, поэтому постоянно учусь сама и с удовольствием пишу для других. За 15 лет работы выполнила более 600 дипломов и... Читать все
    Серьезно отношусь к тренировке собственного интеллекта, поэтому постоянно учусь сама и с удовольствием пишу для других. За 15 лет работы выполнила более 600 дипломов и диссертаций, Есть любимые темы - они дешевле обойдутся, ибо в радость)
    #Кандидатские #Магистерские
    76 Выполненных работ
    Ольга Р. доктор, профессор
    4.2 (13 отзывов)
    Преподаватель ВУЗа, опыт выполнения студенческих работ на заказ (от рефератов до диссертаций): 20 лет. Образование высшее . Все заказы выполняются в заранее согласован... Читать все
    Преподаватель ВУЗа, опыт выполнения студенческих работ на заказ (от рефератов до диссертаций): 20 лет. Образование высшее . Все заказы выполняются в заранее согласованные сроки и при необходимости дорабатываются по рекомендациям научного руководителя (преподавателя). Буду рада плодотворному и взаимовыгодному сотрудничеству!!! К каждой работе подхожу индивидуально! Всегда готова по любому вопросу договориться с заказчиком! Все работы проверяю на антиплагиат.ру по умолчанию, если в заказе не стоит иное и если это заранее не обговорено!!!
    #Кандидатские #Магистерские
    21 Выполненная работа
    Антон П. преподаватель, доцент
    4.8 (1033 отзыва)
    Занимаюсь написанием студенческих работ (дипломные работы, маг. диссертации). Участник международных конференций (экономика/менеджмент/юриспруденция). Постоянно публик... Читать все
    Занимаюсь написанием студенческих работ (дипломные работы, маг. диссертации). Участник международных конференций (экономика/менеджмент/юриспруденция). Постоянно публикуюсь, имею высокий индекс цитирования. Спикер.
    #Кандидатские #Магистерские
    1386 Выполненных работ
    Дарья С. Томский государственный университет 2010, Юридический, в...
    4.8 (13 отзывов)
    Практикую гражданское, семейное право. Преподаю указанные дисциплины в ВУЗе. Выполняла работы на заказ в течение двух лет. Обучалась в аспирантуре, подготовила диссерт... Читать все
    Практикую гражданское, семейное право. Преподаю указанные дисциплины в ВУЗе. Выполняла работы на заказ в течение двух лет. Обучалась в аспирантуре, подготовила диссертационное исследование, которое сейчас находится на рассмотрении в совете.
    #Кандидатские #Магистерские
    18 Выполненных работ