Czy istnieje niedeterministyczny algorytm liniowego czasu dla CNF-SAT?

Problem decyzyjny CNF-SAT można opisać następująco:

Dane wejściowe: wzór logiczny $\phi$ w spójnej postaci normalnej.

Pytanie: Czy istnieje przypisanie zmiennej spełniające $\phi$ ?

Rozważam kilka różnych podejść do rozwiązania CNF-SAT za pomocą niedeterministycznej maszyny Turinga z dwiema taśmami .

Uważam, że istnieje NTM, który rozwiązuje CNF-SAT etapami $n \cdot \texttt{poly}(\log(n))$ .

Pytanie: Czy istnieje NTM, który rozwiązuje CNF-SAT w krokach $O(n)$ ?

Wszelkie odnośne referencje są doceniane, nawet jeśli zapewniają jedynie niedeterministyczne podejścia zbliżone do liniowego.

time-complexity sat turing-machines np nondeterminism Michael Wehar
źródło

Santhanam w 2001 roku napisał: „SAT

NTIME (

polylog

), wynik wynikający z faktów, że SAT może być zaakceptowany w czasie

polylog

na NRAM i że istnieje skuteczna symulacja NRAM przez NTM , z powodu Gurewicza i Szelacha ”. Więc nie wydaje mi się, że SAT

NTIME (

) jest znana. (Odniesienie dotyczy LNCS 363 z 1989 r.)

\in

$\in$

n

$n$

(n)

$(n)$

n

$n$

(n)

$(n)$

\in

$\in$

n

$n$

András Salamon

@Boson, załóż, że otrzymujesz nie tylko zadowalające zadanie, ale także pełne obliczenie formuły. Jak sprawdziłbyś, czy jest to prawidłowe obliczenie w czasie liniowym? Nie jest jasne, nawet możesz to zrobić dla 3CNF-SAT, ponieważ musisz skakać, aby sprawdzić przypisanie do zmiennych.

Kaveh

@Boson Nie jest jasne, czy można sprawdzić, czy przypisanie spełnia formułę w czasie liniowym za pomocą TM z dwiema taśmami. Prawdopodobnie będziesz musiał wielokrotnie przesuwać głowę do przodu i do tyłu. Jeśli masz skuteczne podejście do tej weryfikacji, daj mi znać. :)

Michael Wehar

Tylko uwaga: jeśli zmienne są reprezentowane jako jednoargumentowe (SAT wciąż jest NPC), to istnieje dwuwarstwowy NTM, który rozpoznaje niezrównanie zadowalającą formułę

φ

$\varphi$

kroki

2 | φ |

$2|\varphi|$

Marzio De Biasi

@MichaelWehar jeśli używasz sortowania zliczającego, możesz posortować n kluczy z zakresu [0, k] w czasie O (n + k) w rozsądnym modelu o swobodnym dostępie (np. Maszyna Turinga o dostępie swobodnym, gdzie możesz wziąć O (log) n) czas na spisanie indeksu, a następnie przejście do tego indeksu taśmy w 1 kroku). Jeśli kodujesz każdy literał jako ciąg bitów (log n + 1), całkowita liczba klauzul i zmiennych wynosi co najwyżej O (n / log n), w którym to przypadku operacje czasu O (log n) na wszystkich literałach są w porządku. Rozszerzenie na dwie taśmy TM nie jest proste, przynajmniej z sortowaniem zliczającym.

Ryan Williams

Odpowiedzi:

To tylko rozszerzony komentarz. Kilka razy temu zapytałem (siebie :-), jak szybko może być wielopasmowy NTM, który akceptuje (rozsądnie zakodowany) język NP-zupełny. Wpadłem na ten pomysł:

3-SAT pozostaje NP-kompletny, nawet jeśli zmienne są reprezentowane w jedności. W szczególności możemy przekonwertować klauzulę - załóżmy - o dowolnej formule 3-SAT na zmiennych i klauzulach sekwencji znaków nad alfabetem w którym każde wystąpienie zmiennej jest reprezentowane jako jednoargumentowe: $(x_i \lor \neg x_j \lor x_k)$ $\varphi$ $n$ $m$ $\Sigma = \{ +, -, 1 \}$

