Connect 4 Game Engine
Chess engines mathematically predict how long it will take for a player to win a game, or the likelihood of a player winning at all. This project does the same thing for Connect 4.
Solved mode
The AI was trained on 67,557 unique and legal positions at move 4, meaning both players have played four moves each. Each position is labeled with the game-theoretic outcome of win, loss or tie. The positions are restricted to those in which neither player has won and neither has a forcing move on the next play (three in a row and similar positions). The dataset came from work by John Tromp, tromp.github.io.
Sidenote: simple html pages like the one linked above are extremely optimized for browsers that expect thousands of lines of JavaScript.
Connect 4 is a solved game: a first player who plays optimally wins 100% of the time. Most people do not.
Formal methods
There is also a TLA+ specification for Connect 4, shrunk to a checkable size. A full 7 by 6 board is far too large to check on a Mac Mini.
SPECIFICATION Spec
CONSTANTS
BoardWidth = 4
BoardHeight = 4
WinningLength = 3
PROPERTY Termination
INVARIANT TypeOK
% To check the CorrectWinner invariant:
% INVARIANT CorrectWinner
------------------- MODULE Connect4 -------------------
EXTENDS Integers, FiniteSets, Sequences, TLC
CONSTANTS BoardWidth, BoardHeight, WinningLength
ASSUME BoardWidth \in Nat \land BoardHeight \in Nat \land WinningLength \in Nat
Players == {"red", "yellow"}
Board == 1..(BoardWidth*BoardHeight)
Empty == "empty"
(* --fair means that if a move is continuously enabled, it will eventually be taken *)
Fairness == \A col \in 1..BoardWidth : WF_vars(board, player, \A row \in 1..BoardHeight : board[row][col] /= Empty)
VARIABLES
board, (* The game board *)
player, (* The current player *)
winner (* The winner of the game, or "none" *)
vars == <<board, player, winner>>
-----------------------------------------------------------------------------
Init ==
/\ board = [row \in 1..BoardHeight |-> [col \in 1..BoardWidth |-> Empty]]
/\ player \in Players
/\ winner = "none"
-----------------------------------------------------------------------------
(* Helper function to check for a win *)
HasWinningLine(b, p, r, c) ==
LET
HorizontalCheck == \E i \in 0..(WinningLength-1) : c+i <= BoardWidth /\ (\forall j \in 0..(WinningLength-1) : b[r][c+i-j] = p)
VerticalCheck == \E i \in 0..(WinningLength-1) : r+i <= BoardHeight /\ (\forall j \in 0..(WinningLength-1) : b[r+i-j][c] = p)
DiagDescCheck == \E i \in 0..(WinningLength-1) : r+i <= BoardHeight /\ c+i <= BoardWidth /\ (\forall j \in 0..(WinningLength-1) : b[r+i-j][c+i-j] = p)
DiagAscCheck == \E i \in 0..(WinningLength-1) : r-i >= 1 /\ c+i <= BoardWidth /\ (\forall j \in 0..(WinningLength-1) : b[r-i+j][c+i-j] = p)
IN HorizontalCheck \/ VerticalCheck \/ DiagDescCheck \/ DiagAscCheck
Winner(b) ==
CHOOSE p \in Players : \E r \in 1..BoardHeight, c \in 1..BoardWidth : HasWinningLine(b, p, r, c)
-----------------------------------------------------------------------------
(* An action that represents a player making a move *)
Move(col) ==
/\ winner = "none"
/\ \E row \in 1..BoardHeight : board[row][col] = Empty
/\ LET rowToFill == CHOOSE r \in 1..BoardHeight : board[r][col] = Empty /\ (r = BoardHeight \/ board[r+1][col] /= Empty)
IN board' = [board EXCEPT ![rowToFill][col] = player]
/\ player' = IF player = "red" THEN "yellow" ELSE "red"
/\ winner' = IF \E p \in Players: \E r \in 1..BoardHeight, c \in 1..BoardWidth : HasWinningLine(board', p, r, c)
THEN Winner(board')
ELSE "none"
-----------------------------------------------------------------------------
Next == \E col \in 1..BoardWidth : Move(col)
Spec == Init /\ [][Next]_vars
Termination == <>(winner /= "none") \/ \A r \in 1..BoardHeight, c \in 1..BoardWidth : board[r][c] /= Empty
=============================================================================