Tractable Unordered 3-CNF Games.

The classic TQBF problem can be viewed as a game in which two players alternate turns assigning truth values to a CNF formula’s variables in a prescribed order, and the winner is determined by whether the CNF gets satisfied. The complexity of deciding which player has a winning strategy in this game is well-understood: it is \(\textsf {NL}\)-complete for 2-CNFs and \(\textsf {PSPACE}\)-complete for 3-CNFs.