Compare commits
8
Commits
ddf07e730a
..
main
| Author | SHA1 | Date | |
|---|---|---|---|
|
|
39ff5cb340 | ||
|
|
220cec06a9 | ||
|
|
e27427d231 | ||
|
|
f37e08768d | ||
|
|
74bde266d0 | ||
|
|
d751d1b13e | ||
|
|
0a7ce1e49e | ||
|
|
3e667d6de0 |
@@ -1 +1,5 @@
|
||||
cmake-build*/
|
||||
build*/
|
||||
.venv*/
|
||||
__pycache__/
|
||||
*.pyc
|
||||
|
||||
+338
-12
@@ -15,24 +15,46 @@ python3 benchmarks/run.py --binary build-benchmark/partridge_benchmark \
|
||||
The default policy is one unrecorded warm-up followed by five repetitions per
|
||||
case, with a 600-second timeout for each process. Solver stdout is captured;
|
||||
the probe renders into an in-memory stream so grids do not perturb terminal I/O.
|
||||
Override the policy with `--orders`, `--warmup`, `--repetitions`, and
|
||||
`--timeout`. Order 9 is intentionally supported but may be omitted during
|
||||
local iteration because the current solver takes minutes:
|
||||
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.
|
||||
The production default also applies the pruning rules described below.
|
||||
Use `--pruning valley-capacity`, `--pruning large-square`, or
|
||||
`--no-pruning` to measure each rule alone or obtain an unpruned search.
|
||||
Use `--component-pruning gcd`, `--component-pruning subset-sum`, or
|
||||
`--component-pruning none` to compare the component-area rule separately.
|
||||
Component pruning is disabled by default because the measurements below do not
|
||||
recover its cost.
|
||||
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:
|
||||
|
||||
```sh
|
||||
python3 benchmarks/run.py --binary build-benchmark/partridge_benchmark \
|
||||
--orders 7 8 --warmup 1 --repetitions 5 --timeout 60 > benchmark.json
|
||||
--orders 8 9 --warmup 1 --repetitions 5 --timeout 60 > benchmark.json
|
||||
```
|
||||
|
||||
Use `--direct-search` when benchmarking the skyline core rather than the public
|
||||
even-predecessor construction used for odd orders from 9 onwards:
|
||||
|
||||
```sh
|
||||
python3 benchmarks/run.py --binary build-benchmark/partridge_benchmark \
|
||||
--orders 6 7 8 9 --warmup 1 --repetitions 5 --timeout 60 \
|
||||
--candidate-order ascending --direct-search > direct.json
|
||||
```
|
||||
|
||||
The JSON contains every run and median, range, and median absolute deviation
|
||||
for solve, construction, independent validation, and rendering. The current
|
||||
direct-search solver reports zero construction time: its setup and allocation
|
||||
remain part of solve time. The separate construction field is reserved for
|
||||
future constructive solution paths. The document also records compiler,
|
||||
for solve, construction, independent validation, and rendering. Direct-search
|
||||
cases report zero construction time: their setup and allocation remain part of
|
||||
solve time. Constructed odd-order cases report predecessor search and
|
||||
construction separately. The document also records compiler,
|
||||
flags, build type, commit, OS/CPU metadata, worker count, search policy, seed,
|
||||
timeouts, errors, invalid outputs, and the stdout policy. Search counts must
|
||||
be stable across repeated runs. Prune and task counters are zero for the
|
||||
current unpruned, single-threaded solver and reserve stable schema fields for
|
||||
be stable across repeated runs. Prune counters report enabled search rules;
|
||||
they are zero in the corresponding disabled modes. Task counters remain zero
|
||||
for the current single-threaded solver and reserve stable schema fields for
|
||||
later work.
|
||||
|
||||
The runner writes its JSON report before returning a failure status if any mode
|
||||
@@ -58,6 +80,285 @@ 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.
|
||||
|
||||
## Valley-capacity pruning
|
||||
|
||||
For a selected valley, let its rim be the lower height of its two neighbours,
|
||||
treating a board edge as full height. Until the valley reaches that rim, no
|
||||
square wider than the valley can enter it. Therefore the combined area of all
|
||||
remaining squares no wider than the valley must be at least the valley width
|
||||
times its depth below the rim. Rejecting a state when that necessary
|
||||
inequality fails is sound. At widths one and two it provides the usual
|
||||
narrow-gap capacity checks without separate special cases.
|
||||
|
||||
The rule is compiled out of the recursive search in `--no-pruning` mode.
|
||||
Instrumented output records `valley_capacity_checks` and
|
||||
`valley_capacity_prunes` as well as the aggregate pruning counters, allowing
|
||||
enabled and disabled runs to report nodes, checks, hits, and elapsed time.
|
||||
|
||||
Measurements used the issue #10 working tree based on commit `f37e087`, Apple
|
||||
Clang 21.0.0, `-O3 -DNDEBUG`, macOS arm64, one worker, one warm-up, and five
|
||||
measured repetitions. The production ascending policy and D4 constraint were
|
||||
enabled. Every result passed the benchmark's independent validator and all
|
||||
counters were stable:
|
||||
|
||||
| Order | Valley capacity | Median solve (range) | Nodes | Checks | Prunes |
|
||||
| --- | --- | ---: | ---: | ---: | ---: |
|
||||
| 7 exhaustive | enabled | 0.996 s (0.990-0.998 s) | 13,833,048 | 13,833,048 | 7,411,551 |
|
||||
| 7 exhaustive | disabled | 1.110 s (1.109-1.111 s) | 14,997,603 | 0 | 0 |
|
||||
| 8 first solution | enabled | 0.205 s (0.204-0.208 s) | 2,724,096 | 2,724,095 | 1,606,836 |
|
||||
| 8 first solution | disabled | 0.228 s (0.228-0.233 s) | 2,931,203 | 0 | 0 |
|
||||
|
||||
The rule reduced nodes by 7.8% for order 7 and 7.1% for order 8. Its low
|
||||
per-node cost also reduced median counted solve time by 10.3% and 9.9%,
|
||||
respectively, so it remains enabled by default.
|
||||
|
||||
## Remaining-large-square pruning
|
||||
|
||||
For a remaining side `k`, a skyline can contain an empty `k`-by-`k` box only
|
||||
if it has `k` consecutive columns whose filled heights are no greater than the
|
||||
board height minus `k`. A single linear scan tracks qualifying consecutive
|
||||
columns. If no such run exists, the square cannot be placed and the state is
|
||||
infeasible even when its total empty area is sufficient.
|
||||
|
||||
Empty-box feasibility is monotonic in the side length: a box which fits the
|
||||
largest remaining square also fits every smaller remaining size. The solver
|
||||
therefore invokes only one `O(board width)` scan per surviving node, after the
|
||||
cheaper valley-capacity check. It does not attempt an unproven multiplicity
|
||||
bound. `--pruning large-square` measures the rule independently;
|
||||
`--pruning valley-capacity` provides the production baseline without it.
|
||||
Instrumented output records `large_square_checks` and
|
||||
`large_square_prunes`.
|
||||
|
||||
Measurements used the issue #15 working tree based on commit `e27427d`, Apple
|
||||
Clang 21.0.0, `-O3 -DNDEBUG`, macOS arm64, one worker, one warm-up, and seven
|
||||
measured repetitions. Counter-free and counted runs were interleaved; the
|
||||
table reports the counter-free production instantiation. The baseline keeps
|
||||
valley-capacity pruning enabled, so it isolates the new rule. All results
|
||||
passed independent validation and counters were stable:
|
||||
|
||||
| Search | Large-square check | Median solve | Nodes | Checks | Prunes |
|
||||
| --- | --- | ---: | ---: | ---: | ---: |
|
||||
| Order 7 exhaustive | enabled | 0.946 s | 13,221,239 | 6,163,390 | 227,321 |
|
||||
| Order 7 exhaustive | disabled | 0.947 s | 13,833,048 | 0 | 0 |
|
||||
| Order 8 first solution | enabled | 0.195 s | 2,597,678 | 1,063,472 | 38,177 |
|
||||
| Order 8 first solution | disabled | 0.197 s | 2,724,096 | 0 | 0 |
|
||||
| Order 9 direct | enabled | 1.225 s | 14,840,146 | 5,592,843 | 54,900 |
|
||||
| Order 9 direct | disabled | 1.208 s | 14,995,127 | 0 | 0 |
|
||||
|
||||
The rule reduced nodes by 4.4% for order 7, 4.6% for order 8, and 1.0% for
|
||||
direct order 9. Counter-free median time improved by 0.12% and 0.89% on the
|
||||
two distinct searches in the public benchmark set. Public order 9 constructs
|
||||
from the improving order-8 search. Direct order 9, which bypasses that public
|
||||
route, regressed by 1.39%; it remains documented as a caution for future
|
||||
policy tuning.
|
||||
|
||||
Checking only every fourth placement depth was also measured. It retained
|
||||
fewer prunes and was slower than checking every surviving node by 2.2% for
|
||||
order 7, 2.3% for order 8, and 0.6% for direct order 9, so the periodic
|
||||
schedule was rejected. Incremental maintenance would need additional
|
||||
per-size window state and undo logic for an `O(W)` scan whose public net cost
|
||||
is already recovered; it was not added without evidence that the complexity
|
||||
would improve elapsed time. The simple every-node scan remains enabled by
|
||||
default for the measured public benchmark benefit.
|
||||
|
||||
## Component-area pruning
|
||||
|
||||
In a skyline, every non-full column is empty from its filled height to the top
|
||||
of the board. Adjacent non-full columns therefore belong to the same empty
|
||||
component, while a full-height column is an impassable separator. Each
|
||||
remaining square must lie wholly within one such component, so every component
|
||||
area must be the sum of a bounded subset of the remaining square areas.
|
||||
|
||||
The `gcd` mode first rejects a component area which is not divisible by the
|
||||
greatest common divisor of all remaining square areas. The `subset-sum` mode
|
||||
then computes exact reachable areas using each remaining multiplicity as a
|
||||
bound. Each component is checked against the same reachable set; this is a
|
||||
necessary condition, not a claim that independently selected subsets are
|
||||
mutually disjoint.
|
||||
|
||||
The check is triggered only after a placement reaches full board height and
|
||||
can create or extend a component boundary. This keeps the potentially more
|
||||
expensive bounded subset sum off ordinary nodes. Instrumented output records
|
||||
`component_area_checks`, `component_area_prunes`, `component_gcd_prunes`, and
|
||||
`component_subset_prunes`. The three `--component-pruning` modes allow the
|
||||
trigger cost, cheap gcd rule, and bounded subset sum to be compared directly.
|
||||
Use `--component-schedule periodic-8` to compare the event-driven boundary
|
||||
trigger with checking every eighth placement depth.
|
||||
|
||||
Measurements used the issue #13 working tree based on commit `220cec0`, Apple
|
||||
Clang 21.0.0, `-O3 -DNDEBUG`, macOS arm64, one worker, one warm-up, and seven
|
||||
measured repetitions for the boundary-trigger modes. Counter-free and counted
|
||||
runs were interleaved; the table reports counter-free medians. The existing
|
||||
valley-capacity and large-square rules remained enabled. All results passed
|
||||
independent validation and counters were stable:
|
||||
|
||||
| Order | Component rule | Median solve | Nodes | Checks | Prunes |
|
||||
| --- | --- | ---: | ---: | ---: | ---: |
|
||||
| 7 exhaustive | disabled | 0.985 s | 13,221,239 | 0 | 0 |
|
||||
| 7 exhaustive | gcd | 1.027 s | 13,220,729 | 171,088 | 2,568 |
|
||||
| 7 exhaustive | subset sum | 1.052 s | 13,189,961 | 161,706 | 69,483 |
|
||||
| 8 first solution | disabled | 0.203 s | 2,597,678 | 0 | 0 |
|
||||
| 8 first solution | gcd | 0.212 s | 2,597,548 | 23,943 | 637 |
|
||||
| 8 first solution | subset sum | 0.219 s | 2,592,212 | 23,097 | 11,858 |
|
||||
|
||||
Gcd-only checking changed fewer than 0.005% of nodes while slowing the
|
||||
counter-free solver by 4.3% for both orders. Bounded subset sum reduced nodes
|
||||
by only 0.24% for order 7 and 0.21% for order 8, while slowing them by 6.8% and
|
||||
7.5%. Neither rule is enabled by default.
|
||||
|
||||
The boundary trigger is an incremental event check: it runs only when the
|
||||
latest placement reaches full height and can change the component partition.
|
||||
For comparison, subset sum was also sampled every eighth placement depth with
|
||||
one warm-up and three measured repetitions. Periodic checking made 1,501,035
|
||||
checks for order 7 and 290,774 for order 8, versus 161,706 and 23,097 at
|
||||
boundary events. Its counter-free medians were 1.088 s and 0.227 s, 10.5% and
|
||||
11.7% slower than disabled pruning and materially worse than boundary
|
||||
triggering. The periodic schedule is retained only as an opt-in measurement
|
||||
mode; event-triggered checking is the cheaper schedule if component pruning is
|
||||
reconsidered with new evidence.
|
||||
|
||||
## 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
|
||||
cell. Equal adjacent heights form conceptual vertical bars. A valley is a
|
||||
maximal bar lower than both neighbours, with board edges treated as bars of
|
||||
full board height. Each node scans for the smallest-width valley, breaking
|
||||
ties by lower height and then leftmost position, and tries every available
|
||||
square which fits at that valley's far-left edge.
|
||||
|
||||
This branching remains complete: the bottom-left cell of the selected valley
|
||||
must be covered, a square covering it cannot begin to the left across the
|
||||
taller neighbour, and it cannot extend beyond the equal-height run without
|
||||
overlap or leaving an unreachable hole. Trying every fitting available size
|
||||
therefore includes the placement used by every possible completion.
|
||||
|
||||
For board width `W` and order `n`, the skyline scan is `O(W)`. A node tries at
|
||||
most `n` candidates and each placement or exact undo changes at most `n`
|
||||
heights, giving `O(W + n^2)` local work. The skyline, multiplicities,
|
||||
placements, and recursion stack use `O(W + n^2)` state, compared with the
|
||||
former `O(W^2)` cell grid.
|
||||
|
||||
One-run exploratory measurements used the issue #4 dirty worktree at base
|
||||
commit `0a7ce1e`, Apple Clang 21.0.0, `-O3 -DNDEBUG`, macOS arm64, one worker,
|
||||
no warm-up, and a 15-second timeout. Every completed result passed the
|
||||
independent benchmark validator:
|
||||
|
||||
| Order | Result | Ascending time | Ascending nodes | Descending time | Descending nodes |
|
||||
| --- | --- | ---: | ---: | ---: | ---: |
|
||||
| 6 | infeasible | 0.040 s | 659,598 | 0.039 s | 659,598 |
|
||||
| 7 | infeasible | 3.103 s | 43,604,507 | 3.071 s | 43,604,507 |
|
||||
| 8 | solution | 0.585 s | 7,735,369 | 0.941 s | 12,186,125 |
|
||||
| 9 direct | solution | 3.831 s | 45,840,266 | timeout | unavailable |
|
||||
|
||||
The infeasible orders exhaust the same tree in either direction. Ascending
|
||||
was selected as the default because it reaches the first order-8 solution with
|
||||
36% fewer nodes and also completed direct order 9 within the timeout;
|
||||
descending direct order 9 did not.
|
||||
|
||||
A direct ascending order-10 probe exceeded 20 seconds. Public order 10 is
|
||||
also a direct search, and public order 11 first searches order 10 before using
|
||||
odd-predecessor construction. Consequently neither 10 nor 11 is in the
|
||||
routine correctness suite: doing so would test the same unresolved order-10
|
||||
search bottleneck, while the existing route-boundary test still verifies that
|
||||
11 selects construction. Revisit both sizes when order 10 completes within a
|
||||
practical test budget.
|
||||
|
||||
## Candidate policy selection
|
||||
|
||||
Candidate ordering is a deterministic search policy and does not alter the
|
||||
smallest-valley selection or set of placements tried. `ascending` tries
|
||||
smaller available squares first and `descending` tries larger ones first.
|
||||
`best-fit` first tries a square exactly as wide as the selected valley, because
|
||||
that placement closes the valley without leaving a shelf remainder, then tries
|
||||
the other sizes in ascending order. If no exact-width square fits, best-fit
|
||||
and ascending are identical at that node.
|
||||
|
||||
The policy comparison used the issue #12 working tree based on commit
|
||||
`d751d1b`, Apple Clang 21.0.0, `-O3 -DNDEBUG`, macOS arm64, and one worker.
|
||||
Order 8 used two warm-ups and seven sequential measured repetitions; direct
|
||||
order 9 used one warm-up and three measured repetitions. All completed
|
||||
results passed independent validation and node counts were stable:
|
||||
|
||||
| Order | Policy | Counted median (range) | Counter-free median | Nodes |
|
||||
| --- | --- | --- | --- | ---: |
|
||||
| 8 | ascending | 0.808 s (0.790–0.852 s) | 0.794 s | 7,735,369 |
|
||||
| 8 | descending | 1.310 s (1.279–1.449 s) | 1.268 s | 12,186,125 |
|
||||
| 8 | best-fit | 0.817 s (0.813–0.857 s) | 0.823 s | 7,679,349 |
|
||||
| 9 direct | ascending | 5.522 s (5.499–5.830 s) | not measured | 45,840,266 |
|
||||
| 9 direct | best-fit | 5.651 s (5.533–5.820 s) | not measured | 45,746,016 |
|
||||
|
||||
The earlier direct-order-9 descending probe exceeded its 15-second limit.
|
||||
Ascending is retained as the stable single-threaded default because it had the
|
||||
lowest measured median time to the first solution at both measured solvable
|
||||
sizes. Best-fit's slightly smaller trees did not compensate for its policy
|
||||
checks, while descending was substantially worse. Exhaustive infeasible
|
||||
order-5 tests visit the same number of nodes under all three policies, which
|
||||
checks that ordering does not affect completeness.
|
||||
|
||||
One policy therefore applies to the currently measured sizes 8 and 9. This
|
||||
does not establish that ascending is optimal for order 10: a bounded best-fit
|
||||
order-9 comparison changed the search tree by only 0.2%, so there was no
|
||||
evidence that repeating the known long order-10/11 search would be useful.
|
||||
Keep 10 and 11 as opt-in benchmark cases. Public order 11 is particularly
|
||||
important to interpret correctly: it constructs from an order-10 search, so it
|
||||
does not independently measure an odd-order candidate policy.
|
||||
|
||||
A worker portfolio was considered but not added. Running identical policies
|
||||
duplicates the same deterministic traversal. Pairing ascending with best-fit
|
||||
adds little diversity on the measured trees, and pairing ascending with
|
||||
descending dedicates a worker to the consistently slower policy. Splitting a
|
||||
shared frontier could avoid duplicated prefixes, but that is the parallel
|
||||
frontier work tracked separately in issue #11. Seeded randomized ordering was
|
||||
also rejected for now: the deterministic alternatives already select a clear
|
||||
default, and there is no measurement showing that seed distributions would
|
||||
improve time to first solution. The benchmark schema retains its nullable
|
||||
seed field so a future evidence-backed randomized policy can report
|
||||
reproducible runs without changing the format.
|
||||
|
||||
## Post-correctness baseline
|
||||
|
||||
This framework starts from commit `ce39d0a` after the rendering assertion fix
|
||||
@@ -80,9 +381,34 @@ Counts were stable across repetitions. Interleaved counter-free medians were
|
||||
overheads of 0.53% and 0.64% respectively. Construction time was zero; median
|
||||
independent validation and rendering times were each below 0.02 milliseconds.
|
||||
|
||||
Order 9 was not rerun for this initial baseline because its documented runtime
|
||||
is several minutes. The default suite includes it with a per-run timeout.
|
||||
Order 9 was not rerun for this initial baseline because the former direct
|
||||
search took several minutes. The default suite includes it with a per-run
|
||||
timeout.
|
||||
|
||||
## Odd construction comparison
|
||||
|
||||
The order-9 construction was measured from the issue 6 working tree based on
|
||||
commit `ddf07e7`, using Apple Clang 21.0.0 with `-O3 -DNDEBUG`, macOS arm64,
|
||||
one worker, one warm-up, and three measured repetitions. Counter-free and
|
||||
counted runs were interleaved:
|
||||
|
||||
| Order | Mode | Search median (range) | Construction median | Nodes |
|
||||
| --- | --- | --- | --- | ---: |
|
||||
| 8 | counter-free | 1.773 s (1.770–1.775 s) | 0 | 0 |
|
||||
| 8 | counted | 1.849 s (1.848–1.850 s) | 0 | 60,485,176 |
|
||||
| 9 | counter-free | 1.778 s (1.773–1.779 s) | 0.458 us | 0 |
|
||||
| 9 | counted | 1.852 s (1.845–1.912 s) | 0.416 us | 60,485,176 |
|
||||
|
||||
All runs completed with valid results and stable counters. The matching
|
||||
order-8 and order-9 search counts demonstrate that the new path searches only
|
||||
the predecessor. Compared with the recorded 158.69-second direct order-9
|
||||
elapsed time in `results.md`, the 1.778-second counter-free median plus
|
||||
construction is approximately 89 times faster. The benchmark working tree
|
||||
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).
|
||||
|
||||
@@ -19,14 +19,23 @@ if(BUILD_TESTING)
|
||||
tests/tests.cc)
|
||||
add_test(NAME validator COMMAND partridge_tests validator)
|
||||
add_test(NAME construction COMMAND partridge_tests construction)
|
||||
add_test(NAME solver-odd-route COMMAND partridge_tests solver-odd-route)
|
||||
add_test(NAME rendering COMMAND partridge_tests rendering)
|
||||
add_test(NAME solver-small COMMAND partridge_tests solver-small)
|
||||
add_test(NAME solver-completion COMMAND partridge_tests solver-completion)
|
||||
add_test(NAME search-counters COMMAND partridge_tests search-counters)
|
||||
add_test(NAME skyline-search COMMAND partridge_tests skyline-search)
|
||||
add_test(NAME d4-symmetry COMMAND partridge_tests d4-symmetry)
|
||||
add_test(NAME valley-capacity COMMAND partridge_tests valley-capacity)
|
||||
add_test(NAME large-square COMMAND partridge_tests large-square)
|
||||
add_test(NAME component-area COMMAND partridge_tests component-area)
|
||||
find_package(Python3 COMPONENTS Interpreter)
|
||||
if(Python3_Interpreter_FOUND)
|
||||
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()
|
||||
|
||||
@@ -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:
|
||||
|
||||
- <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.
|
||||
@@ -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.
|
||||
|
||||
+22
-5
@@ -12,8 +12,27 @@ ctest --test-dir build --output-on-failure
|
||||
The tests independently check board dimensions, square multiplicities, bounds,
|
||||
overlap, and complete coverage. They cover small unsatisfiable solver inputs, a
|
||||
known order-8 solution, invalid placement diagnostics, and construction of an
|
||||
order-9 solution from the order-8 fixture. The rendering test also formats the
|
||||
known order-8 solution and checks the resulting grid dimensions and coverage.
|
||||
order-9 solution from the order-8 fixture. The routed best-fit order-9 solver
|
||||
test checks that its search counters exactly match order 8. The skyline tests
|
||||
check smallest-width valley selection and deterministic tie-breaking, validate
|
||||
an order-8 result with descending candidates, and independently validate a
|
||||
direct order-9 search with ascending candidates. An
|
||||
exhaustive infeasible order also checks that all three policies visit the same
|
||||
search space. Focused D4 tests cover all eight rotations and reflections,
|
||||
even and odd midlines, diagonals, corners, and the odd-board centre. They
|
||||
independently validate order-8 solutions with symmetry enabled and disabled
|
||||
and check that only the enabled search records symmetry pruning. The direct
|
||||
order-9 test is deliberately separate from the
|
||||
public order-9 route, which uses even-predecessor construction. Orders 10 and
|
||||
11 are not routine tests because both public routes require the same long
|
||||
direct order-10 search; the route-boundary test still checks that order 11
|
||||
selects odd construction. 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
|
||||
|
||||
@@ -38,6 +57,4 @@ ctest --test-dir build-ubsan --output-on-failure
|
||||
```
|
||||
|
||||
The sanitizer flags shown are supported by Clang and GCC. Other compilers may
|
||||
require different flags. A feasible solver run currently exposes the
|
||||
pre-existing defect tracked by issue #14; the test additions deliberately do
|
||||
not include its separate fix.
|
||||
require different flags.
|
||||
|
||||
+178
-11
@@ -20,6 +20,47 @@ namespace {
|
||||
return std::chrono::duration<double>(end - begin).count();
|
||||
}
|
||||
|
||||
struct TimedSolution {
|
||||
Results result;
|
||||
double search_seconds;
|
||||
double construction_seconds;
|
||||
};
|
||||
|
||||
auto solve(std::uint64_t order, bool instrument,
|
||||
SearchPolicy policy, bool direct_search,
|
||||
SymmetryBreaking symmetry,
|
||||
Pruning pruning,
|
||||
ComponentPruning component_pruning,
|
||||
ComponentSchedule component_schedule,
|
||||
SearchCounters &counters)
|
||||
-> TimedSolution {
|
||||
auto const predecessor_order =
|
||||
!direct_search && uses_odd_construction(order) ? order - 1 : order;
|
||||
auto const search_begin = Clock::now();
|
||||
auto predecessor =
|
||||
instrument
|
||||
? search_solution_instrumented(predecessor_order, counters,
|
||||
policy, symmetry, pruning,
|
||||
component_pruning,
|
||||
component_schedule)
|
||||
: search_solution(predecessor_order, policy, symmetry, pruning,
|
||||
component_pruning, component_schedule);
|
||||
auto const search_end = Clock::now();
|
||||
|
||||
auto const construction_begin = Clock::now();
|
||||
auto result = !direct_search && uses_odd_construction(order)
|
||||
? construct_odd_solution(order, std::move(predecessor))
|
||||
: std::move(predecessor);
|
||||
auto const construction_end = Clock::now();
|
||||
return {
|
||||
std::move(result),
|
||||
seconds(search_begin, search_end),
|
||||
!direct_search && uses_odd_construction(order)
|
||||
? seconds(construction_begin, construction_end)
|
||||
: 0.0,
|
||||
};
|
||||
}
|
||||
|
||||
auto valid(std::uint64_t order, Results const &result) -> bool {
|
||||
auto const expected = triangle_num(order);
|
||||
if (result.length() != expected) {
|
||||
@@ -56,11 +97,41 @@ namespace {
|
||||
}
|
||||
|
||||
auto boolean(bool value) -> char const * { return value ? "true" : "false"; }
|
||||
|
||||
auto pruning_name(Pruning const pruning) -> char const * {
|
||||
switch (pruning) {
|
||||
case Pruning::all: return "all";
|
||||
case Pruning::valley_capacity: return "valley-capacity";
|
||||
case Pruning::large_square: return "large-square";
|
||||
case Pruning::disabled: return "none";
|
||||
}
|
||||
assert(false);
|
||||
return "none";
|
||||
}
|
||||
|
||||
auto component_pruning_name(ComponentPruning const pruning) -> char const * {
|
||||
switch (pruning) {
|
||||
case ComponentPruning::disabled: return "none";
|
||||
case ComponentPruning::gcd: return "gcd";
|
||||
case ComponentPruning::subset_sum: return "subset-sum";
|
||||
}
|
||||
assert(false);
|
||||
return "none";
|
||||
}
|
||||
|
||||
auto component_schedule_name(ComponentSchedule const schedule)
|
||||
-> char const * {
|
||||
return schedule == ComponentSchedule::boundary ? "boundary"
|
||||
: "periodic-8";
|
||||
}
|
||||
}
|
||||
|
||||
int main(int argc, char **argv) {
|
||||
if (argc != 3) {
|
||||
std::cerr << "usage: partridge_benchmark ORDER counters|plain\n";
|
||||
if (argc < 3 || argc > 9) {
|
||||
std::cerr << "usage: partridge_benchmark ORDER counters|plain "
|
||||
"[ascending|descending|best-fit] [public|direct] "
|
||||
"[d4|none] [all|valley-capacity|large-square|none] "
|
||||
"[subset-sum|gcd|none] [boundary|periodic-8]\n";
|
||||
return 2;
|
||||
}
|
||||
auto const order = static_cast<std::uint64_t>(std::strtoull(argv[1], nullptr, 10));
|
||||
@@ -69,21 +140,85 @@ int main(int argc, char **argv) {
|
||||
std::cerr << "counter mode must be counters or plain\n";
|
||||
return 2;
|
||||
}
|
||||
auto const policy =
|
||||
argc < 4 || std::string_view(argv[3]) == "ascending"
|
||||
? SearchPolicy::ascending
|
||||
: std::string_view(argv[3]) == "descending"
|
||||
? SearchPolicy::descending
|
||||
: SearchPolicy::best_fit;
|
||||
if (argc >= 4 && std::string_view(argv[3]) != "ascending" &&
|
||||
std::string_view(argv[3]) != "descending" &&
|
||||
std::string_view(argv[3]) != "best-fit") {
|
||||
std::cerr << "search policy must be ascending, descending, or best-fit\n";
|
||||
return 2;
|
||||
}
|
||||
auto const direct_search =
|
||||
argc >= 5 && std::string_view(argv[4]) == "direct";
|
||||
if (argc >= 5 && std::string_view(argv[4]) != "public" &&
|
||||
std::string_view(argv[4]) != "direct") {
|
||||
std::cerr << "search route must be public or direct\n";
|
||||
return 2;
|
||||
}
|
||||
auto const symmetry =
|
||||
argc < 6 || std::string_view(argv[5]) == "d4"
|
||||
? SymmetryBreaking::d4_unit_square
|
||||
: SymmetryBreaking::disabled;
|
||||
if (argc >= 6 && std::string_view(argv[5]) != "d4" &&
|
||||
std::string_view(argv[5]) != "none") {
|
||||
std::cerr << "symmetry mode must be d4 or none\n";
|
||||
return 2;
|
||||
}
|
||||
auto const pruning =
|
||||
argc < 7 || std::string_view(argv[6]) == "all"
|
||||
? Pruning::all
|
||||
: std::string_view(argv[6]) == "valley-capacity"
|
||||
? Pruning::valley_capacity
|
||||
: std::string_view(argv[6]) == "large-square"
|
||||
? Pruning::large_square
|
||||
: Pruning::disabled;
|
||||
if (argc >= 7 && std::string_view(argv[6]) != "all" &&
|
||||
std::string_view(argv[6]) != "valley-capacity" &&
|
||||
std::string_view(argv[6]) != "large-square" &&
|
||||
std::string_view(argv[6]) != "none") {
|
||||
std::cerr << "pruning mode must be all, valley-capacity, "
|
||||
"large-square, or none\n";
|
||||
return 2;
|
||||
}
|
||||
auto const component_pruning =
|
||||
argc < 8 || std::string_view(argv[7]) == "none"
|
||||
? ComponentPruning::disabled
|
||||
: std::string_view(argv[7]) == "gcd"
|
||||
? ComponentPruning::gcd
|
||||
: ComponentPruning::subset_sum;
|
||||
if (argc >= 8 && std::string_view(argv[7]) != "subset-sum" &&
|
||||
std::string_view(argv[7]) != "gcd" &&
|
||||
std::string_view(argv[7]) != "none") {
|
||||
std::cerr << "component pruning mode must be subset-sum, gcd, or none\n";
|
||||
return 2;
|
||||
}
|
||||
auto const component_schedule =
|
||||
argc < 9 || std::string_view(argv[8]) == "boundary"
|
||||
? ComponentSchedule::boundary
|
||||
: ComponentSchedule::periodic_eight;
|
||||
if (argc == 9 && std::string_view(argv[8]) != "boundary" &&
|
||||
std::string_view(argv[8]) != "periodic-8") {
|
||||
std::cerr << "component schedule must be boundary or periodic-8\n";
|
||||
return 2;
|
||||
}
|
||||
|
||||
SearchCounters counters;
|
||||
auto const solve_begin = Clock::now();
|
||||
auto result = instrument ? find_solution_instrumented(order, counters)
|
||||
: find_solution(order);
|
||||
auto const solve_end = Clock::now();
|
||||
auto timed =
|
||||
solve(order, instrument, policy, direct_search, symmetry, pruning,
|
||||
component_pruning, component_schedule, counters);
|
||||
|
||||
auto const validation_begin = Clock::now();
|
||||
auto const validation_ok = valid(order, result);
|
||||
auto const validation_ok = valid(order, timed.result);
|
||||
auto const validation_end = Clock::now();
|
||||
|
||||
auto const render_begin = Clock::now();
|
||||
std::ostringstream rendered;
|
||||
auto *const old_buffer = std::cout.rdbuf(rendered.rdbuf());
|
||||
result.output();
|
||||
timed.result.output();
|
||||
std::cout.rdbuf(old_buffer);
|
||||
auto const render_end = Clock::now();
|
||||
|
||||
@@ -92,10 +227,26 @@ int main(int argc, char **argv) {
|
||||
<< "{\"schema_version\":1"
|
||||
<< ",\"order\":" << order
|
||||
<< ",\"instrumented\":" << boolean(instrument)
|
||||
<< ",\"solved\":" << boolean(!result.squares().empty())
|
||||
<< ",\"candidate_order\":\""
|
||||
<< (policy == SearchPolicy::ascending
|
||||
? "ascending"
|
||||
: policy == SearchPolicy::descending ? "descending" : "best-fit")
|
||||
<< "\""
|
||||
<< ",\"search_route\":\""
|
||||
<< (direct_search ? "direct" : "public") << "\""
|
||||
<< ",\"symmetry_breaking\":\""
|
||||
<< (symmetry == SymmetryBreaking::d4_unit_square ? "d4" : "none")
|
||||
<< "\""
|
||||
<< ",\"pruning\":\""
|
||||
<< pruning_name(pruning) << "\""
|
||||
<< ",\"component_pruning\":\""
|
||||
<< component_pruning_name(component_pruning) << "\""
|
||||
<< ",\"component_schedule\":\""
|
||||
<< component_schedule_name(component_schedule) << "\""
|
||||
<< ",\"solved\":" << boolean(!timed.result.squares().empty())
|
||||
<< ",\"valid\":" << boolean(validation_ok)
|
||||
<< ",\"timing_seconds\":{\"solve\":" << seconds(solve_begin, solve_end)
|
||||
<< ",\"construction\":0"
|
||||
<< ",\"timing_seconds\":{\"solve\":" << timed.search_seconds
|
||||
<< ",\"construction\":" << timed.construction_seconds
|
||||
<< ",\"validation\":" << seconds(validation_begin, validation_end)
|
||||
<< ",\"render\":" << seconds(render_begin, render_end) << "}"
|
||||
<< ",\"counters\":{\"search_nodes\":" << counters.search_nodes
|
||||
@@ -104,6 +255,22 @@ int main(int argc, char **argv) {
|
||||
<< ",\"backtracks\":" << counters.backtracks
|
||||
<< ",\"prune_checks\":" << counters.prune_checks
|
||||
<< ",\"prune_hits\":" << counters.prune_hits
|
||||
<< ",\"valley_capacity_checks\":"
|
||||
<< counters.valley_capacity_checks
|
||||
<< ",\"valley_capacity_prunes\":"
|
||||
<< counters.valley_capacity_prunes
|
||||
<< ",\"large_square_checks\":"
|
||||
<< counters.large_square_checks
|
||||
<< ",\"large_square_prunes\":"
|
||||
<< counters.large_square_prunes
|
||||
<< ",\"component_area_checks\":"
|
||||
<< counters.component_area_checks
|
||||
<< ",\"component_area_prunes\":"
|
||||
<< counters.component_area_prunes
|
||||
<< ",\"component_gcd_prunes\":"
|
||||
<< counters.component_gcd_prunes
|
||||
<< ",\"component_subset_prunes\":"
|
||||
<< counters.component_subset_prunes
|
||||
<< ",\"generated_tasks\":" << counters.generated_tasks
|
||||
<< ",\"completed_tasks\":" << counters.completed_tasks << "}}\n";
|
||||
return validation_ok ? 0 : 1;
|
||||
|
||||
+91
-5
@@ -74,16 +74,37 @@ def environment(binary):
|
||||
"logical_cpus": os.cpu_count(),
|
||||
},
|
||||
"workers": 1,
|
||||
"search_policy": "single-threaded, deterministic, largest-fitting-first",
|
||||
"search_policy": "single-threaded, deterministic, smallest-width valley",
|
||||
"seed": None,
|
||||
}
|
||||
|
||||
|
||||
def run_once(binary, order, mode, timeout):
|
||||
def run_once(
|
||||
binary,
|
||||
order,
|
||||
mode,
|
||||
search_policy,
|
||||
search_route,
|
||||
symmetry,
|
||||
pruning,
|
||||
component_pruning,
|
||||
component_schedule,
|
||||
timeout,
|
||||
):
|
||||
started = time.monotonic()
|
||||
try:
|
||||
process = subprocess.run(
|
||||
[str(binary), str(order), mode],
|
||||
[
|
||||
str(binary),
|
||||
str(order),
|
||||
mode,
|
||||
search_policy,
|
||||
search_route,
|
||||
symmetry,
|
||||
pruning,
|
||||
component_pruning,
|
||||
component_schedule,
|
||||
],
|
||||
check=False,
|
||||
capture_output=True,
|
||||
text=True,
|
||||
@@ -216,6 +237,41 @@ def main():
|
||||
parser.add_argument("--warmup", type=int, default=1)
|
||||
parser.add_argument("--repetitions", type=int, default=5)
|
||||
parser.add_argument("--timeout", type=float, default=600.0)
|
||||
parser.add_argument(
|
||||
"--candidate-order",
|
||||
dest="search_policy",
|
||||
choices=("ascending", "descending", "best-fit"),
|
||||
default="ascending",
|
||||
)
|
||||
parser.add_argument("--direct-search", action="store_true")
|
||||
parser.add_argument(
|
||||
"--no-symmetry",
|
||||
action="store_true",
|
||||
help="disable unique-unit-square D4 symmetry breaking",
|
||||
)
|
||||
parser.add_argument(
|
||||
"--pruning",
|
||||
choices=("all", "valley-capacity", "large-square", "none"),
|
||||
default="all",
|
||||
help="select independently measurable pruning rules",
|
||||
)
|
||||
parser.add_argument(
|
||||
"--no-pruning",
|
||||
action="store_true",
|
||||
help="disable all pruning (compatibility alias for --pruning none)",
|
||||
)
|
||||
parser.add_argument(
|
||||
"--component-pruning",
|
||||
choices=("subset-sum", "gcd", "none"),
|
||||
default="none",
|
||||
help="select component-area pruning strength",
|
||||
)
|
||||
parser.add_argument(
|
||||
"--component-schedule",
|
||||
choices=("boundary", "periodic-8"),
|
||||
default="boundary",
|
||||
help="trigger component checks on boundaries or every eighth depth",
|
||||
)
|
||||
parser.add_argument(
|
||||
"--measure-overhead",
|
||||
action="store_true",
|
||||
@@ -241,11 +297,33 @@ def main():
|
||||
mode_results = {mode: {"runs": []} for mode in modes}
|
||||
for trial in range(args.warmup):
|
||||
for mode in trial_modes(modes, trial):
|
||||
run_once(args.binary, order, mode, args.timeout)
|
||||
run_once(
|
||||
args.binary,
|
||||
order,
|
||||
mode,
|
||||
args.search_policy,
|
||||
"direct" if args.direct_search else "public",
|
||||
"none" if args.no_symmetry else "d4",
|
||||
"none" if args.no_pruning else args.pruning,
|
||||
"none" if args.no_pruning else args.component_pruning,
|
||||
args.component_schedule,
|
||||
args.timeout,
|
||||
)
|
||||
for trial in range(args.repetitions):
|
||||
for mode in trial_modes(modes, trial):
|
||||
mode_results[mode]["runs"].append(
|
||||
run_once(args.binary, order, mode, args.timeout)
|
||||
run_once(
|
||||
args.binary,
|
||||
order,
|
||||
mode,
|
||||
args.search_policy,
|
||||
"direct" if args.direct_search else "public",
|
||||
"none" if args.no_symmetry else "d4",
|
||||
"none" if args.no_pruning else args.pruning,
|
||||
"none" if args.no_pruning else args.component_pruning,
|
||||
args.component_schedule,
|
||||
args.timeout,
|
||||
)
|
||||
)
|
||||
for result in mode_results.values():
|
||||
result["summary"] = summarize(result["runs"])
|
||||
@@ -270,6 +348,14 @@ def main():
|
||||
"warmup_runs": args.warmup,
|
||||
"measured_repetitions": args.repetitions,
|
||||
"per_run_timeout_seconds": args.timeout,
|
||||
"candidate_order": args.search_policy,
|
||||
"search_route": "direct" if args.direct_search else "public",
|
||||
"symmetry_breaking": "none" if args.no_symmetry else "d4",
|
||||
"pruning": "none" if args.no_pruning else args.pruning,
|
||||
"component_pruning": (
|
||||
"none" if args.no_pruning else args.component_pruning
|
||||
),
|
||||
"component_schedule": args.component_schedule,
|
||||
"stdout": "captured; rendered grid suppressed by probe",
|
||||
},
|
||||
"cases": cases,
|
||||
|
||||
@@ -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())
|
||||
@@ -11,6 +11,7 @@
|
||||
#include <string_view>
|
||||
#include <vector>
|
||||
#include <iostream>
|
||||
#include <numeric>
|
||||
|
||||
namespace {
|
||||
using size_t = std::uint64_t;
|
||||
@@ -131,97 +132,6 @@ namespace {
|
||||
std::vector<Square> squares_;
|
||||
};
|
||||
|
||||
/** An N * N grid of characters. */
|
||||
struct Grid {
|
||||
// Type to use for the grid contents
|
||||
using T = std::int_fast64_t;
|
||||
|
||||
/** Construct a grid of given side-length. */
|
||||
explicit Grid(size_t length) : grid_(length * length, empty), length_(length) {
|
||||
}
|
||||
|
||||
Grid(Grid const &other) = delete;
|
||||
|
||||
Grid(Grid &&other) noexcept = default;
|
||||
|
||||
Grid &operator=(Grid const &other) = delete;
|
||||
|
||||
Grid &operator=(Grid &&other) noexcept = default;
|
||||
|
||||
~Grid() noexcept = default;
|
||||
|
||||
/** Get grid length */
|
||||
[[nodiscard]] auto end() const noexcept -> size_t { return static_cast<size_t>(grid_.size()); }
|
||||
|
||||
/** Add a square to the grid. */
|
||||
auto add(Square const &sq) noexcept -> void {
|
||||
/* One would expect the fastest way to do this would be to have x be the
|
||||
* fastest increasing index so we store [pos, pos + 1,..., pos+length, ...]
|
||||
* But experimentation tells us this isn't so, and storing
|
||||
* [pos, pos + length, ..., pos + 1, ...] is faster!
|
||||
*/
|
||||
for (auto x = 0; x < sq.length(); ++x) {
|
||||
for (auto y = sq.pos(); y < sq.pos() + sq.length() * length_; y += length_) {
|
||||
grid_[x + y] = filled;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/** Clear a square from the grid. */
|
||||
auto clear(Square const &sq) noexcept -> void {
|
||||
for (auto x = 0; x < sq.length(); ++x) {
|
||||
for (auto y = sq.pos(); y < sq.pos() + sq.length() * length_; y += length_) {
|
||||
grid_[x + y] = empty;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/** \brief Get length of the largest square that fits at \a pos in the grid.
|
||||
*/
|
||||
[[nodiscard]] auto largest_square(Pos pos, size_t n) const noexcept -> size_t {
|
||||
assert(pos < end());
|
||||
|
||||
/* Because of how we walk through the grid (starting at 0,0 then increasing
|
||||
* x followed by y) we can assume that if the position (b, y) is clear
|
||||
* (i.e. a '.') then (b, y + i) is clear for all i > 0.
|
||||
*
|
||||
* This means we only need to look for the first non-clear position along the
|
||||
* current row.
|
||||
*/
|
||||
auto const pos_x = pos % length_;
|
||||
auto const pos_y0 = pos - pos_x;
|
||||
auto b = pos;
|
||||
// Make sure we don't go looking in the next row.
|
||||
auto const e = std::min(pos + n, pos_y0 + length_);
|
||||
while (b < e) {
|
||||
if (grid_[b] != empty) { break; }
|
||||
++b;
|
||||
}
|
||||
// Check that this length fits vertically as well.
|
||||
auto const len = b - pos;
|
||||
auto const pos_y = pos / length_;
|
||||
auto const ye = std::min(pos_y + len, length_);
|
||||
return ye - pos_y;
|
||||
}
|
||||
|
||||
/** Get the next position to check starting at pos.
|
||||
*
|
||||
* Returns grid_.length() if no more positions available.
|
||||
*/
|
||||
[[nodiscard]] auto next_pos(Pos pos) const noexcept -> Pos {
|
||||
auto const b = grid_.begin() + static_cast<std::ptrdiff_t>(pos);
|
||||
auto const p = std::find(b, grid_.end(), empty);
|
||||
return p - grid_.begin();
|
||||
}
|
||||
|
||||
private:
|
||||
std::vector<T> grid_; ///< The grid
|
||||
size_t length_; ///< Side length
|
||||
|
||||
static constexpr char empty = 0; ///< Character used for an empty cell.
|
||||
static constexpr char filled = 1; ///< Character used for a filled cell,
|
||||
};
|
||||
|
||||
/** Get the n-th triangular number. */
|
||||
auto triangle_num(size_t n) noexcept -> size_t { return (n * (n + 1)) / 2; }
|
||||
|
||||
@@ -241,116 +151,605 @@ namespace {
|
||||
size_t backtracks = 0;
|
||||
size_t prune_checks = 0;
|
||||
size_t prune_hits = 0;
|
||||
size_t valley_capacity_checks = 0;
|
||||
size_t valley_capacity_prunes = 0;
|
||||
size_t large_square_checks = 0;
|
||||
size_t large_square_prunes = 0;
|
||||
size_t component_area_checks = 0;
|
||||
size_t component_area_prunes = 0;
|
||||
size_t component_gcd_prunes = 0;
|
||||
size_t component_subset_prunes = 0;
|
||||
size_t generated_tasks = 0;
|
||||
size_t completed_tasks = 0;
|
||||
};
|
||||
|
||||
/** Find a solution to the \a n th Partridge problem.
|
||||
/** Deterministic order in which a skyline node tries fitting squares. */
|
||||
enum class SearchPolicy {
|
||||
ascending,
|
||||
descending,
|
||||
/** Close the selected valley when possible, then try smaller sizes first. */
|
||||
best_fit,
|
||||
};
|
||||
|
||||
/** Whether to remove equivalent board orientations from the search. */
|
||||
enum class SymmetryBreaking {
|
||||
disabled,
|
||||
d4_unit_square,
|
||||
};
|
||||
|
||||
/** Cheap necessary conditions applied before branching at a search node. */
|
||||
enum class Pruning {
|
||||
disabled = 0,
|
||||
valley_capacity = 1,
|
||||
large_square = 2,
|
||||
all = 3,
|
||||
};
|
||||
|
||||
/** Component-area rule used after a full-height boundary is created. */
|
||||
enum class ComponentPruning {
|
||||
disabled,
|
||||
gcd,
|
||||
subset_sum,
|
||||
};
|
||||
|
||||
enum class ComponentSchedule {
|
||||
boundary,
|
||||
periodic_eight,
|
||||
};
|
||||
|
||||
enum class ComponentFeasibility {
|
||||
feasible,
|
||||
gcd_failure,
|
||||
subset_sum_failure,
|
||||
};
|
||||
|
||||
/** Return whether a cell is the canonical representative of its D4 orbit.
|
||||
*
|
||||
* Returns the grid of the solution.
|
||||
* Reflect a cell into the left half of the board, rotate so its distance
|
||||
* from the left edge is no greater than its distance from the top edge, and
|
||||
* finally reflect it into the top half. The resulting fundamental region is
|
||||
* the closed triangle x <= y <= floor((length - 1) / 2). Closed boundaries
|
||||
* retain representatives whose orbit is smaller than eight.
|
||||
*/
|
||||
template<bool Instrument>
|
||||
auto find_solution_impl(size_t const n, SearchCounters *const counters) noexcept
|
||||
-> Results {
|
||||
/* Implementation is iterative, as opposed to recursive.
|
||||
*
|
||||
* The recursive implementation is easier to understand - but is
|
||||
* slightly slower because of the repeated function calls (and
|
||||
* entry/exit).
|
||||
*
|
||||
* The basic algorithm is to start at the origin of the grid we
|
||||
* want to place squares on and iterate over the permutations of
|
||||
* available squares until we find one that fits.
|
||||
*/
|
||||
[[nodiscard]] auto canonical_unit_position(size_t const x,
|
||||
size_t const y,
|
||||
size_t const length) noexcept
|
||||
-> bool {
|
||||
assert(x < length);
|
||||
assert(y < length);
|
||||
return x <= y && y <= (length - 1) / 2;
|
||||
}
|
||||
|
||||
// grid is our in-progress grid of square positions.
|
||||
auto const length = triangle_num(n);
|
||||
Grid grid(length);
|
||||
/** A maximal level skyline segment which is lower than its neighbours. */
|
||||
struct Valley {
|
||||
size_t x;
|
||||
size_t height;
|
||||
size_t width;
|
||||
};
|
||||
|
||||
/* avail_sqs is a vector indexed by square length indicating how many
|
||||
* squares are available. Initially set up so that avail_sqs[i] = i.
|
||||
*/
|
||||
Avail avail_sqs;
|
||||
for (auto i = 0; i <= n; ++i) { avail_sqs.push_back(i); }
|
||||
/** Return the narrowest local valley, breaking ties by height then x. */
|
||||
[[nodiscard]] auto smallest_valley(std::vector<size_t> const &skyline) noexcept
|
||||
-> Valley {
|
||||
Valley best{0, 0, skyline.size()};
|
||||
bool found = false;
|
||||
for (size_t begin = 0; begin < skyline.size();) {
|
||||
auto end = begin + 1;
|
||||
while (end < skyline.size() && skyline[end] == skyline[begin]) {
|
||||
++end;
|
||||
}
|
||||
auto const left_height =
|
||||
begin == 0 ? skyline.size() : skyline[begin - 1];
|
||||
auto const right_height =
|
||||
end == skyline.size() ? skyline.size() : skyline[end];
|
||||
auto const lower_than_left = skyline[begin] < left_height;
|
||||
auto const lower_than_right = skyline[begin] < right_height;
|
||||
auto const width = end - begin;
|
||||
if (lower_than_left && lower_than_right &&
|
||||
(!found || width < best.width ||
|
||||
(width == best.width && skyline[begin] < best.height) ||
|
||||
(width == best.width && skyline[begin] == best.height &&
|
||||
begin < best.x))) {
|
||||
best = {begin, skyline[begin], width};
|
||||
found = true;
|
||||
}
|
||||
begin = end;
|
||||
}
|
||||
assert(found);
|
||||
return best;
|
||||
}
|
||||
|
||||
/* sqs is a vector used as a stack of the squares currently placed.
|
||||
* We reserve the length we need so as not to have too many allocations.
|
||||
*/
|
||||
std::vector<Square> sqs;
|
||||
sqs.reserve(length);
|
||||
/** Return whether the remaining narrow pieces can fill a valley to its rim.
|
||||
*
|
||||
* Until the valley reaches the lower of its two neighbouring heights, no
|
||||
* square wider than the valley can enter it. The area of all remaining
|
||||
* squares no wider than the valley is therefore an upper bound on the area
|
||||
* available to fill this isolated strip. This includes the familiar
|
||||
* width-one and width-two gap checks without special cases.
|
||||
*/
|
||||
[[nodiscard]] auto valley_has_sufficient_capacity(
|
||||
Valley const valley, std::vector<size_t> const &skyline,
|
||||
Avail const &available) noexcept -> bool {
|
||||
auto const end = valley.x + valley.width;
|
||||
auto const left_height =
|
||||
valley.x == 0 ? skyline.size() : skyline[valley.x - 1];
|
||||
auto const right_height =
|
||||
end == skyline.size() ? skyline.size() : skyline[end];
|
||||
auto const rim_height = std::min(left_height, right_height);
|
||||
auto const required_area = valley.width * (rim_height - valley.height);
|
||||
|
||||
// Start at the origin with a square of longest side length.
|
||||
Pos pos = 0;
|
||||
size_t idx = n;
|
||||
size_t available_area = 0;
|
||||
auto const largest = std::min(
|
||||
valley.width, static_cast<size_t>(available.size() - 1));
|
||||
for (size_t side = 1; side <= largest; ++side) {
|
||||
available_area += available[side] * side * side;
|
||||
}
|
||||
return available_area >= required_area;
|
||||
}
|
||||
|
||||
/** Return whether the skyline contains an empty box for a square.
|
||||
*
|
||||
* A side-k square fits exactly when k consecutive columns have heights no
|
||||
* greater than board height minus k. Tracking the current qualifying run
|
||||
* checks this in one pass without allocations.
|
||||
*/
|
||||
[[nodiscard]] auto skyline_has_empty_square(
|
||||
std::vector<size_t> const &skyline, size_t const side) noexcept -> bool {
|
||||
assert(side > 0);
|
||||
assert(side <= skyline.size());
|
||||
auto const maximum_height = skyline.size() - side;
|
||||
size_t run = 0;
|
||||
for (auto const height: skyline) {
|
||||
run = height <= maximum_height ? run + 1 : 0;
|
||||
if (run == side) {
|
||||
return true;
|
||||
}
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
/** Return whether the largest remaining square has any feasible position.
|
||||
*
|
||||
* Feasible empty boxes are monotonic in the side length: a box which fits
|
||||
* the largest remaining square also fits every smaller one. It is therefore
|
||||
* sufficient to test only the largest size with non-zero multiplicity.
|
||||
*/
|
||||
[[nodiscard]] auto remaining_large_square_fits(
|
||||
std::vector<size_t> const &skyline, Avail const &available) noexcept
|
||||
-> bool {
|
||||
for (auto side = available.size() - 1; side != 0; --side) {
|
||||
if (available[side] != 0) {
|
||||
return skyline_has_empty_square(skyline, side);
|
||||
}
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
/** Return areas of empty regions separated by full-height columns.
|
||||
*
|
||||
* Every non-full skyline column is empty from its height to the top of the
|
||||
* board. Adjacent non-full columns therefore connect at the top row, while
|
||||
* a full-height column is an impassable separator.
|
||||
*/
|
||||
[[nodiscard]] auto empty_component_areas(
|
||||
std::vector<size_t> const &skyline) -> std::vector<size_t> {
|
||||
std::vector<size_t> areas;
|
||||
size_t area = 0;
|
||||
for (auto const height: skyline) {
|
||||
if (height == skyline.size()) {
|
||||
if (area != 0) {
|
||||
areas.push_back(area);
|
||||
area = 0;
|
||||
}
|
||||
} else {
|
||||
area += skyline.size() - height;
|
||||
}
|
||||
}
|
||||
if (area != 0) {
|
||||
areas.push_back(area);
|
||||
}
|
||||
return areas;
|
||||
}
|
||||
|
||||
/** Check necessary component-area conditions for the remaining squares.
|
||||
*
|
||||
* Every square lies wholly within one empty component, so each component
|
||||
* area must be a sum of a bounded subset of the remaining square areas.
|
||||
* Divisibility by their gcd is a cheaper necessary condition tested first.
|
||||
*/
|
||||
[[nodiscard]] auto component_area_feasibility(
|
||||
std::vector<size_t> const &skyline, Avail const &available,
|
||||
ComponentPruning const pruning) -> ComponentFeasibility {
|
||||
assert(pruning != ComponentPruning::disabled);
|
||||
auto const components = empty_component_areas(skyline);
|
||||
if (components.size() < 2) {
|
||||
return ComponentFeasibility::feasible;
|
||||
}
|
||||
|
||||
size_t divisor = 0;
|
||||
for (size_t side = 1; side < available.size(); ++side) {
|
||||
if (available[side] != 0) {
|
||||
divisor = std::gcd(divisor, side * side);
|
||||
}
|
||||
}
|
||||
if (divisor != 0 &&
|
||||
std::ranges::any_of(components, [divisor](size_t const area) {
|
||||
return area % divisor != 0;
|
||||
})) {
|
||||
return ComponentFeasibility::gcd_failure;
|
||||
}
|
||||
if (pruning == ComponentPruning::gcd) {
|
||||
return ComponentFeasibility::feasible;
|
||||
}
|
||||
|
||||
auto const maximum_area =
|
||||
*std::ranges::max_element(components);
|
||||
std::vector<bool> reachable(maximum_area + 1);
|
||||
reachable[0] = true;
|
||||
for (size_t side = 1; side < available.size(); ++side) {
|
||||
auto const square_area = side * side;
|
||||
for (size_t copy = 0; copy < available[side]; ++copy) {
|
||||
for (auto area = maximum_area; area >= square_area; --area) {
|
||||
if (reachable[area - square_area]) {
|
||||
reachable[area] = true;
|
||||
}
|
||||
if (area == square_area) {
|
||||
break;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
if (std::ranges::any_of(components, [&reachable](size_t const area) {
|
||||
return !reachable[area];
|
||||
})) {
|
||||
return ComponentFeasibility::subset_sum_failure;
|
||||
}
|
||||
return ComponentFeasibility::feasible;
|
||||
}
|
||||
|
||||
template<bool Instrument, bool BreakD4Symmetry, bool PruneValleyCapacity,
|
||||
bool PruneLargeSquare, bool PruneComponents>
|
||||
auto search_skyline(size_t const n, size_t const length,
|
||||
SearchPolicy const policy,
|
||||
std::vector<size_t> &skyline, Avail &available,
|
||||
std::vector<Square> &squares,
|
||||
SearchCounters *const counters,
|
||||
ComponentPruning const component_pruning,
|
||||
ComponentSchedule const component_schedule,
|
||||
bool const check_components) -> bool {
|
||||
if constexpr (Instrument) {
|
||||
assert(counters != nullptr);
|
||||
++counters->search_nodes;
|
||||
}
|
||||
|
||||
while (true) {
|
||||
if (squares.size() == length) {
|
||||
return true;
|
||||
}
|
||||
|
||||
if constexpr (PruneComponents) {
|
||||
auto const should_check =
|
||||
component_schedule == ComponentSchedule::boundary
|
||||
? check_components
|
||||
: squares.size() % 8 == 0;
|
||||
if (should_check) {
|
||||
if constexpr (Instrument) {
|
||||
++counters->prune_checks;
|
||||
++counters->component_area_checks;
|
||||
}
|
||||
auto const feasibility = component_area_feasibility(
|
||||
skyline, available, component_pruning);
|
||||
if (feasibility != ComponentFeasibility::feasible) {
|
||||
if constexpr (Instrument) {
|
||||
++counters->prune_hits;
|
||||
++counters->component_area_prunes;
|
||||
if (feasibility == ComponentFeasibility::gcd_failure) {
|
||||
++counters->component_gcd_prunes;
|
||||
} else {
|
||||
++counters->component_subset_prunes;
|
||||
}
|
||||
}
|
||||
return false;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
auto const valley = smallest_valley(skyline);
|
||||
if constexpr (PruneValleyCapacity) {
|
||||
if constexpr (Instrument) {
|
||||
++counters->prune_checks;
|
||||
++counters->valley_capacity_checks;
|
||||
}
|
||||
if (!valley_has_sufficient_capacity(valley, skyline, available)) {
|
||||
if constexpr (Instrument) {
|
||||
++counters->prune_hits;
|
||||
++counters->valley_capacity_prunes;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
}
|
||||
if constexpr (PruneLargeSquare) {
|
||||
if constexpr (Instrument) {
|
||||
++counters->prune_checks;
|
||||
++counters->large_square_checks;
|
||||
}
|
||||
if (!remaining_large_square_fits(skyline, available)) {
|
||||
if constexpr (Instrument) {
|
||||
++counters->prune_hits;
|
||||
++counters->large_square_prunes;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
}
|
||||
auto const largest =
|
||||
std::min({n, valley.width, length - valley.height});
|
||||
auto try_side = [&](size_t const side) {
|
||||
if constexpr (Instrument) {
|
||||
++counters->loop_iterations;
|
||||
}
|
||||
/* If the idx is 0 we've looked at all possible square lengths for this
|
||||
* position, and they've failed. Pop the last square of the stack, remove
|
||||
* it from the grid and try the next smaller size in the same position.
|
||||
*/
|
||||
if (idx == 0) {
|
||||
// No squares on the stack -> failed to find a solution.
|
||||
if (sqs.empty()) { break; }
|
||||
if (available[side] == 0) {
|
||||
return false;
|
||||
}
|
||||
|
||||
auto sq = sqs.back();
|
||||
sqs.pop_back();
|
||||
grid.clear(sq);
|
||||
++avail_sqs[sq.length()];
|
||||
if constexpr (Instrument) {
|
||||
++counters->backtracks;
|
||||
if constexpr (BreakD4Symmetry) {
|
||||
if (side == 1) {
|
||||
if constexpr (Instrument) {
|
||||
++counters->prune_checks;
|
||||
}
|
||||
if (!canonical_unit_position(valley.x, valley.height, length)) {
|
||||
if constexpr (Instrument) {
|
||||
++counters->prune_hits;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
}
|
||||
pos = sq.pos();
|
||||
idx = sq.length() - 1;
|
||||
continue;
|
||||
}
|
||||
|
||||
// If there are no squares available of the current size try the next one.
|
||||
if (avail_sqs[idx] == 0) {
|
||||
--idx;
|
||||
continue;
|
||||
}
|
||||
|
||||
/* Place a square of side length idx at pos, push this onto the stack and
|
||||
* set up to look at the next position.
|
||||
*/
|
||||
auto const sq = Square(pos, idx);
|
||||
if constexpr (Instrument) {
|
||||
++counters->attempted_placements;
|
||||
}
|
||||
--avail_sqs[idx];
|
||||
grid.add(sq);
|
||||
sqs.push_back(sq);
|
||||
--available[side];
|
||||
std::fill_n(skyline.begin() + static_cast<std::ptrdiff_t>(valley.x),
|
||||
side, valley.height + side);
|
||||
squares.emplace_back(valley.x + valley.height * length, side);
|
||||
|
||||
pos = grid.next_pos(pos + idx);
|
||||
|
||||
// Have we reached the end? If so success!
|
||||
if (pos == grid.end()) { break; }
|
||||
|
||||
if constexpr (Instrument) {
|
||||
++counters->search_nodes;
|
||||
if (search_skyline<Instrument, BreakD4Symmetry, PruneValleyCapacity,
|
||||
PruneLargeSquare, PruneComponents>(
|
||||
n, length, policy, skyline, available, squares, counters,
|
||||
component_pruning, component_schedule,
|
||||
valley.height + side == length)) {
|
||||
return true;
|
||||
}
|
||||
idx = grid.largest_square(pos, n);
|
||||
}
|
||||
|
||||
return {length, sqs};
|
||||
squares.pop_back();
|
||||
std::fill_n(skyline.begin() + static_cast<std::ptrdiff_t>(valley.x),
|
||||
side, valley.height);
|
||||
++available[side];
|
||||
if constexpr (Instrument) {
|
||||
++counters->backtracks;
|
||||
}
|
||||
return false;
|
||||
};
|
||||
|
||||
if (policy == SearchPolicy::best_fit && largest == valley.width &&
|
||||
try_side(largest)) {
|
||||
return true;
|
||||
}
|
||||
if (policy != SearchPolicy::descending) {
|
||||
for (size_t side = 1; side <= largest; ++side) {
|
||||
if (policy == SearchPolicy::best_fit && side == valley.width) {
|
||||
continue;
|
||||
}
|
||||
if (try_side(side)) {
|
||||
return true;
|
||||
}
|
||||
}
|
||||
} else {
|
||||
for (auto side = largest; side != 0; --side) {
|
||||
if (try_side(side)) {
|
||||
return true;
|
||||
}
|
||||
}
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
auto find_solution(size_t const n) noexcept -> Results {
|
||||
return find_solution_impl<false>(n, nullptr);
|
||||
/** Search directly for a solution to the \a n th Partridge problem.
|
||||
*
|
||||
* The state is one filled height per board column. At each node the
|
||||
* narrowest local valley is found by a linear scan and candidates are tried
|
||||
* at its far-left edge. A placement or undo touches one entry per square
|
||||
* column. Scanning the profile costs O(board width); trying up to n
|
||||
* candidates and updating up to n columns for each costs O(n^2), for
|
||||
* O(board width + n^2) local work per node and the same total state.
|
||||
*/
|
||||
template<bool Instrument, bool BreakD4Symmetry, bool PruneValleyCapacity,
|
||||
bool PruneLargeSquare, bool PruneComponents>
|
||||
auto search_solution_impl(size_t const n, SearchPolicy const policy,
|
||||
SearchCounters *const counters,
|
||||
ComponentPruning const component_pruning,
|
||||
ComponentSchedule const component_schedule)
|
||||
-> Results {
|
||||
auto const length = triangle_num(n);
|
||||
std::vector<size_t> skyline(length);
|
||||
Avail available(n + 1);
|
||||
for (size_t side = 0; side <= n; ++side) {
|
||||
available[side] = side;
|
||||
}
|
||||
std::vector<Square> squares;
|
||||
squares.reserve(length);
|
||||
static_cast<void>(
|
||||
search_skyline<Instrument, BreakD4Symmetry, PruneValleyCapacity,
|
||||
PruneLargeSquare, PruneComponents>(
|
||||
n, length, policy, skyline, available, squares, counters,
|
||||
component_pruning, component_schedule, false));
|
||||
|
||||
return {length, std::move(squares)};
|
||||
}
|
||||
|
||||
template<bool Instrument, bool BreakD4Symmetry, bool PruneComponents>
|
||||
auto search_solution_rules(size_t const n, SearchPolicy const policy,
|
||||
Pruning const pruning,
|
||||
SearchCounters *const counters,
|
||||
ComponentPruning const component_pruning,
|
||||
ComponentSchedule const component_schedule)
|
||||
-> Results {
|
||||
switch (pruning) {
|
||||
case Pruning::all:
|
||||
return search_solution_impl<Instrument, BreakD4Symmetry, true, true,
|
||||
PruneComponents>(
|
||||
n, policy, counters, component_pruning, component_schedule);
|
||||
case Pruning::valley_capacity:
|
||||
return search_solution_impl<Instrument, BreakD4Symmetry, true, false,
|
||||
PruneComponents>(
|
||||
n, policy, counters, component_pruning, component_schedule);
|
||||
case Pruning::large_square:
|
||||
return search_solution_impl<Instrument, BreakD4Symmetry, false, true,
|
||||
PruneComponents>(
|
||||
n, policy, counters, component_pruning, component_schedule);
|
||||
case Pruning::disabled:
|
||||
return search_solution_impl<Instrument, BreakD4Symmetry, false, false,
|
||||
PruneComponents>(
|
||||
n, policy, counters, component_pruning, component_schedule);
|
||||
}
|
||||
assert(false);
|
||||
return search_solution_impl<Instrument, BreakD4Symmetry, false, false,
|
||||
PruneComponents>(
|
||||
n, policy, counters, component_pruning, component_schedule);
|
||||
}
|
||||
|
||||
template<bool Instrument, bool BreakD4Symmetry>
|
||||
auto search_solution_dispatch(size_t const n, SearchPolicy const policy,
|
||||
Pruning const pruning,
|
||||
SearchCounters *const counters,
|
||||
ComponentPruning const component_pruning,
|
||||
ComponentSchedule const component_schedule)
|
||||
-> Results {
|
||||
if (component_pruning == ComponentPruning::disabled) {
|
||||
return search_solution_rules<Instrument, BreakD4Symmetry, false>(
|
||||
n, policy, pruning, counters, component_pruning,
|
||||
component_schedule);
|
||||
}
|
||||
return search_solution_rules<Instrument, BreakD4Symmetry, true>(
|
||||
n, policy, pruning, counters, component_pruning,
|
||||
component_schedule);
|
||||
}
|
||||
|
||||
auto search_solution(
|
||||
size_t const n,
|
||||
SearchPolicy const policy = SearchPolicy::ascending,
|
||||
SymmetryBreaking const symmetry =
|
||||
SymmetryBreaking::d4_unit_square,
|
||||
Pruning const pruning = Pruning::all,
|
||||
ComponentPruning const component_pruning =
|
||||
ComponentPruning::disabled,
|
||||
ComponentSchedule const component_schedule =
|
||||
ComponentSchedule::boundary)
|
||||
-> Results {
|
||||
if (symmetry == SymmetryBreaking::d4_unit_square) {
|
||||
return search_solution_dispatch<false, true>(
|
||||
n, policy, pruning, nullptr, component_pruning,
|
||||
component_schedule);
|
||||
}
|
||||
return search_solution_dispatch<false, false>(
|
||||
n, policy, pruning, nullptr, component_pruning,
|
||||
component_schedule);
|
||||
}
|
||||
|
||||
auto search_solution_instrumented(size_t const n,
|
||||
SearchCounters &counters,
|
||||
SearchPolicy const policy =
|
||||
SearchPolicy::ascending,
|
||||
SymmetryBreaking const symmetry =
|
||||
SymmetryBreaking::d4_unit_square,
|
||||
Pruning const pruning =
|
||||
Pruning::all,
|
||||
ComponentPruning const component_pruning =
|
||||
ComponentPruning::disabled,
|
||||
ComponentSchedule const component_schedule =
|
||||
ComponentSchedule::boundary)
|
||||
-> Results {
|
||||
counters = {};
|
||||
if (symmetry == SymmetryBreaking::d4_unit_square) {
|
||||
return search_solution_dispatch<true, true>(
|
||||
n, policy, pruning, &counters, component_pruning,
|
||||
component_schedule);
|
||||
}
|
||||
return search_solution_dispatch<true, false>(
|
||||
n, policy, pruning, &counters, component_pruning,
|
||||
component_schedule);
|
||||
}
|
||||
|
||||
/** Construct an odd-order solution from its even-order predecessor. */
|
||||
auto construct_odd_solution(size_t const odd_order, Results predecessor)
|
||||
-> Results {
|
||||
assert(odd_order >= 9);
|
||||
assert(odd_order % 2 == 1);
|
||||
assert(predecessor.length() == triangle_num(odd_order - 1));
|
||||
|
||||
auto const old_length = predecessor.length();
|
||||
auto const new_length = triangle_num(odd_order);
|
||||
std::vector<Square> squares;
|
||||
squares.reserve(predecessor.squares().size() + odd_order);
|
||||
for (auto const &square: predecessor.squares()) {
|
||||
auto const x = square.pos() % old_length;
|
||||
auto const y = square.pos() / old_length;
|
||||
squares.emplace_back(x + y * new_length, square.length());
|
||||
}
|
||||
|
||||
for (size_t y = 0; y < old_length; y += odd_order) {
|
||||
squares.emplace_back(old_length + y * new_length, odd_order);
|
||||
}
|
||||
for (size_t x = 0; x <= old_length; x += odd_order) {
|
||||
squares.emplace_back(x + old_length * new_length, odd_order);
|
||||
}
|
||||
return {new_length, std::move(squares)};
|
||||
}
|
||||
|
||||
[[nodiscard]] auto uses_odd_construction(size_t const n) noexcept -> bool {
|
||||
return n >= 9 && n % 2 == 1;
|
||||
}
|
||||
|
||||
auto find_solution(
|
||||
size_t const n,
|
||||
SearchPolicy const policy = SearchPolicy::ascending,
|
||||
SymmetryBreaking const symmetry =
|
||||
SymmetryBreaking::d4_unit_square,
|
||||
Pruning const pruning = Pruning::all,
|
||||
ComponentPruning const component_pruning =
|
||||
ComponentPruning::disabled,
|
||||
ComponentSchedule const component_schedule =
|
||||
ComponentSchedule::boundary) -> Results {
|
||||
if (uses_odd_construction(n)) {
|
||||
return construct_odd_solution(
|
||||
n, search_solution(
|
||||
n - 1, policy, symmetry, pruning, component_pruning,
|
||||
component_schedule));
|
||||
}
|
||||
return search_solution(n, policy, symmetry, pruning, component_pruning,
|
||||
component_schedule);
|
||||
}
|
||||
|
||||
auto find_solution_instrumented(size_t const n,
|
||||
SearchCounters &counters) noexcept -> Results {
|
||||
counters = {};
|
||||
return find_solution_impl<true>(n, &counters);
|
||||
SearchCounters &counters,
|
||||
SearchPolicy const policy =
|
||||
SearchPolicy::ascending,
|
||||
SymmetryBreaking const symmetry =
|
||||
SymmetryBreaking::d4_unit_square,
|
||||
Pruning const pruning =
|
||||
Pruning::all,
|
||||
ComponentPruning const component_pruning =
|
||||
ComponentPruning::disabled,
|
||||
ComponentSchedule const component_schedule =
|
||||
ComponentSchedule::boundary)
|
||||
-> Results {
|
||||
if (uses_odd_construction(n)) {
|
||||
return construct_odd_solution(
|
||||
n, search_solution_instrumented(
|
||||
n - 1, counters, policy, symmetry, pruning,
|
||||
component_pruning, component_schedule));
|
||||
}
|
||||
return search_solution_instrumented(
|
||||
n, counters, policy, symmetry, pruning, component_pruning,
|
||||
component_schedule);
|
||||
}
|
||||
} // anon namespace
|
||||
|
||||
|
||||
@@ -0,0 +1,2 @@
|
||||
# Optional research dependency; not used by the build or default solver.
|
||||
ortools>=9.14,<10
|
||||
@@ -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())
|
||||
+487
-22
@@ -8,6 +8,7 @@
|
||||
|
||||
#include <algorithm>
|
||||
#include <array>
|
||||
#include <span>
|
||||
#include <sstream>
|
||||
#include <string>
|
||||
|
||||
@@ -16,6 +17,8 @@ namespace {
|
||||
std::uint64_t x;
|
||||
std::uint64_t y;
|
||||
std::uint64_t side;
|
||||
|
||||
auto operator==(Placement const &) const noexcept -> bool = default;
|
||||
};
|
||||
|
||||
struct Validation {
|
||||
@@ -148,21 +151,6 @@ namespace {
|
||||
return Results(side, std::move(squares));
|
||||
}
|
||||
|
||||
auto construct_next_odd(std::uint64_t even_order,
|
||||
std::vector<Placement> placements)
|
||||
-> std::vector<Placement> {
|
||||
auto const old_side = even_order * (even_order + 1) / 2;
|
||||
auto const square_side = even_order + 1;
|
||||
|
||||
for (std::uint64_t y = 0; y < old_side; y += square_side) {
|
||||
placements.push_back({old_side, y, square_side});
|
||||
}
|
||||
for (std::uint64_t x = 0; x <= old_side; x += square_side) {
|
||||
placements.push_back({x, old_side, square_side});
|
||||
}
|
||||
return placements;
|
||||
}
|
||||
|
||||
auto expect(bool condition, std::string const &message) -> int {
|
||||
if (condition) {
|
||||
return 0;
|
||||
@@ -178,6 +166,35 @@ namespace {
|
||||
});
|
||||
}
|
||||
|
||||
auto d4_orbit(Placement const &placement, std::uint64_t const length)
|
||||
-> std::array<Placement, 8> {
|
||||
auto const far_x = length - 1 - placement.x;
|
||||
auto const far_y = length - 1 - placement.y;
|
||||
return {{
|
||||
{placement.x, placement.y, placement.side},
|
||||
{far_y, placement.x, placement.side},
|
||||
{far_x, far_y, placement.side},
|
||||
{placement.y, far_x, placement.side},
|
||||
{far_x, placement.y, placement.side},
|
||||
{far_y, far_x, placement.side},
|
||||
{placement.x, far_y, placement.side},
|
||||
{placement.y, placement.x, placement.side},
|
||||
}};
|
||||
}
|
||||
|
||||
auto canonical_members(Placement const &placement, std::uint64_t const length)
|
||||
-> std::vector<Placement> {
|
||||
auto orbit = d4_orbit(placement, length);
|
||||
std::vector<Placement> members;
|
||||
for (auto const &member: orbit) {
|
||||
if (canonical_unit_position(member.x, member.y, length) &&
|
||||
std::ranges::find(members, member) == members.end()) {
|
||||
members.push_back(member);
|
||||
}
|
||||
}
|
||||
return members;
|
||||
}
|
||||
|
||||
auto test_validator() -> int {
|
||||
int failures = 0;
|
||||
auto const valid = known_order_8();
|
||||
@@ -225,10 +242,66 @@ namespace {
|
||||
}
|
||||
|
||||
auto test_construction() -> int {
|
||||
auto const constructed = construct_next_odd(8, known_order_8());
|
||||
auto const validation = validate(9, 45, 45, constructed);
|
||||
return expect(validation.valid(),
|
||||
"even-to-odd construction was rejected:\n" + validation.text());
|
||||
auto predecessor = renderable_result(36, known_order_8());
|
||||
auto const predecessor_count = predecessor.squares().size();
|
||||
auto const constructed = construct_odd_solution(9, std::move(predecessor));
|
||||
auto const converted = to_independent(constructed);
|
||||
auto const validation = validate(9, constructed);
|
||||
|
||||
int failures = 0;
|
||||
failures += expect(
|
||||
validation.valid(),
|
||||
"even-to-odd construction was rejected:\n" + validation.text());
|
||||
failures += expect(constructed.length() == 45,
|
||||
"constructed board has the wrong side length");
|
||||
failures += expect(converted.placements.size() == predecessor_count + 9,
|
||||
"construction did not add exactly nine squares");
|
||||
|
||||
auto const expected_border = std::array<Placement, 9>{{
|
||||
{36, 0, 9}, {36, 9, 9}, {36, 18, 9}, {36, 27, 9},
|
||||
{0, 36, 9}, {9, 36, 9}, {18, 36, 9}, {27, 36, 9},
|
||||
{36, 36, 9},
|
||||
}};
|
||||
failures += expect(
|
||||
std::ranges::equal(
|
||||
std::span(converted.placements).subspan(predecessor_count),
|
||||
expected_border),
|
||||
"constructed border coordinates are incorrect");
|
||||
failures += expect(
|
||||
std::ranges::equal(
|
||||
std::span(converted.placements).first(predecessor_count),
|
||||
known_order_8()),
|
||||
"construction translated predecessor coordinates unexpectedly");
|
||||
return failures;
|
||||
}
|
||||
|
||||
auto test_odd_solver_route() -> int {
|
||||
SearchCounters even_counters;
|
||||
SearchCounters odd_counters;
|
||||
auto const even =
|
||||
find_solution_instrumented(8, even_counters, SearchPolicy::best_fit);
|
||||
auto const odd =
|
||||
find_solution_instrumented(9, odd_counters, SearchPolicy::best_fit);
|
||||
|
||||
int failures = 0;
|
||||
failures += expect(
|
||||
!uses_odd_construction(1) && !uses_odd_construction(7) &&
|
||||
!uses_odd_construction(8) && uses_odd_construction(9) &&
|
||||
!uses_odd_construction(10) && uses_odd_construction(11),
|
||||
"odd construction route does not preserve direct handling boundaries");
|
||||
auto const validation = validate(9, odd);
|
||||
failures += expect(validation.valid(),
|
||||
"order-9 routed result is invalid:\n" + validation.text());
|
||||
failures += expect(odd.squares().size() == even.squares().size() + 9,
|
||||
"order-9 route did not construct from order 8");
|
||||
failures += expect(
|
||||
odd_counters.search_nodes == even_counters.search_nodes &&
|
||||
odd_counters.loop_iterations == even_counters.loop_iterations &&
|
||||
odd_counters.attempted_placements ==
|
||||
even_counters.attempted_placements &&
|
||||
odd_counters.backtracks == even_counters.backtracks,
|
||||
"order-9 route did not perform exactly the order-8 search");
|
||||
return failures;
|
||||
}
|
||||
|
||||
auto test_rendering() -> int {
|
||||
@@ -293,11 +366,385 @@ namespace {
|
||||
failures += expect(counters.attempted_placements > 0 &&
|
||||
counters.backtracks > 0,
|
||||
"instrumented solver did not count placements/backtracks");
|
||||
failures += expect(counters.prune_checks == 0 &&
|
||||
counters.prune_hits == 0 &&
|
||||
failures += expect(counters.prune_checks >= counters.prune_hits &&
|
||||
counters.valley_capacity_checks >=
|
||||
counters.valley_capacity_prunes &&
|
||||
counters.large_square_checks >=
|
||||
counters.large_square_prunes &&
|
||||
counters.component_area_checks >=
|
||||
counters.component_area_prunes &&
|
||||
counters.component_area_prunes ==
|
||||
counters.component_gcd_prunes +
|
||||
counters.component_subset_prunes &&
|
||||
counters.generated_tasks == 0 &&
|
||||
counters.completed_tasks == 0,
|
||||
"unimplemented solver counters were not zero");
|
||||
"search counters are inconsistent");
|
||||
return failures;
|
||||
}
|
||||
|
||||
auto test_d4_symmetry() -> int {
|
||||
int failures = 0;
|
||||
|
||||
// A generic cell has eight distinct images: identity, three rotations,
|
||||
// and four reflected rotations. Exactly one must survive.
|
||||
auto const generic = d4_orbit({5, 9, 1}, 36);
|
||||
auto distinct_generic = std::vector<Placement>(generic.begin(),
|
||||
generic.end());
|
||||
std::ranges::sort(
|
||||
distinct_generic, {}, [](Placement const &placement) {
|
||||
return std::array{placement.x, placement.y};
|
||||
});
|
||||
distinct_generic.erase(
|
||||
std::ranges::unique(distinct_generic).begin(),
|
||||
distinct_generic.end());
|
||||
failures += expect(distinct_generic.size() == generic.size(),
|
||||
"generic D4 test point does not have eight images");
|
||||
for (std::size_t index = 0; index < generic.size(); ++index) {
|
||||
failures += expect(
|
||||
canonical_members(generic[index], 36) ==
|
||||
std::vector<Placement>{{5, 9, 1}},
|
||||
"D4 transform " + std::to_string(index) +
|
||||
" did not select the same canonical representative");
|
||||
}
|
||||
|
||||
// Closed boundaries are important because diagonal, midline, corner, and
|
||||
// centre cells have non-trivial stabilizers and therefore smaller orbits.
|
||||
for (auto const test_case:
|
||||
std::array<std::pair<std::uint64_t, Placement>, 8>{{
|
||||
{36, {0, 0, 1}},
|
||||
{36, {0, 17, 1}},
|
||||
{36, {7, 7, 1}},
|
||||
{36, {7, 17, 1}},
|
||||
{45, {0, 22, 1}},
|
||||
{45, {11, 11, 1}},
|
||||
{45, {11, 22, 1}},
|
||||
{45, {22, 22, 1}},
|
||||
}}) {
|
||||
failures += expect(
|
||||
canonical_members(test_case.second, test_case.first).size() == 1,
|
||||
"boundary orbit did not retain exactly one distinct representative");
|
||||
}
|
||||
failures += expect(
|
||||
canonical_unit_position(7, 17, 36) &&
|
||||
!canonical_unit_position(8, 7, 36) &&
|
||||
!canonical_unit_position(7, 18, 36) &&
|
||||
canonical_unit_position(22, 22, 45) &&
|
||||
!canonical_unit_position(22, 23, 45),
|
||||
"canonical triangle mishandled a diagonal or midline boundary");
|
||||
|
||||
SearchCounters enabled_counters;
|
||||
SearchCounters disabled_counters;
|
||||
auto const enabled = search_solution_instrumented(
|
||||
8, enabled_counters, SearchPolicy::ascending,
|
||||
SymmetryBreaking::d4_unit_square, Pruning::disabled,
|
||||
ComponentPruning::disabled);
|
||||
auto const disabled = search_solution_instrumented(
|
||||
8, disabled_counters, SearchPolicy::ascending,
|
||||
SymmetryBreaking::disabled, Pruning::disabled,
|
||||
ComponentPruning::disabled);
|
||||
auto enabled_validation = validate(8, enabled);
|
||||
auto disabled_validation = validate(8, disabled);
|
||||
failures += expect(
|
||||
enabled_validation.valid(),
|
||||
"symmetry-enabled solution failed independent validation:\n" +
|
||||
enabled_validation.text());
|
||||
failures += expect(
|
||||
disabled_validation.valid(),
|
||||
"symmetry-disabled solution failed independent validation:\n" +
|
||||
disabled_validation.text());
|
||||
|
||||
auto const unit = std::ranges::find_if(
|
||||
enabled.squares(),
|
||||
[](Square const &square) { return square.length() == 1; });
|
||||
failures += expect(
|
||||
unit != enabled.squares().end() &&
|
||||
canonical_unit_position(unit->pos() % enabled.length(),
|
||||
unit->pos() / enabled.length(),
|
||||
enabled.length()),
|
||||
"symmetry-enabled search placed the unique unit square outside the "
|
||||
"canonical region");
|
||||
failures += expect(
|
||||
enabled_counters.prune_checks > 0 && enabled_counters.prune_hits > 0 &&
|
||||
disabled_counters.prune_checks == 0 &&
|
||||
disabled_counters.prune_hits == 0,
|
||||
"symmetry instrumentation did not distinguish enabled and disabled "
|
||||
"search");
|
||||
return failures;
|
||||
}
|
||||
|
||||
auto test_skyline_search() -> int {
|
||||
int failures = 0;
|
||||
auto const narrowest =
|
||||
smallest_valley(std::vector<std::uint64_t>{4, 2, 2, 4, 0, 0, 0, 4});
|
||||
failures += expect(
|
||||
narrowest.x == 1 && narrowest.height == 2 && narrowest.width == 2,
|
||||
"skyline did not select the smallest-width valley");
|
||||
|
||||
auto const tie =
|
||||
smallest_valley(std::vector<std::uint64_t>{4, 1, 4, 4, 2, 4});
|
||||
failures += expect(tie.x == 1 && tie.height == 1 && tie.width == 1,
|
||||
"skyline valley tie-break is not deterministic");
|
||||
|
||||
SearchCounters descending_counters;
|
||||
auto const descending = search_solution_instrumented(
|
||||
8, descending_counters, SearchPolicy::descending);
|
||||
auto validation = validate(8, descending);
|
||||
failures += expect(
|
||||
validation.valid(),
|
||||
"descending skyline search returned an invalid order-8 solution:\n" +
|
||||
validation.text());
|
||||
|
||||
SearchCounters direct_nine_counters;
|
||||
auto const direct_nine = search_solution_instrumented(
|
||||
9, direct_nine_counters, SearchPolicy::ascending);
|
||||
validation = validate(9, direct_nine);
|
||||
failures += expect(
|
||||
validation.valid(),
|
||||
"direct skyline search returned an invalid order-9 solution:\n" +
|
||||
validation.text());
|
||||
failures += expect(
|
||||
direct_nine_counters.search_nodes != descending_counters.search_nodes,
|
||||
"direct order-9 coverage unexpectedly reused predecessor construction");
|
||||
|
||||
SearchCounters ascending_exhaustive;
|
||||
SearchCounters descending_exhaustive;
|
||||
SearchCounters best_fit_exhaustive;
|
||||
static_cast<void>(search_solution_instrumented(
|
||||
5, ascending_exhaustive, SearchPolicy::ascending));
|
||||
static_cast<void>(search_solution_instrumented(
|
||||
5, descending_exhaustive, SearchPolicy::descending));
|
||||
static_cast<void>(search_solution_instrumented(
|
||||
5, best_fit_exhaustive, SearchPolicy::best_fit));
|
||||
failures += expect(
|
||||
ascending_exhaustive.search_nodes == descending_exhaustive.search_nodes &&
|
||||
ascending_exhaustive.search_nodes == best_fit_exhaustive.search_nodes,
|
||||
"candidate policy changed the exhaustive skyline search space");
|
||||
return failures;
|
||||
}
|
||||
|
||||
auto test_valley_capacity_pruning() -> int {
|
||||
int failures = 0;
|
||||
Avail available(5);
|
||||
|
||||
available[1] = 1;
|
||||
failures += expect(
|
||||
!valley_has_sufficient_capacity(
|
||||
{1, 0, 1}, std::vector<std::uint64_t>{4, 0, 4}, available),
|
||||
"width-one gap accepted insufficient unit-square capacity");
|
||||
|
||||
available = {};
|
||||
available.resize(5);
|
||||
available[2] = 1;
|
||||
failures += expect(
|
||||
!valley_has_sufficient_capacity(
|
||||
{1, 0, 2}, std::vector<std::uint64_t>{4, 0, 0, 4}, available),
|
||||
"width-two gap accepted insufficient narrow-piece area");
|
||||
available[2] = 2;
|
||||
failures += expect(
|
||||
valley_has_sufficient_capacity(
|
||||
{1, 0, 2}, std::vector<std::uint64_t>{4, 0, 0, 4}, available),
|
||||
"width-two gap rejected exactly sufficient narrow-piece area");
|
||||
|
||||
available = {};
|
||||
available.resize(5);
|
||||
available[1] = 1;
|
||||
available[2] = 1;
|
||||
failures += expect(
|
||||
!valley_has_sufficient_capacity(
|
||||
{1, 2, 2}, std::vector<std::uint64_t>{5, 2, 2, 5}, available),
|
||||
"general valley accepted less area than required to reach its rim");
|
||||
available[2] = 2;
|
||||
failures += expect(
|
||||
valley_has_sufficient_capacity(
|
||||
{1, 2, 2}, std::vector<std::uint64_t>{5, 2, 2, 5}, available),
|
||||
"general valley rejected sufficient fitting-square area");
|
||||
|
||||
for (auto const order: std::array<std::uint64_t, 5>{1, 2, 3, 4, 5}) {
|
||||
SearchCounters pruned_counters;
|
||||
SearchCounters unpruned_counters;
|
||||
auto const pruned = search_solution_instrumented(
|
||||
order, pruned_counters, SearchPolicy::ascending,
|
||||
SymmetryBreaking::disabled, Pruning::valley_capacity,
|
||||
ComponentPruning::disabled);
|
||||
auto const unpruned = search_solution_instrumented(
|
||||
order, unpruned_counters, SearchPolicy::ascending,
|
||||
SymmetryBreaking::disabled, Pruning::disabled,
|
||||
ComponentPruning::disabled);
|
||||
failures += expect(
|
||||
pruned.squares().empty() == unpruned.squares().empty(),
|
||||
"valley pruning changed exhaustive order-" +
|
||||
std::to_string(order) + " feasibility");
|
||||
failures += expect(
|
||||
pruned_counters.search_nodes <= unpruned_counters.search_nodes,
|
||||
"valley pruning enlarged the exhaustive order-" +
|
||||
std::to_string(order) + " search");
|
||||
}
|
||||
|
||||
SearchCounters counters;
|
||||
static_cast<void>(search_solution_instrumented(
|
||||
5, counters, SearchPolicy::ascending, SymmetryBreaking::disabled,
|
||||
Pruning::valley_capacity, ComponentPruning::disabled));
|
||||
failures += expect(
|
||||
counters.valley_capacity_checks > 0 &&
|
||||
counters.valley_capacity_prunes > 0 &&
|
||||
counters.prune_checks == counters.valley_capacity_checks &&
|
||||
counters.prune_hits == counters.valley_capacity_prunes,
|
||||
"valley pruning instrumentation did not count checks and hits");
|
||||
return failures;
|
||||
}
|
||||
|
||||
auto test_large_square_pruning() -> int {
|
||||
int failures = 0;
|
||||
auto const fragmented =
|
||||
std::vector<std::uint64_t>{0, 5, 0, 5, 0, 5};
|
||||
failures += expect(
|
||||
!skyline_has_empty_square(fragmented, 2),
|
||||
"large-square check accepted a fragmented state without a 2x2 box");
|
||||
failures += expect(
|
||||
skyline_has_empty_square(
|
||||
std::vector<std::uint64_t>{0, 0, 5, 5, 5, 5}, 2),
|
||||
"large-square check rejected an available 2x2 box");
|
||||
|
||||
Avail available(4);
|
||||
available[1] = 1;
|
||||
available[2] = 1;
|
||||
failures += expect(
|
||||
!remaining_large_square_fits(fragmented, available),
|
||||
"remaining-square check ignored the impossible largest square");
|
||||
available[2] = 0;
|
||||
failures += expect(
|
||||
remaining_large_square_fits(fragmented, available),
|
||||
"remaining-square check did not use geometric size monotonicity");
|
||||
|
||||
// The fragmented profile has 21 empty cells, more than the area of the
|
||||
// remaining 2x2 square, but no two adjacent columns have two free rows.
|
||||
std::uint64_t filled_area = 0;
|
||||
for (auto const height: fragmented) {
|
||||
filled_area += height;
|
||||
}
|
||||
failures += expect(
|
||||
filled_area <= 36 - 4,
|
||||
"fragmented test state does not have sufficient total empty area");
|
||||
|
||||
for (auto const order: std::array<std::uint64_t, 5>{1, 2, 3, 4, 5}) {
|
||||
SearchCounters pruned_counters;
|
||||
SearchCounters baseline_counters;
|
||||
auto const pruned = search_solution_instrumented(
|
||||
order, pruned_counters, SearchPolicy::ascending,
|
||||
SymmetryBreaking::disabled, Pruning::all,
|
||||
ComponentPruning::disabled);
|
||||
auto const baseline = search_solution_instrumented(
|
||||
order, baseline_counters, SearchPolicy::ascending,
|
||||
SymmetryBreaking::disabled, Pruning::valley_capacity,
|
||||
ComponentPruning::disabled);
|
||||
failures += expect(
|
||||
pruned.squares().empty() == baseline.squares().empty(),
|
||||
"large-square pruning changed exhaustive order-" +
|
||||
std::to_string(order) + " feasibility");
|
||||
failures += expect(
|
||||
pruned_counters.search_nodes <= baseline_counters.search_nodes,
|
||||
"large-square pruning enlarged the exhaustive order-" +
|
||||
std::to_string(order) + " search");
|
||||
}
|
||||
|
||||
SearchCounters counters;
|
||||
static_cast<void>(search_solution_instrumented(
|
||||
5, counters, SearchPolicy::ascending, SymmetryBreaking::disabled,
|
||||
Pruning::large_square, ComponentPruning::disabled));
|
||||
failures += expect(
|
||||
counters.large_square_checks > 0 &&
|
||||
counters.large_square_prunes > 0 &&
|
||||
counters.prune_checks == counters.large_square_checks &&
|
||||
counters.prune_hits == counters.large_square_prunes,
|
||||
"large-square instrumentation did not count checks and prunes");
|
||||
return failures;
|
||||
}
|
||||
|
||||
auto test_component_area_pruning() -> int {
|
||||
int failures = 0;
|
||||
auto const components =
|
||||
empty_component_areas(std::vector<std::uint64_t>{2, 4, 1, 1});
|
||||
failures += expect(
|
||||
components == std::vector<std::uint64_t>{2, 6},
|
||||
"full-height boundary did not split the expected component areas");
|
||||
failures += expect(
|
||||
empty_component_areas(
|
||||
std::vector<std::uint64_t>{2, 1, 4, 4}) ==
|
||||
std::vector<std::uint64_t>{5},
|
||||
"adjacent non-full columns did not remain one empty component");
|
||||
|
||||
Avail gcd_available(3);
|
||||
gcd_available[2] = 2;
|
||||
failures += expect(
|
||||
component_area_feasibility(
|
||||
std::vector<std::uint64_t>{2, 4, 1, 1}, gcd_available,
|
||||
ComponentPruning::gcd) ==
|
||||
ComponentFeasibility::gcd_failure,
|
||||
"component gcd check accepted indivisible component areas");
|
||||
|
||||
Avail subset_available(3);
|
||||
subset_available[1] = 1;
|
||||
subset_available[2] = 1;
|
||||
failures += expect(
|
||||
component_area_feasibility(
|
||||
std::vector<std::uint64_t>{2, 4, 1, 4}, subset_available,
|
||||
ComponentPruning::gcd) ==
|
||||
ComponentFeasibility::feasible,
|
||||
"component gcd check rejected a gcd-one state");
|
||||
failures += expect(
|
||||
component_area_feasibility(
|
||||
std::vector<std::uint64_t>{2, 4, 1, 4}, subset_available,
|
||||
ComponentPruning::subset_sum) ==
|
||||
ComponentFeasibility::subset_sum_failure,
|
||||
"bounded subset sum accepted unreachable component areas");
|
||||
failures += expect(
|
||||
component_area_feasibility(
|
||||
std::vector<std::uint64_t>{3, 4, 0, 4}, subset_available,
|
||||
ComponentPruning::subset_sum) ==
|
||||
ComponentFeasibility::feasible,
|
||||
"bounded subset sum rejected reachable component areas");
|
||||
|
||||
for (auto const order: std::array<std::uint64_t, 5>{1, 2, 3, 4, 5}) {
|
||||
SearchCounters pruned_counters;
|
||||
SearchCounters periodic_counters;
|
||||
SearchCounters baseline_counters;
|
||||
auto const pruned = search_solution_instrumented(
|
||||
order, pruned_counters, SearchPolicy::ascending,
|
||||
SymmetryBreaking::disabled, Pruning::all,
|
||||
ComponentPruning::subset_sum);
|
||||
auto const periodic = search_solution_instrumented(
|
||||
order, periodic_counters, SearchPolicy::ascending,
|
||||
SymmetryBreaking::disabled, Pruning::all,
|
||||
ComponentPruning::subset_sum,
|
||||
ComponentSchedule::periodic_eight);
|
||||
auto const baseline = search_solution_instrumented(
|
||||
order, baseline_counters, SearchPolicy::ascending,
|
||||
SymmetryBreaking::disabled, Pruning::all,
|
||||
ComponentPruning::disabled);
|
||||
failures += expect(
|
||||
pruned.squares().empty() == baseline.squares().empty() &&
|
||||
periodic.squares().empty() == baseline.squares().empty(),
|
||||
"component pruning changed exhaustive order-" +
|
||||
std::to_string(order) + " feasibility");
|
||||
failures += expect(
|
||||
pruned_counters.search_nodes <= baseline_counters.search_nodes &&
|
||||
periodic_counters.search_nodes <=
|
||||
baseline_counters.search_nodes,
|
||||
"component pruning enlarged the exhaustive order-" +
|
||||
std::to_string(order) + " search");
|
||||
}
|
||||
|
||||
SearchCounters counters;
|
||||
static_cast<void>(search_solution_instrumented(
|
||||
5, counters, SearchPolicy::ascending, SymmetryBreaking::disabled,
|
||||
Pruning::disabled, ComponentPruning::subset_sum));
|
||||
failures += expect(
|
||||
counters.component_area_checks > 0 &&
|
||||
counters.component_area_prunes > 0 &&
|
||||
counters.component_area_prunes ==
|
||||
counters.component_gcd_prunes +
|
||||
counters.component_subset_prunes,
|
||||
"component-area instrumentation did not count checks and prune kinds");
|
||||
return failures;
|
||||
}
|
||||
|
||||
@@ -328,6 +775,9 @@ int main(int argc, char **argv) {
|
||||
if (test == "construction") {
|
||||
return test_construction();
|
||||
}
|
||||
if (test == "solver-odd-route") {
|
||||
return test_odd_solver_route();
|
||||
}
|
||||
if (test == "rendering") {
|
||||
return test_rendering();
|
||||
}
|
||||
@@ -340,6 +790,21 @@ int main(int argc, char **argv) {
|
||||
if (test == "search-counters") {
|
||||
return test_search_counters();
|
||||
}
|
||||
if (test == "skyline-search") {
|
||||
return test_skyline_search();
|
||||
}
|
||||
if (test == "d4-symmetry") {
|
||||
return test_d4_symmetry();
|
||||
}
|
||||
if (test == "valley-capacity") {
|
||||
return test_valley_capacity_pruning();
|
||||
}
|
||||
if (test == "large-square") {
|
||||
return test_large_square_pruning();
|
||||
}
|
||||
if (test == "component-area") {
|
||||
return test_component_area_pruning();
|
||||
}
|
||||
std::cerr << "unknown test: " << test << '\n';
|
||||
return 2;
|
||||
}
|
||||
|
||||
@@ -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())
|
||||
@@ -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())
|
||||
Reference in New Issue
Block a user