Теорема Курселя

Перейти к навигацииПерейти к поиску

Теорема Курселя — утверждение о том, что любое свойство графа, определяемое в монадической логике второго порядка[англ.] логике графов[англ.], может быть установлено за линейное время на графах с ограниченной древесной шириной[1][2][3]. Результат впервые доказан Брюно Курселем[англ.] в 1990 году[4] и независимо переоткрыт Бори, Паркером и Товейем[5]. Результат считается прототипом алгоритмических метатеорем[6][7].

Формулировки

Множества вершин

В варианте логики графов второго порядка, известном как MSO1[8], граф описывается множеством вершин V и бинарным отношением смежности adj(.,.), а ограничение логикой второго порядка означает, что свойство графа может быть определено в терминах множеств вершин заданного графа, но не в терминах множеств рёбер или пар вершин.

В качестве примера свойство графа раскрашиваемости в три цвета (представленный тремя множествами вершин R, G и B) может быть определён формулой логики второго порядка

∃R,G,B. (∀v∈V. (v∈R ∨ v∈G ∨ v∈B)) ∧
(∀u,v∈V. ((u∈R ∧ v∈R) ∨ (u∈G ∧ v∈G) ∨ (u∈B ∧ v∈B)) → ¬adj(u,v)).

Первая часть этой формулы обеспечивает, что три класса цветов включают все вершины графа, а вторая часть обеспечивает, что каждое из них образует независимое множество. (Можно также добавить предложение в формулу, обеспечивающее непересечение трёх классов цвета, но на результат это не повлияет.) Таким образом, по теореме Курселя можно проверить раскрашиваемость в 3 цвета графа с ограниченной древесной шириной за линейное время.

Для этого варианта логики графов теорема Курселя может быть расширена от древесной ширины до кликовой ширины — для любого фиксированного MSO1 свойства P и любой фиксированной границы b на кликовую ширину графа существует алгоритм линейного времени проверки, имеет ли граф с кликовой шириной, не превосходящей b, свойство P[9].

Множества рёбер

Теорему Курселя можно использовать с более строгим вариантом логики графов второго порядка, известном как MSO2. В этой формулировке граф представляется множеством вершин V, множеством рёбер E и отношением инцидентности между вершинами и рёбрами. Этот вариант позволяет ввести количественный показатель над множеством вершин или рёбер, но не над более сложными отношениями над парами вершин и рёбер.

Например, свойство иметь гамильтонов цикл может быть выражено в MSO2 при определении цикла как множества рёбер, включающего ровно по два ребра, инцидентных каждой вершине, такого, что любое непустое собственное подмножество вершин имеет ребро в цикле и это ребро имеет в точности одну конечную точку в подмножестве. Гамильтоновость, однако, нельзя выразить в терминах MSO1[10].

Модульная сравнимость

Другое направление расширения теоремы Курселя касается логических формул, включающих предикаты для подсчёта длины теста. В этом контексте невозможно осуществить произвольные арифметические операции над размерами множеств, и даже невозможно проверить, что множества имеют один и тот же размер. Однако MSO1 и MSO2 могут быть расширены до логик, называемых CMSO1 и CMSO2, которые включают для любых двух констант q и r предикат , который проверяет, сравнима ли мощность множества S с r по модулю q. Теорему Курселя можно расширить на эти логики[4].

Разрешимость и оптимизация

Как утверждалось выше, теорема Курселя применима, в основном, к задачам разрешимости — имеет граф свойство или нет. Те же методы, тем не менее, позволяют также решить задачи оптимизации, в которых вершинам или рёбрам графа присвоены некоторые целые веса и ищется минимум или максимум весов, для которых множество удовлетворяет заданному свойству, выраженному в терминах логики второго порядка. Эти задачи оптимизации могут быть решены за линейное время на графах с ограниченной кликовой шириной[9][11].

Ёмкостная сложность

