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

Смирнов Петр Юрьевич
Бесплатно
В избранное
Работа доступна по лицензии 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.9 (522 отзыва)
    Кандидат технических наук. Специализируюсь на выполнении работ по метрологии и стандартизации
    Кандидат технических наук. Специализируюсь на выполнении работ по метрологии и стандартизации
    #Кандидатские #Магистерские
    836 Выполненных работ
    Кормчий В.
    4.3 (248 отзывов)
    Специализация: диссертации; дипломные и курсовые работы; научные статьи.
    Специализация: диссертации; дипломные и курсовые работы; научные статьи.
    #Кандидатские #Магистерские
    335 Выполненных работ
    Егор В. кандидат наук, доцент
    5 (428 отзывов)
    Здравствуйте. Занимаюсь выполнением работ более 14 лет. Очень большой опыт. Более 400 успешно защищенных дипломов и диссертаций. Берусь только со 100% уверенностью. Ск... Читать все
    Здравствуйте. Занимаюсь выполнением работ более 14 лет. Очень большой опыт. Более 400 успешно защищенных дипломов и диссертаций. Берусь только со 100% уверенностью. Скорее всего Ваш заказ будет выполнен раньше срока.
    #Кандидатские #Магистерские
    694 Выполненных работы
    Антон П. преподаватель, доцент
    4.8 (1033 отзыва)
    Занимаюсь написанием студенческих работ (дипломные работы, маг. диссертации). Участник международных конференций (экономика/менеджмент/юриспруденция). Постоянно публик... Читать все
    Занимаюсь написанием студенческих работ (дипломные работы, маг. диссертации). Участник международных конференций (экономика/менеджмент/юриспруденция). Постоянно публикуюсь, имею высокий индекс цитирования. Спикер.
    #Кандидатские #Магистерские
    1386 Выполненных работ
    Татьяна П.
    4.2 (6 отзывов)
    Помогаю студентам с решением задач по ТОЭ и физике на протяжении 9 лет. Пишу диссертацию на соискание степени кандидата технических наук, имею опыт годовой стажировки ... Читать все
    Помогаю студентам с решением задач по ТОЭ и физике на протяжении 9 лет. Пишу диссертацию на соискание степени кандидата технических наук, имею опыт годовой стажировки в одном из крупнейших университетов Германии.
    #Кандидатские #Магистерские
    9 Выполненных работ
    Оксана М. Восточноукраинский национальный университет, студент 4 - ...
    4.9 (37 отзывов)
    Возможно выполнение работ по правоведению и политологии. Имею высшее образование менеджера ВЭД и правоведа, защитила кандидатскую и докторскую диссертации по политоло... Читать все
    Возможно выполнение работ по правоведению и политологии. Имею высшее образование менеджера ВЭД и правоведа, защитила кандидатскую и докторскую диссертации по политологии.
    #Кандидатские #Магистерские
    68 Выполненных работ
    Олег Н. Томский политехнический университет 2000, Инженерно-эконо...
    4.7 (96 отзывов)
    Здравствуйте! Опыт написания работ более 12 лет. За это время были успешно защищены более 2 500 написанных мною магистерских диссертаций, дипломов, курсовых работ. Явл... Читать все
    Здравствуйте! Опыт написания работ более 12 лет. За это время были успешно защищены более 2 500 написанных мною магистерских диссертаций, дипломов, курсовых работ. Являюсь действующим преподавателем одного из ВУЗов.
    #Кандидатские #Магистерские
    177 Выполненных работ
    Виктор В. Смоленская государственная медицинская академия 1997, Леч...
    4.7 (46 отзывов)
    Имеют опыт грамотного написания диссертационных работ по медицине, а также отдельных ее частей (литературный обзор, цели и задачи исследования, материалы и методы, выв... Читать все
    Имеют опыт грамотного написания диссертационных работ по медицине, а также отдельных ее частей (литературный обзор, цели и задачи исследования, материалы и методы, выводы).Пишу статьи в РИНЦ, ВАК.Оформление патентов от идеи до регистрации.
    #Кандидатские #Магистерские
    100 Выполненных работ
    Шагали Е. УрГЭУ 2007, Экономика, преподаватель
    4.4 (59 отзывов)
    Серьезно отношусь к тренировке собственного интеллекта, поэтому постоянно учусь сама и с удовольствием пишу для других. За 15 лет работы выполнила более 600 дипломов и... Читать все
    Серьезно отношусь к тренировке собственного интеллекта, поэтому постоянно учусь сама и с удовольствием пишу для других. За 15 лет работы выполнила более 600 дипломов и диссертаций, Есть любимые темы - они дешевле обойдутся, ибо в радость)
    #Кандидатские #Магистерские
    76 Выполненных работ