CC engine: charge node lower bound as a default CC rule (GH-157)

MODIFICATIONS.md

@@ -42,7 +42,7 @@ Optional engine, off by default (PI 2026-10-16): enable with `-engine=cc` (or `-
 
 | File | Description |
 |------|-------------|
-| `cc_half.h`, `cc_half.cc` | Exact connected-cluster (CC) level search for one CSS half (Dumer, Kovalev, Pryadko 2017): clusters grown from a seed along one odd parity row at a time; syndrome-free clusters below the level are dead ends (a nontrivial one is reported as an inconsistency); rules `excl` (sibling exclusion), `pack` (disjoint odd-row packing bound), `orbf` (orbit seeds from the GH-85 verified per-half orbits, replacing the index rule), `mrv` (fewest-candidate branching), `parity` (GH-133: odd levels skipped on a half whose column weights are all odd; per-node parity check), `leaf` (GH-133: Zobrist hash from column to qubit; the closing qubit is looked up at budget 1, and at budget 2 each candidate is completed by one lookup), `overlap` (GH-138: a minimum logical meets every same-type stabilizer row g in at most floor(\|g\|/2) qubits; incremental counters, the rest of a tight row is forbidden); uint64 bitsets with an incremental syndrome; `-cc-seed` relabeling; test-only mutants 1-3 (1 forbidden set not restored, 2 packing prune `>=`, 3 orbit seed rule off by one) and 5-7 (5 parity forced on a half with an even column weight, 6 leaf budget off by one, 7 leaf closure without the detector check) and 8-10 (GH-138: 8 overlap limit off by one, 9 parity checks used as stabilizer rows, 10 even-weight tie cut). |
+| `cc_half.h`, `cc_half.cc` | Exact connected-cluster (CC) level search for one CSS half (Dumer, Kovalev, Pryadko 2017): clusters grown from a seed along one odd parity row at a time; syndrome-free clusters below the level are dead ends (a nontrivial one is reported as an inconsistency); rules `excl` (sibling exclusion), `pack` (disjoint odd-row packing bound), `orbf` (orbit seeds from the GH-85 verified per-half orbits, replacing the index rule), `mrv` (fewest-candidate branching), `parity` (GH-133: odd levels skipped on a half whose column weights are all odd; per-node parity check), `leaf` (GH-133: Zobrist hash from column to qubit; the closing qubit is looked up at budget 1, and at budget 2 each candidate is completed by one lookup), `overlap` (GH-138: a minimum logical meets every same-type stabilizer row g in at most floor(\|g\|/2) qubits; incremental counters, the rest of a tight row is forbidden); uint64 bitsets with an incremental syndrome; `-cc-seed` relabeling; test-only mutants 1-3 (1 forbidden set not restored, 2 packing prune `>=`, 3 orbit seed rule off by one) and 5-7 (5 parity forced on a half with an even column weight, 6 leaf budget off by one, 7 leaf closure without the detector check) and 8-10 (GH-138: 8 overlap limit off by one, 9 parity checks used as stabilizer rows, 10 even-weight tie cut); GH-157 (default rule since 2026-10-29): `charge` (raised local-degree LP-dual charge node lower bound, exact integers), evaluation gates `-cc-lb-minr`, `-cc-lb-gap`, `-cc-lb-auto`, `-cc-lb-raise`, mutant 15 (charge inflated). |
 | `cc_ubsearch.h`, `cc_ubsearch.cc` (GH-140, GH-146) | Randomized low-weight logical finder for one CSS half (`-ub-search`): random information sets (random column order, Gauss-Jordan elimination of H with pivots in that order, systematic kernel basis), words of 1-2 (optionally 3) systematic basis vectors below a weight threshold, detector check (G c != 0), greedy local improvement by same-type stabilizer rows; deterministic per seed; test mutant 11 (no detector check and no improvement). GH-146 collision mode (`-ub-isd`): Stern / Dumer collision step with Canteaut-Chabaud pivot swaps (`cc_swap`, `isd_round`, `iterate_isd`), parser `parse_isd`. |
 | `cc_aut.h`, `cc_aut.cc` (GH-152) | Candidate automorphisms for `-cc-aut=on`: colour refinement to the coarsest equitable partition of the coloured Tanner graph (qubits, rows of each class), individualisation of one vertex and lockstep refinement of a source and a target partition (McKay 1981, written from the published description), backtracking over the first non-singleton cell, edge-checked vertex maps; orbit computation by union-find from the first vertex of the smallest qubit cell (complete when that vertex's point stabiliser is trivial), one class-exchanging (swap) map; deterministic work counters. Candidates only: every map is GF(2)-verified by the wrapper before use. |
 | `cc_driver.h`, `cc_driver.cc` | Driver: start-up detector check (rank[H;G] + rank S = n and commutation), both halves interleaved level by level (cheaper half first) or one half under a verified XZ-dual map, stop rule (a hit at level w ends the run once the other half's lower bound is >= w), anytime `TRY`/`LB`/`UB`/`RESULT` lines, witness verification (H e = 0, independent GF(2) rank test against the same-type stabilizers, dual image check), its own check of the XZ-dual map (pi(rs Hz) = rs Hx and pi(rs Hx) = rs Hz), always-on traps (`RESULT -1 TRAP`, never a value; earlier bounds withdrawn), optional `-ub-basis`, `-cc-trace`, `-cc-stats`; test-only sequential schedule (`-cc-schedule=sequential`) and driver mutant 4 (stop rule without the other half's lower bound, run under the sequential schedule). |
@@ -155,6 +155,66 @@ the node reduction against `-cc-rules=excl,pack,orbf,parity,leaf` (exact, determ
 pair sums g1 + g2 whose limit is not implied by the rows (e.g. TN rows of weight 9 sharing 2-3 qubits) cut a
 further 0-17 % of the nodes on TN_250 / TN_144 / BB_288 but cost more time than they saved (S0 of GH-138).
 
+GH-157 (`charge`; in the default `-cc-rules` since the PI's decision of 2026-10-29, on top of the GH-152 `-cc-aut=on`
+default; `-cc-rules=excl,pack,orbf,parity,leaf,overlap` restores the previous CC search; tuning `-cc-lb-minr=K` (3),
+`-cc-lb-gap=G` (0), `-cc-lb-raise=on|off` (on), `-cc-lb-auto=P` (40)). Sources, used from the published mathematics
+only: the detector-charge bound of Banfi, Ferrari, Favano, Tarable and Barletta, arXiv:2610.28008 (2026); the scaled
+feasible set-cover dual of Okada and Kasai's `cpm-ldpc-distance` (github.com/kasaikenta/cpm-ldpc-distance,
+verification/README). No third-party code was read or copied. (The round also evaluated a Gallai edge-cover bound,
+`ecover`; it never improved time and was removed at the PI's request; see the GH-157 report.)
+
+*Setting.* A node of the level-w search is a cluster S with odd-row set U (rows of H with odd overlap with S) and
+available set A (qubits neither in S nor forbidden by excl, orbf, overlap). Let r = w - |S|. For u in U write
+N_A(u) = N(u) & A, and tau(U, A) = the minimum size of a set T within A with T & N_A(u) nonempty for every u in U
+(tau = infinity if some N_A(u) is empty).
+
+*Lemma 1 (hitting set).* If e in F, |e| = w, S within e and e avoids every forbidden qubit, then |e \ S| >= tau(U, A).
+Proof: e \ S lies in A (it avoids S and the forbidden set). H(e \ S) = H e + H S = syn(S), so every u in U has odd,
+hence nonzero, overlap with e \ S, i.e. e \ S meets N_A(u). This is the same fact the `pack` rule uses (each selected
+disjoint row needs its own qubit of e \ S).
+
+*Lemma 2 (weak duality, `charge`).* For every y >= 0 on U with sum_{u in U, j in N(u)} y_u <= 1 for each j in A,
+sum_u y_u <= tau(U, A). Proof: for a hitting set T, sum_u y_u <= sum_u y_u |T & N_A(u)| = sum_{j in T}
+sum_{u : j in N_A(u)} y_u <= |T|. (This is the LP dual of the hitting-set relaxation; Banfi et al.'s detector charges
+with unit column costs and Okada-Kasai's scaled set-cover dual are such vectors.)
+- Local-degree charge: c_j = |{u in U : j in N(u)}| for j in A, y_u = 1 / max_{j in N_A(u)} c_j. Feasible: a qubit j
+  lies in c_j rows, each with y_u <= 1/c_j (the max over the row includes c_j), so its load is <= 1.
+- Raise: rows in index order, y_u += min_{j in N_A(u)} (1 - load_j) when positive, loads updated. Every load stays <= 1,
+  so y stays feasible and sum y only grows.
+- Prune iff sum_u y_u > r. Then tau > r, so by Lemma 1 no weight-w element of F extends S while avoiding the forbidden
+  qubits. Integer arithmetic: every value is a multiple of 1/L, L = lcm(1..D) with D = max c_j at the node; the code
+  stores L y_u and compares L sum y > L r exactly. The rule is idle if D > 32 (L > 1.4e14) or there are >= 2^15 odd
+  rows (no overflow of int64 sums). The search copies the odd rows' candidate sets once (counting c_j on the way) and
+  calls `lb_charge_counted`, the second half of the tested `lb_charge`; the local charge stops as soon as its sum
+  exceeds r, and the raise runs only when the local charge does not already prune.
+
+*Evaluation gates.* The charge is evaluated only (i) after the pack scan found no prune, (ii) when r >= lb-minr
+(default 3; at r <= 2 the leaf lookups are cheaper), (iii) when |U| > r (tau <= |U| always, so nothing is lost), (iv)
+when r - p <= lb-gap (default 0; p = the node's greedy packing, with pack on; on the S0 codes 76-99 % of all prunes
+occur at r = p, see `optimization/experiments/GH-157/dev/gap_histogram.txt`), and (v) while the half is not switched
+off by -cc-lb-auto (default 40 %: after an EMPTY level with at least 100 000 evaluations of which fewer than 40 %
+pruned, the charge stays off for the rest of that half; the decision depends only on deterministic counters). Each gate
+only skips a sound prune.
+
+*Theorem (exactness with the other rules).* A prune means: no weight-w element of F contains S and avoids the
+forbidden set. Every other rule's argument (excl, orbf, parity, leaf, overlap; see GH-124/133/138) fixes one
+weight-w element e* with S within e* and e* disjoint from the forbidden set, and needs that such a node is not
+pruned: Lemmas 1-2 guarantee exactly that. The rule adds no forbidden qubits and change no branching order, so the
+sibling-exclusion and orbit arguments (including the GH-152 orbits and dual maps, which are verified automorphisms) are unchanged; it only removes nodes, so node counts can only fall. The parity
+rule's L+1 strengthening adds nothing (on a qualifying half r = |U| mod 2 already). An odd row without an available
+qubit is a dead end, as for `pack`.
+
+*Tests (`make test-cc`, Part I).* (a) 20 000 random hitting-set instances (<= 10 sets over <= 14 qubits, a third with
+every qubit in <= 2 sets) against brute-force tau: charge (with and without the raise) <= tau, local charge <= raised
+charge, and the early-exit contract for every r. (b) On every Part A half, the 128 base rule subsets plus charge in
+three gate configurations (lb-minr 1, 2, 3 with lb-gap unlimited, 0, 1) x seeds 0..2 (seed 1 with the auto switch-off
+after any level at 60 %, seed 2 without the raise): ladders against enumeration. (c) Part B driver configurations with
+charge (the default set, minr 1 and 3, gap 0 / 1 / unlimited, with and without pack, and the pre-GH-157 rule set);
+Part H runs the default (charge + `-cc-aut`) on relabelled codes with hidden symmetry.
+*Mutant.* 15: charge inflated by 1/D (an extra L/D per row; infeasible) - exceeds tau on random instances and makes
+half ladders wrong. Statistics (`-cc-stats`, printed only with charge on): `lbeval`, `chgprune`, `lbdead`, the prunes by
+remaining budget. *Evidence.* `optimization/experiments/GH-157/REPORT.md`.
+
 GH-140 (`-ub-search=off|on|budget:S`; on by default inside CC since 2026-10-23, PI decision). *What it adds.* Per searched half (with a verified
 dual map: the X half only, its words mapped to the Z half and verified there too) a `UbFinder` (cc_ubsearch.h). The
 driver time-slices it with the level ladder in the same thread: at the top of every ladder iteration and, through

NOTICE

@@ -91,6 +91,13 @@ Modified files (partial list): Solver.h, Solver.cc
   the GH-87/GH-107 verified XZ-dual maps, the stop rule, independent
   witness verification and the verified basis-row upper bound (see
   README, "Connected-cluster (CC) engine").
+  The CC node lower bound `charge` (GH-157, a default CC rule since the
+  PI's decision of 2026-10-29) was implemented from published mathematics
+  only: the detector-charge bound of F. Banfi, G. Ferrari, A. Favano,
+  A. Tarable, R. Barletta, arXiv:2610.28008 (2026), and the scaled
+  feasible set-cover dual of K. Okada and K. Kasai, cpm-ldpc-distance
+  (https://github.com/kasaikenta/cpm-ldpc-distance). No third-party code
+  was read or copied.
 
   src/cc/cc_aut.h, src/cc/cc_aut.cc (GH-152, -cc-aut=on, the CC default
   since 2026-10-28) find candidate automorphisms of the coloured Tanner

README.md

@@ -157,7 +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 |
-| `-cc-rules=excl,pack,orbf,parity,leaf,overlap[,mrv]` | **(experimental)** CC pruning rules (default `excl,pack,orbf,parity,leaf,overlap`; `none` = plain CC; `excl,pack,orbf` = the GH-124 engine, `excl,pack,orbf,parity,leaf` = the GH-133 engine): 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), fewest-candidate branching |
+| `-cc-rules=excl,pack,orbf,parity,leaf,overlap,charge[,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), fewest-candidate branching |
 | `-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 |
 | `-ub-basis[=on\|off]` | **(experimental, CC only)** Emit the minimum weight of the verified logical basis rows as an initial upper bound (default on; `-ub-basis=off` disables it) |
@@ -182,7 +182,7 @@ to the behaviour before GH-124.
 | Use the CC engine | `-engine=cc` | no flag, or `-engine=maxsat` (default) |
 | Let DistQLDPC choose per code | `-engine=auto` (CC unless the code is dense, see below; `-v` prints `c engine: auto -> cc\|maxsat (...)`) | `-engine=maxsat` |
 | Seed for timing panels (both engines) | `-seed=N` (N > 0; CC: same as `-cc-seed=N`) | no flag or `-seed=0` (main's search) |
-| Pruning rules (CC only) | `-cc-rules=excl,pack,orbf,parity,leaf,overlap` (default), add `mrv` for fewest-candidate branching | `-cc-rules=none` (plain CC), or list only the rules you want, e.g. `-cc-rules=excl,pack,orbf,parity,leaf` (the GH-133 engine, no `overlap`) |
+| Pruning rules (CC only) | `-cc-rules=excl,pack,orbf,parity,leaf,overlap,charge` (default), add `mrv` for fewest-candidate branching | `-cc-rules=none` (plain CC), or list only the rules you want, e.g. `-cc-rules=excl,pack,orbf,parity,leaf` (the GH-133 engine, no `overlap`) |
 | Orbit seeds (CC only) | default (rule `orbf`) | drop `orbf` from `-cc-rules`, or `-no-symbreak` (index seeds) |
 | Single-half search under a verified XZ-dual map (CC only) | `-cc-dual=on` (default) | `-cc-dual=off` or `-dualmode=off` |
 | Tanner-graph automorphism candidates for the orbit seeds and the dual map (CC only, GH-152) | `-cc-aut=on` (default since 2026-10-28) | `-cc-aut=off` (the CC search before GH-152) |
@@ -194,7 +194,7 @@ to the behaviour before GH-124.
 Examples:
 
 ```bash
-./bin/distqldpc -engine=cc BB_288_12_18                  # CC with all rules (excl, pack, orbf, parity, leaf, overlap), dual map, basis UB
+./bin/distqldpc -engine=cc BB_288_12_18                  # CC with all rules (excl, pack, orbf, parity, leaf, overlap, charge), dual map, basis UB
 ./bin/distqldpc -engine=cc -cc-rules=none BB_288_12_18   # plain connected-cluster search, no extra pruning
 ./bin/distqldpc -engine=cc -ub-basis=off BB_288_12_18    # no initial upper bound from the basis rows
 ./bin/distqldpc -engine=cc -cc-aut=off TN_200_10_10      # CC without the Tanner-graph automorphism candidates (GH-152)