Courcellova věta

Courcelleův teorém je tvrzení, že libovolnou vlastnost grafu definovanou v monadické logice druhého řádu grafové logice lze stanovit v lineárním čase na grafech s omezenou šířkou stromu [1] [2] [3] . Výsledek byl poprvé prokázán Brunem Courcellem v roce 1990 [4] a nezávisle znovu objeven Bory, Parker a Tovey [5] . Výsledek je považován za prototyp algoritmických metateorémů [6] [7] .

Formulace

Množiny vrcholů

Ve variantě logiky grafu druhého řádu známé jako MSO 1 [8] je graf popsán množinou vrcholů V a binárním vztahem sousednosti adj(.,.) a omezení na logiku druhého řádu znamená, že vlastnost grafu může být definována z hlediska množin vrcholů daného grafu, ale ne z hlediska množin hran nebo dvojic vrcholů.

Například vlastnost tříbarevného grafu (reprezentovaného třemi sadami vrcholů R , G a B ) lze definovat logickým vzorcem druhého řádu.

∃ 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 )).

První část tohoto vzorce zajišťuje, že tři barevné třídy zahrnují všechny vrcholy grafu, a druhá část zajišťuje, že každá z nich tvoří nezávislou množinu . (Můžete také do vzorce přidat klauzuli, abyste zajistili, že se tři barevné třídy nebudou protínat, ale to neovlivní výsledek.) Podle Courcelleovy věty je tedy možné zkontrolovat 3-barevnost grafu pomocí a omezená šířka stromu v lineárním čase.

Pro tuto variantu grafové logiky lze Courcelleův teorém rozšířit ze šířky stromu na šířku kliky — pro jakoukoli pevnou vlastnost  MSO 1 P a jakoukoli pevnou mez b na šířku kliky v grafu existuje lineární časový algoritmus, který kontroluje, zda má graf a šířka kliky nejvýše b . vlastnost P [9] .

Sady hran

Courcelleův teorém lze použít s přísnější logikou grafů druhého řádu známou jako MSO 2 . V této formulaci je graf reprezentován množinou vrcholů V , množinou hran E a incidenčním vztahem mezi vrcholy a hranami. Tato volba umožňuje kvantifikovat přes sadu vrcholů nebo hran, ale ne přes složitější vztahy přes páry vrcholů a hran.

Například vlastnost mít hamiltonovský cyklus může být vyjádřena v MSO 2 definováním cyklu jako množiny hran, včetně přesně dvou hran spadajících do každého vrcholu, takže každá neprázdná vlastní podmnožina vrcholů má hranu v cyklu a tato hrana má přesně jeden koncový bod v podmnožině. Hamiltonianitu však nelze vyjádřit pomocí MSO 1 [10] .

Modulární srovnatelnost

Další rozšíření Courcelleovy věty se týká logických vzorců, které obsahují predikáty pro výpočet délky testu. V tomto kontextu je nemožné provádět libovolné aritmetické operace s velikostmi množin a dokonce je nemožné zkontrolovat, že množiny mají stejnou velikost. MSO 1 a MSO 2 však mohou být rozšířeny na logiku nazývanou CMSO 1 a CMSO 2 , která obsahuje pro libovolné dvě konstanty q a r predikát , který testuje, zda je mohutnost S srovnatelná s r modulo q . Courcelleův teorém lze rozšířit i na tyto logiky [4] .

Řešitelnost a optimalizace

Jak bylo uvedeno výše, Courcelleova věta platí hlavně pro problémy řešitelnosti  – ať už má graf nějakou vlastnost, nebo ne. Stejné metody však umožňují i ​​řešení optimalizačních problémů , kdy jsou vrcholům nebo hranám grafu přiřazeny nějaké celočíselné váhy a hledají se minimální nebo maximální váhy, pro které množina splňuje danou vlastnost vyjádřenou v sekundách- logika objednávky. Tyto optimalizační problémy lze řešit v lineárním čase na grafech s omezenou šířkou kliky [9] [11] .

