Tic-Tac-Toe

Two players, X and O, take turns marking an empty cell of a 3 × 3 board, with X moving first. The first player to complete a line of three of their own marks — any of the 8 winning lines: 3 rows, 3 columns, or 2 diagonals — wins immediately; the game ends the instant a line completes. If the board fills with no line, the game is a draw.

The whole game is built as an explicit transition system — a graph whose nodes are board positions and whose edges are legal moves. A breadth-first search from the empty board enumerates every position the rules can actually produce; positions reached by different move orders are merged into a single node, collapsing the game tree (255,168 distinct complete games) into a compact graph of 5,478 reachable positions connected by 16,167 legal-move transitions.

Two reductions keep everything exact. Terminating the instant a line completes is simply the rule of the game, so boards where play continues after a win never appear. And because the grid looks the same under rotations and reflections — the 8-element dihedral symmetry group D4 — symmetric boards are the same position strategically; taking one canonical representative per symmetry class cuts the 5,478 positions to 765, computed by two independent methods that are checked against each other.

Tic-tac-toe is finite, deterministic, zero-sum and perfect information — both players see everything — so it has a well-defined game value, computed by backward-induction minimax: solving the game from its endings backwards to the first move. The value of the empty board is 0, a draw, which settles the strategic-logic questions <<X>> F x_win (“X can force a win”) and <<O>> F o_win: both are FALSE. The result is not just read off the value — the optimal strategy is extracted and re-verified by reachability, restricting the hero side to its optimal moves, letting the opponent play anything, and checking by search that no line of play ever reaches a loss for the hero.

A final layer uses the SMT solver z3 — a program that proves logical formulas outright rather than testing cases — to discharge an inductive invariant: a property true of the empty board and preserved by every legal move, and therefore true of every reachable position. It certifies that every reachable board has a single well-defined outcome (the two players can never both hold a completed line), without enumerating the 5,478 positions at all.

Perfect play from the empty board is a certified draw: neither X nor O can force a win, and the reachability certificate confirms the optimal player is never beaten — for either side. Every first move (corner, edge, or centre) is optimal and leads to a draw under best play. Of the 958 terminal positions, 626 are X wins, 316 are O wins, and just 16 are draws; the D4 symmetry quotient also shrinks the game tree to 26,830 strategically distinct games, a 7.16× reduction in positions.

The forced draw only holds between two perfect players. Against a fallible opponent the exact odds — computed in rational arithmetic, with the optimal side maximising its win probability and the random side choosing uniformly among legal moves — are heavily one-sided:

A perfect player never loses to a random one and wins almost always — the forced draw is a statement about perfect opposition, not about how the game usually goes.