solver: break board dihedral symmetry

Constrain the unique unit square to a closed D4 fundamental region once its placement is known. This preserves one representative of every board-orientation orbit without assigning identities to repeated squares.

Keep a symmetry-disabled benchmark path, document the proof and measurements, and cover generic, diagonal, midline, corner, and centre orbits.

Tests: Release, Debug, ASan, and UBSan CTest (11 passed each)

Refs: #3
This commit was merged in pull request #25.
This commit is contained in:
Codex instance
2026-07-30 18:18:45 +01:00
parent 74bde266d0
commit f37e08768d
7 changed files with 284 additions and 28 deletions
+47
View File
@@ -18,6 +18,9 @@ the probe renders into an in-memory stream so grids do not perturb terminal I/O.
Override the policy with `--orders`, `--warmup`, `--repetitions`, `--timeout`,
and `--candidate-order`. The choices are `ascending`, `descending`, and
`best-fit`; ascending candidate sizes are the production default.
The production default also removes equivalent D4 board orientations by
constraining the unique unit square. Pass `--no-symmetry` to obtain an
otherwise identical unconstrained baseline.
Order 9 uses the constructive odd-order path, searching order 8 and then tiling
the enlarged border, so it is suitable for normal local benchmarking:
@@ -69,6 +72,50 @@ Do not use wall-clock thresholds as correctness checks. Keep the generated
JSON outside version control unless it is being deliberately added as a named
comparison baseline.
## D4 board symmetry
Every solution contains exactly one 1-by-1 square. Rotations and reflections
of the whole board preserve square sizes, multiplicities, and coverage, so the
unit square can select the orientation without assigning identities to any of
the repeated larger squares. For a board of width `W`, the solver accepts the
unit square only in the closed fundamental triangle
`x <= y <= floor((W - 1) / 2)`. Reflecting a cell toward the left edge,
swapping its coordinates if necessary, and reflecting toward the top edge
maps every D4 orbit into this triangle. Closed diagonal and midline
boundaries retain the smaller orbits of symmetric cells.
The check is made only when the skyline search is ready to place the unit
square, so it never rejects a partial state before the square's position is
decidable. The implementation remains compile-time counter-free in normal
solver calls and keeps the single-threaded deterministic search policy.
Instrumented runs count examined and rejected unit-square placements as prune
checks and hits.
Measurements used the issue #3 dirty working tree based on commit `74bde26`,
Apple Clang 21.0.0, `-O3 -DNDEBUG`, macOS arm64, one worker, one warm-up, and
five sequential measured repetitions. All results passed the benchmark's
independent cell-coverage validator and counts were stable:
| Route | D4 constraint | Median solve (range) | Nodes | Prune hits |
| --- | --- | ---: | ---: | ---: |
| Order 8 public | enabled | 0.245 s (0.244-0.248 s) | 2,931,203 | 1,329,567 |
| Order 8 public | disabled | 0.679 s (0.659-0.709 s) | 7,735,369 | 0 |
| Order 9 direct | enabled | 1.705 s (1.671-1.740 s) | 16,231,918 | 6,755,171 |
| Order 9 direct | disabled | 4.542 s (4.482-4.662 s) | 45,840,266 | 0 |
Thus the constraint reduced nodes by 62% for order 8 and 65% for direct order
9; counted median solve time fell by 64% and 62%, respectively.
A public order-10 probe with the D4 constraint, ascending policy, and a
45-second per-process bound did not complete. Public order 11 first performs
that identical order-10 core search and only then adds its inexpensive odd
border, so adding either order to routine correctness tests would duplicate
the same unresolved bottleneck. They remain useful opt-in heavyweight
benchmark targets with explicit timeouts. A direct order-11 benchmark is a
different experiment: it bypasses the public odd construction and searches
the larger core itself, so it must not be presented as public order-11
performance.
## Smallest-valley skyline
The solver stores one filled height per board column instead of one value per