Existe-t-il un algorithme de temps linéaire non déterministe pour CNF-SAT?

Le problème de décision CNF-SAT peut être décrit comme suit:

Entrée: Une formule booléenne $\phi$ sous forme normale conjonctive.

Question: Existe-t-il une affectation de variable qui satisfait $\phi$ ?

J'envisage plusieurs approches différentes pour résoudre CNF-SAT avec une machine de Turing à deux bandes non déterministe .

Je crois qu'il existe un NTM qui résout CNF-SAT en $n \cdot \texttt{poly}(\log(n))$ étapes .

Question: Existe - t-il un NTM qui résout CNF-SAT en étapes $O(n)$ ?

Toutes les références pertinentes sont appréciées même si elles ne fournissent que des approches non déterministes à temps quasi linéaire.

time-complexity sat turing-machines np nondeterminism Michael Wehar
la source

Santhanam en 2001 a écrit: "SAT

NTIME (

polylog

), un résultat qui découle des faits que SAT peut être accepté en

polylog

sur un NRAM et qu'il existe une simulation efficace des NRAM par les MNT , à cause de Gurevich et Shelah. " Il me semble donc peu probable que SAT

NTIME (

) soit connu. (La référence est au LNCS 363 de 1989.)

\in

$\in$

n

$n$

(n)

$(n)$

n

$n$

(n)

$(n)$

\in

$\in$

n

$n$

András Salamon

@Boson, supposez que l'on vous donne non seulement une affectation satisfaisante mais aussi un calcul complet de la formule. Comment vérifieriez-vous s'il s'agit d'un calcul valide en temps linéaire? Ce n'est pas clair même si vous pouvez le faire pour 3CNF-SAT car vous devez sauter pour rechercher l'affectation aux variables.

Kaveh du

@Boson Il n'est pas clair si vous pouvez vérifier que l'affectation satisfait la formule en temps linéaire avec une MT à deux bandes. Vous devrez probablement déplacer la tête de bande d'avant en arrière plusieurs fois. Si vous avez une approche efficace pour cette vérification, veuillez me le faire savoir. :)

Michael Wehar

Juste une note: si les variables sont représentées en unaire (SAT est toujours NPC), alors il y a un NTM à deux bandes qui reconnaît une formule unaire satisfaisable

dans

étapes

φ

$\varphi$

2 | φ |

$2|\varphi|$

Marzio De Biasi

@MichaelWehar si vous utilisez un tri de comptage, vous pouvez trier n clés dans la plage [0, k] dans le temps O (n + k) dans un modèle d'accès aléatoire raisonnable (par exemple, la machine de Turing à accès aléatoire, où vous pouvez prendre O (log n) le temps d'écrire un index, puis peut sauter à cet index de la bande en 1 étape). Si vous codez chaque littéral sous la forme d'une chaîne de bits (log n + 1), le nombre total de clauses et de variables est au maximum de O (n / log n), auquel cas des opérations de temps O (log n) sur tous les littéraux vont bien. L'extension à deux bandes TM n'est pas simple, du moins avec le tri par comptage.

Ryan Williams

Réponses:

Ce n'est qu'un commentaire étendu. Il y a quelques fois, j'ai demandé (moi-même :-) à quelle vitesse un NTM multitape qui accepte un langage NP-complet (raisonnablement encodé) peut être. J'ai eu cette idée:

3-SAT reste NP-complet même si les variables sont représentées en unaire. En particulier, nous pouvons convertir une clause - supposons - d'une formule arbitraire 3-SAT sur variables et clauses dans une séquence de caractères sur l'alphabet dans lequel chaque occurrence de variable est représentée en unaire: $(x_i \lor \neg x_j \lor x_k)$ $\varphi$ $n$ $m$ $\Sigma = \{ +, -, 1 \}$

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

Par exemple, peut être converti en: $(x_2 \lor -x3 \lor +4)$

+110-1110+11110

On peut donc convertir une formule 3-SAT en une chaîne équivalente concaténant ses clauses. La langue $\varphi_i$ $U(\varphi_i)$ est NP-complet. $L_U = \{ U(\varphi_i) \mid \varphi_i \in 3-SAT \}$

Un NTM à 2 bandes peut décider si une chaîne dans le temps de cette façon. $x \in L_U$ $2|x|$

