Azərbaycanca AzərbaycancaБеларускі БеларускіDansk DanskDeutsch DeutschEspañola EspañolaFrançais FrançaisIndonesia IndonesiaItaliana Italiana日本語 日本語Қазақ ҚазақLietuvos LietuvosNederlands NederlandsPortuguês PortuguêsРусский Русскийසිංහල සිංහලแบบไทย แบบไทยTürkçe TürkçeУкраїнська Українська中國人 中國人United State United StateAfrikaans Afrikaans
Підтримка
www.wikidata.uk-ua.nina.az

Теоре ма Курселя твердження про те що будь яку властивість графа що визначається в en en можна встановити за лінійний ча

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

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

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

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

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

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

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

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

Для цього варіанту логіки графів теорему Курселя можна розширити від деревної ширини до клікової ширини — для будь-якої фіксованої MSO1 властивості P і будь-якої фіксованої межі b на клікову ширину графа існує алгоритм лінійного часу перевірки, чи має граф з кліковою шириною, що не перевершує b, властивість P.

Множини ребер

Теорему Курселя можна використати зі строгішим варіантом логіки графів другого порядку, відомим як MSO2. У цьому формулюванні граф подається множиною вершин V, множиною ребер E і відношенням інцидентності між вершинами і ребрами. Цей варіант дозволяє ввести кількісний показник над множиною вершин або ребер, але не над складнішими відношеннями над парами вершин і ребер.

Наприклад, властивість мати гамільтонів цикл можна виразити в MSO2 при визначенні циклу як множини ребер, що включає рівно по два ребра, інцидентних кожній вершині, такої, що будь-яка непорожня власна підмножина вершин має ребро в циклі і це ребро має рівно одну кінцеву точку в підмножині. Гамільтоновість, однак, не можна виразити в термінах MSO1.

Модульна порівнянність

Інший напрямок розширення теореми Курселя стосується логічних формул, які включають предикати для підрахунку довжини тесту. У цьому контексті неможливо здійснити довільні арифметичні операції над розмірами множин, і навіть неможливо перевірити, що множини мають однаковий розмір. Однак MSO1 і MSO2 можна розширити до логік, званих CMSO1 і CMSO2, які включають для будь-яких двох констант q і r предикат image, який перевіряє, чи (порівнянна) потужність множини S із r за модулем q. Теорему Курселя можна розширити на ці логіки.

Розв'язність та оптимізація

Як стверджувалося вище, теорема Курселя застосовна, переважно, до задач розв'язності — має граф властивість чи ні. Ті ж методи, проте, дозволяють також розв'язати задачі оптимізації, в яких вершинам або ребрам графа присвоєно деякі цілі ваги і шукається мінімум або максимум ваг, для яких множина задовольняє певній властивості, вираженій у термінах логіки другого порядку. Ці задачі оптимізації можна розв'язати за лінійний час на графах з обмеженою кліковою шириною.

Ємнісна складність

Замість обмеження часової складності алгоритму, що розпізнає MSO-властивості графів з обмеженою деревною шириною, можна також аналізувати [en] таких алгоритмів, тобто обсяг пам'яті, необхідний понад вхідні дані (в припущенні, що вхідні дані не можуть змінюватись і зайняту під них пам'ять не можна використати в інших цілях). Зокрема, можна розпізнати графи з обмеженою деревною шириною і будь-яку MSO-властивість на цих графах за допомогою детермінованої машини Тюрінга, яка використовує тільки логарифмічну пам'ять.

Стратегія доведення і складність

Типовий підхід до доведення теореми Курселя використовує побудову скінченного висхідного [en], що діє на деревних декомпозиціях даного графа.

Докладніше, два графи G1 і G2, кожен зі вказаною підмножиною T вершин, які називають кінцевими, можна вважати еквівалентними згідно з MSO-формулою F, якщо для будь-якого іншого графа H, перетин якого з G1 і G2 складається тільки з вершин T, два графи G1 ∪ H і G2 ∪ H поводяться однаково відносно формули F — або обидва задовольняють F, або обидва не задовольняють F. Це відношення еквівалентності, і за індукцією за довжиною F можна показати (якщо розміри T і F обмежені), що відношення має скінченне число класів еквівалентності.

