Note: In 2002, 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. He lost this bet.
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 winning figure. The first player to make a winning figure wins the game. Each winning figure consists of a chain of stones. There are three kinds of winning figures: bridges, forks, and cycles. The requirements for these are:
Since the first player to move in Havannah has a distinct advantage, the pie rule is generally implemented for fairness. This rule allows the second player to choose whether to switch positions with the first player after the first player makes the first move. The pie rule is not included in the following formalisation.
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.
(This definition is used directly in the definition of distance, neigbour, neighbours_of, corner_points, and side_points below.)
df distance((x1,y1,z1) in points, (x2,y2,z2) in points) = ( |x1-x2| + |y1-y2| + |z1-z2| )/2The 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.
(This definition is used directly in the definition of neigbour and cycles below.)
df neighbour = { (p,q) in points2 | distance(p,q) = 1 }
(This definition is used directly in the definition of neigbour and cycles below.)
df neighbours_of(p in points) = { q in points | (p,q) in neighbour }
(This definition is used directly in the definition of cornerside_points and side_points below.)
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.
df positions = powerset(points)
df connected_in(Q in positions) = (neighbour intersection Q2)*In this * stands for the transitive closure of a relation.
df connected_within(a in Q, Q in positions) = { b in Q | (a,b) in connected_in(Q) }
df groups = { group in positions | Forall a,b in group ((a,b) in connected_in(group)) }
df bridges = { position in positions | Exists group in groups ( group subset position and count( position intersection corner_points ) = 2 ) }
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 ) }
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 ) )
df winning = cycles union bridges union forks
df game_board_positions = { (a,b) in positions2 | a intersection b = {} and (count(a) = count(b) or count(a) = count(b) + 1) and not(a in winning and b in winning) }Furthermore, we have to define intermediate board positions, which do not contain a winning position for both players:
df intermediate_game_board_positions = { (a,b) in game_board_positions | not(a in winning) and not(b in winning) }
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 }
df Havannah_games = { (p0, .., pn) in game_board_positionsn | p0 = ({},{}) and Forall 0<=i<n (pi in intermediate_game_board_positions) and Forall 0<i<=n (pi in valid_proceedings(pi-1) and ( pn in (game_board_positions - intermediate_game_board_positions) or valid_proceedings(game, pn) = {}) }
df players = { player = { (p, q) in game_board_positions2 | q in valid_proceedings(p) } | Forall p in {p | (p,q) in player} count({q | (p,q) in player}) <= 1) }
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)
df outcome((p0, .., pn-1, (a, b)) in games) = if a in winning then 1 elif b in winning then -1 else 0 fi
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.