Gibt es einen nicht deterministischen linearen Zeitalgorithmus für CNF-SAT?

Das Entscheidungsproblem CNF-SAT kann wie folgt beschrieben werden:

Eingabe: Eine Boolesche Formel $\phi$ in konjunktiver Normalform.

Frage: Gibt es eine Variablenzuordnung, die erfüllt $\phi$ ?

Ich überlege mir verschiedene Ansätze, um CNF-SAT mit einer nicht deterministischen Zwei-Band-Turing-Maschine zu lösen .

Ich glaube, dass es ein NTM gibt, das CNF-SAT in $n \cdot \texttt{poly}(\log(n))$ Schritten löst .

Frage: Gibt es ein NTM, das CNF-SAT in $O(n)$ Schritten löst ?

Alle relevanten Referenzen sind erwünscht, selbst wenn sie nur nicht deterministische Ansätze mit nahezu linearer Zeit liefern.

time-complexity sat turing-machines np nondeterminism Michael Wehar
quelle

Santhanam 2001 schrieb: „SAT

NTIME (

polylog

), ein Ergebnis , das aus den Tatsachen folgt , dass SAT in akzeptiert werden

polylog

Zeit auf einem NRAM und dass es eine effiziente Simulation von NRAMs von NTMs dank Gurevich und Shelah. " Daher erscheint es mir unwahrscheinlich, dass SAT

NTIME (

) bekannt ist. (Der Verweis bezieht sich auf LNCS 363 von 1989.)

\in

$\in$

n

$n$

(n)

$(n)$

n

$n$

(n)

$(n)$

\in

$\in$

n

$n$

András Salamon

@Boson, gehen Sie davon aus, dass Sie nicht nur eine zufriedenstellende Aufgabe erhalten, sondern auch eine vollständige Berechnung der Formel. Wie würden Sie überprüfen, ob es sich um eine gültige Berechnung in linearer Zeit handelt? Es ist nicht klar, ob Sie dies auch für 3CNF-SAT tun können, da Sie herumspringen müssen, um die Zuordnung zu den Variablen nachzuschlagen.

Kaveh

@Boson Es ist nicht klar, ob Sie mit einem Two-Tape TM überprüfen können, ob die Zuweisung die Formel in linearer Zeit erfüllt. Wahrscheinlich müssten Sie den Bandkopf viele Male hin und her bewegen. Wenn Sie einen effizienten Ansatz für diese Überprüfung haben, lassen Sie es mich bitte wissen. :)

Michael Wehar

Nur eine Anmerkung: Wenn Variablen in unary dargestellt werden (SAT ist immer noch NPC), gibt es ein NTM mit zwei Bändern, das eine unary erfüllbare Formel

erkennt

Schritte

φ

$\varphi$

2 | φ |

$2|\varphi|$

Marzio De Biasi

@MichaelWehar Wenn Sie eine Zählsortierung verwenden, können Sie n Schlüssel im Bereich [0, k] in der Zeit O (n + k) in einem vernünftigen Zufallszugriffsmodell sortieren (z. B. Zufallszugriffsmaschine, in die Sie O (log n) Zeit, einen Index aufzuschreiben, dann kann in 1 Schritt zu diesem Index des Bandes gesprungen werden. Wenn Sie jedes Literal als Bitfolge (log n + 1) codieren, beträgt die Gesamtzahl der Klauseln und Variablen höchstens O (n / log n), in diesem Fall O (log n) -Zeitoperationen für alle Literale sind gut. Die Erweiterung auf zwei TM-Bänder ist nicht einfach, zumindest beim Zählen der Sortierung.

Ryan Williams

Antworten:

Dies ist nur ein erweiterter Kommentar. Vor einiger Zeit habe ich mich gefragt, wie schnell ein Multitape-NTM sein kann, das eine (vernünftig codierte) NP-vollständige Sprache akzeptiert. Ich bin auf diese Idee gekommen:

3-SAT bleibt NP-vollständig, auch wenn Variablen unär dargestellt werden. Insbesondere können wir eine Klausel - angenommen - einer beliebigen 3-SAT-Formel auf Variablen und Klauseln in einer Folge von Zeichen über dem Alphabet konvertieren in der jede Variable unär dargestellt wird: $(x_i \lor \neg x_j \lor x_k)$ $\varphi$ $n$ $m$ $\Sigma = \{ +, -, 1 \}$

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

Zum Beispiel konvertiert werden in: $(x_2 \lor -x3 \lor +4)$

+110-1110+11110

Wir können also eine 3-SAT-Formel in eine äquivalente Zeichenfolge umwandeln, die ihre Klauseln verkettet. Die Sprache $\varphi_i$ $U(\varphi_i)$ NP-vollständig. $L_U = \{ U(\varphi_i) \mid \varphi_i \in 3-SAT \}$

Ein 2-Band-NTM kann entscheiden, ob ein String ist $x \in L_U$ auf diese Weise. $2|x|$

Der erste Kopf tastet die Eingabe von links nach rechts ab und verfolgt sie mit der internen Logik, wenn er eine Klausel betritt oder verlässt oder das Ende der Formel erreicht. Immer wenn es ein oder , bewegt sich der zweite Kopf auf der , die nach rechts . Am Ende von , wenn der zweite Kopf auf einer dann schätzt er einen Wahrheitswert oder $+$ $-$ $1^i$ $x_i$ $1^i$ $0$ $+$ $-$ (er nimmt eine Zuordnung vor) und schreibt ihn auf das zweite Band; Wenn es ein oder dieser Variablen bereits ein Wert zugewiesen. $+$ $-$
In beiden Fällen vergleicht das NTM unter Verwendung der internen Logik den Wahrheitswert unter dem zweiten Kopf (die Zuordnung) mit dem zuletzt gesehenen oder ; wenn sie übereinstimmen, ist die Klausel erfüllt; $+$ $-$
dann kann der zweite Kopf in die Zelle ganz rechts zurückkehren;
Mit der internen Logik kann der NTM verfolgen, ob alle Klauseln erfüllt sind, während sich der erste Kopf zum Ende der Eingabe bewegt.

Beispiel:

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)

