Gramatyka kontekstowa dla SAT?

Według klasycznego wyniku Kurody, klasa złożoności NSPACE [ ]$n$ (znana również jako NLIN-SPACE) jest właśnie klasą CSL języków kontekstowych . Problem satysfakcji SAT występuje w NSPACE [ ], ponieważ domysły o liniowym rozmiarze dla rozwiązania można sprawdzić z co najwyżej liniowym obciążeniem dla księgowości. Oznacza to, że SAT musi mieć gramatykę kontekstową (CSG).$n$

Czy ktoś próbował dostarczyć CSG dla SAT?

Zdaję sobie sprawę, że wiele pytań związanych z CSL jest nierozstrzygalnych (na przykład decydowanie, czy dany CSG generuje pusty język). Nawet biorąc pod uwagę CSG dla SAT, nadal trzeba by pokonać przeszkodę, że decydowanie o członkostwie w języku podanym przez CSG jest w zasadzie kompletne z PSPACE. Ale może się zdarzyć, że problem członkostwa w CSG, który definiuje SAT, występuje w NP, z powodu jakiejś specjalnej struktury języka. Przeredagowanie, aby odpowiedzieć na komentarz MCH: Ale może się zdarzyć, że problem członkostwa w CSG, który definiuje SAT, może być pokazany w NP ze względu na jakąś specjalną strukturę gramatyki, a nie dlatego, że już wiemy, że musi być NP.

• S.-Y. Kuroda, Klasy języków i automaty ograniczone liniowo , Informacja i kontrola 7 (2) 207–223, 1964. doi: 10.1016 / S0019-9958 (64) 90120-2

Wyjaśnienie:

Zamierzonym celem jest tutaj specjalna funkcja gramatyki dla SAT, która pozwala na rozpoznanie jej przez maszynę NTIME [poli ( )], a nie przez NSPACE [ ] DTIME [ ] uwiązany.$n$$n$$\subseteq$$2^{O(n)}$

Dowód twierdzenia 3 w pracy Landwebera z 1963 r. Konstruuje CSG z automatu ograniczonego liniowo. (Kuroda podał odwrotnie, konstruując automat związany z liniami dla dowolnego CSG.) Jednak procedura Landwebera nie wydaje się dostarczać gramatyki dla SAT, która ma specjalną formę: wszystkie urządzenia rozpoznające NSPACE [ ] są traktowane w ten sam ogólny sposób. Innymi słowy, nie jest jasne, dlaczego SAT CSG powinien mieć problem z członkostwem NP, a nie być ukończony PSPACE. Miałem nadzieję na bardziej jednoznaczną konstrukcję, która wykorzystywałaby NP-SAT w jakiś istotny sposób.$n$

Być może lepszym, bardziej precyzyjnym pytaniem jest, czy:

1. istnieje automat z ograniczeniem liniowym, który rozpoznaje SAT,
2. z którego można wydobyć CSG,
3. więc język zdefiniowany przez CSG jest w NP z powodu jakiejś cechy gramatyki (a nie dlatego, że już wiemy, że jest w NP)?

W ciągu pięciu dekad z pewnością ktoś próbował to zrobić! Ponieważ nie mogę znaleźć niczego opublikowanego w ten sposób, chciałbym zrozumieć, dlaczego to podejście nie zadziałało, lub wskaźnik do pracy, za którym tęskniłem.

• Peter S. Landweber, Trzy twierdzenia o gramatyce struktury fraz typu 1 , Informacja i kontrola 6 (2) 131–136, 1963. doi: 10.1016 / S0019-9958 (63) 90169-4

Choć nie konstruuje bezpośrednio gramatyki kontekstowej dla SAT, poniższy artykuł może rzucić nieco światła.

Rundy WC, złożoność rozpoznawania w językach pośrednich , teoria przełączania i automatu, 1973, 145-158 http://dx.doi.org/10.1109/SWAT.1973.5

Artykuł Roundsa podaje jednokierunkowy niedeterministyczny automat stosu (1-NSA) rozpoznający SAT, a następnie pokazuje problem członkostwa w 1-NSA (i jego odpowiednim nadzbirze, Indeksowana gramatyka Aho) jest ogólnie w NP. Innymi słowy, SAT jako automat CSL / liniowy jest wyjątkowy, ponieważ wykorzystuje swoją pamięć tylko jako stos.