Hex as a boolean formula

Did anyone notice that Hex can be considered as a game on a boolean formula?

For example in 2x2 Hex we have the formula:

( A1 and A2 ) or ( B1 and A2 ) or ( B1 and B2 )

Players take turn setting variables to 0 or 1. In this example red plays 1 and blue plays 0. Red wins if the formula reduces to 1 and blue wins if it reduces to 0.

With optimal play, it must be possible to simplify and reduce such formulas to either 0 or 1.

The above formula could be rewritten as:

not( ( A1 and B1 ) or ( B1 and A2 ) or ( A2 and B2 ) )

which is basically the point of view of blue instead of red.

But we also know that somehow this must reduce to:

( B1 or A2 )

and this in turn to 1.

It is not difficult to prove that Hex of any size can be reduced to a game on a boolean formula. Question is then, is it possible to build a theory how to reduce and prove such formulas?

Has there been any research on games on boolean formulas? Hex is just a special case of this type of game, and many other connection games seems to fall into the same category.

Yes you are right that the game can be expressed with boolean formulas, but you just write down every possible path, this soon gonna explode.

Unfortunately the formula doesn't reduce to (B1 or A2), you can see that if only one of those is true then the formula on top is false, your formula becomes true when a winning path is formed, before that happens it is always false.

On the other hand the 2nd formula is always true until player 1 formed a winning path. Btw the formula can be rewritten as: (not(A1) or not(B1)) and (not(B1) or not(A2)) and (not(A2) or not(B2))

You actually have 3 values, you could express your reduction the following way, then it would be correct (for correct play):

(B1(player1) and A2(empty) and B2(empty)) or (A2(player1) and A1(empty) and B1(empty))

So you can basically express anything with logic.

Of course there are some quantifiers missing in my formulas for them to be strictly correct. Specifically player 1 is at turn, otherwise we could not reduce it to (B1 or A2) or indeed to 1.

If player 0 would be at turn, we could instead reduce it to (B1 and A2) or equivalent to not( B1 or A2 ) and this in turn would get reduced to 0.

Keep in mind when I make these reductions I'm not using only logical reductions but rather I use the optimal play criteria which somehow must be expressed with universal and existential quantifiers.

Maraca is right, you can express only the "winning condition" using boolean (propositional) logic. You can express the "winning position" concept with first order logic. The "first player is winning in an empty 2x2 board" concept can be expressed in logic in this way: it_exists move_1, for_each move_2, it_exists move_3, for_each move_4, ( ( A1(move_1) or A1(move_3) ) and ( A2 (move_1) or A2 (move_3) ) ) or ( ( B1 (move_1) or B1 (move_3) ) and ( A2 (move_1) or A2 (move_3) ) ) or ( ( B1 (move_1) or B1 (move_3) ) and ( B2 (move_1) or B2 (move_3) ) ). Very readable, isn't it? :D heh

Oh, and there are other conditions to add obviously. For each cell we've to add the condition that it can't be played two times. For example A1(move_1) and A1(move_2) can't be both be true and so "not ( A1(move_1) and A1(move_2) )"..

compare to this:

The game of Hex: The hierarchical approach, by Vadim Anshelevich

I would like to correct my first claim about propositional logic. It can be used to express the "winning position" concept too, for finite boards at least, but almost surely at the cost of a formula of exponential lenght. The "winning condition" instead is obviously computable using a polynomial boolean formula, even if nobody has written that formula here. First order logic allows one to use the "winning condition" boolean formula to express the "winning position" concept but at the cost of quantifiers (and when you eliminate them, you get again an exponential mess).

I mean, nobody has written here how to compute the "winning condition" on a NxN board, using only a decent number of and/or/not. 2x2 is too trivial.. :)

Ring von Fehler, if you're interested i've some games were the "incompleteness" of and-or rules doesn't allow one to prove the win.. hex is tricky.. :)

Hex is PSPACE-complete

(the decision problem: is a given position a first-player win).

( reference)

So it is highly unlikely that it would be in P (polynomial-size

first order formula), or in NP (polynomial-size formula

with existentially quantified variables).

Still, I like to think that one *should* try to apply SAT solvers

to games (well, perhaps endgames). Could be used to guess-and-verify

a winning line. Looking at most life-and-death problems (in Go books),

the answer is no a tree, but path (since any deviation is "obviously" inferior).

Ring, you confuse propositional logic with first order logic. A first order formula can have quantifiers, isn't it? Just a note on terminology.

Right. In my statement, read "P-size propositional formula" (both instances).