Cette variation de TQBF est-elle toujours complète sur PSPACE?

Décider si une formule booléenne quantifiée telle que

$\forall x_1 \exists x_2 \forall x_3\cdots \exists x_n \varphi(x_1, x_2,\ldots , x_n),$

évalue toujours à true est un problème classique PSPACE-complete. Cela peut être considéré comme un jeu entre deux joueurs, avec des mouvements alternés. Le premier joueur décide de la valeur de vérité des variables impaires et le deuxième joueur décide de la valeur de vérité des variables paires. Le premier joueur essaie de rendre faux et le second joueur essaie de le rendre vrai. Décider qui a une stratégie gagnante est complet sur PSPACE.$\varphi$

J'envisage un problème similaire avec deux joueurs, l'un essayant de rendre une formule booléenne vraie et l'autre essayant de la rendre fausse. La différence est que lors d'un coup, un joueur peut choisir une variable et une valeur de vérité pour celle-ci (par exemple, comme le tout premier coup, le joueur un pourrait décider de mettre sur vrai, puis au coup suivant, le joueur deux pourrait décider pour définir sur false). Cela signifie que les joueurs peuvent décider laquelle des variables (parmi celles auxquelles aucune valeur de vérité n'a encore été attribuée) ils souhaitent attribuer une valeur de vérité, au lieu d'avoir à jouer au jeu dans l'ordre .$\varphi$$x_8$$x_3$$x_1 , \ldots , x_n$

Le problème reçoit une formule booléenne sur variables pour décider si le joueur un (essayant de le rendre faux) ou le joueur deux (essayant de le rendre vrai) a une stratégie gagnante. Ce problème est clairement encore dans PSPACE, car l'arbre de jeu a une profondeur linéaire.$\varphi$$n$

Reste-t-il PSPACE complet?

Il s'agit d'un jeu de satisfaction de contraintes non ordonné et il est PSPACE-complet et il a été prouvé que PSPACE-complet n'est que récent ; une preuve peut être trouvée dans:

Lauri Ahlroth et Pekka Orponen, Unordered Constraint Satisfaction Games . Notes de cours en informatique Volume 7464, 2012, pp 64-75.

Abstrait:Nous considérons des jeux de satisfaction de contraintes à deux joueurs sur des systèmes de contraintes booléennes, dans lesquels les joueurs choisissent à tour de rôle l'une des variables disponibles et la définissent sur vrai ou faux, dans le but de maximiser (pour le joueur I) ou de minimiser (pour le joueur II) le nombre de contraintes satisfaites. Contrairement aux jeux d'affectation de variables de type QBF standard, nous n'imposons aucun ordre dans lequel les variables doivent être jouées. Cela rend la configuration du jeu plus naturelle, mais aussi plus difficile à contrôler. Nous proposons des stratégies d'approximation à facteur constant en temps polynomial pour le joueur I lorsque les contraintes sont des fonctions de parité ou des fonctions de seuil avec un seuil qui est petit par rapport à l'arité des contraintes. De plus, nous prouvons que le problème de déterminer si Player I peut satisfaire toutes les contraintes est PSPACE-complete même dans ce paramètre non ordonné,

Du contenu:

...
Notre exemple générique d'un jeu de satisfaction de contraintes non ordonné est le jeu sur les formules booléennes ( GBF ). Une instance de ce jeu est donnée par un ensemble de m formules booléennes non constantes sur un ensemble commun de n variables . Nous appelons les formules de clauses même si nous n'exigeons généralement pas qu'elles soient des disjonctions. ... Un jeu sur déroule de sorte qu'à chaque tour le joueur à déplacer sélectionne une des variables précédemment non sélectionnées et lui assigne une valeur de vérité. Le joueur I démarre et le jeu se termine lorsque toutes les variables ont reçu une valeur. Dans la version décision de GBFX = { x 1 , . . . , x n } C $C = \{c_1,...,c_m\}$$X = \{x_1,...,x_n\}$$C$

$C$, la question est de savoir si la joueuse I a une stratégie de gain complète, grâce à laquelle elle peut satisfaire toutes les clauses, peu importe ce que fait la joueuse II. Dans le cas positif, nous disons que l'instance est GBF-satisfiable. ..

... Théorème 4 : Le problème de décider de la GBF-satisfiabilité d'une formule booléenne est PSPACE-complet.

EDIT : Daniel Grier a découvert que le résultat a également été réglé par Schaefer dans les années 70, voir sa réponse sur cette page pour la référence (et le voter :-). Schaefer a prouvé que le jeu est toujours PSPACE complet même s'il est limité aux formules CNF positives (c'est-à-dire les formules propositionnelles sous forme normale conjonctive dans lesquelles aucune variable négative ne se produit) avec au plus 11 variables dans chaque conjonction.

Il peut également être intéressant de noter que ce problème a également été résolu dans les années 70 par Thomas Schaefer dans  Complexité des problèmes de décision basés sur des jeux finis d'information parfaite à deux personnes . En fait, il prouve un résultat légèrement plus fort en ce que le langage reste PSPACE complet même lorsqu'il est limité aux formules CNF positives.

Nous avons prouvé que ce jeu est complet sur PSPACE pour les 5-CNF mais qu'il a un algorithme de temps linéaire pour les 2-CNF. Le meilleur résultat précédent était les 6-CNF d'Ahlroth et Orponen.

Vous pouvez trouver le document de conférence à ISAAC 2018 .

Mise à jour: 16 novembre 2019

Nous avons prouvé que le jeu est traitable pour les 3-CNF sous certaines restrictions sur les 3-CNF. Nous avons également radicalement conjecturé que ce jeu est également utilisable sans aucune restriction sur les 3-CNF. Vous pouvez trouver la version initiale à ECCC .