Une variante de Critical SAT en DP

Une langue est dans la classe ssi il y a deux langues et telles que $L$ $DP$ $L1 \in NP$ $L2 \in coNP$ $L = L1 \cap L2$

A canonique problème -complete est SAT-UNSAT: étant donné deux expressions 3-CNF, et , est - il vrai que est satisfiable et est pas? $DP$ $F$ $G$ $F$ $G$

Le problème SAT critique est également connu pour être -complet: étant donné une expression 3-CNF , est-il vrai que n'est pas satisfaisant mais la suppression d'une clause la rend satisfaisable? $DP$ $F$ $F$

J'examine la variante suivante du problème SAT critique: étant donné une expression 3-CNF , est-il vrai que est satisfaisable mais l'ajout de 3 clauses (sur mais en utilisant les mêmes variables que ) le rend insatisfaisant? Mais je n'arrive pas à trouver une réduction de SAT-UNSAT ou même à prouver que c'est ou difficile. $F$ $F$ $F$ $F$ $NP$ $coNP$

Ma question: cette variante est-elle complète DP?

Merci pour vos réponses.

cc.complexity-theory np-hardness complexity-classes sat Xavier Labouze
la source

Je ne connaissais pas DP: classe intéressante, surtout si CRITICAL-SAT est complet pour ça.

Suresh Venkat

S'il y a deux affectations satisfaisantes

, alors

n'est pas maximal. (supposons qu'elles diffèrent sur la variable

, alors

n'est pas impliqué par la formule et l'ajouter ou une clause la contenant ne changera pas la satisfiabilité.) Si nous pouvons trouver une clause non impliquée par la formule en temps polynomial, nous pouvons ajouter c'est négation de la formule et en utilisant simplement la règle de la clause unitaire. Finalement, nous trouverons la valeur de toutes les variables pour une affectation satisfaisante. Il suffit ensuite de vérifier si la formule est équivalente à la formule canonique pour cette affectation.

τ \neq τ^{'} ⊨ φ

$\tau\neq\tau' \vDash \varphi$

φ

$\varphi$

p

$p$

p

$p$

Kaveh

@Kaveh: J'ai mal compris votre question raffinée. Dans votre version de la question, "il n'y a pas de clause qui n'est pas impliquée par la formule et qui puisse y être ajoutée sans la rendre insatisfaisante" équivaut à la condition qu'il y ait exactement une affectation satisfaisante, et c'est une norme américaine - problème complet (donc coNP-difficile).

Tsuyoshi Ito du

Xavier: Vous avez raison, la langue de la version de @ Kaveh est un sous-ensemble de la langue de votre version. Mais cela n'implique pas de réductibilité entre les deux problèmes (dans les deux sens). N'oubliez pas qu'une réduction doit mapper les instances yes aux instances yes et no-instances à no-instances.

Tsuyoshi Ito du

Désolé, j'ai écrit dans la direction opposée. La langue de votre version est un sous-ensemble de la langue de la version de Kaveh.

Tsuyoshi Ito du

Réponses:

[Je l'ai fait dans une bonne réponse b / c quelqu'un l'a donné -1]

Si une clause est autorisée à être ajoutée, alors le langage est vide - clairement à toute formule satisfaisable vous pouvez ajouter un 3 clauses composé de variables qui n'apparaissent pas dans : sera satisfaisable. $F$ $c$ $F$ $F \cup \{ c \}$

$F$

La justification est la suivante:

$F \in L$ $F \in SAT$ $c$ $F$ $F \cup \{c\} \in UNSAT$ $c = l_1 \lor l_2 \lor l_3 \notin F$ $l_i$ $F \cup \{ c \}$ $F$ $l_i=0$ $i=1,2,3$ $l_1=1$ $c$ $F \cup \{c\}$ $c'$ $c$ $c' \notin F$ $c' = \neg l_1 \lor l_2 \lor l_3$ $F$ $l_1 = 1$ $F \in L$ $c \in F$ $F$ $c$ $F$ $F$ $F$ affrontement, ce qui peut clairement être fait en temps linéaire.

Anton Belov
la source

Votre observation est essentiellement: pour avoir la réponse Oui, F doit contenir exactement sept des huit clauses sur n'importe quel choix de trois variables distinctes. Par conséquent, trouver l'affectation unique (ou détecter une incohérence) se fait facilement en temps polynomial.

Tsuyoshi Ito du

@Xavier: Les deux problèmes peuvent sembler similaires, mais l'observation d'Anton montre qu'ils sont tout simplement très différents. Ceci est très courant dans la complexité de calcul. Des exemples typiques incluent la comparaison entre 2SAT et 3SAT et entre le circuit eulérien et le circuit hamiltonien.

Tsuyoshi Ito du

@Xavier - La réponse de Tayfun est incorrecte . Il montre que le problème est en DP - c'est bien, tout problème en P est automatiquement en DP. Afin de montrer que le problème est DP-complet, il doit montrer la réduction à un autre problème DP-complet (par exemple la première variante de Critical SAT). J'ai soumis la modification à sa réponse, mais elle est dans la file d'attente pour un "examen par les pairs".

Anton Belov

@Anton: La modification drastique des réponses postées par d'autres utilisateurs n'est généralement pas recommandée. Si vous pensez que la réponse de Tayfun est fondamentalement incorrecte, vous ne devriez pas essayer de la corriger en la modifiant.

Tsuyoshi Ito du

Il ressort très clairement du problème SAT-UNSAT que pour une formule, vous vérifiez la satisfiabilité pour l'autre formule, vous vérifiez l'insatisfiabilité ... Dans le problème de sat critique d'origine, vous ne tenez pas pour acquis que la formule booléenne donnée est insatisfaisante. Vous devez le vérifier. De même avec la version Xaviers, vous devez vérifier que la formule booléenne donnée est satisfaisable.

Tayfun Pay du

-1

Puis-je proposer une réponse à ma propre question grâce à vos commentaires: la variante de Critical SAT est en P.

$F$ $F$ $F$

$F$ $F$

$F$

$F$ $F$ $F$ $F$ $F$ $F$

$F$ $F$ $F$ $F$ $F$ $F$ $F$ $F$ $F$

$F$ $F$

$F$ $\binom{n}{3}$ $\frac{n(n-1)(n-2)}{3}$ $n$

Xavier Labouze
la source

Vous avez reformulé le problème d'origine à votre convenance.

Tayfun Pay du

Je ne suis pas sûr de la version 3-SAT. Étant donné une formule booléenne dans CNF avec des clauses M et une variable N, IF M = (3 ^ N) - (2 ^ N), la formule booléenne donnée est alors INSATISFAIT ou n'a qu'une seule solution. Même ainsi, pour vérifier la satisfaction à cette instance est toujours NP. Il n'y a aucun moyen que votre version soit en P.

Tayfun Pay

@Xavier: Cette réponse semble correcte, mais je pense que c'est la même chose que ce que fait Anton dans sa réponse.

Tsuyoshi Ito

@Tsuyoshi, vous avez raison, je viens de présenter le problème 2 dont la première partie (tester si une formule contient toutes les clauses qu'elle implique) m'intéresse - au fait, avez-vous une idée de la complexité de cette première partie?

Xavier Labouze