Twierdzenie Courcelle'a

W badaniu algorytmów grafowych twierdzenie Courcelle'a jest stwierdzeniem, że każdą właściwość grafową definiowalną w monadycznej logice grafów drugiego rzędu można rozstrzygnąć w czasie liniowym na grafach o ograniczonej szerokości drzewa . Wynik został po raz pierwszy udowodniony przez Bruno Courcelle w 1990 roku i niezależnie ponownie odkryty przez Borie, Parker i Tovey (1992) . Jest uważany za archetyp algorytmicznych meta-twierdzeń .

preparaty

Zestawy wierzchołków

W jednej odmianie monadycznej logiki wykresu drugiego rzędu, znanej jako MSO ₁ , wykres jest opisany przez zbiór wierzchołków i binarną relację sąsiedztwa ${\ Displaystyle \ nazwa operatora {przym.} (.,.)}$ , a ograniczenie do logiki monadycznej oznacza, że ​​dana właściwość grafu może być zdefiniowana w kategoriach zbiorów wierzchołków danego grafu, ale nie w kategoriach zbiorów krawędzi czy zbiorów krotek wierzchołków.

Na przykład właściwość wykresu, który można $pokolorować$ trzema kolorami (reprezentowanymi przez trzy zestawy wierzchołków , i i ) może być zdefiniowana przez sekundę monadyczną R $R$$}$ -formuła zamówienia

$${\ displaystyle {\begin{wyrównane}\istnieje R\ \istnieje G\ \istnieje B\ {\Bigl (}&\forall v\ (v\in R\vee v\in G\vee v\in B)\klin { }\\&\forall u\ \forall v\ {\bigl (}(u\in R\wedge v\in R)\rightarrow \lnot \operatorname {adj} (u,v){\bigr )}\wedge {}\\&\forall u\ \forall v\ {\bigl (}(u\in G\wedge v\in G)\rightarrow \lnot \operatorname {adj} (u,v){\bigr )}\ klin {}\\&\forall u\ \forall v\ {\bigl (}(u\in B\klin v\in B)\rightarrow \lnot \operatorname {adj} (u,v){\bigr )} {\Bigr}}\end{wyrównane}}}$$

z konwencją nazewnictwa , zgodnie z którą zmienne pisane wielkimi literami oznaczają zbiory wierzchołków, a zmienne pisane małymi literami oznaczają poszczególne wierzchołki (tak, że wyraźna deklaracja, która jest która, może zostać pominięta we wzorze). Pierwsza część tego wzoru zapewnia, że ​​trzy klasy kolorów obejmują wszystkie wierzchołki grafu, a reszta zapewnia, że ​​każdy z nich tworzy niezależny zestaw . (Możliwe byłoby również dodanie klauzul do wzoru, aby upewnić się, że trzy klasy kolorów są rozłączne, ale nie ma to wpływu na wynik). Zatem na mocy twierdzenia Courcelle'a można przetestować 3-kolorowalność wykresów o ograniczonej szerokości drzewa w czas liniowy.

$\ Pi}$ przypadku tej odmiany logiki grafów twierdzenie Courcelle'a można rozszerzyć od szerokości drzewa do szerokości kliki : dla każdej ustalonej właściwości MSO ₁ i każdej ustalonej granicy ${\ displaystyle$ szerokości kliki a Π $\ Pi}$ , istnieje algorytm czasu liniowego do testowania, czy wykres o szerokości kliki co najwyżej ma właściwość $displaystyle$ . Pierwotne sformułowanie tego wyniku wymagało podania wykresu wejściowego wraz z konstrukcją dowodzącą, że ma on ograniczoną szerokość kliki, ale późniejsze algorytmy aproksymacji szerokości kliki usunęły ten wymóg.

Zestawy brzegowe

