Le SAT 1 sur 3 reste-t-il NP-difficile même si chaque variable se produit à la fois positivement et négativement?

Le problème standard 1-en-3 SAT (ou XSAT ou X3SAT) est:
Instance : une formule CNF avec chaque clause contenant exactement 3 littéraux
Question : y a-t-il un paramètre d'assignation satisfaisant avec précision 1 littéral par clause vrai?

Le problème est NP-complet et reste difficile même si aucune variable ne se produit. Je me demande si ce problème devient facile ou reste difficile si chaque variable doit se produire au moins une fois positivement et au moins une fois négativement .

La réduction habituelle de 3SAT montrant que le SAT 1 en 3 est dur remplace une clause par des clauses , , où sont frais pour chaque clause. Ainsi, cette réduction n'aide pas à répondre à ma question. J'ai eu du mal à trouver un gadget montrant la dureté de cette variante, car si exactement 1 littéral dans une clause est vrai, alors 2 littéraux non symétriques sont faux. Si cela s'avère facile, penser en termes de partitions de l'ensemble de clauses pourrait le faire, mais je ne vois pas comment. $(x\lor y \lor z)$ $(\lnot x \lor a \lor b)$ $(y\lor b\lor c)$ $(\lnot z \lor c \lor d)$ $a,b,c,d$

cc.complexity-theory np-hardness sat Dominik Peters
la source

Peut-il être réduit à 2 sat?

Joshua Herman

indice: pour chaque var , ajoutez des clauses et, par exemple, .

X_{i}

$X_i$

(X_{i} \lor {\bar{X}}_{i} \lor W) \land (X_{i} \lor {\bar{X}}_{i} \lor Y) \land (X_{i} \lor {\bar{X}}_{i} \lor Z)

$(X_i\vee \overline X_i \vee W) \wedge (X_i\vee \overline X_i \vee Y)\wedge (X_i\vee \overline X_i \vee Z)$

(W \lor Y \lor \bar{Z})

$(W \vee Y \vee \overline Z)$

Neal Young

Ha, ça marche (bien sûr en ajoutant aussi ). Je vais laisser la question ouverte au cas où quelqu'un pourrait la résoudre sans l' astuce toujours si peu satisfaisante .

(\bar{W} \lor Y \lor Z) \land (W \lor \bar{Y} \lor Z)

$(\overline W \lor Y\lor Z)\land(W\lor\overline Y \lor Z)$

X_{i} \lor {\bar{X}}_{i}

$X_i\lor\overline X_i$

Dominik Peters

Puis-je vous encourager à rédiger une réponse complète à votre propre question, peut-être basée sur l'idée de Neal Young? (Soit dit en passant, je ne sais pas pourquoi c'est "insatisfaisant". Une réduction est une réduction.)

Si ce cas spécial est celui qui vous intéresse vraiment, alors peut-être qu'il est logique de modifier votre question pour refléter cette contrainte supplémentaire?

Réponses:

Dans un commentaire, OP a exprimé son intérêt pour une réduction qui générait des instances avec 3 variables distinctes par clause. Voici une approche simple:

La réduction est de 1 sur 3 SAT avec 3 variables distinctes par clause:

Tout d'abord, incluez toutes les clauses dans la formule d'entrée en tant que clauses dans la formule de sortie.
Deuxièmement, introduisez trois nouvelles variables , et et ajoutez les trois clauses suivantes à la formule de sortie: , et . $F_1$ $F_2$ $F_3$ $(\neg F_1, F_2, F_3)$ $(F_1, \neg F_2, F_3)$ $(F_1, F_2, \neg F_3)$
Enfin, pour chaque variable dans la formule d'origine, introduisez une nouvelle variable et ajoutez les deux clauses suivantes à la formule de sortie: et . $x$ $x'$ $(x, x', F_1)$ $(\neg x, \neg x', F_1)$

Vérifions que cette réduction fait ce que nous voulons. Les propriétés suivantes sont ce que nous voulons:

Chaque clause a toujours trois variables distinctes.
Chaque variable apparaît dans une clause positive et dans une clause négative.
La formule d'entrée est équivalente à la formule de sortie.

La propriété 1 est triviale à vérifier. La propriété 2 est également facile à vérifier: les variables , et apparaissent chacune à la fois positivement et négativement dans les clauses ajoutées au deuxième point, tandis que toutes les autres variables de la formule apparaissent à la fois positivement et négativement dans les clauses ajoutées dans le troisième puce. $F_1$ $F_2$ $F_3$

Quant à la propriété 3, elle est moins banale mais toujours facile. Vous pouvez facilement affirmer que la seule affectation pour les variables , et qui satisfait chaque clause à partir du deuxième point est de rendre les trois faux. Mais en supposant une valeur false pour , les clauses et ajoutées au troisième point sont satisfaites si et seulement si . Puisqu'il n'y a pas d'autres contraintes sur , cela signifie qu'il est toujours possible d'étendre une affectation satisfaisante pour la formule d'entrée dans une affectation satisfaisante pour la formule de sortie: définissez simplement chaque $F_1$ $F_2$ $F_3$ $F_i$ $F_1$ $(x, x', F_1)$ $(\neg x, \neg x', F_1)$ $x' = \neg x$ $x'$ $x'$ pour être la négation du correspondant et définir chaque sur faux. $x$ $F_i$

Mikhail Rudoy
la source