2-SAT avec XOR-relations NP-complet?

Je me demande s'il existe un algorithme polynomial pour "2-SAT avec relations XOR". Les deux 2-SAT et XOR-SAT sont en P, mais est-ce que sa combinaison?

Exemple d'entrée:

• Partie 2-SAT: (a or !b) and (b or c) and (b or d)

• Partie XOR: (a xor b xor c xor 1) and (b xor c xor d)

En d'autres termes, l'entrée est la formule booléenne suivante:

Exemple de sortie: satisfaisant: a = 1, b = 1, c = 0, d = 0.

Le nombre de clauses 2-SAT et le nombre de clauses XOR dans l'entrée sont tous les deux , où est le nombre de variables booléennes.$O(n)$$n$

Les relations 2-SAT avec XOR peuvent être prouvées NP-complètes par réduction de 3-SAT. Toute clause 3-SAT peut être réécrite dans l'expression équisatisfiable de relations 2-SAT-avec-XOR avec et comme nouvelles variables.

Vous n'avez pas spécifié l'arité de vos relations XOR, mais comme dans la réduction SAT-to-3SAT habituelle, vous pouvez toujours arranger que leur arité soit au plus 3. Maintenant, vous êtes en grande position pour appliquer le théorème de dichotomie de Schaefer , qui vous dire si votre problème est en P ou NP-complet (ce sont les deux seules options). S'il s'avère être en P, la prochaine étape pourrait être de regarder Allender et al. , ce qui vous permettra de savoir à quel point votre problème est facile.

Selon le théorème de dichotomie de Schaefer , c'est NP-complet.

Considérons le cas où toutes les clauses contiennent 2 ou 3 littéraux; on peut alors considérer cela comme un problème de satisfaction de contraintes sur un ensemble de relations d'arité 3. En particulier, les relations sont les suivantes: , , , , .$\Gamma$$R(x,y,z)$$x \lor y$$x \lor \neg y$$\neg x \lor \neg y$$x \oplus y \oplus z$$x \oplus y \oplus \neg z$

Appliquez maintenant le théorème de dichotomie de Schaefer, dans sa forme moderne . Vérifiez chacune des six opérations pour voir s'il s'agit d'un polymorphisme:

• Unaire 0: Pas un polymorphisme de .$x \lor y$
• Unaire 1: Pas un polymorphisme de .$\neg x \lor \neg y$
• ET binaire: Pas un polymorphisme de . (Considérons et ; ils satisfont tous les deux à la relation, mais leur point par point ET ne le fait pas.)$x \lor y$$(0,1,0)$$(1,0,0)$$(0,0,0)$
• OU binaire: pas un polymorphisme de . (Considérez et ; ils satisfont la relation, mais ne le fait pas.)$\neg x \lor \neg y$$(0,1,0)$$(1,0,0)$$(1,1,0)$
• Majorité ternaire: Pas un polymorphisme de . (Considérons et et ; ils satisfont la relation, mais leur majorité ne le fait pas.)$x \oplus y \oplus z$$(0,0,1)$$(0,1,0)$$(1,0,0)$$(0,0,0)$
• Minorité ternaire: Pas un polymorphisme de . (Considérez , et ; ils satisfont la relation, mais pas leur minorité .)( 0 , 1 , 0 ) ( 1 , 0 , 0 ) ( 1 , 1 , 0 ) ( 0 , 0 , 0 $x \lor y$$(0,1,0)$$(1,0,0)$$(1,1,0)$$(0,0,0)$

Il s'ensuit que ce problème est NP-complet, même si vous limitez toutes les clauses XOR à être de longueur au plus 3.

D'un autre côté, si toutes les clauses XOR sont limitées à être de longueur au plus 2, alors c'est en P. En particulier est équivalent à , donc une telle formule est équivalente à une formule 2SAT, dont la satisfiabilité peut être déterminée en temps polynomial.( x ∨ y ) ∧ ( ¬ x ∨ ¬ y $(x \oplus y)$$(x \lor y) \land (\neg x \lor \neg y)$