GH-218: drop dense (4-cycle-rich) overlap rows from cap 16 on: fixes TN_216, costs TN_180 card-mto (PI decision)

MODIFICATIONS.md

@@ -34,6 +34,7 @@ New code, not derived from MaxCDCL.
 | Stern / Dumer collision mode of the shared finder (GH-146; `-ub-isd=off\|stern\|dumer[:P,L,W,B,R]`, default stern since 2026-10-23, PI; `-ub-isd=off` = previous finder, GH-140) | Applies to the CC `-ub-search` finder and to the MaxSAT `-ub-pre` pre-pass (both use `UbFinder`). Per round: W Canteaut-Chabaud pivot swaps on the stored systematic columns (or a fresh elimination), a random split of the information set into two halves and a random window of L reduced rows; all subsets of size <= P of each half (`dumer`: the window pivot columns are elements too), bucketed by the window part of their column sum; every colliding pair with different detector parities is weighed, kept words go through the unchanged detector check, stabilizer local improvement and the driver's / pre-pass's independent verification. Single systematic words are also tried every round. Defaults from S0: P 2, L automatic (about log2 of the list size), W 32, B 1 round per iteration. `-ub-isd=off` = the GH-140 enumeration byte for byte (identical to GH-144's 6d2b7a1 on tier0+1). Soundness below (GH-146). See `optimization/experiments/GH-146/`. |
 | Tanner-graph automorphism candidates for the CC engine (GH-152; `-cc-aut=on\|off`, default on since 2026-10-28, PI decision; `-cc-aut=off` = previous CC search; experimental) | CC wrapper `min_distance_css_cc` only. With `-cc-aut=on`, `distcc::find_row_automorphisms` (`src/cc/cc_aut.{h,cc}`) proposes colour-preserving automorphisms of the Tanner graph (qubits, Hx rows, Hz rows) and one map exchanging the Hx and Hz rows. The generators are tried as extra candidates in `find_half_symmetry` after the GH-75 family, under the same two GF(2) checks (new optional arguments, default = old behaviour). The swap map is offered to `verify_dual_perm` (new, the `find_dual_maps` check for one map) only when `find_dual_maps` finds no map. `-v` prints `c cc aut:` lines. With `-cc-aut=off` no line of any log changes (identity verified on tier0+1, both engines); since the default flip (2026-10-28) the default MaxSAT path is still byte-identical, and the default CC path equals `-cc-aut=on`. Test mutants 13/14 (candidates or the swap map used without the GF(2) check). The MaxSAT path is unchanged. Soundness below (GH-152). See `optimization/experiments/GH-152/`. |
 | Stabilizer-overlap dominance constraints in the MaxSAT split (GH-148; `-stab-overlap=off\|on\|auto`, default auto since the PI's adoption decision; `-stab-overlap=off` = previous search; silently off with -joint/-roundingsat unless given explicitly) | Split MaxSAT path only (an explicit `-stab-overlap=on\|auto` is refused with -joint/-roundingsat/-engine=cc). For every CSS half, the rows g of the same-type stabilizer matrix (X half: Hx; Z half: Hz) that pass a GF(2) check Hpar g = 0 and Glog g = 0 on the input matrices (duplicates removed) give the constraint "at most floor(\|g\|/2) of the qubits of g are 1" in each probe: by default (`-stab-overlap-enc=native`) as a native propagator inside MaxCDCL (`Solver::setOverlapRows`, set by `run_css_half` after `build_css_half`; see the `Solver.h` / `Solver.cc` section), or as clauses (`add_overlap_constraints` at the end of `build_css_half`): `clauses` = binomial clauses for \|g\| <= 9 and Sinz's sequential counter above, `bin` / `seq` = one of them for every row. `on`: every verified row in every probe; `auto`: row g only in probes of cap c >= 2 (floor(\|g\|/2) + 1) (`-stab-overlap-ratio=X` sets the factor). With `-stab-overlap=off` the instance and the `-v` log are those of the search before the adoption byte for byte (main e52d15b; identity verified on tier0+1 x 2 modes). Soundness below (GH-148). See `optimization/experiments/GH-148/`. |
+| Dense overlap rows dropped from cap 16 on (GH-218; `-stab-overlap-c4=N\|off` default 11, `-stab-overlap-pilot=N` default 0, `-stab-overlap-pilot-cap=P` default 12; `-stab-overlap-c4=off` = GH-148's search byte for byte) | Split MaxSAT path, with `-stab-overlap=on\|auto`. Rows on more than N Tanner 4-cycles of the stabilizer matrix (every weight-9 TN row; no BB/LP/GB row) are used as in GH-148 until a half's first probe with cap >= P' + 4 (P' = max(P, lb, activation cap); 16 on the TN codes) and dropped from there on; opt-in `-stab-overlap-pilot=N` > 0 decides per half by a pilot instead ("weight <= P'?" with and without them, N seeds, keep iff the median conflict ratio is <= 1). Sparse rows always as in GH-148. Removes the TN_216 regression of GH-148 (Z half). Soundness below (GH-218). See `optimization/experiments/GH-218/`. |
 | CC engine switch (GH-124 S0, experimental) | `-engine=maxsat` (default) leaves the search above unchanged (byte-identical `-v` logs); `-engine=cc` runs the connected-cluster level search of `src/cc/` on the same CSS split through the same pipe protocol and output; `-engine=auto` is a structural selector (not the default): CC unless a half's parity matrix has a row of weight > 32 or, for n >= 64, a mean row weight > n/4 (pre-S1 rule; every bundled code goes to CC). `-seed=N` (timing seeds): N > 0 sets `random_seed` of every MaxCDCL solver on the MaxSAT path from the application layer (the engine source is unchanged; N = 0 or no flag keeps main's search byte for byte) and equals `-cc-seed=N` with the CC engine. A CC no-answer stop sends `RESULT -1 TRAP` on the pipe, and the parent withdraws the bounds it had received (MaxSAT never sends it). `find_dual_maps` additionally keeps the verified qubit maps (its report output is unchanged). Flags: `-seed`, `-cc-rules`, `-cc-dual`, `-ub-basis`, `-ub-search` and `-cc-ub-*` (GH-140), `-cc-seed`, `-cc-trace`, `-cc-stats`, `-cc-mutant` and `-cc-schedule` (tests only). Conflicting combinations are rejected (exit 1): CC flags without `-engine=cc\|auto`; `-joint`, `-roundingsat`, the dumps and `-native-parity-opb` with `-engine=cc\|auto`; the cardinality flags and `-dualshare-stats` with `-engine=cc` (`-engine=auto` warns about the flags its choice ignores). See `optimization/experiments/GH-124/`. |
 
 ### `src/cc/` (GH-124, experimental; new code, not derived from MaxCDCL or any third-party code)
@@ -570,6 +571,29 @@ d = 3..5: RESULT = enumeration, every UB >= d, LBs monotone <= d; test mutants (
 and 2 (the half's parity rows used as g without the GF(2) check) must give wrong answers. `make test-cc-flags`:
 values, conflicts, `-v` lines, no output with the flag off. *Evidence.* `optimization/experiments/GH-148/REPORT.md`.
 
+GH-218 (`-stab-overlap-c4=N|off`, `-stab-overlap-pilot=N`, `-stab-overlap-pilot-cap=P`, split MaxSAT path,
+`src/core/distqldpc.cc`; defaults 11 / 0 / 12; `-stab-overlap-c4=off` = GH-148's search byte for byte). *What it
+changes.* Which of GH-148's verified rows a probe carries. A row g is *dense* if it lies on more than N Tanner 4-cycles
+of the same-type stabilizer matrix, c4(g) = sum over the other distinct rows g' of C(|g & g'|, 2). Sparse rows are used
+exactly as in GH-148. The dense rows of a half are used as in GH-148 until the half's first probe whose cap is at least
+P' + 4, where P' = max(P, the half's lb, the cap from which the -stab-overlap ratio activates every dense row), and are
+dropped from that probe on. With `-stab-overlap-pilot=N` > 0 (opt-in) a pilot runs instead, once per half, the probe
+"weight <= P'?" (stop at the first solution) with and without the dense rows for N solver seeds (the run's seed + 0, 1,
+...), and keeps the dense rows for the rest of the half iff the median of conflicts(with) / conflicts(without) is <= 1.
+*Why every probe
+answer stays the same.* GH-148's argument holds for any subset of the verified rows (see GH-148 above: each row alone
+keeps every minimum-weight element of F_h, so FOUND / NONE / OPT are unchanged and every returned solution is an
+element of F_h); the gate only chooses a subset per half and probe (from the 4-cycle counts, the probe's cap, the half's
+lb and, with the pilot, conflict counts), and any choice is sound. The pilot probes' own answers are not used: they only
+decide. The choice is a deterministic function of the matrices, the flags and the seed. *Tests.* `make test-cc` Part G: five
+more driver configurations with dense rows under the pilot (margin and pilot cap lowered by a test-only knob so that
+the pilot runs on the small Part B codes; also pilot off and one seed); Part G (c): the selection of sparse rows equals
+a brute-force 4-cycle count on every tier0 code and the tier2 / tier4 TN codes for 7 values of N, the dense flags
+partition the verified rows, forced with / without dense rows the probe answers agree at caps d - 1 and d on the tier0
+TN halves, and pilot decisions are reproducible; test mutant 3 (overlaps counted instead of qubit pairs) changes
+selections and is caught. `make test-cc-flags`: values, conflicts, `-v` lines; on TN_108_2_12 with `-ub-pre=off` (caps up to 16) a
+`c OVERLAP-DROP X cap 16` line by default and a pilot line with `-stab-overlap-pilot=3`; with `-ub-pre` no line. *Evidence.* `optimization/experiments/GH-218/` and the PR for issue #218.
+
 Fix round 1 (S0a): the S0 spec's literal mutants 3 ("orbit seeds without forbidding earlier orbits") and 4 ("stop
 rule without checking the other half's lower bound") are equivalent mutants as built: the first only drops a
 restriction, so every level verdict stays exact; the second skips a check that the lockstep pick order (lowest
@@ -647,6 +671,9 @@ not a change to MaxSAT costs or quantum-code distance semantics. See
   limit a conflict clause (p's literal and lim other true qubits of the row, all false) is returned; at the limit
   every unassigned qubit of the row is enqueued false with the reason clause OR ~x over the lim true qubits and
   the implied one (implied literal at position 0)
+- `ovHas` / `ovWatched(p)` (GH-218): the two call sites of `ovPropagate` first test inline that p sets a qubit
+  variable on at least one row true (the only case in which `ovPropagate` does anything), so the propagation is the
+  same and literals that cannot tighten a row no longer pay a call
 - `ovClause(r, mask, impliedPos)`: reason/conflict clauses (OR of ~x over a (lim+1)-subset of row r) are
   allocated on first use with `ca.alloc(lits, false)` and cached by (row, subset) in an open-addressing table;
   they belong to no clause list and are never watched; a cached clause is reordered when it becomes a reason

README.md

@@ -157,6 +157,7 @@ The distance definition, Pauli weight and output format are unchanged.
 | `-ub-pre=off\|on\|S` | **(GH-144; default `on` = 60 s since 2026-10-23; `-ub-pre=off` restores the previous search)** MaxSAT split only: before the bound search, run the randomized low-weight logical finder of GH-140 on both halves for at most S seconds (each half stops earlier after 16 re-hits of its bound or a plateau of max(1000, 4 x the iteration of its last improvement) iterations; tuning `-ub-pre-hits=H`, `-ub-pre-plateau=P`). The lightest verified word weight U0 is printed as the first `c d_ub`; the doubling probes stop below U0 - 1 and the rest of the search only proves that no logical of weight <= U - 1 exists (probes at U - 1). Every word is checked against the half instance before use; `-seed=N` also seeds the finder. Cost: <= 0.3 s on tiers 1-4, U0 = d on every bundled code with a known distance |
 | `-ub-isd=off\|stern\|dumer[:P,L,W,B,R]` | **(GH-146; default `stern` since 2026-10-23; `-ub-isd=off` restores the previous finder, the GH-140 enumeration)** Collision mode of the randomized finder used by `-ub-search` (CC) and `-ub-pre` (MaxSAT): a Stern step instead of the 1-2-row enumeration. The information set of each random systematic form is split at random into two halves; all subsets of size <= P of each half are bucketed by the sum of their columns on L random redundancy rows, and every colliding pair whose detector parities differ is weighed (words with up to 2P ones on the information set and none on the window). `dumer` also lets the window coordinates take part in the subsets. Between rounds, W Canteaut-Chabaud pivot swaps re-randomise the information set (0: a fresh elimination); B rounds form one finder iteration; R > 0 forces a fresh elimination every R rounds. Defaults P 2, L automatic (about log2 of the list size), W 32, B 1, R 0. Needs `-ub-search=on\|budget:S` or `-ub-pre=S`; every word is still verified before use |
 | `-stab-overlap=off\|on\|auto` | **(GH-148; default `auto` since the PI's adoption decision; `-stab-overlap=off` restores the previous search; silently off with `-joint` / `-roundingsat` unless given explicitly)** MaxSAT split only: every probe of a half also requires that at most floor(\|g\|/2) qubits of each same-type stabilizer row g are 1 (rows verified with H g = 0 and G g = 0; a minimum-weight logical always satisfies this, otherwise x + g would be lighter, so no probe answer changes). `on`: all rows in every probe; `auto`: row g only in probes with cap >= 2 (floor(\|g\|/2) + 1) (factor `-stab-overlap-ratio=X`); encoding `-stab-overlap-enc=native\|clauses\|bin\|seq` (default `native`: an "at most k" propagator inside MaxCDCL with lazily created reason clauses; `clauses`: binomial clauses up to \|g\| = 9, sequential counter above). `-frontier-stats` adds a `c OVERLAP` line per probe with the native propagator. `-v` prints the rows used per half and the active rows per probe |
+| `-stab-overlap-c4=N\|off`, `-stab-overlap-pilot=N`, `-stab-overlap-pilot-cap=P` | **(GH-218; defaults 11, 0, 12; `-stab-overlap-c4=off` restores GH-148's search)** With `-stab-overlap`: rows g on more than N Tanner 4-cycles of the stabilizer matrix (sum over the other rows g' of C(\|g & g'\|, 2); every weight-9 TN row, no BB/LP/GB row) are *dense*. They are used as in GH-148 until a half's first probe with cap >= P' + 4 (P' = max(P, lb, the cap from which the ratio activates every dense row); 16 on the TN codes) and dropped from there on. With `-stab-overlap-pilot=N` > 0 (opt-in) a pilot instead runs "weight <= P'?" with and without the dense rows for N seeds and keeps them iff the median conflict ratio is <= 1. Any row subset is sound, so no answer changes. `-v` / `-frontier-stats` print the decision (`c stab-overlap ... dropped`, `c OVERLAP-DROP`; with a pilot `c stab-overlap pilot`, `c OVERLAP-PILOT`) |
 | `-cc-rules=excl,pack,orbf,parity,leaf,overlap,charge[,tiebreak][,sparse,sparseov,sparsemrv,xorunit][,mrv]` | **(experimental)** CC pruning rules (default `excl,pack,orbf,parity,leaf,overlap,charge` since GH-157; `none` = plain CC; `excl,pack,orbf` = the GH-124 engine, `excl,pack,orbf,parity,leaf` = the GH-133 engine, `excl,pack,orbf,parity,leaf,overlap` = the engine before GH-157): sibling exclusion, disjoint odd-row packing bound, orbit seeds from the verified per-half automorphisms, even-weight parity shortcut (GH-133), leaf hash lookup (GH-133), stabilizer-overlap rule (GH-138: a minimum logical meets every same-type stabilizer row g in at most floor(\|g\|/2) qubits; the rest of a row that reaches this limit is forbidden), `charge` (GH-157: fractional LP-dual charge node lower bound on the qubits still needed; evaluated at remaining budget >= `-cc-lb-minr=K` (default 3) where the packing is exactly at its limit (`-cc-lb-gap=G`, default 0), switched off per half by `-cc-lb-auto=P` (default 40: after a level with >= 100 000 evaluations of which < P % pruned); `-cc-lb-raise=off` drops the charge's raise step), `tiebreak` (GH-162, opt-in, needs `overlap`: for an even row g the tie \|e & g\| = \|g\|/2 is cut unless the first qubit of g lies in e, in a per-seed order that puts the seed first, then the earlier orbits, then descending label; sound because the lexicographically least minimum logical in that order has no such tie and is reached by the seed rule; the first(g) tie-break idea is from Qubitserf 04b9349, S. Cercelescu, MIT), fewest-candidate branching. GH-181, opt-in: `sparse` adds redundant parity rows (sums of two parity rows that are no heavier than the heavier of the two; every logical satisfies them) to the packing bound, scanned lightest first; `sparseov` adds such sums of two stabilizer rows to the overlap rule; `sparsemrv` uses fewest-candidate branching over the parity and redundant rows on halves where `sparse` added rows (together with `mrv` it adds nothing: `mrv` already branches that way on every half); `xorunit` forbids the last free qubit of an even row and branches first on an odd row with one free qubit (not recommended: few nodes saved, slower). Rows are added only on TN_200, TN_250, TN_496 and a few tier-0 codes; the tokens combine with `charge`, `tiebreak` and every `-cc-roworder`; the idea of redundant pair-XOR checks is from Qubitserf 04b9349 (S. Cercelescu, MIT) |
 | `-cc-dual=on\|off` | **(experimental)** With a verified XZ-dual map, CC searches only the X half (default `on`; `-dualmode=off` also disables it) |
 | `-cc-aut=on\|off` | **(experimental, GH-152; default `on` since 2026-10-28, PI; `-cc-aut=off` restores the previous CC search)** CC engine only. Tanner-graph automorphism candidates: individualisation-refinement on the coloured Tanner graph (qubits, Hx rows, Hz rows) proposes extra qubit permutations for the orbit seeds and one map exchanging Hx and Hz for the single-half search. Every candidate must pass the same GF(2) checks as the built-in family before it is used. Gives orbit seeds on TN codes the built-in family misses (e.g. TN_288/324/432/540/576, TN_200, TN_250) and a dual map on the LP codes and TN_496; on every other bundled code the CC search is unchanged (identical node counts). Detection takes at most 11 ms. The MaxSAT path never uses it |