Twierdzenie Courcelle'a może być również użyte z silniejszą odmianą monadycznej logiki drugiego rzędu, znaną jako MSO ₂ . W tym sformułowaniu graf jest reprezentowany przez zbiór V wierzchołków, zbiór E krawędzi oraz relację padania między wierzchołkami a krawędziami. Ta odmiana pozwala na kwantyfikację na zestawach wierzchołków lub krawędzi, ale nie na bardziej złożonych relacjach na krotkach wierzchołków lub krawędzi.

Na przykład właściwość posiadania cyklu Hamiltona można wyrazić w MSO ₂ , opisując cykl jako zbiór krawędzi, który zawiera dokładnie dwie krawędzie incydentne z każdym wierzchołkiem, tak że każdy niepusty właściwy podzbiór wierzchołków ma krawędź w domniemanym cyklu z dokładnie jednym punktem końcowym w podzbiorze. Jednak hamiltoniczności nie można wyrazić w MSO ₁ .

Oznaczone wykresy

Możliwe jest zastosowanie tych samych wyników do grafów, w których wierzchołki lub krawędzie mają etykiety ze stałego skończonego zbioru, albo poprzez rozszerzenie logiki grafów w celu włączenia predykatów opisujących etykiety, albo poprzez przedstawienie etykiet za pomocą niekwantyfikowanych zmiennych zbioru wierzchołków lub zbioru krawędzi .

Modułowe kongruencje

Inny kierunek rozszerzenia twierdzenia Courcelle'a dotyczy formuł logicznych zawierających predykaty do obliczania rozmiaru testu. W tym kontekście nie jest możliwe wykonywanie dowolnych operacji arytmetycznych na rozmiarach zbiorów, ani nawet sprawdzanie, czy dwa zbiory mają ten sam rozmiar. Jednak MSO ₁ i MSO ₂ można rozszerzyć na logiki zwane CMSO ₁ i CMSO ₂ , które obejmują dla każdych dwóch stałych q i r ${\ displaystyle \ nazwa operatora {karta} _ {q, r}(S)}$ predykatu , który sprawdza, czy liczność zbioru S jest zgodna z r modulo q . Twierdzenie Courcelle'a można rozszerzyć na te logiki.

Decyzja a optymalizacja

Jak stwierdzono powyżej, twierdzenie Courcelle'a stosuje się przede wszystkim do problemów decyzyjnych : czy graf ma właściwość, czy nie. Jednak te same metody pozwalają również na rozwiązanie problemów optymalizacyjnych , w których wierzchołki lub krawędzie grafu mają wagi całkowite i poszukuje się zbioru wierzchołków o minimalnej lub maksymalnej wadze, który spełnia daną właściwość wyrażoną w logice drugiego rzędu. Te problemy optymalizacyjne można rozwiązać w czasie liniowym na wykresach o ograniczonej szerokości kliki.

Złożoność przestrzeni

Zamiast ograniczać złożoność czasową algorytmu, który rozpoznaje właściwość MSO na grafach o ograniczonej szerokości drzewa, można również analizować złożoność przestrzenną takiego algorytmu; to znaczy ilość pamięci potrzebnej poza rozmiarem samego wejścia (które zakłada się, że jest reprezentowane tylko do odczytu, tak że jego wymagań dotyczących miejsca nie można wykorzystać do innych celów). W szczególności możliwe jest rozpoznanie wykresów o ograniczonej szerokości drzewa i dowolnej właściwości MSO na tych wykresach za pomocą deterministycznej maszyny Turinga , która wykorzystuje tylko przestrzeń logarytmiczną .

Dowód strategii i złożoności

automatu drzewiastego oddolnego, który działa na dekompozycje drzewa danego grafu.

Bardziej szczegółowo, dwa grafy G ₁ i G ₂ , każdy z określonym podzbiorem T wierzchołków zwanych końcówkami, można zdefiniować jako równoważne w odniesieniu do wzoru MSO F , jeśli dla wszystkich innych grafów H , których przecięcie z G ₁ i G ₂ składa się tylko z wierzchołków w T , dwa grafy G ₁ ∪ H i G ₂ ∪ H zachowują się tak samo względem F : albo oba modelują F , albo oba nie modelują F . Jest to relacja równoważności i można wykazać przez indukcję po długości F , że (gdy oba rozmiary T i F są ograniczone) ma ona skończenie wiele klas równoważności .

