Formalisation of the game Havannah

by Frans Faase

Introduction

This pages gives a formal definition of the rules of the game Havannah, which was invented by Christian Freeling. (Havannah on Wikipedia). It is a connection game in the class of symmetrical board games with complete information. Despite its simple rules, it is a game with unexpected depth. The combination of strong strategical element, and yet rather simple rules, make the game into a good candidate for a test case in game playing theory.

Note: Christian has put a reward of 1000 euros for making a program for the game of Havannah, that can beat him 1 out of 10 (!) games within the next ten years. If you want to rise to the challenge, please contact Abstract Games Magazine.

Description of the game

The game is played on a hexagonal board, with either 8 or 10 points on each side. By drawing lines parallel to the sides and between the points on the sides the board is filled with triangles. The points on the sides and the intersection points of the lines together constitute the positions where the stones can be placed. The size of the board determines the difficulty of the game.

In turn, the players place a stone of their colour on one of the unoccupied positions. Once a stone has been placed on the board, it remains there until the end of the game. This means that stones cannot be moved or beaten. For that matter the game can also played with paper and (coloured) pencils. See this PostScript file or this PDF for a board where the positions are represented by circles. Or this PDF with six boards on one page.

The aim of the game is to make a wining figure. The first player to make a wining figure wins the game. Each wining figure consists of a chain of stones. There are three kinds of wining figures: bridges, forks, and cycles. The requirements for these are:

Representation of the board

The first step in the formal definition of the game is the representation of the board. Let size be the size of the board. It is equal to 8 or 10.

Definition of points

The set of points on the board can be defined using: 
df  points
    =  { (x,y,z) in {1-size,..,size-1}3
       | x + y + z = 0
       }
In this definition we start with a cube of points and take the points that are on the intersection of a plane, that goes right through the middle of six of the ribs, creating the desired hexagonal set of points.

The coordinates with which the points are defined have a degree of freedom of only two. This means that each of the elements can always be calculated if the other two are known.

Definition of distance

We can define the distance between two points as the length of the shortest path between the points. We can do so using: 
df  distance((x1,y1,z1) in points, (x2,y2,z2) in points)
    = ( |x1-x2| + |y1-y2| + |z1-z2| )/2
The sum of absolute differences of the coordinates is always even, because the degree of freedom is two. The points with the same distance to a given point are on the imaginary hexagon of which the corners are on the lines through this point and on the given distance.

Definition of neigbour

With this definition it is also possible to define the neighbour relation: 
df  neighbour
    = { (p,q) in points2
      | distance(p,q) = 1
      }

Definition of neighbours_of

And a function that returns all neighbours of a point: 
df  neighbours_of(p in points)
    = { q  in points
      | (p,q) in neighbour
      }

Definition of corner_points and side_points

The points on the board can be divided into different kinds. Two of these kinds are the corner and side points. These we can define using: 
df  corner_points
    =  { p in points
       | count(neighbours_of(p)) = 3
       }

df  side_points
    =  { p in points
       | count(neighbours_of(p)) = 4
       }
With this definition we have established the board and some of its properties.

Groups

Connected groups of stones play an important role in the game. For this reason we give some definitions concerning groups based on the neighbour relation.

Definition of positions

First we define the set of all subsets of points, which we call positions: 
df  positions = powerset(points)

Definition of connected_in

Next we define a function that returns all pairs of points that are connected in a given subset of points: 
df  connected_in(Q in positions)
    = (neighbour intersection Q2)*
In this * stands for the transitive closure of a relation.

Definition of connected_within

Using this we can define a function that returns a set of points that are connected with a point in a given subset of all points: 
df  connected_within(a in Q, Q in positions)
    = { b in Q
      | (a,b) in connected_in(Q)
      }

Definition of groups

A group is subset of points in which all points are connected with each other. The following defines the set of all groups: 
df  groups
    = { group in positions
      | Forall  a,b in group  ((a,b) in connected_in(group))
      }

Wining figures

In this section we define the collection of all wining groups.

Definition of bridges

We start with the simplest winning figure, the bridge, which connects two corner points. The set of all positions that contain a bridge is defined by: 
df  bridges
    = { position in positions
      | Exists group in groups
          (    group subset position
           and count( position intersection corner_points ) = 2
          )
      }

Definition of forks

Next we look at the forks, which a groups of connected points that touch on three different sides. The definition of the set of all positions that contain a fork: 
df  forks
    = { position in positions
      | Exists group in groups
          (    group subset position
           and count({ connected_within(s, side_points)
                     | s in (position intersection side_points)
                     }) = 3
          )
      }

