ocr_benchmark.py

from ccsolver.ocr_result import load_ocr_levels_from_json as load_ocr_levels
from ccsolver.benchmark import run_benchmark, compare
from ccsolver.solvers.mip_tsp import MTZSolver, DFJSolver
from ccsolver.solvers.z3_hamcycle import Z3HamCycleSolver

ocr_levels = load_ocr_levels("assets_ocr", level_ids=list(range(1000)))
benchmark_levels = [(lid, ocr.to_game()) for lid, ocr in ocr_levels]

mtz_scip = run_benchmark(MTZSolver(backend="SCIP"), benchmark_levels, n=20, output_dir="out/ocr_mtz_scip")
mtz_sat  = run_benchmark(MTZSolver(backend="SAT"),  benchmark_levels, n=20, output_dir="out/ocr_mtz_sat")
dfj_scip = run_benchmark(DFJSolver(backend="SCIP"), benchmark_levels, n=20, output_dir="out/ocr_dfj_scip")
dfj_sat  = run_benchmark(DFJSolver(backend="SAT"),  benchmark_levels, n=20, output_dir="out/ocr_dfj_sat")
z3       = run_benchmark(Z3HamCycleSolver(),               benchmark_levels, n=20, output_dir="out/ocr_z3")

compare([mtz_scip, mtz_sat, dfj_scip, dfj_sat, z3])

# Spot-check: verify solver solutions match the book solutions
print("\n=== Solution verification ===")
for lid, ocr in ocr_levels:
    game = ocr.to_game()
    result = MTZSolver(backend="SCIP").solve(game)
    if result.success:
        diffs = ocr.solution_diff(result.edges, game)
        status = "OK" if not diffs else f"MISMATCH ({len(diffs)} chain(s))"
        print(f"  Level {lid:3d}: {status}")
        for d in diffs:
            print(d)
    else:
        print(f"  Level {lid:3d}: unsolvable")