Деревна декомпозиція заданого графа G складається з дерева і, для кожного вузла дерева, підмножини вершин графа G, званої кошиком. Ця підмножина має задовольняти двом властивостям — для кожної вершини v із G кошик, що містить v, має бути асоційованим із нерозривним піддеревом, і для кожного ребра uv із G має існувати кошик, що містить як u, так і v. Вершини в кошику можуть розумітися як кінцеві елементи підграфа G, подані піддеревами деревної декомпозиції, що ростуть із цього кошика. Якщо граф G має обмежену деревну ширину, він має деревну декомпозицію, в якій усі кошики мають обмежений розмір і такий розклад можна знайти за фіксовано-параметрично розв'язний час. Більш того, можна вибрати деревний розклад, що утворює двійкове дерево з тільки двома дочірніми піддеревами на кошик. Таким чином, можна здійснити висхідне обчислення на цій деревній декомпозиції, обчислюючи ідентифікатор для класу еквівалентності піддерева, що має корінь у кожному кошику, комбінуючи ребра, представлених всередині кошика, з двома ідентифікаторами класів еквівалентності двох дочірніх елементів.

Розмір автомата, побудованого таким способом, не є елементарною функцією від розміру вхідної MSO-формули. Ця неелементарна складність призводить до того, що неможливо (якщо тільки не P = NP) перевірити MSO-властивості за час, фіксовано-параметрично розв'язний з елементарною функціональною залежністю від параметра.

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

Доказ теореми Курселя показує строгіший результат — не тільки будь-яку (з предикатом підрахунку довжини) властивість логіки другого порядку можна розпізнати за лінійний час для графів з обмеженою деревною шириною, але й її можна розпізнати скінченним [en]. Гіпотеза Курселя обернена на цьому — якщо властивість графів з обмеженою шириною розпізнається автоматом над деревами, то її можна визначити в термінах логіки другого порядку. Попри Лапуарові спроби доведення, гіпотезу вважають недоведеною. Однак відомі деякі окремі випадки, зокрема, гіпотеза істинна для графів з деревною шириною три і менше.

Більш того, для графів Халіна (особливого виду графів з деревною шириною три) предикат підрахунку довжини не обов'язковий — для цих графів будь-яку властивість, яку можна розпізнати автоматом на деревах, можна визначити в термінах логіки другого порядку. Це також стосується, загалом, деяких класів графів, у яких деревну декомпозицію саму можна описати в MSOL. Однак це не може бути істинним для всіх графів з обмеженою деревною шириною, оскільки, в загальному випадку, предикат підрахунку довжини додає сили логіці другого порядку. Наприклад, графи з парним числом вершин можна розпізнати за предикатом, але не можна розпізнати без нього.

Виконуваність і теорема Сіїза

[en] для формул логіки другого порядку є задачею визначення, чи існує принаймні один граф (який, можливо, належить до обмеженого сімейства графів), для якого формула істинна. Для довільних сімейств графів та довільних формул ця задача нерозв'язна. Виконуваність формул MSO2, однак, розв'язна для графів з обмеженою деревною шириною, а виконуваність формул MSO1 розв'язна для графів з обмеженою кліковою шириною. Доведення використовує побудову автомата над деревом для формули, а потім перевірку, чи має автомат прийнятний шлях.

Як частково обернене твердження Сіїз довів, що кожного разу, коли сімейство графів має розв'язну проблему MSO2 виконуваності, сімейство повинне мати обмежену деревну ширину. Доведення спирається на теорему Робертсона і Сеймура про те, що сімейства графів з необмеженою деревною шириною мають довільно великі мінори-решітки. Сіїз також припустив, що будь-яке сімейство графів з розв'язною проблемою MSO1 виконуваності повинне мати обмежену клікову ширину. Гіпотезу не доведено, але ослаблена гіпотеза із заміною MSO1 на CMSO1 істинна.

Застосування

Грое використав теорему Курселя, щоб показати, що обчислення числа схрещень графа G є [en] задачею з квадратичною залежністю від розміру G, що покращує кубічний за часом алгоритм, заснований на теоремі Робертсона — Сеймура. Пізніше поліпшення до лінійного часу Каварабайаши і Риїдом використовує той самий підхід. Якщо даний граф G має малу деревну ширину, теорему Курселя можна застосувати до цієї проблеми безпосередньо. З іншого боку, якщо G має велику деревну ширину, то він містить великий мінор-решітку, всередині якого граф можна спростити, не змінюючи числа схрещень. Алгоритм Грое виконує це спрощення до отримання графа з малою деревною шириною, а потім застосовує теорему Курселя для розв'язання зменшеної підзадачі.

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

