Théorème de dichotomie de Schaefer

Théorème de dichotomie de Schaefer dans la théorie de la complexité computationnelle, une branche de l'informatique, Le théorème de dichotomie de Schaefer énonce les conditions nécessaires et suffisantes dans lesquelles un ensemble fini S de relations sur le domaine booléen produit des problèmes polynomiaux ou NP-complets lorsque les relations de S sont utilisées pour contraindre certaines des variables propositionnelles.[1] C'est ce qu'on appelle un théorème de dichotomie parce que la complexité du problème défini par S est soit en P, soit en NP-complet par opposition à l'une des classes de complexité intermédiaire dont on sait qu'elles existent (en supposant P ≠ NP) par le théorème de Ladner.

Les cas particuliers du théorème de dichotomie de Schaefer incluent la complétude NP de SAT (le problème de satisfaisabilité booléenne) et ses deux variantes populaires 1-en-3 SAT et pas toutes égales 3SAT (souvent désigné par NAE-3SAT). En réalité, pour ces deux variantes de SAT, Le théorème de dichotomie de Schaefer montre que leurs versions monotones (où les négations de variables ne sont pas autorisées) sont aussi NP-complets.

Contenu 1 Présentation originale 2 Présentation moderne 3 Propriétés des polymorphismes 4 Généralisations 5 Travaux connexes 6 Voir également 7 References Original presentation Schaefer defines a decision problem that he calls the Generalized Satisfiability problem for S (noté SAT(S)), où {style d'affichage S={R_{1},ldots ,R_{m}}} est un ensemble fini de relations sur des variables propositionnelles. Une instance du problème est une formule S, c'est à dire. une conjonction de contraintes de la forme {style d'affichage R_{j}(X_{je_{1}},ldots ,X_{je_{n}})} où {style d'affichage R_{j}en S} et le {style d'affichage x_{je_{j}}} sont des variables propositionnelles. Le problème est de déterminer si la formule donnée est satisfiable, en d'autres termes si les variables peuvent être affectées de valeurs telles qu'elles satisfassent toutes les contraintes données par les relations de S.

Schaefer identifie six classes d'ensembles de relations booléennes pour lesquelles SAT(S) est dans P et prouve que tous les autres ensembles de relations génèrent un problème NP-complet. Un ensemble fini de relations S sur le domaine booléen définit un problème de satisfiabilité calculable en temps polynomial si l'une des conditions suivantes est vérifiée: toutes les relations qui ne sont pas constamment fausses sont vraies quand tous ses arguments sont vrais; toutes les relations qui ne sont pas constamment fausses sont vraies quand tous ses arguments sont faux; toutes les relations sont équivalentes à une conjonction de clauses binaires; toutes les relations sont équivalentes à une conjonction de clauses de Horn; toutes les relations sont équivalentes à une conjonction de clauses à double corne; toutes les relations sont équivalentes à une conjonction de formules affines. [2] Autrement, le problème SAT(S) est NP-complet.

Modern presentation A modern, une présentation simplifiée du théorème de Schaefer est donnée dans un article explicatif de Hubie Chen.[3][4] En termes modernes, le problème SAT(S) est considéré comme un problème de satisfaction de contraintes sur le domaine booléen. Dans cette zone, il est standard de désigner l'ensemble des relations par Γ et le problème de décision défini par Γ comme CSP(C).

Cette compréhension moderne utilise l'algèbre, en particulier, algèbre universelle. Pour le théorème de dichotomie de Schaefer, le concept le plus important en algèbre universelle est celui de polymorphisme. Une opération {style d'affichage f:D^{m}à D} est un polymorphisme d'une relation {displaystyle Rsubseteq D^{k}} si, pour tout choix de m tuples {style d'affichage (t_{11},pointsc ,t_{1k}),pointsc ,(t_{m1},pointsc ,t_{mk})} de R, il considère que le tuple obtenu à partir de ces m tuples en appliquant f en coordonnées, c'est à dire. {style d'affichage (F(t_{11},pointsc ,t_{m1}),pointsc ,F(t_{1k},pointsc ,t_{mk}))} , est dans R. C'est-à-dire, une opération f est un polymorphisme de R si R est fermé par f: l'application de f à n'importe quel tuple dans R donne un autre tuple à l'intérieur de R. Un ensemble de relations Γ est dit avoir un polymorphisme f si chaque relation dans Γ a f comme polymorphisme. Cette définition permet la formulation algébrique du théorème de dichotomie de Schaefer.

Soit Γ un langage de contraintes fini sur le domaine booléen. Le problème CSP(C) est décidable en temps polynomial si Γ a l'une des six opérations suivantes comme polymorphisme: l'opération unaire constante 0; l'opération unaire constante 1; l'opération ET binaire ∧; l'opération OU binaire ∨; l'opération majoritaire ternaire {nom de l'opérateur de style d'affichage {Majorité} (X,y,z)=(xcoin y)vé (xcoin z)vé (ycoin z);} l'opération ternaire minoritaire {nom de l'opérateur de style d'affichage {Minorité} (X,y,z)=xoplus yoplus z.} Autrement, le problème CSP(C) est NP-complet.

Dans cette formulation, il est facile de vérifier si l'une des conditions de traçabilité tient.

Properties of Polymorphisms Given a set Γ of relations, il existe un lien étonnamment étroit entre ses polymorphismes et la complexité de calcul de CSP(C).

