The monotone formula game

A Neighborhood of Infinity just posted about an interesting abstract game (modeling games such as hex in which it is never harmful to make a move) in which one is given a monotone Boolean formula and two players, True and False, take turns to set values of the variables of the formula in an attempt to make the formula's overall value match their names.

Lacking a blogger account to leave a comment, or other contact information, I thought I'd post here a partial answer to one of his questions:

Is there a nice way to evaluate any position in the game?

It turns out to be at least NP-hard, although PSPACE-completeness seems a more likely final classification. To prove NP-hardness, transform any 3-SAT formula to a monotone formula by replacing each negated variable \( \lnot v_i \) by a new variable \( u_i \); then take the disjunction of this modified formula with \( n \) terms of the form \( ( v_i \wedge u_i ) \). If True plays first, then she can win if and only if the original 3-SAT formula is satisfied: we can assume without loss of generality that False's strategy is always to answer setting \( v_i={} \)True by setting \( u_i={} \)False and vice versa (otherwise True could win next turn by setting both \( v_i \) and \( u_i \) to True), so for this formula any strategy for True amounts to a truth assignment for the original 3-SAT formula's variables, QED.

ETA 2 Dec: It does in fact turn out to be PSPACE-complete.

To see this, we reduce from the known PSPACE-complete problem of evaluating quantified Boolean formulas: that is, formulas of the form \[ \exists v_1 \forall v_2 \exists v_3 \dots p(v_1,v_2,v_3,\dots). \] To translate a quantified formula into a monotone formula, perform the following steps:

1. Use De Morgan's rule to transform the predicate \( p \) into a formula in which the \( \lnot \) operation applies only to variables and not to more complex subformulas.

2. Replace every subexpression \( \lnot v_i \) with a variable \( u_i \), as in the NP-hardness proof, resulting in a monotone predicate \( p^*(v_1,u_1,v_2,u_2,\dots) \)

3. Create new variables \( x_i \) for each pair of \( v_i \) and \( u_i \).

4. Form the overall monotone formula \[ \begin{align} \biggl( (&v_1\vee u_1)\wedge (v_1\vee x_1)\wedge (u_1\vee x_1) \wedge{} \\ \Bigl(& (v_2\wedge u_2) \vee (v_2\wedge x_2) \vee (u_2\vee x_2) \vee{} \\ &\bigl( (v_3\vee u_3)\wedge (v_3\vee x_3)\wedge (v_3\vee x_3) \wedge{} \\ &\dots p^* \bigr) \Bigr) \biggr) \\ \end{align} \]

I claim that the resulting game is won by T, moving first, if and only if the quantified Boolean formula is true. This follows by induction on the number of quantifiers from the following:

Lemma: the overall game is equivalent to one in which T chooses exactly one of \( v_1 \) or \( u_1 \) to be true, followed by a game in which F moves first in the subformula

\[ \bigl((v_2\vee u_2)\wedge (v_2\vee x_2)\wedge (u_2\vee x_2)\wedge\dots p^*)\bigr). \]

Proof: T can cause the game to have this value by the following strategy: first move in \( v_1 \) or \( u_1 \), then play in the subformula until F moves in \( v_1 \), \( u_1 \), or \( x_1 \), at which point T immediately responds at the third of these variables. F can cause the game to have this value or better by the following strategy: first, if T avoids playing in \( v_1 \), \( u_1 \), or \( x_1 \), then F can play in \( x_1 \) and win next turn. If T plays in \( x_1 \), F can play in one of \( v_1 \) or \( u_1 \), forcing T to respond in the other one, and F rather than T has usurped the choice of \( v_1 \)'s value. Finally, if T plays in \( v_1 \) or \( u_1 \), F plays in the other one, forcing T to respond in \( x_1 \) and achieving the stated game value. Since both T and F can force the game to have the same value, that is the overall value of the game, QED.

---

Comments: