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

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

Формулювання

Множини вершин

У варіанті логіки графів другого порядку, відомому як MSO₁, граф описується множиною вершин V і бінарним відношенням суміжності adj(.,.), а обмеження логікою другого порядку означає, що властивість графа можна визначити в термінах множин вершин заданого графа, але не в термінах множин ребер або пар вершин.

Як приклад, властивість графа розфарбовуваності в три кольори (подану трьома множинами вершин R, G і B) можна визначити формулою логіки другого порядку

Перша частина цієї формули забезпечує, що три класи кольорів включають усі вершини графа, а друга частина забезпечує, що кожен з них утворює незалежну множину. (Можна також додати у формулу речення, що забезпечує неперетинність трьох колірних класів, але на результат це не вплине.) Таким чином, за теоремою Курселя можна за лінійний час перевірити розфарбовуваність у 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 (15 травня). — С. 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 (15 травня). — С. 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 (15 травня). — С. 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 (15 травня). — С. 125–150. — DOI:10.1007/s002249910009.
• Stefan Arnborg, Jens Lagergren, Detlef Seese. Easy problems for tree-decomposable graphs // Journal of Algorithms. — 1991. — Т. 12, вип. 2 (15 травня). — С. 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 (15 травня). — С. 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. — 15 травня. — arXiv:1503.01604.
• D. Kaller. Definability equals recognizability of partial 3-trees and k-connected partial k-trees // Algorithmica. — 2000. — Т. 27, вип. 3 (15 травня). — С. 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 (15 травня). — С. 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 (15 травня). — С. 91–126. — (Series B). — 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 (15 травня). — С. 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 (15 травня). — С. 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.