Merge pull request #38 from SaridakisStamatisChristos/codex/add-swordfish,-simple-coloring,-and-sat-cross-check

Add advanced strategies, SAT cross-check, and demo notebook

Author: SaridakisStamatisChristos

README.md

@@ -87,6 +87,7 @@ sudoku-dlx explain --grid "<81chars>" --json
 #   - pairs: naked pair, hidden pair (row/col/box)
 #   - triples: naked triple, hidden triple (row/col/box)
 #   - fish: X-Wing (rows & columns)
+#   - advanced: Swordfish (rows & columns), Simple Coloring (Rule 2)
 # Deterministic steps for reproducible tutorials.
 
 # Dataset stats
@@ -104,8 +105,20 @@ sudoku-dlx gen   --seed 123 --givens 28 --minimal --symmetry rot180
 
 # Trace & Visualize
 sudoku-dlx solve --grid "<81chars>" --trace out.json
-# Then open web/visualizer.html in your browser and load out.json
-# (works on GitHub Pages)
+# Open web/visualizer.html and load out.json
+```
+
+## Cross-check with SAT (optional)
+Install the optional extra:
+
+```bash
+pip install -e ".[sat]"
+```
+
+Then verify solutions using an independent SAT solver:
+
+```bash
+sudoku-dlx solve --grid "<81chars>" --crosscheck sat
 ```
 
 What this gives you

notebooks/demo.ipynb

@@ -0,0 +1,110 @@
+{
+  "cells": [
+    {
+      "cell_type": "markdown",
+      "metadata": {},
+      "source": [
+        "# Sudoku DLX — Demo Notebook\n",
+        "\n",
+        "This notebook walks through:\n",
+        "1. Generate & analyze a puzzle\n",
+        "2. Solve & capture a trace\n",
+        "3. Review human-style explanation steps\n",
+        "4. (Optional) SAT cross-check\n",
+        "\n",
+        "> Set up locally with `pip install -e \".[dev]\"` and optionally `pip install -e \".[sat]\"`."
+      ]
+    },
+    {
+      "cell_type": "code",
+      "execution_count": null,
+      "metadata": {},
+      "outputs": [],
+      "source": [
+        "from textwrap import dedent\n",
+        "\n",
+        "from sudoku_dlx import analyze, generate, solve, to_string, explain, build_reveal_trace\n",
+        "from sudoku_dlx.crosscheck import sat_solve\n",
+        "\n",
+        "puzzle = generate(seed=123, target_givens=30, minimal=False, symmetry=\"mix\")\n",
+        "print(\"Puzzle:\")\n",
+        "for row in puzzle:\n",
+        "    print(\" \\".join(str(x) if x else \".\" for x in row))\n",
+        "print(\"\nAnalysis:\")\n",
+        "print(analyze(puzzle))"
+      ]
+    },
+    {
+      "cell_type": "code",
+      "execution_count": null,
+      "metadata": {},
+      "outputs": [],
+      "source": [
+        "result = solve([row[:] for row in puzzle])\n",
+        "assert result is not None\n",
+        "print(\"Solved in\", f\"{result.stats.ms:.2f} ms\", \"nodes:\", result.stats.nodes)\n",
+        "print(\"Solution (81):\", to_string(result.grid))\n",
+        "trace = build_reveal_trace(puzzle, result.grid, result.stats)\n",
+        "print(\"Trace keys:\", list(trace.keys()))"
+      ]
+    },
+    {
+      "cell_type": "markdown",
+      "metadata": {},
+      "source": [
+        "### Human-style steps"
+      ]
+    },
+    {
+      "cell_type": "code",
+      "execution_count": null,
+      "metadata": {},
+      "outputs": [],
+      "source": [
+        "explanation = explain(puzzle, max_steps=200)\n",
+        "print(\"Steps:\", len(explanation['steps']))\n",
+        "print(\"Progress:\", explanation['progress'])\n",
+        "print(\"Example step:\", explanation['steps'][0] if explanation['steps'] else None)"
+      ]
+    },
+    {
+      "cell_type": "markdown",
+      "metadata": {},
+      "source": [
+        "### Optional: SAT cross-check\n",
+        "If `python-sat` is installed, the SAT solution should match DLX."
+      ]
+    },
+    {
+      "cell_type": "code",
+      "execution_count": null,
+      "metadata": {},
+      "outputs": [],
+      "source": [
+        "sat_grid = None\n",
+        "try:\n",
+        "    sat_grid = sat_solve(puzzle)\n",
+        "except Exception as exc:\n",
+        "    print(\"SAT unavailable:\", exc)\n",
+        "if sat_grid is not None:\n",
+        "    print(\"SAT solved:\", to_string(sat_grid))\n",
+        "    print(\"Match:\", to_string(sat_grid) == to_string(result.grid))\n",
+        "else:\n",
+        "    print(\"SAT solver not installed. Run pip install -e '.[sat]'\")"
+      ]
+    }
+  ],
+  "metadata": {
+    "kernelspec": {
+      "display_name": "Python 3",
+      "language": "python",
+      "name": "python3"
+    },
+    "language_info": {
+      "name": "python",
+      "pygments_lexer": "ipython3"
+    }
+  },
+  "nbformat": 4,
+  "nbformat_minor": 5
+}