Kapacitní složitost

Namísto omezování časové složitosti algoritmu, který rozpoznává vlastnosti MSO ohraničených grafů šířky stromu, lze také analyzovat kapacitní složitost takových algoritmů, to znamená množství paměti požadované nad rámec vstupních dat (za předpokladu, že vstupní data nelze měnit a jsou obsazena jejich pamětí nelze použít pro jiné účely). Zejména lze rozpoznat ohraničené grafy šířky stromu a jakoukoli vlastnost MSO na těchto grafech pomocí deterministického Turingova stroje , který používá pouze logaritmickou paměť [12] .

Důkaz strategie a složitosti

Typický přístup k dokazování Courcelleovy věty využívá konstrukci konečného vzestupného automatu působícího na stromové rozklady daného grafu [6] .

Podrobněji, dva grafy G 1 a G 2 , každý se specifikovanou podmnožinou T vrcholů, nazývaných koncové body, lze považovat za ekvivalentní podle vzorce F MSO , pokud pro jakýkoli jiný graf H , jehož průsečík s G 1 a G 2 se skládá pouze z vrcholů T se dva grafy G 1  ∪  H a G 2  ∪  H chovají vzhledem k formuli F  stejně — buď oba splňují F , nebo oba nesplňují F . Toto je relace ekvivalence a indukcí na délce F lze ukázat (jsou-li velikosti T a F omezené), že relace má konečný počet tříd ekvivalence [13] .

Stromový rozklad daného grafu G se skládá ze stromu a pro každý uzel stromu z podmnožiny vrcholů G , nazývané koš. Tato podmnožina musí splňovat dvě vlastnosti – pro každý vrchol v v G musí být segment obsahující v asociován s pevným podstromem a pro každou hranu uv v G musí existovat segment obsahující jak u , tak v . Vrcholy v koši lze považovat za konečné prvky podgrafu G reprezentované podstromy rozkladu stromů vyrůstajícími z tohoto koše. Pokud má graf G ohraničenou šířku stromu, má stromový rozklad, ve kterém mají všechny koše omezenou velikost a takový rozklad lze nalézt v pevně-parametricky řešitelném čase [14] . Navíc je možné zvolit rozklad stromu, který vytvoří binární strom s pouze dvěma podřízenými podstromy na kbelík. Je tedy možné provést výpočet zdola nahoru na této dekompozici stromu výpočtem identifikátoru třídy ekvivalence podstromu zakořeněného v každém segmentu zkombinováním hran reprezentovaných v rámci segmentu se dvěma identifikátory třídy ekvivalence dvou potomků [15 ] .

Velikost takto konstruovaného automatu není elementární funkcí velikosti vstupního vzorce MSO. Tato neelementární složitost vede k tomu, že je nemožné (pokud P = NP ) zkontrolovat MSO-vlastnosti v čase, který je pevně-parametricky řešitelný s elementární funkční závislostí na parametru [16] .

Courcelleova hypotéza

Důkaz Courcelleovy věty ukazuje přesnější výsledek – nejenže lze jakoukoli (s predikátem počítající délku) vlastnost logiky druhého řádu rozpoznat v lineárním čase pro grafy s omezenou šířkou stromu, ale lze ji rozpoznat také pomocí konečného automat nad stromem . Courcelleova domněnka je opakem toho - pokud je vlastnost grafů s omezenou šířkou rozpoznána automatem nad stromy, pak ji lze definovat v termínech logiky druhého řádu. Přes pokusy Lapoira o důkaz [17] je domněnka považována za neprokázanou [18] . Jsou však známy některé speciální případy, zejména domněnka platí pro grafy se šířkou stromu tři a menší [19] .