la première tête analyse l'entrée de gauche à droite et avec la logique interne, elle garde une trace lorsqu'elle entre ou quitte une clause ou atteint la fin de la formule. Chaque fois qu'il trouve un ou , la deuxième tête commence à se déplacer à droite avec elle sur le qui représente . A la fin de , si la deuxième tête est sur un alors elle devine une valeur de vérité ou $+$ $-$ $1^i$ $x_i$ $1^i$ $0$ $+$ $-$ (elle fait une affectation) et l'écrit sur la deuxième bande; s'il trouve un ou alors cette variable a déjà reçu une valeur; $+$ $-$
dans les deux cas, en utilisant la logique interne, le NTM fait correspondre la valeur de vérité sous la deuxième tête (l'affectation) avec la dernière vue ou; s'ils correspondent alors la clause est satisfaite; $+$ $-$
alors la deuxième tête peut retourner dans la cellule la plus à droite;
avec la logique interne, le NTM peut garder une trace si toutes les clauses sont satisfaites pendant que la première tête se déplace vers la fin de l'entrée.

Exemple:

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)

Le temps peut être réduit à si nous ajoutons des symboles redondants à la représentation de la clause: $|x|$

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

( marque la fin de la formule) $\text{+++}$

De cette façon, la deuxième tête peut retourner dans la cellule la plus à gauche tandis que la première balaye la partie . Utilisation de comme délimiteur de clause et $0^i$ $\text{++}$ $\text{+++}$ comme marqueur pour la fin de la formule, nous pouvons utiliser la même représentation pour les formules CNF avec un nombre arbitraire de littéraux par clause.

Marzio De Biasi
la source

La représentation unaire est sans ambiguïté, donc on peut utiliser 0/1 pour +/-, donnant 011011110111110 pour votre premier exemple. 00 sert alors de marqueur de fin de clause, car 000 ne peut pas autrement se produire (si 00 se produit, alors c'est le marqueur de fin d'une variable et le signe suivant, donc le symbole suivant doit être 1). Le worktape seul contient le deviner

affectation de bits aux

des variables. Lorsqu'une variable est lue, la tête de bande de travail avance et est ensuite reculée au début lorsque le 0 est vu, donc au plus

étapes pour chaque bit de l'entrée.

v

$v$

v

$v$

2

$2$

András Salamon

En d'autres termes, même un NDTM avec une bande d'entrée unidirectionnelle et une seule bande de travail utilise au plus

étapes pour Unary SAT codé avec un alphabet booléen.

2 n

$2n$

András Salamon

Pour rendre les choses encore plus ordonnées, on peut en outre exiger que l'entrée contienne d'abord un préfixe avec le nombre de variables

spécifié en unaire. Cela permet de construire la conjecture lors de la lecture du préfixe. Il s'agit alors d'une sorte de codage "SATLIB unaire", de taille au plus quadratique dans une instance SAT standard, tant que chaque variable apparaît au moins une fois dans la formule et que les variables sont numérotées de 0 à

. Ces exigences semblent raisonnables.

v

$v$

v - 1

$v-1$

András Salamon,

@ AndrásSalamon: bien! En fixant l'encodage et le modèle (bande de lecture unidirectionnelle + bande de travail bidirectionnelle), nous obtenons un pire temps d'exécution de

sur les entrées de taille

, où

peut être rendu arbitrairement grand en incorporant un stockage fixe dans la logique interne de TM . Il pourrait être intéressant d'étudier si quelque chose peut être prouvé en utilisant le sens unique de la bande d'entrée et un argument de section transversale.

2 n - c

$2n - c$

n

$n$

c

$c$

Marzio De Biasi

Oui, pour autant que je sache, le produit d'espace-temps pour Unary SAT est quelque chose comme

par un argument standard. La représentation unaire des variables évite l'écart entre laborne supérieure

la plus connueet une borne supérieure

directepour CNF-SAT (bien que un meilleur algorithme dans ce cas pourrait alors également réduire l'écart).

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

Pas exactement ce que vous recherchez, mais pour le NTM 1 bande, la réponse semble être négative: SAT n'est pas résoluble par un NTM 1 bande en temps linéaire non déterministe.

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

Boson
la source

Ce théorème ne concerne que les machines de Turing à une tête .

$\:$ (Par exemple, les machines de Turing à deux têtes peuvent facilement décider de la langue du palindrome en temps linéaire et en espace constant.)

$\;\;\;\;$

C'est bien! Merci beaucoup. Mais, je suis plus intéressé par le cas de deux bandes. :)

Michael Wehar

Comme l'a écrit @Ricky. AFAIK il est toujours cohérent avec ce que nous savons que SAT est en temps linéaire déterministe. Pour prouver le contraire, vous auriez besoin d'une limite inférieure de temps super-linéaire pour SAT et nous n'en avons pas (ne semble pas être proche de un).

Kaveh