ETH: k-SAT vs. SAT?

8

Sei SAT die Sprache jener Instanzen von SAT, die Variablen , sei -SAT die Sprache jener Instanzen von SAT, in denen jede Klausel enthalten ist höchstens Literale, und sei -SAT ihr Schnittpunkt. Sei , wobei das Infimum über alle Algorithmen (Maschinen in einem Rechenmodell) reicht. Sei s_ \ infty = \ lim_ {k \ to \ infty} s_kv[v]={0,1,,v1}kkkvsk=infM{δcv(M decides k-SATv in 2vδc) time)}s=limksk. Damit dies sinnvoll ist, muss davon ausgegangen werden, dass die Größe der Eingabe in Bezug auf die Anzahl der Variablen angemessen begrenzt ist. Andernfalls könnte man Klauseln wiederholen, um zu erzwingen, dass sk und s so groß wie gewünscht sind. Nehmen wir also an, dass Klauseln nicht wiederholt werden.

Beachten Sie, dass jede k CNF-Formel dann höchstens O(vk) , sodass die Größe der Eingabeformel nicht wichtig ist, wenn ein Exponent betrachtet wird, der in v linear ist v. Daraus folgt, dass s3s4s .

Die Exponential Time Hypothesis (ETH) ist die Aussage, dass sk>0 für einige k3 . Die Sequenz (sk) steigt unendlich oft an, wenn die ETH gilt. Die Starke ETH (SETH) ist die Aussage, dass s1 oder s=1 , je nachdem, welche Referenz verwendet wird.

Im Gegensatz dazu enthält jede Instanz von SAT v bis zu 3v unterschiedliche Klauseln (jede Variable kann in jeder Klausel positiv, negativ oder nicht vorhanden sein). Daher kann eine Eingabe die Länge Ω(2nlog3) selbst wenn keine Klausel wiederholt wird. Dies ist also eine Untergrenze für die Zeit zum Lesen der Eingabe und dann auch für die Gesamtzeit.

Wenn wir dann , es ist klar, dass nur unter Berücksichtigung der Eingabegrößen. Selbst wenn eine Eingabeformel keine Klausel enthalten muss, die von einer anderen subsumiert wird, . Nach dem trivialen Algorithmus ist es auch so, dass .sω=infM{δcv(M decides SATv in 2vδc) time)}sωlog3>1.58sω1.5sω1+log3

Warum gibt es eine Lücke zwischen und , wenn SETH angenommen wird?ssω

In gewissem Sinne ist nur ein anderer Weg, um das Limit zu erreichen, daher scheint es rätselhaft, dass es eine Lücke geben sollte.sω

  • Russell Impagliazzo und Ramamohan Paturi, Zur Komplexität von Satk , JCSS 62 367–375, 2001. doi: 10.1006 / jcss.2000.1727 ( Preprint )
  • Evgeny Dantsin und Alexander Wolpert, über mäßig exponentielle Zeit für SAT , SAT 2010, LNCS 6175 313–325. doi: 10.1007 / 978-3-642-14186-7_27 ( Preprint )
  • Chris Calabro, Russell Impagliazzo und Ramamohan Paturi, Die Komplexität der Erfüllbarkeit kleiner Schaltungen , IWPEC 2009, LNCS 5917 75–85. doi: 10.1007 / 978-3-642-11269-0_6 ( Preprint )
  • Marek Cygan, Holger Dell, Daniel Lokshtanov, Dániel Marx, Jesper Nederlof, Yoshio Okamoto, Ramamohan Paturi, Saket Saurabh, Magnus Wahlström, auf Probleme so hart , wie CNF-SAT , arXiv: 1112.2275v3 , 27. März 2014.
András Salamon
quelle

Antworten:

6

Der Unterschied zwischen Ihren Definitionen besteht darin, dass die Klauselbreite in mit der Anzahl der Variablen wachsen darf, während sie für beliebig groß, aber konstant ist.sωs

Es ist ein ähnliches Problem wie PH vs PSPACE. Wenn Sie eine beliebige konstante Anzahl von Quantifiziereränderungen vornehmen, erhalten Sie die Polynomhierarchie. Wenn Sie jedoch zulassen, dass die Formel vollständig quantifiziert wird, erhalten Sie ein PSPACE-vollständiges Problem.

Stefan Schneider
quelle
4

Eine bessere Möglichkeit, diese Exponenten zu definieren, besteht darin, nach der Laufzeit in der Form fragen , wobei ein beliebiges Polynom der Eingabegröße ist. Dann verschwinden Artefakte wie die Größe .cnpoly(|F|)poly(|F|)3v

Hirsch
quelle
Das scheint ein vernünftiger Ansatz zu sein, der durch parametrisierte Komplexität motiviert ist. Die Arbeiten zur ETH scheinen sie jedoch entweder ziemlich vage zu lassen oder verwenden eine Definition, die im Wesentlichen die oben angegebene ist. Hast du einen Zeiger?
András Salamon
Wenn wir über k-SAT sprechen, spielt es keine Rolle, da die Formelgröße in der Anzahl der Variablen polynomisch ist. Schauen Sie sich zum Beispiel Zeiger an, wie Impagliazzo, Paturi und Zane die Klasse SE in "Welche Probleme haben stark exponentielle Komplexität?", Journal of Computer and System Sciences 63, 512–530 (2001) definieren.
Hirsch
Danke, das ist nützlich. Ich habe mich bisher nur wirklich auf das Sparsification Lemma aus diesem Artikel konzentriert.
András Salamon