Logique contrainte
En informatique théorique et en théorie des jeux, la logique contrainte (nom original en anglais : constraint logic) est un formalisme proposé par Robert A. Hearn et Erik D. Demaine[1] pour démontrer plus simplement des résultats de complexité théorique pour des jeux de plateau, comme le jeu de pousse-pousse qui a été montré complet pour la classe PSPACE[2]. La logique contrainte propose des gadgets et est utilisée pour prouver la dureté de généralisation de problèmes sur les graphes comme ensemble indépendant[3].
Définition modifier
La logique contrainte est un ensemble de règles de coups possibles dans un jeu sur des graphes particuliers appelés des graphes contraints. Un graphe contraint est un graphe orienté où chaque arc est pondéré par 1 (on le dessine alors en rouge), soit 2 (on le dessine alors en bleu). Chaque sommet est étiqueté par un entier, appelé flot entrant minimal. En fait, on peut supposer que le flot entrant minimal est toujours de deux. Le flot entrant d'un sommet est la somme des poids des arcs entrants dans ce sommet. Les contraintes sont les suivantes : une configuration est légale si en chaque sommet, le flot entrant est plus grand ou égal au flot entrant minimal.
Un coup dans un graphe contraint consiste à inverser un arc, si la configuration reste toujours légale. Dans un tel jeu, on exécute plusieurs coups et un joueur gagne s'il inverse un arc particulier.
Si le jeu est multi-joueurs, chaque joueur contrôle un ensemble d'arcs et un possède un arc particulier à inverser pour gagner. On dit que le jeu est déterministe si la suite d'inversions est forcée. On dit que le jeu est borné si on rajoute la condition que chaque arc n'est inversé qu'une fois au plus.
La logique contrainte permet de simuler des portes ET et des portes OU, mais ne permet pas de simuler des portes NON (en ce sens, la logique est dite monotone[1] p. 19).
Simulation d'une porte ET modifier
La figure ci-contre représente un sommet d'un graphe contraint. On suppose son flot entrant minimal est 2. Les deux arcs rouges pondérés par 1 représentent les deux entrées de la porte. L'un des arcs représente la valeur vraie s'il est dirigé vers le sommet, et faux sinon. L'arc bleu est pondéré par 2 et représente la sortie de la porte. Il est vrai s'il est sortant. La table suivante donne la table de vérité d'un ET et l'interprétation sur la porte ET dans un graphe contraint :
| x | arc rouge de x | y | arc rouge de y | x et y | arc bleu de (x et y) |
|---|---|---|---|---|---|
| 0 | sortant | 0 | sortant | 0 | forcément entrant pour satisfaire un flot entrant minimal de 2 |
| 0 | sortant | 1 | entrant | 0 | forcément entrant pour satisfaire un flot entrant minimal de 2 |
| 1 | entrant | 0 | sortant | 0 | forcément entrant pour satisfaire un flot entrant minimal de 2 |
| 1 | sortant | 1 | entrant | 1 | peut être sortant |
Simulation d'une porte OU modifier
Une porte OU est simulé par un sommet de flot entrant minimal égal à 2, mais avec trois arcs bleus pondérés par 2. Deux d'entre eux représentent les deux entrées de la porte. L'autre représente la sortie. De la même manière, un arc d'entrée est dirigé vers le sommet s'il est vraie, alors que l'arc de sortie représente le vrai s'il est sortant. La table suivante donne la table de vérité d'un OU et l'interprétation sur la porte OU dans un graphe contraint :
| x | arc bleu de x | y | arc bleu de y | x ou y | arc bleu de (x ou y) |
|---|---|---|---|---|---|
| 0 | sortant | 0 | sortant | 0 | forcément entrant pour satisfaire un flot entrant minimal de 2 |
| 0 | sortant | 1 | entrant | 1 | peut être sortant |
| 1 | entrant | 0 | sortant | 1 | peut être sortant |
| 1 | sortant | 1 | entrant | 1 | peut être sortant |
Lien entre jeu et complexité modifier
Le problème de satisfaction d'un graphe contraint, i.e. savoir si on peut orienter les arêtes d'un graphe non orienté avec des arcs de poids 1 ou 2 de façon à avoir un flot entrant de 2 en chaque sommet, est NP-complet. La démonstration donnée par Erik Demaine et Robert A. Hearn repose sur une réduction depuis 3SAT.
La table suivante donne les complexités de décider l'existence d'une stratégie gagnante : étant donné un graphe contraint, l'arc à inverser (ou les arcs à inverser) pour gagner, existe-t-il une stratégie gagnante pour que chaque joueur inverse son arc à inverser.
| 0 joueur (simulation) | 1 joueur (puzzle) | 2 joueurs | Équipes avec information imparfaite | |
|---|---|---|---|---|
| Non borné | PSPACE-complet | PSPACE-complet | EXPTIME-complet | RE (indécidable) |
| Borné | P-complet | NP-complet | PSPACE-complet | NEXPTIME-complet |
Le problème de l'existence d'une stratégie gagnante pour un joueur dans le cas borné est PSPACE-complet et se démontre depuis le problème TQBF, qui est le problème qui consiste à savoir si une formule booléenne quantifiée est vraie. La démonstration utilise des gadgets pour la formule CNF et pour les quantificateurs existentiels et universels[5],[4].
Le cas de plus de 2 joueurs donne les mêmes complexités que pour 2 joueurs[1] p. 85. Le dernier cas est différent et consiste à opposer deux équipes de joueurs. Mais les joueurs ont de l'information imparfaite comme dans les travaux de Peterson et Reif[6]. Aussi, dans la version bornée, on allège un peu l'hypothèse : on donne une borne k et chaque arc ne peut être retourner qu'au plus k fois ; la complexité dans le cas k=1 est un problème ouvert lorsque l'ouvrage[1] a été écrit.
On modifie donc la logique contrainte de la façon suivante Il y a N joueurs : 1, 2..., N. Il y a deux équipes : les blancs et les noirs. Chaque joueur appartient à une et une seule des deux équipes. Chaque joueur ne voit l'orientation que d'un sous-ensemble d'arcs. Les arcs contrôlés par un joueur sont vus par ce même joueur. Le jeu se déroule ainsi : chaque joueur joue à tour de rôle : 1, 2, ..., N. Chaque joueur inverse un arc contrôlé par lui, qui n'a pas été précédemment inversé ; de plus, il doit savoir que ce coup est légal, juste à partir de la connaissance de l'orientation des arcs vus par lui. L'équipe blanche (noire) gagne si l'un des joueurs blancs (noirs) inverse son arc gagnant. La démonstration de la NEXPTIME-dureté repose sur une variante des formules booléennes quantifiées : formules booléennes quantifiées avec dépendance.
De manière intéressante, les bornes inférieures des complexités sont les mêmes si on se restreint aux graphes planaires.
Références modifier
- (en) Robert Aubrey Hearn, Games, puzzles, and computation (thèse de doctorat), Massachusetts Institute of Technology, (lire en ligne).
- (en) Robert A. Hearn et Erik D. Demaine, « PSPACE-completeness of sliding-block puzzles and other problems through the nondeterministic constraint logic model of computation », Theoretical Computer Science, vol. 343, nos 1–2, , p. 72–96 (DOI 10.1016/j.tcs.2005.05.008, MR 2168845).
- (en) Tom C. van der Zanden, « 10th International Symposium on Parameterized and Exact Computation », LIPIcs. Leibniz Int. Proc. Inform., Schloss Dagstuhl. Leibniz-Zent. Inform., Wadern, vol. 43, , p. 282–293 (DOI 10.4230/LIPIcs.IPEC.2015.282, MR 3452428, arXiv 1509.02683).
- « Constraint graphs », sur people.irisa.fr (consulté le )
- Neil Gurram, « Non Deterministic Constraint Logic », sur Erik Demaine
- (en) Gary L. Peterson et John H. Reif, « Multiple-person alternation », dans Proceedings of the 20th Annual Symposium on Foundations of Computer Science, IEEE Computer Society, , 348–363 p. (DOI 10.1109/SFCS.1979.25, lire en ligne)
