Is this variation of TQBF still PSPACE-complete?

Question

Deciding if a quantified boolean formula such as

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

always evaluates to true is a classical PSPACE-complete problem. This can be viewed as a game between two players, with alternating moves. The first player decides the truth value of the odd-numbered variables and the second player decides the truth value of the even-numbered variables. The first player tries to make $\varphi$ false and the second player tries to make it true. Deciding who has a winning strategy is PSPACE-complete.

I am considering a similar problem with two players, one trying to make a boolean formula $\varphi$ true and the other trying to make it false. The difference is that on a move, a player can choose a variable and a truth value for it (for example, as the very first move, player one might decide to set $x_8$ to true and then in the next move, player two might decide to set $x_3$ to false). This means that the players can decide which of the variables (of those that have not yet been assigned a truth value) they want to assign a truth value, instead of having to play the game in the order $x_1 , \ldots , x_n$.

The problem is given a boolean formula $\varphi$ on $n$ variables to decide if player one (trying to make it false) or player two (trying to make it true) has a winning strategy. This problem is clearly still in PSPACE, since the game tree has linear depth.

Does it remain PSPACE complete?

Answer 1

It is an Unordered Constraint Satisfaction game and it is PSPACE-complete and it has been proved to be PSPACE-complete only recently; a proof can be found in:

Lauri Ahlroth and Pekka Orponen, Unordered Constraint Satisfaction Games. Lecture Notes in Computer Science Volume 7464, 2012, pp 64-75.

Abstract: We consider two-player constraint satisfaction games on systems of Boolean constraints, in which the players take turns in selecting one of the available variables and setting it to true or false, with the goal of maximising (for Player I) or minimising (for Player II) the number of satisfied constraints. Unlike in standard QBF-type variable assignment games, we impose no order in which the variables are to be played. This makes the game setup more natural, but also more challenging to control. We provide polynomial-time, constant-factor approximation strategies for Player I when the constraints are parity functions or threshold functions with a threshold that is small compared to the arity of the constraints. Also, we prove that the problem of determining if Player I can satisfy all constraints is PSPACE-complete even in this unordered setting, and when the constraints are disjunctions of at most 6 literals (an unordered-game analogue of 6-QBF).

From the content:

...
Our generic example of an unordered constraint satisfaction game is the Game on Boolean Formulas (GBF). An instance of this game is given by a set of m non-constant Boolean formulas $C = \{c_1,...,c_m\}$ over a common set of n variables $X = \{x_1,...,x_n\}$. We refer to the formulas in $C$ as clauses even though we do not in general require them to be disjunctions.
...
A game on $C$ proceeds so that on each turn the player to move selects one of the previously nonselected variables and assigns a truth value to it. Player I starts, and the game ends when all variables have been assigned a value. In the decision version of GBF, the question is whether Player I has a comprehensive winning strategy, by which she can make all clauses satisfied no matter what Player II does. In the positive case we say that the instance is GBF-satisfiable. ..

... Theorem 4: The problem of deciding GBF-satisfiability of a Boolean formula is PSPACE-complete.

EDIT: Daniel Grier's has found out that the result was also settled by Schaefer in the '70s, see his answer on this page for the reference (and upvote it :-). Schaefer proved that the game is still PSPACE-complete even if restricted to positive CNF formulas (i.e. propositional formulas in conjunctive normal form in which no negated variables occur) with at most 11 variables in each conjunction.

Answer 2

It may also be worthwhile to note that this problem was also solved in the 70's by Thomas Schaefer in Complexity of decision problems based on finite two-person perfect-information games. In fact, he proves a slightly stronger result in that the language remains PSPACE-complete even when restricted to positive CNF formulas.

Answer 3

We proved that this game is PSPACE-complete for 5-CNFs but has Linear Time algorithm for 2-CNFs. The previous best result was Ahlroth and Orponen's 6-CNFs.

You can find the conference paper at ISAAC 2018.

**Update: Nov, 16, 2019

We proved that the game is tractable for 3-CNFs under some restrictions on 3-CNFs. We also radically conjectured that this game is also tractable under no restrictions on 3-CNFs. You can find the initial version at ECCC.

**Update July, 9, 2020

We have proved the game remains PSPACE-Complete even if it is a positive 6-CNF. This is an improvement over Thomas Schaefer's result in the STOC 1978 paper where he proved the game is PSPACE-complete for positive 11-CNF. You can find the draft at ECCC.