Codex instance
0a7ce1e49e
Provide a separately installed OR-Tools model to compare a generic constraint solver with the native first-solution path without adding a production or default-test dependency. Use no-overlap, exact-fill, edge and equal-copy symmetry constraints, validate placements independently, and record model size, memory, worker count and timings for orders 8 and 9. Keep the tool only as a reference and defer DLX absent new evidence. Tests: Release CTest (9 passed) Tests: Python reference tests and compilation checks Tests: independently validated CP-SAT orders 8 and 9 Refs: #5
118 lines
5.2 KiB
Markdown
118 lines
5.2 KiB
Markdown
# 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:
|
||
|
||
- <https://zayenz.se/blog/post/partridge-packing/> for exact fill, edge
|
||
exclusions, and identical-piece ordering;
|
||
- <https://or-tools.github.io/docs/pdoc/ortools/sat/python/cp_model> for the
|
||
current fixed-size interval and `add_no_overlap_2d` APIs;
|
||
- <https://developers.google.com/optimization/install/> 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
|
||
<https://www.tunbury.org/2025/12/17/partridge-puzzle/> 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.
|