Dekompozycja drzewa danego grafu G składa się z drzewa i dla każdego węzła drzewa podzbioru wierzchołków G zwanego workiem. Musi spełniać dwie właściwości: dla każdego wierzchołka v G , worki zawierające v muszą być powiązane z ciągłym poddrzewem drzewa, a dla każdej krawędzi uv G , musi istnieć worek zawierający zarówno u , jak i v . Wierzchołki w worku można traktować jako końcówki podgrafu G , reprezentowanego przez poddrzewo dekompozycji drzewa wychodzącego z tego worka. Kiedy G ma ograniczoną szerokość drzewa, ma dekompozycję drzewa, w której wszystkie torby mają ograniczony rozmiar, a taki rozkład można znaleźć w czasie o ustalonych parametrach. Co więcej, możliwe jest wybranie tej dekompozycji drzewa tak, aby tworzyło drzewo binarne , z tylko dwoma poddrzewami potomnymi na worek. Dlatego możliwe jest wykonanie obliczeń oddolnych na tej dekompozycji drzewa, obliczając identyfikator klasy równoważności poddrzewa zakorzenionego w każdym worku, łącząc krawędzie reprezentowane w worku z dwoma identyfikatorami klas równoważności jego dwóch dzieci.

Wielkość tak skonstruowanego automatu nie jest elementarną funkcją wielkości wejściowej formuły MSO. Ta nieelementarna złożoność jest konieczna w tym sensie, że (chyba że P = NP ) nie jest możliwe przetestowanie właściwości MSO na drzewach w czasie, który jest możliwy do ustalenia przy stałym parametrze z elementarną zależnością od parametru.

Twierdzenie Bojańczyka-Pilipczuka

Dowody twierdzenia Courcelle'a pokazują silniejszy wynik: nie tylko każdą (zliczającą) monadyczną właściwość drugiego rzędu można rozpoznać w czasie liniowym dla grafów o ograniczonej szerokości drzewa, ale także można ją rozpoznać za pomocą automatu drzewa o skończonych stanach . Courcelle przypuszczał, że jest odwrotnie: jeśli właściwość grafów o ograniczonej szerokości drzewa jest rozpoznawana przez automat drzewny, to można ją zdefiniować w zliczaniu monadycznej logiki drugiego rzędu. W 1998 Lapoire (1998) zażądał rozwiązania przypuszczenia. Jednak dowód jest powszechnie uważany za niezadowalający. Do 2016 roku rozwiązano tylko kilka przypadków szczególnych: w szczególności przypuszczenie zostało udowodnione dla grafów o szerokości drzewa co najwyżej trzech, dla grafów połączonych k o szerokości drzewa k , dla grafów o stałej szerokości drzewa i cięciwy oraz dla k - grafy płaszczyzn zewnętrznych . Ogólną wersję hipotezy ostatecznie udowodnili Mikołaj Bojańczyk i Michał Pilipczuk.

Co więcej, dla grafów Halina (specjalny przypadek trzech grafów o szerokości drzewa) liczenie nie jest potrzebne: dla tych grafów każda właściwość, którą może rozpoznać automat drzewny, może być również zdefiniowana w monadycznej logice drugiego rzędu. To samo odnosi się bardziej ogólnie do pewnych klas grafów, w których dekompozycja drzewa może być opisana w MSOL. Jednak nie może to być prawdą dla wszystkich grafów o ograniczonej szerokości drzewa, ponieważ ogólnie zliczanie dodaje dodatkowej mocy w stosunku do monadycznej logiki drugiego rzędu bez liczenia. Na przykład grafy z parzystą liczbą wierzchołków można rozpoznać za pomocą liczenia, ale nie bez.

