Repository navigation
[Mac agent] MaxSAT: gate -stab-overlap to remove the TN_216 regression (GH-148 follow-up) #218
Description
Hub: #15. Follow-up of #148 (PR #158, -stab-overlap=auto made the MaxSAT default).
Problem
With -stab-overlap=auto, TN_216_4_18 is slower on 5-seed medians (#148 adoption check):
- no-card 9282 -> 14191 s (1.53x), card-mto 10217 -> 14220 s (1.39x);
- TN_144_2_13 is 1.06-1.09x slower.
This violates the Tier 5 1.2x rule (PI 2026-10-31). The gains to keep: BB_288 0.20x (Tier 2), BB_360 and LP_1122 newly solved at Tier 5, LP_1020 1270 -> 566 s.
Plan
- Diagnose. Instrument both arms (
-stab-overlap=auto/off) on TN_216 and TN_144 with per-probe counters: propagations, conflicts, lookahead work, native-row calls/propagations/conflicts, split by search and lookahead. [Mac agent] MaxSAT path: stabilizer-overlap dominance constraints in every CSS-half probe #148's log analysis already places the loss in the Z-half refutations at caps 16-17 (1.25-1.35x conflicts, about 17 % more time per conflict). - Rule. Design a gating or tuning rule that removes the TN slowdown and keeps the BB/LP gains. The rule only decides whether and how to use a valid constraint (any subset of the verified rows is sound), so probe answers are unchanged.
- Gates. Tier 0 (tests, a mutant), new rule disabled = byte-identical to main; Tiers 1-4 with 5 seeds; Tier 5 6 h with the 1.2x rule, TN_216 against the pre-[Mac agent] MaxSAT path: stabilizer-overlap dominance constraints in every CSS-half probe #148 baseline (12b3e05), BB_360 and LP_1122 still solved.
Server: yfclab2 cores 112-119.
Activity
GH-218: flag tests for -stab-overlap-c4; -v lines carry the gate count
GH-218: fix TN_72_8_8 flag check (rows active only with -stab-overlap…
GH-218: per-half pilot for dense overlap rows (-stab-overlap-pilot=N,…
GH-218: tests for dense rows and the pilot (Part G configs and (c) ch…
GH-218: TN_108 pilot flag check uses pilot cap 1 (P = lb = 9)
GH-218: pilot cap also covers the activation cap of the dense rows (t…
GH-218: TN_108 pilot flag check: cpu limit 60 s (the cap-10 pilot nee…
GH-218: README / MODIFICATIONS entries (soundness: any row subset; pi…
GH-218: default -stab-overlap-pilot=0 (dense rows dropped from cap 16…
GH-218: Tier 0 evidence (tests, identity tiers 0-4, ub-pre caps per s…
Merge main (134d756) into GH-218
GH-218: Tier 5 logs and table; docs point to the experiment directory…
guluchen commentedon Nov 4, 2026
Result: PR #222, not merged; it needs a PI decision.
The rule
-stab-overlap-c4=11drops the dense rows (every weight-9 TN row) from cap 16 on.Mechanism: a search effect in the TN Z half at caps 16-17, not propagator overhead. TN_180's X half gains 0.48-0.66x from the same kind of rows, and no cheap signal tells the two apart (a cap-12 pilot is not predictive). Details are in the PR.
guluchen commentedon Nov 5, 2026
PR #222 closed unmerged by PI decision; GH-148 is kept as is. See #222 for the data.
🤖 Generated with Claude Code