Opisowa złożoność

W teoretycznej informatyki The złożoność opisowe jest gałęzią teorii złożoności i teorii modeli , który charakteryzuje klas złożoności pod względem logiki do opisywania problemów.

Złożoność opisowa daje nowy punkt widzenia, ponieważ definiujemy klasy złożoności bez odwoływania się do pojęcia maszyn, takich jak maszyny Turinga . Na przykład klasa NP odpowiada zestawowi problemów dających się wyrazić w egzystencjalnej logice drugiego rzędu : jest to twierdzenie Fagina .

Zasada

Przykład: kolorowanie wykresu

Wyjaśnijmy zasadę złożoności opisowej problemem 3-kolorowania grafu . Chodzi o problem decyzyjny, który polega na poznaniu danego grafu, czy można pokolorować jego wierzchołki trzema kolorami, tak aby dwa sąsiadujące ze sobą wierzchołki nie były tego samego koloru. Rysunek po prawej przedstawia przykład wykresu z trzema kolorami.

Problem 3 barwienia jest w klasie NP . Rzeczywiście, mając dane kolorowanie, łatwo jest sprawdzić (tj. w czasie wielomianowym w rozmiarze grafu), że dwa sąsiednie wierzchołki nie są tego samego koloru.
Natomiast problem trójkolorowości opisuje formuła logiki następnego egzystencjalnego drugiego rzędu . Ta formuła brzmi: „istnieje jeden zestaw wierzchołków C 1 , inny zestaw wierzchołków C 2 , inny zestaw wierzchołków C 3 (1, 2, 3 to trzy możliwe kolory), takie jak: ∃VS1,∃VS2,∃VS3,(∀s,⋁ja=13VSja(s))∧(∀s⋀ja,jot=1ja≠jot3(¬VSja(s)∨¬VSjot(s)))∧(∀t,R(s,t)→⋀ja=13(¬VSja(s)∨¬VSja(t))){\ displaystyle \ istnieje C_ {1}, \ istnieje C_ {2}, \ istnieje C_ {3}, \ left (\ forall s, \ bigvee _ {i = 1} ^ {3} C_ {i} (s) \ right) \ land \ left (\ forall s \ bigwedge _ {i, j = 1i \ neq j} ^ {3} (\ lnie C_ {i} (s) \ lor \ lnot C_ {j} (s)) \ right) \ land \ left (\ forall t, R (s, t) \ rightarrow \ bigwedge _ {i = 1} ^ {3} (\ l nie C_ {i} (s) \ lor \ l nie C_ {i} (t)) \ prawo)} ${\ displaystyle \ istnieje C_ {1}, \ istnieje C_ {2}, \ istnieje C_ {3}, \ left (\ forall s, \ bigvee _ {i = 1} ^ {3} C_ {i} (s) \ right) \ land \ left (\ forall s \ bigwedge _ {i, j = 1i \ neq j} ^ {3} (\ lnie C_ {i} (s) \ lor \ lnot C_ {j} (s)) \ right) \ land \ left (\ forall t, R (s, t) \ rightarrow \ bigwedge _ {i = 1} ^ {3} (\ l nie C_ {i} (s) \ lor \ l nie C_ {i} (t)) \ prawo)}$
- dowolny wierzchołek jest pokolorowany (każdy wierzchołek należy do jednego z podzbiorów C i ),
- każdy wierzchołek ma co najwyżej jeden kolor (każdy wierzchołek znajduje się co najwyżej w jednym z podzbiorów C i ),
- dwa sąsiednie wierzchołki mają różne kolory.

Problem decyzyjny jako zapytanie

Tak więc, w złożoności opisowej, problem decyzyjny jest opisany za pomocą logicznej formuły, która odpowiada wykonaniu zapytania (na przykład zapytanie „czy graf 3 można pokolorować?”). Przykładem problemu decyzyjnego jest model (np. wykres dla problemu trzech kolorów jest postrzegany jako model), na którym można oceniać formuły logiczne. Pozytywne przypadki problemu decyzyjnego (tj. w przykładzie 3-kolorowe wykresy) to dokładnie modele, w których wzór jest prawdziwy.

Inny przykład

Rozważmy problem decyzyjny A polegający na ustaleniu, czy graf G jest taki, że każdy wierzchołek G dopuszcza krawędź incydentu. Wykres G jest postrzegany jako model, w którym elementami domeny są wierzchołki grafu, a relacja grafu jest predykatem . Problem decyzyjny A może być wyrażony w logice pierwszego rzędu, ponieważ pozytywne przypadki są opisane wzorem (każdy wierzchołek s dopuszcza następcę t). $R$ ${\ displaystyle \ forall s, \ isist t, sRt}$

