Repository navigation
[Mac agent] MaxSAT path: stabilizer-overlap dominance constraints in every CSS-half probe #148
Description
Round (2026-10-23), baseline main 12b3e05
Defaults of the baseline: MaxSAT path with -frontier=auto, -oddcap-skip=on, -ub-pre=on; optional CC engine (-engine=cc, src/cc/) with -ub-search=on. GH-146 (Stern finder) is not merged and is not used.
Where the gap is. On Tier 5 the open codes now have verified upper bounds (BB_1080 <= 48, TN_576 <= 37, TN_612 <= 40) but certified lower bounds of only BB 30 / TN 9-24 (CC), and the default MaxSAT path stops at lb 17/18 (BB, LP, TN ge17) or lb 9 (TN ge9: its cap-16 refutation does not finish in 6 h). Since GH-144, every Tier 1-4 run of the MaxSAT path is dominated by its final refutation at U0 - 1 (the pre-pass gives U0 = d on every Tier 1-4 code). The PI wants solver-level differentiation from MaxCDCL on the default MaxSAT path. So the lever is: make each refutation probe cheaper with knowledge that a generic MaxSAT engine cannot have.
Records read: GH-121 (PIB, parity-row iset bound in the lookahead: mixed, TN regressions, not adopted), GH-124, GH-127 (unit lb ladder: Tier 1/2/4 FAIL), GH-128 (p1skip: no effect on tiers 1-4), GH-129 (frontier on everywhere: TN FAIL), GH-130, GH-133, GH-138 (CC overlap rule: BB nodes 0.20-0.47x, LP Z halves 0.49-0.73x, TN 0.67-0.96x), GH-140, GH-144, docs/LITERATURE_CC_2026.md.
Three proposals
A (selected). Stabilizer-overlap dominance constraints in every MaxSAT half probe (-stab-overlap).
- Hypothesis: the CC engine's strongest new exact rule ([Mac agent] CC engine: stabilizer-overlap pruning (Lee 2026) with forbidden-qubit propagation #138, Lee 2026 rule iv) can be stated as cardinality constraints of the half instance. For the X half (F = {x : Hz x = 0, Gx x != 0}) and every row g of the same-type stabilizer matrix (Hx) with Hz g = 0 and Gx g = 0 (verified over GF(2) at start-up; otherwise the rule is off for that half), x in F implies x + g in F and |x + g| = |x| + |g| - 2|x & g|, so every minimum-weight element of F satisfies |x & g| <= floor(|g|/2). Adding these constraints to each probe removes only non-minimum solutions; every probe answer (FOUND iff cap >= d_h, NONE iff cap < d_h, OPT = d_h) is unchanged, and the [Agent experiment] mac-split-symbreak-20261009: symmetry breaking inside interleaved CSS halves (GH-73 x GH-75 interaction) #85 orbit clauses compose (they keep some minimum-weight element, and every minimum-weight element satisfies the overlap constraints).
- Change: in
build_css_half, behind-stab-overlap=on|off(default off), one at-most-floor(|g|/2) constraint per stabilizer row (binomial clauses for short rows, a sequential counter for long rows); unit propagation then forbids the rest of a row once it is tight (the [Mac agent] CC engine: stabilizer-overlap pruning (Lee 2026) with forbidden-qubit propagation #138 forbidding, for free). MaxCDCL's lookahead sees fewer ways to repair odd rows, so its disjoint-core lower bounds rise and refutations shorten. Default off: the default path stays byte-identical to main. - Expected effect: refutation speed-ups where CC's overlap rule cut nodes most (BB, LP Z halves; TN smaller), so Tier 1-4 geomeans < 1; on Tier 5, faster cap-16 refutations (TN ge9 cells may reach lb 17), possibly TN_252 / BB_360 / LP refutations finishing within 6 h. Risk: extra clauses cost propagation time in the lookahead (the [Mac agent] PIB: parity-row iset bound in the MaxCDCL lookahead (structural lower bound from the code's checks) #121 lesson: per-conflict cost matters on TN).
- Correctness risk: medium-low. The argument needs only H g = 0 and G g = 0 (checked) and the non-strict inequality (the even tie |x & g| = |g|/2 must not be cut). Tests: MaxSAT driver vs exhaustive enumeration on random CSS codes and rotated surface codes (weight-2 boundary stabilizers make the rule bind hard); mutants (limit off by one; parity rows used instead of stabilizer rows) must give wrong answers.
B. MaxSAT Phase 2 step policy after Phase 1. After Phase 1, when U - lb is large, probe intermediate caps (lb ladder, step 2 on all-odd halves) instead of going straight to U - 1, to raise the anytime lower bound on Tier 5. Weaker: with the pre-pass, U0 = d on every Tier 1-4 code, so a ladder can only add refutations there (GH-127's unit ladder already failed Tier 1/2/4 for this reason, and its descent savings are now gone); it cannot meet "geomean < 1" on Tiers 1-4 and changes no refutation.
C. Stronger CC lower bound (fractional / LP packing, greedy-improved packing). Weaker for this round: it touches only the optional CC engine, not the default MaxSAT path the PI wants differentiated; GH-133 showed the existing packing already closes almost every cluster at budget 2-4, so a per-node LP (10-100x a node) must cut nodes by more than that to pay.
Why not candidate (a) as a packing propagator: a disjoint odd-check packing inside MaxCDCL duplicates what its lookahead already computes (disjoint inconsistent soft subsets via unit propagation: an odd parity row with its unassigned qubits is exactly such a subset), and GH-121 (PIB) implemented it with mixed results (TN regressions). The overlap rule is the part of (a) that adds information MaxCDCL cannot derive, so A keeps (a)'s idea and drops its redundant half.
Plan and gates (docs/OPTIMIZATION_LOOP_POLICY.md)
- Branch
experiment/gh-148-stab-overlapfrom 12b3e05. Flag default off; default path byte-identical to main (-vlogs, tier0+1 x 2 modes). - Tier 0: unit tests (driver vs enumeration, mutants), flag checks, tier0 answers.
- Tier 1-4: yfclab2, 5 seeds (main = frozen 12b3e05 with
-seed), both modes, arms concurrent on pinned cores 90-123 only (4 GB cap); pass = per tier and mode geomean of seed-median ratios < 1 and no cell > 1.25. Stop at the first failed gate. - Tier 5 (preregistered): 27 codes x 2 modes = 54 candidate cells, default seed, 6 h, in two waves on cores 90-123 (wave 1: 34 cells, wave 2: 20 cells plus main drift controls on the spare cores); comparison with main's recorded Tier 5 for this MaxSAT path ([Mac agent] Seed the MaxSAT path with the verified upper-bound finder (pre-pass) #144 S1, binary 6d2b7a1
-ub-pre=60, identical MaxSAT path to 12b3e05 by log identity, to be re-checked) and with the drift controls. - No timing on the Mac. No PR, no merge.
Hub: #15
Activity
GH-148: native overlap propagator in MaxCDCL (default encoding), S0 data
guluchen commentedon Oct 23, 2026
S0 done, S1 preregistration (before any gated run). Branch
experiment/gh-148-stab-overlap, evaluated commit2b297b5(frozen on yfclab2 asfrozen/server-gh148-2b297b5, sha256933ae40b...).S0 (informational, yfclab2 cores 90-123, 3 seeds, no-card;
optimization/experiments/GH-148/S0/):on, all rows): conflicts fall where caps are large relative to the row weight (BB_288 0.22x, LP_544 0.64x, TN_250 0.72x, BB_144_14_14 0.92x) but the extra clauses slow the small-cap Tier 1 runs (LP_340 1.27-1.45x wall with unchanged conflicts, LP_442 1.2x).-stab-overlap-enc=native, now the default encoding): same conflicts, lower overhead (tier 1-4 wall geomean 0.815 vs 0.843 for clauses; TN_250 0.81, clauses 0.75).Evaluated arm:
-stab-overlap=auto(native propagator; a row g is active in a probe of cap c iff c >= 2 (floor(|g|/2) + 1), the cost model fixed in S0 before the TN_250 data). Consequence: on Tier 1 (LP_340, LP_442: caps <= 8 < 10) no row is ever active, so the search is identical to main.Gate rules (unchanged policy plus two preregistered points):
-frontier-stats) for every seed has gate ratio 1.000 (the measured ratio is reported too). A tier made only of identity cells is reported as neutral (identical search) and does not stop the sequence; this is flagged for the PI.6d2b7a1 -ub-pre=60, log-identical to 12b3e05 on tier0+1 x 2 modes: 30/30) plus the drift controls.🤖 Generated with Claude Code
GH-148: Tier 0-4 data (tests, identity, tier0 answers, 5-seed panels)
guluchen commentedon Oct 23, 2026
Tier 0-4 results (
-stab-overlap=auto, binary2b297b5, yfclab2 cores 90-123, main = frozen 12b3e05; seed medians over seeds 0-4):make test-cc(300/200 and 1500/600),make test-cc-flags329 checks, tier0 78/78 answers (auto, on, on+clauses), default and-stab-overlap=offlogs = main (30/30 modulo main's own timing-dependent ub-pre convergence print order)Tier 5 wave 1 (34 cells, 6 h) started 10:19 CST.
🤖 Generated with Claude Code
guluchen commentedon Oct 23, 2026
Round paused by the PI (token budget) during Tier 5 wave 1; all runs on yfclab2 cores 90-123 were stopped. Tiers 0-4 passed (see the previous comment); Tier 5 was not evaluated. Status note:
optimization/experiments/GH-148/STATUS.mdon branchexperiment/gh-148-stab-overlap. No PR.🤖 Generated with Claude Code
GH-148: status note (paused by PI before the Tier 5 evaluation)
GH-148: Tier 5 (54 cells x 6 h) and final report
guluchen commentedon Oct 28, 2026
Tier 5 result (
-stab-overlap=auto, binary2b297b5; 27 tier5 codes x {no-card, card-mto} = 54 cells, 6 h, default seed, all at once on yfclab2 cores 0-53, 4 GB cap; compared with main 12b3e05's recorded Tier 5 frombaselines/main-12b3e05, same cores and protocol). The earlier stopped attempt is not counted.{lb}to{ub}stems, and against main's bounds; 0 runner errors or kills.Gate verdicts: Tier 0 PASS, Tier 1 PASS (neutral, identical search), Tier 2 PASS (0.698 / 0.697), Tier 3 PASS (0.949 / 0.994, watch TN_144), Tier 4 PASS (0.781 / 0.859), Tier 5 PASS (watch TN_216).
Recommendation: adoption-eligible. Two PI decisions are needed:
-stab-overlap=off;autois the candidate default for the split MaxSAT path. Is a 5-seed TN check (TN_216 / TN_144) wanted first?After a merge, the baselines need re-recording. No PR is open and nothing is merged.
Report:
optimization/experiments/GH-148/REPORT.mdonexperiment/gh-148-stab-overlap(commit 239c230). It includes the 12b3e05 -> e52d15b map of the 17 renamed stems.🤖 Generated with Claude Code
GH-148: merge origin/main (e52d15b + HGP matrix library) into the branch
GH-148: make -stab-overlap=auto the MaxSAT default (draft adoption, P…
GH-148: 5-seed TN check (TN_216 regression confirmed), Tier 0 after t…
guluchen commentedon Oct 28, 2026
Adoption check (PI decision 2026-10-28): 5-seed confirmation of the watch cells. Draft adoption PR: #158 (needs a PI decision, not merged).
yfclab2, cores 0-39, one process per pinned core, 4 GB cap, both arms of a cell run concurrently. Main is
frozen/server-main-12b3e05; the candidate isfrozen/server-gh148-2b297b5with-stab-overlap=auto. Seeds 0-4. Limits: TN_216 21600 s, TN_144 1800 s.All 40 runs solved with the right answers, with no science issue.
The branch now also merges current main (e52d15b solver source). Tier 0 passes on the merge commit and on the default-flip commit.
The REPORT has a TN_216 diagnosis from the existing logs:
It also proposes two gating hypotheses (H1: a row-weight / cache budget; H2: a 4-cycle-density gate). Evidence is in
optimization/experiments/GH-148/ADOPT/.Merge pull request #158 from guluchen/experiment/gh-148-stab-overlap
Merge main (GH-148 stab-overlap) into GH-152 adoption branch
Merge main (GH-148, GH-152 -cc-aut default) into GH-157