Die Zeit kann auf reduziert werden wenn wir der Klauseldarstellung einige redundante Symbole hinzufügen: $|x|$

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

( markiert das Ende der Formel) $\text{+++}$

Auf diese Weise kann der zweite Kopf zur Zelle ganz links zurückkehren, während der erste die abtastet $0^i$ Teil . Mit als Klauselbegrenzer und als Markierung für das Ende der Formel können wir dieselbe Darstellung für CNF-Formeln mit einer beliebigen Anzahl von Litern pro Klausel verwenden. $\text{++}$ $\text{+++}$

Marzio De Biasi
quelle

Die unäre Darstellung ist eindeutig, daher kann 0/1 für +/- verwendet werden, was 011011110111110 für Ihr erstes Beispiel ergibt. 00 dient dann als Endemarker, da 000 sonst nicht vorkommen kann (wenn 00 vorkommt, ist es der Endemarker einer Variablen und das nächste Zeichen, das nächste Symbol muss also 1 sein). Das einzelne Arbeitsband enthält die erratene

Bit-Zuordnung zu den

Variablen. Wenn eine Variable gelesen wird, bewegt sich der Arbeitsbandkopf vorwärts und wird dann an den Anfang zurückbewegt, wenn die 0 zu sehen ist, also höchstens

Schritte für jedes Bit der Eingabe.

v

$v$

v

$v$

2

$2$

András Salamon

Mit anderen Worten, selbst ein NDTM mit einem Einweg- Eingabeband und einem einzelnen Arbeitsband verwendet für Unary SAT, das mit einem Booleschen Alphabet codiert ist, höchstens

Schritte.

2 n

$2n$

András Salamon

Um die Dinge noch aufgeräumter zu machen, kann man ferner verlangen , dass der Eingang zunächst einen Präfix mit der Anzahl der Variablen enthält

in einstelligen angegeben. Dadurch kann die Vermutung beim Lesen des Präfixes erstellt werden. Dies ist dann eine Art "unäre SATLIB" -Codierung, deren Größe in einer Standard-SAT-Instanz höchstens quadratisch ist, solange jede Variable in der Formel mindestens einmal vorkommt und die Variablen mit 0 bis

nummeriert sind . Dies scheinen vernünftige Anforderungen zu sein.

v

$v$

v - 1

$v-1$

András Salamon

@ AndrásSalamon: gut! Wenn wir die Codierung und das Modell (Einweg-Leseband + Zweiweg-Arbeitsband) korrigieren, erhalten wir eine schlechteste Laufzeit von

für Eingaben der Größe

, wobei

beliebig groß gemacht werden kann , wobei ein Teil des festen Speichers in die interne TM-Logik eingebettet wird . Es könnte interessant sein, zu untersuchen, ob mit der Einbahnigkeit des Eingabebands und einem Querschnittargument etwas bewiesen werden kann.

2 n - c

$2n - c$

n

$n$

c

$c$

Marzio De Biasi

Ja, soweit ich das Time-Space-Produkt für Unary SAT beurteilen kann, ist es so etwas wie

durch ein Standardargument. Die unäre Darstellung von Variablen vermeidet die Lücke zwischen der bekanntestenUntergrenze von

und einer einfachenObergrenze von

für CNF-SAT (obwohl Ein besserer Algorithmus könnte dann auch die Lücke verkleinern.

Θ (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

Nicht genau das, wonach Sie suchen, aber für 1-Band-NTM scheint die Antwort negativ zu sein: SAT ist durch 1-Band-NTM in nicht deterministischer linearer Zeit nicht lösbar.

Nach diesem Papier (Satz 4.1), die Klasse der regulären Sprachen ist genau die Klasse der durch ein 1-Band NTM rechtzeitig erkannt Sprachen . Wenn es also ein 1-Band-NTM gäbe, das SAT in der Zeit löst , dann wäre SAT (genauer gesagt die Menge der erfüllbaren Formeln in CNF) eine reguläre Sprache und daher im deterministischen konstanten Raum lösbar. $REG$ $o(n \log(n))$ $o(n \log(n))$

Boson
quelle

In diesem Satz geht es nur um Einkopf- Turingmaschinen.

$\:$ (Zum Beispiel können Zweikopf-Turingmaschinen die Palindrom-Sprache leicht in linearer Zeit und konstantem Raum bestimmen .)

$\;\;\;\;$

Das ist toll! Vielen Dank. Am meisten interessiert mich aber der Fall mit zwei Bändern. :)

Michael Wehar

Wie @Ricky schrieb. AFAIK, es stimmt immer noch mit dem überein, was wir wissen, dass SAT in einer deterministischen linearen Zeit vorliegt. Um zu beweisen, dass Sie eine superlineare Zeituntergrenze für SAT benötigen und wir keine haben (scheinen nicht nahe bei einer zu sein).

Kaveh