[guluchen]

Experiment record for #206 (hub #15). Stacked on PR #204 (#183), which is stacked on PR #180 (#162). Do not merge before the PI says merge.

What changed

New value -cc-roworder=auto (opt-in; the default stays index). Each searched CSS half holds two exact level searches:

• A: input row order, the given -cc-rules without mrv. With the tiebreak rules this is the [Mac agent] CC engine: orbit-compatible even-weight overlap tie-break #162 configuration.
• B: the [Mac agent] CC engine: MRV branching and BFS row order on top of tiebreak #183 reversed-BFS row order, the given rules with mrv.

A searches from level 1. At the first level that A refutes in at least -cc-probe=S seconds (default 0.1 s):

• B re-runs the same level, aborted through the existing poll hook once it has used A's search time (finder slices excluded);
• if B ends EMPTY first, B searches the rest of that half, otherwise A does;
• there is one probe per half, and no probe once the half is finished (lb >= U).

-cc-probe-growth=F (F >= 1) adds re-probes at F times the last probe level's time. It is off by default: in Tier 5 no re-probe ever changed a decision, and each cost one level.

Soundness (MODIFICATIONS.md, GH-206):

• A and B are each exact level searches.
• The precondition of every later level is established by the earlier refutations, whichever exact search produced them.
• A probe changes no bound: the probe level is already refuted, and an aborted probe is discarded.
• A probe that returns FOUND or INCONSISTENT after an EMPTY is a trap.
• Timing noise can change speed, never answers.

Test-only mutant 21: after every refuted level, the probe runs level w + 1 with a zero time cap, and an aborted probe is counted as a refuted level.

Development note

The first version (one probe at the first level >= 1 s, binary ab91aac) failed Tier 3: TN_144 was 1.33x tb, because the probe ran on the last refuted level. It also missed most Tier 2-3 gains, because those runs finish before a level reaches 1 s. Its records are in optimization/experiments/GH-206/v1_ab91aac/. The current version fixes both problems:

• probes start at 0.1 s;
• there is no probe once the half is finished;
• the default is one probe per half (14ec146 introduced the first two; fca5d3c sets the single-probe default).

Tier 0 (14ec146): PASS

• make test-cc: CC_ENGINE_TESTS PASS. Part B: 1,800 auto driver runs against enumeration, 0 bad. They cover probes after every refuted level that always or never switch, time-based probes with threshold 0 s and poll at every node, finder on and off, and tbbase asc. Part H auto configurations: 0 bad. Mutant 21: 18/400 runs wrong. Parts R, T and the rest: unchanged and passing.
• Identity vs [Mac agent] CC engine: MRV branching and BFS row order on top of tiebreak #183 d26070d on the tier0+1 -v logs: identical in 14 configurations. The only differences are 3 known timing-dependent MaxSAT ub-pre lines.
• Answers: 23 tier0-3 codes x 11 auto variants, 253 runs, all correct; 151 witnesses verified by an independent GF(2) script.
• make test-cc-flags: PASS (469 checks).

Tier 1-4 seed panel (5 seeds; cores 33-39 and 41-43)

Geomean of median wall ratios (max cell):

Tier	auto vs main	auto vs tb	tbmrvbfs (GH-183) vs main
1 (process floor, 11 repetitions)	1.001 (1.003)	0.997 (0.999)	1.004
2 (6)	0.889 (1.216)	0.902 (1.000)	0.642 (1.216)
3 (2)	0.674 (0.978)	0.666 (0.956)	0.586
4 (1)	0.399	0.428	0.404

• Tier 1: the single-shot panel shows LP_442 at 1.36, the usual 0.025 <-> 0.034 s process-floor flip. The repeated round-robin measurement gives every arm within ±0.5 % of main.
• Tier 2: the max cell 1.216 is LP_544, a 0.04 s run.
• Panel summary: auto keeps the Tier 3-4 gains (TN_144 0.46, TN_250 0.40 vs main) and part of the Tier 2 gains (BB_144 0.79, TN_108 0.67). On codes whose levels stay below 0.1 s (BB_288, GB_144, TN_200) it equals tb.

Tier 5 (6 h, default seed)

