solver: prune insufficient valley capacity

A selected valley cannot admit a square wider than itself until it reaches the lower neighbouring rim. Reject states whose remaining narrow-square area cannot fill that strip, including width-one and width-two gaps.

Keep an unpruned benchmark mode and dedicated counters so the rule remains independently measurable. Record the soundness argument and the measured default-on improvement.

Tests: Debug CTest (12 passed)

Tests: ASan+UBSan CTest (12 passed)

Refs: #10
This commit was merged in pull request #26.
This commit is contained in:
Codex instance
2026-07-31 08:11:30 +01:00
parent f37e08768d
commit e27427d231
6 changed files with 234 additions and 26 deletions
+37 -2
View File
@@ -21,6 +21,8 @@ and `--candidate-order`. The choices are `ascending`, `descending`, and
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 valley-capacity rule described below.
Pass `--no-pruning` to obtain an otherwise identical unpruned search.
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:
@@ -45,8 +47,9 @@ 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
@@ -72,6 +75,38 @@ 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.
## D4 board symmetry
Every solution contains exactly one 1-by-1 square. Rotations and reflections