Schaefer's Boolean Formula Games

For a few years (okay, okay, like, 5 years) I've been working on a paper about boolean formula games.  These are games that include a formula involving some boolean variables.  A turn consists of either assigning a value to an unassigned variable or flipping the value of a variable (depending on the game).

The canonical problem in PSPACE is QBF, which can be phrased as the following game.  There is a boolean formula in terms of some variables x₀ through x_n-1.  The first player (named True) chooses a value for x₀, then the next player (False) chooses a value for x₁, then True assigns x₂, and so on.  Once all variables have been assigned, True wins if the formula has been made true, and False wins otherwise. 

A beautiful and classic paper of Thomas Schaefer defines a bunch of other games (mostly formula games) and shows that they are PSPACE-complete.  (He also shows that Snort and Node-Kayles are PSPACE-complete.)  I've recently updated my ruleset table to include Schaefer's games, and I'd like to add a guide here to translate between Schaefer's technical names and the ruleset names I'm using.  I'm hoping that this can be used as a helpful reference when browsing the paper.  (F used in my notes below refers to the type of formula.  Schaefer often defines separate games for CNF and DNF formulas; I've combined them for brevity.)

Unrestricted QBF:  This is the same game as QBF, except that players may choose any variable they want to assign (instead of needing to choose the next variable).  This is not listed as a game in Schaefer's work mostly because the next one (a special case) is instead.

Positive QBF:  (Schaefer: G_pos(POS F))  This is the same game as Unrestricted QBF, except that the formula must contain no negations.  It is a special case of Unrestricted QBF.

Partitioned Variables QBF: (Schaefer: G_%free(F))  This is the same game as Unrestricted QBF, except that the variables are partitioned in half into two groups, one for each player.  On your turn, you choose any unassigned variable in your partition and assigns a value to it.

Positive Avoid True (Schaefer: G_avoid(POS F))  Similar to Positive QBF, except that all variables are initialized to false and players take turns choosing a variable to flip to true.  The first player to cause the entire formula to be a tautology loses.  Played on positive formulas to enforce that the game will end.

Partitioned Positive Avoid True (Schaefer: G_%avoid(POS F))  Just like Positive Avoid True, except that (as in Partitioned Variables QBF) the variables are partitioned into two equal sets ahead of time.  Each player must choose from their set on their turn.

Positive Seek True (Schaefer: G_seek(POS F))  The same as Positive Avoid True, except that the first player to cause the formula to be a tautology wins.

Partitioned Positive Seek True (Schaefer: G_%seek(POS F))  Just like Partitioned Positive Avoid True, except the first player to cause the formula to be a tautology wins.

These are very useful games to start with to show PSPACE-hardness of other games.  In my table, I've listed which versions of these games are known to be hard, so that the appropriate cases can be covered (if necessary).