Twierdzenie Fagina

Pierwszym wynikiem tej dziedziny, a jednym z najważniejszych jest twierdzenie Fagina, które podaje równoważność między:

klasy NP , z definicji, klasa problemów decyzyjnych, dla których nie jest łatwo poszukać rozwiązania;
oraz klasę problemów dających się wyrazić w egzystencjalnej logice drugiego rzędu , czyli logice drugiego rzędu, w której zabrania się uniwersalnego kwantowania na predykatach i funkcjach.

Korespondencja między klasami a logiką

Wiele innych klas również zostało scharakteryzowanych w ten sam sposób i zostały podsumowane w poniższej tabeli, głównie przez Neila Immermana .

Klasy złożoności	Odpowiednia logika
AC⁰	logika pierwszego rzędu
Holandia	logika pierwszego rzędu z domknięciem przechodnim
P	Logika pierwszego rzędu z najmniejszym punktem stałym
NP	egzystencjalna logika drugiego rzędu
współ-NP	uniwersalna logika drugiego rzędu
PH	logika drugiego rzędu
PSPACE	logika drugiego rzędu z domknięciem przechodnim
CZAS EKSPLOATACJI	Logika drugiego rzędu z najmniejszym punktem stałym
PODSTAWOWY	logika wyższego rzędu
RE	logika egzystencjalna pierwszego rzędu na liczbach całkowitych
rdzeń	uniwersalna logika pierwszego rzędu nad liczbami całkowitymi

Przykład dla NL

Zainteresowania

Neil Immerman uzasadnia teorię złożoności opisowej, ponieważ pokazuje, że klasy złożoności zdefiniowane za pomocą maszyn Turinga są naturalne : można je zdefiniować, nawet jeśli nie używamy klasycznych modeli obliczeniowych. Ponadto teoria ta daje nowy punkt widzenia na pewne wyniki i pewne hipotezy teorii złożoności, na przykład twierdzenie Abiteboula i Vianu (en) wskazuje, że klasy P i PSPACE są równe, jeśli logika Inflacyjny Punkt Ustalenia (IFP) i Częściowy Punkty stałe (PFP) są równe.

Link zewnętrzny

Strona Neila Immermana o złożoności opisowej, z diagramem .

Warianty

Klasa PTIME poprzecinana problemami niezmienniczymi przez bisymulację odpowiada logice wyższego wymiaru rachunku mu .

Bibliografia

Artykuły

(en) Ronald Fagin , „ Uogólnione widma pierwszego rzędu i zbiory rozpoznawalne w czasie wielomianowym ” , Proc. Sympoz. SIAM-AMS. Zał. Matematyka. , Amer. Matematyka. Soc., tom. VII „Złożoność obliczeń” ,1974, s. 43-73 ( Math Reviews 0371622 , przeczytane online , dostęp 7 listopada 2019 )
(en) Neil Immerman , “ Languages Which Capture Complexity Classes ” , STOC '83 Proceedings z piętnastego dorocznego sympozjum ACM on Theory of computing ,1983, s. 347-354 ( ISBN 0-89791-099-0 , DOI 10.1145 / 800061.808765 , czytaj online )
(i) Serge Abiteboul i Victor Vianu , „ Generic Obliczenia i jego złożoność ” , stoc '91 Materiały dwudziestym trzecim rocznej ACM Symposium na teorii Computing ,1991, s. 209-219 ( ISBN 0-89791-397-3 , DOI 10.1145 / 103418.103444 )

Pracuje

(en) Neil Immerman , Descriptive Complexity , New York, Springer-Verlag,1999( ISBN 0-387-98600-6 , prezentacja online )
(en) Martin Grohe , Descriptive Complexity, Canonization, and Definiable Graph Structure Theory , Cambridge University Press,2017, 554 s. ( ISBN 978-1-139-02886-8 , czytaj online ) , rozdz. I.3 („Złożoność opisowa”) , s. 40-93

Uwagi i referencje

( Fagin 1974 ).
Źródła znaczenie: Jesteśmy teraz gotowi do wskazania Fagin za twierdzenia i Immerman-Vardiego twierdzenia, prawdopodobnie dwóch najbardziej podstawowych wyników w opisowej teorii złożoności. w ( Grohe 2017 )
Patrz wstęp ( Immerman 1983 ).
( Abiteboul i Vianu 1991 ).
Martin Otto , „ Bisimulation-invariant PTIME i wyżejwymiarowy rachunek μ ”, „ Informatyka teoretyczna” , tom. 224 n o 1,6 sierpnia 1999 r., s. 237-265 ( ISSN 0304-3975 , DOI 10.1016 / S0304-3975 (98) 00314-4 , odczyt online , dostęp 22 listopada 2019 )