Sudoku
Most Sudoku solvers hand you the answer; this one hands you the reasoning. It solves the way a person does — applying the lowest technique that makes progress and recording WHAT it did and WHY at every step as a single ordered trace, so the answer is just the last line of an argument you can read and check by hand. Five techniques (naked/hidden single, locked candidates, naked pair, x-wing), applied lowest-first. It never guesses: faced with a puzzle beyond its ladder it says “ceiling-hit” rather than searching — an honest difficulty read, not a failure. Deterministic: the same givens always produce the byte-identical trace.
The honest edge
It only makes FORCED moves — it reasons, it does not search or backtrack, so a puzzle needing a technique above x-wing returns ceiling-hit (a difficulty read), not a guessed fill. And ‘broken’ fires when reasoning empties a cell; a contradiction sitting between two givens no technique touches reads as ceiling-hit, because the solver reasons about the puzzle rather than front-validating your input.
Run it
python3 sudoku.py --demo
test_sudoku.py (130/130, mutation-bitten, pinned golden trace)
Python standard library only, deterministic + headless
The code — every file that ships
sudoku.py549 lineson GitHub →
#!/usr/bin/env python3
"""sudoku — a Sudoku solver that shows its work.
Most solvers hand you the answer. This one hands you the *reasoning*: it solves
the way a person does — applying the lowest technique that makes progress and
recording WHAT it did and WHY at every step, as a single ordered trace. The
answer is just the last line of an argument you can read.
from sudoku import solve, from_string
result = solve(from_string("53..7....6..195....98....6.8...6...34..8.3..17...2...6.6....28....419..5....8..79"))
result.status # 'solved-unique' | 'ceiling-hit' | 'broken'
for step in result.trace:
print(step.reason) # "naked single: 4 is the only candidate left for r1c3 ..."
Five techniques, applied lowest-first (so the explanation reads like a human
tutor, easiest move first):
1. naked single — a cell with only one candidate left
2. hidden single — a digit that fits only one cell in a unit
3. locked candidates — pointing / claiming (an elimination technique)
4. naked pair — two cells locking two digits to themselves
5. x-wing — the basic fish
Three honest terminal states:
solved-unique — solved by these techniques alone; `solution` is filled in.
ceiling-hit — consistent but needs a technique above the ladder (a
DIFFICULTY read, not a failure — this puzzle is "harder
than x-wing", which is useful information).
broken — a cell ran out of candidates; the givens contradict.
Properties (see test_sudoku.py):
- Deterministic: the same givens always produce the byte-identical trace.
- Certifying: every placement/elimination carries a human sentence saying
why it is forced. The trace is a proof you can check by hand.
- Never guesses: it only makes forced moves. It will say "ceiling-hit"
before it will backtrack — it does not search, it reasons.
Zero dependencies (Python standard library only). Headless: givens in, a
SolveResult out — no I/O in the solver, no globals, no randomness.
Origin: the reasoning core of a self-explaining Sudoku teaching app, stripped to
stand alone. MIT licensed — take the folder.
"""
from __future__ import annotations
import re
from dataclasses import dataclass, asdict
from typing import Callable, Dict, List, Optional, Set, Tuple
Cell = Tuple[int, int] # (row, col), 0-indexed
Grid = List[List[int]] # 9x9, 0 = empty
Candidates = Dict[Cell, Set[int]]
N = 9
DIGITS = frozenset(range(1, 10))
# ── The trace (the spine — everything folds from this) ──────────────────────
@dataclass
class TechniqueApplication:
technique: str # rung name
cells_affected: List[Cell] # coordinates touched
candidates_eliminated: List[Tuple[Cell, int]] # what this step ruled out
reason: str # the human sentence: WHY
def to_dict(self) -> dict:
d = asdict(self)
d["cells_affected"] = [list(c) for c in self.cells_affected]
d["candidates_eliminated"] = [
[list(c), dg] for c, dg in self.candidates_eliminated
]
return d
@dataclass
class SolveResult:
status: str # solved-unique|ceiling-hit|broken
trace: List[TechniqueApplication]
solution: Optional[Grid] = None # present iff solved-unique
def to_dict(self) -> dict:
return {
"status": self.status,
"trace": [t.to_dict() for t in self.trace],
"solution": self.solution,
}
# ── Geometry (units: rows, cols, boxes) ─────────────────────────────────────
def _peers(cell: Cell) -> Set[Cell]:
r, c = cell
peers: Set[Cell] = set()
for k in range(N):
peers.add((r, k))
peers.add((k, c))
br, bc = 3 * (r // 3), 3 * (c // 3)
for dr in range(3):
for dc in range(3):
peers.add((br + dr, bc + dc))
peers.discard(cell)
return peers
def _units() -> List[List[Cell]]:
units: List[List[Cell]] = []
for r in range(N):
units.append([(r, c) for c in range(N)]) # rows
for c in range(N):
units.append([(r, c) for r in range(N)]) # cols
for br in range(0, N, 3):
for bc in range(0, N, 3):
units.append([(br + dr, bc + dc)
for dr in range(3) for dc in range(3)]) # boxes
return units
_UNITS = _units()
_UNIT_NAME = (
["row " + str(i + 1) for i in range(N)]
+ ["column " + str(i + 1) for i in range(N)]
+ ["box " + str(i + 1) for i in range(N)]
)
def compute_candidates(grid: Grid) -> Candidates:
"""For every empty cell, the digits not already used by one of its peers.
Deterministic and total — the fixed point recomputes this each step.
"""
cands: Candidates = {}
for r in range(N):
for c in range(N):
if grid[r][c] != 0:
continue
seen = {grid[pr][pc] for pr, pc in _peers((r, c)) if grid[pr][pc] != 0}
cands[(r, c)] = set(DIGITS) - seen
return cands
# ── The ladder (reorderable DATA — the one live research object) ────────────
# A rung: given the candidate grid, return the ONE lowest-rung, row-major-first
# applicable move as a TechniqueApplication, or None. Rungs never mutate.
#
# Two KINDS of rung share this signature, and the loop tells them apart by ONE
# schema-stable signal — `candidates_eliminated`:
# PLACEMENT rung (naked/hidden-single): places a digit; `candidates_eliminated`
# is [] and the placed digit is the first [1-9] in `reason`.
# ELIMINATION rung (locked-candidates, pairs, x-wing): places NOTHING; it
# prunes candidates, so `candidates_eliminated` is non-empty and there is
# no placed digit. `cells_affected` are the cells it pruned FROM.
# Invariant: `candidates_eliminated` non-empty <=> elimination step. A rung
# that would eliminate nothing returns None (no progress -> the loop would spin).
Rung = Callable[[Grid, Candidates], Optional[TechniqueApplication]]
def _rowmajor(cells) -> list:
"""The within-rung tie-break: smallest (row, col) first."""
return sorted(cells)
def _box_of(cell: Cell) -> Tuple[int, int]:
r, c = cell
return (3 * (r // 3), 3 * (c // 3))
def _box_cells(br: int, bc: int) -> List[Cell]:
return [(br + dr, bc + dc) for dr in range(3) for dc in range(3)]
def _box_num(br: int, bc: int) -> int:
return (br // 3) * 3 + (bc // 3) + 1
# Row/column units in a fixed order (rows 1-9 then cols 1-9), for the line-based
# rungs; digit names within a reason are 1-indexed to match the singles' voice.
_ROWS: List[List[Cell]] = [[(r, c) for c in range(N)] for r in range(N)]
_COLS: List[List[Cell]] = [[(r, c) for r in range(N)] for c in range(N)]
_BOXES: List[Tuple[int, int]] = [(br, bc) for br in range(0, N, 3)
for bc in range(0, N, 3)]
def rung_naked_single(grid: Grid, cands: Candidates) -> Optional[TechniqueApplication]:
for cell in _rowmajor(cands):
opts = cands[cell]
if len(opts) == 1:
d = next(iter(opts))
r, c = cell
return TechniqueApplication(
technique="naked-single",
cells_affected=[cell],
candidates_eliminated=[],
reason=(f"naked single: {d} is the only candidate left for "
f"r{r + 1}c{c + 1} — every other digit is already used "
f"by one of its peers."),
)
return None
def rung_hidden_single(grid: Grid, cands: Candidates) -> Optional[TechniqueApplication]:
# Units in a fixed order; within a unit, digits ascending; first hit wins.
for ui, unit in enumerate(_UNITS):
empties = [cell for cell in unit if cell in cands]
for d in range(1, 10):
spots = [cell for cell in empties if d in cands[cell]]
if len(spots) == 1:
cell = spots[0]
# Skip if a naked single would already place it (lower rung wins).
if len(cands[cell]) == 1:
continue
r, c = cell
# The placed digit MUST be the first numeral in the reason:
# _placed_digit greps the first \b[1-9]\b, so leading with a
# unit number would make it place the unit's number, not {d}.
return TechniqueApplication(
technique="hidden-single",
cells_affected=[cell],
candidates_eliminated=[],
reason=(f"hidden single: {d} can only go in r{r + 1}c{c + 1} "
f"— within {_UNIT_NAME[ui]} it fits nowhere else."),
)
return None
def rung_locked_candidates(grid: Grid, cands: Candidates) -> Optional[TechniqueApplication]:
"""Locked candidates (pointing + claiming). An ELIMINATION rung.
Pointing: within a box, if every candidate for a digit lies in one line
(row or col), that digit is eliminated from the rest of that line.
Claiming: within a line, if every candidate for a digit lies in one box,
that digit is eliminated from the rest of that box.
"""
# ── Pointing: box -> line ───────────────────────────────────────────────
for br, bc in _BOXES:
cells = _box_cells(br, bc)
for d in range(1, 10):
spots = [cell for cell in cells if cell in cands and d in cands[cell]]
if len(spots) < 2:
continue
rows = {r for r, _c in spots}
cols = {c for _r, c in spots}
if len(rows) == 1:
r = next(iter(rows))
targets = _rowmajor(cell for cell in _ROWS[r]
if cell not in cells
and cell in cands and d in cands[cell])
if targets:
return TechniqueApplication(
technique="locked-candidates",
cells_affected=targets,
candidates_eliminated=[(cell, d) for cell in targets],
reason=(f"locked candidates: in box {_box_num(br, bc)}, "
f"{d} can only go in row {r + 1}, so {d} is "
f"eliminated from the rest of row {r + 1}."),
)
if len(cols) == 1:
c = next(iter(cols))
targets = _rowmajor(cell for cell in _COLS[c]
if cell not in cells
and cell in cands and d in cands[cell])
if targets:
return TechniqueApplication(
technique="locked-candidates",
cells_affected=targets,
candidates_eliminated=[(cell, d) for cell in targets],
reason=(f"locked candidates: in box {_box_num(br, bc)}, "
f"{d} can only go in column {c + 1}, so {d} is "
f"eliminated from the rest of column {c + 1}."),
)
# ── Claiming: line -> box ───────────────────────────────────────────────
for name, unit in ([(f"row {i + 1}", u) for i, u in enumerate(_ROWS)]
+ [(f"column {i + 1}", u) for i, u in enumerate(_COLS)]):
for d in range(1, 10):
spots = [cell for cell in unit if cell in cands and d in cands[cell]]
if len(spots) < 2:
continue
boxes = {_box_of(cell) for cell in spots}
if len(boxes) == 1:
br, bc = next(iter(boxes))
box = _box_cells(br, bc)
targets = _rowmajor(cell for cell in box
if cell not in unit
and cell in cands and d in cands[cell])
if targets:
return TechniqueApplication(
technique="locked-candidates",
cells_affected=targets,
candidates_eliminated=[(cell, d) for cell in targets],
reason=(f"locked candidates: in {name}, {d} can only go "
f"in box {_box_num(br, bc)}, so {d} is eliminated "
f"from the rest of box {_box_num(br, bc)}."),
)
return None
def rung_naked_pair(grid: Grid, cands: Candidates) -> Optional[TechniqueApplication]:
"""Naked pair. Two cells in a unit sharing the SAME two candidates {x, y}
lock those digits to themselves, eliminating x and y from every other cell
in that unit."""
for ui, unit in enumerate(_UNITS):
bi = _rowmajor(cell for cell in unit
if cell in cands and len(cands[cell]) == 2)
for i in range(len(bi)):
for j in range(i + 1, len(bi)):
a, b = bi[i], bi[j]
if cands[a] != cands[b]:
continue
pair = sorted(cands[a]) # [x, y]
elim: List[Tuple[Cell, int]] = []
for cell in unit:
if cell in (a, b) or cell not in cands:
continue
for d in pair:
if d in cands[cell]:
elim.append((cell, d))
if elim:
elim.sort()
affected = _rowmajor({c for c, _d in elim})
ar, ac = a
br_, bc_ = b
return TechniqueApplication(
technique="naked-pair",
cells_affected=affected,
candidates_eliminated=elim,
reason=(f"naked pair: {pair[0]} and {pair[1]} are locked "
f"to r{ar + 1}c{ac + 1} and r{br_ + 1}c{bc_ + 1} "
f"in {_UNIT_NAME[ui]}, so both are eliminated from "
f"the rest of that unit."),
)
return None
def rung_x_wing(grid: Grid, cands: Candidates) -> Optional[TechniqueApplication]:
"""X-wing (basic fish). If two rows each have digit d as a candidate in
EXACTLY the same two columns, d is eliminated from those columns in every
other row (and the column-based transpose)."""
# ── Row-based: base = two rows, cross = two columns ─────────────────────
for d in range(1, 10):
rowcols: Dict[int, Tuple[int, int]] = {}
for r in range(N):
cols = [c for c in range(N)
if (r, c) in cands and d in cands[(r, c)]]
if len(cols) == 2:
rowcols[r] = (cols[0], cols[1])
bases = sorted(rowcols)
for i in range(len(bases)):
for j in range(i + 1, len(bases)):
r1, r2 = bases[i], bases[j]
if rowcols[r1] != rowcols[r2]:
continue
c1, c2 = rowcols[r1]
targets = _rowmajor(
(r, c) for r in range(N) if r not in (r1, r2)
for c in (c1, c2)
if (r, c) in cands and d in cands[(r, c)])
if targets:
return TechniqueApplication(
technique="x-wing",
cells_affected=targets,
candidates_eliminated=[(cell, d) for cell in targets],
reason=(f"X-wing: {d} in rows {r1 + 1} and {r2 + 1} is "
f"confined to columns {c1 + 1} and {c2 + 1}, so "
f"{d} is eliminated from those columns in every "
f"other row."),
)
# ── Column-based (transpose): base = two columns, cross = two rows ──────
for d in range(1, 10):
colrows: Dict[int, Tuple[int, int]] = {}
for c in range(N):
rows = [r for r in range(N)
if (r, c) in cands and d in cands[(r, c)]]
if len(rows) == 2:
colrows[c] = (rows[0], rows[1])
bases = sorted(colrows)
for i in range(len(bases)):
for j in range(i + 1, len(bases)):
c1, c2 = bases[i], bases[j]
if colrows[c1] != colrows[c2]:
continue
r1, r2 = colrows[c1]
targets = _rowmajor(
(r, c) for c in range(N) if c not in (c1, c2)
for r in (r1, r2)
if (r, c) in cands and d in cands[(r, c)])
if targets:
return TechniqueApplication(
technique="x-wing",
cells_affected=targets,
candidates_eliminated=[(cell, d) for cell in targets],
reason=(f"X-wing: {d} in columns {c1 + 1} and {c2 + 1} is "
f"confined to rows {r1 + 1} and {r2 + 1}, so "
f"{d} is eliminated from those rows in every "
f"other column."),
)
return None
# ORDER IS DATA — reorder to change the difficulty model, never hard-code it.
# New techniques (wings, chains) append here; the solve loop never changes.
LADDER: List[Tuple[str, int, Rung]] = [
("naked-single", 1, rung_naked_single),
("hidden-single", 2, rung_hidden_single),
("locked-candidates", 3, rung_locked_candidates),
("naked-pair", 4, rung_naked_pair),
("x-wing", 5, rung_x_wing),
]
def _is_contradiction(grid: Grid, cands: Candidates) -> bool:
for cell, opts in cands.items():
if not opts: # an empty cell with no candidate = broken
return True
return False
def _complete(grid: Grid) -> bool:
return all(grid[r][c] != 0 for r in range(N) for c in range(N))
def _placed_digit(step: TechniqueApplication) -> int:
# CONTRACT: a PLACEMENT reason MUST lead with the placed digit — it is the
# first \b[1-9]\b in the string, before any row/col/unit numeral. Both
# placement rungs honor this. Never call this on an elimination step
# (candidates_eliminated non-empty); use its structured (cell, digit) pairs.
m = re.search(r"\b([1-9])\b", step.reason)
return int(m.group(1))
def _is_placement(step: TechniqueApplication) -> bool:
"""A step is a PLACEMENT iff it eliminates no candidates (it places a digit);
otherwise it is an ELIMINATION (it prunes candidates, places nothing)."""
return not step.candidates_eliminated
def solve(givens: Grid) -> SolveResult:
"""solve(givens) -> SolveResult. Prefer-lowest-rung fixed point.
Candidates are CARRIED, not recomputed each step: a placement prunes the
placed digit from the placed cell's peers; an elimination prunes the pruned
(cell, digit) pairs. Recomputing from the grid alone would lose every
elimination-rung deduction (they don't live in the grid), so the persistent
candidate set is what lets a later single depend on an earlier elimination.
"""
grid = [row[:] for row in givens]
cands = compute_candidates(grid)
trace: List[TechniqueApplication] = []
while True:
if _is_contradiction(grid, cands):
return SolveResult(status="broken", trace=trace, solution=None)
if _complete(grid):
return SolveResult(status="solved-unique", trace=trace,
solution=[row[:] for row in grid])
# walk the ladder bottom-up; apply the LOWEST rung that makes progress
step: Optional[TechniqueApplication] = None
for _name, _tier, rung in LADDER:
step = rung(grid, cands)
if step is not None:
break
if step is None:
# no rung progresses, board consistent but unfinished — a
# DIFFICULTY read, not a failure.
return SolveResult(status="ceiling-hit", trace=trace, solution=None)
if _is_placement(step):
(r, c) = step.cells_affected[0]
d = _placed_digit(step)
grid[r][c] = d
del cands[(r, c)]
for peer in _peers((r, c)):
if peer in cands:
cands[peer].discard(d)
else:
for cell, dig in step.candidates_eliminated:
if cell in cands:
cands[cell].discard(dig)
trace.append(step)
# ── convenience: parse / print an 81-char string ("." or "0" = empty) ───────
def from_string(s: str) -> Grid:
s = "".join(ch for ch in s if not ch.isspace())
if len(s) != 81:
raise ValueError(f"expected 81 cells, got {len(s)}")
g: Grid = []
for r in range(N):
row = []
for c in range(N):
ch = s[r * N + c]
row.append(0 if ch in ".0" else int(ch))
g.append(row)
return g
def to_string(grid: Grid) -> str:
return "".join(str(grid[r][c]) for r in range(N) for c in range(N))
def render(grid: Grid) -> str:
"""A human-readable 9x9 grid with box separators (for the CLI)."""
lines = []
for r in range(N):
if r in (3, 6):
lines.append("------+-------+------")
cells = []
for c in range(N):
if c in (3, 6):
cells.append("|")
cells.append(str(grid[r][c]) if grid[r][c] else ".")
lines.append(" ".join(cells))
return "\n".join(lines)
# ── CLI: read an 81-char puzzle, print the reasoning, then the answer ───────
def _main(argv: List[str]) -> int:
demo = "53..7....6..195....98....6.8...6...34..8.3..17...2...6.6....28....419..5....8..79"
if argv and argv[0] in ("-h", "--help"):
print("usage: python3 sudoku.py [81-char-puzzle | --demo]")
print(" cells 1-9; '.' or '0' = empty; whitespace ignored")
print(" prints the step-by-step reasoning, then the solution")
return 0
arg = argv[0] if argv else "--demo"
puzzle = demo if arg in ("", "--demo") else arg
try:
grid = from_string(puzzle)
except ValueError as e:
print(f"bad puzzle: {e}")
return 2
print("puzzle:")
print(render(grid))
print()
result = solve(grid)
print(f"status: {result.status} ({len(result.trace)} steps)\n")
for i, step in enumerate(result.trace, 1):
print(f" {i:>2}. {step.reason}")
if result.solution is not None:
print("\nsolution:")
print(render(result.solution))
elif result.status == "ceiling-hit":
print("\n(consistent, but needs a technique above this solver's ladder — "
"a difficulty read, not a failure.)")
return 0
if __name__ == "__main__":
import sys
raise SystemExit(_main(sys.argv[1:]))
test_sudoku.py248 lineson GitHub →
#!/usr/bin/env python3
# SPDX-License-Identifier: MIT
"""test_sudoku.py — proves the solver is certifying, deterministic, and honest.
The claims that ARE the tool:
1. CERTIFYING: every step carries a reason, and the reason is CHECKABLE —
a placement's reason leads with the digit it places, and re-applying the
whole trace to the givens reproduces the solution. The trace is a proof.
2. DETERMINISTIC: the same givens produce the byte-identical trace, every run.
3. THREE HONEST STATES: solved-unique (with a valid solution), ceiling-hit
(consistent but beyond the ladder — a difficulty read), broken (givens
contradict). Each is reachable and correctly labelled.
4. NEVER GUESSES: it stops at ceiling-hit rather than searching. A puzzle
needing a technique above x-wing returns ceiling-hit, not a lucky answer.
Plus a mutation bite so a vacuously-green run fails loud. stdlib only.
Exit 0 = all pass, exit 1 = a failure (loud).
"""
import sys
import os
sys.path.insert(0, os.path.dirname(os.path.abspath(__file__)))
from sudoku import (
solve, from_string, to_string, compute_candidates,
SolveResult, TechniqueApplication, _peers, _units, N, LADDER,
)
_pass = 0
_fail = 0
def eq(name, got, want):
global _pass, _fail
if got == want:
_pass += 1
else:
_fail += 1
print(f"FAIL {name}\n got: {got!r}\n want: {want!r}")
def ok(name, cond):
global _pass, _fail
if cond:
_pass += 1
else:
_fail += 1
print(f"FAIL {name}")
# ── Fixtures ─────────────────────────────────────────────────────────────────
EASY = "53..7....6..195....98....6.8...6...34..8.3..17...2...6.6....28....419..5....8..79"
EASY_SOLUTION = "534678912672195348198342567859761423426853791713924856961537284287419635345286179"
# A grid that is complete and correct = solve returns it unchanged, zero steps.
SOLVED = EASY_SOLUTION
# A contradiction the solver actually REACHES: the near-complete easy solution
# with r1c1 blanked and a 5 planted in its box, so r1c1's only digit (5) is
# already taken by a peer — compute_candidates leaves it with an empty set and
# _is_contradiction fires. (Note: a contradiction between two GIVENS that no
# technique touches reads as ceiling-hit, not broken — the solver reasons, it
# does not front-validate the givens. That is correct and intentional.)
BROKEN = ".54678912672195348198342567859761423426853791713924856961537284287419635345286179"
def is_valid_solution(s: str) -> bool:
"""A solved grid: 81 non-zero cells, every row/col/box a permutation of 1-9."""
g = from_string(s)
if any(g[r][c] == 0 for r in range(N) for c in range(N)):
return False
for unit in _units():
vals = sorted(g[r][c] for r, c in unit)
if vals != list(range(1, 10)):
return False
return True
# ── PROPERTY 1: certifying — the trace is a checkable proof ───────────────────
(lambda: None)() # keep the section visible
def _replay_trace(givens, result):
"""Re-apply the recorded trace to the givens; a placement's reason must lead
with the digit it places, and applying every placement must reproduce the
solution. This proves the reasons are not decorative — they carry the moves."""
import re
g = [row[:] for row in givens]
for step in result.trace:
if not step.candidates_eliminated: # placement
(r, c) = step.cells_affected[0]
d = int(re.search(r"\b([1-9])\b", step.reason).group(1))
g[r][c] = d
return g
r_easy = solve(from_string(EASY))
ok("easy solves", r_easy.status == "solved-unique")
ok("easy solution is valid", r_easy.solution is not None and is_valid_solution(to_string(r_easy.solution)))
eq("easy solution matches known answer", to_string(r_easy.solution), EASY_SOLUTION)
ok("every step has a non-empty reason", all(s.reason.strip() for s in r_easy.trace))
ok("trace is non-trivial", len(r_easy.trace) > 10)
# the certifying check: replaying the trace's placements reproduces the solution
replayed = _replay_trace(from_string(EASY), r_easy)
eq("replaying the trace reproduces the solution", to_string(replayed), EASY_SOLUTION)
# every placement step's reason leads with the digit actually placed in the solution
import re
for step in r_easy.trace:
if not step.candidates_eliminated: # placement
(rr, cc) = step.cells_affected[0]
placed = int(re.search(r"\b([1-9])\b", step.reason).group(1))
ok(f"placement reason leads with placed digit @r{rr+1}c{cc+1}",
placed == from_string(EASY_SOLUTION)[rr][cc])
# ── PROPERTY 2: deterministic — byte-identical trace every run ────────────────
def trace_signature(result):
return to_string_result(result)
def to_string_result(result):
import json
return json.dumps(result.to_dict(), sort_keys=True)
sig1 = to_string_result(solve(from_string(EASY)))
sig2 = to_string_result(solve(from_string(EASY)))
sig3 = to_string_result(solve(from_string(EASY)))
ok("deterministic: run 1 == run 2", sig1 == sig2)
ok("deterministic: run 2 == run 3", sig2 == sig3)
# GOLDEN: pin the canonical trace signature by hash. Self-equality alone is a
# weak determinism test (a benign reorder stays self-equal); a pinned golden
# catches any change to the tie-break / scan order that reorders the trace.
import hashlib as _hl
_golden = "1f4fc6f7b5886070bb06a38c5457ef9c93a4c4dabdb9735518786b8f57e91548"
_got = _hl.sha256(sig1.encode()).hexdigest()
ok("deterministic: trace matches the pinned golden signature", _got == _golden)
# solving does not mutate the givens
givens = from_string(EASY)
before = to_string(givens)
solve(givens)
eq("solve does not mutate givens", to_string(givens), before)
# ── PROPERTY 3: three honest terminal states ──────────────────────────────────
# solved-unique (already covered above)
# broken:
r_broken = solve(from_string(BROKEN))
ok("contradiction -> broken", r_broken.status == "broken")
ok("broken has no solution", r_broken.solution is None)
# an already-solved grid: solved-unique, zero steps, solution == input
r_done = solve(from_string(SOLVED))
ok("already-solved -> solved-unique", r_done.status == "solved-unique")
eq("already-solved needs zero steps", len(r_done.trace), 0)
eq("already-solved returns the same grid", to_string(r_done.solution), SOLVED)
# ── PROPERTY 4: never guesses — ceiling-hit before search ─────────────────────
# The empty grid is consistent but has no forced move for these techniques,
# so a NON-searching solver must return ceiling-hit (a searching one would
# "solve" it to some arbitrary valid grid). This is the anti-guess proof.
EMPTY = "." * 81
r_empty = solve(from_string(EMPTY))
ok("empty grid -> ceiling-hit (does NOT guess a solution)", r_empty.status == "ceiling-hit")
ok("ceiling-hit has no solution", r_empty.solution is None)
# a partial consistent grid with no forced single also ceiling-hits rather than searching
# (17-clue minimal puzzles typically need guessing; a bare 2-clue grid certainly does)
SPARSE = "1................2..............................................................."
r_sparse = solve(from_string(SPARSE))
ok("sparse consistent grid -> ceiling-hit, not a guessed fill",
r_sparse.status == "ceiling-hit" and r_sparse.solution is None)
# ── The elimination rungs actually fire (coverage that the ladder is exercised) ─
# Not every easy puzzle exercises the higher rungs; assert the ladder is complete
# and each rung is callable and returns the right SHAPE when it does fire.
ok("ladder has all five rungs", [name for name, _t, _f in LADDER] ==
["naked-single", "hidden-single", "locked-candidates", "naked-pair", "x-wing"])
# a placement step: candidates_eliminated empty; an elimination step: non-empty.
for step in r_easy.trace:
placement = not step.candidates_eliminated
if placement:
ok(f"placement step has one affected cell ({step.technique})", len(step.cells_affected) == 1)
else:
ok(f"elimination step eliminated something ({step.technique})", len(step.candidates_eliminated) >= 1)
# ── input validation ──────────────────────────────────────────────────────────
def raises(name, fn):
global _pass, _fail
try:
fn()
_fail += 1
print(f"FAIL {name} (expected raise)")
except Exception:
_pass += 1
raises("from_string rejects wrong length", lambda: from_string("123"))
raises("from_string rejects 80 chars", lambda: from_string("." * 80))
ok("from_string accepts 81 with whitespace", to_string(from_string("." * 81)) == "0" * 81)
ok("from_string treats 0 and . both as empty",
from_string("0" * 81) == from_string("." * 81))
# ── candidates helper is correct ──────────────────────────────────────────────
cands = compute_candidates(from_string(EASY))
# r1c3 (row 0, col 2) is empty in EASY; its candidates must exclude peers' givens
ok("candidates computed for empty cells only",
all(from_string(EASY)[r][c] == 0 for (r, c) in cands))
ok("a candidate set never contains a peer's given",
all(all((from_string(EASY)[pr][pc] not in opts)
for (pr, pc) in _peers(cell) if from_string(EASY)[pr][pc] != 0)
for cell, opts in cands.items()))
# ── MUTATION BITE: prove the certifying check is not vacuously green ───────────
# If the reasons were decorative (not carrying the placed digit), the replay
# would NOT reproduce the solution. This bite asserts that (a) the trace has
# real placement steps, and (b) mangling a reason's leading digit WOULD break
# the replay — so a no-op reason (the plausible mutation) fails loud here.
placements = [s for s in r_easy.trace if not s.candidates_eliminated]
ok("mutation bite: trace has real placements", len(placements) > 0)
def _replay_with_broken_reasons(givens, result):
"""Replay but with every placement reason's digit forced to 1 — must NOT
reproduce the solution (unless every placed digit really is 1, impossible)."""
g = [row[:] for row in givens]
for step in result.trace:
if not step.candidates_eliminated:
(r, c) = step.cells_affected[0]
g[r][c] = 1 # deliberately wrong: ignore the real reason
return to_string(g)
ok("mutation bite: breaking the reason breaks the replay",
_replay_with_broken_reasons(from_string(EASY), r_easy) != EASY_SOLUTION)
# and: if solve silently returned 'solved' on the empty grid (a searching
# mutation), property 4 would flip. Assert the anti-guess invariant has teeth:
ok("mutation bite: empty grid is genuinely unforced (>50 empty cells, 0 forced singles)",
len(compute_candidates(from_string(EMPTY))) == 81
and all(len(v) == 9 for v in compute_candidates(from_string(EMPTY)).values()))
print(("PASS" if _fail == 0 else "FAIL") + f" — {_pass} passed, {_fail} failed")
sys.exit(0 if _fail == 0 else 1)