[Mac agent] CC engine: per-half probe between tiebreak and MRV + reversed-BFS row order (-cc-roworder=auto)

Hub: #15. Follow-up of #183 (PR #204, stacked on #162 / PR #180; none merged).

Hypothesis

#183 showed that MRV branching plus the reversed-BFS row order (-cc-rules=...,tiebreak,mrv -cc-roworder=bfs) depends on the code family and on the half:

large BB codes and TN_496 search 2.5-3.7x faster at equal levels;
the Tier 5 LP codes are 1.2-3x slower;
most row-weight-9 TN codes are 1.2-1.8x slower, and on TN_180 the effect differs between the X and Z halves.

A per-half probe should keep the gains and remove the regressions.

Change

New value -cc-roworder=auto. Each searched half starts with configuration A (input row order, the given rules without mrv; with the tiebreak rules this is the #162 configuration).

At the first level of that half whose search takes at least -cc-probe=S seconds (default 1) and ends EMPTY:

the same level is run again with configuration B (reversed-BFS row order, the given rules with mrv);
the re-run is aborted through the existing poll hook once it uses A's search time;
if B finishes first, B searches every later level of that half, otherwise A does.

The probe happens once per half and costs at most one extra level of the size that triggered it.

Soundness

A and B are each exact level searches ([Mac agent] CC engine: orbit-compatible even-weight overlap tie-break #162, [Mac agent] CC engine: MRV branching and BFS row order on top of tiebreak #183 proofs), and the probe level is already refuted by A.
Choosing which exact search runs the later levels cannot change any verdict. The level-w precondition holds for every later level whichever configuration refuted the earlier ones.
An aborted probe changes no bound.
A probe that disagrees with A (FOUND or INCONSISTENT after A's EMPTY) is a trap.

Plan

Tests: driver oracle with forced switch / stay / time-based probes, with and without the finder; mutant: an aborted probe taken as a refuted level.
Tier 0-4 on 5-seed medians, vs main and vs tb.
Tier 5 (6 h): LP_1428 / 1768 / 2610 and the other LP codes, TN_180 / 216 / 252 / 288, BB_360 / 756 / 864 / 1080.
yfclab2 cores 33-39 and 41-43.

GH-206: probes at 0.1 s then 30x (-cc-probe-growth), no probe when th…

GH-206: v2 Tier 0 records and Tier 1-4 seed panel (v1 records archived)

GH-206: one probe per half by default (-cc-probe-growth=0); re-probes…

GH-206: first Tier 5 run (growth 30) records, single-probe derivation…

GH-206: Tier 5 confirmation with the final binary (one probe per half)

Result: PR #215, stacked on #204; do not merge before the PI says merge.

Tier 0: PASS (1,800 auto driver runs against enumeration, 0 bad; mutant 21 caught; identity; GF(2) witnesses; flags).
Tier 1-4 panel: geomean vs main 1.001 (repeated, process floor) / 0.889 / 0.674 / 0.399; vs tb 0.997 / 0.902 / 0.666 / 0.428. No cell above 1.25, apart from the process-floor single shots in Tier 1.
Tier 5 confirmation (final binary, same-session references):
- BB_756, BB_864, BB_1080 and TN_496 are within 0.6-2.3 % of tb+mrv+bfs (lb 32 / 32 / 32 / 24).
- TN_252, TN_288 and TN_180 equal tb (TN_288 lb 22, TN_252 d=21 at 0.99x); TN_216 is 0.64x tb.
- The LP codes equal tb's search plus a 0.2-0.5 s probe.
First design (one probe at 1 s) failed Tier 3 and was replaced. Re-probes at 30x never changed a decision and cost up to one level each, so the default is one probe per half.

Merge GH-183 branch (with GH-162 and main c94d390, GH-157 charge defa…

Merge main (7d91569: GH-162 and GH-183 merges, stem renames #216) into …

Merge pull request #215 from guluchen/experiment/gh-206-cc-roworder-auto

Merged into main at 30ce62a as opt-in (PI-approved order 2026-10-31).

-cc-roworder still defaults to index, and the CC default rule set is unchanged (excl,pack,orbf,parity,leaf,overlap,charge).

Retarget and conflicts

PR CC engine: per-half probe between tiebreak and MRV + reversed-BFS row order (-cc-roworder=auto, GH-206; do not merge before PI says merge) #215 was retargeted to main after CC engine: MRV branching and seed-anchored reversed-BFS row order (GH-183, opt-in; do not merge before PI says merge) #204 merged.
I merged the updated [Mac agent] CC engine: MRV branching and BFS row order on top of tiebreak #183 branch into it, then main 7d91569.
Conflicts were resolved by keeping both sides:
- With -cc-roworder=auto, both HalfSearch objects (A and B) now get the [Mac agent] CC engine: fractional-charge / edge-cover node lower bounds #157 charge settings (lb_minr, lb_gap, lb_raise, lb_auto).
- DriverOptions keeps the [Mac agent] CC engine: fractional-charge / edge-cover node lower bounds #157 fields as well as the probe fields.
- cc_half.h keeps the ROWORDER_AUTO enum and the [Mac agent] CC engine: fractional-charge / edge-cover node lower bounds #157 LbWork/lb_charge API.
- -cc-mutant accepts 0..15 and 17..21. Mutant 21 keeps its number.
Tests: the auto driver configurations that stand for the candidate now use the new default rules (with charge) plus tiebreak. These are auto-switch, auto-time, auto-time-ubsearch, mutant21-switch and aut-auto-switch. The flag tests now also accept the default rules + tiebreak with -cc-roworder=auto.

Checks (yfclab2, cores 5-23, 4 GB cap)

make test-cc PASS:
- [Mac agent] CC engine: per-half probe between tiebreak and MRV + reversed-BFS row order (-cc-roworder=auto) #206 Part B: 1800 auto driver runs, 0 bad.
- Mutant 21: 18/400 runs wrong.
- Parts R and T and mutants 15 and 17-20 still caught.
make test-cc-flags PASS (514 checks).
Tier 0+1 answers equal the stems, 15/15 in each of three configurations: the CC default, -cc-roworder=auto, and -cc-rules=excl,pack,orbf,parity,leaf,overlap,charge,tiebreak -cc-roworder=auto.
With the flag off, the tier 0+1 -v logs are byte-identical to main 7d91569:
- -ub-search=off, -cc-stats and -cc-aut=off: 45/45.
- CC default: 14/15. The remaining one differs only in a time-sliced ub-search finder line.
GitHub CI passed.

Merge GH-206 stack (GH-162, GH-183, GH-206 and main c94d390 with GH-157…

GH-181 merge: restore the closing fi of the GH-206 flag section

Merge main (30ce62a: GH-162, GH-183, GH-206 merges) into GH-181

Navigation Menu

[Mac agent] CC engine: per-half probe between tiebreak and MRV + reversed-BFS row order (-cc-roworder=auto) #206

Hypothesis

Change

Soundness

Plan

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

[Mac agent] CC engine: per-half probe between tiebreak and MRV + reversed-BFS row order (-cc-roworder=auto) #206

Description

Hypothesis

Change

Soundness

Plan

Activity

guluchen commented on Oct 30, 2026

guluchen commented on Oct 30, 2026

Metadata

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

Issue actions