0xDE (11011110) wrote,

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 ~vi by a new variable ui; then take the disjunction of this modified formula with n terms of the form (vi and ui). 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 vi=True by setting ui=False and vice versa (otherwise True could win next turn by setting both vi and ui 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 v1)(all v2)(exists v3)...p(v1,v2,v3,...). 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 not operation applies only to variables and not to more complex subformulas.
2. Replace every subexpression not(vi) with a variable ui, as in the NP-hardness proof, resulting in a monotone predicate p*(v1,u1,v2,u2,...)
3. Create new variables xi for each pair of vi and ui.
4. Form the overall monotone formula ((v1 or u1) and (v1 or x1) and (u1 or x1) and ((v2 and u2) or (v2 and x2) or (u2 and x2) or ((v3 or u3) and (v3 or x3) and (u3 or x3) and ... p*)))

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 v1 or u1 to be true, followed by a game in which F moves first in the subformula ((v2 and u2) or (v2 and x2) or (u2 and x2) or ((v3 or u3) and (v3 or x3) and (u3 or x3) and ... p*)).

Proof: T can cause the game to have this value by the following strategy: first move in v1 or u1, then play in the subformula until F moves in v1, u1, or x1, 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 v1, u1, or x1, then F can play in x1 and win next turn. If T plays in x1, F can play in one of v1 or u1, forcing T to respond in the other one, and F rather than T has usurped the choice of v1's value. Finally, if T plays in v1 or u1, F plays in the other one, forcing T to respond in x1 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.
Tags: abstract games, complexity theory
  • Post a new comment


    default userpic

    Your reply will be screened

    Your IP address will be recorded