Existe um algoritmo de tempo linear não determinístico para CNF-SAT?

O problema de decisão CNF-SAT pode ser descrito da seguinte maneira:

Entrada: uma fórmula booleana na forma normal conjuntiva. $\phi$

Pergunta: Existe uma atribuição de variável que satisfaça ? $\phi$

Estou considerando várias abordagens diferentes para resolver o CNF-SAT com uma máquina de Turing de duas fitas não determinística .

Eu acredito que existe um NTM que resolve CNF-SAT nas . $n \cdot \texttt{poly}(\log(n))$

Pergunta: Existe um NTM que resolva CNF-SAT nas etapas ? $O(n)$

Quaisquer referências relevantes são apreciadas, mesmo que apenas forneçam abordagens não determinísticas no tempo quase linear.

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

Santhanam escreveu em 2001: "SAT NTIME ( polylog ), resultado que resulta dos fatos de que SAT pode ser aceito em polylog em uma NRAM e que existe uma simulação eficiente de NRAMs por MNTs, devido a Gurevich e Selá. " Portanto, parece-me improvável que SAT NTIME ( ) seja conhecido. (A referência é a LNCS 363 de 1989.)

\in

$\in$

n

$n$

(n)

$(n)$

n

$n$

(n)

$(n)$

\in

$\in$

n

$n$

András Salamon

@Boson, suponha que você receba não apenas uma tarefa satisfatória, mas também um cálculo completo da fórmula. Como você verificaria se é um cálculo válido em tempo linear? Não está claro, mesmo que você possa fazê-lo no 3CNF-SAT, porque você precisa pular para procurar a atribuição das variáveis.

Kaveh

@Boson Não está claro se você pode verificar se a atribuição satisfaz a fórmula em tempo linear com uma TM de duas fitas. Você provavelmente teria que mover a cabeça da fita para frente e para trás várias vezes. Se você tiver uma abordagem eficiente para esta verificação, entre em contato. :)

Michael Wehar

Apenas uma observação: se as variáveis são representadas em unário (SAT ainda é NPC), existe um NTM de duas fitas que reconhece uma fórmula satisfatória unária

steps

φ

$\varphi$

2 | φ |

$2|\varphi|$

Marzio De Biasi

@MichaelWehar, se você usar uma classificação de contagem, poderá classificar n chaves no intervalo [0, k] no tempo O (n + k) em um modelo de acesso aleatório razoável (por exemplo, Máquina de Turing de acesso aleatório, onde você pode usar O (log n) tempo para anotar um índice e depois pular para esse índice da fita em uma etapa). Se você codificar cada literal como uma sequência de bits (log n + 1), o número total de cláusulas e variáveis será no máximo O (n / log n); nesse caso, operações de tempo O (log n) em todos os literais Estão bem. A extensão para duas fitas TM não é simples, pelo menos com a classificação de contagem.

Ryan Williams

Respostas:

Este é apenas um comentário estendido. Algumas vezes atrás eu perguntei (eu :-) quão rápido um NTM multitape que aceita uma linguagem NP completa (razoavelmente codificada) pode ser. Eu tive essa ideia:

O 3-SAT permanece NP-completo, mesmo que as variáveis sejam representadas em unárias. Em particular, pode converter uma cláusula - suponha que - de uma fórmula arbitrária 3-SAT em variáveis e cláusulas em uma sequência de caracteres através alfabeto em que cada ocorrência variável é representada em unário: $(x_i \lor \neg x_j \lor x_k)$ $\varphi$ $n$ $m$ $\Sigma = \{ +, -, 1 \}$

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

Por exemplo, pode ser convertido em: $(x_2 \lor -x3 \lor +4)$

+110-1110+11110

Assim, podemos converter uma fórmula 3-SAT em uma seqüência equivalente concatenação de suas cláusulas. A linguagem é NP-completo. $\varphi_i$ $U(\varphi_i)$ $L_U = \{ U(\varphi_i) \mid \varphi_i \in 3-SAT \}$

Um NTM de 2 fitas pode decidir se uma sequência no tempo nesse caminho. $x \in L_U$ $2|x|$

o primeiro cabeçalho verifica a entrada da esquerda para a direita e, com a lógica interna, mantém o controle quando entra ou sai de uma cláusula ou chega ao final da fórmula. Sempre que encontra um ou , o segundo cabeçote começa a se mover com ele no que representa . No final de , se o segundo cabeçalho estiver em , ele adivinha um valor de verdade ou (faz uma atribuição) e o grava na segunda fita; se encontrar um ou , essa variável já recebeu um valor; $+$ $-$ $1^i$ $x_i$ $1^i$ $0$ $+$ $-$ $+$ $-$
nos dois casos, usando a lógica interna, o NTM corresponde ao valor de verdade sob o segundo cabeçalho (a atribuição) com o último visto ou ; se eles correspondem, a cláusula é satisfeita; $+$ $-$
então a segunda cabeça pode retornar à célula mais à direita;
com a lógica interna, o NTM pode acompanhar se todas as cláusulas são satisfeitas enquanto o primeiro cabeçalho se move para o final da entrada.

Exemplo:

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)

O tempo pode ser reduzido para se adicionarmos alguns símbolos redundantes à representação da cláusula: $|x|$

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

( marca o final da fórmula) $\text{+++}$

Dessa maneira, o segundo cabeçote pode retornar à célula mais à esquerda, enquanto o primeiro verifica a parte . Usando como delimitador de cláusula e como marcador para o final da fórmula, podemos usar a mesma representação para fórmulas CNF com um número arbitrário de literais por cláusula. $0^i$ $\text{++}$ $\text{+++}$

Marzio De Biasi
fonte

v

$v$

v

$v$

2

$2$

2 n

$2n$

v

$v$

v - 1

$v-1$

2 n - c

$2n - c$

n

$n$

c

$c$

Θ (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'})$

Não é exatamente o que você está procurando, mas para o NTM de 1 fita, a resposta parece ser negativa: o SAT não é solucionável por um NTM de 1 fita em tempo linear não determinístico.

$REG$ $o(n \log(n))$ $o(n \log(n))$

Boson
fonte

Esse teorema é apenas sobre máquinas de Turing de uma cabeça .

$\:$ (Por exemplo, máquinas de Turing de duas cabeças podem facilmente decidir a linguagem do palíndromo em tempo linear e espaço constante.)

$\;\;\;\;$

Isso é ótimo! Muito obrigado. Mas, eu estou mais interessado no caso de duas fitas. :)

Michael Wehar

Como escreveu o @Ricky. AFAIK ainda é consistente com o que sabemos que o SAT está no tempo linear determinístico. Para provar o contrário, você precisaria de um limite inferior de tempo superlinear para o SAT e não temos um (não parece estar perto de um).

Kaveh