$+ 1^{i} 0,- 1^{j} ,+ 1^{k}$

Na przykład można przekonwertować na: $(x_2 \lor -x3 \lor +4)$

+110-1110+11110

Możemy więc przekonwertować wzór 3-SAT na równoważny ciąg łączący jego zdania. Język $\varphi_i$ $U(\varphi_i)$ jest NP-kompletny. $L_U = \{ U(\varphi_i) \mid \varphi_i \in 3-SAT \}$

NTM z 2 taśmami może zdecydować, czy ciąg w czasie w ten sposób. $x \in L_U$ $2|x|$

pierwsza głowa skanuje dane wejściowe od lewej do prawej iz wewnętrzną logiką śledzi, kiedy wchodzi lub wychodzi z klauzuli lub osiąga koniec formuły. Ilekroć znajdzie znak lub , druga głowa zaczyna się przesuwać w prawo na który reprezentuje . Na końcu , jeśli druga głowa ma wartość wówczas zgaduje wartość prawdy lub (wykonuje przypisanie) i zapisuje ją na drugiej taśmie; jeśli znajdzie znak lub wówczas tej zmiennej przypisano już wartość; $+$ $-$ $1^i$ $x_i$ $1^i$ $0$ $+$ $-$ $+$ $-$
w obu przypadkach, używając wewnętrznej logiki, NTM dopasowuje wartość prawdy pod drugą głową (przypisanie) do ostatnio widzianego lub ; jeśli się zgadzają, klauzula jest spełniona; $+$ $-$
wtedy druga głowa może powrócić do skrajnie prawej komórki;
z wewnętrzną logiką NTM może śledzić, czy wszystkie klauzule są spełnione, gdy pierwsza głowa przesuwa się w kierunku końca wejścia.

Przykład:

Tape 1 (formula)    Tape 2 (variable assignments)
+110-1110+11110...  0000000000000...
^                   ^
+110-1110+11110...  0000000000000...
 ^                  ^
+110-1110+11110...  0000000000000...
  ^                  ^
+110-1110+11110...  0+00000000000... first guess set x2=T; matches +
  ^                  ^               so remember that current clause is satisfied
+110-1110+11110...  0+00000000000... 
  ^                  ^
...
+110-1110+11110...  0+00000000000... 
    ^               ^
...
+110-1110+11110...  0++0000000000... second guess set x3=T
       ^              ^              don't reject because current
                                     clause is satisfied (and in every
                                     case another literal must be parsed)

Czas można skrócić do jeśli dodamy kilka zbędnych symboli do reprezentacji klauzuli: $|x|$

$+ 1^{i} 0^i,- 1^{j} 0^j ,+ 1^{k} 0^k \; ... \; \text{+++}$

( oznacza koniec formuły) $\text{+++}$

W ten sposób druga głowa może powrócić do lewej komórki, podczas gdy pierwsza skanuje część . Używanie jako separatora klauzul i $0^i$ $\text{++}$ $\text{+++}$ jako znacznika końca formuły, możemy użyć tej samej reprezentacji dla formuł CNF z dowolną liczbą literałów na klauzulę.

Marzio De Biasi
źródło

Jednoznaczna reprezentacja jest jednoznaczna, więc można użyć 0/1 dla +/-, podając 011011110111110 jako pierwszy przykład. 00 następnie służy jako znacznik końca klauzuli, ponieważ 000 nie może wystąpić w przeciwnym razie (jeśli 00 występuje, to jest to znacznik końcowy zmiennej i następny znak, więc następnym symbolem musi być 1). Pojedyncza taśma robocza zawiera odgadnięte przyporządkowanie

bitowe do zmiennych

