¿Existe un algoritmo de tiempo lineal no determinista para CNF-SAT?

El problema de decisión CNF-SAT se puede describir de la siguiente manera:

Entrada: Una fórmula booleana en forma conjuntiva normal. $\phi$

Pregunta: ¿Existe una asignación variable que satisfaga ? $\phi$

Estoy considerando varios enfoques diferentes para resolver CNF-SAT con una máquina de Turing de dos cintas no determinista .

Creo que hay una NTM que resuelve CNF-SAT en . $n \cdot \texttt{poly}(\log(n))$

Pregunta: ¿Hay una NTM que resuelva CNF-SAT en pasos ? $O(n)$

Se aprecia cualquier referencia relevante incluso si solo proporcionan enfoques no deterministas de tiempo casi lineal.

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

Santhanam en 2001 escribió: "SAT NTIME ( polylog ), un resultado que se deduce de los hechos de que SAT puede ser aceptado en polylog en un NRAM y que existe una simulación eficiente de NRAM por NTM, debido a Gurevich y Shelah ". Por lo tanto, me parece poco probable que se conozca SAT NTIME ( ). (La referencia es a LNCS 363 de 1989.)

\in

$\in$

n

$n$

(n)

$(n)$

n

$n$

(n)

$(n)$

\in

$\in$

n

$n$

András Salamon

@Boson, suponga que se le da no solo una tarea satisfactoria sino también un cálculo completo de la fórmula. ¿Cómo verificaría si es un cálculo válido en tiempo lineal? No está claro, incluso si puede hacerlo para 3CNF-SAT porque tiene que saltar para buscar la asignación a las variables.

Kaveh

@Boson No está claro si puede verificar que la asignación satisface la fórmula en tiempo lineal con una TM de dos cintas. Es probable que tenga que mover la cabeza de la cinta hacia adelante y hacia atrás muchas veces. Si tiene un enfoque eficiente para esta verificación, hágamelo saber. :)

Michael Wehar

Solo una nota: si las variables se representan en unario (SAT sigue siendo NPC), entonces hay una NTM de dos cintas que reconoce una fórmula satisfactoria unaria

pasos

φ

$\varphi$

2 | φ |

$2|\varphi|$

Marzio De Biasi

@MichaelWehar si usa una ordenación de conteo, puede ordenar n claves en el rango [0, k] en el tiempo O (n + k) en un modelo de acceso aleatorio razonable (por ejemplo, máquina de Turing de acceso aleatorio, donde puede tomar O (log n) tiempo para escribir un índice, luego puede saltar a ese índice de la cinta en 1 paso). Si codifica cada literal como una cadena de bits (log n + 1), el número total de cláusulas y variables es como máximo O (n / log n), en cuyo caso las operaciones de tiempo O (log n) en todos los literales estan bien. Extender hasta dos cintas TM no es sencillo, al menos con el recuento.

Ryan Williams

Respuestas:

Este es solo un comentario extendido. Hace algunas veces pregunté (a mí mismo :-) qué tan rápido puede ser un NTM multitapa que acepta un lenguaje NP (razonablemente codificado). Se me ocurrió esta idea:

3-SAT permanece NP-completo incluso si las variables se representan en unario. En particular, podemos convertir una cláusula, supongamos , de una fórmula arbitraria 3-SAT en variables y cláusulas en una secuencia de caracteres sobre el alfabeto en el que cada aparición de variable se representa en unario: $(x_i \lor \neg x_j \lor x_k)$ $\varphi$ $n$ $m$ $\Sigma = \{ +, -, 1 \}$

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

Por ejemplo, se puede convertir a: $(x_2 \lor -x3 \lor +4)$

+110-1110+11110

Entonces podemos convertir una fórmula 3-SAT en una cadena equivalente concatenando sus cláusulas. El lenguaje es NP-completo. $\varphi_i$ $U(\varphi_i)$ $L_U = \{ U(\varphi_i) \mid \varphi_i \in 3-SAT \}$

Una NTM de 2 cintas puede decidir si una cadena en el tiempo De este modo. $x \in L_U$ $2|x|$

la primera cabeza escanea la entrada de izquierda a derecha y con la lógica interna realiza un seguimiento cuando ingresa o sale de una cláusula o llega al final de la fórmula. Cada vez que encuentra un o , la segunda cabeza comienza a moverse hacia la derecha con ella en el que representa . Al final de , si el segundo encabezado está en , adivina un valor de verdad o (realiza una asignación) y lo escribe en la segunda cinta; si encuentra un o entonces a esa variable ya se le ha asignado un valor; $+$ $-$ $1^i$ $x_i$ $1^i$ $0$ $+$ $-$ $+$ $-$
en ambos casos, usando la lógica interna, el NTM hace coincidir el valor de verdad debajo del segundo encabezado (la asignación) con el último visto o ; si coinciden, entonces se cumple la cláusula; $+$ $-$
entonces la segunda cabeza puede regresar a la celda más a la derecha;
Con la lógica interna, el NTM puede realizar un seguimiento si se cumplen todas las cláusulas mientras el primer cabezal se mueve hacia el final de la entrada.