Definition of cycles

Finanlly, we look at the cycles. The definition of the set of all positions that contain a cycle: 
df  cycles
    = { position in positions
      | Exists  n>1, (p0,..,pn-1) in positionn
          (Forall  1<=i<n
             (    distance(pi,p(i+1) mod n) = 1
              and distance(pi,p(i+2) mod n) >= 2
             )
          )
      }
It is not obvious that this definition is sufficient and complete. If there exists a cycle in a group encircling at least one point, it is possible to create a cycle without sharp angles and still encircling at least one point. A sharp angle consists of three successive points in the chain that are all neighbours of each other. The middle of these points can be removed out of the chain, without disconnecting it. By repeating this process of removing sharp angles in the chain we get a chain that fits the given definition.

The other way around is that we have to prove that the cycles defined with this definition do enclose at least one point. If we show that the cycles which are defined by this definition do at least have six points, it is easy to see that these cycles do enclose at least one point. We show that the cycle must at least have six points by stating the following: 

Forall (p0,..,pn-1) in pointsn
   (Forall  1<=i<n
       (    distance(pi,p(i+1) mod n) = 1
        and distance(pi,p(i+2) mod n) >= 2
       )
    => Forall  1<=i<n
          (    distance(pi,p(i+3) mod n) >= 2
           and distance(pi,p(i+4) mod n) >= 2
           and distance(pi,p(i+5) mod n) >= 1
           and distance(pi,p(i+6) mod n) >= 0
          )
   )

Definitiom of wining and nonwining

Now we can define the collection of all wining and non-wining positions: 
df  wining = cycles union bridges union forks

df  nonwining = positions - wining

Definitiom of minimal_wining

Using the above we could also define all minimal wining figures, of which any true subset is not a wining collection: 
df  minimal_wining
    = { win in wining
      | Forall s propersubset win (s in nonwining)
      }

Havannah games

With all of the above, we can give the formalization of Havannah games.

Definition of game_board_positions

A board position can simply be defined as a pair of two disjoint subset of points. Because players take turns placing stones, and because stones are never removed, the number of stones of board postions that can occur in games are such that the number of stones are either the same or that the first player has one more than the second player. Also a game ends when one of the players has reached a wining position, which is a minimal wining position. 
df  game_board_positions
    = { (a,b) in (nonwining union minimal_wining)2
      |     a union b = {}
        and (count(a) = count(b) or count(a) = count(b) + 1)
        and not(a in minimal_wining and b in minimal_wining)
      }

Definition of valid_proceedings

For a given board position we can define a set of board positions as the result of a valid move: 
df  valid_proceedings((a,b) in game_board_positions)
    = { (c,d) in game_board_positions
      |     a subset c and b subset d
      	and count(c) + count(d) = count(a) + count(b) + 1
      }

Definition of Havannah_games

Now we can define the set of all games as sequences of board positions, where the first position is the empty board and the last position does not have any valid proceedings. 
df  Havannah_games
    = { (p0, .., pn) in game_board_positionsn
      |     p0 = ({},{})
        and Forall 0<i<=n (pi in valid_proceedings(pi-1)
        and valid_proceedings(pn) = {}
      }

Playing games

Although the previous section defines the set of all legal Havannah games, we could still continue with formalizing how a game is played between two players.

Definition of players

A player is defined as a mapping of all game board positions to a proceeding game board position that would represent the move that the player would make in the given situation. The set of all possible different players is defined by: 
df  players
    = { { (p, q) in game_board_positions2
        | q in valid_proceedings(p)
        }
      }

Definition of played_game

Given two players from the set of players, we can define the game that they would have played together. This is defined by the following function: 
df  played_game(player0 in players, player1 in players)
    = (p0, .., pn) in Havannah_games
      where Forall 0<=i<n ((pi, pi+1) in playeri mod 2)

Definition of outcome

Given a game, we can define the outcome as one of -1, 0, or 1 depending on whether the first player won or lost. 
df  outcome((p0, .., pn-1, (a, b)) in games)
    = if a in wining
      then 1
      elif b in wining
      then -1
      else 0
      fi

Definition of super_Havannah_players

Finally, we define the set of super Havannah player. These are players that never lose from any other player (except themselves). 
df super_Havannah_players
     = { player in players
       | Forall q in players - {p}
            (    outcome(played_game(p,q)) >= 0
             and outcome(played_game(q,p)) >= 0)
       }
How many such super Havannah players exist, is unknown. We could also define the set of players that always lose. But than we are actually defining another type of game.

home and email