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

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

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

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

В варианте логики графов второго порядка, известном как MSO₁, граф описывается множеством вершин 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 цвета графа с ограниченной древесной шириной за линейное время.

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

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

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

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

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

Другое направление расширения теоремы Курселя касается логических формул, включающих предикаты для подсчёта длины теста. В этом контексте невозможно осуществить произвольные арифметические операции над размерами множеств, и даже невозможно проверить, что множества имеют один и тот же размер. Однако MSO₁ и MSO₂ могут быть расширены до логик, называемых CMSO₁ и CMSO₂, которые включают для любых двух констант q и r предикат $\operatorname {card} _{q,r}(S)$, который проверяет, сравнима ли мощность множества S с r по модулю q. Теорему Курселя можно расширить на эти логики.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

В качестве частично обратного утверждения Сииз доказал, что всякий раз, когда семейство графов имеет разрешимую проблему MSO₂ выполнимости, семейство должно иметь ограниченную древесную ширину. Доказательство опирается на теорему Робертсона и Сеймура о том, что семейства графов с неограниченной древесной шириной имеют произвольно большие миноры-решётки. Сииз также высказал предположение, что любое семейство графов с разрешимой проблемой MSO₁ выполнимости должно иметь ограниченную кликовую ширину. Гипотеза не доказана, но ослабленная гипотеза с заменой MSO₁ на CMSO₁ верна.

Приложения

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

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

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

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

Литература

• 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.