diff --git a/.gitignore b/.gitignore index 625fade..e7335ce 100644 --- a/.gitignore +++ b/.gitignore @@ -1 +1,5 @@ cmake-build*/ +build*/ +.venv*/ +__pycache__/ +*.pyc diff --git a/BENCHMARKING.md b/BENCHMARKING.md index 3579fa9..e24bd8f 100644 --- a/BENCHMARKING.md +++ b/BENCHMARKING.md @@ -109,3 +109,6 @@ was necessarily dirty with the issue 6 implementation. New optimization issues should quote the exact JSON environment, policy, median/spread, stable counters, and counted overhead from this runner for both before and after revisions. + +The separate optional CP-SAT reference benchmark and its model, memory, worker, +and timing report are documented in [CP_SAT_REFERENCE.md](./CP_SAT_REFERENCE.md). diff --git a/CMakeLists.txt b/CMakeLists.txt index 19f79ed..758e28c 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -29,5 +29,8 @@ if(BUILD_TESTING) add_test(NAME benchmark-format COMMAND "${Python3_EXECUTABLE}" "${CMAKE_CURRENT_SOURCE_DIR}/benchmarks/run.py" --self-test) + add_test(NAME reference-support + COMMAND "${Python3_EXECUTABLE}" + "${CMAKE_CURRENT_SOURCE_DIR}/tests/reference_test.py") endif() endif() diff --git a/CP_SAT_REFERENCE.md b/CP_SAT_REFERENCE.md new file mode 100644 index 0000000..5d01cec --- /dev/null +++ b/CP_SAT_REFERENCE.md @@ -0,0 +1,117 @@ +# Optional CP-SAT reference + +Issue #5 evaluated a CP-SAT model as a correctness and performance reference. +It is deliberately isolated from the C++ build: CMake, the native executable, +and the normal CTest suite do not require OR-Tools. + +## Setup and use + +Google recommends installing the Python wheel with `pip` in a virtual +environment. From the repository root: + +```sh +python3 -m venv .venv-cp-sat +.venv-cp-sat/bin/python -m pip install -r requirements-cp-sat.txt +.venv-cp-sat/bin/python tools/cp_sat_reference.py 8 --workers 8 \ + --time-limit 600 > cp-sat-order-8.json +``` + +The report includes the OR-Tools version, available and selected workers, +first-solution setting, model variable/constraint and serialized sizes, build, +solve and independent-validation times, process peak RSS, solver statistics, +placements, and validator diagnostics. `ru_maxrss` is a high-water mark for +the complete Python process, not a solver-only allocation measurement. + +For repeated measurements: + +```sh +.venv-cp-sat/bin/python benchmarks/run_cp_sat.py \ + --solver tools/cp_sat_reference.py --order 8 --workers 8 \ + --repetitions 3 --time-limit 600 > cp-sat-benchmark.json +``` + +Generated reports are not versioned. The dependency-free validator can also +check the `solution` member extracted from a report: + +```sh +python3 tools/partridge_validator.py solution.json +``` + +## Recorded order-8 comparison + +On 30 July 2026, three measured runs used OR-Tools 9.15.6755, Python +3.13.14, macOS arm64, all 8 available logical CPUs/workers, first-solution +search, and a 600-second limit per run. All solutions passed independent +validation and the model was stable across runs: + +| Metric | Result | +| --- | ---: | +| Pieces | 36 | +| Variables | 2,664 | +| Constraints | 5,497 | +| Exact-fill literals | 2,592 | +| Edge exclusions | 140 | +| Serialized model | 244,006 bytes | +| Solve time | 2.080 s median (2.019–3.046 s) | +| Process peak RSS | 220,364,800–231,702,528 bytes | + +One order-9 CP-SAT run with the same dependency and all 8 workers also passed +independent validation. Its model contained 45 pieces, 4,140 variables, 8,493 +constraints, 4,050 exact-fill literals, 176 edge exclusions, and a 377,709-byte +serialized proto. It solved in 54.623 seconds and the process peak RSS was +363,888,640 bytes. This is a single observation rather than a distribution. + +The native Release benchmark on the same machine used one worker and one +warm-up followed by three instrumented measurements. It also produced valid +solutions, with stable counters and a 1.854-second solve median +(1.852–1.866 seconds) for order 8. Order 9 uses the native odd-order +construction: its predecessor search median was 1.846 seconds +(1.840–1.848 seconds), and construction took 0.250 microseconds median. These +are first-feasible timings, not proof-time or solution-enumeration +measurements. CP-SAT is competitive at order 8 but uses eight workers and a +much larger runtime dependency, and it is substantially slower than native +construction at order 9; the comparison does not justify replacing the native +solver. + +## Model + +There are `side` named copies of every square size from 1 through the order. +Each copy has integer x/y starts and fixed-size x/y intervals constrained by +`NoOverlap2D`. Exact-fill constraints require the sizes of all intervals +covering every row and column to sum to the board side. Positions that would +leave an edge strip whose area cannot be filled by smaller pieces are excluded. +Copies of an equal size are strictly ordered by `(x, y)` encoded as +`x * board_side + y`. CP-SAT uses all explicitly selected workers and stops +after its first feasible solution. + +The validator is independent of OR-Tools and checks dimensions, bounds, +multiplicity, pairwise cell occupancy, and complete coverage. It implements +the same validation contract as the independent native test validator, rather +than sharing its C++ implementation. Its known-order-8 and invalid-case tests +mirror the native validator tests. It can also be used for native placements, +so solver constraints are not treated as proof of correctness. + +The model follows: + +- for exact fill, edge + exclusions, and identical-piece ordering; +- for the + current fixed-size interval and `add_no_overlap_2d` APIs; +- for optional virtual + environment installation. + +## Decision + +Keep the model as an optional, disposable research/reference tool; do not make +it a production solver or a required dependency. It provides an independently +validated second implementation and useful solver statistics, while the native +specialized search and odd-order construction remain simpler to distribute and +benchmark. + +Do not pursue DLX without new evidence. A cell-placement exact-cover matrix is +large, and identical square copies introduce substantial symmetric +arrangements. The reported DLX and SAT attempts at + did not find a practical +order-9 route even after ordering reduced memory. CP-SAT can express the +global no-overlap, per-line fill reasoning, edge exclusions, and copy ordering +directly; a fresh DLX experiment is not justified by the present evidence. diff --git a/README.md b/README.md index 4ff9fce..05e948e 100644 --- a/README.md +++ b/README.md @@ -66,3 +66,7 @@ instructions. Performance measurements use the separate opt-in suite described in [BENCHMARKING.md](./BENCHMARKING.md). + +The research-only OR-Tools comparison is optional and documented in +[CP_SAT_REFERENCE.md](./CP_SAT_REFERENCE.md). It does not affect the native +build or its dependencies. diff --git a/TESTING.md b/TESTING.md index 7af94d4..dfd1eb9 100644 --- a/TESTING.md +++ b/TESTING.md @@ -17,6 +17,11 @@ checks that its search counters exactly match order 8. The rendering test also formats the known order-8 solution and checks the resulting grid dimensions and coverage. +When Python is available, `reference-support` also tests the dependency-free +placement JSON validator. If the optional OR-Tools package is present, it +additionally builds and solves the trivial order-1 CP-SAT model; otherwise that +part is skipped without changing the default test result. + ## Debug and sanitizers Use a separate build directory for each configuration: diff --git a/benchmarks/run_cp_sat.py b/benchmarks/run_cp_sat.py new file mode 100644 index 0000000..fbb5207 --- /dev/null +++ b/benchmarks/run_cp_sat.py @@ -0,0 +1,82 @@ +#!/usr/bin/env python3 +"""Repeat the optional CP-SAT reference and summarize its JSON reports.""" + +from __future__ import annotations + +import argparse +import json +import statistics +import subprocess +import sys +from pathlib import Path + + +def main() -> int: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--solver", type=Path, required=True) + parser.add_argument("--order", type=int, default=8) + parser.add_argument("--workers", type=int, required=True) + parser.add_argument("--repetitions", type=int, default=3) + parser.add_argument("--time-limit", type=float, default=600) + args = parser.parse_args() + if args.repetitions < 1: + parser.error("repetitions must be positive") + + runs = [] + process_errors = [] + for _ in range(args.repetitions): + command = [ + sys.executable, + str(args.solver), + str(args.order), + "--workers", + str(args.workers), + "--time-limit", + str(args.time_limit), + ] + process = subprocess.run(command, text=True, capture_output=True) + try: + report = json.loads(process.stdout) + except json.JSONDecodeError as error: + parser.exit(1, f"reference produced invalid JSON: {error}\n{process.stderr}") + runs.append(report) + if process.returncode != 0: + process_errors.append( + { + "returncode": process.returncode, + "stderr": process.stderr, + "status": report.get("result", {}).get("status"), + } + ) + + completed = [run for run in runs if run["result"]["valid"]] + solve_times = [run["timing_seconds"]["solve"] for run in completed] + first_model = runs[0]["model"] + model_stable = all(run["model"] == first_model for run in runs) + output = { + "schema": "partridge-cp-sat-benchmark-v1", + "order": args.order, + "workers": args.workers, + "repetitions": args.repetitions, + "completed": len(completed), + "model": first_model, + "model_stable": model_stable, + "process_errors": process_errors, + "peak_rss_bytes": [run["memory"]["peak_rss_bytes"] for run in runs], + "solve_seconds": solve_times, + "solve_median_seconds": statistics.median(solve_times) if solve_times else None, + "runs": runs, + } + json.dump(output, sys.stdout, indent=2, sort_keys=True) + sys.stdout.write("\n") + return ( + 0 + if len(completed) == args.repetitions + and not process_errors + and model_stable + else 1 + ) + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/requirements-cp-sat.txt b/requirements-cp-sat.txt new file mode 100644 index 0000000..e54923d --- /dev/null +++ b/requirements-cp-sat.txt @@ -0,0 +1,2 @@ +# Optional research dependency; not used by the build or default solver. +ortools>=9.14,<10 diff --git a/tests/reference_test.py b/tests/reference_test.py new file mode 100644 index 0000000..43232f7 --- /dev/null +++ b/tests/reference_test.py @@ -0,0 +1,83 @@ +#!/usr/bin/env python3 +"""Dependency-free tests for the CP-SAT reference support code.""" + +from __future__ import annotations + +import importlib.util +import json +import subprocess +import sys +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[1] +sys.path.insert(0, str(ROOT / "tools")) +from partridge_validator import validate # noqa: E402 + + +KNOWN_ORDER_8 = { + "order": 8, + "board_side": 36, + "placements": [ + {"x": x, "y": y, "side": side} + for x, y, side in [ + (0, 0, 8), (8, 0, 8), (16, 0, 8), (24, 0, 8), + (32, 0, 4), (32, 4, 4), (0, 8, 8), (8, 8, 8), + (16, 8, 8), (24, 8, 6), (30, 8, 6), (24, 14, 5), + (29, 14, 7), (0, 16, 6), (6, 16, 3), (9, 16, 8), + (17, 16, 7), (6, 19, 3), (24, 19, 5), (29, 21, 7), + (0, 22, 7), (7, 22, 2), (17, 23, 1), (18, 23, 6), + (7, 24, 6), (13, 24, 5), (24, 24, 5), (29, 28, 3), + (32, 28, 4), (0, 29, 7), (13, 29, 7), (20, 29, 7), + (27, 29, 2), (7, 30, 6), (27, 31, 5), (32, 32, 4), + ] + ], +} + + +def main() -> int: + assert validate(KNOWN_ORDER_8) == [] + + invalid = json.loads(json.dumps(KNOWN_ORDER_8)) + invalid["placements"].pop() + diagnostics = validate(invalid) + assert any("side 4 has multiplicity 3; expected 4" in d for d in diagnostics) + assert any("not completely covered" in d for d in diagnostics) + + invalid = json.loads(json.dumps(KNOWN_ORDER_8)) + invalid["placements"][0]["x"] = 36 + diagnostics = validate(invalid) + assert any("outside the board" in diagnostic for diagnostic in diagnostics) + assert any("not completely covered" in diagnostic for diagnostic in diagnostics) + + invalid = json.loads(json.dumps(KNOWN_ORDER_8)) + invalid["placements"][1]["x"] = invalid["placements"][0]["x"] + invalid["placements"][1]["y"] = invalid["placements"][0]["y"] + diagnostics = validate(invalid) + assert any("overlaps placement 0" in diagnostic for diagnostic in diagnostics) + + invalid = json.loads(json.dumps(KNOWN_ORDER_8)) + invalid["placements"][0]["side"] = 9 + diagnostics = validate(invalid) + assert any("invalid side length" in diagnostic for diagnostic in diagnostics) + + if importlib.util.find_spec("ortools") is not None: + process = subprocess.run( + [ + sys.executable, + str(ROOT / "tools" / "cp_sat_reference.py"), + "1", + "--workers", + "1", + ], + text=True, + capture_output=True, + check=True, + ) + report = json.loads(process.stdout) + assert report["result"]["valid"] + assert validate(report["solution"]) == [] + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/tools/cp_sat_reference.py b/tools/cp_sat_reference.py new file mode 100644 index 0000000..4526201 --- /dev/null +++ b/tools/cp_sat_reference.py @@ -0,0 +1,260 @@ +#!/usr/bin/env python3 +"""Optional OR-Tools CP-SAT reference solver for the Partridge puzzle.""" + +from __future__ import annotations + +import argparse +import importlib.metadata +import json +import os +import resource +import sys +import tempfile +import time +from dataclasses import dataclass +from pathlib import Path +from typing import Any + +sys.path.insert(0, str(Path(__file__).resolve().parent)) +from partridge_validator import validate # noqa: E402 + + +@dataclass +class Piece: + side: int + copy: int + x: Any + y: Any + + +def maximum_rss_bytes() -> int: + rss = resource.getrusage(resource.RUSAGE_SELF).ru_maxrss + # Darwin reports bytes; Linux and the other supported Unix wheels use KiB. + return int(rss if sys.platform == "darwin" else rss * 1024) + + +def minimum_edge_distance(side: int) -> int: + for distance in range(1, side + 1): + available = (distance * (distance + 1) // 2) ** 2 + if distance * side > available: + return distance + raise AssertionError("every non-unit side has a limiting edge distance") + + +def add_edge_exclusions(model: Any, start: Any, side: int, board_side: int) -> int: + if side == 1: + return 0 + distance = minimum_edge_distance(side) + forbidden = list(range(1, distance + 1)) + forbidden += list( + range(board_side - side - distance, board_side - side) + ) + for position in sorted(set(forbidden)): + model.add(start != position) + return len(set(forbidden)) + + +def build_model(order: int, cp_model: Any) -> tuple[Any, list[Piece], dict[str, int]]: + from ortools.util.python.sorted_interval_list import Domain + + board_side = order * (order + 1) // 2 + model = cp_model.CpModel() + pieces: list[Piece] = [] + x_intervals = [] + y_intervals = [] + edge_exclusions = 0 + + for side in range(order, 0, -1): + equal_size: list[Piece] = [] + for copy in range(side): + name = f"s{side}_{copy}" + x = model.new_int_var(0, board_side - side, f"x_{name}") + y = model.new_int_var(0, board_side - side, f"y_{name}") + piece = Piece(side, copy, x, y) + pieces.append(piece) + equal_size.append(piece) + x_intervals.append( + model.new_fixed_size_interval_var(x, side, f"xi_{name}") + ) + y_intervals.append( + model.new_fixed_size_interval_var(y, side, f"yi_{name}") + ) + edge_exclusions += add_edge_exclusions(model, x, side, board_side) + edge_exclusions += add_edge_exclusions(model, y, side, board_side) + + # Strict lexicographic ordering of the (x, y) coordinate pairs. + for before, after in zip(equal_size, equal_size[1:]): + model.add( + before.x * board_side + before.y + < after.x * board_side + after.y + ) + + model.add_no_overlap_2d(x_intervals, y_intervals) + + exact_fill_literals = 0 + for axis in ("x", "y"): + for line in range(board_side): + contributions = [] + for index, piece in enumerate(pieces): + start = getattr(piece, axis) + overlaps = model.new_bool_var(f"{axis}_{line}_covers_{index}") + overlap_domain = Domain.from_intervals( + [[line - piece.side + 1, line]] + ) + model.add_linear_expression_in_domain( + start, overlap_domain + ).only_enforce_if(overlaps) + model.add_linear_expression_in_domain( + start, overlap_domain.complement() + ).only_enforce_if(overlaps.negated()) + contributions.append(piece.side * overlaps) + exact_fill_literals += 1 + model.add(sum(contributions) == board_side) + + return model, pieces, { + "pieces": len(pieces), + "edge_exclusions": edge_exclusions, + "exact_fill_literals": exact_fill_literals, + } + + +def model_proto(model: Any) -> Any: + if hasattr(model, "proto"): + return model.proto + return model.Proto() + + +def serialized_model_size(model: Any) -> int: + """Return the binary proto size across old protobuf and new pybind APIs.""" + proto = model_proto(model) + if hasattr(proto, "SerializeToString"): + return len(proto.SerializeToString()) + descriptor, path = tempfile.mkstemp(suffix=".bin") + os.close(descriptor) + try: + if not model.export_to_file(path): + raise RuntimeError("OR-Tools could not export the model proto") + return os.path.getsize(path) + finally: + os.unlink(path) + + +def solve(order: int, workers: int, time_limit: float | None) -> dict[str, Any]: + try: + from ortools.sat.python import cp_model + except ImportError as error: + raise RuntimeError( + "OR-Tools is optional and is not installed; see " + "CP_SAT_REFERENCE.md for virtual-environment instructions" + ) from error + + initial_rss = maximum_rss_bytes() + build_begin = time.perf_counter() + model, pieces, counts = build_model(order, cp_model) + build_seconds = time.perf_counter() - build_begin + proto = model_proto(model) + model_stats = { + **counts, + "variables": len(proto.variables), + "constraints": len(proto.constraints), + "serialized_bytes": serialized_model_size(model), + } + + solver = cp_model.CpSolver() + solver.parameters.num_search_workers = workers + solver.parameters.stop_after_first_solution = True + if time_limit is not None: + solver.parameters.max_time_in_seconds = time_limit + + solve_begin = time.perf_counter() + status = solver.solve(model) + solve_seconds = time.perf_counter() - solve_begin + feasible = status in (cp_model.FEASIBLE, cp_model.OPTIMAL) + board_side = order * (order + 1) // 2 + placements = ( + [ + { + "x": solver.value(piece.x), + "y": solver.value(piece.y), + "side": piece.side, + } + for piece in pieces + ] + if feasible + else [] + ) + solution = { + "order": order, + "board_side": board_side, + "placements": placements, + } + validation_begin = time.perf_counter() + diagnostics = validate(solution) if feasible else ["no solution produced"] + validation_seconds = time.perf_counter() - validation_begin + peak_rss = maximum_rss_bytes() + + return { + "schema": "partridge-cp-sat-reference-v1", + "dependency": { + "name": "ortools", + "version": importlib.metadata.version("ortools"), + "optional": True, + }, + "configuration": { + "workers": workers, + "available_cpus": os.cpu_count(), + "first_solution": True, + "time_limit_seconds": time_limit, + }, + "model": model_stats, + "result": { + "status": solver.status_name(status), + "feasible": feasible, + "valid": feasible and not diagnostics, + "diagnostics": diagnostics, + }, + "timing_seconds": { + "build": build_seconds, + "solve": solve_seconds, + "solver_wall": solver.wall_time, + "validation": validation_seconds, + }, + "memory": { + "initial_rss_bytes": initial_rss, + "peak_rss_bytes": peak_rss, + "peak_rss_increase_bytes": max(0, peak_rss - initial_rss), + }, + "solution": solution, + "solver_stats": solver.response_stats(), + } + + +def main() -> int: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("order", type=int) + parser.add_argument( + "--workers", + type=int, + default=max(1, os.cpu_count() or 1), + help="CP-SAT search workers (default: all available logical CPUs)", + ) + parser.add_argument("--time-limit", type=float) + args = parser.parse_args() + if args.order < 1: + parser.error("order must be positive") + if args.workers < 1: + parser.error("workers must be positive") + if args.time_limit is not None and args.time_limit <= 0: + parser.error("time limit must be positive") + + try: + report = solve(args.order, args.workers, args.time_limit) + except RuntimeError as error: + parser.exit(2, f"{error}\n") + json.dump(report, sys.stdout, indent=2, sort_keys=True) + sys.stdout.write("\n") + return 0 if report["result"]["valid"] else 1 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/tools/partridge_validator.py b/tools/partridge_validator.py new file mode 100644 index 0000000..7f468f3 --- /dev/null +++ b/tools/partridge_validator.py @@ -0,0 +1,97 @@ +#!/usr/bin/env python3 +"""Dependency-free independent validator for Partridge placement JSON.""" + +from __future__ import annotations + +import argparse +import json +import sys +from typing import Any + + +def validate(document: dict[str, Any]) -> list[str]: + """Return diagnostics for a placement document, or an empty list.""" + diagnostics: list[str] = [] + try: + order = int(document["order"]) + board_side = int(document["board_side"]) + placements = document["placements"] + except (KeyError, TypeError, ValueError) as error: + return [f"invalid document: {error}"] + + expected_side = order * (order + 1) // 2 + if order < 1: + diagnostics.append("order must be positive") + if board_side != expected_side: + diagnostics.append( + f"board side is {board_side}; expected triangular number {expected_side}" + ) + if not isinstance(placements, list): + return diagnostics + ["placements must be a list"] + if board_side < 0: + return diagnostics + ["board side must not be negative"] + + multiplicities = [0] * (max(order, 0) + 1) + occupied = [-1] * (board_side * board_side) + for index, raw in enumerate(placements): + try: + x = int(raw["x"]) + y = int(raw["y"]) + side = int(raw["side"]) + except (KeyError, TypeError, ValueError) as error: + diagnostics.append(f"placement {index} is malformed: {error}") + continue + + description = f"placement {index} at ({x}, {y}) with side {side}" + if side < 1 or side > order: + diagnostics.append(f"{description} has an invalid side length") + continue + multiplicities[side] += 1 + if x < 0 or y < 0 or x + side > board_side or y + side > board_side: + diagnostics.append(f"{description} is outside the board bounds") + continue + + overlap = -1 + for row in range(y, y + side): + for column in range(x, x + side): + cell = column + row * board_side + if occupied[cell] != -1: + overlap = occupied[cell] + else: + occupied[cell] = index + if overlap != -1: + diagnostics.append(f"{description} overlaps placement {overlap}") + + for side in range(1, order + 1): + if multiplicities[side] != side: + diagnostics.append( + f"side {side} has multiplicity {multiplicities[side]}; expected {side}" + ) + if -1 in occupied: + diagnostics.append("board is not completely covered") + return diagnostics + + +def main() -> int: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument( + "input", + nargs="?", + type=argparse.FileType("r", encoding="utf-8"), + default=sys.stdin, + ) + args = parser.parse_args() + document = json.load(args.input) + diagnostics = validate(document) + json.dump( + {"valid": not diagnostics, "diagnostics": diagnostics}, + sys.stdout, + indent=2, + sort_keys=True, + ) + sys.stdout.write("\n") + return 0 if not diagnostics else 1 + + +if __name__ == "__main__": + raise SystemExit(main())