Вместо ограничения временной сложности алгоритма, распознающего MSO-свойства графов с ограниченной древесной шириной, можно также анализировать емкостную сложность[англ.] таких алгоритмов, то есть величину памяти, необходимую сверх входных данных (в предположении, что входные данные не могут быть изменены и занятая под них память не может быть использована в других целях). В частности, можно распознать графы с ограниченной древесной шириной и любое MSO-свойство на этих графах с помощью детерминированной машины Тьюринга, которая использует только логарифмическую память[англ.][12].

Стратегия доказательства и сложность

Типичный подход к доказательству теоремы Курселя использует построение конечного восходящего автомата[англ.], действующего на древесных декомпозициях данного графа[6].

Более подробно, два графа G1 и G2, каждый с указанным подмножеством T вершин, называемых конечными, могут считаться эквивалентными согласно MSO-формуле F, если для любого другого графа H, пересечение которого с G1 и G2 состоит только из вершин T, два графа G1 ∪ H и G2 ∪ H ведут себя одинаково по отношению к формуле F — либо оба удовлетворяют F, либо оба не удовлетворяют F. Это отношение эквивалентности, и по индукции по длине F можно показать (если размеры T и F ограничены), что отношение имеет конечное число классов эквивалентности[13].

Древесная декомпозиция заданного графа G состоит из дерева и, для каждого узла дерева, подмножества вершин графа G, называемого корзиной. Это подмножество должно удовлетворять двум свойствам — для каждой вершины v из G корзина, содержащая v, должна быть ассоциирована с неразрывным поддеревом и для каждого ребра uv из G должна существовать корзина, содержащая как u, так и v. Вершины в корзине могут пониматься как конечные элементы подграфа G, представленные поддеревьями древесной декомпозиции, растущими из этой корзины. Если граф G имеет ограниченную древесную ширину, он имеет древесную декомпозицию, в которой все корзины имеют ограниченный размер и такое разложение может быть найдено за фиксированно-параметрически разрешимое время[14]. Более того, можно выбрать древесное разложение, образующее двоичное дерево с только двумя дочерними поддеревьями на корзину. Таким образом, можно осуществить восходящее вычисление на этой древесной декомпозиции, вычисляя идентификатор для класса эквивалентности поддерева, имеющего корень в каждой корзине, путём комбинирования рёбер, представленных внутри корзины, с двумя идентификаторами классов эквивалентности двух дочерних элементов[15].

Размер автомата, построенного таким способом, не является элементарной функцией от размера входной MSO-формулы. Эта неэлементарная сложность приводит к тому, что невозможно (если только не P = NP) проверить MSO-свойства за время, фиксированно-параметрически разрешимое с элементарной функциональной зависимостью от параметра[16].

Гипотеза Курселя

Доказательство теоремы Курселя показывает более строгий результат — не только любое (с предикатом подсчёта длины) свойство логики второго порядка может быть распознано за линейное время для графов с ограниченной древесной шириной, но и оно может быть распознано конечным автоматом над деревом[англ.]. Гипотеза Курселя обратна этому — если свойство графов с ограниченной шириной распознаётся автоматом над деревьями, то оно может быть определено в терминах логики второго порядка. Несмотря на попытки доказательства, предпринятые Лапуаром[17], гипотеза считается недоказанной[18]. Однако известны некоторые специальные случаи, в частности, гипотеза верна для графов с древесной шириной три и менее[19].

Более того, для графов Халина (специального вида графов с древесной шириной три) предикат подсчёта длины не обязателен — для этих графов любое свойство, которое может быть распознано автоматом на деревьях, может быть определено в терминах логики второго порядка. То же самое верно, в более общем случае, для некоторых классов графов, в которых древесная декомпозиция сама может быть описана в MSOL. Однако это не может быть верно для всех графов с ограниченной древесной шириной, поскольку, в общем случае, предикат подсчёта длины добавляет силу логике второго порядка. Например, графы с чётным числом вершин могут быть распознаны по предикату, но не могут быть распознаны без него[18].

