Tic-tac-toe is finite, deterministic, perfect-information and zero-sum, so it has an exact game-theoretic value computed by backward-induction minimax on its transition system. We enumerate every reachable position, quotient by the board's symmetry, solve the game, and discharge the result as temporal-logic / reachability properties — the same pipeline the hidden-information games use, but with the hidden information removed, so the answer is exact.
A state is the 3×3 board (9 cells over {empty, X, O}); X moves first, so the side to move is fixed by the mark counts. Transitions are the legal moves (mark any empty cell); the game ends the instant a line completes or the board fills. Different move orders reaching the same board are the same state, so the game tree folds into a DAG. BFS from the empty board enumerates 5,478 reachable positions (626 X-wins, 316 O-wins, 16 draws, 4,520 non-terminal). The unmerged tree — distinct games counting move order, stopping at a win — has 255,168 leaves.
The 3×3 grid is invariant under D4 — 8 symmetries (4 rotations × 2 reflections). Boards related by a rotation or reflection are the same position strategically, so we quotient by D4 (the geometric analogue of a player-relabeling symmetry). That collapses 5,478 positions into 765 canonical positions — computed two independent ways (canonicalize every concrete board; BFS the quotient) that agree exactly.
We solve the game by minimax (X maximises, O minimises a +1/0/−1 payoff). The value of the empty board is 0 — a draw. As alternating-time (ATL) reachability properties:
Neither side can force a win. We don't just read off the value: we extract the optimal
strategy and re-verify it by reachability — playing the hero side optimally against
every opponent reply, no line ever reaches a loss for the hero. That certificate is the
temporal statement ⟨⟨hero⟩⟩ (¬lose U draw_or_win). The solver you play above runs
exactly this strategy — which is why it never loses.
A forced draw holds only between two perfect players. Against a uniform-random opponent the optimal side does far better — computed exactly by rational expectimax:
| Match-up | Mover wins | Draw | Mover loses |
|---|---|---|---|
| Optimal X vs random O | 191/192 ≈ 99.48% | 1/192 | 0 |
| Optimal O vs random X | 887/945 ≈ 93.86% | 43/945 | 1/63 ≈ 1.59% |
The optimal player never loses and wins almost always — the odds bar above shows this edge.
"At most one player has a completed line" is not a static fact about arbitrary boards (a parity-respecting board can carry two lines — those boards are just unreachable). So we prove it as a reachability invariant by induction over the move relation: z3 discharges BASE (the empty board satisfies the invariant) and STEP (every legal move preserves it) as ∀-theorems (UNSAT of each negation). That certifies the model's "stop at the first win" handling is sound for all 5,478 reachable positions without enumerating them.
Property. In normal-play Nim the player to move wins under perfect play iff the nim-sum (XOR of the heap sizes) is non-zero; the losing (P-) positions are exactly those with nim-sum 0. This is Bouton's theorem (1901), the Nim instance of the Sprague–Grundy theorem.
g = mex of the successors' values, computed by recursion (grundy.py); a single heap of size n has g = n, and Bouton's theorem gives g(h₁…hₖ) = h₁ ⊕ … ⊕ hₖ.grundy == XOR and XOR = 0 ⇔ mover loses on all 400 configs with ≤3 heaps of size ≤6.smt_proof.py discharges, as ∀-theorems over all positions (bit-vector XOR, UNSAT-of-negation):
L1 (progress) nim-sum ≠ 0 ⇒ ∃ a move to nim-sum 0, and L2 (closure) nim-sum = 0 ⇒ every move yields nim-sum ≠ 0. Together they are the winning-strategy certificate the bot plays.Everything here is exact — there is no estimation anywhere. The odds bar shows the true value: from a non-zero nim-sum the side to move wins with certainty.
Pig is a push-your-luck race: each turn you roll a die, banking a growing turn total, but rolling a 1 wipes it and ends your turn. We model two-player Pig as a stochastic game / Markov Decision Process, solve it by value iteration to the win-probability fixpoint, and certify the result — reproducing the Neller-Presser (2004) optimal-play solution.
Pig is fully observable (no hidden information), zero-sum (exactly one player wins), and symmetric (both face identical rules), so its value collapses to a single function for the player to move:
A state is just (myScore, oppScore, turnTotal) — a sufficient statistic: nothing else in
the history affects legal future play. Scores run 0–99; the turn total runs 0–99. The two actions are
roll and hold.
The opponent’s turn is the mover’s loss (zero-sum), so a turn-handover flips the value to
1 − V:
P=? [F win]“Who wins under optimal play?” is a probabilistic-reachability property — the probability of
eventually reaching a win state — written PCTL-style as P=? [F win] from the start
state (0,0,0). For an MDP this is the optimal reachability value, the fixpoint of the
Bellman operator, computed by value iteration exactly as PRISM/Storm do.
There is no discount factor, so convergence is not automatic. It holds because every state cedes the turn with positive probability (a bust, or the always-available hold), which resets the turn total and hands control over; the fresh-turn values over the finite 100×100 grid form a monotone, bounded Bellman system with a unique fixpoint. Iteration reaches it in ~150 sweeps.
We certify the converged value by recomputing its Bellman residual
max_s |V*(s) − (backup of V*)(s)| and checking it is 0 — exactly the fixpoint
check a probabilistic model checker performs. So the headline number is a certified value, not a
simulation; a Monte-Carlo run only cross-checks it.
| Quantity | Value | Status |
|---|---|---|
| First-player optimal win prob | 0.5306 (53.06%) | certified (exact, fixpoint) |
| Second-player optimal win prob | 0.4694 | certified (exact) |
| “Hold at 20” self-play (1st) | 0.5347 | certified (exact) |
| Optimal vs hold-20 (1st / 2nd) | 0.587 / 0.522 | certified (exact) |
| Bellman residual of V* | 0.0 | fixpoint certificate |
The optimal policy is the argmax of the Bellman equation — a roll/hold boundary
“roll until the turn total reaches t, then hold”. The folk heuristic “hold at 20” is close
from the start (optimal is “hold at 21” at 0–0) but wrong in general:
A truly-optimal player beats a hold-at-20 player head-to-head from both seats (0.587 going first, 0.522 going second; seat-average 0.555 > 0.5). The edge is small because hold-at-20 is a strong heuristic — but the state-dependent optimum strictly dominates the flat threshold. (Note: optimal self-play 0.5306 is below hold-20 self-play 0.5347 — these are different games; optimality is defined against an optimal opponent.)
The odds bar reads the certified value table directly: for the current state it shows
V(myScore, oppScore, turnTotal) reframed as P(you win). The “optimal call” line shows the
solver’s exact roll/hold decision and threshold for whoever is to move. The 16-bit table embedded here
reproduces the Python value iteration to ~1e-4 — the same numbers, in the browser.
mdp.py / verify.py).