Repository navigation
GH-148: stabilizer-overlap propagator as the MaxSAT default (-stab-overlap=auto) - #158
Merged
Merged
Conversation
…(-stab-overlap=off|on|auto, default off) Each probe of a CSS half may add, for every same-type stabilizer row g with Hpar g = 0 and Glog g = 0 (GF(2)-checked), the constraint |x & g| <= floor(|g|/2): every minimum-weight logical satisfies it (else x + g is lighter), so no probe answer changes. Binomial clauses up to |g| = 9, sequential counter above. auto: row g only in probes with cap >= 2 (floor(|g|/2) + 1). Default off: the default path is main's byte for byte. Tests: make test-cc Part G (driver vs enumeration, encoding check, mutants 1/2), make test-cc-flags section 7e. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Solver::setOverlapRows / ovPropagate: 'at most k of these qubits true' checked when a qubit becomes true in propagate() and propagateForLK(); reason and conflict clauses are allocated on first use, cached, relocated in relocAll and never reduced on the fly. Inactive (byte-identical) without rows. -stab-overlap-enc=native (default) | clauses | bin | seq. Tests: Part G with native configurations and mutants, encoding check for all three encodings, flag checks. S0 exploration results under optimization/experiments/GH-148/S0. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Tier 5 of -stab-overlap=auto (binary 2b297b5) on yfclab2 cores 0-53, all 54 cells at once, compared with main 12b3e05's recorded Tier 5 (baselines/main-12b3e05): solved 10 vs 6 (new: BB_360_12_24 d=24, LP_1122_148_20 d=20, both modes), no cell lost, final lb higher on 5 cells and never lower, ub identical on all 54, no semantic issue (checked against 12b3e05 and e52d15b stems). Watch: TN_216 solve time 1.57x / 1.15x (single seed). REPORT.md covers Tiers 0-5 with gate verdicts and the recommendation; runner allows cores 0-53 for this run; analyzer analyze_t5final.py; 12b3e05 -> e52d15b stem map; the stopped earlier attempt is kept under raw/ and not counted. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Brings in GH-146 (-ub-isd=stern default for both finders), the 17 tier5 stem renames to {lb}to{ub}, and the later main commits (HGP matrix library and its CI, README author lines; no solver source change after e52d15b). Conflicts resolved by keeping both features: README / MODIFICATIONS flag rows and soundness paragraphs (GH-146 first, then GH-148), the help text, the unit-test header and PreCfg (GH-148 positional fields before GH-146's defaulted isd fields, so both initializer styles still work), and test_cc_flags.sh (GH-148 checks renumbered 7f). -stab-overlap stays default off here. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…I decides) -stab-overlap=auto (stabilizer-overlap "at most floor(|g|/2)" rows as a native MaxCDCL propagator on the split MaxSAT path) passed Tiers 0-5 against main 12b3e05 (tier2 0.70/0.70, tier4 0.78/0.86, Tier 5 10 vs 6 solved cells, 5 higher lbs, nothing lost), but the 5-seed check confirms the TN_216 regression (seed-median 1.53x no-card, 1.39x card-mto; TN_144 1.09x/1.08x). This commit makes it the default for the PI to weigh that trade-off; -stab-overlap=off restores the previous search byte for byte. Like the default -ub-pre, a default (not explicitly requested) auto is silently off with -joint / -roundingsat; an explicit on/auto there is still an error. The tuning flags -stab-overlap-enc / -stab-overlap-ratio now apply to the default. Updated: README / MODIFICATIONS flag rows and the GH-148 paragraph, NOTICE, the help text, test_cc_flags.sh (default prints the auto lines and the c OVERLAP line, tuning flags accepted without an explicit mode, rejected after -stab-overlap=off, -joint silently off) and the Part D comment of test_cc_engine.cc (it now runs the new default). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…he main merge, diagnosis 5-seed confirmation on yfclab2 cores 0-39 (main 12b3e05 vs -stab-overlap=auto 2b297b5, both arms concurrent): TN_216_4_18 seed-median 1.529x (no-card, seeds 1.15-1.63) and 1.392x (card-mto, 1.05-1.69), above the 1.25 cell rule; TN_144_2_13 1.093x / 1.084x. 40/40 solved, no science issue. Tier 0 on cores 100-107 for the main merge and the adoption commit: build, test-cc, test-cc-flags, smoke pass; tier0 answers 78/78 = stems with auto/on/off; -v logs vs frozen main e52d15b (flag off) and default vs merge auto 30/30 equal modulo main's own timing-dependent ub-pre X/Z print order. REPORT.md: adoption-check section with the table, Tier 0 summary and a TN_216 diagnosis from the existing logs (loss in the Z-half refutations at caps 16-17, ~0.5% overlap-row conflicts, ~17% per-conflict overhead, reason cache saturated at 108 x C(9,5)) with two gating hypotheses. Evidence under ADOPT/. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Draft: this needs a PI decision. Do not merge without one. The 5-seed check confirmed the TN_216 regression, and it fails the 1.25 cell rule. The PI's original instruction was to stop before a PR in that case. This draft exists so the PI can weigh the trade-off below.
Closes nothing yet. Issue #148. Report:
optimization/experiments/GH-148/REPORT.md(see the "Adoption check" section at the end).What this PR does
123011df, which has the same solver source as e52d15b plus the HGP library and its CI) intoexperiment/gh-148-stab-overlap. It keeps both features: [Mac agent] Stern/Dumer collision step in the verified upper-bound finder (large open codes) #146's-ub-isd=sterndefault and [Mac agent] MaxSAT path: stabilizer-overlap dominance constraints in every CSS-half probe #148's flag. Conflicts were resolved in the README / MODIFICATIONS flag rows and soundness paragraphs, the help text, and the tests. The 17 tier5{lb}to{ub}stem renames came through cleanly.-stab-overlap=autothe MaxSAT default (0574792). This is the stabilizer-overlap "at most floor(|g|/2)" row constraint, run as a native MaxCDCL propagator on the split path.-stab-overlap=offrestores the previous search byte for byte.-joint/-roundingsat, the same way the-ub-predefault behaves.test_cc_flags.share updated in the same way as Defaults: -ub-pre=on (MaxSAT) and -ub-search=on (CC); re-tier LP_442/BB_288/LP_714 #147 / Adopt GH-146 Stern finder as default (both engines); tier5 stems get verified upper bounds #149.ADOPT/and the REPORT section).The trade-off for the PI
-stab-overlap=auto5-seed confirmation (yfclab2, cores 0-39, pinned, 4 GB cap, both arms concurrent)
All 40 runs solved with the right answers (18 and 13), with no science issue.
Tier 0 (yfclab2, cores 100-107), PASS on both the merge commit and the default-flip commit
make test-cc(Part G: 3600 runs, 0 bad; mutants 1 and 2 caught),make test-cc-flags(369 / 376 checks, 0 failed) andscripts/smoke_test.shall pass.-stab-overlap=auto|on|off, both modes: 78/78 equal the stems.-vlogs on tier0+1, both modes, compared with frozen main e52d15b, with the flag off: 30/30 identical. This counts after sorting the twoc ub-pre X/Zlines, which main itself prints in either order. The new default equals the merge's explicit-stab-overlap=autoon 30/30.Diagnosis of TN_216 (existing logs only)
Z cap 17NONE proof takes 1.25-1.35x the conflicts and 1.56-1.74x the time. X-half probes are neutral.-frontier=autostatistic. This keeps all BB/LP gains but drops the TN gains.Options for the PI
offas the default and close this PR. The flag stays available.auto(H1 / H2) round, then re-check TN_216 / TN_180 / TN_468.Note
If this is merged, the main baselines must be re-recorded (Tier 0-5) unless the PI waives that. BB_360_12_24 and LP_1122_148_20 become solvable by MaxSAT within 6 h, but in more than 5000 s, so they stay in Tier 5.
🤖 Generated with Claude Code