В обчислювальній топології Бартон і Дауні розширили теорему Курселя з MSO2 до логіки другого порядку на симпліційних комплексах обмеженої розмірності, що дозволяє ввести кількісні характеристики для будь-якої фіксованої розмірності. Як наслідок, вони показали, як обчислити деякі [en] 3-многовида, а також як розв'язати ефективно деякі задачі в [en], коли многовид має тріангуляцію (за винятком вироджених симплексів), двоїстий граф якої має малу деревну ширину.

Методи, засновані на теоремі Курселя, використано в [en], поданні знань і логічних висновків, теорії автоматів і перевірці моделей.

Примітки

  1. Eger, 2008.
  2. Courcelle, Engelfriet, 2012.
  3. Downey, Fellows, 2013, с. 265–278.
  4. Courcelle, 1990, с. 12–75.
  5. Borie, Parker, Tovey, 1992, с. 555–581.
  6. Kneis, Langer, 2009, с. 65–81.
  7. Lampis, 2010, с. 549–560.
  8. MSO = monadic second-order
  9. 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. 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. 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. — .
  • 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) — .
  • Rodney G. Downey, Michael R. Fellows. Fundamentals of parameterized complexity. — London : Springer, 2013. — С. 265–278. — (Texts in Computer Science) — . — 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 (28 червня). — С. 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 (28 червня). — С. 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 (28 червня). — С. 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 (28 червня). — С. 125–150. — DOI:10.1007/s002249910009.
  • Stefan Arnborg, Jens Lagergren, Detlef Seese. Easy problems for tree-decomposable graphs // Journal of Algorithms. — 1991. — Т. 12, вип. 2 (28 червня). — С. 308–340. — DOI:10.1016/0196-6774(91)90006-K.
  • Michael Elberfeld, Andreas Jakoby, Till Tantau. . — 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 (28 червня). — С. 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. — 28 червня. — arXiv:1503.01604.
  • D. Kaller. Definability equals recognizability of partial 3-trees and k-connected partial k-trees // Algorithmica. — 2000. — Т. 27, вип. 3 (28 червня). — С. 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 (28 червня). — С. 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 // . — 2007. — Т. 97, вип. 1 (28 червня). — С. 91–126. — (Series B). — DOI:10.1016/j.jctb.2006.04.003.
  • Martin Grohe. . — 2001. — С. 231–236. — DOI:10.1145/380752.380805.
  • Ken-ichi Kawarabayashi, Bruce Reed. . — 2007. — С. 382–390. — DOI:10.1145/1250790.1250848.
  • Georg Gottlob, Stephanie Tien Lee. A logical approach to multicut problems // . — 2007. — Т. 103, вип. 4 (28 червня). — С. 136–141. — DOI:10.1016/j.ipl.2007.03.005.
  • Benjamin A. Burton, Rodney G. Downey. Courcelle's theorem for triangulations. — 2014. — ()
  • 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 (28 червня). — С. 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.

Вікіпедія, Українська, Україна, книга, книги, бібліотека, стаття, читати, завантажити, безкоштовно, безкоштовно завантажити, mp3, відео, mp4, 3gp, jpg, jpeg, gif, png, малюнок, музика, пісня, фільм, книга, гра, ігри, мобільний, телефон, android, ios, apple, мобільний телефон, samsung, iphone, xiomi, xiaomi, redmi, honor, oppo, nokia, sonya, mi, ПК, web, Інтернет

