title: EXPTIME
text: # 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 ${\mbox{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 :
  
      ${\mbox{EXPTIME}}=\bigcup _{k\in \mathbb {N} }{\mbox{ DTIME }}\left(2^{n^{k}}\right).$
  
  ## Propriétés
  
  Comme l'illustre l'image de droite, on a les inclusions suivantes : P $\scriptstyle \subseteq$ NP $\scriptstyle \subseteq$ PSPACE $\scriptstyle \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 « padding » (remplissage), on a le théorème suivant, lié au problème P=NP :
  
  Théorème — Si EXPTIME$\scriptstyle \neq$NEXPTIME alors P$\scriptstyle \neq$NP
  
  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-complet ;
  * la logique propositionnelle dynamique (PDL).
  
  Des versions succinctes de certains problèmes P-complets sont EXPTIME-complets, comme SUCCINCT CIRCUIT VALUE.
  
  ## EXPTIME et jeux à deux joueurs
  
  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 joueur 1 et des plaques perforées du joueur 2. 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 13 littéraux par clause. On se donne aussi une valuation initiale sur les 2k variables apparaissant dans la formule. L'ensemble des variables est partitionné en deux : les k variables contrôlés par le premier joueur et les k variables 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.
  
  