. Kiedy zmienna jest czytana, głowa taśmy roboczej przesuwa się do przodu, a następnie jest cofana do początku, gdy widoczne jest 0, czyli co najwyżej

kroki dla każdego bitu wejścia.

v

$v$

v

$v$

2

$2$

András Salamon,

Innymi słowy, nawet NDTM z jednokierunkową taśmą wejściową i pojedynczą taśmą roboczą wykorzystuje co najwyżej

kroków dla Unary SAT zakodowanego alfabetem boolowskim.

2 n

$2n$

András Salamon,

Aby uczynić rzeczy jeszcze bardziej uporządkowanymi, można dodatkowo wymagać, aby dane wejściowe zawierały najpierw przedrostek z liczbą zmiennych

określonych w unary. Pozwala to na budowanie domysłów podczas czytania prefiksu. Jest to zatem rodzaj „jednoargumentowego kodowania SATLIB”, o wielkości co najwyżej kwadratowej w standardowej instancji SAT, o ile każda zmienna pojawia się co najmniej raz w formule, a zmienne są ponumerowane od 0 do

. Są to rozsądne wymagania.

v

$v$

v - 1

$v-1$

András Salamon,

@ AndrásSalamon: dobrze! Naprawiając kodowanie i model (taśma odczytu jednokierunkowego + taśma robocza dwukierunkowa) otrzymujemy najgorszy czas działania

na wejściach o rozmiarze

, gdzie

może być dowolnie duże, osadzając pewną stałą pamięć w wewnętrznej logice TM . Interesujące może być zbadanie, czy coś można udowodnić za pomocą jednostronności taśmy wejściowej i argumentu przekroju.

2 n - c

$2n - c$

n

$n$

c

$c$

Marzio De Biasi,

Tak, o ile mogę powiedzieć, iloczyn czasoprzestrzenny dla Unary SAT to coś w rodzaju

standardowym argumentem. Jednoargumentowa reprezentacja zmiennych pozwala uniknąć przerwy między najlepiej znanądolną granicą

a bezpośredniągórną granicą

dla CNF-SAT (chociaż lepszy algorytm w takim przypadku może również zmniejszyć różnicę).

Θ (n \sqrt{n})

$\Theta(n\sqrt{n})$

Ω (n^{2} / (\log n)^{1 + ε})

$\Omega(n^2/(\log n)^{1+\varepsilon})$

O (n^{3} / (\log n)^{ε^{'}})

$O(n^3/(\log n)^{\varepsilon'})$

András Salamon,

Nie do końca to, czego szukasz, ale w przypadku NTM z 1 taśmą odpowiedź wydaje się być przecząca: SAT nie jest rozwiązywalny z NTM z 1 taśmą w niedeterministycznym czasie liniowym.

Zgodnie z tym artykułem (Twierdzenie 4.1), klasa języków regularnych jest dokładnie klasą języków rozpoznawanych przez 1-taśmowy NTM w czasie . Zatem jeśli istniałby 1-taśmowy NTM rozwiązujący SAT w czasie , to SAT (a dokładniej zbiór zadowalających wzorów w CNF) byłby językiem regularnym, a zatem rozwiązalnym w deterministycznej stałej przestrzeni. $REG$ $o(n \log(n))$ $o(n \log(n))$

Boson
źródło

Twierdzenie, że jest tylko o jednym głowy maszyn Turinga.

$\:$ (Na przykład dwugłowicowe maszyny Turinga mogą łatwo decydować o języku palindromu w czasie liniowym i stałej przestrzeni).

$\;\;\;\;$

To jest świetne! Dziękuję Ci bardzo. Ale najbardziej interesuje mnie sprawa dwóch taśm. :)

Michael Wehar

Jak napisał @Ricky. AFAIK nadal jest zgodny z tym, co wiemy, że SAT jest w deterministycznym czasie liniowym. Aby udowodnić inaczej, potrzebna byłaby dolna granica czasu superlinearnego dla SAT, a my jej nie mamy (wydaje się, że nie jest blisko jednego).

Kaveh