research: benchmark CP-SAT as a reference solver #5

Closed
opened 2026-07-30 16:23:33 +01:00 by mcp · 1 comment
Collaborator

Background

A recent MiniZinc/OR-Tools CP-SAT model used no-overlap, exact row/column fill, edge-placement restrictions and identical-piece symmetry breaking to solve orders 8 through 11. It provides a useful external performance and correctness reference, although bespoke skyline search appears more promising.

Generic DLX and SAT attempts have also struggled with the large placement matrix and identical-copy symmetry.

Proposed work

  • Build a disposable or optional CP-SAT reference model.
  • Use interval coordinates, NoOverlap2D, exact-fill reasoning, edge exclusions and lexicographic ordering of equal sizes.
  • Configure first-solution search and available workers.
  • Compare output and time against the bespoke solver.
  • Record why DLX is not pursued unless new evidence changes the tradeoff.

Acceptance criteria

  • CP-SAT solutions pass the same independent validator as native solutions.
  • Report model size, memory, workers and elapsed time for feasible representative orders.
  • Keep external solver dependencies optional.
  • Make a documented keep/remove decision after benchmarking.

References

## Background A recent MiniZinc/OR-Tools CP-SAT model used no-overlap, exact row/column fill, edge-placement restrictions and identical-piece symmetry breaking to solve orders 8 through 11. It provides a useful external performance and correctness reference, although bespoke skyline search appears more promising. Generic DLX and SAT attempts have also struggled with the large placement matrix and identical-copy symmetry. ## Proposed work - Build a disposable or optional CP-SAT reference model. - Use interval coordinates, `NoOverlap2D`, exact-fill reasoning, edge exclusions and lexicographic ordering of equal sizes. - Configure first-solution search and available workers. - Compare output and time against the bespoke solver. - Record why DLX is not pursued unless new evidence changes the tradeoff. ## Acceptance criteria - CP-SAT solutions pass the same independent validator as native solutions. - Report model size, memory, workers and elapsed time for feasible representative orders. - Keep external solver dependencies optional. - Make a documented keep/remove decision after benchmarking. ## References - https://zayenz.se/blog/post/partridge-packing/ - https://www.tunbury.org/2025/12/17/partridge-puzzle/
Author
Collaborator

Implementation decision and review record:

  • Keep CP-SAT as an optional Python research/reference tool; do not add OR-Tools to the native build or default test dependencies.
  • Model named square copies with interval coordinates, NoOverlap2D, exact row/column fill, conservative edge exclusions, and strict lexicographic ordering of equal-size placements.
  • Configure an explicit worker count, a time limit, and first-feasible termination.
  • Validate every reported solution with a dependency-free validator implementing the same dimensions, multiplicity, bounds, overlap, and complete-coverage contract as the native independent tests.
  • Keep the reference implementation after benchmarking, but not as the production architecture. Do not pursue DLX without new evidence because the placement matrix and identical-copy symmetry remain unfavorable.

Review strengthened validator parity tests, subprocess-error/model-stability reporting, generated-artifact ignores, and documentation of the separate validator implementation. Final review found no outstanding correctness or scope issues.

Verification:

  • Release CTest with system Python and no OR-Tools dependency: 9/9 passed.
  • Optional OR-Tools 9.15.6755 tests in a Python 3.13.14 scoped virtual environment: passed.
  • Python compilation checks: passed.
  • Independent review run of order 8: valid, 36 pieces, 2,664 variables, 5,497 constraints, 244,006-byte model.
  • git diff --check: clean.

Recorded comparison on 8 logical CPUs:

  • Order 8 CP-SAT, 8 workers, 3 valid runs: 2.080 s median (2.019–3.046 s), 220,364,800–231,702,528 bytes peak RSS.
  • Native order 8, 1 worker, 3 valid runs: 1.854 s median (1.852–1.866 s).
  • Order 9 CP-SAT, 8 workers, one valid observation: 54.623 s, 363,888,640 bytes peak RSS, 45 pieces, 4,140 variables, 8,493 constraints, 377,709-byte model.
  • Native order 9 construction, 1 worker: 1.846 s predecessor-search median plus 0.250 microseconds construction.

The order-9 CP-SAT number is a single stochastic observation, and ru_maxrss is whole-process high-water memory rather than solver-only allocation.

References used: the issue's MiniZinc/CP-SAT and DLX reports, current OR-Tools Python API documentation, and Google’s optional virtual-environment installation guidance.

Implementation decision and review record: - Keep CP-SAT as an optional Python research/reference tool; do not add OR-Tools to the native build or default test dependencies. - Model named square copies with interval coordinates, `NoOverlap2D`, exact row/column fill, conservative edge exclusions, and strict lexicographic ordering of equal-size placements. - Configure an explicit worker count, a time limit, and first-feasible termination. - Validate every reported solution with a dependency-free validator implementing the same dimensions, multiplicity, bounds, overlap, and complete-coverage contract as the native independent tests. - Keep the reference implementation after benchmarking, but not as the production architecture. Do not pursue DLX without new evidence because the placement matrix and identical-copy symmetry remain unfavorable. Review strengthened validator parity tests, subprocess-error/model-stability reporting, generated-artifact ignores, and documentation of the separate validator implementation. Final review found no outstanding correctness or scope issues. Verification: - Release CTest with system Python and no OR-Tools dependency: 9/9 passed. - Optional OR-Tools 9.15.6755 tests in a Python 3.13.14 scoped virtual environment: passed. - Python compilation checks: passed. - Independent review run of order 8: valid, 36 pieces, 2,664 variables, 5,497 constraints, 244,006-byte model. - `git diff --check`: clean. Recorded comparison on 8 logical CPUs: - Order 8 CP-SAT, 8 workers, 3 valid runs: 2.080 s median (2.019–3.046 s), 220,364,800–231,702,528 bytes peak RSS. - Native order 8, 1 worker, 3 valid runs: 1.854 s median (1.852–1.866 s). - Order 9 CP-SAT, 8 workers, one valid observation: 54.623 s, 363,888,640 bytes peak RSS, 45 pieces, 4,140 variables, 8,493 constraints, 377,709-byte model. - Native order 9 construction, 1 worker: 1.846 s predecessor-search median plus 0.250 microseconds construction. The order-9 CP-SAT number is a single stochastic observation, and `ru_maxrss` is whole-process high-water memory rather than solver-only allocation. References used: the issue's MiniZinc/CP-SAT and DLX reports, current OR-Tools Python API documentation, and Google’s optional virtual-environment installation guidance.
mcp closed this issue 2026-07-30 17:41:02 +01:00
Sign in to join this conversation.
No labels
1 Participants
Notifications
Due Date
No due date set.
Dependencies

No dependencies set.

Reference: mgrettondann/partridge-cpp#5