Teore ma Kurselya tverdzhennya pro te sho bud yaku vlastivist grafa sho viznachayetsya v en en mozhna vstanoviti za linijnij chas na grafah z obmezhenoyu derevnoyu shirinoyu Rezultat upershe doviv en 1990 roku i nezalezhno perevidkrili Bori Parker i Tovej Rezultat vvazhayut prototipom algoritmichnih metateorem FormulyuvannyaMnozhini vershin U varianti logiki grafiv drugogo poryadku vidomomu yak MSO1 graf opisuyetsya mnozhinoyu vershin V i binarnim vidnoshennyam sumizhnosti adj a obmezhennya logikoyu drugogo poryadku oznachaye sho vlastivist grafa mozhna viznachiti v terminah mnozhin vershin zadanogo grafa ale ne v terminah mnozhin reber abo par vershin Yak priklad vlastivist grafa rozfarbovuvanosti v tri kolori podanu troma mnozhinami vershin R G i B mozhna viznachiti formuloyu logiki drugogo poryadku Persha chastina ciyeyi formuli zabezpechuye sho tri klasi koloriv vklyuchayut usi vershini grafa a druga chastina zabezpechuye sho kozhen z nih utvoryuye nezalezhnu mnozhinu Mozhna takozh dodati u formulu rechennya sho zabezpechuye neperetinnist troh kolirnih klasiv ale na rezultat ce ne vpline Takim chinom za teoremoyu Kurselya mozhna za linijnij chas pereviriti rozfarbovuvanist u 3 kolori grafa z obmezhenoyu derevnoyu shirinoyu Dlya cogo variantu logiki grafiv teoremu Kurselya mozhna rozshiriti vid derevnoyi shirini do klikovoyi shirini dlya bud yakoyi fiksovanoyi MSO1 vlastivosti P i bud yakoyi fiksovanoyi mezhi b na klikovu shirinu grafa isnuye algoritm linijnogo chasu perevirki chi maye graf z klikovoyu shirinoyu sho ne perevershuye b vlastivist P Mnozhini reber Teoremu Kurselya mozhna vikoristati zi strogishim variantom logiki grafiv drugogo poryadku vidomim yak MSO2 U comu formulyuvanni graf podayetsya mnozhinoyu vershin V mnozhinoyu reber E i vidnoshennyam incidentnosti mizh vershinami i rebrami Cej variant dozvolyaye vvesti kilkisnij pokaznik nad mnozhinoyu vershin abo reber ale ne nad skladnishimi vidnoshennyami nad parami vershin i reber Napriklad vlastivist mati gamiltoniv cikl mozhna viraziti v MSO2 pri viznachenni ciklu yak mnozhini reber sho vklyuchaye rivno po dva rebra incidentnih kozhnij vershini takoyi sho bud yaka neporozhnya vlasna pidmnozhina vershin maye rebro v cikli i ce rebro maye rivno odnu kincevu tochku v pidmnozhini Gamiltonovist odnak ne mozhna viraziti v terminah MSO1 Modulna porivnyannist Inshij napryamok rozshirennya teoremi Kurselya stosuyetsya logichnih formul yaki vklyuchayut predikati dlya pidrahunku dovzhini testu U comu konteksti nemozhlivo zdijsniti dovilni arifmetichni operaciyi nad rozmirami mnozhin i navit nemozhlivo pereviriti sho mnozhini mayut odnakovij rozmir Odnak MSO1 i MSO2 mozhna rozshiriti do logik zvanih CMSO1 i CMSO2 yaki vklyuchayut dlya bud yakih dvoh konstant q i r predikat cardq r S displaystyle operatorname card q r S yakij pereviryaye chi porivnyanna potuzhnist mnozhini S iz r za modulem q Teoremu Kurselya mozhna rozshiriti na ci logiki Rozv yaznist ta optimizaciya Yak stverdzhuvalosya vishe teorema Kurselya zastosovna perevazhno do zadach rozv yaznosti maye graf vlastivist chi ni Ti zh metodi prote dozvolyayut takozh rozv yazati zadachi optimizaciyi v yakih vershinam abo rebram grafa prisvoyeno deyaki cili vagi i shukayetsya minimum abo maksimum vag dlya yakih mnozhina zadovolnyaye pevnij vlastivosti virazhenij u terminah logiki drugogo poryadku Ci zadachi optimizaciyi mozhna rozv yazati za linijnij chas na grafah z obmezhenoyu klikovoyu shirinoyu Yemnisna skladnist Zamist obmezhennya chasovoyi skladnosti algoritmu sho rozpiznaye MSO vlastivosti grafiv z obmezhenoyu derevnoyu shirinoyu mozhna takozh analizuvati en takih algoritmiv tobto obsyag pam yati neobhidnij ponad vhidni dani v pripushenni sho vhidni dani ne mozhut zminyuvatis i zajnyatu pid nih pam yat ne mozhna vikoristati v inshih cilyah Zokrema mozhna rozpiznati grafi z obmezhenoyu derevnoyu shirinoyu i bud yaku MSO vlastivist na cih grafah za dopomogoyu determinovanoyi mashini Tyuringa yaka vikoristovuye tilki logarifmichnu pam yat Strategiya dovedennya i skladnistTipovij pidhid do dovedennya teoremi Kurselya vikoristovuye pobudovu skinchennogo vishidnogo en sho diye na derevnih dekompoziciyah danogo grafa Dokladnishe dva grafi G1 i G2 kozhen zi vkazanoyu pidmnozhinoyu T vershin yaki nazivayut kincevimi mozhna vvazhati ekvivalentnimi zgidno z MSO formuloyu F yaksho dlya bud yakogo inshogo grafa H peretin yakogo z G1 i G2 skladayetsya tilki z vershin T dva grafi G1 H i G2 H povodyatsya odnakovo vidnosno formuli F abo obidva zadovolnyayut F abo obidva ne zadovolnyayut F Ce vidnoshennya ekvivalentnosti i za indukciyeyu za dovzhinoyu F mozhna pokazati yaksho rozmiri T i F obmezheni sho vidnoshennya maye skinchenne chislo klasiv ekvivalentnosti Derevna dekompoziciya zadanogo grafa G skladayetsya z dereva i dlya kozhnogo vuzla dereva pidmnozhini vershin grafa G zvanoyi koshikom Cya pidmnozhina maye zadovolnyati dvom vlastivostyam dlya kozhnoyi vershini v iz G koshik sho mistit v maye buti asocijovanim iz nerozrivnim pidderevom i dlya kozhnogo rebra uv iz G maye isnuvati koshik sho mistit yak u tak i v Vershini v koshiku mozhut rozumitisya yak kincevi elementi pidgrafa G podani pidderevami derevnoyi dekompoziciyi sho rostut iz cogo koshika Yaksho graf G maye obmezhenu derevnu shirinu vin maye derevnu dekompoziciyu v yakij usi koshiki mayut obmezhenij rozmir i takij rozklad mozhna znajti za fiksovano parametrichno rozv yaznij chas Bilsh togo mozhna vibrati derevnij rozklad sho utvoryuye dvijkove derevo z tilki dvoma dochirnimi pidderevami na koshik Takim chinom mozhna zdijsniti vishidne obchislennya na cij derevnij dekompoziciyi obchislyuyuchi identifikator dlya klasu ekvivalentnosti piddereva sho maye korin u kozhnomu koshiku kombinuyuchi rebra predstavlenih vseredini koshika z dvoma identifikatorami klasiv ekvivalentnosti dvoh dochirnih elementiv Rozmir avtomata pobudovanogo takim sposobom ne ye elementarnoyu funkciyeyu vid rozmiru vhidnoyi MSO formuli Cya neelementarna skladnist prizvodit do togo sho nemozhlivo yaksho tilki ne P NP pereviriti MSO vlastivosti za chas fiksovano parametrichno rozv yaznij z elementarnoyu funkcionalnoyu zalezhnistyu vid parametra Gipoteza KurselyaDokaz teoremi Kurselya pokazuye strogishij rezultat ne tilki bud yaku z predikatom pidrahunku dovzhini vlastivist logiki drugogo poryadku mozhna rozpiznati za linijnij chas dlya grafiv z obmezhenoyu derevnoyu shirinoyu ale j yiyi mozhna rozpiznati skinchennim en Gipoteza Kurselya obernena na comu yaksho vlastivist grafiv z obmezhenoyu shirinoyu rozpiznayetsya avtomatom nad derevami to yiyi mozhna viznachiti v terminah logiki drugogo poryadku Popri Lapuarovi sprobi dovedennya gipotezu vvazhayut nedovedenoyu Odnak vidomi deyaki okremi vipadki zokrema gipoteza istinna dlya grafiv z derevnoyu shirinoyu tri i menshe Bilsh togo dlya grafiv Halina osoblivogo vidu grafiv z derevnoyu shirinoyu tri predikat pidrahunku dovzhini ne obov yazkovij dlya cih grafiv bud yaku vlastivist yaku mozhna rozpiznati avtomatom na derevah mozhna viznachiti v terminah logiki drugogo poryadku Ce takozh stosuyetsya zagalom deyakih klasiv grafiv u yakih derevnu dekompoziciyu samu mozhna opisati v MSOL Odnak ce ne mozhe buti istinnim dlya vsih grafiv z obmezhenoyu derevnoyu shirinoyu oskilki v zagalnomu vipadku predikat pidrahunku dovzhini dodaye sili logici drugogo poryadku Napriklad grafi z parnim chislom vershin mozhna rozpiznati za predikatom ale ne mozhna rozpiznati bez nogo Vikonuvanist i teorema Siyiza en dlya formul logiki drugogo poryadku ye zadacheyu viznachennya chi isnuye prinajmni odin graf yakij mozhlivo nalezhit do obmezhenogo simejstva grafiv dlya yakogo formula istinna Dlya dovilnih simejstv grafiv ta dovilnih formul cya zadacha nerozv yazna Vikonuvanist formul MSO2 odnak rozv yazna dlya grafiv z obmezhenoyu derevnoyu shirinoyu a vikonuvanist formul MSO1 rozv yazna dlya grafiv z obmezhenoyu klikovoyu shirinoyu Dovedennya vikoristovuye pobudovu avtomata nad derevom dlya formuli a potim perevirku chi maye avtomat prijnyatnij shlyah Yak chastkovo obernene tverdzhennya Siyiz doviv sho kozhnogo razu koli simejstvo grafiv maye rozv yaznu problemu MSO2 vikonuvanosti simejstvo povinne mati obmezhenu derevnu shirinu Dovedennya spirayetsya na teoremu Robertsona i Sejmura pro te sho simejstva grafiv z neobmezhenoyu derevnoyu shirinoyu mayut dovilno veliki minori reshitki Siyiz takozh pripustiv sho bud yake simejstvo grafiv z rozv yaznoyu problemoyu MSO1 vikonuvanosti povinne mati obmezhenu klikovu shirinu Gipotezu ne dovedeno ale oslablena gipoteza iz zaminoyu MSO1 na CMSO1 istinna ZastosuvannyaGroe vikoristav teoremu Kurselya shob pokazati sho obchislennya chisla shreshen grafa G ye en zadacheyu z kvadratichnoyu zalezhnistyu vid rozmiru G sho pokrashuye kubichnij za chasom algoritm zasnovanij na teoremi Robertsona Sejmura Piznishe polipshennya do linijnogo chasu Kavarabajashi i Riyidom vikoristovuye toj samij pidhid Yaksho danij graf G maye malu derevnu shirinu teoremu Kurselya mozhna zastosuvati do ciyeyi problemi bezposeredno Z inshogo boku yaksho G maye veliku derevnu shirinu to vin mistit velikij minor reshitku vseredini yakogo graf mozhna sprostiti ne zminyuyuchi chisla shreshen Algoritm Groe vikonuye ce sproshennya do otrimannya grafa z maloyu derevnoyu shirinoyu a potim zastosovuye teoremu Kurselya dlya rozv yazannya zmenshenoyi pidzadachi Gottlob i Li zauvazhili sho teorema Kurselya zastosovna do deyakih zadach poshuku minimalnoyi mnozhini rozriziv u grafi yaksho struktura utvorena grafom i mnoyu rozrizalnih par maye obmezhenu derevnu shirinu V rezultati voni otrimali fiksovano parametrichno rozv yazuvanij algoritm dlya cih zadach parametrizovanij odnim parametrom sho pokrashuye poperedni rozv yazki yaki kombinuyut kilka parametriv V obchislyuvalnij topologiyi Barton i Dauni rozshirili teoremu Kurselya z MSO2 do logiki drugogo poryadku na simplicijnih kompleksah obmezhenoyi rozmirnosti sho dozvolyaye vvesti kilkisni harakteristiki dlya bud yakoyi fiksovanoyi rozmirnosti Yak naslidok voni pokazali yak obchisliti deyaki en 3 mnogovida a takozh yak rozv yazati efektivno deyaki zadachi v en koli mnogovid maye triangulyaciyu za vinyatkom virodzhenih simpleksiv dvoyistij graf yakoyi maye malu derevnu shirinu Metodi zasnovani na teoremi Kurselya vikoristano v en podanni znan i logichnih visnovkiv teoriyi avtomativ i perevirci modelej PrimitkiEger 2008 Courcelle Engelfriet 2012 Downey Fellows 2013 s 265 278 Courcelle 1990 s 12 75 Borie Parker Tovey 1992 s 555 581 Kneis Langer 2009 s 65 81 Lampis 2010 s 549 560 MSO monadic second order Courcelle Makowsky Rotics 2000 s 125 150 Courcelle Engelfriet 2012 s 336 Proposition 5 13 Arnborg Lagergren Seese 1991 s 308 340 Elberfeld Jakoby Tantau 2010 s 143 152 Downey Fellows 2013 s 266 Theorem 13 1 1 Downey Fellows 2013 s 195 203 Section 10 5 Bodlaender s theorem Downey Fellows 2013 s 237 247 Section 12 6 Tree automata Frick Grohe 2004 s 3 31 Lapoire 1998 s 618 628 Jaffke Bodlaender 2015 Kaller 2000 s 348 381 Seese 1991 Seese 1991 s 169 195 Courcelle Oum 2007 s 91 126 Grohe 2001 Kawarabayashi Reed 2007 Grohe 2001 s 231 236 Kawarabayashi Reed 2007 s 382 390 Gottlob Lee 2007 Gottlob Lee 2007 s 136 141 Burton Downey 2014 Grohe Marino 1999 s 70 82 Gottlob Pichler Wei 2010 s 105 132 Madhusudan Parlato 2011 s 283 294 Obdrzalek 2003 s 80 92 LiteraturaEger 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 T 138 Encyclopedia of Mathematics and its Applications ISBN 9781139644006 Rodney G Downey Michael R Fellows Fundamentals of parameterized complexity London Springer 2013 S 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 T 85 vip 1 28 chervnya S 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 T 7 vip 5 6 28 chervnya S 555 581 DOI 10 1007 BF01758777 Joachim Kneis Alexander Langer A practical approach to Courcelle s theorem Electronic Notes in Theoretical Computer Science 2009 T 251 28 chervnya S 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 T 6346 S 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 T 33 vip 2 28 chervnya S 125 150 DOI 10 1007 s002249910009 Stefan Arnborg Jens Lagergren Detlef Seese Easy problems for tree decomposable graphs Journal of Algorithms 1991 T 12 vip 2 28 chervnya S 308 340 DOI 10 1016 0196 6774 91 90006 K Michael Elberfeld Andreas Jakoby Till Tantau 2010 S 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 T 130 vip 1 3 28 chervnya S 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 25OCo27 1998 Proceedings 1998 S 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 28 chervnya arXiv 1503 01604 D Kaller Definability equals recognizability of partial 3 trees and k connected partial k trees Algorithmica 2000 T 27 vip 3 28 chervnya S 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 T 53 vip 2 28 chervnya S 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 2007 T 97 vip 1 28 chervnya S 91 126 Series B DOI 10 1016 j jctb 2006 04 003 Martin Grohe 2001 S 231 236 DOI 10 1145 380752 380805 Ken ichi Kawarabayashi Bruce Reed 2007 S 382 390 DOI 10 1145 1250790 1250848 Georg Gottlob Stephanie Tien Lee A logical approach to multicut problems 2007 T 103 vip 4 28 chervnya S 136 141 DOI 10 1016 j ipl 2007 03 005 Benjamin A Burton Rodney G Downey Courcelle s theorem for triangulations 2014 Martin Grohe Julian Marino Database Theory ICDT 99 7th International Conference Jerusalem Israel January 10 12 1999 Proceedings 1999 T 1540 S 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 T 174 vip 1 28 chervnya S 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 T 46 1 S 283 294 SIGPLAN Notices DOI 10 1145 1926385 1926419 Jan Obdrzalek Computer Aided Verification 15th International Conference CAV 2003 Boulder CO USA July 8 12 2003 Proceedings 2003 T 2725 S 80 92 Lecture Notes in Computer Science DOI 10 1007 978 3 540 45069 6 7

Дата публікації:
Топ