Системы доказательств, основанные на диаграммах принятия решений
Мы изучаем сложность цейтинских формул 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.
Хочешь уникальную работу?
Больше 3 000 экспертов уже готовы начать работу над твоим проектом!
4.8 (2878 отзывов)
4 (15 отзывов)
5 (49 отзывов)
5 (9 отзывов)
4.6 (71 отзыв)
5 (154 отзыва)
5 (20 отзывов)
4.8 (211 отзывов)
4.7 (82 отзыва)