Выполнимость и теорема Сииза

Проблема выполнимости[англ.] для формул логики второго порядка является задачей определения, существует ли по меньшей мере один граф (возможно, принадлежащий ограниченному семейству графов), для которого формула верна. Для произвольных семейств графов и произвольных формул эта задача неразрешима. Выполнимость формул MSO2, однако, разрешима для графов с ограниченной древесной шириной, а выполнимость формул MSO1 разрешима для графов с ограниченной кликовой шириной. Доказательство использует построение автомата над деревом для формулы, а затем проверку, имеет ли автомат приемлемый путь.

В качестве частично обратного утверждения Сииз[20] доказал, что всякий раз, когда семейство графов имеет разрешимую проблему MSO2 выполнимости, семейство должно иметь ограниченную древесную ширину. Доказательство опирается на теорему Робертсона и Сеймура о том, что семейства графов с неограниченной древесной шириной имеют произвольно большие миноры-решётки[21]. Сииз также высказал предположение, что любое семейство графов с разрешимой проблемой MSO1 выполнимости должно иметь ограниченную кликовую ширину. Гипотеза не доказана, но ослабленная гипотеза с заменой MSO1 на CMSO1 верна[22].

Приложения

Гроэ[23] использовал теорему Курселя, чтобы показать, что вычисление числа пересечений графа G является фиксированно-параметрически разрешимой[англ.] задачей с квадратичной зависимостью от размера G, что улучшает кубический по времени алгоритм, основанный на теореме Робертсона — Сеймура. Более позднее улучшение до линейного времени Каварабайаши и Риидом[24] использует тот же подход. Если данный граф G имеет малую древесную ширину, теорема Курселя может быть применена к этой проблеме непосредственно. С другой стороны, если G имеет большую древесную ширину, то он содержит большой минор-решётку, внутри которого граф может быть упрощён без изменения числа пересечений. Алгоритм Гроэ осуществляет это упрощение, пока оставшийся граф не будет иметь малую древесную ширину, а затем применяет теорему Курселя для решения уменьшенной подзадачи[25][26].

Готтлоб и Ли[27] заметили, что теорема Курселя применима к некоторым задачам поиска минимального множественных разрезов в графе, если структура, образованная графом и множеством разрезающих пар, имеет ограниченную древесную ширину. В результате они получили фиксированно-параметрически разрешимый алгоритм для этих задач, параметризированный одним параметром, древесной шириной, что улучшает предыдущие решения, комбинирующие несколько параметров[28].

В вычислительной топологии Бартон и Дауни[29] расширили теорему Курселя с MSO2 до логики второго порядка на симплициальных комплексах ограниченной размерности, что позволяет введение количественных характеристик для любой фиксированной размерности. Как следствие, они показали, как вычислить некоторые квантовые инварианты[англ.] 3-многообразий, а также как решить эффективно некоторые задачи в дискретной теории Морса[англ.], когда многообразие имеет триангуляцию (исключая вырожденные симплексы), двойственный граф которой имеет малую древесную ширину[29].

Методы, основанные на теореме Курселя, были использованы в теории баз данных[англ.][30], представлении знаний и логических выводов[31], теории автоматов[32] и проверке моделей[33].