Ejemplo:

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)

El tiempo puede reducirse a si agregamos algunos símbolos redundantes a la representación de la cláusula: $|x|$

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

( marca el final de la fórmula) $\text{+++}$

De esta manera, la segunda cabeza puede volver a la celda más a la izquierda, mientras que la primera escanea la parte . Usando como delimitador de cláusula y como marcador para el final de la fórmula, podemos usar la misma representación para fórmulas CNF con un número arbitrario de literales por cláusula. $0^i$ $\text{++}$ $\text{+++}$

Marzio De Biasi
fuente

La representación unaria es inequívoca, por lo que se puede usar 0/1 para +/-, dando 011011110111110 para su primer ejemplo. 00 entonces sirve como marcador de fin de cláusula, ya que 000 no puede ocurrir de otra manera (si ocurre 00, entonces es el marcador final de una variable y el siguiente signo, por lo que el siguiente símbolo debe ser 1). La única cinta de trabajo contiene la asignación adivinada de

bit a las variables

. Cuando se lee una variable, la cabeza de la cinta de trabajo se mueve hacia adelante y luego se mueve hacia el principio cuando se ve el 0, por lo tanto, como máximo

pasos para cada bit de la entrada.

v

$v$

v

$v$

2

$2$

András Salamon

En otras palabras, incluso un NDTM con una cinta de entrada unidireccional y una sola cinta de trabajo utiliza como máximo

pasos para SAT Unario codificado con un alfabeto booleano.

2 n

$2n$

András Salamon

Para hacer las cosas aún más ordenadas, se puede requerir que la entrada primero contenga un prefijo con el número de variables

especificado en unario. Esto permite construir la suposición mientras se lee el prefijo. Este es un tipo de codificación "SATLIB unaria", de tamaño como máximo cuadrático en una instancia SAT estándar, siempre que cada variable aparezca al menos una vez en la fórmula y las variables estén numeradas de 0 a

. Estos parecen ser requisitos razonables.

v

$v$

v - 1

$v-1$

András Salamon

@ AndrásSalamon: ¡bien! Al arreglar la codificación y el modelo (cinta de lectura unidireccional + cinta de trabajo bidireccional) obtenemos el peor tiempo de ejecución de

en entradas de tamaño

, donde

puede hacerse arbitrariamente grande incrustando algo de almacenamiento fijo en la lógica interna de TM . Podría ser interesante investigar si algo puede probarse utilizando la unidireccionalidad de la cinta de entrada y un argumento de sección transversal.

2 n - c

$2n - c$

n

$n$

c

$c$

Marzio De Biasi

Sí, por lo que puedo decir, el producto espacio-temporal para Unary SAT es algo así como

por un argumento estándar. La representación unaria de variables evita la brecha entre ellímite inferior

más conocidoy unlímite superiordirecto de

para CNF-SAT (aunque un algoritmo mejor en ese caso también podría reducir la brecha).

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

No es exactamente lo que está buscando, pero para la NTM de 1 cinta, la respuesta parece ser negativa: SAT no se puede resolver con una NTM de 1 cinta en un tiempo lineal no determinista.

Según este documento (Teorema 4.1), la clase de idiomas regulares es exactamente la clase de idiomas reconocidos por una NTM de 1 cinta en el tiempo . Por lo tanto, si existiera un SAT de resolución de NTM de 1 cinta en el tiempo , entonces SAT (más precisamente, el conjunto de fórmulas satisfactorias en CNF) sería un lenguaje regular, por lo tanto solucionable en un espacio constante determinista. $REG$ $o(n \log(n))$ $o(n \log(n))$

Boson
fuente

Ese teorema es solo sobre máquinas Turing de una cabeza .

$\:$ (Por ejemplo, las máquinas Turing de dos cabezales pueden decidir fácilmente el lenguaje palíndromo en tiempo lineal y espacio constante).

$\;\;\;\;$

¡Esto es genial! Muchas gracias. Pero, estoy más interesado en el caso de dos cintas. :)

Michael Wehar

Como escribió @Ricky. AFAIK todavía es consistente con lo que sabemos que SAT está en tiempo lineal determinista. Para demostrar lo contrario, necesitaría un límite inferior de tiempo superlineal para SAT y no tenemos uno (no parece estar cerca de uno).

Kaveh