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

Мы изучаем сложность цейтинских формул 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

Таким образом, мы решили поставленные задачи: построили верхнюю оценку на 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.