Примечания

  1. ↑ Eger, 2008.
  2. ↑ Courcelle, Engelfriet, 2012.
  3. ↑ Downey, Fellows, 2013, с. 265–278.
  4. ↑ 1 2 Courcelle, 1990, с. 12–75.
  5. ↑ Borie, Parker, Tovey, 1992, с. 555–581.
  6. ↑ 1 2 Kneis, Langer, 2009, с. 65–81.
  7. ↑ Lampis, 2010, с. 549–560.
  8. ↑ MSO = monadic second-order
  9. ↑ 1 2 Courcelle, Makowsky, Rotics, 2000, с. 125–150.
  10. ↑ Courcelle, Engelfriet, 2012, с. 336, Proposition 5.13.
  11. ↑ Arnborg, Lagergren, Seese, 1991, с. 308–340.
  12. ↑ Elberfeld, Jakoby, Tantau, 2010, с. 143–152.
  13. ↑ Downey, Fellows, 2013, с. 266, Theorem 13.1.1.
  14. ↑ Downey, Fellows, 2013, с. 195–203 Section 10.5: Bodlaender's theorem.
  15. ↑ Downey, Fellows, 2013, с. 237–247, Section 12.6: Tree automata.
  16. ↑ Frick, Grohe, 2004, с. 3–31.
  17. ↑ Lapoire, 1998, с. 618–628.
  18. ↑ 1 2 Jaffke, Bodlaender, 2015.
  19. ↑ Kaller, 2000, с. 348–381.
  20. ↑ Seese, 1991.
  21. ↑ Seese, 1991, с. 169–195.
  22. ↑ Courcelle, Oum, 2007, с. 91–126.
  23. ↑ Grohe, 2001.
  24. ↑ Kawarabayashi, Reed, 2007.
  25. ↑ Grohe, 2001, с. 231–236.
  26. ↑ Kawarabayashi, Reed, 2007, с. 382–390.
  27. ↑ Gottlob, Lee, 2007.
  28. ↑ Gottlob, Lee, 2007, с. 136–141.
  29. ↑ 1 2 Burton, Downey, 2014.
  30. ↑ Grohe, Mariño, 1999, с. 70–82.
  31. ↑ Gottlob, Pichler, Wei, 2010, с. 105–132.
  32. ↑ Madhusudan, Parlato, 2011, с. 283–294.
  33. ↑ Obdržálek, 2003, с. 80–92.

