Czy SAT w ograniczonej szerokości jest rozstrzygalny w przestrzeni logów?

Elberfeld, Jakoby i Tantau 2010 ( ECCC TR10-062 ) dowiodły, że zajmująca mało miejsca wersja twierdzenia Bodlaendera. Wykazali, że w przypadku wykresów o szerokości co najwyżej rozkład drzewa o szerokości k można znaleźć za pomocą przestrzeni logarytmicznej. Stały współczynnik w ograniczonej przestrzeni zależy od k . (Twierdzenie Bodlaendera pokazuje liniowe ograniczenie czasowe z wykładniczą zależnością od k w współczynniku stałym).$k$$k$$k$$k$

SAT staje się łatwy, gdy zestaw klauzul ma małą szerokość. W szczególności Fischer, Makowsky i Ravve 2008 wykazali, że o zadowalalności wzorów CNF z szerokością wykresu występowania ograniczonego przez można decydować co najwyżej 2 O ( k ) n operacji arytmetycznych, gdy podany jest rozkład drzewa. Zgodnie z twierdzeniem Bodlaendera obliczenie rozkładu drzewa wykresu padania dla ustalonego k może być wykonane w czasie liniowym, a zatem SAT można ustalić dla ograniczonych wzorów szerokości w czasie, który jest wielomianem niskiego stopnia w liczbie zmiennych n .$k$$2^{O(k)} n$$k$$n$

Można zatem oczekiwać, że SAT powinien być rzeczywiście rozstrzygalny przy użyciu przestrzeni logarytmicznej, dla formuł o ograniczonej szerokości wykresu częstości. Nie jest jasne, jak zmodyfikować Fischera i in. podejście do decydowania o SAT w czymś zajmującym mało miejsca. Algorytm działa poprzez obliczenie wyrażenia liczby rozwiązań, poprzez włączenie-wykluczenie i rekurencyjną ocenę liczby rozwiązań o mniejszych formułach. Chociaż ograniczona szerokość grzbietu pomaga, podformuły wydają się zbyt duże, aby obliczyć je w przestrzeni logarytmicznej.

To prowadzi mnie do pytania:

Czy wiadomo, że SAT dla formuł o ograniczonej krzyżówce występuje w lub N L ?$\mathsf{L}$$\mathsf{NL}$

Rzeczywiście, korzystając z wyników w Elberfeld-Jakoby-Tantau-2010, można wykazać, że o SAT można decydować w przestrzeni logicznej na formułach, których wykres występowania ograniczył szerokość. Oto szkic głównych kroków dowodu tego roszczenia.

1. Pojęcia rozkładu drzewa i szerokości drzewa można uogólnić na dowolne struktury relacyjne. Patrz na przykład sekcje 2 i 3 tego artykułu autorstwa Dalmau, Kolaitis i Vardi.
2. Twierdzenie Courcelle'a stwierdza, że ​​logika MSO może być ustalona w czasie liniowym na relacyjnych strukturach o stałej szerokości.
3. $t$$f(t)\cdot n$
4. $\tau$$F$$I$$\tau$$I$
5. $\tau$
6. Dlatego, według twierdzenia Bodlandera + Courcelle'a, można zdecydować, czy formuła stałej szerokości poprzecznej jest zadowalająca w czasie liniowym.
7. Elberfeld-Jakoby-Tantau-2010 pokazuje, że „czas liniowy” można zastąpić „przestrzenią logarytmiczną” zarówno w twierdzeniu Bodlaendera, jak i Courcelle'a.
8. $\varphi$$\tau$$\tau$$\varphi$
9. W szczególności SAT można określić w przestrzeni logów na wykresach stałej szerokości.