EXPTIME

En théorie de la complexité, EXPTIME (ou EXP) est la classe de complexité qui est l'ensemble des problèmes de décision décidés par une machine de Turing déterministe en temps exponentiel.

Définition formelle

Si l'on appelle $\text{DTIME}(t(n))$, l'ensemble de tous les problèmes qui peuvent être résolus par des machines de Turing déterministes utilisant un temps $O(t(n))$ pour une fonction $t$ en la taille de l'entrée $n$, alors on peut définir EXPTIME formellement par :

$\text{EXPTIME}=\bigcup _{k\in \mathbb{N}}\text{ DTIME }\left(2^{n^k}\right).$

Propriétés

Diagramme d'inclusions des classes de complexité classiques.

Comme l'illustre l'image de droite, on a les inclusions suivantes : P $\subseteq$ NP $\subseteq$ PSPACE $\subseteq$ EXPTIME.

EXPTIME est une classe relativement grosse, qui contient des problèmes considérés comme impossibles à résoudre de façon efficace. Mais il existe des classes plus grosses comme EXPSPACE et NEXPTIME (respectivement les problèmes pouvant être résolus en espace exponentiel, et en temps exponentiel sur machine non déterministe).

Par un argument de « Modèle:Langue » (remplissage), on a le théorème suivant, lié au problème P=NP : Modèle:Théorème

De plus d'après le théorème de hiérarchie en temps déterministe, la classe P est différente de la classe EXPTIME.

La classe EXPTIME est égale à la classe APSPACE, l'équivalent de PSPACE sur machine de Turing alternante, d'après le théorème de Chandra-Kozen-Stockmeyer.

En complexité descriptive, EXPTIME correspond à SO(LFP), c'est-à-dire à la logique du second ordre avec plus petit point fixe.

Problèmes EXPTIME-complets

Le problème de l'arrêt d'une machine de Turing après k pas de temps (où k est écrit en notation binaire) est EXPTIME-complet. C'est une restriction du problème de l'arrêt, qui est indécidable dans le cas général.

Le problème de satisfiabilité des logiques suivantes sont EXPTIME-complets :

• la logique temporelle CTL est EXPTIME-completModèle:Référence nécessaire ;
• la logique propositionnelle dynamique (PDL).

Des versions succinctes de certains problèmes P-complets sont EXPTIME-complets, comme SUCCINCT CIRCUIT VALUEModèle:Référence nécessaire.

EXPTIME et jeux à deux joueurs

Jeu PEEK, un des premiers jeux à deux joueurs démontré EXPTIME-complet par Chandra et Stockmeyer.

Via les machines de Turing alternantes, et via l'égalité entre la classe APSPACE (en espace polynomial sur une machine alternante) et EXPTIME, Chandra et Stockmeyer ont exhibé des jeux booléens à information parfaite à deux joueurs et des jeux sur des graphes qui sont EXPTIME-complets.

Un des jeux booléens, EXPTIME-complet, est présenté comme un jeu à deux joueurs appelé PEEK. Une boîte est perforée et contient des plaques perforées du Modèle:Nobr et des plaques perforées du Modèle:Nobr. Les joueurs jouent tour à tour : soit il ne fait rien soit il tire ou pousse une de ses plaques. Un des joueurs gagnent s'il arrive à aligner verticalement une série de trous à travers toute la boîte. Une instance de PEEK est la description des deux ensembles de plaques perforées (arbitrairement grandes). Plus formellement, le jeu PEEK, appelé G4 dans l'article de Chandra et Stockmeyer, est le suivant. En entrée, on se donne une formule booléenne sous forme normale disjonctive avec au plus Modèle:Nb par clause. On se donne aussi une valuation initiale sur les Modèle:Nobr apparaissant dans la formule. L'ensemble des variables est partitionné en deux : les Modèle:Nobr contrôlés par le premier joueur et les Modèle:Nobr contrôlés par le deuxième. Le premier joueur qui rend la formule vrai gagne. Le problème de décision consiste à décider si le premier joueur a une stratégie gagnante.

Les travaux de Chandra Stockmeyer ont alors permis de montrer que des versions généralisées de jeux, comme les échecs, les dames et le go sont EXPTIME-complets ; ces jeux ont été généralisés dans le sens où la taille du plateau est donnée en entrée du problème. Aussi, la logique contrainte est un outil pour démontrer la EXPTIME-dureté de certains jeux.

Aussi, les travaux de Chandra et Stockmeyer ont permis à Littman de démontrer que le problème de la planification automatique où les actions sont non-déterministes et où l'agent a information parfaite est EXPTIME-dur.

Voir aussi

Articles connexes

• Théorie de la complexité (informatique théorique)
• Classe de complexité
• E (complexité) : la classe des problèmes de EXPTIME qui ont un exposant linéaire en fonction de la taille, autrement dit E = DTIME$(2^{O(n)})$.

Liens externes

• Modèle:Complexity Zoo