Une relation R est dite primitive positive définissable, ou court pp-définissable, d'un ensemble Γ de relations si R(v1, ... , vk) ⇔ ∃x1 ... xm. C est valable pour une certaine conjonction C de contraintes de Γ et d'équations sur les variables {v1,...,vk, x1,...,xm}. Par exemple, si Γ est constitué de la relation ternaire nae(X,y,z) tenir si x,y,z ne sont pas tous égaux, et R(X,y,z) est x∨y∨z, alors R peut être pp-défini par R(X,y,z) ⇔ ∃a. non(0,X,un) ∧ non(y,z,¬a); cette réduction a été utilisée pour prouver que NAE-3SAT est NP-complet. L'ensemble de toutes les relations pp-définissables à partir de Γ est noté ≪Γ≫. Si Γ' ⊆ ≪Γ≫ pour des ensembles de contraintes finis Γ et Γ', puis CSP(C') réduit à CSP(C).[5] Étant donné un ensemble Γ de relations, Pol(C) désigne l'ensemble des polymorphismes de Γ. inversement, si O est un ensemble d'opérations, puis Inv(O) désigne l'ensemble des relations ayant toutes les opérations en O comme un polymorphisme. Pol et Inv construisent ensemble une connexion Galois. Pour tout ensemble fini Γ de relations sur un domaine fini, ≪Γ≫ = Inv(Pol(C)) détient, C'est, l'ensemble des relations pp-définissables à partir de Γ peut être dérivé des polymorphismes de Γ.[6] En outre, si Pol(C) ⊆ Pol(C') pour deux ensembles de relations finis Γ et Γ', alors Γ' ⊆ ≪Γ≫ et CSP(C') réduit à CSP(C). En conséquence, deux ensembles de relations ayant les mêmes polymorphismes conduisent à la même complexité de calcul.[7] Generalizations The analysis was later fine-tuned: CSP(C) est soit résoluble dans co-NLOGTIME, L-complet, NL-complet, ⊕L-complet, P-complet ou NP-complet et étant donné Γ, on peut décider en temps polynomial lequel de ces cas est vrai.[8] Le théorème de dichotomie de Schaefer a été récemment généralisé à une classe plus large de relations.[9] Related work If the problem is to count the number of solutions, qui est noté #CSP(C), alors un résultat similaire de Creignou et Hermann est valable.[10] Soit Γ un langage de contraintes fini sur le domaine booléen. Le problème #CSP(C) est calculable en temps polynomial si Γ admet comme polymorphisme une opération de Mal'tsev. Autrement, le problème #CSP(C) est #P-complet. Une opération de Mal'tsev m est une opération ternaire qui satisfait {style d'affichage m(X,y,y)=m(y,y,X)=x.} Un exemple d'opération Mal'tsev est l'opération minoritaire donnée dans le, formulation algébrique du théorème de dichotomie de Schaefer ci-dessus. Ainsi, quand Γ a l'opération minoritaire comme polymorphisme, il n'est pas seulement possible de décider CSP(C) en temps polynomial, mais pour calculer #CSP(C) en temps polynomial. Il y a au total 4 Opérations Mal'tsev sur les variables booléennes, déterminé par les valeurs de {style d'affichage m(J,F,J)} et {style d'affichage m(F,J,F)} . Un exemple moins symétrique est donné par {style d'affichage m(X,y,z)=(xcoin z)vé (coin négatif (xvee z))} . Sur un autre domaine, tels que des groupes, des exemples d'opérations Mal'tsev comprennent {style d'affichage x-y+z} et {style d'affichage xy^{-1}z.} Pour les grands domaines, même pour un domaine de taille trois, l'existence d'un polymorphisme de Mal'tsev pour Γ n'est plus une condition suffisante pour la tractabilité de #CSP(C). Cependant, l'absence d'un polymorphisme de Mal'tsev pour Γ implique toujours la #P-dureté de #CSP(C).

Voir aussi Théorèmes de classification Max/min CSP/Ones, un ensemble similaire de contraintes pour les problèmes d'optimisation Références ^ Schaefer, Thomas J. (1978). "La complexité des problèmes de satisfaction". STOCK 1978. pp. 216–226. est ce que je:10.1145/800133.804350. ^ Schäfer (1978, p.218 à gauche) définit une formule affine comme étant de la forme x1 ⊕ ... ⊕ xn = c, où chaque xi est une variable, c est une constante, c'est à dire. vrai ou faux, et "⊕" désigne XOR, c'est à dire. addition dans un anneau booléen. ^ Chen, Hubie (Décembre 2009). "Un rendez-vous de logique, Complexité, et algèbre". Enquêtes informatiques ACM. 42 (1): 1–32. arXiv:cs/0611018. est ce que je:10.1145/1592451.1592453. ^ Chen, Hubie (Décembre 2006). "Un rendez-vous de logique, Complexité, et algèbre". Actualités SIGACT (Colonne logique). arXiv:cs/0611018. ^ Chen (2006), p.8, Proposition 3.9; Chen utilise la réduction polynomiale plusieurs fois ^ Chen (2006), p.9, Théorème 3.13 ^ Chen (2006), p.11, Théorème 3.15 ^ Allender, Éric; terrain constructible, Michael; Immerman, Neil; Schnoor, Henning; Vollmer, Héribert (Juin 2009). "La complexité des problèmes de satisfaisabilité: Affiner le théorème de Schaefer" (PDF). Journal des sciences informatiques et des systèmes. 75 (4): 245–254. est ce que je:10.1016/j.jcss.2008.11.001. Récupéré 2013-09-19. ^ Bodirski, Manuel; Pentecôte, Michael (2015). "Théorème de Schaefer pour les graphes". J. ACM. 62 (3): 19:1–19:52. arXiv:1011.2894. est ce que je:10.1145/2764899. ^ Creigné, Nadia; Hermann, Miki (1996). "Complexité des problèmes de comptage de satisfaisabilité généralisée". Information et calcul. 125 (1): 1–12. est ce que je:10.1006/inco.1996.0016. ISSN 0890-5401. Catégories: Programmation par contraintesThéorèmes en théorie de la complexité computationnelle