Литература

  • Eger, Steffen. Regular Languages, Tree Width, and Courcelle's Theorem: An Introduction (англ.). — VDM Publishing, 2008. — ISBN 978-3639076332.
  • Bruno Courcelle, Joost Engelfriet. Graph Structure and Monadic Second-Order Logic: A Language-Theoretic Approach. — Cambridge University Press, 2012. — Т. 138. — (Encyclopedia of Mathematics and its Applications). — ISBN 9781139644006.
  • Rodney G. Downey, Michael R. Fellows. Fundamentals of parameterized complexity. — London: Springer, 2013. — С. 265–278. — (Texts in Computer Science). — ISBN 978-1-4471-5558-4. — doi:10.1007/978-1-4471-5559-1.
  • Bruno Courcelle. The monadic second-order logic of graphs. I. Recognizable sets of finite graphs // Information and Computation. — 1990. — Т. 85, вып. 1. — С. 12–75. — doi:10.1016/0890-5401(90)90043-H.
  • Richard B. Borie, R. Gary Parker, Craig A. Tovey. Automatic generation of linear-time algorithms from predicate calculus descriptions of problems on recursively constructed graph families // Algorithmica. — 1992. — Т. 7, вып. 5-6. — С. 555–581. — doi:10.1007/BF01758777.
  • Joachim Kneis, Alexander Langer. A practical approach to Courcelle's theorem // Electronic Notes in Theoretical Computer Science. — 2009. — Т. 251. — С. 65–81. — doi:10.1016/j.entcs.2009.08.028.
  • Michael Lampis. Proc. 18th Annual European Symposium on Algorithms / Mark de Berg, Ulrich Meyer. — Springer, 2010. — Т. 6346. — С. 549–560. — (Lecture Notes in Computer Science). — doi:10.1007/978-3-642-15775-2_47.
  • B. Courcelle, J. A. Makowsky, U. Rotics. Linear time solvable optimization problems on graphs of bounded clique-width // Theory of Computing Systems. — 2000. — Т. 33, вып. 2. — С. 125–150. — doi:10.1007/s002249910009.
  • Stefan Arnborg, Jens Lagergren, Detlef Seese. Easy problems for tree-decomposable graphs // Journal of Algorithms. — 1991. — Т. 12, вып. 2. — С. 308–340. — doi:10.1016/0196-6774(91)90006-K.
  • Michael Elberfeld, Andreas Jakoby, Till Tantau. Proc. 51st Annual IEEE Symposium on Foundations of Computer Science (FOCS 2010). — 2010. — С. 143–152. — doi:10.1109/FOCS.2010.21.
  • Markus Frick, Martin Grohe. The complexity of first-order and monadic second-order logic revisited // Annals of Pure and Applied Logic. — 2004. — Т. 130, вып. 1-3. — С. 3–31. — doi:10.1016/j.apal.2004.01.007.
  • Denis Lapoire. STACS 98: 15th Annual Symposium on Theoretical Aspects of Computer Science Paris, France, February 25ÔÇô27, 1998, Proceedings. — 1998. — С. 618–628. — doi:10.1007/bfb0028596.
  • Lars Jaffke, Hans L. Bodlaender. MSOL-definability equals recognizability for Halin graphs and bounded degree k-outerplanar graphs. — 2015. — arXiv:1503.01604.
  • D. Kaller. Definability equals recognizability of partial 3-trees and k-connected partial k-trees // Algorithmica. — 2000. — Т. 27, вып. 3. — С. 348–381. — doi:10.1007/s004530010024.
  • D. Seese. The structure of the models of decidable monadic theories of graphs // Annals of Pure and Applied Logic. — 1991. — Т. 53, вып. 2. — С. 169–195. — doi:10.1016/0168-0072(91)90054-P.
  • Bruno Courcelle, Sang-il Oum. Vertex-minors, monadic second-order logic, and a conjecture by Seese // Journal of Combinatorial Theory. — 2007. — Т. 97, вып. 1. — С. 91–126. — doi:10.1016/j.jctb.2006.04.003.
  • Martin Grohe. Proceedings of the Thirty-third Annual ACM Symposium on Theory of Computing (STOC '01). — 2001. — С. 231–236. — doi:10.1145/380752.380805.
  • Ken-ichi Kawarabayashi, Bruce Reed. Proceedings of the Thirty-ninth Annual ACM Symposium on Theory of Computing (STOC '07). — 2007. — С. 382–390. — doi:10.1145/1250790.1250848.
  • Georg Gottlob, Stephanie Tien Lee. A logical approach to multicut problems // Information Processing Letters. — 2007. — Т. 103, вып. 4. — С. 136–141. — doi:10.1016/j.ipl.2007.03.005.
  • Benjamin A. Burton, Rodney G. Downey. Courcelle's theorem for triangulations. — 2014. — (International Congress of Mathematicians).
  • Martin Grohe, Julian Mariño. Database Theory — ICDT’99: 7th International Conference Jerusalem, Israel, January 10–12, 1999, Proceedings. — 1999. — Т. 1540. — С. 70–82. — (Lecture Notes in Computer Science). — doi:10.1007/3-540-49257-7_6.
  • Georg Gottlob, Reinhard Pichler, Fang Wei. Bounded treewidth as a key to tractability of knowledge representation and reasoning // Artificial Intelligence. — 2010. — Т. 174, вып. 1. — С. 105–132. — doi:10.1016/j.artint.2009.10.003.
  • P. Madhusudan, Gennaro Parlato. Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '11). — 2011. — Т. 46 (1). — С. 283–294. — (SIGPLAN Notices). — doi:10.1145/1926385.1926419.
  • Jan Obdržálek. Computer Aided Verification: 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings. — 2003. — Т. 2725. — С. 80–92. — (Lecture Notes in Computer Science). — doi:10.1007/978-3-540-45069-6_7.