Confirmation run. Final binary fca5d3c (one probe per half), with same-session references from the same binary, on yfclab2 cores 24-35, 37-39, 41-43 (core 36 skipped: a root process uses ~16 % of it). Table: optimization/experiments/GH-206/S3_tier5_final/summary.md.

Code	Same-session reference	auto	Probe choice
BB_756_16_30to34	tbmrvbfs lb 32 @ 11952 s	lb 32 @ 12032 s (1.007)	B
BB_864_4_30to40	tbmrvbfs lb 32 @ 11473 s	lb 32 @ 11539 s (1.006)	B
BB_1080_4_30to48	tbmrvbfs lb 32 @ 8745 s	lb 32 @ 8949 s (1.023)	B
TN_496_2_23to30	tbmrvbfs lb 24 @ 12224 s	lb 24 @ 12308 s (1.007)	B
TN_252_2_21	tb d=21 @ 11477 s	d=21 @ 11376 s (0.991)	A, A
TN_288_2_22to24	tb lb 22 @ 20645 s	lb 22 @ 20344 s (0.985)	A, A
TN_216_4_18	tb d=18 @ 661 s	d=18 @ 426 s (0.644)	B (X), A (Z)
TN_180_2_17	tb d=17 @ 235 s	d=17 @ 176 s	A, A
BB_360_12_24	(tbmrvbfs 28 s, #204)	d=24 @ 34 s	B
LP_1428 / 1768 / 2610 / 1122 / 1054	tb 124.0 / 15.9 / 2.98 / 4.59 / 1.69 s (clean core 34)	124.2 / 16.2 / 3.20 / 5.07 / 1.86 s	A

• Node identity. auto's node counts at the largest common level equal those of the configuration it chose: BB L30, TN_252 L20, TN_180 L16, every LP level.
• Gains kept. On BB and TN_496, auto is within 0.6-2.3 % of tbmrvbfs.
• Regressions gone. On LP and the row-weight-9 TN codes, auto equals tb's search plus a 0.1-0.5 s probe.
• Relative to the CC engine: MRV branching and seed-anchored reversed-BFS row order (GH-183, opt-in; do not merge before PI says merge) #204 stack:
  • LP_1428: 1.5x slower with tbmrvbfs, equal to tb with auto.
  • TN_288: lb 21 with tbmrvbfs, lb 22 with auto.
  • TN_252: 1.17x slower with tbmrvbfs, equal to tb with auto.
• Relative to main / [Mac agent] CC engine: orbit-compatible even-weight overlap tie-break #162 tb (CC engine: MRV branching and seed-anchored reversed-BFS row order (GH-183, opt-in; do not merge before PI says merge) #204 records): BB_756 and BB_864 reach lb 32, where main and tb reach 30. BB_1080 reaches lb 32 at 8949 s, against 19378 s for tb.

First Tier 5 run (14ec146, re-probes at 30x; S2_tier5_growth30/). It made the same per-half decisions, and no re-probe ever switched. Each losing re-probe cost a full level, though, up to 9447 s on BB_864 at level 30. That is why the default is now one probe.

Cross-check of the #183 lower bounds (relabeled seeds 1-3, 8 h): BB_756 >= 32, BB_864 >= 32 and TN_496 >= 24 are REPRODUCED, 9/9 runs (see #183). Stems are unchanged.

Verdict

• Tier 0 passes. Tiers 2-4 pass vs main and vs tb; Tier 1 is a process-floor tie (±0.5 %).
• In Tier 5, auto keeps the MRV + reversed-BFS gains on BB and TN_496 (within 2.3 %) and removes the LP and row-weight-9 TN regressions: tb's search plus a probe of at most 0.5 s.
• Recommendation: if the PI adopts the CC engine: orbit-compatible even-weight overlap tie-break (GH-162, opt-in; do not merge before PI says merge) #180 / CC engine: MRV branching and seed-anchored reversed-BFS row order (GH-183, opt-in; do not merge before PI says merge) #204 stack, adopt it through -cc-roworder=auto, rather than through mrv plus -cc-roworder=bfs as fixed settings. Making it the CC default needs a separate PI decision.

Scientific semantics changed: no (opt-in flag; default output byte-identical).
PI action required: yes (adoption decision for the stack #180 / #204 / this PR).

🤖 Generated with Claude Code