Voir la source de EXPTIME

{{Voir homonymes|EXP}}

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

== Définition formelle ==
Si l'on appelle <math>\mbox{DTIME}(t(n))</math>, l'ensemble de tous les problèmes qui peuvent être résolus par des [[machine de Turing|machines de Turing]] déterministes utilisant un temps <math>O(t(n))</math> pour une fonction <math>t</math> en la taille de l'entrée <math>n</math>, alors on peut définir EXPTIME formellement par :

:<math> \mbox{EXPTIME} = \bigcup_{k \in \mathbb{N} } \mbox{ DTIME } \left( 2^{ n^k } \right) . </math>

== Propriétés ==
[[Fichier:Complexity subsets pspace.svg|vignette|Diagramme d'inclusions des classes de complexité classiques.]]
Comme l'illustre l'image de droite, on a les inclusions suivantes : [[P (complexité)|P]] <math>\scriptstyle\subseteq</math> [[NP (complexité)|NP]] <math>\scriptstyle\subseteq</math> [[PSPACE]] <math>\scriptstyle\subseteq</math> 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 [[complexité en espace|espace]] exponentiel, et en temps exponentiel sur [[machine de Turing non déterministe|machine non déterministe]]).

Par un argument de « {{langue|en|padding}} » (remplissage), on a le théorème suivant<ref>{{Computational Complexity (Arora et Barak)|numéro chapitre=2.6.2|titre chapitre=EXP and NEXP}}.</ref>, lié au [[problème P=NP]] :
{{théorème|Si EXPTIME<math>\scriptstyle\neq</math>NEXPTIME alors  P<math>\scriptstyle\neq</math>NP}}

De plus d'après le [[théorème de hiérarchie en temps déterministe]], la classe [[P (complexité)|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 [[Ashok K. Chandra|Chandra]]-[[Dexter Kozen|Kozen]]-[[Larry Stockmeyer|Stockmeyer]]<ref>{{article
 |doi=10.1145/322234.322243
 |nom1=Chandra | prénom1=Ashok K.
 |nom2=Kozen | prénom2=Dexter C.
 |nom3=Stockmeyer | prénom3=Larry J.
 |titre=Alternation
 |périodique=[[Journal of the ACM]]
 |volume=28|numéro=1|passage=114-133
 |année=1981}}.</ref>.

En [[complexité descriptive]], EXPTIME correspond à SO(LFP), c'est-à-dire à la [[Logique d'ordre supérieur|logique du second ordre]] avec plus petit point fixe<ref>{{Complexity Zoo|fin=E#exp|nom=EXPTIME}}.</ref>.

== 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 (complexité)|complet]]<ref>{{lien web|lang=en|auteur=Chris Umans|url=http://users.cms.caltech.edu/~umans/cs21/lec16-17.pdf|format=pdf|titre=CS21 Decidability and Tractability (Lecture 16-17)|année=2017|site=[[Caltech]]}}.</ref>. C'est une restriction du [[problème de l'arrêt]], qui est [[Décidabilité|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{{Référence nécessaire|date=9 novembre 2017}} ;
* la [[Calcul des propositions|logique propositionnelle]] dynamique (PDL)<ref>{{Article|langue=en|titre=A near-optimal method for reasoning about action|périodique=Journal of Computer and System Sciences|volume=20|numéro=2|date=1980-04-01|issn=0022-0000|doi=10.1016/0022-0000(80)90061-6|lire en ligne=https://www.sciencedirect.com/science/article/pii/0022000080900616|consulté le=2018-03-05|pages=231–254}}.</ref>.

Des versions succinctes de certains problèmes P-complets sont EXPTIME-complets, comme SUCCINCT CIRCUIT VALUE{{Référence nécessaire|date=9 novembre 2017}}.

== EXPTIME et jeux à deux joueurs ==
[[Fichier:Peek game.png|vignette|Jeu PEEK, un des premiers jeux à deux joueurs démontré EXPTIME-complet par Chandra et Stockmeyer.]]
Via les [[Machine de Turing alternante|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<ref>{{Article|langue=en|prénom1=L.|nom1=Stockmeyer|prénom2=A.|nom2=Chandra|titre=Provably Difficult Combinatorial Games|périodique=SIAM Journal on Computing|volume=8|numéro=2|date=1979-05-01|issn=0097-5397|doi=10.1137/0208013|lire en ligne=http://epubs.siam.org/doi/abs/10.1137/0208013|consulté le=2017-10-26|pages=151–174}}.</ref>.

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 {{nobr|joueur 1}} et des plaques perforées du {{nobr|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 {{nb|13 littéraux}} par clause. On se donne aussi une [[valuation]] initiale sur les {{nobr|2k variables}} apparaissant dans la formule. L'ensemble des variables est partitionné en deux : les {{nobr|k variables}} contrôlés par le premier joueur et les {{nobr|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]]<ref>{{article|lang=en
 | auteur=[[Aviezri Fraenkel]]
 | auteur2 = D. Lichtenstein
 | titre = Computing a perfect strategy for n&times;n chess requires time exponential in n
 | périodique = J. Comb. Th. A
 | numéro = 31
 | année = 1981
 | passage = 199-214}}.</ref>, les [[dames]]<ref>{{article|lang=en
 | auteur = J. M. Robson
 | titre = N by N checkers is Exptime complete
 | périodique = SIAM Journal on Computing
 | volume = 13| numéro = 2| passage = 252-267
 | année = 1984| doi = 10.1137/0213018}}.</ref> et le [[Jeu de go|go]]<ref>{{Chapitre|lang=en
 | auteur = J. M. Robson
 | titre chapitre = The complexity of Go
 | titre ouvrage = Information Processing; Proceedings of IFIP Congress
 | année = 1983
 | passage = 413-417}}.</ref> 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<ref>{{Ouvrage|langue=en|prénom1=Robert Aubrey|nom1=Hearn|titre=Games, puzzles, and computation|nature ouvrage=thèse de doctorat|date=2006-01-01|lire en ligne=http://dl.acm.org/citation.cfm?id=1269411|consulté le=2018-04-28}}.</ref>.

Aussi, les travaux de Chandra et Stockmeyer ont permis à Littman de démontrer que le problème de la [[Planification (intelligence artificielle)|planification automatique]] où les actions sont non-déterministes et où l'agent a information parfaite est EXPTIME-dur<ref>{{Article|prénom1=Michael L.|nom1=Littman|titre=Probabilistic Propositional Planning: Representations and Complexity|périodique=In Proceedings of the Fourteenth National Conference on Artificial Intelligence|éditeur=MIT Press|date=1997|lire en ligne=http://citeseer.ist.psu.edu/viewdoc/summary?doi=10.1.1.38.3076|consulté le=2019-02-10|pages=748–754}}</ref>.

== Notes et références ==
{{Références}}

== 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<math>(2^{O(n)})</math>.

=== Liens externes ===
* {{Complexity Zoo|fin=E#exp|nom=EXPTIME}}

{{Palette|Théorie de la complexité}}

{{Portail|Informatique théorique}}

[[Catégorie:Classe de complexité]]