<p>It may also be worthwhile to note that this problem was also solved in the 70's by Thomas Schaefer in ￼<a href="http://dl.acm.org/citation.cfm?id=803629">Complexity of decision problems based on finite two-person perfect-information games</a>.  In fact, he proves a slightly stronger result in that the language remains PSPACE-complete even when restricted to positive CNF formulas.</p>

CC BY-SA 3.0
2014-09-05T15:46:19.493Z
Interesting! (Ahlroth and Orponen didn't know it? BTW they cite another paper of Schaefer: On the complexity of some two-person perfect-information games (1978) which contains the well known PSPACE completeness results of Geography and Node-Kayles).  Is there a free copy of the paper available? (the linked one is beyond paywall).
Marzio De Biasi
CC BY-SA 3.0
2014-09-05T15:57:16.000Z
Unfortunately, I don't think so.  I remember once trying to find a copy that was not behind a paywall for some time with little success.
Daniel Grier
CC BY-SA 3.0
2014-09-05T16:02:34.357Z
BTW congratulations for your nice result on PSPACE-completeness of Poset Games!
Marzio De Biasi
CC BY-SA 3.0
2014-09-09T21:05:11.720Z
As far as I can tell, the 1978 paper (On the complexity of some two-person...) is the journal version of the 1976 STOC paper (Complexity of decision problems...), which it cites.
András Salamon
CC BY-SA 3.0
2014-09-05T15:24:53.350Z
2014-09-05T15:24:53.350Z
Daniel Grier
<p>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.</p>
<p>You can find the conference paper at <a href="http://drops.dagstuhl.de/opus/volltexte/2018/9957/pdf/LIPIcs-ISAAC-2018-9.pdf" rel="nofollow noreferrer">ISAAC 2018</a>.</p>
<p>**Update: Nov, 16, 2019</p>
<p>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 <a href="https://eccc.weizmann.ac.il/report/2019/160/" rel="nofollow noreferrer">ECCC</a>.</p>
<p>**Update July, 9, 2020</p>
<p>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 <a href="https://eccc.weizmann.ac.il/report/2020/097/" rel="nofollow noreferrer">ECCC</a>.</p>

CC BY-SA 4.0
2018-02-24T01:28:03.637Z
2020-07-09T14:04:22.887Z
2020-07-09T14:04:22.887Z
Lutfar Rahman Milu
<p>It is an <strong>Unordered Constraint Satisfaction game</strong> and it is PSPACE-complete <strike>and it has been proved to be PSPACE-complete only recently</strike>;
a proof can be found in: </p>

<p>Lauri Ahlroth and Pekka Orponen, <a href="http://users.ics.aalto.fi/orponen/papers/csg.pdf" rel="noreferrer">Unordered Constraint Satisfaction Games</a>.
Lecture Notes in Computer Science Volume 7464, 2012, pp 64-75.</p>

<p><strong>Abstract:</strong> 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).</p>

<p>From the content:</p>

<p>...<br>
Our generic example of an unordered constraint satisfaction game is the <em>Game on
Boolean Formulas</em> (<strong>GBF</strong>). 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.<br>
...<br>
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 <strong>GBF</strong>, 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 <strong>GBF-satisfiable.</strong> ..</p>

<p>...
<strong>Theorem 4</strong>: The problem of deciding <em>GBF-satisfiability</em> of a Boolean formula is PSPACE-complete.</p>

<p><strong>EDIT</strong>: Daniel Grier's has found out that the result was also settled by Schaefer in the '70s, see <a href="https://cstheory.stackexchange.com/questions/25671/is-this-variation-of-tqbf-still-pspace-complete#25686">his answer on this page</a> for the reference (and upvote it :-). Schaefer proved that the game is still PSPACE-complete even if restricted to <em>positive CNF formulas</em> (i.e. propositional formulas in conjunctive normal form in which no negated variables occur) with at most 11 variables in each conjunction.</p>

CC BY-SA 3.0
2014-09-03T18:17:34.720Z
2014-09-05T18:01:31.557Z
2017-04-13T12:32:28.080Z
Marzio De Biasi
<p>Deciding if a quantified boolean formula such as</p>

<p><span class="math-container">$\forall x_1 \exists x_2 \forall x_3\cdots \exists x_n \varphi(x_1, x_2,\ldots , x_n),$</span></p>

<p>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 <span class="math-container">$\varphi$</span> false and the second player tries to make it true. Deciding who has a winning strategy is PSPACE-complete.</p>

<p>I am considering a similar problem with two players, one trying to make a boolean formula <span class="math-container">$\varphi$</span> 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 <span class="math-container">$x_8$</span> to true and then in the next move, player two might decide to set <span class="math-container">$x_3$</span> 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 <span class="math-container">$x_1 , \ldots , x_n$</span>. </p>

<p>The problem is given a boolean formula <span class="math-container">$\varphi$</span>  on <span class="math-container">$n$</span> 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.</p>

<p>Does it remain PSPACE complete?</p>

<cc.complexity-theory><sat><gt.game-theory><pspace>
Is this variation of TQBF still PSPACE-complete?
JWM
# Is this variation of TQBF still PSPACE-complete?

(Asked by: username_0 on 2014-09-03)

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?

**Tags:** cc.complexity-theory, sat, gt.game-theory, pspace

---

## 3 answers

### Answer by username_2 on 2014-09-03. Score: 37 | Accepted answer

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](http://users.ics.aalto.fi/orponen/papers/csg.pdf).
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](https://cstheory.stackexchange.com/questions/25671/is-this-variation-of-tqbf-still-pspace-complete#25686) 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 by username_1 on 2014-09-05. Score: 29

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](http://dl.acm.org/citation.cfm?id=803629). In fact, he proves a slightly stronger result in that the language remains PSPACE-complete even when restricted to positive CNF formulas.

> **Comments:**
> **username_2**: Interesting! (Ahlroth and Orponen didn't know it? BTW they cite another paper of Schaefer: On the complexity of some two-person perfect-information games (1978) which contains the well known PSPACE completeness results of Geography and Node-Kayles).  Is there a free copy of the paper available? (the linked one is beyond paywall).  
> **username_1**: Unfortunately, I don't think so.  I remember once trying to find a copy that was not behind a paywall for some time with little success.  
> **username_2**: BTW congratulations for your nice result on PSPACE-completeness of Poset Games!  
> **username_3**: As far as I can tell, the 1978 paper (On the complexity of some two-person...) is the journal version of the 1976 STOC paper (Complexity of decision problems...), which it cites.  

---

### Answer by username_4 on 2018-02-24. Score: 13

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](http://drops.dagstuhl.de/opus/volltexte/2018/9957/pdf/LIPIcs-ISAAC-2018-9.pdf).

\*\*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](https://eccc.weizmann.ac.il/report/2019/160/).

\*\*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](https://eccc.weizmann.ac.il/report/2020/097/).


---

