| """Is the Sudoku result meaningful, or is the benchmark simply saturated? |
| |
| A neural solver scoring 100% on a test split proves nothing on its own. The |
| questions that decide whether the number means anything: |
| |
| 1. HOW HARD ARE THESE PUZZLES? If plain constraint propagation - no search, no |
| backtracking, the first thing anyone writes - already solves every test |
| puzzle, then the benchmark is trivial and 100% is the expected result for any |
| competent method rather than evidence of anything. This is the test that |
| matters most, and it is run first. |
| |
| 2. IS THE MARGIN STATISTICALLY REAL? 100% against a published 98.3% on 1000 |
| puzzles: exact binomial, not eyeballing. |
| |
| 3. DOES IT HOLD PER SEED? A mean of 100% could hide a split. |
| |
| 4. DOES IT GENERALISE TO HARDER PUZZLES? SATNet's puzzles carry 31-42 clues. |
| Stripping clues while VERIFYING the solution stays unique gives strictly |
| harder instances from the same distribution, and shows whether the model |
| learned Sudoku or learned this clue-density. |
| |
| Every puzzle generated for (4) is checked to have exactly one solution by an |
| exhaustive counter, so "accuracy" remains well defined. |
| """ |
| import argparse, glob, json, os, sys |
| from collections import defaultdict |
|
|
| import numpy as np |
|
|
| sys.path.insert(0, os.path.dirname(os.path.abspath(__file__))) |
| from sudoku import GRID, CELLS, load_satnet, split |
|
|
| PEERS = None |
|
|
|
|
| def _build_peers(): |
| """For each cell, the 20 cells sharing its row, column or box.""" |
| peers = [] |
| for i in range(CELLS): |
| r, c = divmod(i, GRID) |
| br, bc = 3 * (r // 3), 3 * (c // 3) |
| s = set() |
| for k in range(GRID): |
| s.add(r * GRID + k) |
| s.add(k * GRID + c) |
| for dr in range(3): |
| for dc in range(3): |
| s.add((br + dr) * GRID + bc + dc) |
| s.discard(i) |
| peers.append(sorted(s)) |
| return peers |
|
|
|
|
| def candidates(grid): |
| """Per-cell candidate sets as 9-bit masks; None if a contradiction appears. |
| |
| Values are forced to Python ints: numpy integer scalars lack .bit_length(), |
| and mixing the two silently produces numpy masks that then fail. |
| """ |
| g = [int(v) for v in grid] |
| cand = [0x1FF if v == 0 else (1 << (v - 1)) for v in g] |
| for i, v in enumerate(g): |
| if v: |
| bit = 1 << (v - 1) |
| for p in PEERS[i]: |
| if cand[p] & bit: |
| cand[p] &= ~bit |
| if cand[p] == 0: |
| return None |
| return cand |
|
|
|
|
| def propagate(grid): |
| """Constraint propagation only: naked singles + hidden singles to fixpoint. |
| |
| This is the baseline every Sudoku solver starts from and it uses no search. |
| If it solves the whole test split, the split is trivial. |
| """ |
| g = [int(v) for v in grid] |
| while True: |
| cand = candidates(g) |
| if cand is None: |
| return None |
| changed = False |
| for i in range(CELLS): |
| if g[i] == 0 and bin(cand[i]).count("1") == 1: |
| g[i] = cand[i].bit_length() |
| changed = True |
| if not changed: |
| |
| for unit in UNITS: |
| for d in range(9): |
| bit = 1 << d |
| spots = [i for i in unit if g[i] == 0 and cand[i] & bit] |
| if len(spots) == 1: |
| g[spots[0]] = d + 1 |
| changed = True |
| if not changed: |
| return g |
|
|
|
|
| def _units(): |
| us = [] |
| for r in range(GRID): |
| us.append([r * GRID + c for c in range(GRID)]) |
| for c in range(GRID): |
| us.append([r * GRID + c for r in range(GRID)]) |
| for br in range(0, GRID, 3): |
| for bc in range(0, GRID, 3): |
| us.append([(br + dr) * GRID + bc + dc for dr in range(3) for dc in range(3)]) |
| return us |
|
|
|
|
| def count_solutions(grid, limit=2): |
| """Exhaustive count of solutions, stopping at `limit`. Used for uniqueness.""" |
| g = [int(v) for v in grid] |
|
|
| def rec(): |
| cand = candidates(g) |
| if cand is None: |
| return 0 |
| best, bi = 10, -1 |
| for i in range(CELLS): |
| if g[i] == 0: |
| n = bin(cand[i]).count("1") |
| if n < best: |
| best, bi = n, i |
| if n == 1: |
| break |
| if bi < 0: |
| return 1 |
| total = 0 |
| for d in range(9): |
| if cand[bi] & (1 << d): |
| g[bi] = d + 1 |
| total += rec() |
| g[bi] = 0 |
| if total >= limit: |
| return total |
| return total |
|
|
| return rec() |
|
|
|
|
| def wilson(k, n, z=1.96): |
| if n == 0: |
| return 0.0, 0.0 |
| p = k / n |
| d = 1 + z * z / n |
| c = (p + z * z / (2 * n)) / d |
| h = z * np.sqrt(p * (1 - p) / n + z * z / (4 * n * n)) / d |
| return max(0.0, c - h), min(1.0, c + h) |
|
|
|
|
| def binom_p(k, n, p0): |
| """One-sided exact binomial: P(X >= k) under H0: rate = p0.""" |
| from math import comb |
| return float(sum(comb(n, i) * p0 ** i * (1 - p0) ** (n - i) for i in range(k, n + 1))) |
|
|
|
|
| PEERS = _build_peers() |
| UNITS = _units() |
|
|
| p = argparse.ArgumentParser() |
| p.add_argument("--root", default="data/sudoku") |
| p.add_argument("--runs", default="runs") |
| p.add_argument("--n_hard", type=int, default=200) |
| p.add_argument("--out", default="figures/sudoku_validate.json") |
| a = p.parse_args() |
|
|
| X, Y, tok = load_satnet(a.root) |
| (Xtr, Ytr), (Xte, Yte) = split(X, Y) |
| out = {} |
|
|
| print("=" * 78) |
| print("1. HOW HARD IS THIS BENCHMARK? (the test that decides if 100% means anything)") |
| print("=" * 78) |
| cp_solved = 0 |
| for i in range(len(Xte)): |
| g = propagate(Xte[i]) |
| if g is not None and all(v > 0 for v in g) and np.array_equal(g, Yte[i]): |
| cp_solved += 1 |
| cp_rate = cp_solved / len(Xte) |
| out["classical_propagation"] = cp_rate |
| print(f" constraint propagation alone, NO search: {cp_solved}/{len(Xte)} = {cp_rate*100:.2f}%") |
| print(f" clues per test puzzle: min={(Xte>0).sum(1).min()} " |
| f"max={(Xte>0).sum(1).max()} mean={(Xte>0).sum(1).mean():.1f}") |
| if cp_rate > 0.99: |
| print(" >>> The split is SATURATED: a search-free classical solver already") |
| print(" >>> solves it. 100% is the expected result for any competent method,") |
| print(" >>> and the neural number should NOT be presented as a capability claim.") |
| else: |
| print(f" >>> Not saturated: propagation alone leaves {(1-cp_rate)*100:.1f}% unsolved,") |
| print(" >>> so the benchmark does discriminate between methods.") |
|
|
| print() |
| print("=" * 78) |
| print("2. IS THE MARGIN STATISTICALLY REAL?") |
| print("=" * 78) |
| runs = defaultdict(list) |
| for f in sorted(glob.glob(os.path.join(a.runs, "sud1-*/result.json"))): |
| r = json.load(open(f)) |
| arg = r["args"] |
| runs[(arg["mode"], "aug" if arg.get("augment") else "plain")].append(r) |
|
|
| for key in sorted(runs): |
| rs = runs[key] |
| best = max((max(r["decode"].values(), key=lambda v: v["board"]) for r in rs), |
| key=lambda v: v["board"]) |
| per_seed = [max(r["decode"].values(), key=lambda v: v["board"])["board"] for r in rs] |
| k = int(round(np.mean(per_seed) * len(Xte))) |
| lo, hi = wilson(k, len(Xte)) |
| pv = binom_p(k, len(Xte), 0.983) |
| print(f" {key[0]}/{key[1]:<6} best {np.mean(per_seed)*100:6.2f}% " |
| f"95% CI [{lo*100:.2f}, {hi*100:.2f}] per-seed {[round(x*100,2) for x in per_seed]}" |
| f" p(vs 98.3%)={pv:.2g}") |
| out[f"{key[0]}/{key[1]}"] = {"mean": float(np.mean(per_seed)), |
| "per_seed": per_seed, "ci": [lo, hi], "p_vs_satnet": pv} |
|
|
| print() |
| print("=" * 78) |
| print(f"3. DOES IT GENERALISE TO HARDER PUZZLES? (stripping clues, uniqueness verified)") |
| print("=" * 78) |
| rng = np.random.default_rng(0) |
| hard = {} |
| for target in (30, 26, 22): |
| made, tries = [], 0 |
| for idx in range(len(Xte)): |
| if len(made) >= a.n_hard or tries > a.n_hard * 12: |
| break |
| tries += 1 |
| sol = Yte[idx] |
| cells = list(rng.permutation(CELLS)) |
| g = list(sol) |
| removed = 0 |
| for c in cells: |
| if CELLS - removed <= target: |
| break |
| keep = g[c] |
| g[c] = 0 |
| if count_solutions(g, 2) == 1: |
| removed += 1 |
| else: |
| g[c] = keep |
| if sum(1 for v in g if v) <= target + 2: |
| made.append((np.array(g), sol)) |
| if made: |
| P = np.stack([m[0] for m in made]) |
| S = np.stack([m[1] for m in made]) |
| cp = sum(1 for i in range(len(P)) |
| if (lambda r: r is not None and all(v > 0 for v in r) |
| and np.array_equal(r, S[i]))(propagate(P[i]))) |
| hard[target] = {"n": len(P), "clues": float((P > 0).sum(1).mean()), |
| "classical_propagation": cp / len(P)} |
| print(f" target ~{target} clues: built {len(P)} unique puzzles " |
| f"(mean {(P>0).sum(1).mean():.1f} clues) " |
| f"constraint propagation solves {cp/len(P)*100:.1f}%") |
| np.save(os.path.join(os.path.dirname(a.out) or ".", f"hard_{target}_puz.npy"), P) |
| np.save(os.path.join(os.path.dirname(a.out) or ".", f"hard_{target}_sol.npy"), S) |
| out["harder"] = hard |
|
|
| os.makedirs(os.path.dirname(a.out) or ".", exist_ok=True) |
| json.dump(out, open(a.out, "w"), indent=2, default=float) |
| print(f"\nwrote {a.out}") |
| print("harder puzzle sets saved next to it for the model to be evaluated on") |
|
|