Navíc pro Halinovy ​​grafy (speciální druh tří grafů o šířce stromu) není nutný predikát počítání délky - u těchto grafů lze jakoukoli vlastnost, kterou dokáže rozpoznat automat na stromech, definovat v termínech sekund- logika objednávky. Totéž platí obecněji pro určité třídy grafů, ve kterých lze samotný rozklad stromu popsat v MSOL. To však nemůže platit pro všechny grafy s omezenou šířkou stromu, protože predikát počítání délky obecně dodává logice druhého řádu na síle. Například grafy se sudým počtem vrcholů lze rozpoznat podle predikátu, ale bez něj nelze rozpoznat [18] .

Splnitelnost a Seaisova věta

Problém splnitelnosti pro logické vzorce druhého řádu je problém určit, zda existuje alespoň jeden graf (případně patřící do omezené rodiny grafů), pro který vzorec platí. Pro libovolné rodiny grafů a libovolných vzorců je tento problém neřešitelný . Splnitelnost vzorců MSO 2 je však rozhoditelná pro grafy s omezenou šířkou stromu a splnitelnost vzorců MSO 1 je rozhoditelná pro grafy s omezenou šířkou kliky. Důkaz využívá vytvoření automatu nad stromem pro vzorec a následné ověření, zda má automat přijatelnou cestu.

Jako částečný opak, Sees [20] dokázal, že kdykoli má rodina grafů rozhoditelný problém splnitelnosti MSO 2 , rodina musí mít omezenou šířku stromu. Důkaz je založen na teorému Robertsona a Seymoura, že rodiny grafů s neomezenou šířkou stromu mají libovolně velké menší mřížky [ 21 ] . Sees také předpokládal, že jakákoli rodina grafů s rozhoditelným problémem splnitelnosti MSO 1 musí mít omezenou šířku kliky. Hypotéza nebyla prokázána, ale oslabená hypotéza s nahrazením MSO 1 za CMSO 1 je pravdivá [22] .

Aplikace

Grohe [23] použil Courcelleovu větu, aby ukázal, že výpočet průsečíku grafu G je problém s pevnými parametry řešitelnými s kvadratickou závislostí na velikosti G , což zlepšuje časově kubický algoritmus založený na Robertsonově- Seymourova věta . Pozdější vylepšení lineárního času od Kawarabayashi a Reeda [24] používá stejný přístup. Pokud má daný graf G malou stromovou šířku, lze na tento problém přímo aplikovat Courcelleovu větu. Na druhou stranu, pokud má G velkou šířku stromu, pak obsahuje velkou menší mřížku , uvnitř které lze graf zjednodušit bez změny počtu průsečíků. Groeův algoritmus provádí toto zjednodušení, dokud zbývající graf nemá malou stromovou šířku, a poté aplikuje Courcelleovu větu k vyřešení redukovaného dílčího problému [25] [26] .

Gottlob a Lee [27] si všimli, že Courcelleův teorém je aplikovatelný na některé problémy hledání minimálních násobných řezů v grafu, pokud struktura tvořená grafem a sadou řezných párů má omezenou šířku stromu. V důsledku toho získali pro tyto problémy řešitelný algoritmus s pevnými parametry, parametrizovaný jediným parametrem, treewidth, který vylepšuje předchozí řešení, která kombinují více parametrů [28] .

Ve výpočetní topologii rozšířili Barton a Downey [29] Courcelleův teorém MSO 2 na logiku druhého řádu o simpliciálních komplexech ohraničené dimenze, což umožňuje zavedení kvantitativních charakteristik pro jakoukoli pevnou dimenzi. V důsledku toho ukázali, jak vypočítat některé kvantové invarianty 3 - variet a také jak efektivně řešit některé problémy v diskrétní Morseově teorii , když varieta má triangulaci (kromě degenerovaných simpliců), jejíž duální graf má malá šířka stromu [29] .

Metody založené na Courcelleově teorému byly použity v teorii databází [30] , reprezentaci znalostí a vyvozování [31] , teorii automatů [32] a model checkingu [33] .

Poznámky

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

Literatura