pyproject.toml

@@ -28,6 +28,8 @@ sudoku-dlx = "sudoku_dlx.cli:main"
 
 [project.optional-dependencies]
 dev = ["pytest>=8", "pytest-cov>=5", "ruff>=0.6", "black>=24.8", "pre-commit>=3.7", "hypothesis>=6.113"]
+# optional solver cross-checkers
+sat = ["python-sat>=0.1.8"]
 
 [project.urls]
 Homepage = "https://github.com/SaridakisStamatisChristos/sudoku_dlx"

src/sudoku_dlx/__init__.py

@@ -16,6 +16,7 @@
 from .canonical import canonical_form
 from .generate import generate
 from .rating import rate
+from .crosscheck import sat_solve
 from .solver import (
     SOLVER,
     generate_minimal,
@@ -44,6 +45,7 @@
     "rate",
     "canonical_form",
     "generate",
+    "sat_solve",
     # Legacy exports
     "SOLVER",
     "generate_minimal",

src/sudoku_dlx/cli.py

@@ -4,6 +4,7 @@
 from typing import Optional
 
 from .api import analyze, build_reveal_trace, from_string, is_valid, solve, to_string
+from .crosscheck import sat_solve
 from .explain import explain
 from .canonical import canonical_form
 from .generate import generate
@@ -64,6 +65,7 @@ def yes(b: bool) -> str:
 
 def cmd_solve(ns: argparse.Namespace) -> int:
     grid = from_string(_read_grid_arg(ns))
+    grid_for_crosscheck = [row[:] for row in grid]
     if not is_valid(grid):
         print("Invalid puzzle (duplicate in row/col/box).", file=sys.stderr)
         return 2
@@ -80,6 +82,22 @@ def cmd_solve(ns: argparse.Namespace) -> int:
         outp = pathlib.Path(ns.trace)
         outp.parent.mkdir(parents=True, exist_ok=True)
         outp.write_text(json.dumps(trace, indent=2, sort_keys=True), encoding="utf-8")
+    if ns.crosscheck:
+        if ns.crosscheck == "sat":
+            sat_grid = sat_solve(grid_for_crosscheck)
+            if sat_grid is None:
+                print(
+                    "# crosscheck: SAT solver unavailable (install optional extra: pip install -e '.[sat]')",
+                    file=sys.stderr,
+                )
+            else:
+                ok = to_string(sat_grid) == to_string(result.grid)
+                status = "OK" if ok else "MISMATCH"
+                print(f"# crosscheck[sat]: {status}", file=sys.stderr)
+                if not ok:
+                    print(f"# SAT solution: {to_string(sat_grid)}", file=sys.stderr)
+        else:
+            print(f"# crosscheck: unknown method {ns.crosscheck!r}", file=sys.stderr)
     if ns.stats:
         print(
             f"# solved in {result.stats.ms:.2f} ms · nodes {result.stats.nodes} · backtracks {result.stats.backtracks}",
@@ -349,6 +367,7 @@ def main(argv: Optional[list[str]] = None) -> int:
     solve_parser.add_argument("--pretty", action="store_true", help="print 9x9 grid format")
     solve_parser.add_argument("--stats", action="store_true", help="print timing & node stats to stderr")
     solve_parser.add_argument("--trace", help="write a solution-reveal trace JSON to this path")
+    solve_parser.add_argument("--crosscheck", choices=["sat"], help="verify solution with external solver")
     solve_parser.set_defaults(func=cmd_solve)
 
     rate_parser = sub.add_parser("rate", help="estimate difficulty in [0,10]")

src/sudoku_dlx/crosscheck.py

@@ -0,0 +1,86 @@
+from __future__ import annotations
+
+"""SAT cross-check utilities using python-sat (optional extra)."""
+
+from typing import List, Optional
+
+Grid = List[List[int]]
+
+
+def _var(r: int, c: int, d: int) -> int:
+    """Map (row, col, digit) triples to CNF variables in [1, 729]."""
+
+    return r * 81 + c * 9 + d + 1
+
+
+def _encode_cnf(grid: Grid) -> list[list[int]]:
+    cnf: list[list[int]] = []
+    # 1) Each cell has at least one digit
+    for r in range(9):
+        for c in range(9):
+            cnf.append([_var(r, c, d) for d in range(9)])
+    # 2) Each cell has at most one digit
+    for r in range(9):
+        for c in range(9):
+            for d1 in range(9):
+                for d2 in range(d1 + 1, 9):
+                    cnf.append([-_var(r, c, d1), -_var(r, c, d2)])
+    # 3) Rows: each digit appears exactly once
+    for r in range(9):
+        for d in range(9):
+            cnf.append([_var(r, c, d) for c in range(9)])
+            for c1 in range(9):
+                for c2 in range(c1 + 1, 9):
+                    cnf.append([-_var(r, c1, d), -_var(r, c2, d)])
+    # 4) Columns: each digit appears exactly once
+    for c in range(9):
+        for d in range(9):
+            cnf.append([_var(r, c, d) for r in range(9)])
+            for r1 in range(9):
+                for r2 in range(r1 + 1, 9):
+                    cnf.append([-_var(r1, c, d), -_var(r2, c, d)])
+    # 5) Boxes: each digit appears exactly once
+    for br in range(0, 9, 3):
+        for bc in range(0, 9, 3):
+            cells = [(r, c) for r in range(br, br + 3) for c in range(bc, bc + 3)]
+            for d in range(9):
+                cnf.append([_var(r, c, d) for (r, c) in cells])
+                for i in range(9):
+                    for j in range(i + 1, 9):
+                        r1, c1 = cells[i]
+                        r2, c2 = cells[j]
+                        cnf.append([-_var(r1, c1, d), -_var(r2, c2, d)])
+    # 6) Givens
+    for r in range(9):
+        for c in range(9):
+            v = grid[r][c]
+            if v:
+                cnf.append([_var(r, c, v - 1)])
+    return cnf
+
+
+def sat_solve(grid: Grid) -> Optional[Grid]:
+    """Solve a Sudoku grid via SAT; returns the solved grid or ``None`` if unavailable."""
+
+    try:
+        from pysat.solvers import Minisat22  # type: ignore import-not-found
+    except Exception:
+        return None
+
+    cnf = _encode_cnf(grid)
+    with Minisat22(bootstrap_with=cnf) as solver:
+        if not solver.solve():
+            return None
+        model = solver.get_model()
+
+    solved: Grid = [[0] * 9 for _ in range(9)]
+    for r in range(9):
+        for c in range(9):
+            for d in range(9):
+                if _var(r, c, d) in model:
+                    solved[r][c] = d + 1
+                    break
+    return solved
+
+
+__all__ = ["sat_solve"]