Spełnialność i twierdzenie Seese'a

Problem spełnialności formuły monadycznej logiki drugiego rzędu polega na określeniu, czy istnieje co najmniej jeden wykres (prawdopodobnie w ograniczonej rodzinie grafów), dla którego wzór jest prawdziwy. W przypadku dowolnych rodzin grafów i dowolnych formuł problem ten jest nierozstrzygalny . Jednak spełnialność formuł MSO ₂ jest rozstrzygalna dla grafów o ograniczonej szerokości drzewa, a spełnialność formuł MSO ₁ jest rozstrzygalna dla grafów o ograniczonej szerokości kliki. Dowód polega na zbudowaniu automatu drzewiastego dla formuły, a następnie sprawdzeniu, czy automat ma akceptującą ścieżkę.

Jako częściowa odwrotność, Seese (1991) udowodnił, że ilekroć rodzina grafów ma rozstrzygalny problem spełnialności MSO ₂ , rodzina musi mieć ograniczoną szerokość drzewa. Dowód opiera się na twierdzeniu Robertsona i Seymoura , że ​​rodziny grafów o nieograniczonej szerokości drzewa mają dowolnie duże drugorzędne siatki . Seese przypuszczał również, że każda rodzina grafów z rozstrzygalnym problemem spełnialności MSO ₁ musi mieć ograniczoną szerokość kliki; nie zostało to udowodnione, ale osłabienie hipotezy, która zastępuje MSO ₁ przez CMSO ₁ , jest prawdziwe.

Aplikacje

Grohe (2001) użył twierdzenia Courcelle'a, aby pokazać, że obliczenie liczby przecięcia wykresu G jest wykonalne dla stałych parametrów z kwadratową zależnością od rozmiaru G , ulepszając algorytm czasu sześciennego oparty na twierdzeniu Robertsona – Seymoura . Dodatkowe późniejsze udoskonalenie czasu liniowego autorstwa Kawarabayashi i Reeda (2007) opiera się na tym samym podejściu. Jeśli dany graf G ma małą szerokość drzewa, twierdzenie Courcelle'a można zastosować bezpośrednio do tego problemu. Z drugiej strony, jeśli G ma dużą szerokość drzewa, to zawiera dużą drobną siatkę , w obrębie której wykres można uprościć, pozostawiając niezmienioną liczbę przecięć. Algorytm Grohe'a wykonuje te uproszczenia, dopóki pozostały graf nie ma małej szerokości drzewa, a następnie stosuje twierdzenie Courcelle'a do rozwiązania zredukowanego podproblemu.

Gottlob i Lee (2007) zauważyli, że twierdzenie Courcelle'a ma zastosowanie do kilku problemów znajdowania minimalnych cięć wielokierunkowych w grafie, gdy struktura utworzona przez graf i zbiór par cięć ma ograniczoną szerokość drzewa. W rezultacie uzyskują wykonalny algorytm o stałych parametrach dla tych problemów, sparametryzowany jednym parametrem, szerokością drzewa, ulepszając poprzednie rozwiązania, które łączyły wiele parametrów.

W topologii obliczeniowej Burton i Downey (2014) rozszerzają twierdzenie Courcelle'a z MSO ₂ do formy monadycznej logiki drugiego rzędu na uproszczonych zespołach o ograniczonym wymiarze, która umożliwia kwantyfikację na uproszczeniach o dowolnym ustalonym wymiarze. W konsekwencji pokazują, jak obliczyć pewne niezmienniki kwantowe 3- rozmaitości , a także jak skutecznie rozwiązać pewne problemy w dyskretnej teorii Morse'a , gdy rozmaitość ma triangulację (unikając zdegenerowanych uproszczeń), której graf dualny ma małą szerokość drzewa.

Metody oparte na twierdzeniu Courcelle'a zostały również zastosowane w teorii baz danych , reprezentacji i rozumowaniu wiedzy , teorii automatów i sprawdzaniu modeli .